Theory of Uninterpreted Functions
1/******************************************************************************
2 * Top contributors (to current version):
3 * Yoni Zohar
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the capabilities of the cvc5 uf solver.
14 */
15
16#include <cvc5/cvc5.h>
17
18#include <iostream>
19
20using namespace cvc5;
21
22int main()
23{
24 TermManager tm;
25 Solver slv(tm);
26 slv.setLogic("QF_UF");
27
28 // Sorts
29 Sort u = tm.mkUninterpretedSort("U");
30 Sort boolean = tm.getBooleanSort();
31 Sort uTou = tm.mkFunctionSort({u}, u);
32 Sort uPred = tm.mkFunctionSort({u}, boolean);
33
34 // Variables
35 Term x = tm.mkConst(u, "x");
36 Term y = tm.mkConst(u, "y");
37
38 // Functions
39 Term f = tm.mkConst(uTou, "f");
40 Term p = tm.mkConst(uPred, "p");
41
42 // Terms
43 Term f_x = tm.mkTerm(Kind::APPLY_UF, {f, x});
44 Term f_y = tm.mkTerm(Kind::APPLY_UF, {f, y});
45 Term p_f_x = tm.mkTerm(Kind::APPLY_UF, {p, f_x});
46 Term p_f_y = tm.mkTerm(Kind::APPLY_UF, {p, f_y});
47
48 // Construct the assertions
49 Term assertions =
50 tm.mkTerm(Kind::AND,
51 {
52 tm.mkTerm(Kind::EQUAL, {x, f_x}),
53 tm.mkTerm(Kind::EQUAL, {y, f_y}),
54 p_f_x.notTerm(),
55 p_f_y
56 });
57 slv.assertFormula(assertions);
58
59 std::cout << slv.checkSat() << std::endl;
60
61 return 0;
62}
1/******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the capabilities of the cvc5 uf solver.
14 */
15
16#include <cvc5/c/cvc5.h>
17#include <stdio.h>
18
19int main()
20{
21 Cvc5TermManager* tm = cvc5_term_manager_new();
22 Cvc5* slv = cvc5_new(tm);
23 cvc5_set_logic(slv, "QF_UF");
24
25 // Sorts
26 Cvc5Sort un_sort = cvc5_mk_uninterpreted_sort(tm, "U");
27 Cvc5Sort bool_sort = cvc5_get_boolean_sort(tm);
28 Cvc5Sort domain[1] = {un_sort};
29 Cvc5Sort un_to_un_sort = cvc5_mk_fun_sort(tm, 1, domain, un_sort);
30 Cvc5Sort un_pred_sort = cvc5_mk_fun_sort(tm, 1, domain, bool_sort);
31
32 // Variables
33 Cvc5Term x = cvc5_mk_const(tm, un_sort, "x");
34 Cvc5Term y = cvc5_mk_const(tm, un_sort, "y");
35
36 // Functions
37 Cvc5Term f = cvc5_mk_const(tm, un_to_un_sort, "f");
38 Cvc5Term p = cvc5_mk_const(tm, un_pred_sort, "p");
39
40 // Terms
41 Cvc5Term args2[2] = {f, x};
42 Cvc5Term f_x = cvc5_mk_term(tm, CVC5_KIND_APPLY_UF, 2, args2);
43 args2[1] = y;
44 Cvc5Term f_y = cvc5_mk_term(tm, CVC5_KIND_APPLY_UF, 2, args2);
45 args2[0] = p;
46 args2[1] = f_x;
47 Cvc5Term p_f_x = cvc5_mk_term(tm, CVC5_KIND_APPLY_UF, 2, args2);
48 args2[1] = f_y;
49 Cvc5Term p_f_y = cvc5_mk_term(tm, CVC5_KIND_APPLY_UF, 2, args2);
50
51 // Construct the assertions
52 Cvc5Term not_p_f_x = cvc5_mk_term(tm, CVC5_KIND_NOT, 1, &p_f_x);
53 args2[0] = x;
54 args2[1] = f_x;
55 Cvc5Term eq1 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
56 args2[0] = y;
57 args2[1] = f_y;
58 Cvc5Term eq2 = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
59 args2[0] = eq1;
60 args2[1] = eq2;
61 cvc5_assert_formula(slv, cvc5_mk_term(tm, CVC5_KIND_AND, 2, args2));
62 cvc5_assert_formula(slv, not_p_f_x);
63 cvc5_assert_formula(slv, p_f_y);
64
65 printf("%s\n", cvc5_result_to_string(cvc5_check_sat(slv)));
66
67 cvc5_delete(slv);
68 cvc5_term_manager_delete(tm);
69 return 0;
70}
1/******************************************************************************
2 * Top contributors (to current version):
3 * Yoni Zohar
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
12 *
13 * A simple demonstration of the capabilities of the cvc5 uf solver.
14 */
15
16import io.github.cvc5.*;
17import java.util.Iterator;
18
19public class Uf
20{
21 public static void main(String[] args) throws CVC5ApiException
22 {
23 Solver slv = new Solver();
24 {
25 slv.setLogic("QF_UF");
26
27 // Sorts
28 Sort u = slv.mkUninterpretedSort("U");
29 Sort bool = slv.getBooleanSort();
30 Sort uTou = slv.mkFunctionSort(u, u);
31 Sort uPred = slv.mkFunctionSort(u, bool);
32
33 // Variables
34 Term x = slv.mkConst(u, "x");
35 Term y = slv.mkConst(u, "y");
36
37 // Functions
38 Term f = slv.mkConst(uTou, "f");
39 Term p = slv.mkConst(uPred, "p");
40
41 // Terms
42 Term f_x = slv.mkTerm(Kind.APPLY_UF, f, x);
43 Term f_y = slv.mkTerm(Kind.APPLY_UF, f, y);
44 Term p_f_x = slv.mkTerm(Kind.APPLY_UF, p, f_x);
45 Term p_f_y = slv.mkTerm(Kind.APPLY_UF, p, f_y);
46
47 // Construct the assertions
48 Term assertions = slv.mkTerm(Kind.AND,
49 new Term[] {
50 slv.mkTerm(Kind.EQUAL, x, f_x),
51 slv.mkTerm(Kind.EQUAL, y, f_y),
52 p_f_x.notTerm(),
53 p_f_y
54 });
55 slv.assertFormula(assertions);
56
57 System.out.println("Call checkSat to show that the assertions are satisfiable. \n"
58 + "cvc5: " + slv.checkSat() + ".\n");
59
60 Context.deletePointers();
61 }
62 }
63}
examples/api/python/pythonic/uf.py
1###############################################################################
2# Top contributors (to current version):
3# Yoni Zohar
4#
5# This file is part of the cvc5 project.
6#
7# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8# in the top-level source directory and their institutional affiliations.
9# All rights reserved. See the file COPYING in the top-level source
10# directory for licensing information.
11# #############################################################################
12#
13# A simple demonstration of the capabilities of the cvc5 uf solver.
14##
15from cvc5.pythonic import *
16
17if __name__ == "__main__":
18
19 U = DeclareSort("U")
20 x, y = Consts("x y", U)
21
22 f = Function("f", U, U)
23 p = Function("p", U, BoolSort())
24
25 assumptions = [f(x) == x, f(y) == y, Not(p(f(x))), p(f(y))]
26
27 s = Solver()
28 s.add(assumptions)
29 assert sat == s.check()
1#!/usr/bin/env python
2###############################################################################
3# Top contributors (to current version):
4# Yoni Zohar
5#
6# This file is part of the cvc5 project.
7#
8# Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
9# in the top-level source directory and their institutional affiliations.
10# All rights reserved. See the file COPYING in the top-level source
11# directory for licensing information.
12# #############################################################################
13#
14# A simple demonstration of the solving capabilities of the cvc5 uf solver.
15##
16
17import cvc5
18from cvc5 import Kind
19
20if __name__ == "__main__":
21 tm = cvc5.TermManager()
22 slv = cvc5.Solver(tm)
23 slv.setLogic("QF_UF")
24
25 # Sorts
26 u = tm.mkUninterpretedSort("U")
27 integer = tm.getIntegerSort()
28 boolean = tm.getBooleanSort()
29 uTou = tm.mkFunctionSort(u, u)
30 uPred = tm.mkFunctionSort(u, boolean)
31
32 # Variables
33 x = tm.mkConst(u, "x")
34 y = tm.mkConst(u, "y")
35
36 # Functions
37 f = tm.mkConst(uTou, "f")
38 p = tm.mkConst(uPred, "p")
39
40
41 # Terms
42 f_x = tm.mkTerm(Kind.APPLY_UF, f, x)
43 f_y = tm.mkTerm(Kind.APPLY_UF, f, y)
44 p_f_x = tm.mkTerm(Kind.APPLY_UF, p, f_x)
45 p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y)
46
47 # Construct the assertions
48 assertions = tm.mkTerm(Kind.AND,
49 tm.mkTerm(Kind.EQUAL, x, f_x),
50 tm.mkTerm(Kind.EQUAL, y, f_y),
51 p_f_x.notTerm(),
52 p_f_y)
53
54 slv.assertFormula(assertions)
55 assert(slv.checkSat().isSat())
56
1(set-logic QF_UF)
2
3(declare-sort U 0)
4
5(declare-const x U)
6(declare-const y U)
7
8(declare-fun f (U) U)
9(declare-fun p (U) Bool)
10
11(assert (= x (f x)))
12(assert (= y (f y)))
13(assert (not (p (f x))))
14(assert (p (f y)))
15
16(check-sat)