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
21using namespace std;
22using namespace cvc5;
23
24int 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(Kind::MULT, {three, y});
47  Term diff = slv.mkTerm(Kind::SUB, {y, x});
48
49  // Formulas
50  Term x_geq_3y = slv.mkTerm(Kind::GEQ, {x, three_y});
51  Term x_leq_y = slv.mkTerm(Kind::LEQ, {x, y});
52  Term neg2_lt_x = slv.mkTerm(Kind::LT, {neg2, x});
53
54  Term assertions = slv.mkTerm(Kind::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(Kind::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(Kind::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}