mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity

new qe example

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-02 12:04:02 -07:00
parent 230382d4c9
commit e08c569d8d
1 changed files with 27 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

27
examples/c++/example.cpp
View file

@ -633,6 +633,32 @@ void tactic_example9() {
std::cout << t(g) << "\n";
}
void tactic_qe() {
std::cout << "tactic example using quantifier elimination\n";
context c;
// Create a solver using "qe" and "smt" tactics
solver s =
(tactic(c, "qe") &
tactic(c, "smt")).mk_solver();
expr a = c.int_const("a");
expr b = c.int_const("b");
expr x = c.int_const("x");
expr f = implies(x <= a, x < b);
// We have to use the C API directly for creating quantified formulas.
Z3_app vars[] = {(Z3_app) x};
expr qf = to_expr(c, Z3_mk_forall_const(c, 0, 1, vars,
0, 0, // no pattern
f));
std::cout << qf << "\n";
s.add(qf);
std::cout << s.check() << "\n";
std::cout << s.get_model() << "\n";
}
void visit(expr const & e) {
if (e.is_app()) {
unsigned num = e.num_args();
@ -691,6 +717,7 @@ int main() {
tactic_example7(); std::cout << "\n";
tactic_example8(); std::cout << "\n";
tactic_example9(); std::cout << "\n";
tactic_qe(); std::cout << "\n";
tst_visit(); std::cout << "\n";
std::cout << "done\n";
}