mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
move tactic_params to params
This commit is contained in:
Nikolaj Bjorner
parent
203652da74
commit
06eb460c75
12 changed files with 40 additions and 21 deletions
|
|
@ -21,12 +21,14 @@ Author:
|
|||
#include "ast/ast_pp.h"
|
||||
#include "ast/arith_decl_plugin.h"
|
||||
#include "ast/simplifiers/extract_eqs.h"
|
||||
#include "params/tactic_params.hpp"
|
||||
|
||||
|
||||
namespace euf {
|
||||
|
||||
class basic_extract_eq : public extract_eq {
|
||||
ast_manager& m;
|
||||
bool m_ite_solver = true;
|
||||
|
||||
public:
|
||||
basic_extract_eq(ast_manager& m) : m(m) {}
|
||||
|
|
@ -41,7 +43,7 @@ namespace euf {
|
|||
eqs.push_back(dependent_eq(to_app(y), expr_ref(x, m), d));
|
||||
}
|
||||
expr* c, * th, * el, * x1, * y1, * x2, * y2;
|
||||
if (m.is_ite(f, c, th, el)) {
|
||||
if (m_ite_solver && m.is_ite(f, c, th, el)) {
|
||||
if (m.is_eq(th, x1, y1) && m.is_eq(el, x2, y2)) {
|
||||
if (x1 == y2 && is_uninterp_const(x1))
|
||||
std::swap(x2, y2);
|
||||
|
|
@ -58,6 +60,11 @@ namespace euf {
|
|||
if (m.is_not(f, x) && is_uninterp_const(x))
|
||||
eqs.push_back(dependent_eq(to_app(x), expr_ref(m.mk_false(), m), d));
|
||||
}
|
||||
|
||||
void updt_params(params_ref const& p) {
|
||||
tactic_params tp(p);
|
||||
m_ite_solver = p.get_bool("ite_solver", tp.solve_eqs_ite_solver());
|
||||
}
|
||||
};
|
||||
|
||||
class arith_extract_eq : public extract_eq {
|
||||
|
|
@ -65,6 +72,7 @@ namespace euf {
|
|||
arith_util a;
|
||||
expr_ref_vector m_args;
|
||||
expr_sparse_mark m_nonzero;
|
||||
bool m_enabled = true;
|
||||
|
||||
|
||||
// solve u mod r1 = y -> u = r1*mod!1 + y
|
||||
|
|
@ -215,6 +223,8 @@ namespace euf {
|
|||
public:
|
||||
arith_extract_eq(ast_manager& m) : m(m), a(m), m_args(m) {}
|
||||
void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) override {
|
||||
if (!m_enabled)
|
||||
return;
|
||||
auto [f, d] = e();
|
||||
expr* x, * y;
|
||||
if (m.is_eq(f, x, y) && a.is_int_real(x)) {
|
||||
|
|
@ -224,12 +234,20 @@ namespace euf {
|
|||
}
|
||||
|
||||
void pre_process(dependent_expr_state& fmls) override {
|
||||
if (!m_enabled)
|
||||
return;
|
||||
m_nonzero.reset();
|
||||
for (unsigned i = 0; i < fmls.size(); ++i) {
|
||||
auto [f, d] = fmls[i]();
|
||||
add_pos(f);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void updt_params(params_ref const& p) {
|
||||
tactic_params tp(p);
|
||||
m_enabled = p.get_bool("theory_solver", tp.solve_eqs_ite_solver());
|
||||
}
|
||||
};
|
||||
|
||||
void register_extract_eqs(ast_manager& m, scoped_ptr_vector<extract_eq>& ex) {
|
||||
|
|
|
|||
|
|
@ -40,6 +40,7 @@ namespace euf {
|
|||
virtual ~extract_eq() {}
|
||||
virtual void get_eqs(dependent_expr const& e, dep_eq_vector& eqs) = 0;
|
||||
virtual void pre_process(dependent_expr_state& fmls) {}
|
||||
virtual void updt_params(params_ref const& p) {}
|
||||
};
|
||||
|
||||
void register_extract_eqs(ast_manager& m, scoped_ptr_vector<extract_eq>& ex);
|
||||
|
|
|
|||
|
|
@ -24,6 +24,7 @@ Author:
|
|||
#include "ast/rewriter/expr_replacer.h"
|
||||
#include "ast/simplifiers/solve_eqs.h"
|
||||
#include "ast/converters/generic_model_converter.h"
|
||||
#include "params/tactic_params.hpp"
|
||||
|
||||
|
||||
namespace euf {
|
||||
|
|
@ -46,7 +47,8 @@ namespace euf {
|
|||
m_next.resize(m_id2var.size());
|
||||
|
||||
for (auto const& eq : eqs)
|
||||
m_next[var2id(eq.var)].push_back(eq);
|
||||
if (can_be_var(eq.var))
|
||||
m_next[var2id(eq.var)].push_back(eq);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -136,10 +138,7 @@ namespace euf {
|
|||
tout << "after normalizing variables\n";
|
||||
for (unsigned id : m_subst_ids) {
|
||||
auto const& eq = m_next[id][0];
|
||||
expr* def = nullptr;
|
||||
proof* pr = nullptr;
|
||||
expr_dependency* dep = nullptr;
|
||||
m_subst->find(eq.var, def, pr, dep);
|
||||
expr* def = m_subst->find(eq.var);
|
||||
tout << mk_pp(eq.var, m) << "\n----->\n" << mk_pp(def, m) << "\n\n";
|
||||
});
|
||||
}
|
||||
|
|
@ -201,14 +200,11 @@ namespace euf {
|
|||
}
|
||||
|
||||
void solve_eqs::updt_params(params_ref const& p) {
|
||||
// TODO
|
||||
#if 0
|
||||
tactic_params tp(m_params);
|
||||
m_ite_solver = p.get_bool("ite_solver", tp.solve_eqs_ite_solver());
|
||||
m_theory_solver = p.get_bool("theory_solver", tp.solve_eqs_theory_solver());
|
||||
m_max_occs = p.get_uint("solve_eqs_max_occs", tp.solve_eqs_max_occs());
|
||||
m_context_solve = p.get_bool("context_solve", tp.solve_eqs_context_solve());
|
||||
#endif
|
||||
tactic_params tp(p);
|
||||
m_config.m_max_occs = p.get_uint("solve_eqs_max_occs", tp.solve_eqs_max_occs());
|
||||
m_config.m_context_solve = p.get_bool("context_solve", tp.solve_eqs_context_solve());
|
||||
for (auto* ex : m_extract_plugins)
|
||||
ex->updt_params(p);
|
||||
}
|
||||
|
||||
void solve_eqs::collect_statistics(statistics& st) const {
|
||||
|
|
|
|||
|
|
@ -30,6 +30,10 @@ namespace euf {
|
|||
unsigned m_num_steps = 0;
|
||||
unsigned m_num_elim_vars = 0;
|
||||
};
|
||||
struct config {
|
||||
bool m_context_solve = true;
|
||||
unsigned m_max_occs = UINT_MAX;
|
||||
};
|
||||
|
||||
th_rewriter m_rewriter;
|
||||
scoped_ptr_vector<extract_eq> m_extract_plugins;
|
||||
|
|
@ -40,6 +44,7 @@ namespace euf {
|
|||
|
||||
expr_mark m_unsafe_vars; // expressions that cannot be replaced
|
||||
stats m_stats;
|
||||
config m_config;
|
||||
|
||||
void add_subst(dependent_eq const& eq);
|
||||
|
||||
|
|
|
|||
|
|
@ -16,6 +16,7 @@ z3_add_component(params
|
|||
rewriter_params.pyg
|
||||
seq_rewriter_params.pyg
|
||||
solver_params.pyg
|
||||
tactic_params.pyg
|
||||
EXTRA_REGISTER_MODULE_HEADERS
|
||||
context_params.h
|
||||
)
|
||||
|
|
|
|||
|
|
@ -19,6 +19,4 @@ z3_add_component(tactic
|
|||
TACTIC_HEADERS
|
||||
probe.h
|
||||
tactic.h
|
||||
PYG_FILES
|
||||
tactic_params.pyg
|
||||
)
|
||||
|
|
|
|||
|
|
@ -20,7 +20,7 @@ Notes:
|
|||
#include "ast/rewriter/rewriter_def.h"
|
||||
#include "ast/scoped_proof.h"
|
||||
#include "tactic/tactical.h"
|
||||
#include "tactic/tactic_params.hpp"
|
||||
#include "params/tactic_params.hpp"
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ Revision History:
|
|||
#include "ast/ast_pp.h"
|
||||
#include "ast/expr_substitution.h"
|
||||
#include "tactic/goal_shared_occs.h"
|
||||
#include "tactic/tactic_params.hpp"
|
||||
#include "params/tactic_params.hpp"
|
||||
|
||||
namespace {
|
||||
class propagate_values_tactic : public tactic {
|
||||
|
|
|
|||
|
|
@ -28,7 +28,7 @@ Revision History:
|
|||
#include "tactic/goal_shared_occs.h"
|
||||
#include "tactic/tactical.h"
|
||||
#include "ast/converters/generic_model_converter.h"
|
||||
#include "tactic/tactic_params.hpp"
|
||||
#include "params/tactic_params.hpp"
|
||||
|
||||
class solve_eqs_tactic : public tactic {
|
||||
struct imp {
|
||||
|
|
|
|||
|
|
@ -83,7 +83,7 @@ public:
|
|||
m_simp->reduce();
|
||||
m_goal->inc_depth();
|
||||
if (in->models_enabled())
|
||||
in->set(m_simp->get_model_converter());
|
||||
in->set(m_simp->get_model_converter().get());
|
||||
result.push_back(in.get());
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -44,7 +44,7 @@ Notes:
|
|||
#include "solver/solver2tactic.h"
|
||||
#include "solver/parallel_tactic.h"
|
||||
#include "solver/parallel_params.hpp"
|
||||
#include "tactic/tactic_params.hpp"
|
||||
#include "params/tactic_params.hpp"
|
||||
#include "parsers/smt2/smt2parser.h"
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue