From 8e5c1fcfd150e6b51040f1802f86e831e674f134 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 23 Jan 2019 16:06:25 -0800
Subject: [PATCH] make context_solve configurable and exposed as top-level
tactic parameter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/tactic/CMakeLists.txt | 2 ++
src/tactic/core/blast_term_ite_tactic.cpp | 13 ++++-----
src/tactic/core/propagate_values_tactic.cpp | 6 +++--
src/tactic/core/solve_eqs_tactic.cpp | 29 ++++++++++-----------
4 files changed, 27 insertions(+), 23 deletions(-)
diff --git a/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt
index c9554b76a..495078afc 100644
--- a/src/tactic/CMakeLists.txt
+++ b/src/tactic/CMakeLists.txt
@@ -22,4 +22,6 @@ z3_add_component(tactic
probe.h
sine_filter.h
tactic.h
+ PYG_FILES
+ tactic_params.pyg
)
diff --git a/src/tactic/core/blast_term_ite_tactic.cpp b/src/tactic/core/blast_term_ite_tactic.cpp
index eefb9418e..259b479c5 100644
--- a/src/tactic/core/blast_term_ite_tactic.cpp
+++ b/src/tactic/core/blast_term_ite_tactic.cpp
@@ -16,11 +16,12 @@ Author:
Notes:
--*/
-#include "tactic/tactical.h"
+#include "util/cooperate.h"
#include "ast/normal_forms/defined_names.h"
#include "ast/rewriter/rewriter_def.h"
-#include "util/cooperate.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) {
+ tactic_params tp(p);
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_inflation = p.get_uint("max_inflation", UINT_MAX); // multiplicative factor of initial term size.
+ m_max_steps = p.get_uint("max_steps", tp.blast_term_ite_max_steps());
+ 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 {
insert_max_memory(r);
insert_max_steps(r);
- r.insert("max_args", CPK_UINT,
- "(default: 128) maximum number of arguments (per application) that will be considered by the greedy (quadratic) heuristic.");
+ r.insert("max_inflation", CPK_UINT, "(default: infinity) multiplicative factor of initial term size.");
}
void operator()(goal_ref const & in, goal_ref_buffer & result) override {
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index f9712120f..351b606e6 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -23,6 +23,7 @@ Revision History:
#include "ast/ast_smt2_pp.h"
#include "ast/expr_substitution.h"
#include "tactic/goal_shared_occs.h"
+#include "tactic/tactic_params.hpp"
namespace {
class propagate_values_tactic : public tactic {
@@ -37,7 +38,8 @@ class propagate_values_tactic : public tactic {
params_ref m_params;
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) {
@@ -215,7 +217,7 @@ public:
void collect_param_descrs(param_descrs & r) override {
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 {
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index 1ed230886..623f83db4 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -25,6 +25,7 @@ Revision History:
#include "tactic/goal_shared_occs.h"
#include "tactic/tactical.h"
#include "tactic/generic_model_converter.h"
+#include "tactic/tactic_params.hpp"
class solve_eqs_tactic : public tactic {
struct imp {
@@ -40,6 +41,7 @@ class solve_eqs_tactic : public tactic {
bool m_theory_solver;
bool m_ite_solver;
unsigned m_max_occs;
+ bool m_context_solve;
scoped_ptr<expr_substitution> m_subst;
scoped_ptr<expr_substitution> m_norm_subst;
expr_sparse_mark m_candidate_vars;
@@ -72,9 +74,11 @@ class solve_eqs_tactic : public tactic {
ast_manager & m() const { return m_manager; }
void updt_params(params_ref const & p) {
- m_ite_solver = p.get_bool("ite_solver", true);
- m_theory_solver = p.get_bool("theory_solver", true);
- m_max_occs = p.get_uint("solve_eqs_max_occs", UINT_MAX);
+ tactic_params tp(p);
+ 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());
}
void checkpoint() {
@@ -555,7 +559,7 @@ class solve_eqs_tactic : public tactic {
insert_solution(g, idx, arg, var, def, pr);
}
else {
- IF_VERBOSE(0,
+ IF_VERBOSE(10000,
verbose_stream() << "eq not solved " << mk_pp(arg, m()) << "\n";
verbose_stream() << is_uninterp_const(lhs) << " " << !m_candidate_vars.is_marked(lhs) << " "
<< !occurs(lhs, rhs) << " " << check_occs(lhs) << "\n";);
@@ -726,7 +730,7 @@ class solve_eqs_tactic : public tactic {
++idx;
}
- IF_VERBOSE(10,
+ IF_VERBOSE(10000,
verbose_stream() << "ordered vars: ";
for (app* v : m_ordered_vars) verbose_stream() << mk_pp(v, m()) << " ";
verbose_stream() << "\n";);
@@ -811,12 +815,6 @@ class solve_eqs_tactic : public tactic {
}
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";);
m_num_steps += m_r->get_num_steps() + 1;
@@ -922,8 +920,9 @@ class solve_eqs_tactic : public tactic {
while (true) {
collect_num_occs(*g);
collect(*g);
- // TBD Disabled until tested more:
- // collect_hoist(*g);
+ if (m_context_solve) {
+ collect_hoist(*g);
+ }
if (m_subst->empty())
break;
sort_vars();
@@ -941,7 +940,6 @@ class solve_eqs_tactic : public tactic {
g->inc_depth();
g->add(mc.get());
result.push_back(g.get());
- //IF_VERBOSE(0, g->display(verbose_stream()));
TRACE("solve_eqs", g->display(tout););
SASSERT(g->is_well_sorted());
}
@@ -968,10 +966,11 @@ public:
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("theory_solver", CPK_BOOL, "(default: true) use theory solvers.");
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,