mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

add (disabled) code path to enable nested conjunctions

Browse source 
for experiments with disabling flat-and-or dependency
This commit is contained in:
Nikolaj Bjorner 2023-03-01 20:39:39 -08:00
parent 46d37b6e30
commit acd2eaa390
2 changed files with 31 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -23,7 +23,7 @@ Author:
#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) {
m(m), m_args1(m), m_args2(m), m_refs(m), m_subst(m) {
updt_params(p);
}
@ -185,7 +185,7 @@ expr_ref hoist_rewriter::hoist_predicates(obj_hashtable<expr> const& preds, unsi
br_status hoist_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
switch (f->get_decl_kind()) {
case OP_OR:
case OP_OR:
return mk_or(num_args, args, result);
default:
return BR_FAILED;
@ -193,6 +193,33 @@ br_status hoist_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
}
bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) {
#if 0
if (!args)
return m.is_and(e) || (m.is_not(e, e) && m.is_or(e));
expr_fast_mark1 visited;
args->reset();
args->push_back(e);
m_refs.reset();
for (unsigned i = 0; i < args->size(); ++i) {
e = args->get(i);
if (visited.is_marked(e))
goto drop;
m_refs.push_back(e);
visited.mark(e, true);
if (m.is_and(e))
args->append(to_app(e)->get_num_args(), to_app(e)->get_args());
else if (m.is_not(e, e) && m.is_or(e))
for (expr* arg : *to_app(e))
args->push_back(::mk_not(m, arg));
else
continue;
drop:
(*args)[i] = args->back();
args->pop_back();
--i;
}
return args->size() > 1;
#else
if (m.is_and(e)) {
if (args) {
args->reset();
@ -209,6 +236,7 @@ bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) {
}
return true;
}
#endif
return false;
}

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

@ -29,7 +29,7 @@ class bool_rewriter;
class hoist_rewriter {
ast_manager & m;
expr_ref_vector m_args1, m_args2;
expr_ref_vector m_args1, m_args2, m_refs;
obj_hashtable<expr> m_preds1, m_preds2;
basic_union_find m_uf1, m_uf2, m_uf0;
ptr_vector<expr> m_es;