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