diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index a83b4a035..35a055329 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -23,6 +23,66 @@ Notes: #include"smt_params_helper.hpp" #include"rewriter_types.h" #include"filter_model_converter.h" +#include"ast_util.h" + +typedef obj_map expr2expr_map; + +void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector& assumptions, scoped_ptr& bool2dep, ref& fmc) { + scoped_ptr dep2bool; + dep2bool = alloc(expr2expr_map); + bool2dep = alloc(expr2expr_map); + ptr_vector deps; + ast_manager& m = g->m(); + expr_ref_vector clause(m); + unsigned sz = g->size(); + for (unsigned i = 0; i < sz; i++) { + expr * f = g->form(i); + expr_dependency * d = g->dep(i); + if (d == 0) { + clauses.push_back(f); + } + else { + // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f. + clause.reset(); + clause.push_back(f); + deps.reset(); + m.linearize(d, deps); + SASSERT(!deps.empty()); // d != 0, then deps must not be empty + ptr_vector::iterator it = deps.begin(); + ptr_vector::iterator end = deps.end(); + for (; it != end; ++it) { + expr * d = *it; + if (is_uninterp_const(d) && m.is_bool(d)) { + // no need to create a fresh boolean variable for d + if (!bool2dep->contains(d)) { + assumptions.push_back(d); + bool2dep->insert(d, d); + } + clause.push_back(m.mk_not(d)); + } + else { + // must normalize assumption + expr * b = 0; + if (!dep2bool->find(d, b)) { + b = m.mk_fresh_const(0, m.mk_bool_sort()); + dep2bool->insert(d, b); + bool2dep->insert(b, d); + assumptions.push_back(b); + if (!fmc) { + fmc = alloc(filter_model_converter, m); + } + fmc->insert(to_app(b)->get_decl()); + } + clause.push_back(m.mk_not(b)); + } + } + SASSERT(clause.size() > 1); + expr_ref cls(m); + cls = mk_or(m, clauses.size(), clauses.c_ptr()); + clauses.push_back(cls); + } + } +} class smt_tactic : public tactic { smt_params m_params; @@ -128,7 +188,6 @@ public: } }; - typedef obj_map expr2expr_map; virtual void operator()(goal_ref const & in, goal_ref_buffer & result, @@ -147,65 +206,17 @@ public: TRACE("smt_tactic_memory", tout << "wasted_size: " << m.get_allocator().get_wasted_size() << "\n";); scoped_init_ctx init(*this, m); SASSERT(m_ctx != 0); - - scoped_ptr dep2bool; - scoped_ptr bool2dep; - ptr_vector assumptions; + + expr_ref_vector clauses(m); + scoped_ptr bool2dep; + ptr_vector assumptions; ref fmc; if (in->unsat_core_enabled()) { if (in->proofs_enabled()) throw tactic_exception("smt tactic does not support simultaneous generation of proofs and unsat cores"); - dep2bool = alloc(expr2expr_map); - bool2dep = alloc(expr2expr_map); - ptr_vector deps; - ptr_vector clause; - unsigned sz = in->size(); - for (unsigned i = 0; i < sz; i++) { - expr * f = in->form(i); - expr_dependency * d = in->dep(i); - if (d == 0) { - m_ctx->assert_expr(f); - } - else { - // create clause (not d1 \/ ... \/ not dn \/ f) when the d's are the assumptions/dependencies of f. - clause.reset(); - clause.push_back(f); - deps.reset(); - m.linearize(d, deps); - SASSERT(!deps.empty()); // d != 0, then deps must not be empty - ptr_vector::iterator it = deps.begin(); - ptr_vector::iterator end = deps.end(); - for (; it != end; ++it) { - expr * d = *it; - if (is_uninterp_const(d) && m.is_bool(d)) { - // no need to create a fresh boolean variable for d - if (!bool2dep->contains(d)) { - assumptions.push_back(d); - bool2dep->insert(d, d); - } - clause.push_back(m.mk_not(d)); - } - else { - // must normalize assumption - expr * b = 0; - if (!dep2bool->find(d, b)) { - b = m.mk_fresh_const(0, m.mk_bool_sort()); - dep2bool->insert(d, b); - bool2dep->insert(b, d); - assumptions.push_back(b); - if (!fmc) { - fmc = alloc(filter_model_converter, m); - } - fmc->insert(to_app(b)->get_decl()); - } - clause.push_back(m.mk_not(b)); - } - } - SASSERT(clause.size() > 1); - expr_ref cls(m); - cls = m.mk_or(clause.size(), clause.c_ptr()); - m_ctx->assert_expr(cls); - } + extract_clauses_and_dependencies(in, clauses, assumptions, bool2dep, fmc); + for (unsigned i = 0; i < clauses.size(); ++i) { + m_ctx->assert_expr(clauses[i].get()); } } else if (in->proofs_enabled()) { diff --git a/src/smt/tactic/smt_tactic.h b/src/smt/tactic/smt_tactic.h index 521a454f7..631c345c7 100644 --- a/src/smt/tactic/smt_tactic.h +++ b/src/smt/tactic/smt_tactic.h @@ -20,15 +20,21 @@ Notes: #define _SMT_TACTIC_H_ #include"params.h" +#include"ast.h" +#include"obj_hashtable.h" +#include"goal.h" class tactic; +class filter_model_converter; tactic * mk_smt_tactic(params_ref const & p = params_ref()); // syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config) tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref()); + +void extract_clauses_and_dependencies(goal_ref const& g, expr_ref_vector& clauses, ptr_vector& assumptions, scoped_ptr >& bool2dep, ref& fmc); + /* ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)") */ - #endif diff --git a/src/tactic/nlsat_smt/nl_purify_tactic.cpp b/src/tactic/nlsat_smt/nl_purify_tactic.cpp index 0484c2ce2..f7acf529f 100644 --- a/src/tactic/nlsat_smt/nl_purify_tactic.cpp +++ b/src/tactic/nlsat_smt/nl_purify_tactic.cpp @@ -115,8 +115,6 @@ public: arith_util & u() { return m_owner.m_util; } - bool produce_proofs() const { return m_owner.m_produce_proofs; } - expr * mk_interface_var(expr* arg) { expr* r; if (m_interface_cache.find(arg, r)) { @@ -145,7 +143,7 @@ public: return is_app(e) && (to_app(e)->get_family_id() == u().get_family_id()); } - void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result) { + void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref& pr) { expr_ref old_pred(m.mk_app(f, num, args), m); polarity_t pol; VERIFY(m_polarities.find(old_pred, pol)); @@ -154,10 +152,13 @@ public: m_new_preds.push_back(to_app(result)); m_owner.m_fmc->insert(to_app(result)->get_decl()); if (pol != pol_neg) { - m_owner.m_nl_g->assert_expr(m.mk_or(m.mk_not(result), m.mk_app(f, num, args))); + m_owner.m_nl_g->assert_expr(m.mk_or(m.mk_not(result), old_pred)); } if (pol != pol_pos) { - m_owner.m_nl_g->assert_expr(m.mk_or(result, m.mk_not(m.mk_app(f, num, args)))); + m_owner.m_nl_g->assert_expr(m.mk_or(result, m.mk_not(old_pred))); + } + if (m_owner.m_produce_proofs) { + pr = m.mk_oeq(old_pred, result); } TRACE("nlsat_smt", tout << old_pred << " : " << result << "\n";); } @@ -183,7 +184,7 @@ public: br_status reduce_app_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { if (f->get_family_id() == m.get_basic_family_id()) { if (f->get_decl_kind() == OP_EQ && u().is_real(args[0])) { - mk_interface_bool(f, num, args, result); + mk_interface_bool(f, num, args, result, pr); return BR_DONE; } else { @@ -194,7 +195,7 @@ public: switch (f->get_decl_kind()) { case OP_LE: case OP_GE: case OP_LT: case OP_GT: // these are the only real cases of non-linear atomic formulas besides equality. - mk_interface_bool(f, num, args, result); + mk_interface_bool(f, num, args, result, pr); return BR_DONE; default: return BR_FAILED; @@ -209,12 +210,14 @@ public: bool is_arith_op(expr* e) { return is_app(e) && to_app(e)->get_family_id() == u().get_family_id(); } + br_status reduce_app_real(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref & pr) { bool has_interface = false; bool is_arith = false; if (f->get_family_id() == u().get_family_id()) { switch (f->get_decl_kind()) { - case OP_NUM: case OP_IRRATIONAL_ALGEBRAIC_NUM: + case OP_NUM: + case OP_IRRATIONAL_ALGEBRAIC_NUM: return BR_FAILED; default: is_arith = true; @@ -238,6 +241,9 @@ public: } if (has_interface) { result = m.mk_app(f, num, m_args.c_ptr()); + if (m_owner.m_produce_proofs) { + pr = m.mk_oeq(m.mk_app(f, num, args), result); // push proof object to mk_interface_var? + } TRACE("nlsat_smt", tout << result << "\n";); return BR_DONE; } @@ -264,6 +270,7 @@ private: } }; + arith_util & u() { return m_util; } void check_point() { @@ -727,7 +734,6 @@ public: r.set_bool_mode(); rewrite_goal(r, g); - g->inc_depth(); for (unsigned i = 0; i < g->size(); ++i) { m_solver->assert_expr(g->form(i)); } @@ -740,3 +746,43 @@ public: tactic * mk_nl_purify_tactic(ast_manager& m, params_ref const& p) { return alloc(nl_purify_tactic, m, p); } + +#if 0 + void mark_interface_vars(goal_ref const& g) { + expr_mark visited; + ptr_vector todo; + unsigned sz = g->size(); + for (unsigned i = 0; i < sz; i++) { + todo.push_back(g->form(i)); + } + while (!todo.empty()) { + expr* e = todo.back(); + todo.pop_back(); + if (visited.is_marked(e)) { + continue; + } + visited.mark(e); + if (is_quantifier(e)) { + todo.push_back(to_quantifier(e)->get_expr()); + continue; + } + if (is_var(e)) { + continue; + } + app* ap = to_app(e); + sz = ap->get_num_args(); + bool is_arith = is_arith_op(e); + for (unsigned i = 0; i < sz; ++i) { + expr* arg = ap->get_arg(i); + todo.push_back(arg); + if (is_arith && !is_arith_op(arg)) { + m_interface_vars.mark(arg); + } + else if (!is_arith && is_arith_op(arg) && ap->get_family_id() != m.get_basic_family_id()) { + m_interface_vars.mark(arg); + } + } + } + + } +#endif