1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
/******************************************************************************
* Top contributors (to current version):
* Mudathir Mohamed, Daniel Larraz, Morgan Deters
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* A simple demonstration of the capabilities of cvc5
*
* A simple demonstration of how to use uninterpreted functions, combining this
* with arithmetic, and extracting a model at the end of a satisfiable query.
* The model is displayed using getValue().
*/
import io.github.cvc5.*;
import java.util.Iterator;
public class Combination
{
private static void prefixPrintGetValue(Solver slv, Term t)
{
prefixPrintGetValue(slv, t, 0);
}
private static void prefixPrintGetValue(Solver slv, Term t, int level)
{
System.out.println("slv.getValue(" + t + "): " + slv.getValue(t));
for (Term c : t)
{
prefixPrintGetValue(slv, c, level + 1);
}
}
public static void main(String[] args) throws CVC5ApiException
{
TermManager tm = new TermManager();
Solver slv = new Solver(tm);
{
slv.setOption("produce-models", "true"); // Produce Models
slv.setOption("dag-thresh", "0"); // Disable dagifying the output
slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language
slv.setLogic("QF_UFLIRA");
// Sorts
Sort u = tm.mkUninterpretedSort("u");
Sort integer = tm.getIntegerSort();
Sort bool = tm.getBooleanSort();
Sort uToInt = tm.mkFunctionSort(u, integer);
Sort intPred = tm.mkFunctionSort(integer, bool);
// Variables
Term x = tm.mkConst(u, "x");
Term y = tm.mkConst(u, "y");
// Functions
Term f = tm.mkConst(uToInt, "f");
Term p = tm.mkConst(intPred, "p");
// Constants
Term zero = tm.mkInteger(0);
Term one = tm.mkInteger(1);
// Terms
Term f_x = tm.mkTerm(Kind.APPLY_UF, f, x);
Term f_y = tm.mkTerm(Kind.APPLY_UF, f, y);
Term sum = tm.mkTerm(Kind.ADD, f_x, f_y);
Term p_0 = tm.mkTerm(Kind.APPLY_UF, p, zero);
Term p_f_y = tm.mkTerm(Kind.APPLY_UF, p, f_y);
// Construct the assertions
Term assertions = tm.mkTerm(Kind.AND,
new Term[] {
tm.mkTerm(Kind.LEQ, zero, f_x), // 0 <= f(x)
tm.mkTerm(Kind.LEQ, zero, f_y), // 0 <= f(y)
tm.mkTerm(Kind.LEQ, sum, one), // f(x) + f(y) <= 1
p_0.notTerm(), // not p(0)
p_f_y // p(f(y))
});
slv.assertFormula(assertions);
System.out.println("Given the following assertions:\n" + assertions + "\n");
System.out.println("Prove x /= y is entailed. \n"
+ "cvc5: " + slv.checkSatAssuming(tm.mkTerm(Kind.EQUAL, x, y)) + ".\n");
System.out.println("Call checkSat to show that the assertions are satisfiable. \n"
+ "cvc5: " + slv.checkSat() + ".\n");
System.out.println("Call slv.getValue(...) on terms of interest.");
System.out.println("slv.getValue(" + f_x + "): " + slv.getValue(f_x));
System.out.println("slv.getValue(" + f_y + "): " + slv.getValue(f_y));
System.out.println("slv.getValue(" + sum + "): " + slv.getValue(sum));
System.out.println("slv.getValue(" + p_0 + "): " + slv.getValue(p_0));
System.out.println("slv.getValue(" + p_f_y + "): " + slv.getValue(p_f_y) + "\n");
System.out.println("Alternatively, iterate over assertions and call slv.getValue(...) "
+ "on all terms.");
prefixPrintGetValue(slv, assertions);
System.out.println();
System.out.println("You can also use nested loops to iterate over terms.");
Iterator<Term> it1 = assertions.iterator();
while (it1.hasNext())
{
Term t = it1.next();
System.out.println("term: " + t);
Iterator<Term> it2 = t.iterator();
while (it2.hasNext())
{
System.out.println(" + child: " + it2.next());
}
}
System.out.println();
System.out.println("Alternatively, you can also use for-each loops.");
for (Term t : assertions)
{
System.out.println("term: " + t);
for (Term c : t)
{
System.out.println(" + child: " + c);
}
}
}
Context.deletePointers();
}
}
|
