mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-17 08:42:15 +00:00
Code Activity

bit-blast equalities before checking

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-19 04:39:18 -08:00
parent f014ab9598
commit 57c4ce4082
1 changed files with 26 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/muz_qe/pdr_prop_solver.cpp
View file

@ -26,6 +26,7 @@ Revision History:
#include "model_pp.h" #include "model_pp.h"
#include "front_end_params.h" #include "front_end_params.h"
#include "datatype_decl_plugin.h" #include "datatype_decl_plugin.h"
#include "bv_decl_plugin.h"
#include "pdr_farkas_learner.h" #include "pdr_farkas_learner.h"
#include "ast_smt2_pp.h" #include "ast_smt2_pp.h"
#include "expr_replacer.h" #include "expr_replacer.h"
@ -94,9 +95,12 @@ namespace pdr {
void expand_literals(expr_ref_vector& conjs) { void expand_literals(expr_ref_vector& conjs) {
arith_util arith(m); arith_util arith(m);
datatype_util dt(m); datatype_util dt(m);
bv_util bv(m);
expr* e1, *e2, *c, *val; expr* e1, *e2, *c, *val;
for (unsigned i = 0; i < conjs.size(); ++i) { rational r;
unsigned bv_size;
for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get(); expr* e = conjs[i].get();
if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) { if (m.is_eq(e, e1, e2) && arith.is_int_real(e1)) {
conjs[i] = arith.mk_le(e1,e2); conjs[i] = arith.mk_le(e1,e2);
@ -109,7 +113,8 @@ namespace pdr {
} }
++i; ++i;
} }
else if (m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) { else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) ||
(m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){
func_decl* f = to_app(val)->get_decl(); func_decl* f = to_app(val)->get_decl();
func_decl* r = dt.get_constructor_recognizer(f); func_decl* r = dt.get_constructor_recognizer(f);
conjs[i] = m.mk_app(r,c); conjs[i] = m.mk_app(r,c);
@ -118,6 +123,24 @@ namespace pdr {
conjs.push_back(m.mk_eq(m.mk_app(acc[i], c), to_app(val)->get_arg(i))); conjs.push_back(m.mk_eq(m.mk_app(acc[i], c), to_app(val)->get_arg(i)));
} }
} }
else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) ||
(m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) {
rational two(2);
for (unsigned j = 0; j < bv_size; ++j) {
parameter p(j);
expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c);
if ((r % two).is_zero()) {
e = m.mk_not(e);
}
r = div(r, two);
if (j == 0) {
conjs[i] = e;
}
else {
conjs.push_back(e);
}
}
}
} }
} }
@ -341,7 +364,7 @@ namespace pdr {
} }
fl.get_lemmas(pr, bs, lemmas); fl.get_lemmas(pr, bs, lemmas);
safe.elim_proxies(lemmas); safe.elim_proxies(lemmas);
fl.simplify_lemmas(lemmas); // redundant fl.simplify_lemmas(lemmas); // redundant?
if (m_fparams.m_arith_mode == AS_DIFF_LOGIC && if (m_fparams.m_arith_mode == AS_DIFF_LOGIC &&
!is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) { !is_difference_logic(m, lemmas.size(), lemmas.c_ptr())) {
IF_VERBOSE(1, IF_VERBOSE(1,