mirror of
https://github.com/Z3Prover/z3
synced 2025-10-30 11:12:28 +00:00
resurrected test/quant_elim.cpp
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura
parent
6580a83594
commit
10b95de82e
1 changed files with 500 additions and 0 deletions
500
src/test/quant_elim.cpp
Normal file
500
src/test/quant_elim.cpp
Normal file
|
|
@ -0,0 +1,500 @@
|
|||
#include "ast.h"
|
||||
#include "front_end_params.h"
|
||||
#include "simplifier.h"
|
||||
#include "qe.h"
|
||||
#include "basic_simplifier_plugin.h"
|
||||
#include "arith_simplifier_plugin.h"
|
||||
#include "array_simplifier_plugin.h"
|
||||
#include "bv_simplifier_plugin.h"
|
||||
#include "ast_pp.h"
|
||||
#include "smtlib.h"
|
||||
#include "smtparser.h"
|
||||
#include "lbool.h"
|
||||
#include <sstream>
|
||||
#include "reg_decl_plugins.h"
|
||||
|
||||
|
||||
static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char const* option) {
|
||||
|
||||
// enable_trace("bit2int");
|
||||
//enable_trace("gomory_cut");
|
||||
enable_trace("final_check_arith");
|
||||
enable_trace("arith_final_check");
|
||||
//enable_trace("arith_branching");
|
||||
enable_trace("theory_arith_int");
|
||||
enable_trace("presburger");
|
||||
enable_trace("quant_elim");
|
||||
// enable_trace("arith_simplifier_plugin");
|
||||
// enable_trace("non_linear");
|
||||
// enable_trace("gomory_cut_detail");
|
||||
// enable_trace("arith");
|
||||
// enable_trace("bv");
|
||||
// enable_trace("after_search");
|
||||
// enable_trace("bv_bit_prop");
|
||||
|
||||
simplifier simp(m);
|
||||
front_end_params params;
|
||||
params.m_quant_elim = true;
|
||||
|
||||
std::cout << mk_pp(fml, m) << "\n";
|
||||
qe::expr_quant_elim qe(m, params);
|
||||
expr_ref result(m);
|
||||
qe(m.mk_true(), fml, result);
|
||||
std::cout << " -> " << mk_pp(result, m) << " " << expected_outcome << "\n";
|
||||
if (expected_outcome == l_true && !m.is_true(result)) {
|
||||
std::cout << "ERROR: expected true, instead got " << ast_pp(result, m).c_str() << "\n";
|
||||
//exit(-1);
|
||||
}
|
||||
if (expected_outcome == l_false && !m.is_false(result)) {
|
||||
std::cout << "ERROR: expected false, instead got " << ast_pp(result, m).c_str() << "\n";
|
||||
//exit(-1);
|
||||
}
|
||||
}
|
||||
|
||||
static void test_formula(lbool expected_outcome, char const* fml) {
|
||||
ast_manager m;
|
||||
reg_decl_plugins(m);
|
||||
scoped_ptr<smtlib::parser> parser = smtlib::parser::create(m);
|
||||
parser->initialize_smtlib();
|
||||
|
||||
std::ostringstream buffer;
|
||||
buffer << "(benchmark presburger :status unknown :logic AUFLIA :extrapreds ((p1) (p2) (p3)) "
|
||||
<< ":extrafuns ((a Int) (b Int))\n"
|
||||
<< ":extrapreds ((p) (q) (r))\n"
|
||||
<< ":datatypes ((list (nil) (cons (hd Int) (tl list))))\n"
|
||||
<< ":datatypes ((cell (cnil) (ccons (car cell) (cdr cell))))\n"
|
||||
<< ":extrasorts (U)\n"
|
||||
<< ":extrafuns ((f U U))\n"
|
||||
<< ":formula " << fml << ")";
|
||||
parser->parse_string(buffer.str().c_str());
|
||||
smtlib::benchmark* b = parser->get_benchmark();
|
||||
smtlib::theory::expr_iterator it = b->begin_formulas();
|
||||
smtlib::theory::expr_iterator end = b->end_formulas();
|
||||
for (; it != end; ++it) {
|
||||
test_qe(m, expected_outcome, *it, 0);
|
||||
}
|
||||
}
|
||||
|
||||
void tst_quant_elim() {
|
||||
|
||||
test_formula(l_undef, "(exists ((p1 Bool) (q1 Bool) (r1 Bool))\
|
||||
(and (or (not p1) (not q1) r1)\
|
||||
(or (and (not p) (not q) (not p1) q1)\
|
||||
(and (not p) q p1 (not q1))\
|
||||
(and p (not q) p1 q1)\
|
||||
(and p q p1 q1))\
|
||||
(or (and (not r) (not r1))\
|
||||
(and (= p p1) (= q q1) r r1)\
|
||||
(and (not (and (= p p1) (= q q1))) (not (= r r1))))))");
|
||||
|
||||
|
||||
test_formula(l_false,"(forall (x Int) (y Int) (or (= x 0) (< (* 5 y) (* 6 x)) (> (* 5 y) (* 6 x))))");
|
||||
|
||||
test_formula(l_false, "(forall (a Int) (b Int) (exists (x Int) (and (< a (* 20 x)) (< (* 20 x) b))))");
|
||||
|
||||
test_formula(l_undef, "(exists (u U) (= (f u) u))");
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (l Int) (forall (x Int) (implies (>= x l) "
|
||||
" (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 7 v))))))))");
|
||||
|
||||
|
||||
test_formula(l_true, "(forall (x Int) (y Int) (implies (= (* 6 x) (* 5 y)) (exists (d Int) (= y (* 3 d)))))");
|
||||
|
||||
test_formula(l_undef, "(exists (x Int) (= (- a (mod x 4)) 0))");
|
||||
// return;
|
||||
|
||||
|
||||
// test_formula(l_true, "(exists (x Int) (y Int) (= 1 (+ (* 5 x) (* 3 y))))");
|
||||
|
||||
|
||||
test_formula(l_undef, "(exists (a Bool) (b Bool) (or (and p1 a) (and p2 (not b))))");
|
||||
|
||||
|
||||
|
||||
|
||||
test_formula(l_false,
|
||||
"(forall (x Int) (q1 Int) (q2 Int) (r1 Int) (r2 Int) "
|
||||
" (implies "
|
||||
" (and (< x 4699) "
|
||||
" (= (* 2622 x) (+ (* 65536 q1) r1)) "
|
||||
" (<= 0 q1) "
|
||||
" (<= 0 r1) "
|
||||
" (< r1 65536) "
|
||||
" (= x (+ (* 100 q2) r2)) "
|
||||
" (<= 0 q2) "
|
||||
" (<= 0 r2) "
|
||||
" (< r2 100)) "
|
||||
" (= q1 q2)))");
|
||||
|
||||
|
||||
|
||||
test_formula(l_undef,
|
||||
"(forall (l list) (or (= l nil) (exists (x Int) (ll list) (= l (cons x ll)))))");
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
test_formula(l_false, "(exists (x Real) (forall (y Real) (>= x y)))");
|
||||
test_formula(l_false, "(exists (x Real) (forall (y Real) (> x y)))");
|
||||
test_formula(l_false, "(exists (x Real) (forall (y Real) (< x y)))");
|
||||
test_formula(l_false, "(exists (x Real) (forall (y Real) (<= x y)))");
|
||||
|
||||
test_formula(l_true, "(exists (x Real) (exists (y Real) (< x y)))");
|
||||
test_formula(l_true, "(exists (x Real) (exists (y Real) (<= x y)))");
|
||||
test_formula(l_true, "(exists (x Real) (exists (y Real) (>= x y)))");
|
||||
test_formula(l_true, "(exists (x Real) (exists (y Real) (> x y)))");
|
||||
|
||||
test_formula(l_true, "(forall (x Real) (exists (y Real) (< x y)))");
|
||||
test_formula(l_true, "(forall (x Real) (exists (y Real) (<= x y)))");
|
||||
test_formula(l_true, "(forall (x Real) (exists (y Real) (>= x y)))");
|
||||
test_formula(l_true, "(forall (x Real) (exists (y Real) (> x y)))");
|
||||
|
||||
test_formula(l_false, "(forall (x Real) (forall (y Real) (< x y)))");
|
||||
test_formula(l_false, "(forall (x Real) (forall (y Real) (<= x y)))");
|
||||
test_formula(l_false, "(forall (x Real) (forall (y Real) (>= x y)))");
|
||||
test_formula(l_false, "(forall (x Real) (forall (y Real) (> x y)))");
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (l Int) (forall (x Int) (implies (>= x l) "
|
||||
" (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 5 v))))))))");
|
||||
|
||||
|
||||
test_formula(l_false, "(forall (d Int) (implies (>= d 0) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (+ (* 3 x) (* 5 y)))))))");
|
||||
|
||||
test_formula(l_true, "(forall (y Int) (implies (exists (d Int) (= y (* 6 d))) (exists (d Int) (= y (* 2 d)))))");
|
||||
|
||||
test_formula(l_true, "(forall (y Int) (implies (exists (d Int) (= y (* 65 d))) (exists (d Int) (= y (* 5 d)))))");
|
||||
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (z Int) (forall (w Int) (exists (x Int) (y Int) "
|
||||
" (or (and (< (+ (* 3 x) w) 2) (< 1 (- (+ (* 2 x) z) w))) "
|
||||
" (and (< z (* 2 y)) (> z y))))))");
|
||||
|
||||
|
||||
test_formula(l_true, "(exists (x Int) (y Int) (and (> x 0) (>= y 0) (= 1 (- (* 3 x) (* 5 y)))))");
|
||||
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (a Int) (b Int) "
|
||||
" (and (not (= a 1)) (= a b) (or (= a (* 2 b)) (= (* 2 b) (+ 1 (* 3 a))))))");
|
||||
|
||||
|
||||
|
||||
test_formula(l_true,
|
||||
"(forall (x Int) (iff (and (not (= 0 (mod x 2))) (= 0 (mod (- x 1) 3))) "
|
||||
" (or (= 0 (mod (- x 1) 12)) (= 0 (mod (- x 7) 12)))))");
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
test_formula(l_false, "(exists (x Int) (and (< (* 3 x) 2) (< 1 (* 2 x))))");
|
||||
|
||||
|
||||
test_formula(l_true, "(forall (x Int) (y Int) (or (= 0 (mod x 5)) (not (= (* 6 x) (* 5 y)))))");
|
||||
|
||||
|
||||
test_formula(l_false, "(forall (x Int) (exists (y Int) (= x (* 2 y))))");
|
||||
test_formula(l_false,
|
||||
"(forall (x Int) "
|
||||
" (implies (not (= 0 (mod x 2))) "
|
||||
" (or (= 0 (mod (- x 1) 4)) "
|
||||
" (= 0 (mod (- x 1) 8)) "
|
||||
" (= 0 (mod (- x 3) 8)) "
|
||||
" (= 0 (mod (- x 1) 6)) "
|
||||
" (= 0 (mod (- x 1) 14)) "
|
||||
" (= 0 (mod (- x 9) 14)) "
|
||||
" (= 0 (mod (- x 11) 14)) "
|
||||
" (= 0 (mod (- x 5) 24)) "
|
||||
" (= 0 (mod (- x 11) 24))))) ");
|
||||
|
||||
test_formula(l_true,
|
||||
"(forall (x Int) (iff (and (not (= 0 (mod x 2))) (= 0 (mod (- x 1) 3))) "
|
||||
" (or (= 0 (mod (- x 1) 12)) (= 0 (mod (- x 7) 12)))))");
|
||||
|
||||
|
||||
|
||||
|
||||
test_formula(l_false,
|
||||
"(forall (d Int) (c Int) (b Int) "
|
||||
" (and (= c 0) (= d (* b c)) (= d 0)))");
|
||||
|
||||
|
||||
|
||||
|
||||
//return;
|
||||
|
||||
test_formula(l_undef, "(exists (k!12 Int) (k!11 Int) (and (= (ite (= k!11 0) 0 k!11) k!11) (not (= (ite (= k!12 (+ 1)) 1 0) 0))))");
|
||||
//return;
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
test_formula(l_false,
|
||||
"(forall (a Int) (b Int) (x Int) (y Int) (z Int) "
|
||||
" (implies (and (= (+ a 2) b) (= x (+ 1 (- b a))) (= y (- b 2)) (= z 3)) false))");
|
||||
|
||||
|
||||
|
||||
test_formula(l_false,
|
||||
"(exists (a Int) (b Int) "
|
||||
" (and (> a 1) (> b 1) (= a b) (or (= a (* 2 b)) (= (* 2 b) (+ 1 (* 3 a))))))");
|
||||
|
||||
|
||||
|
||||
test_formula(l_true, "(forall (d Int) (implies true (exists (x Int) (y Int) (and true true (= d (+ (* 3 x) (* 5 y)))))))");
|
||||
|
||||
// This one takes forever without bit-vectors
|
||||
test_formula(l_true, "(forall (d Int) (implies (>= d 8) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (+ (* 3 x) (* 5 y)))))))");
|
||||
|
||||
test_formula(l_true, "(forall (d Int) (implies (>= d 0) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (- (* 3 x) (* 5 y)))))))");
|
||||
|
||||
|
||||
test_formula(l_false, "(exists (x Int) (y Int) (z Int) (= 1 (- (* 4 x) (* 6 y))))");
|
||||
|
||||
//return;
|
||||
|
||||
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (l Int) (forall (x Int) (implies (>= x l) "
|
||||
" (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 8 v))))))))");
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (l Int) (forall (x Int) (implies (>= x l) "
|
||||
" (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 8 v))))))))");
|
||||
|
||||
#if 0
|
||||
|
||||
// too slow.
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (l Int) (forall (x Int) (implies (>= x l) "
|
||||
" (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 7 u) (* 8 v))))))))");
|
||||
|
||||
|
||||
#endif
|
||||
|
||||
test_formula(l_true, "(forall (x Int) (exists (y Int) (and (<= (* 2 y) x) (< x (* 2 (+ y 1))))))");
|
||||
|
||||
|
||||
test_formula(l_false, "(exists (x Int) (y Int) (and (> y 0) (> y (* 2 x)) (< y (+ x 2)) (= 0 (mod y 2))))");
|
||||
|
||||
test_formula(l_false, "(exists (x Int) (and (< (* 3 x) 3) (< 1 (* 2 x))))");
|
||||
|
||||
|
||||
test_formula(l_true, "(exists (x Int) (and (< (* 3 x) 4) (< 1 (* 2 x))))");
|
||||
|
||||
test_formula(l_false, "(exists (x Int) (and (< (+ (* 3 x) 1) 10) (> (- (* 7 x) 6) 7) (= 0 (mod x 3))))");
|
||||
|
||||
|
||||
test_formula(l_false, "(exists (x Int) (y Int) (and (< (- 1 (* 5 y)) x) (< (+ 1 y) (* 13 x)) (< (+ x 2) 0) (> y 0)))");
|
||||
|
||||
test_formula(l_false, "(exists (x Int) (y Int) (and (< (- 1 (* 5 y)) x) (< (+ 1 y) (* 13 x)) (< x -2)))");
|
||||
|
||||
test_formula(l_true, "(exists (w Int) (z Int) (y Int) (x Int) (and (< (- 1 (* 5 y)) (+ x (* 2 z))) (< (+ 1 y w (* -4 z)) (* 13 x)) (< x -2) (> z 0)))");
|
||||
|
||||
|
||||
|
||||
test_formula(l_true,
|
||||
"(forall (w Int) "
|
||||
" (exists (z Int) (y Int) (x Int) "
|
||||
" (and (< (- 1 (* 5 y)) (+ x (* 2 z))) "
|
||||
" (< (- (+ 1 y) (* 4 z)) (* 13 x)) "
|
||||
" (< x -2) (> z 0) (< x 10)))) ");
|
||||
|
||||
|
||||
test_formula(l_false,
|
||||
"(forall (d Int) (c Int) (b Int) "
|
||||
" (and (= c 0) (= d (* b c)) (= d 4)))");
|
||||
|
||||
test_formula(l_undef,
|
||||
"(exists (d Int) (c Int) (b Int) "
|
||||
" (and (= c 0) (= d (* b c)) (= d 0)))");
|
||||
|
||||
test_formula(l_undef,
|
||||
"(exists (d Int) (c Int) (b Int) "
|
||||
" (and (= c 0) (= d (* b c)) (= d 4)))");
|
||||
|
||||
|
||||
|
||||
// Tests from Harrison's HOL-light version of Cooper.
|
||||
|
||||
test_formula(l_true, "(forall (x Int) (y Int) (not (= (+ 1 (* 2 x)) (* 2 y))))");
|
||||
|
||||
|
||||
test_formula(l_false, "(exists (x Int) (y Int) (= 1 (- (* 4 x) (* 6 y))))");
|
||||
|
||||
|
||||
|
||||
// "(forall (x Int) (implies (< b x) (<= a x)))"
|
||||
// "(forall (x Int) (implies (< b x) (< a x)))"
|
||||
|
||||
|
||||
test_formula(l_false, "(forall (d Int) (implies (>= d 0) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (+ (* 3 x) (* 5 y)))))))");
|
||||
|
||||
test_formula(l_true, "(forall (d Int) (implies true (exists (x Int) (y Int) (and true true (= d (+ (* 3 x) (* 5 y)))))))");
|
||||
|
||||
// This one takes forever without bit-vectors
|
||||
test_formula(l_true, "(forall (d Int) (implies (>= d 8) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (+ (* 3 x) (* 5 y)))))))");
|
||||
|
||||
test_formula(l_true, "(forall (d Int) (implies (>= d 0) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= d (- (* 3 x) (* 5 y)))))))");
|
||||
|
||||
test_formula(l_true, "(exists (x Int) (y Int) (and (> x 0) (>= y 0) (= 1 (- (* 3 x) (* 5 y)))))");
|
||||
|
||||
test_formula(l_false, "(exists (x Int) (y Int) (z Int) (= 1 (- (* 4 x) (* 6 y))))");
|
||||
|
||||
// "(forall (x Int) (implies (< b (* 3 x)) (a < (* 3 x))))"
|
||||
|
||||
test_formula(l_false, "(forall (x Int) (y Int) (implies (<= x y) (< (+ 1 (* 2 x)) (* 2 y))))");
|
||||
|
||||
|
||||
test_formula(l_true, "(forall (x Int) (y Int) (z Int) (implies (= (+ 1 (* 2 x)) (* 2 y)) (> (+ x y z) 129)))");
|
||||
|
||||
// Formula examples from Cooper's paper.
|
||||
|
||||
|
||||
test_formula(l_true, "(forall (a Int) (exists (b Int) (or (< a (+ (* 4 b) (* 3 a))) (and (not (< a b)) (> a (+ b 1))))))");
|
||||
|
||||
test_formula(l_false, "(exists (y Int) (forall (x Int) (and (> (+ x (* 5 y)) 1) (> (- (* 13 x) y) 1) (< (+ x 2) 0))))");
|
||||
|
||||
// Harrison's formulas:
|
||||
|
||||
test_formula(l_false, "(forall (x Int) (y Int) (implies (and (>= x 0) (>= y 0)) (or (< (- (* 12 x) (* 8 y)) 0) (> (- (* 12 x) (* 8 y)) 2))))");
|
||||
|
||||
|
||||
// test_formula(l_true, "(exists (x Int) (y Int) (= 1 (+ (* 5 x) (* 3 y))))");
|
||||
|
||||
|
||||
test_formula(l_false, "(exists (x Int) (y Int) (= 1 (+ (* 5 x) (* 10 y))))");
|
||||
|
||||
test_formula(l_true, "(exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= 1 (- (* 5 x) (* 6 y)))))");
|
||||
|
||||
test_formula(l_true, "(exists (x Int) (y Int) (z Int) (w Int) (= 1 (+ (* 2 w) (* 3 x) (* 4 y) (* 5 z))))");
|
||||
|
||||
test_formula(l_true, "(exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= 1 (- (* 5 x) (* 3 y)))))");
|
||||
|
||||
test_formula(l_true, "(exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= 1 (- (* 3 x) (* 5 y)))))");
|
||||
|
||||
test_formula(l_false,"(exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= 1 (- (* 6 x) (* 3 y)))))");
|
||||
|
||||
test_formula(l_true, "(forall (x Int) (y Int) (or (= 0 (mod x 5)) (= 0 (mod y 6)) (not (= (* 6 x) (* 5 y)))))");
|
||||
|
||||
|
||||
test_formula(l_false,"(forall (x Int) (y Int) (or (not (= (* 6 x) (* 5 y)))))");
|
||||
|
||||
|
||||
|
||||
// Positive variant of the Bezout theorem (see the exercise). *)
|
||||
|
||||
test_formula(l_true, "(forall (z Int) (implies (> z 7) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= (+ (* 3 x) (* 5 y)) z)))))");
|
||||
|
||||
test_formula(l_false,"(forall (z Int) (implies (> z 2) (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= (+ (* 3 x) (* 5 y)) z)))))");
|
||||
|
||||
test_formula(l_true,
|
||||
"(forall (z Int) (implies (<= z 7) "
|
||||
" (iff (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= z (+ (* 3 x) (* 5 y))))) "
|
||||
" (not (exists (x Int) (y Int) (and (>= x 0) (>= y 0) (= (- 7 z) (+ (* 3 x) (* 5 y))))))))) ");
|
||||
|
||||
// Basic result about congruences.
|
||||
|
||||
test_formula(l_true,
|
||||
"(forall (x Int) "
|
||||
" (iff (and (not (exists (m Int) (= x (* 2 m)))) (exists (m Int) (= x (+ (* 3 m) 1)))) "
|
||||
" (or (exists (m Int) (= x (+ (* 12 m) 1))) (exists (m Int) (= x (+ (* 12 m) 7))))))");
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
// Inspired by the Collatz conjecture.
|
||||
|
||||
test_formula(l_false,
|
||||
"(forall (a Int) (b Int) (x Int) (y Int) (z Int) "
|
||||
" (implies (and (= (+ a 2) b) (= x (+ 1 (- b a))) (= y (- b 2)) (= z 3)) false))");
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (a Int) (b Int) "
|
||||
" (and (not (= a 1)) (= a b) (or (= a (* 2 b)) (= (* 2 b) (+ 1 (* 3 a))))))");
|
||||
|
||||
|
||||
test_formula(l_false,
|
||||
"(exists (a Int) (b Int) "
|
||||
" (and (> a 1) (> b 1) (= a b) (or (= a (* 2 b)) (= (* 2 b) (+ 1 (* 3 a))))))");
|
||||
|
||||
test_formula(l_false,
|
||||
"(exists (a Int) (b Int) "
|
||||
" (and (> a 1) (> b 1) "
|
||||
" (or (= a (* 2 b)) (= (* 2 b) (+ 1 (* 3 a)))) "
|
||||
" (or (= b (* 2 a)) (= (* 2 a) (+ 1 (* 3 b))))))");
|
||||
|
||||
#if 0
|
||||
// Bob Constable's "stamp problem".
|
||||
|
||||
test_formula(l_true,
|
||||
"(forall (x Int) (implies (>= x 8) "
|
||||
" (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 5 v)))))))");
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (l Int) (forall (x Int) (implies (>= x l) "
|
||||
" (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 5 v))))))))");
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (l Int) (forall (x Int) (implies (>= x l) "
|
||||
" (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 7 v))))))))");
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (l Int) (forall (x Int) (implies (>= x l) "
|
||||
" (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 3 u) (* 8 v))))))))");
|
||||
|
||||
test_formula(l_true,
|
||||
"(exists (l Int) (forall (x Int) (implies (>= x l) "
|
||||
" (exists (u Int) (v Int) (and (>= u 0) (>= v 0) (= x (+ (* 7 u) (* 8 v))))))))");
|
||||
#endif
|
||||
|
||||
// Example from reciprocal mult: (2622 * x)>>16 = x/100 within a range.
|
||||
|
||||
|
||||
test_formula(l_true,
|
||||
"(forall (x Int) (y Int) "
|
||||
" (iff (exists (d Int) (= (+ x y) (* 2 d))) "
|
||||
" (iff (exists (d Int) (= x (* 2 d))) (exists (d Int) (= y (* 2 d))))))");
|
||||
|
||||
test_formula(l_true,
|
||||
"(forall (n Int) "
|
||||
" (implies (and (< 0 n) (< n 2400)) "
|
||||
" (or (and (<= n 2) (<= 2 (* 2 n))) "
|
||||
" (and (<= n 3) (<= 3 (* 2 n))) "
|
||||
" (and (<= n 5) (<= 5 (* 2 n))) "
|
||||
" (and (<= n 7) (<= 7 (* 2 n))) "
|
||||
" (and (<= n 13) (<= 13 (* 2 n))) "
|
||||
" (and (<= n 23) (<= 23 (* 2 n))) "
|
||||
" (and (<= n 43) (<= 43 (* 2 n))) "
|
||||
" (and (<= n 83) (<= 83 (* 2 n))) "
|
||||
" (and (<= n 163) (<= 163 (* 2 n))) "
|
||||
" (and (<= n 317) (<= 317 (* 2 n))) "
|
||||
" (and (<= n 631) (<= 631 (* 2 n))) "
|
||||
" (and (<= n 1259) (<= 1259 (* 2 n))) "
|
||||
" (and (<= n 2503) (<= 2503 (* 2 n)))))) ");
|
||||
|
||||
|
||||
|
||||
|
||||
memory::finalize();
|
||||
#ifdef _WINDOWS
|
||||
_CrtDumpMemoryLeaks();
|
||||
#endif
|
||||
exit(0);
|
||||
}
|
||||
|
||||
|
||||
Loading…
Add table
Add a link
Reference in a new issue