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

fixes related to #6577

Browse source 
- enforce elim-and in bool-rewriter when invoking hoisting.
- make cnf tactic more resilient to non-normalized input.
- enable eliminate predicates on ground formulas
This commit is contained in:
Nikolaj Bjorner 2023-02-12 13:43:44 -08:00
parent ede9e5ffc2
commit cac5052685
5 changed files with 69 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/ast/rewriter/bool_rewriter.h
View file

@ -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); }

22
src/ast/rewriter/hoist_rewriter.cpp
View file

@ -17,16 +17,30 @@ Author:
#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<expr> 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;
}

7
src/ast/rewriter/hoist_rewriter.h
View file

@ -25,8 +25,11 @@ Notes:
#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<expr> 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<expr> 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 @@ public:
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 {

2
src/ast/simplifiers/eliminate_predicates.cpp
View file

@ -1008,8 +1008,6 @@ void eliminate_predicates::reset() {
void eliminate_predicates::reduce() {
if (!m_fmls.has_quantifiers())
return;
reset();
init_clauses();
find_definitions();

41
src/tactic/core/tseitin_cnf_tactic.cpp
View file

@ -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);