mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
commit
38037caf4d
|
@ -3,6 +3,16 @@
|
|||
#include "ast_pp.h"
|
||||
#include "reg_decl_plugins.h"
|
||||
|
||||
static void check_equiv(ast_manager& m, expr* e1, expr* e2) {
|
||||
front_end_params fp;
|
||||
smt::solver solver(m, fp);
|
||||
expr_ref equiv(m);
|
||||
equiv = m.mk_not(m.mk_eq(e1,e2));
|
||||
solver.assert_expr(equiv);
|
||||
lbool is_sat = solver.check();
|
||||
SASSERT(is_sat == l_false);
|
||||
}
|
||||
|
||||
static void simplify_formula(ast_manager& m, expr* e) {
|
||||
expr_ref result(m);
|
||||
expr_context_simplifier simp(m);
|
||||
|
@ -11,8 +21,10 @@ static void simplify_formula(ast_manager& m, expr* e) {
|
|||
|
||||
TRACE("expr_context_simplifier",
|
||||
tout
|
||||
<< mk_pp(e, m) << " |-> "
|
||||
<< mk_pp(e, m) << "\n|->\n"
|
||||
<< mk_pp(result.get(), m) << "\n";);
|
||||
|
||||
check_equiv(m, e, result);
|
||||
|
||||
}
|
||||
|
||||
|
@ -27,8 +39,15 @@ void tst_expr_context_simplifier() {
|
|||
parser->parse_string(
|
||||
"(benchmark samples :logic QF_LIA \n"
|
||||
" :extrafuns ((x Int) (y Int) (z Int) (u Int)) \n"
|
||||
" :extrapreds ((p) (q) (r)) \n"
|
||||
" :formula (and (<= 1 x) (or (<= 1 x) (<= x y))) \n"
|
||||
" :formula (and (<= 2 (ite (<= z 1) (ite (<= z 1) x y) (* 2 x))) (<= x y)) \n"
|
||||
" :formula (or (and (not p) q (or (not r) (and (or (not p) q) r)))\
|
||||
(and (not p) q (or (and p (not q) r) (and (or (not p) q) (not r)))) \
|
||||
(and (or (and p (not q)) (and p q))\
|
||||
(or (and p q r) (and (or (not p) (not q)) (not r))))\
|
||||
(and (not p) (not q) (or (and (not p) q r) (and (or p (not q)) (not r))))\
|
||||
(and (not p) (not q) (or (not r) (and (or p (not q)) r))))\n"
|
||||
")"
|
||||
);
|
||||
|
||||
|
|
|
@ -60,6 +60,7 @@ static void test_formula(lbool expected_outcome, char const* fml) {
|
|||
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"
|
||||
|
@ -76,6 +77,17 @@ static void test_formula(lbool expected_outcome, char const* fml) {
|
|||
|
||||
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))))");
|
||||
|
@ -99,6 +111,8 @@ void tst_quant_elim() {
|
|||
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 "
|
||||
|
|
Loading…
Reference in a new issue