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
|
/******************************************************************************
* Top contributors (to current version):
* Aina Niemetz, Tim King, Mudathir Mohamed
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 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 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
{
Solver slv = new Solver();
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 = slv.mkUninterpretedSort("u");
Sort integer = slv.getIntegerSort();
Sort bool = slv.getBooleanSort();
Sort uToInt = slv.mkFunctionSort(u, integer);
Sort intPred = slv.mkFunctionSort(integer, bool);
// Variables
Term x = slv.mkConst(u, "x");
Term y = slv.mkConst(u, "y");
// Functions
Term f = slv.mkConst(uToInt, "f");
Term p = slv.mkConst(intPred, "p");
// Constants
Term zero = slv.mkInteger(0);
Term one = slv.mkInteger(1);
// Terms
Term f_x = slv.mkTerm(Kind.APPLY_UF, f, x);
Term f_y = slv.mkTerm(Kind.APPLY_UF, f, y);
Term sum = slv.mkTerm(Kind.PLUS, f_x, f_y);
Term p_0 = slv.mkTerm(Kind.APPLY_UF, p, zero);
Term p_f_y = slv.mkTerm(Kind.APPLY_UF, p, f_y);
// Construct the assertions
Term assertions = slv.mkTerm(Kind.AND,
new Term[] {
slv.mkTerm(Kind.LEQ, zero, f_x), // 0 <= f(x)
slv.mkTerm(Kind.LEQ, zero, f_y), // 0 <= f(y)
slv.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.checkEntailed(slv.mkTerm(Kind.DISTINCT, 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);
}
}
}
}
|
