Theory of Linear Arithmetic ¶
This example asserts three constraints over an integer variable
x
and a real variable
y
.
Firstly, it checks that these constraints entail an upper bound on the difference
y
-
x
<=
2/3
.
Secondly, it checks that this bound is tight by asserting
y
-
x
=
2/3
and checking for satisfiability.
The two checks are separated by using
push
and
pop
.
examples/api/cpp/linear_arith.cpp
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Tim King, Mathias Preiner
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 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 linear arithmetic solving capabilities and
14 * the push pop of cvc5. This also gives an example option.
15 */
16
17 #include <iostream>
18
19 #include <cvc5/cvc5.h>
20
21 using namespace std;
22 using namespace cvc5;
23
24 int main()
25 {
26 Solver slv;
27 slv.setLogic("QF_LIRA"); // Set the logic
28
29 // Prove that if given x (Integer) and y (Real) then
30 // the maximum value of y - x is 2/3
31
32 // Sorts
33 Sort real = slv.getRealSort();
34 Sort integer = slv.getIntegerSort();
35
36 // Variables
37 Term x = slv.mkConst(integer, "x");
38 Term y = slv.mkConst(real, "y");
39
40 // Constants
41 Term three = slv.mkInteger(3);
42 Term neg2 = slv.mkInteger(-2);
43 Term two_thirds = slv.mkReal(2, 3);
44
45 // Terms
46 Term three_y = slv.mkTerm(MULT, {three, y});
47 Term diff = slv.mkTerm(SUB, {y, x});
48
49 // Formulas
50 Term x_geq_3y = slv.mkTerm(GEQ, {x, three_y});
51 Term x_leq_y = slv.mkTerm(LEQ, {x, y});
52 Term neg2_lt_x = slv.mkTerm(LT, {neg2, x});
53
54 Term assertions = slv.mkTerm(AND, {x_geq_3y, x_leq_y, neg2_lt_x});
55
56 cout << "Given the assertions " << assertions << endl;
57 slv.assertFormula(assertions);
58
59
60 slv.push();
61 Term diff_leq_two_thirds = slv.mkTerm(LEQ, {diff, two_thirds});
62 cout << "Prove that " << diff_leq_two_thirds << " with cvc5." << endl;
63 cout << "cvc5 should report UNSAT." << endl;
64 cout << "Result from cvc5 is: "
65 << slv.checkSatAssuming(diff_leq_two_thirds.notTerm()) << endl;
66 slv.pop();
67
68 cout << endl;
69
70 slv.push();
71 Term diff_is_two_thirds = slv.mkTerm(EQUAL, {diff, two_thirds});
72 slv.assertFormula(diff_is_two_thirds);
73 cout << "Show that the assertions are consistent with " << endl;
74 cout << diff_is_two_thirds << " with cvc5." << endl;
75 cout << "cvc5 should report SAT." << endl;
76 cout << "Result from cvc5 is: " << slv.checkSat() << endl;
77 slv.pop();
78
79 cout << "Thus the maximum value of (y - x) is 2/3."<< endl;
80
81 return 0;
82 }
examples/api/java/LinearArith.java
1 /******************************************************************************
2 * Top contributors (to current version):
3 * Mudathir Mohamed, Morgan Deters, Tim King
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 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 linear arithmetic solving capabilities and
14 * the push pop of cvc5. This also gives an example option.
15 */
16
17 import io.github.cvc5.*;
18 public class LinearArith
19 {
20 public static void main(String args[]) throws CVC5ApiException
21 {
22 try (Solver slv = new Solver())
23 {
24 slv.setLogic("QF_LIRA"); // Set the logic
25
26 // Prove that if given x (Integer) and y (Real) then
27 // the maximum value of y - x is 2/3
28
29 // Sorts
30 Sort real = slv.getRealSort();
31 Sort integer = slv.getIntegerSort();
32
33 // Variables
34 Term x = slv.mkConst(integer, "x");
35 Term y = slv.mkConst(real, "y");
36
37 // Constants
38 Term three = slv.mkInteger(3);
39 Term neg2 = slv.mkInteger(-2);
40 Term two_thirds = slv.mkReal(2, 3);
41
42 // Terms
43 Term three_y = slv.mkTerm(Kind.MULT, three, y);
44 Term diff = slv.mkTerm(Kind.SUB, y, x);
45
46 // Formulas
47 Term x_geq_3y = slv.mkTerm(Kind.GEQ, x, three_y);
48 Term x_leq_y = slv.mkTerm(Kind.LEQ, x, y);
49 Term neg2_lt_x = slv.mkTerm(Kind.LT, neg2, x);
50
51 Term assertions = slv.mkTerm(Kind.AND, x_geq_3y, x_leq_y, neg2_lt_x);
52
53 System.out.println("Given the assertions " + assertions);
54 slv.assertFormula(assertions);
55
56 slv.push();
57 Term diff_leq_two_thirds = slv.mkTerm(Kind.LEQ, diff, two_thirds);
58 System.out.println("Prove that " + diff_leq_two_thirds + " with cvc5.");
59 System.out.println("cvc5 should report UNSAT.");
60 System.out.println(
61 "Result from cvc5 is: " + slv.checkSatAssuming(diff_leq_two_thirds.notTerm()));
62 slv.pop();
63
64 System.out.println();
65
66 slv.push();
67 Term diff_is_two_thirds = slv.mkTerm(Kind.EQUAL, diff, two_thirds);
68 slv.assertFormula(diff_is_two_thirds);
69 System.out.println("Show that the assertions are consistent with ");
70 System.out.println(diff_is_two_thirds + " with cvc5.");
71 System.out.println("cvc5 should report SAT.");
72 System.out.println("Result from cvc5 is: " + slv.checkSat());
73 slv.pop();
74
75 System.out.println("Thus the maximum value of (y - x) is 2/3.");
76 }
77 }
78 }
examples/api/python/pythonic/linear_arith.py
1 from cvc5.pythonic import *
2
3 slv = SolverFor('QF_LIRA')
4
5 x = Int('x')
6 y = Real('y')
7
8 slv += And(x >= 3 * y, x <= y, -2 < x)
9 slv.push()
10 print(slv.check(y-x <= 2/3))
11 slv.pop()
12 slv.push()
13 slv += y-x == 2/3
14 print(slv.check())
15 slv.pop()
examples/api/python/linear_arith.py
1 #!/usr/bin/env python
2 ###############################################################################
3 # Top contributors (to current version):
4 # Makai Mann, Aina Niemetz, Mathias Preiner
5 #
6 # This file is part of the cvc5 project.
7 #
8 # Copyright (c) 2009-2022 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 linear
15 # arithmetic solver through the Python API. This is a direct translation of
16 # linear_arith-new.cpp.
17 ##
18
19 import cvc5
20 from cvc5 import Kind
21
22 if __name__ == "__main__":
23 slv = cvc5.Solver()
24 slv.setLogic("QF_LIRA")
25
26 # Prove that if given x (Integer) and y (Real) and some constraints
27 # then the maximum value of y - x is 2/3
28
29 # Sorts
30 real = slv.getRealSort()
31 integer = slv.getIntegerSort()
32
33 # Variables
34 x = slv.mkConst(integer, "x")
35 y = slv.mkConst(real, "y")
36
37 # Constants
38 three = slv.mkInteger(3)
39 neg2 = slv.mkInteger(-2)
40 two_thirds = slv.mkReal(2, 3)
41
42 # Terms
43 three_y = slv.mkTerm(Kind.MULT, three, y)
44 diff = slv.mkTerm(Kind.SUB, y, x)
45
46 # Formulas
47 x_geq_3y = slv.mkTerm(Kind.GEQ, x, three_y)
48 x_leq_y = slv.mkTerm(Kind.LEQ, x ,y)
49 neg2_lt_x = slv.mkTerm(Kind.LT, neg2, x)
50
51 assertions = slv.mkTerm(Kind.AND, x_geq_3y, x_leq_y, neg2_lt_x)
52
53 print("Given the assertions", assertions)
54 slv.assertFormula(assertions)
55
56 slv.push()
57 diff_leq_two_thirds = slv.mkTerm(Kind.LEQ, diff, two_thirds)
58 print("Prove that", diff_leq_two_thirds, "with cvc5")
59 print("cvc5 should report UNSAT")
60 print("Result from cvc5 is:",
61 slv.checkSatAssuming(diff_leq_two_thirds.notTerm()))
62 slv.pop()
63
64 print()
65
66 slv.push()
67 diff_is_two_thirds = slv.mkTerm(Kind.EQUAL, diff, two_thirds)
68 slv.assertFormula(diff_is_two_thirds)
69 print("Show that the assertions are consistent with\n", diff_is_two_thirds, "with cvc5")
70 print("cvc5 should report SAT")
71 print("Result from cvc5 is:", slv.checkSat())
72 slv.pop()
examples/api/smtlib/linear_arith.smt2
1 (set-logic QF_LIRA)
2 (declare-const x Int)
3 (declare-const y Real)
4 (assert
5 (and
6 (>= x (* 3 y))
7 (<= x y)
8 (< (- 2) x)
9 )
10 )
11 (push 1)
12 (echo "Checking entailement by asserting the negation")
13 (echo "Unsat == ENTAILED")
14 (assert (not (<= (- y x) (/ 2 3))))
15 (check-sat)
16 (pop 1)
17 (push 1)
18 (echo "Checking that the assertions are consistent")
19 (assert (= (- y x) (/ 2 3)))
20 (check-sat)
21 (pop 1)