mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2012-11-04 12:49:58 -08:00
commit 2c66afadd6
14 changed files with 2015 additions and 446 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/muz_qe/dl_mk_interp_tail_simplifier.cpp
View file

@ -371,18 +371,21 @@ namespace datalog {
bool mk_interp_tail_simplifier::propagate_variable_equivalences(rule * r, rule_ref& res) {
unsigned u_len = r->get_uninterpreted_tail_size();
unsigned len = r->get_tail_size();
if (u_len==len) {
if (u_len == len) {
return false;
}
ptr_vector<expr> todo;
for (unsigned i=u_len; i<len; i++) {
for (unsigned i = u_len; i < len; i++) {
todo.push_back(r->get_tail(i));
SASSERT(!r->is_neg_tail(i));
}
m_rule_subst.reset(r);
obj_hashtable<expr> leqs;
expr_ref_vector trail(m);
expr_ref tmp1(m), tmp2(m);
bool found_something = false;
#define TRY_UNIFY(_x,_y) if (m_rule_subst.unify(_x,_y)) { found_something = true; }
@ -424,6 +427,17 @@ namespace datalog {
TRY_UNIFY(arg1, m.mk_true());
}
}
else if (!neg && (a.is_le(t, arg1, arg2) || a.is_ge(t, arg2, arg1))) {
tmp1 = a.mk_sub(arg1, arg2);
tmp2 = a.mk_sub(arg2, arg1);
if (false && leqs.contains(tmp2) && IS_FLEX(arg1) && IS_FLEX(arg2)) {
TRY_UNIFY(arg1, arg2);
}
else {
trail.push_back(tmp1);
leqs.insert(tmp1);
}
}
}
if (!found_something) {

11
src/muz_qe/dl_mk_interp_tail_simplifier.h
View file

@ -24,6 +24,7 @@ Revision History:
#include "dl_rule_transformer.h"
#include "unifier.h"
#include "substitution.h"
#include "arith_decl_plugin.h"
namespace datalog {
@ -60,11 +61,10 @@ namespace datalog {
}
};
ast_manager & m;
context & m_context;
th_rewriter & m_simp;
ast_manager & m;
context & m_context;
th_rewriter & m_simp;
arith_util a;
rule_substitution m_rule_subst;
class normalizer_cfg;
@ -82,6 +82,7 @@ namespace datalog {
m(ctx.get_manager()),
m_context(ctx),
m_simp(ctx.get_rewriter()),
a(m),
m_rule_subst(ctx) {}
/**If rule should be retained, assign transformed version to res and return true;

10
src/muz_qe/dl_mk_slice.cpp
View file

@ -732,7 +732,7 @@ namespace datalog {
void mk_slice::update_rule(rule& r, rule_set& dst) {
rule* new_rule;
rule_ref new_rule(rm);
if (rule_updated(r)) {
init_vars(r);
app_ref_vector tail(m);
@ -794,16 +794,20 @@ namespace datalog {
}
new_rule = rm.mk(head.get(), tail.size(), tail.c_ptr(), (const bool*) 0);
rm.fix_unbound_vars(new_rule, false);
TRACE("dl", r.display(m_ctx, tout << "replacing:\n"); new_rule->display(m_ctx, tout << "by:\n"););
}
else {
new_rule = &r;
}
dst.add_rule(new_rule);
dst.add_rule(new_rule.get());
if (m_pc) {
m_pc->insert(&r, new_rule, 0, 0);
m_pc->insert(&r, new_rule.get(), 0, 0);
}
}

60
src/muz_qe/dl_rule.cpp
View file

@ -41,6 +41,7 @@ Revision History:
#include"quant_hoist.h"
#include"expr_replacer.h"
#include"bool_rewriter.h"
#include"qe_lite.h"
namespace datalog {
@ -613,14 +614,65 @@ namespace datalog {
return r;
}
void rule_manager::reduce_unbound_vars(rule_ref& r) {
unsigned ut_len = r->get_uninterpreted_tail_size();
unsigned t_len = r->get_tail_size();
ptr_vector<sort> vars;
uint_set index_set;
qe_lite qe(m);
expr_ref_vector conjs(m);
if (ut_len == t_len) {
return;
}
get_free_vars(r->get_head(), vars);
for (unsigned i = 0; i < ut_len; ++i) {
get_free_vars(r->get_tail(i), vars);
}
for (unsigned i = ut_len; i < t_len; ++i) {
conjs.push_back(r->get_tail(i));
}
for (unsigned i = 0; i < vars.size(); ++i) {
if (vars[i]) {
index_set.insert(i);
}
}
qe(index_set, false, conjs);
bool change = conjs.size() != t_len - ut_len;
for (unsigned i = 0; !change && i < conjs.size(); ++i) {
change = r->get_tail(ut_len+i) != conjs[i].get();
}
if (change) {
app_ref_vector tail(m);
svector<bool> tail_neg;
for (unsigned i = 0; i < ut_len; ++i) {
tail.push_back(r->get_tail(i));
tail_neg.push_back(r->is_neg_tail(i));
}
for (unsigned i = 0; i < conjs.size(); ++i) {
tail.push_back(ensure_app(conjs[i].get()));
}
tail_neg.resize(tail.size(), false);
r = mk(r->get_head(), tail.size(), tail.c_ptr(), tail_neg.c_ptr());
TRACE("dl", r->display(m_ctx, tout << "reduced rule\n"););
}
}
void rule_manager::fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination) {
reduce_unbound_vars(r);
if (!m_ctx.fix_unbound_vars()) {
return;
}
if (r->get_uninterpreted_tail_size() == r->get_tail_size()) {
//no interpreted tail to fix
unsigned ut_len = r->get_uninterpreted_tail_size();
unsigned t_len = r->get_tail_size();
if (ut_len == t_len) {
// no interpreted tail to fix
return;
}
@ -633,7 +685,7 @@ namespace datalog {
get_free_vars(r, free_rule_vars);
vctr.count_vars(m, head);
unsigned ut_len = r->get_uninterpreted_tail_size();
for (unsigned i = 0; i < ut_len; i++) {
app * t = r->get_tail(i);
vctr.count_vars(m, t);
@ -642,11 +694,9 @@ namespace datalog {
}
ptr_vector<sort> interp_vars;
//var_idx_set interp_vars;
var_idx_set unbound_vars;
expr_ref_vector tails_with_unbound(m);
unsigned t_len = r->get_tail_size();
for (unsigned i = ut_len; i < t_len; i++) {
app * t = r->get_tail(i);
interp_vars.reset();

6
src/muz_qe/dl_rule.h
View file

@ -83,6 +83,11 @@ namespace datalog {
unsigned hoist_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names);
/**
\brief Perform cheap quantifier elimination to reduce the number of variables in the interpreted tail.
*/
void reduce_unbound_vars(rule_ref& r);
public:
ast_manager& get_manager() const { return m; }
@ -127,6 +132,7 @@ namespace datalog {
void fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination);
/**
\brief apply substitution to variables of rule.
*/

9
src/muz_qe/pdr_context.cpp
View file

@ -472,10 +472,7 @@ namespace pdr {
th_rewriter rw(m);
rw(m_transition);
rw(m_initial_state);
if (ctx.is_dl()) {
hoist_non_bool_if(m_transition);
hoist_non_bool_if(m_initial_state);
}
m_solver.add_formula(m_transition);
m_solver.add_level_formula(m_initial_state, 0);
TRACE("pdr",
@ -578,6 +575,9 @@ namespace pdr {
expr_ref fml = pm.mk_and(conj);
th_rewriter rw(m);
rw(fml);
if (ctx.is_dl()) {
hoist_non_bool_if(fml);
}
TRACE("pdr", tout << mk_pp(fml, m) << "\n";);
SASSERT(is_ground(fml));
if (m.is_false(fml)) {
@ -1825,6 +1825,7 @@ namespace pdr {
++m_stats.m_num_nodes;
m_search.add_leaf(*child);
IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
m_stats.m_max_depth = std::max(m_stats.m_max_depth, child->depth());
}
check_pre_closed(n);
TRACE("pdr", m_search.display(tout););

8
src/muz_qe/pdr_context.h
View file

@ -175,21 +175,25 @@ namespace pdr {
expr_ref m_state;
model_ref m_model;
ptr_vector<model_node> m_children;
unsigned m_level;
unsigned m_level;
unsigned m_orig_level;
unsigned m_depth;
bool m_closed;
public:
model_node(model_node* parent, expr_ref& state, pred_transformer& pt, unsigned level):
m_parent(parent), m_pt(pt), m_state(state), m_model(0), m_level(level), m_orig_level(level), m_closed(false) {
m_parent(parent), m_pt(pt), m_state(state), m_model(0),
m_level(level), m_orig_level(level), m_depth(0), m_closed(false) {
if (m_parent) {
m_parent->m_children.push_back(this);
SASSERT(m_parent->m_level == level+1);
SASSERT(m_parent->m_level > 0);
m_depth = m_parent->m_depth+1;
}
}
void set_model(model_ref& m) { m_model = m; }
unsigned level() const { return m_level; }
unsigned orig_level() const { return m_orig_level; }
unsigned depth() const { return m_depth; }
void increase_level() { ++m_level; }
expr* state() const { return m_state; }
ptr_vector<model_node> const& children() { return m_children; }

8
src/muz_qe/pdr_dl_interface.cpp
View file

@ -201,8 +201,10 @@ void dl_interface::collect_params(param_descrs& p) {
p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)");
p.insert(":generate-proof-trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object");
p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)");
p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples by extending candidate trace within search area");
p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract "
"Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)");
p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples "
"by extending candidate trace within search area");
p.insert(":unfold-rules", CPK_UINT, "PDR: (default 0) unfold rules statically using iterative squarring");
p.insert(":use-model-generalizer", CPK_BOOL, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)");
p.insert(":validate-result", CPK_BOOL, "PDR (default false) validate result (by proof checking or model checking)");
@ -219,5 +221,5 @@ void dl_interface::collect_params(param_descrs& p) {
PRIVATE_PARAMS(p.insert(":simplify-formulas-pre", CPK_BOOL, "PDR: (default false) simplify derived formulas before inductive propagation"););
PRIVATE_PARAMS(p.insert(":simplify-formulas-post", CPK_BOOL, "PDR: (default false) simplify derived formulas after inductive propagation"););
p.insert(":slice", CPK_BOOL, "PDR: (default true) simplify clause set using slicing");
p.insert(":coalesce-rules", CPK_BOOL, "PDR: (default false) coalesce rules");
p.insert(":coalesce-rules", CPK_BOOL, "BMC: (default false) coalesce rules");
}

45
src/muz_qe/pdr_util.cpp
View file

@ -468,7 +468,10 @@ void model_evaluator::eval_arith(app* e) {
void model_evaluator::inherit_value(expr* e, expr* v) {
SASSERT(!is_unknown(v));
SASSERT(m.get_sort(e) == m.get_sort(v));
if (m.is_bool(e)) {
if (is_x(v)) {
set_x(e);
}
else if (m.is_bool(e)) {
SASSERT(m.is_bool(v));
if (is_true(v)) set_true(e);
else if (is_false(v)) set_false(e);
@ -862,12 +865,19 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
fml = m.mk_and(conjs.size(), conjs.c_ptr());
}
//
// (f (if c1 (if c2 e1 e2) e3) b c) ->
// (if c1 (if c2 (f e1 b c)
class ite_hoister {
ast_manager& m;
public:
ite_hoister(ast_manager& m): m(m) {}
br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
if (m.is_ite(f)) {
return BR_FAILED;
}
for (unsigned i = 0; i < num_args; ++i) {
expr* c, *t, *e;
if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) {
@ -875,8 +885,13 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
ptr_vector<expr> args1(num_args, args);
args1[i] = t;
e1 = m.mk_app(f, num_args, args1.c_ptr());
if (t == e) {
result = e1;
return BR_REWRITE1;
}
args1[i] = e;
e2 = m.mk_app(f, num_args, args1.c_ptr());
result = m.mk_app(f, num_args, args);
result = m.mk_ite(c, e1, e2);
return BR_REWRITE3;
}
@ -910,7 +925,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
ite_hoister_star ite_rw(m, p);
expr_ref tmp(m);
ite_rw(fml, tmp);
fml = tmp;
fml = tmp;
}
class test_diff_logic {
@ -934,13 +949,23 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
return is_app(e) && a.get_family_id() == to_app(e)->get_family_id();
}
bool is_var_or_numeric(expr* e) const {
bool is_offset(expr* e) const {
if (a.is_numeral(e)) {
return true;
}
expr* cond, *th, *el;
expr* cond, *th, *el, *e1, *e2;
if (m.is_ite(e, cond, th, el)) {
return is_var_or_numeric(th) && is_var_or_numeric(el);
return is_offset(th) && is_offset(el);
}
// recognize offsets.
if (a.is_add(e, e1, e2)) {
if (is_numeric(e1)) {
return is_offset(e2);
}
if (is_numeric(e2)) {
return is_offset(e1);
}
return false;
}
return !is_arith_expr(e);
}
@ -954,14 +979,14 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
SASSERT(to_app(e)->get_num_args() == 2);
expr * lhs = to_app(e)->get_arg(0);
expr * rhs = to_app(e)->get_arg(1);
if (is_var_or_numeric(lhs) && is_var_or_numeric(rhs))
if (is_offset(lhs) && is_offset(rhs))
return true;
if (!is_numeric(rhs))
std::swap(lhs, rhs);
if (!is_numeric(rhs))
return false;
// lhs can be 'x' or '(+ x (* -1 y))'
if (is_var_or_numeric(lhs))
if (is_offset(lhs))
return true;
expr* arg1, *arg2;
if (!a.is_add(lhs, arg1, arg2))
@ -975,7 +1000,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
expr* m1, *m2;
if (!a.is_mul(arg2, m1, m2))
return false;
return is_minus_one(m1) && is_var_or_numeric(m2);
return is_minus_one(m1) && is_offset(m2);
}
bool test_eq(expr* e) const {
@ -997,7 +1022,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
if (a.is_numeral(e)) {
return true;
}
if (is_var_or_numeric(e)) {
if (is_offset(e)) {
return true;
}
expr* lhs, *rhs;
@ -1005,7 +1030,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
if (!a.is_numeral(lhs)) {
std::swap(lhs, rhs);
}
return a.is_numeral(lhs) && is_var_or_numeric(rhs);
return a.is_numeral(lhs) && is_offset(rhs);
}
if (a.is_mul(e, lhs, rhs)) {
return is_minus_one(lhs) || is_minus_one(rhs);

3
src/muz_qe/qe.cpp
View file

@ -1712,7 +1712,8 @@ namespace qe {
m_solver.get_model(model);
SASSERT(is_sat == l_true);
model_evaluator model_eval2(*model);
model_eval2(x,val);
model_eval2.set_model_completion(true);
model_eval2(x, val);
}
TRACE("qe", tout << mk_pp(x,m) << " " << mk_pp(val, m) << "\n";);
m_current->add_def(x, val);

47
src/muz_qe/qe_datatype_plugin.cpp
View file

@ -133,7 +133,7 @@ namespace qe {
func_decl* f = a->get_decl();
if (m_util.is_recognizer(f) && a->get_arg(0) == x) {
m_recognizers.push_back(a);
TRACE("quant_elim", tout << "add recognizer:" << mk_pp(a, m) << "\n";);
TRACE("qe", tout << "add recognizer:" << mk_pp(a, m) << "\n";);
return true;
}
if (!m.is_eq(a)) {
@ -161,6 +161,10 @@ namespace qe {
unsigned num_neqs() { return m_neq_atoms.size(); }
app* neq_atom(unsigned i) { return m_neq_atoms[i].get(); }
unsigned num_neq_terms() const { return m_neqs.size(); }
expr* neq_term(unsigned i) const { return m_neqs[i]; }
expr* const* neq_terms() const { return m_neqs.c_ptr(); }
unsigned num_recognizers() { return m_recognizers.size(); }
app* recognizer(unsigned i) { return m_recognizers[i].get(); }
@ -212,7 +216,7 @@ namespace qe {
}
void add_atom(app* a, bool is_pos) {
TRACE("quant_elim", tout << "add atom:" << mk_pp(a, m) << " " << (is_pos?"pos":"neg") << "\n";);
TRACE("qe", tout << "add atom:" << mk_pp(a, m) << " " << (is_pos?"pos":"neg") << "\n";);
if (is_pos) {
m_eq_atoms.push_back(a);
}
@ -326,7 +330,7 @@ namespace qe {
for_each_expr(*this, fml.get());
if (m_change) {
fml = get_expr(fml.get());
TRACE("quant_elim", tout << "lift:\n" << mk_pp(fml.get(), m) << "\n";);
TRACE("qe", tout << "lift:\n" << mk_pp(fml.get(), m) << "\n";);
}
return m_change;
}
@ -380,7 +384,7 @@ namespace qe {
}
expr* e = m.mk_and(conj.size(), conj.c_ptr());
m_map.insert(a, e, 0);
TRACE("quant_elim", tout << "replace: " << mk_pp(a, m) << " ==> \n" << mk_pp(e, m) << "\n";);
TRACE("qe", tout << "replace: " << mk_pp(a, m) << " ==> \n" << mk_pp(e, m) << "\n";);
return true;
}
@ -456,7 +460,7 @@ namespace qe {
virtual void assign(contains_app& x, expr* fml, rational const& vl) {
sort* s = x.x()->get_decl()->get_range();
SASSERT(m_datatype_util.is_datatype(s));
TRACE("quant_elim", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
TRACE("qe", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
if (m_datatype_util.is_recursive(s)) {
assign_rec(x, fml, vl);
}
@ -468,16 +472,13 @@ namespace qe {
virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
sort* s = x.x()->get_decl()->get_range();
SASSERT(m_datatype_util.is_datatype(s));
TRACE("quant_elim", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
TRACE("qe", tout << mk_pp(x.x(), m) << " " << vl << "\n";);
if (m_datatype_util.is_recursive(s)) {
subst_rec(x, vl, fml, def);
}
else {
subst_nonrec(x, vl, fml, def);
}
if (def) {
*def = 0; // TBD
}
}
virtual unsigned get_weight( contains_app& x, expr* fml) {
@ -605,7 +606,7 @@ namespace qe {
num_branches = rational(eqs.num_eqs() + 1);
return true;
}
TRACE("quant_elim", tout << "could not get number of branches " << mk_pp(x.x(), m) << "\n";);
TRACE("qe", tout << "could not get number of branches " << mk_pp(x.x(), m) << "\n";);
return false;
}
@ -660,6 +661,7 @@ namespace qe {
SASSERT(m_datatype_util.is_datatype(s));
func_decl* c = 0, *r = 0;
TRACE("qe", tout << mk_pp(x, m) << " " << vl << " " << mk_pp(fml, m) << " " << (def != 0) << "\n";);
//
// Add recognizer to formula.
// Introduce auxiliary variable to eliminate.
@ -673,13 +675,13 @@ namespace qe {
m_ctx.add_var(fresh_x);
m_replace->apply_substitution(x, fresh_x, 0, fml);
add_def(fresh_x, def);
TRACE("quant_elim", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";);
TRACE("qe", tout << "Add recognizer " << mk_pp(is_c, m) << "\n";);
return;
}
if (has_selector(contains_x, fml, c)) {
TRACE("quant_elim", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";);
TRACE("qe", tout << "Eliminate selector " << mk_ll_pp(c, m) << "\n";);
subst_constructor(contains_x, c, fml, def);
return;
}
@ -721,14 +723,19 @@ namespace qe {
}
for (unsigned i = 0; i < eqs.num_neqs(); ++i) {
m_replace->apply_substitution(eqs.neq_atom(i), m.mk_true(), fml);
m_replace->apply_substitution(eqs.neq_atom(i), m.mk_false(), fml);
}
if (def) {
NOT_IMPLEMENTED_YET();
// you need to create a diagonal term
sort* s = m.get_sort(x);
ptr_vector<sort> sorts;
sorts.resize(eqs.num_neq_terms(), s);
func_decl* diag = m.mk_func_decl(symbol("diag"), sorts.size(), sorts.c_ptr(), s);
expr_ref t(m);
t = m.mk_app(diag, eqs.num_neq_terms(), eqs.neq_terms());
add_def(t, def);
}
}
TRACE("quant_elim", tout << "reduced " << mk_pp(fml.get(), m) << "\n";);
TRACE("qe", tout << "reduced " << mk_pp(fml.get(), m) << "\n";);
}
bool get_num_branches_nonrec( contains_app& x, expr* fml, rational& num_branches) {
@ -738,10 +745,10 @@ namespace qe {
func_decl* c = 0, *r = 0;
if (sz != 1 && has_recognizer(x.x(), fml, r, c)) {
TRACE("quant_elim", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
num_branches = rational(1);
}
TRACE("quant_elim", tout << mk_pp(x.x(), m) << " branches: " << sz << "\n";);
TRACE("qe", tout << mk_pp(x.x(), m) << " branches: " << sz << "\n";);
return true;
}
@ -757,7 +764,7 @@ namespace qe {
}
func_decl* c = 0, *r = 0;
if (has_recognizer(x, fml, r, c)) {
TRACE("quant_elim", tout << mk_pp(x, m) << " has a recognizer\n";);
TRACE("qe", tout << mk_pp(x, m) << " has a recognizer\n";);
return;
}
@ -776,7 +783,7 @@ namespace qe {
SASSERT(!m_datatype_util.is_recursive(s));
func_decl* c = 0, *r = 0;
if (has_recognizer(x.x(), fml, r, c)) {
TRACE("quant_elim", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
}
else {
unsigned sz = m_datatype_util.get_datatype_num_constructors(s);

2188
src/muz_qe/qe_lite.cpp
View file

File diff suppressed because it is too large Load diff

12
src/muz_qe/qe_lite.h
View file

@ -22,6 +22,7 @@ Revision History:
#define __QE_LITE_H__
#include "ast.h"
#include "uint_set.h"
class qe_lite {
class impl;
@ -40,6 +41,17 @@ public:
*/
void operator()(app_ref_vector& vars, expr_ref& fml);
/**
\brief
Apply light-weight quantifier elimination to variables present/absent in the index set.
If 'index_of_bound' is true, then the index_set is treated as the set of
bound variables. if 'index_of_bound' is false, then index_set is treated as the
set of variables that are not bound (variables that are not in the index set are bound).
*/
void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml);
void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& conjs);
/**
\brief full rewriting based light-weight quantifier elimination round.
*/

36
src/test/quant_solve.cpp
View file

@ -77,7 +77,7 @@ static void validate_quant_solutions(app* x, expr* fml, expr_ref_vector& guards)
#endif
static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml) {
static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr* fml, bool validate) {
front_end_params params;
qe::expr_quant_elim qe(m, params);
qe::guarded_defs defs(m);
@ -86,7 +86,8 @@ static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, expr*
std::cout << mk_pp(fml, m) << "\n";
if (success) {
defs.display(std::cout);
for (unsigned i = 0; i < defs.size(); ++i) {
for (unsigned i = 0; validate && i < defs.size(); ++i) {
validate_quant_solution(m, fml, defs.guard(i), defs.defs(i));
}
}
@ -106,6 +107,10 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
<< "(declare-const z Int)\n"
<< "(declare-const a Int)\n"
<< "(declare-const b Int)\n"
<< "(declare-const P Bool)\n"
<< "(declare-const Q Bool)\n"
<< "(declare-const r1 Real)\n"
<< "(declare-const r2 Real)\n"
<< "(declare-datatypes () ((IList (nil) (cons (car Int) (cdr IList)))))\n"
<< "(declare-const l1 IList)\n"
<< "(declare-const l2 IList)\n"
@ -140,21 +145,21 @@ static void parse_fml(char const* str, app_ref_vector& vars, expr_ref& fml) {
}
}
static void test_quant_solver(ast_manager& m, app* x, char const* str) {
static void test_quant_solver(ast_manager& m, app* x, char const* str, bool validate = true) {
expr_ref fml = parse_fml(m, str);
test_quant_solver(m, 1, &x, fml);
test_quant_solver(m, 1, &x, fml, validate);
}
static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, char const* str) {
static void test_quant_solver(ast_manager& m, unsigned sz, app*const* xs, char const* str, bool validate = true) {
expr_ref fml = parse_fml(m, str);
test_quant_solver(m, sz, xs, fml);
test_quant_solver(m, sz, xs, fml, validate);
}
static void test_quant_solver(ast_manager& m, char const* str) {
static void test_quant_solver(ast_manager& m, char const* str, bool validate = true) {
expr_ref fml(m);
app_ref_vector vars(m);
parse_fml(str, vars, fml);
test_quant_solver(m, vars.size(), vars.c_ptr(), fml);
test_quant_solver(m, vars.size(), vars.c_ptr(), fml, validate);
}
@ -222,9 +227,18 @@ static void test_quant_solve1() {
test_quant_solver(m, "(exists ((c Cell)) (= c null))");
test_quant_solver(m, "(exists ((c Cell)) (= c (cell null c1)))");
//TBD:
//test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))");
//test_quant_solver(m, "(exists ((c Cell)) (not (= c null)))");
test_quant_solver(m, "(exists ((c Cell)) (not (= c null)))", false);
test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))", false);
test_quant_solver(m, "(exists ((c Cell)) (= (cell c (cdr c1)) c1))", false);
test_quant_solver(m, "(exists ((t Tuple)) (= (tuple a P r1) t))");
test_quant_solver(m, "(exists ((t Tuple)) (= a (first t)))");
test_quant_solver(m, "(exists ((t Tuple)) (= P (second t)))");
test_quant_solver(m, "(exists ((t Tuple)) (= r2 (third t)))");
test_quant_solver(m, "(exists ((t Tuple)) (not (= a (first t))))");
test_quant_solver(m, "(exists ((t Tuple)) (not (= P (second t))))");
test_quant_solver(m, "(exists ((t Tuple)) (not (= r2 (third t))))");
}