diff --git a/src/ast/rewriter/bool_rewriter.h b/src/ast/rewriter/bool_rewriter.h index 8f2221a8ce..4889490845 100644 --- a/src/ast/rewriter/bool_rewriter.h +++ b/src/ast/rewriter/bool_rewriter.h @@ -81,7 +81,10 @@ class bool_rewriter { void push_new_arg(expr* arg, expr_ref_vector& new_args, expr_fast_mark1& neg_lits, expr_fast_mark2& pos_lits); public: - bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_hoist(m), m_local_ctx_cost(0) { updt_params(p); } + bool_rewriter(ast_manager & m, params_ref const & p = params_ref()):m_manager(m), m_hoist(m), m_local_ctx_cost(0) { + updt_params(p); + m_hoist.set(*this); + } ast_manager & m() const { return m_manager; } family_id get_fid() const { return m().get_basic_family_id(); } bool is_eq(expr * t) const { return m().is_eq(t); } diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp index 40ad4604a6..b86f1eb47b 100644 --- a/src/ast/rewriter/hoist_rewriter.cpp +++ b/src/ast/rewriter/hoist_rewriter.cpp @@ -17,16 +17,30 @@ Module Name: #include "ast/rewriter/hoist_rewriter.h" +#include "ast/rewriter/bool_rewriter.h" #include "ast/ast_util.h" #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" - hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p): m(m), m_args1(m), m_args2(m), m_subst(m) { updt_params(p); } +expr_ref hoist_rewriter::mk_and(expr_ref_vector const& args) { + if (m_rewriter) + return m_rewriter->mk_and(args); + else + return ::mk_and(args); +} + +expr_ref hoist_rewriter::mk_or(expr_ref_vector const& args) { + if (m_rewriter) + return m_rewriter->mk_or(args); + else + return ::mk_or(args); +} + br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) { if (num_args < 2) return BR_FAILED; @@ -152,13 +166,13 @@ expr_ref hoist_rewriter::hoist_predicates(obj_hashtable const& preds, unsi for (expr* e : m_args1) if (!preds.contains(e)) fmls.push_back(e); - args.push_back(::mk_and(fmls)); + args.push_back(mk_and(fmls)); } fmls.reset(); - fmls.push_back(::mk_or(args)); + fmls.push_back(mk_or(args)); for (auto* p : preds) fmls.push_back(p); - result = ::mk_and(fmls); + result = mk_and(fmls); return result; } diff --git a/src/ast/rewriter/hoist_rewriter.h b/src/ast/rewriter/hoist_rewriter.h index cc83bfa562..72d44d0bce 100644 --- a/src/ast/rewriter/hoist_rewriter.h +++ b/src/ast/rewriter/hoist_rewriter.h @@ -25,8 +25,11 @@ Module Name: #include "util/union_find.h" #include "util/obj_hashtable.h" +class bool_rewriter; + class hoist_rewriter { ast_manager & m; + bool_rewriter* m_rewriter = nullptr; expr_ref_vector m_args1, m_args2; obj_hashtable m_preds1, m_preds2; basic_union_find m_uf1, m_uf2, m_uf0; @@ -39,6 +42,8 @@ class hoist_rewriter { expr_mark m_mark; bool is_and(expr* e, expr_ref_vector* args); + expr_ref mk_and(expr_ref_vector const& args); + expr_ref mk_or(expr_ref_vector const& args); bool is_var(expr* e) { return m_expr2var.contains(e); } expr* mk_expr(unsigned v) { return m_var2expr[v]; } @@ -48,6 +53,7 @@ class hoist_rewriter { expr_ref hoist_predicates(obj_hashtable const& p, unsigned num_args, expr* const* args); + public: hoist_rewriter(ast_manager & m, params_ref const & p = params_ref()); family_id get_fid() const { return m.get_basic_family_id(); } @@ -56,6 +62,7 @@ class hoist_rewriter { static void get_param_descrs(param_descrs & r) {} br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result); + void set(bool_rewriter& r) { m_rewriter = &r; } }; struct hoist_rewriter_cfg : public default_rewriter_cfg { diff --git a/src/ast/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp index 6c1eccea00..05f347f25e 100644 --- a/src/ast/simplifiers/eliminate_predicates.cpp +++ b/src/ast/simplifiers/eliminate_predicates.cpp @@ -1008,8 +1008,6 @@ void eliminate_predicates::reset() { void eliminate_predicates::reduce() { - if (!m_fmls.has_quantifiers()) - return; reset(); init_clauses(); find_definitions(); diff --git a/src/tactic/core/tseitin_cnf_tactic.cpp b/src/tactic/core/tseitin_cnf_tactic.cpp index bd2f58b442..ec03849bc7 100644 --- a/src/tactic/core/tseitin_cnf_tactic.cpp +++ b/src/tactic/core/tseitin_cnf_tactic.cpp @@ -141,6 +141,7 @@ class tseitin_cnf_tactic : public tactic { sign = !sign; goto start; case OP_OR: + case OP_AND: l = nullptr; m_cache.find(to_app(n), l); SASSERT(l != 0); @@ -187,6 +188,7 @@ class tseitin_cnf_tactic : public tactic { goto start; } case OP_OR: + case OP_AND: visited = false; push_frame(to_app(n)); return; @@ -197,7 +199,6 @@ class tseitin_cnf_tactic : public tactic { push_frame(to_app(n)); } return; - case OP_AND: case OP_XOR: case OP_IMPLIES: case OP_DISTINCT: @@ -617,6 +618,43 @@ class tseitin_cnf_tactic : public tactic { } return DONE; } + + mres match_and(app * t, bool first, bool root) { + if (!m.is_and(t)) + return NO; + if (first) { + bool visited = true; + for (expr* a : *t) + visit(a, visited); + if (!visited) + return CONT; + } + expr_ref_buffer lits(m); + expr_ref l(m), nl(m); + app_ref k(m), nk(m); + if (root) { + for (expr* arg : *t) { + get_lit(arg, false, l); + expr* lits[1] = { l }; + mk_clause(1, lits); + } + } + else { + k = mk_fresh(); + nk = m.mk_not(k); + cache_result(t, k); + + for (expr* arg : *t) { + get_lit(arg, false, l); + mk_clause(nk, l); + inv(l, nl); + lits.push_back(nl); + } + lits.push_back(k); + mk_clause(lits.size(), lits.data()); + } + return DONE; + } mres match_or(app * t, bool first, bool root) { if (!m.is_or(t)) @@ -778,6 +816,7 @@ class tseitin_cnf_tactic : public tactic { fr.m_first = false; TRY(match_or_3and); TRY(match_or); + TRY(match_and); TRY(match_iff3); // TRY(match_iff_or); TRY(match_iff);