1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andres Noetzli, Morgan Deters, Mudathir Mohamed
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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 * ****************************************************************************
13 * A simple demonstration of the C++ interface
15 * Compare to the Java interface in SimpleVC.java; they are virtually
16 * line-by-line identical.
19 #include <cvc5/cvc5.h>
28 // Prove that for integers x and y:
29 // x > 0 AND y > 0 => 2x + y >= 3
31 Sort integer
= slv
.getIntegerSort();
33 Term x
= slv
.mkConst(integer
, "x");
34 Term y
= slv
.mkConst(integer
, "y");
35 Term zero
= slv
.mkInteger(0);
37 Term x_positive
= slv
.mkTerm(Kind::GT
, {x
, zero
});
38 Term y_positive
= slv
.mkTerm(Kind::GT
, {y
, zero
});
40 Term two
= slv
.mkInteger(2);
41 Term twox
= slv
.mkTerm(Kind::MULT
, {two
, x
});
42 Term twox_plus_y
= slv
.mkTerm(Kind::ADD
, {twox
, y
});
44 Term three
= slv
.mkInteger(3);
45 Term twox_plus_y_geq_3
= slv
.mkTerm(Kind::GEQ
, {twox_plus_y
, three
});
47 Term formula
= slv
.mkTerm(Kind::AND
, {x_positive
, y_positive
})
48 .impTerm(twox_plus_y_geq_3
);
50 std::cout
<< "Checking entailment of formula " << formula
<< " with cvc5."
52 std::cout
<< "cvc5 should report UNSAT." << std::endl
;
53 std::cout
<< "Result from cvc5 is: "
54 << slv
.checkSatAssuming(formula
.notTerm()) << std::endl
;