mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

remove simplifier dependencies from ufbv tactics

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-23 12:30:33 -07:00
parent 655b3d9c19
commit f062e17037
5 changed files with 13 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/tactic/ufbv/macro_finder_tactic.cpp
View file

@ -17,10 +17,6 @@ Notes:
--*/
#include "tactic/tactical.h"
#include "ast/simplifier/simplifier.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/simplifier/arith_simplifier_plugin.h"
#include "ast/simplifier/bv_simplifier_plugin.h"
#include "ast/macros/macro_manager.h"
#include "ast/macros/macro_finder.h"
#include "tactic/extension_model_converter.h"
@ -52,18 +48,6 @@ class macro_finder_tactic : public tactic {
fail_if_unsat_core_generation("macro-finder", g);
bool produce_proofs = g->proofs_enabled();
simplifier simp(m_manager);
basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
bsimp->set_eliminate_and(m_elim_and);
simp.register_plugin(bsimp);
arith_simplifier_params a_params;
arith_simplifier_plugin * asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, a_params);
simp.register_plugin(asimp);
bv_simplifier_params bv_params;
bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params);
simp.register_plugin(bvsimp);
macro_manager mm(m_manager);
macro_finder mf(m_manager, mm);

17
src/tactic/ufbv/quasi_macros_tactic.cpp
View file

@ -17,10 +17,6 @@ Notes:
--*/
#include "tactic/tactical.h"
#include "ast/simplifier/simplifier.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "ast/simplifier/arith_simplifier_plugin.h"
#include "ast/simplifier/bv_simplifier_plugin.h"
#include "ast/macros/macro_manager.h"
#include "ast/macros/macro_finder.h"
#include "tactic/extension_model_converter.h"
@ -50,18 +46,7 @@ class quasi_macros_tactic : public tactic {
fail_if_unsat_core_generation("quasi-macros", g);
bool produce_proofs = g->proofs_enabled();
simplifier simp(m_manager);
basic_simplifier_plugin * bsimp = alloc(basic_simplifier_plugin, m_manager);
bsimp->set_eliminate_and(true);
simp.register_plugin(bsimp);
arith_simplifier_params a_params;
arith_simplifier_plugin * asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, a_params);
simp.register_plugin(asimp);
bv_simplifier_params bv_params;
bv_simplifier_plugin * bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, bv_params);
simp.register_plugin(bvsimp);
macro_manager mm(m_manager);
quasi_macros qm(m_manager, mm);
bool more = true;

13
src/tactic/ufbv/ufbv_rewriter.cpp
View file

@ -20,20 +20,23 @@ Revision History:
--*/
#include "util/uint_set.h"
#include "ast/ast_pp.h"
#include "tactic/ufbv/ufbv_rewriter.h"
#include "ast/for_each_expr.h"
#include "ast/rewriter/var_subst.h"
#include "util/uint_set.h"
#include "tactic/ufbv/ufbv_rewriter.h"
ufbv_rewriter::ufbv_rewriter(ast_manager & m, basic_simplifier_plugin & p):
ufbv_rewriter::ufbv_rewriter(ast_manager & m):
m_manager(m),
m_match_subst(m),
m_bsimp(p),
m_bsimp(m),
m_todo(m),
m_rewrite_todo(m),
m_rewrite_cache(m),
m_new_exprs(m) {
params_ref p;
p.set_bool("elim_and", true);
m_bsimp.updt_params(p);
}
ufbv_rewriter::~ufbv_rewriter() {
@ -396,7 +399,7 @@ expr * ufbv_rewriter::rewrite(expr * n) {
if (f->get_family_id() != m_manager.get_basic_family_id())
na = m_manager.mk_app(f, m_new_args.size(), m_new_args.c_ptr());
else
m_bsimp.reduce(f, m_new_args.size(), m_new_args.c_ptr(), na);
m_bsimp.mk_app(f, m_new_args.size(), m_new_args.c_ptr(), na);
TRACE("demodulator_bug", tout << "e:\n" << mk_pp(e, m_manager) << "\nnew_args: \n";
for (unsigned i = 0; i < m_new_args.size(); i++) { tout << mk_pp(m_new_args[i], m_manager) << "\n"; }
tout << "=====>\n";

6
src/tactic/ufbv/ufbv_rewriter.h
View file

@ -23,10 +23,10 @@ Revision History:
#include "ast/ast.h"
#include "ast/substitution/substitution.h"
#include "ast/rewriter/bool_rewriter.h"
#include "util/obj_hashtable.h"
#include "util/obj_pair_hashtable.h"
#include "util/array_map.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
/**
\brief Apply demodulators as a preprocessing technique.
@ -159,7 +159,7 @@ class ufbv_rewriter {
ast_manager & m_manager;
match_subst m_match_subst;
basic_simplifier_plugin & m_bsimp;
bool_rewriter m_bsimp;
fwd_idx_map m_fwd_idx;
back_idx_map m_back_idx;
demodulator2lhs_rhs m_demodulator2lhs_rhs;
@ -194,7 +194,7 @@ protected:
virtual int is_subset(expr * e1, expr * e2) const;
public:
ufbv_rewriter(ast_manager & m, basic_simplifier_plugin & p);
ufbv_rewriter(ast_manager & m);
virtual ~ufbv_rewriter();
void operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);

6
src/tactic/ufbv/ufbv_rewriter_tactic.cpp
View file

@ -17,8 +17,6 @@ Notes:
--*/
#include "tactic/tactical.h"
#include "ast/simplifier/simplifier.h"
#include "ast/simplifier/basic_simplifier_plugin.h"
#include "tactic/ufbv/ufbv_rewriter.h"
#include "tactic/ufbv/ufbv_rewriter_tactic.h"
@ -45,9 +43,7 @@ class ufbv_rewriter_tactic : public tactic {
bool produce_proofs = g->proofs_enabled();
basic_simplifier_plugin bsimp(m_manager);
bsimp.set_eliminate_and(true);
ufbv_rewriter dem(m_manager, bsimp);
ufbv_rewriter dem(m_manager);
expr_ref_vector forms(m_manager), new_forms(m_manager);
proof_ref_vector proofs(m_manager), new_proofs(m_manager);