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