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

make context_solve configurable and exposed as top-level tactic parameter

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-23 16:06:25 -08:00
parent 412eee0dac
commit 8e5c1fcfd1
4 changed files with 27 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/CMakeLists.txt
View file

@ -22,4 +22,6 @@ z3_add_component(tactic
probe.h probe.h
sine_filter.h sine_filter.h
tactic.h tactic.h
PYG_FILES
tactic_params.pyg
) )

13
src/tactic/core/blast_term_ite_tactic.cpp
View file

@ -16,11 +16,12 @@ Author:
Notes: Notes:
--*/ --*/
#include "tactic/tactical.h" #include "util/cooperate.h"
#include "ast/normal_forms/defined_names.h" #include "ast/normal_forms/defined_names.h"
#include "ast/rewriter/rewriter_def.h" #include "ast/rewriter/rewriter_def.h"
#include "util/cooperate.h"
#include "ast/scoped_proof.h" #include "ast/scoped_proof.h"
#include "tactic/tactical.h"
#include "tactic/tactic_params.hpp"
@ -50,9 +51,10 @@ class blast_term_ite_tactic : public tactic {
} }
void updt_params(params_ref const & p) { void updt_params(params_ref const & p) {
tactic_params tp(p);
m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
m_max_steps = p.get_uint("max_steps", UINT_MAX); m_max_steps = p.get_uint("max_steps", tp.blast_term_ite_max_steps());
m_max_inflation = p.get_uint("max_inflation", UINT_MAX); // multiplicative factor of initial term size. m_max_inflation = p.get_uint("max_inflation", tp.blast_term_ite_max_inflation()); // multiplicative factor of initial term size.
} }
@ -182,8 +184,7 @@ public:
void collect_param_descrs(param_descrs & r) override { void collect_param_descrs(param_descrs & r) override {
insert_max_memory(r); insert_max_memory(r);
insert_max_steps(r); insert_max_steps(r);
r.insert("max_args", CPK_UINT, r.insert("max_inflation", CPK_UINT, "(default: infinity) multiplicative factor of initial term size.");
"(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.");
} }
void operator()(goal_ref const & in, goal_ref_buffer & result) override { void operator()(goal_ref const & in, goal_ref_buffer & result) override {

6
src/tactic/core/propagate_values_tactic.cpp
View file

@ -23,6 +23,7 @@ Revision History:
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
#include "ast/expr_substitution.h" #include "ast/expr_substitution.h"
#include "tactic/goal_shared_occs.h" #include "tactic/goal_shared_occs.h"
#include "tactic/tactic_params.hpp"
namespace { namespace {
class propagate_values_tactic : public tactic { class propagate_values_tactic : public tactic {
@ -37,7 +38,8 @@ class propagate_values_tactic : public tactic {
params_ref m_params; params_ref m_params;
void updt_params_core(params_ref const & p) { void updt_params_core(params_ref const & p) {
m_max_rounds = p.get_uint("max_rounds", 4); tactic_params tp(p);
m_max_rounds = p.get_uint("max_rounds", tp.propagate_values_max_rounds());
} }
bool is_shared(expr * t) { bool is_shared(expr * t) {
@ -215,7 +217,7 @@ public:
void collect_param_descrs(param_descrs & r) override { void collect_param_descrs(param_descrs & r) override {
th_rewriter::get_param_descrs(r); th_rewriter::get_param_descrs(r);
r.insert("max_rounds", CPK_UINT, "(default: 2) maximum number of rounds."); r.insert("max_rounds", CPK_UINT, "(default: 4) maximum number of rounds.");
} }
void operator()(goal_ref const & in, goal_ref_buffer & result) override { void operator()(goal_ref const & in, goal_ref_buffer & result) override {

29
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -25,6 +25,7 @@ Revision History:
#include "tactic/goal_shared_occs.h" #include "tactic/goal_shared_occs.h"
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "tactic/tactic_params.hpp"
class solve_eqs_tactic : public tactic { class solve_eqs_tactic : public tactic {
struct imp { struct imp {
@ -40,6 +41,7 @@ class solve_eqs_tactic : public tactic {
bool m_theory_solver; bool m_theory_solver;
bool m_ite_solver; bool m_ite_solver;
unsigned m_max_occs; unsigned m_max_occs;
bool m_context_solve;
scoped_ptr<expr_substitution> m_subst; scoped_ptr<expr_substitution> m_subst;
scoped_ptr<expr_substitution> m_norm_subst; scoped_ptr<expr_substitution> m_norm_subst;
expr_sparse_mark m_candidate_vars; expr_sparse_mark m_candidate_vars;
@ -72,9 +74,11 @@ class solve_eqs_tactic : public tactic {
ast_manager & m() const { return m_manager; } ast_manager & m() const { return m_manager; }
void updt_params(params_ref const & p) { void updt_params(params_ref const & p) {
m_ite_solver = p.get_bool("ite_solver", true); tactic_params tp(p);
m_theory_solver = p.get_bool("theory_solver", true); m_ite_solver = p.get_bool("ite_solver", tp.solve_eqs_ite_solver());
m_max_occs = p.get_uint("solve_eqs_max_occs", UINT_MAX); 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());
} }
void checkpoint() { void checkpoint() {
@ -555,7 +559,7 @@ class solve_eqs_tactic : public tactic {
insert_solution(g, idx, arg, var, def, pr); insert_solution(g, idx, arg, var, def, pr);
} }
else { else {
IF_VERBOSE(0, IF_VERBOSE(10000,
verbose_stream() << "eq not solved " << mk_pp(arg, m()) << "\n"; verbose_stream() << "eq not solved " << mk_pp(arg, m()) << "\n";
verbose_stream() << is_uninterp_const(lhs) << " " << !m_candidate_vars.is_marked(lhs) << " " verbose_stream() << is_uninterp_const(lhs) << " " << !m_candidate_vars.is_marked(lhs) << " "
<< !occurs(lhs, rhs) << " " << check_occs(lhs) << "\n";); << !occurs(lhs, rhs) << " " << check_occs(lhs) << "\n";);
@ -726,7 +730,7 @@ class solve_eqs_tactic : public tactic {
++idx; ++idx;
} }
IF_VERBOSE(10, IF_VERBOSE(10000,
verbose_stream() << "ordered vars: "; verbose_stream() << "ordered vars: ";
for (app* v : m_ordered_vars) verbose_stream() << mk_pp(v, m()) << " "; for (app* v : m_ordered_vars) verbose_stream() << mk_pp(v, m()) << " ";
verbose_stream() << "\n";); verbose_stream() << "\n";);
@ -811,12 +815,6 @@ class solve_eqs_tactic : public tactic {
} }
m_r->operator()(f, new_f, new_pr, new_dep); m_r->operator()(f, new_f, new_pr, new_dep);
#if 0
pb_util pb(m());
if (pb.is_ge(f) && f != new_f) {
IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n");
}
#endif
TRACE("solve_eqs_subst", tout << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n";); TRACE("solve_eqs_subst", tout << mk_ismt2_pp(f, m()) << "\n--->\n" << mk_ismt2_pp(new_f, m()) << "\n";);
m_num_steps += m_r->get_num_steps() + 1; m_num_steps += m_r->get_num_steps() + 1;
@ -922,8 +920,9 @@ class solve_eqs_tactic : public tactic {
while (true) { while (true) {
collect_num_occs(*g); collect_num_occs(*g);
collect(*g); collect(*g);
// TBD Disabled until tested more: if (m_context_solve) {
// collect_hoist(*g); collect_hoist(*g);
}
if (m_subst->empty()) if (m_subst->empty())
break; break;
sort_vars(); sort_vars();
@ -941,7 +940,6 @@ class solve_eqs_tactic : public tactic {
g->inc_depth(); g->inc_depth();
g->add(mc.get()); g->add(mc.get());
result.push_back(g.get()); result.push_back(g.get());
//IF_VERBOSE(0, g->display(verbose_stream()));
TRACE("solve_eqs", g->display(tout);); TRACE("solve_eqs", g->display(tout););
SASSERT(g->is_well_sorted()); SASSERT(g->is_well_sorted());
} }
@ -968,10 +966,11 @@ public:
m_imp->updt_params(p); m_imp->updt_params(p);
} }
void collect_param_descrs(param_descrs & r) override { void collect_param_descrs(param_descrs & r) override {
r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations."); r.insert("solve_eqs_max_occs", CPK_UINT, "(default: infty) maximum number of occurrences for considering a variable for gaussian eliminations.");
r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers."); r.insert("theory_solver", CPK_BOOL, "(default: true) use theory solvers.");
r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver."); r.insert("ite_solver", CPK_BOOL, "(default: true) use if-then-else solver.");
r.insert("context_solve", CPK_BOOL, "(default: false) solve equalities under disjunctions.");
} }
void operator()(goal_ref const & in, void operator()(goal_ref const & in,