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, Haniel Barbosa
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 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
21using namespace std;
22using namespace cvc5;
23
24int main()
25{
26 TermManager tm;
27 Solver slv(tm);
28 slv.setLogic("QF_LIRA"); // Set the logic
29
30 // Prove that if given x (Integer) and y (Real) then
31 // the maximum value of y - x is 2/3
32
33 // Sorts
34 Sort real = tm.getRealSort();
35 Sort integer = tm.getIntegerSort();
36
37 // Variables
38 Term x = tm.mkConst(integer, "x");
39 Term y = tm.mkConst(real, "y");
40
41 // Constants
42 Term three = tm.mkInteger(3);
43 Term neg2 = tm.mkInteger(-2);
44 Term two_thirds = tm.mkReal(2, 3);
45
46 // Terms
47 Term three_y = tm.mkTerm(Kind::MULT, {three, y});
48 Term diff = tm.mkTerm(Kind::SUB, {y, x});
49
50 // Formulas
51 Term x_geq_3y = tm.mkTerm(Kind::GEQ, {x, three_y});
52 Term x_leq_y = tm.mkTerm(Kind::LEQ, {x, y});
53 Term neg2_lt_x = tm.mkTerm(Kind::LT, {neg2, x});
54
55 Term assertions = tm.mkTerm(Kind::AND, {x_geq_3y, x_leq_y, neg2_lt_x});
56
57 cout << "Given the assertions " << assertions << endl;
58 slv.assertFormula(assertions);
59
60
61 slv.push();
62 Term diff_leq_two_thirds = tm.mkTerm(Kind::LEQ, {diff, two_thirds});
63 cout << "Prove that " << diff_leq_two_thirds << " with cvc5." << endl;
64 cout << "cvc5 should report UNSAT." << endl;
65 cout << "Result from cvc5 is: "
66 << slv.checkSatAssuming(diff_leq_two_thirds.notTerm()) << endl;
67 slv.pop();
68
69 cout << endl;
70
71 slv.push();
72 Term diff_is_two_thirds = tm.mkTerm(Kind::EQUAL, {diff, two_thirds});
73 slv.assertFormula(diff_is_two_thirds);
74 cout << "Show that the assertions are consistent with " << endl;
75 cout << diff_is_two_thirds << " with cvc5." << endl;
76 cout << "cvc5 should report SAT." << endl;
77 cout << "Result from cvc5 is: " << slv.checkSat() << endl;
78 slv.pop();
79
80 cout << "Thus the maximum value of (y - x) is 2/3."<< endl;
81
82 return 0;
83}
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 linear arithmetic solving capabilities and
14 * the push pop of cvc5. This also gives an example option.
15 */
16
17#include <cvc5/c/cvc5.h>
18#include <stdio.h>
19
20int main()
21{
22 Cvc5TermManager* tm = cvc5_term_manager_new();
23 Cvc5* slv = cvc5_new(tm);
24 cvc5_set_logic(slv, "QF_LIRA");
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 Cvc5Sort real = cvc5_get_real_sort(tm);
31 Cvc5Sort integer = cvc5_get_integer_sort(tm);
32
33 // Variables
34 Cvc5Term x = cvc5_mk_const(tm, integer, "x");
35 Cvc5Term y = cvc5_mk_const(tm, real, "y");
36
37 // Constants
38 Cvc5Term three = cvc5_mk_integer_int64(tm, 3);
39 Cvc5Term neg2 = cvc5_mk_integer_int64(tm, -2);
40 Cvc5Term two_thirds = cvc5_mk_real_num_den(tm, 2, 3);
41
42 // Terms
43 Cvc5Term args2[2] = {three, y};
44 Cvc5Term three_y = cvc5_mk_term(tm, CVC5_KIND_MULT, 2, args2);
45 args2[0] = y;
46 args2[1] = x;
47 Cvc5Term diff = cvc5_mk_term(tm, CVC5_KIND_SUB, 2, args2);
48
49 // Formulas
50 args2[0] = x;
51 args2[1] = three_y;
52 Cvc5Term x_geq_3y = cvc5_mk_term(tm, CVC5_KIND_GEQ, 2, args2);
53 args2[0] = x;
54 args2[1] = y;
55 Cvc5Term x_leq_y = cvc5_mk_term(tm, CVC5_KIND_LEQ, 2, args2);
56 args2[0] = neg2;
57 args2[1] = x;
58 Cvc5Term neg2_lt_x = cvc5_mk_term(tm, CVC5_KIND_LT, 2, args2);
59
60 Cvc5Term args3[3] = {x_geq_3y, x_leq_y, neg2_lt_x};
61 Cvc5Term assertions = cvc5_mk_term(tm, CVC5_KIND_AND, 3, args3);
62
63 printf("Given the assertions %s\n", cvc5_term_to_string(assertions));
64 cvc5_assert_formula(slv, assertions);
65
66 cvc5_push(slv, 1);
67 args2[0] = diff;
68 args2[1] = two_thirds;
69 Cvc5Term diff_leq_two_thirds = cvc5_mk_term(tm, CVC5_KIND_LEQ, 2, args2);
70 printf("Prove that %s with cvc5.\n",
71 cvc5_term_to_string(diff_leq_two_thirds));
72 printf("cvc5 should report UNSAT.\n");
73 Cvc5Term args1[1] = {diff_leq_two_thirds};
74 Cvc5Term assumptions[1] = {cvc5_mk_term(tm, CVC5_KIND_NOT, 1, args1)};
75 printf("Result from cvc5 is: %s\n\n",
76 cvc5_result_to_string(cvc5_check_sat_assuming(slv, 1, assumptions)));
77 cvc5_pop(slv, 1);
78
79 cvc5_push(slv, 1);
80 args2[0] = diff;
81 args2[1] = two_thirds;
82 Cvc5Term diff_is_two_thirds = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
83 cvc5_assert_formula(slv, diff_is_two_thirds);
84 printf("Show that the assertions are consistent with \n");
85 printf("%s with cvc5.\n", cvc5_term_to_string(diff_is_two_thirds));
86 printf("cvc5 should report SAT.\n");
87 printf("Result from cvc5 is: %s\n",
88 cvc5_result_to_string(cvc5_check_sat(slv)));
89 cvc5_pop(slv, 1);
90
91 printf("Thus the maximum value of (y - x) is 2/3.\n");
92
93 cvc5_delete(slv);
94 cvc5_term_manager_delete(tm);
95 return 0;
96}
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-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 linear arithmetic solving capabilities and
14 * the push pop of cvc5. This also gives an example option.
15 */
16
17import io.github.cvc5.*;
18public class LinearArith
19{
20 public static void main(String args[]) throws CVC5ApiException
21 {
22 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 Context.deletePointers();
78 }
79}
examples/api/python/pythonic/linear_arith.py
1###############################################################################
2# Top contributors (to current version):
3# Alex Ozdemir
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 linear arithmetic solving capabilities and
14# the push pop of cvc5. This also gives an example option.
15##
16from cvc5.pythonic import *
17
18slv = SolverFor('QF_LIRA')
19
20x = Int('x')
21y = Real('y')
22
23slv += And(x >= 3 * y, x <= y, -2 < x)
24slv.push()
25print(slv.check(y-x <= 2/3))
26slv.pop()
27slv.push()
28slv += y-x == 2/3
29print(slv.check())
30slv.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-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 linear
15# arithmetic solver through the Python API. This is a direct translation of
16# linear_arith-new.cpp.
17##
18
19import cvc5
20from cvc5 import Kind
21
22if __name__ == "__main__":
23 tm = cvc5.TermManager()
24 slv = cvc5.Solver(tm)
25 slv.setLogic("QF_LIRA")
26
27 # Prove that if given x (Integer) and y (Real) and some constraints
28 # then the maximum value of y - x is 2/3
29
30 # Sorts
31 real = tm.getRealSort()
32 integer = tm.getIntegerSort()
33
34 # Variables
35 x = tm.mkConst(integer, "x")
36 y = tm.mkConst(real, "y")
37
38 # Constants
39 three = tm.mkInteger(3)
40 neg2 = tm.mkInteger(-2)
41 two_thirds = tm.mkReal(2, 3)
42
43 # Terms
44 three_y = tm.mkTerm(Kind.MULT, three, y)
45 diff = tm.mkTerm(Kind.SUB, y, x)
46
47 # Formulas
48 x_geq_3y = tm.mkTerm(Kind.GEQ, x, three_y)
49 x_leq_y = tm.mkTerm(Kind.LEQ, x ,y)
50 neg2_lt_x = tm.mkTerm(Kind.LT, neg2, x)
51
52 assertions = tm.mkTerm(Kind.AND, x_geq_3y, x_leq_y, neg2_lt_x)
53
54 print("Given the assertions", assertions)
55 slv.assertFormula(assertions)
56
57 slv.push()
58 diff_leq_two_thirds = tm.mkTerm(Kind.LEQ, diff, two_thirds)
59 print("Prove that", diff_leq_two_thirds, "with cvc5")
60 print("cvc5 should report UNSAT")
61 print("Result from cvc5 is:",
62 slv.checkSatAssuming(diff_leq_two_thirds.notTerm()))
63 slv.pop()
64
65 print()
66
67 slv.push()
68 diff_is_two_thirds = tm.mkTerm(Kind.EQUAL, diff, two_thirds)
69 slv.assertFormula(diff_is_two_thirds)
70 print("Show that the assertions are consistent with\n", diff_is_two_thirds, "with cvc5")
71 print("cvc5 should report SAT")
72 print("Result from cvc5 is:", slv.checkSat())
73 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)