diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp index be730a5c7..74ab001b4 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.cpp +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.cpp @@ -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 todo; - for (unsigned i=u_len; iget_tail(i)); SASSERT(!r->is_neg_tail(i)); } m_rule_subst.reset(r); + obj_hashtable 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) { diff --git a/src/muz_qe/dl_mk_interp_tail_simplifier.h b/src/muz_qe/dl_mk_interp_tail_simplifier.h index 99bda325f..5e4fd8fbc 100644 --- a/src/muz_qe/dl_mk_interp_tail_simplifier.h +++ b/src/muz_qe/dl_mk_interp_tail_simplifier.h @@ -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; diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index c56cb5abc..b5e6b9305 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -655,9 +655,7 @@ namespace datalog { tail.push_back(ensure_app(conjs[i].get())); } tail_neg.resize(tail.size(), false); - IF_VERBOSE(1, r->display(m_ctx, verbose_stream() << "reducing rule\n");); r = mk(r->get_head(), tail.size(), tail.c_ptr(), tail_neg.c_ptr()); - IF_VERBOSE(1, r->display(m_ctx, verbose_stream() << "reduced rule\n");); TRACE("dl", r->display(m_ctx, tout << "reduced rule\n");); } } diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index e85cbc031..5481bf218 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -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)) { diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index 045411fb1..1e7ba27c7 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -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"); } diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index a543593b3..33298c515 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -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 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 const& formulas) { ptr_vector 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 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 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 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 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 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 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); diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp index 49a36e5f1..ec042e33d 100644 --- a/src/muz_qe/qe_lite.cpp +++ b/src/muz_qe/qe_lite.cpp @@ -15,148 +15,47 @@ Author: Revision History: - - TBD: integrate Fourier Motzkin elimination - integrate Gaussean elimination --*/ #include "qe_lite.h" #include "expr_abstract.h" #include "used_vars.h" -#include"occurs.h" -#include"for_each_expr.h" -#include"rewriter_def.h" -#include"ast_pp.h" -#include"ast_ll_pp.h" -#include"ast_smt2_pp.h" -#include"tactical.h" -#include"bool_rewriter.h" -#include"var_subst.h" -#include"uint_set.h" -#include"dl_util.h" -#include"th_rewriter.h" +#include "occurs.h" +#include "for_each_expr.h" +#include "rewriter_def.h" +#include "ast_pp.h" +#include "ast_ll_pp.h" +#include "ast_smt2_pp.h" +#include "tactical.h" +#include "bool_rewriter.h" +#include "var_subst.h" +#include "uint_set.h" +#include "dl_util.h" +#include "th_rewriter.h" +#include "dl_util.h" -static void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsigned_vector & order) { - order.reset(); - - // eliminate self loops, and definitions containing quantifiers. - bool found = false; - for (unsigned i = 0; i < definitions.size(); i++) { - var * v = vars[i]; - expr * t = definitions[i]; - if (t == 0 || has_quantifiers(t) || occurs(v, t)) - definitions[i] = 0; - else - found = true; // found at least one candidate - } - - if (!found) - return; +class is_variable_proc { +public: + virtual bool operator()(expr* e) const = 0; +}; - typedef std::pair frame; - svector todo; - - expr_fast_mark1 visiting; - expr_fast_mark2 done; - - unsigned vidx, num; - - for (unsigned i = 0; i < definitions.size(); i++) { - if (definitions[i] == 0) - continue; - var * v = vars[i]; - SASSERT(v->get_idx() == i); - SASSERT(todo.empty()); - todo.push_back(frame(v, 0)); - while (!todo.empty()) { - start: - frame & fr = todo.back(); - expr * t = fr.first; - if (t->get_ref_count() > 1 && done.is_marked(t)) { - todo.pop_back(); - continue; - } - switch (t->get_kind()) { - case AST_VAR: - vidx = to_var(t)->get_idx(); - if (fr.second == 0) { - CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";); - // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula. - if (definitions.get(vidx, 0) != 0) { - if (visiting.is_marked(t)) { - // cycle detected: remove t - visiting.reset_mark(t); - definitions[vidx] = 0; - } - else { - visiting.mark(t); - fr.second = 1; - todo.push_back(frame(definitions[vidx], 0)); - goto start; - } - } - } - else { - SASSERT(fr.second == 1); - if (definitions.get(vidx, 0) != 0) { - visiting.reset_mark(t); - order.push_back(vidx); - } - else { - // var was removed from the list of candidate vars to elim cycle - // do nothing - } - } - if (t->get_ref_count() > 1) - done.mark(t); - todo.pop_back(); - break; - case AST_QUANTIFIER: - UNREACHABLE(); - todo.pop_back(); - break; - case AST_APP: - num = to_app(t)->get_num_args(); - while (fr.second < num) { - expr * arg = to_app(t)->get_arg(fr.second); - fr.second++; - if (arg->get_ref_count() > 1 && done.is_marked(arg)) - continue; - todo.push_back(frame(arg, 0)); - goto start; - } - if (t->get_ref_count() > 1) - done.mark(t); - todo.pop_back(); - break; - default: - UNREACHABLE(); - todo.pop_back(); - break; - } - } - } -} - - -class der2 { - ast_manager & m; - var_subst m_subst; - expr_ref_buffer m_new_exprs; - - ptr_vector m_map; - int_vector m_pos2var; - ptr_vector m_inx2var; - unsigned_vector m_order; - expr_ref_vector m_subst_map; - expr_ref_buffer m_new_args; - th_rewriter m_rewriter; - unsigned m_num_decls; - uint_set m_var_set; +class is_variable_test : public is_variable_proc { enum is_var_kind { BY_VAR_SET, BY_VAR_SET_COMPLEMENT, BY_NUM_DECLS }; - is_var_kind m_var_kind; + uint_set m_var_set; + unsigned m_num_decls; + is_var_kind m_var_kind; +public: + is_variable_test(uint_set const& vars, bool index_of_bound) : + m_var_set(vars), + m_num_decls(0), + m_var_kind(index_of_bound?BY_VAR_SET:BY_VAR_SET_COMPLEMENT) {} - bool is_variable(expr * e) const { + is_variable_test(unsigned num_decls) : + m_num_decls(num_decls), + m_var_kind(BY_NUM_DECLS) {} + + virtual bool operator()(expr* e) const { if (!is_var(e)) { return false; } @@ -172,6 +71,128 @@ class der2 { UNREACHABLE(); return false; } +}; + + +class der2 { + ast_manager & m; + is_variable_proc* m_is_variable; + var_subst m_subst; + expr_ref_buffer m_new_exprs; + + ptr_vector m_map; + int_vector m_pos2var; + ptr_vector m_inx2var; + unsigned_vector m_order; + expr_ref_vector m_subst_map; + expr_ref_buffer m_new_args; + th_rewriter m_rewriter; + + void der_sort_vars(ptr_vector & vars, ptr_vector & definitions, unsigned_vector & order) { + order.reset(); + + // eliminate self loops, and definitions containing quantifiers. + bool found = false; + for (unsigned i = 0; i < definitions.size(); i++) { + var * v = vars[i]; + expr * t = definitions[i]; + if (t == 0 || has_quantifiers(t) || occurs(v, t)) + definitions[i] = 0; + else + found = true; // found at least one candidate + } + + if (!found) + return; + + typedef std::pair frame; + svector todo; + + expr_fast_mark1 visiting; + expr_fast_mark2 done; + + unsigned vidx, num; + + for (unsigned i = 0; i < definitions.size(); i++) { + if (definitions[i] == 0) + continue; + var * v = vars[i]; + SASSERT(v->get_idx() == i); + SASSERT(todo.empty()); + todo.push_back(frame(v, 0)); + while (!todo.empty()) { + start: + frame & fr = todo.back(); + expr * t = fr.first; + if (t->get_ref_count() > 1 && done.is_marked(t)) { + todo.pop_back(); + continue; + } + switch (t->get_kind()) { + case AST_VAR: + vidx = to_var(t)->get_idx(); + if (fr.second == 0) { + CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";); + // Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula. + if (definitions.get(vidx, 0) != 0) { + if (visiting.is_marked(t)) { + // cycle detected: remove t + visiting.reset_mark(t); + definitions[vidx] = 0; + } + else { + visiting.mark(t); + fr.second = 1; + todo.push_back(frame(definitions[vidx], 0)); + goto start; + } + } + } + else { + SASSERT(fr.second == 1); + if (definitions.get(vidx, 0) != 0) { + visiting.reset_mark(t); + order.push_back(vidx); + } + else { + // var was removed from the list of candidate vars to elim cycle + // do nothing + } + } + if (t->get_ref_count() > 1) + done.mark(t); + todo.pop_back(); + break; + case AST_QUANTIFIER: + UNREACHABLE(); + todo.pop_back(); + break; + case AST_APP: + num = to_app(t)->get_num_args(); + while (fr.second < num) { + expr * arg = to_app(t)->get_arg(fr.second); + fr.second++; + if (arg->get_ref_count() > 1 && done.is_marked(arg)) + continue; + todo.push_back(frame(arg, 0)); + goto start; + } + if (t->get_ref_count() > 1) + done.mark(t); + todo.pop_back(); + break; + default: + UNREACHABLE(); + todo.pop_back(); + break; + } + } + } + } + + bool is_variable(expr * e) const { + return (*m_is_variable)(e); + } bool is_neg_var(ast_manager & m, expr * e) { expr* e1; @@ -365,8 +386,8 @@ class der2 { void reduce_quantifier1(quantifier * q, expr_ref & r, proof_ref & pr) { expr * e = q->get_expr(); - m_num_decls = q->get_num_decls(); - m_var_kind = BY_NUM_DECLS; + is_variable_test is_v(q->get_num_decls()); + set_is_variable_proc(is_v); unsigned num_args = 1; expr* const* args = &e; if ((q->is_forall() && m.is_or(e)) || @@ -440,11 +461,9 @@ class der2 { } } - void reduce_var_set(expr_ref& r) { - expr_ref_vector conjs(m); + bool reduce_var_set(expr_ref_vector& conjs) { unsigned def_count = 0; unsigned largest_vinx = 0; - datalog::flatten_and(r, conjs); find_definitions(conjs.size(), conjs.c_ptr(), true, def_count, largest_vinx); @@ -453,18 +472,24 @@ class der2 { SASSERT(m_order.size() <= def_count); // some might be missing because of cycles if (!m_order.empty()) { - expr_ref new_r(m); + expr_ref r(m), new_r(m); + r = m.mk_and(conjs.size(), conjs.c_ptr()); create_substitution(largest_vinx + 1); m_subst(r, m_subst_map.size(), m_subst_map.c_ptr(), new_r); m_rewriter(new_r); - r = new_r; + conjs.reset(); + datalog::flatten_and(new_r, conjs); + return true; } } + return false; } public: - der2(ast_manager & m): m(m), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m) {} + der2(ast_manager & m): m(m), m_is_variable(0), m_subst(m), m_new_exprs(m), m_subst_map(m), m_new_args(m), m_rewriter(m) {} + + void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} void operator()(quantifier * q, expr_ref & r, proof_ref & pr) { TRACE("der", tout << mk_pp(q, m) << "\n";); @@ -491,132 +516,114 @@ public: m_new_exprs.reset(); } - // Keep applying reduce_var-set until r doesn't change anymore - void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& r) { - m_var_kind = index_of_bound?BY_VAR_SET:BY_VAR_SET_COMPLEMENT; - m_var_set = index_set; - expr_ref prev(m); - do { - prev = r; - reduce_var_set(r); - } while (prev != r); + void operator()(expr_ref_vector& r) { + while (reduce_var_set(r)) ; m_new_exprs.reset(); } - void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& r) { - expr_ref fml(m); - fml = m.mk_and(r.size(), r.c_ptr()); - (*this)(index_set, index_of_bound, fml); - r.reset(); - datalog::flatten_and(fml, r); - } - ast_manager& get_manager() const { return m; } }; // ------------------------------------------------------------ // fm_tactic adapted to eliminate designated de-Brujin indices. -typedef ptr_vector clauses; -//typedef unsigned var; -typedef int bvar; -typedef int literal; -typedef svector var_vector; +namespace fm { + typedef ptr_vector clauses; + typedef unsigned var; + typedef int bvar; + typedef int literal; + typedef svector var_vector; -// Encode the constraint -// lits \/ ( as[0]*xs[0] + ... + as[num_vars-1]*xs[num_vars-1] <= c -// if strict is true, then <= is <. -struct constraint { - static unsigned get_obj_size(unsigned num_lits, unsigned num_vars) { - return sizeof(constraint) + num_lits*sizeof(literal) + num_vars*(sizeof(var) + sizeof(rational)); - } - unsigned m_id; - unsigned m_num_lits:29; - unsigned m_strict:1; - unsigned m_dead:1; - unsigned m_mark:1; - unsigned m_num_vars; - literal * m_lits; - var * m_xs; - rational * m_as; - rational m_c; - expr_dependency * m_dep; - ~constraint() { - rational * it = m_as; - rational * end = it + m_num_vars; - for (; it != end; ++it) - it->~rational(); - } - - unsigned hash() const { return hash_u(m_id); } -}; - -typedef ptr_vector constraints; - -class constraint_set { - unsigned_vector m_id2pos; - constraints m_set; -public: - typedef constraints::const_iterator iterator; - - bool contains(constraint const & c) const { - if (c.m_id >= m_id2pos.size()) - return false; - return m_id2pos[c.m_id] != UINT_MAX; - } - - bool empty() const { return m_set.empty(); } - unsigned size() const { return m_set.size(); } - - void insert(constraint & c) { - unsigned id = c.m_id; - m_id2pos.reserve(id+1, UINT_MAX); - if (m_id2pos[id] != UINT_MAX) - return; // already in the set - unsigned pos = m_set.size(); - m_id2pos[id] = pos; - m_set.push_back(&c); - } - - void erase(constraint & c) { - unsigned id = c.m_id; - if (id >= m_id2pos.size()) - return; - unsigned pos = m_id2pos[id]; - if (pos == UINT_MAX) - return; - m_id2pos[id] = UINT_MAX; - unsigned last_pos = m_set.size() - 1; - if (pos != last_pos) { - constraint * last_c = m_set[last_pos]; - m_set[pos] = last_c; - m_id2pos[last_c->m_id] = pos; + // Encode the constraint + // lits \/ ( as[0]*xs[0] + ... + as[num_vars-1]*xs[num_vars-1] <= c + // if strict is true, then <= is <. + struct constraint { + static unsigned get_obj_size(unsigned num_lits, unsigned num_vars) { + return sizeof(constraint) + num_lits*sizeof(literal) + num_vars*(sizeof(var) + sizeof(rational)); + } + unsigned m_id; + unsigned m_num_lits:29; + unsigned m_strict:1; + unsigned m_dead:1; + unsigned m_mark:1; + unsigned m_num_vars; + literal * m_lits; + var * m_xs; + rational * m_as; + rational m_c; + expr_dependency * m_dep; + ~constraint() { + rational * it = m_as; + rational * end = it + m_num_vars; + for (; it != end; ++it) + it->~rational(); } - m_set.pop_back(); - } - constraint & erase() { - SASSERT(!empty()); - constraint & c = *m_set.back(); - m_id2pos[c.m_id] = UINT_MAX; - m_set.pop_back(); - return c; - } + unsigned hash() const { return hash_u(m_id); } + }; - void reset() { m_id2pos.reset(); m_set.reset(); } - void finalize() { m_id2pos.finalize(); m_set.finalize(); } + typedef ptr_vector constraints; - iterator begin() const { return m_set.begin(); } - iterator end() const { return m_set.end(); } -}; - - -#if 0 - - + class constraint_set { + unsigned_vector m_id2pos; + constraints m_set; + public: + typedef constraints::const_iterator iterator; + + bool contains(constraint const & c) const { + if (c.m_id >= m_id2pos.size()) + return false; + return m_id2pos[c.m_id] != UINT_MAX; + } + + bool empty() const { return m_set.empty(); } + unsigned size() const { return m_set.size(); } + + void insert(constraint & c) { + unsigned id = c.m_id; + m_id2pos.reserve(id+1, UINT_MAX); + if (m_id2pos[id] != UINT_MAX) + return; // already in the set + unsigned pos = m_set.size(); + m_id2pos[id] = pos; + m_set.push_back(&c); + } + + void erase(constraint & c) { + unsigned id = c.m_id; + if (id >= m_id2pos.size()) + return; + unsigned pos = m_id2pos[id]; + if (pos == UINT_MAX) + return; + m_id2pos[id] = UINT_MAX; + unsigned last_pos = m_set.size() - 1; + if (pos != last_pos) { + constraint * last_c = m_set[last_pos]; + m_set[pos] = last_c; + m_id2pos[last_c->m_id] = pos; + } + m_set.pop_back(); + } + + constraint & erase() { + SASSERT(!empty()); + constraint & c = *m_set.back(); + m_id2pos[c.m_id] = UINT_MAX; + m_set.pop_back(); + return c; + } + + void reset() { m_id2pos.reset(); m_set.reset(); } + void finalize() { m_id2pos.finalize(); m_set.finalize(); } + + iterator begin() const { return m_set.begin(); } + iterator end() const { return m_set.end(); } + }; - struct imp { + class fm { ast_manager & m; + is_variable_proc* m_is_variable; small_object_allocator m_allocator; arith_util m_util; constraints m_constraints; @@ -630,12 +637,10 @@ public: unsigned_vector m_var2pos; vector m_lowers; vector m_uppers; - obj_hashtable m_forbidden_set; // variables that cannot be eliminated because occur in non OCC ineq part - goal_ref m_new_goal; - ref m_mc; + uint_set m_forbidden_set; // variables that cannot be eliminated because occur in non OCC ineq part + expr_ref_vector m_new_fmls; volatile bool m_cancel; id_gen m_id_gen; - bool m_produce_models; bool m_fm_real_only; unsigned m_fm_limit; unsigned m_fm_cutoff1; @@ -664,11 +669,12 @@ public: } bool is_var(expr * t, expr * & x) const { - if (is_uninterp_const(t)) { + + if ((*m_is_variable)(t)) { x = t; return true; } - else if (m_util.is_to_real(t) && is_uninterp_const(to_app(t)->get_arg(0))) { + else if (m_util.is_to_real(t) && (*m_is_variable)(to_app(t)->get_arg(0))) { x = to_app(t)->get_arg(0); return true; } @@ -713,7 +719,8 @@ public: if (visited.is_marked(x)) return false; // duplicates are not supported... must simplify first visited.mark(x); - if (!m_forbidden_set.contains(to_app(x)->get_decl()) && (!m_fm_real_only || !m_util.is_int(x))) + SASSERT(::is_var(x)); + if (!m_forbidden_set.contains(::to_var(x)->get_idx()) && (!m_fm_real_only || !m_util.is_int(x))) all_forbidden = false; } return !all_forbidden; @@ -1008,6 +1015,8 @@ public: backward_subsumption(c); } } + + public: // --------------------------- // @@ -1015,18 +1024,19 @@ public: // // --------------------------- - imp(ast_manager & _m, params_ref const & p): + fm(ast_manager & _m, params_ref const & p): m(_m), - m_allocator("fm-tactic"), + m_allocator("fm-elim"), m_util(m), m_bvar2expr(m), m_var2expr(m), + m_new_fmls(m), m_inconsistent_core(m) { updt_params(p); m_cancel = false; } - ~imp() { + ~fm() { reset_constraints(); } @@ -1043,26 +1053,27 @@ public: void set_cancel(bool f) { m_cancel = f; } + private: struct forbidden_proc { - imp & m_owner; - forbidden_proc(imp & o):m_owner(o) {} - void operator()(::var * n) {} - void operator()(app * n) { - if (is_uninterp_const(n) && m_owner.m.get_sort(n)->get_family_id() == m_owner.m_util.get_family_id()) { - m_owner.m_forbidden_set.insert(n->get_decl()); + fm & m_owner; + forbidden_proc(fm & o):m_owner(o) {} + void operator()(::var * n) { + if (m_owner.is_var(n) && m_owner.m.get_sort(n)->get_family_id() == m_owner.m_util.get_family_id()) { + m_owner.m_forbidden_set.insert(n->get_idx()); } } + void operator()(app * n) { } void operator()(quantifier * n) {} }; - void init_forbidden_set(goal const & g) { + void init_forbidden_set(expr_ref_vector const & g) { m_forbidden_set.reset(); expr_fast_mark1 visited; forbidden_proc proc(*this); unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { - expr * f = g.form(i); + expr * f = g[i]; if (is_occ(f)) continue; TRACE("is_occ_bug", tout << "not OCC:\n" << mk_ismt2_pp(f, m) << "\n";); @@ -1070,7 +1081,7 @@ public: } } - void init(goal const & g) { + void init(expr_ref_vector const & g) { m_sub_todo.reset(); m_id_gen.reset(); reset_constraints(); @@ -1086,8 +1097,7 @@ public: m_expr2var.reset(); m_lowers.reset(); m_uppers.reset(); - m_new_goal = 0; - m_mc = 0; + m_new_fmls.reset(); m_counter = 0; m_inconsistent = false; m_inconsistent_core = 0; @@ -1178,7 +1188,7 @@ public: } var mk_var(expr * t) { - SASSERT(is_uninterp_const(t)); + SASSERT(::is_var(t)); SASSERT(m_util.is_int(t) || m_util.is_real(t)); var x = m_var2expr.size(); m_var2expr.push_back(t); @@ -1188,7 +1198,7 @@ public: m_expr2var.insert(t, x); m_lowers.push_back(constraints()); m_uppers.push_back(constraints()); - bool forbidden = m_forbidden_set.contains(to_app(t)->get_decl()) || (m_fm_real_only && is_int); + bool forbidden = m_forbidden_set.contains(::to_var(t)->get_idx()) || (m_fm_real_only && is_int); m_forbidden.push_back(forbidden); SASSERT(m_var2expr.size() == m_is_int.size()); SASSERT(m_lowers.size() == m_is_int.size()); @@ -1363,22 +1373,20 @@ public: } else { TRACE("add_constraint_bug", tout << "all variables are forbidden "; display(tout, *c); tout << "\n";); - m_new_goal->assert_expr(to_expr(*c), 0, c->m_dep); + m_new_fmls.push_back(to_expr(*c)); del_constraint(c); return false; } } - void init_use_list(goal const & g) { + void init_use_list(expr_ref_vector const & g) { unsigned sz = g.size(); - for (unsigned i = 0; i < sz; i++) { - if (m_inconsistent) - return; - expr * f = g.form(i); + for (unsigned i = 0; !m_inconsistent && i < sz; i++) { + expr * f = g[i]; if (is_occ(f)) - add_constraint(f, g.dep(i)); + add_constraint(f, 0); else - m_new_goal->assert_expr(f, 0, g.dep(i)); + m_new_fmls.push_back(f); } } @@ -1502,14 +1510,7 @@ public: } clauses tmp_clauses; - void save_constraints(var x) { - if (m_produce_models) { - tmp_clauses.reset(); - copy_constraints(m_lowers[x], tmp_clauses); - copy_constraints(m_uppers[x], tmp_clauses); - m_mc->insert(to_app(m_var2expr.get(x))->get_decl(), tmp_clauses); - } - } + void save_constraints(var x) { } void mark_constraints_dead(constraints const & cs) { constraints::const_iterator it = cs.begin(); @@ -1706,7 +1707,7 @@ public: if (l.empty() || u.empty()) { // easy case mark_constraints_dead(x); - TRACE("fm", tout << "variables was eliminated (trivial case)\n";); + TRACE("fm", tout << "variable was eliminated (trivial case)\n";); return true; } @@ -1776,62 +1777,45 @@ public: c->m_dead = true; expr * new_f = to_expr(*c); TRACE("fm_bug", tout << "asserting...\n" << mk_ismt2_pp(new_f, m) << "\nnew_dep: " << c->m_dep << "\n";); - m_new_goal->assert_expr(new_f, 0, c->m_dep); + m_new_fmls.push_back(new_f); } } } v2cs.finalize(); } - // Copy remaining clauses to m_new_goal + // Copy remaining clauses to m_new_fmls void copy_remaining() { copy_remaining(m_uppers); copy_remaining(m_lowers); } void checkpoint() { - cooperate("fm"); + // cooperate("fm"); if (m_cancel) throw tactic_exception(TACTIC_CANCELED_MSG); if (memory::get_allocation_size() > m_max_memory) throw tactic_exception(TACTIC_MAX_MEMORY_MSG); } - - virtual void operator()(goal_ref const & g, - goal_ref_buffer & result, - model_converter_ref & mc, - proof_converter_ref & pc, - expr_dependency_ref & core) { - SASSERT(g->is_well_sorted()); - mc = 0; pc = 0; core = 0; - tactic_report report("fm", *g); - fail_if_proof_generation("fm", g); - m_produce_models = g->models_enabled(); - - init(*g); - - m_new_goal = alloc(goal, *g, true); - SASSERT(m_new_goal->depth() == g->depth()); - SASSERT(m_new_goal->prec() == g->prec()); - m_new_goal->inc_depth(); + public: - init_use_list(*g); - + void set_is_variable_proc(is_variable_proc& proc) { m_is_variable = &proc;} + + + void operator()(expr_ref_vector& fmls) { + init(fmls); + init_use_list(fmls); if (m_inconsistent) { - m_new_goal->reset(); - m_new_goal->assert_expr(m.mk_false(), 0, m_inconsistent_core); + m_new_fmls.reset(); + m_new_fmls.push_back(m.mk_false()); } else { TRACE("fm", display(tout);); subsume(); var_vector candidates; - sort_candidates(candidates); - - unsigned eliminated = 0; - - if (m_produce_models) - m_mc = alloc(fm_model_converter, m); + sort_candidates(candidates); + unsigned eliminated = 0; unsigned num = candidates.size(); for (unsigned i = 0; i < num; i++) { @@ -1842,23 +1826,19 @@ public: if (try_eliminate(candidates[i])) eliminated++; if (m_inconsistent) { - m_new_goal->reset(); - m_new_goal->assert_expr(m.mk_false(), 0, m_inconsistent_core); + m_new_fmls.reset(); + m_new_fmls.push_back(m.mk_false()); break; } } - report_tactic_progress(":fm-eliminated", eliminated); - report_tactic_progress(":fm-cost", m_counter); if (!m_inconsistent) { copy_remaining(); - mc = m_mc.get(); } } reset_constraints(); - result.push_back(m_new_goal.get()); - TRACE("fm", m_new_goal->display(tout);); - SASSERT(m_new_goal->is_well_sorted()); - } + fmls.reset(); + fmls.append(m_new_fmls); + } void display_constraints(std::ostream & out, constraints const & cs) const { constraints::const_iterator it = cs.begin(); @@ -1882,14 +1862,16 @@ public: } }; -#endif +} // namespace fm class qe_lite::impl { ast_manager& m; der2 m_der; + params_ref m_params; + fm::fm m_fm; public: - impl(ast_manager& m): m(m), m_der(m) {} + impl(ast_manager& m): m(m), m_der(m), m_fm(m, m_params) {} void operator()(app_ref_vector& vars, expr_ref& fml) { if (vars.empty()) { @@ -1939,11 +1921,23 @@ public: } void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml) { - m_der(index_set, index_of_bound, fml); + expr_ref_vector conjs(m); + conjs.push_back(fml); + (*this)(index_set, index_of_bound, conjs); + bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), fml); } + void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& fmls) { - m_der(index_set, index_of_bound, fmls); + datalog::flatten_and(fmls); + is_variable_test is_var(index_set, index_of_bound); + TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";); + IF_VERBOSE(3, for (unsigned i = 0; i < fmls.size(); ++i) verbose_stream() << mk_pp(fmls[i].get(), m) << "\n";); + m_der.set_is_variable_proc(is_var); + m_der(fmls); + m_fm.set_is_variable_proc(is_var); + m_fm(fmls); + TRACE("qe_lite", for (unsigned i = 0; i < fmls.size(); ++i) tout << mk_pp(fmls[i].get(), m) << "\n";); } };