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}