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

add lrb/chb and experiment with them

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-05-28 10:48:31 -07:00
parent 77b2a015a2 f3a0b7e0cd
commit e0a86ccc1a
28 changed files with 459 additions and 281 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
contrib/cmake/src/ast/rewriter/CMakeLists.txt
View file

@ -8,6 +8,7 @@ z3_add_component(rewriter
bv_rewriter.cpp
datatype_rewriter.cpp
der.cpp
distribute_forall.cpp
dl_rewriter.cpp
enum2bv_rewriter.cpp
expr_replacer.cpp

1
contrib/cmake/src/ast/simplifier/CMakeLists.txt
View file

@ -10,7 +10,6 @@ z3_add_component(simplifier
bv_simplifier_params.cpp
bv_simplifier_plugin.cpp
datatype_simplifier_plugin.cpp
distribute_forall.cpp
elim_bounds.cpp
fpa_simplifier_plugin.cpp
inj_axiom.cpp

13
src/ast/simplifier/distribute_forall.cpp → src/ast/rewriter/distribute_forall.cpp
View file

@ -20,12 +20,12 @@ Revision History:
--*/
#include"var_subst.h"
#include"ast_ll_pp.h"
#include"ast_util.h"
#include"distribute_forall.h"
#include"bool_rewriter.h"
distribute_forall::distribute_forall(ast_manager & m, basic_simplifier_plugin & p) :
distribute_forall::distribute_forall(ast_manager & m) :
m_manager(m),
m_bsimp(p),
m_cache(m) {
}
@ -109,6 +109,8 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
expr * e = get_cached(q->get_expr());
if (m_manager.is_not(e) && m_manager.is_or(to_app(e)->get_arg(0))) {
bool_rewriter br(m_manager);
// found target for simplification
// (forall X (not (or F1 ... Fn)))
// -->
@ -121,8 +123,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
for (unsigned i = 0; i < num_args; i++) {
expr * arg = or_e->get_arg(i);
expr_ref not_arg(m_manager);
// m_bsimp.mk_not applies basic simplifications. For example, if arg is of the form (not a), then it will return a.
m_bsimp.mk_not(arg, not_arg);
br.mk_not(arg, not_arg);
quantifier_ref tmp_q(m_manager);
tmp_q = m_manager.update_quantifier(q, not_arg);
expr_ref new_q(m_manager);
@ -132,7 +133,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
expr_ref result(m_manager);
// m_bsimp.mk_and actually constructs a (not (or ...)) formula,
// it will also apply basic simplifications.
m_bsimp.mk_and(new_args.size(), new_args.c_ptr(), result);
br.mk_and(new_args.size(), new_args.c_ptr(), result);
cache_result(q, result);
}
else {

4
src/ast/simplifier/distribute_forall.h → src/ast/rewriter/distribute_forall.h
View file

@ -22,7 +22,6 @@ Revision History:
#define DISTRIBUTE_FORALL_H_
#include"ast.h"
#include"basic_simplifier_plugin.h"
#include"act_cache.h"
/**
@ -47,7 +46,6 @@ Revision History:
class distribute_forall {
typedef act_cache expr_map;
ast_manager & m_manager;
basic_simplifier_plugin & m_bsimp; // useful for constructing formulas and/or/not in simplified form.
ptr_vector<expr> m_todo;
expr_map m_cache;
ptr_vector<expr> m_new_args;
@ -57,7 +55,7 @@ class distribute_forall {
public:
distribute_forall(ast_manager & m, basic_simplifier_plugin & p);
distribute_forall(ast_manager & m);
/**
\brief Apply the distribute_forall transformation (when possible) to all universal quantifiers in \c f.

34
src/cmd_context/cmd_context.cpp
View file

@ -326,6 +326,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
m_numeral_as_real(false),
m_ignore_check(false),
m_exit_on_error(false),
m_processing_pareto(false),
m_manager(m),
m_own_manager(m == 0),
m_manager_initialized(false),
@ -1130,6 +1131,7 @@ void cmd_context::insert_aux_pdecl(pdecl * p) {
}
void cmd_context::reset(bool finalize) {
m_processing_pareto = false;
m_logic = symbol::null;
m_check_sat_result = 0;
m_numeral_as_real = false;
@ -1174,6 +1176,7 @@ void cmd_context::reset(bool finalize) {
}
void cmd_context::assert_expr(expr * t) {
m_processing_pareto = false;
if (!m_check_logic(t))
throw cmd_exception(m_check_logic.get_last_error());
m_check_sat_result = 0;
@ -1186,6 +1189,7 @@ void cmd_context::assert_expr(expr * t) {
}
void cmd_context::assert_expr(symbol const & name, expr * t) {
m_processing_pareto = false;
if (!m_check_logic(t))
throw cmd_exception(m_check_logic.get_last_error());
if (!produce_unsat_cores() || name == symbol::null) {
@ -1286,6 +1290,7 @@ static void restore(ast_manager & m, ptr_vector<expr> & c, unsigned old_sz) {
}
void cmd_context::restore_assertions(unsigned old_sz) {
m_processing_pareto = false;
if (!has_manager()) {
// restore_assertions invokes m(), so if cmd_context does not have a manager, it will try to create one.
SASSERT(old_sz == m_assertions.size());
@ -1303,6 +1308,7 @@ void cmd_context::restore_assertions(unsigned old_sz) {
void cmd_context::pop(unsigned n) {
m_check_sat_result = 0;
m_processing_pareto = false;
if (n == 0)
return;
unsigned lvl = m_scopes.size();
@ -1333,7 +1339,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
unsigned rlimit = m_params.m_rlimit;
scoped_watch sw(*this);
lbool r;
bool was_pareto = false, was_opt = false;
bool was_opt = false;
if (m_opt && !m_opt->empty()) {
was_opt = true;
@ -1342,21 +1348,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
scoped_ctrl_c ctrlc(eh);
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(m().limit(), rlimit);
ptr_vector<expr> cnstr(m_assertions);
cnstr.append(num_assumptions, assumptions);
get_opt()->set_hard_constraints(cnstr);
if (!m_processing_pareto) {
ptr_vector<expr> cnstr(m_assertions);
cnstr.append(num_assumptions, assumptions);
get_opt()->set_hard_constraints(cnstr);
}
try {
r = get_opt()->optimize();
while (r == l_true && get_opt()->is_pareto()) {
was_pareto = true;
get_opt()->display_assignment(regular_stream());
regular_stream() << "\n";
if (get_opt()->print_model()) {
model_ref mdl;
get_opt()->get_model(mdl);
display_model(mdl);
}
r = get_opt()->optimize();
if (r == l_true && get_opt()->is_pareto()) {
m_processing_pareto = true;
}
}
catch (z3_error & ex) {
@ -1366,8 +1366,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
get_opt()->display_assignment(regular_stream());
throw cmd_exception(ex.msg());
}
if (was_pareto && r == l_false) {
r = l_true;
if (m_processing_pareto && r != l_true) {
m_processing_pareto = false;
}
get_opt()->set_status(r);
}
@ -1400,7 +1400,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
validate_model();
}
validate_check_sat_result(r);
if (was_opt && r != l_false && !was_pareto) {
if (was_opt && r != l_false && !m_processing_pareto) {
get_opt()->display_assignment(regular_stream());
}

2
src/cmd_context/cmd_context.h
View file

@ -123,7 +123,6 @@ public:
virtual void display_assignment(std::ostream& out) = 0;
virtual bool is_pareto() = 0;
virtual void set_logic(symbol const& s) = 0;
virtual bool print_model() const = 0;
virtual void get_box_model(model_ref& mdl, unsigned index) = 0;
virtual void updt_params(params_ref const& p) = 0;
};
@ -161,6 +160,7 @@ protected:
status m_status;
bool m_numeral_as_real;
bool m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
bool m_processing_pareto; // used when re-entering check-sat for pareto front.
bool m_exit_on_error;
static std::ostringstream g_error_stream;

3
src/muz/base/rule_properties.cpp
View file

@ -50,7 +50,8 @@ void rule_properties::collect(rule_set const& rules) {
}
for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) {
sort* d = r->get_decl()->get_domain(i);
if (!m.is_bool(d) && !m_dl.is_finite_sort(d) && !m_bv.is_bv_sort(d)) {
sort_size sz = d->get_num_elements();
if (!sz.is_finite()) {
m_inf_sort.push_back(m_rule);
}
}

5
src/opt/opt_context.cpp
View file

@ -318,11 +318,6 @@ namespace opt {
return r;
}
bool context::print_model() const {
opt_params optp(m_params);
return optp.print_model();
}
void context::get_base_model(model_ref& mdl) {
mdl = m_model;
}

1
src/opt/opt_context.h
View file

@ -183,7 +183,6 @@ namespace opt {
virtual bool empty() { return m_scoped_state.m_objectives.empty(); }
virtual void set_hard_constraints(ptr_vector<expr> & hard);
virtual lbool optimize();
virtual bool print_model() const;
virtual void set_model(model_ref& _m) { m_model = _m; }
virtual void get_model(model_ref& _m);
virtual void get_box_model(model_ref& _m, unsigned index);

1
src/opt/opt_params.pyg
View file

@ -7,7 +7,6 @@ def_module_params('opt',
('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
('print_model', BOOL, False, 'display model for satisfiable constraints'),
('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
('elim_01', BOOL, True, 'eliminate 01 variables'),

21
src/sat/sat_config.cpp
View file

@ -126,6 +126,27 @@ namespace sat {
m_drat_file = p.drat_file();
m_drat = (m_drat_check || m_drat_file != symbol("")) && p.threads() == 1;
m_dyn_sub_res = p.dyn_sub_res();
// Parameters used in Liang, Ganesh, Poupart, Czarnecki AAAI 2016.
m_branching_heuristic = BH_VSIDS;
if (p.branching_heuristic() == symbol("vsids")) {
m_branching_heuristic = BH_VSIDS;
}
else if (p.branching_heuristic() == symbol("chb")) {
m_branching_heuristic = BH_CHB;
}
else if (p.branching_heuristic() == symbol("lrb")) {
m_branching_heuristic = BH_LRB;
}
else {
throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids', 'lrb' or 'chb'");
}
m_anti_exploration = m_branching_heuristic != BH_VSIDS;
m_step_size_init = 0.40;
m_step_size_dec = 0.000001;
m_step_size_min = 0.06;
m_reward_multiplier = 0.9;
m_reward_offset = 1000000.0;
}
void config::collect_param_descrs(param_descrs & r) {

14
src/sat/sat_config.h
View file

@ -44,6 +44,12 @@ namespace sat {
GC_PSM_GLUE
};
enum branching_heuristic {
BH_VSIDS,
BH_CHB,
BH_LRB
};
struct config {
unsigned long long m_max_memory;
phase_selection m_phase;
@ -95,6 +101,14 @@ namespace sat {
symbol m_glue_psm;
symbol m_psm_glue;
// branching heuristic settings.
branching_heuristic m_branching_heuristic;
bool m_anti_exploration;
double m_step_size_init;
double m_step_size_dec;
double m_step_size_min;
double m_reward_multiplier;
double m_reward_offset;
config(params_ref const & p);
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);

4
src/sat/sat_params.pyg
View file

@ -9,6 +9,7 @@ def_module_params('sat',
('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'),
('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
('random_seed', UINT, 0, 'random seed'),
('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
@ -21,8 +22,7 @@ def_module_params('sat',
('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
('core.minimize', BOOL, False, 'minimize computed core'),
('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
('threads', UINT, 1, 'number of parallel threads to use'),
('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'), ('threads', UINT, 1, 'number of parallel threads to use'),
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
('drat.check', BOOL, False, 'build up internal proof and check'),

140
src/sat/sat_solver.cpp
View file

@ -174,6 +174,11 @@ namespace sat {
m_phase.push_back(PHASE_NOT_AVAILABLE);
m_prev_phase.push_back(PHASE_NOT_AVAILABLE);
m_assigned_since_gc.push_back(false);
m_last_conflict.push_back(0);
m_last_propagation.push_back(0);
m_participated.push_back(0);
m_canceled.push_back(0);
m_reasoned.push_back(0);
m_case_split_queue.mk_var_eh(v);
m_simplifier.insert_elim_todo(v);
SASSERT(!was_eliminated(v));
@ -580,6 +585,29 @@ namespace sat {
if (m_ext && m_external[v])
m_ext->asserted(l);
switch (m_config.m_branching_heuristic) {
case BH_VSIDS:
break;
case BH_CHB:
m_last_propagation[v] = m_stats.m_conflict;
break;
case BH_LRB:
m_participated[v] = 0;
m_reasoned[v] = 0;
break;
}
if (m_config.m_anti_exploration) {
uint64 age = m_stats.m_conflict - m_canceled[v];
if (age > 0) {
double decay = pow(0.95, age);
m_activity[v] = static_cast<unsigned>(m_activity[v] * decay);
// NB. MapleSAT does not update canceled.
m_canceled[v] = m_stats.m_conflict;
m_case_split_queue.activity_changed_eh(v, false);
}
}
SASSERT(!l.sign() || m_phase[v] == NEG_PHASE);
SASSERT(l.sign() || m_phase[v] == POS_PHASE);
@ -771,7 +799,11 @@ namespace sat {
}
bool solver::propagate(bool update) {
unsigned qhead = m_qhead;
bool r = propagate_core(update);
if (m_config.m_branching_heuristic == BH_CHB) {
update_chb_activity(r, qhead);
}
CASSERT("sat_propagate", check_invariant());
CASSERT("sat_missed_prop", check_missed_propagation());
return r;
@ -1064,6 +1096,18 @@ namespace sat {
}
while (!m_case_split_queue.empty()) {
if (m_config.m_anti_exploration) {
next = m_case_split_queue.min_var();
auto age = m_stats.m_conflict - m_canceled[next];
while (age > 0) {
double decay = pow(0.95, age);
m_activity[next] = static_cast<unsigned>(m_activity[next] * pow(0.95, age));
m_case_split_queue.activity_changed_eh(next, false);
m_canceled[next] = m_stats.m_conflict;
next = m_case_split_queue.min_var();
age = m_stats.m_conflict - m_canceled[next];
}
}
next = m_case_split_queue.next_var();
if (value(next) == l_undef && !was_eliminated(next))
return next;
@ -1828,6 +1872,9 @@ namespace sat {
m_conflicts_since_restart++;
m_conflicts_since_gc++;
m_stats.m_conflict++;
if (m_step_size > m_config.m_step_size_min) {
m_step_size -= m_config.m_step_size_dec;
}
m_conflict_lvl = get_max_lvl(m_not_l, m_conflict);
TRACE("sat", tout << "conflict detected at level " << m_conflict_lvl << " for ";
@ -2175,7 +2222,16 @@ namespace sat {
SASSERT(var < num_vars());
if (!is_marked(var) && var_lvl > 0) {
mark(var);
inc_activity(var);
switch (m_config.m_branching_heuristic) {
case BH_VSIDS:
inc_activity(var);
break;
case BH_CHB:
m_last_conflict[var] = m_stats.m_conflict;
break;
default:
break;
}
if (var_lvl == m_conflict_lvl)
num_marks++;
else
@ -2431,6 +2487,9 @@ namespace sat {
\brief Reset the mark of the variables in the current lemma.
*/
void solver::reset_lemma_var_marks() {
if (m_config.m_branching_heuristic == BH_LRB) {
update_lrb_reasoned();
}
literal_vector::iterator it = m_lemma.begin();
literal_vector::iterator end = m_lemma.end();
SASSERT(!is_marked((*it).var()));
@ -2441,6 +2500,58 @@ namespace sat {
}
}
void solver::update_lrb_reasoned() {
unsigned sz = m_lemma.size();
SASSERT(!is_marked(m_lemma[0].var()));
mark(m_lemma[0].var());
for (unsigned i = m_lemma.size(); i > 0; ) {
--i;
justification js = m_justification[m_lemma[i].var()];
switch (js.get_kind()) {
case justification::NONE:
break;
case justification::BINARY:
update_lrb_reasoned(js.get_literal());
break;
case justification::TERNARY:
update_lrb_reasoned(js.get_literal1());
update_lrb_reasoned(js.get_literal2());
break;
case justification::CLAUSE: {
clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
for (unsigned i = 0; i < c.size(); ++i) {
update_lrb_reasoned(c[i]);
}
break;
}
case justification::EXT_JUSTIFICATION: {
fill_ext_antecedents(m_lemma[i], js);
literal_vector::iterator it = m_ext_antecedents.begin();
literal_vector::iterator end = m_ext_antecedents.end();
for (; it != end; ++it) {
update_lrb_reasoned(*it);
}
break;
}
}
}
reset_mark(m_lemma[0].var());
for (unsigned i = m_lemma.size(); i > sz; ) {
--i;
reset_mark(m_lemma[i].var());
}
m_lemma.shrink(sz);
}
void solver::update_lrb_reasoned(literal lit) {
bool_var v = lit.var();
if (!is_marked(v)) {
mark(v);
m_reasoned[v]++;
m_lemma.push_back(lit);
}
}
/**
\brief Apply dynamic subsumption resolution to new lemma.
Only binary and ternary clauses are used.
@ -2617,6 +2728,18 @@ namespace sat {
bool_var v = l.var();
SASSERT(value(v) == l_undef);
m_case_split_queue.unassign_var_eh(v);
if (m_config.m_branching_heuristic == BH_LRB) {
uint64 interval = m_stats.m_conflict - m_last_propagation[v];
if (interval > 0) {
auto activity = m_activity[v];
auto reward = (m_config.m_reward_offset * (m_participated[v] + m_reasoned[v])) / interval;
m_activity[v] = static_cast<unsigned>(m_step_size * reward + ((1 - m_step_size) * activity));
m_case_split_queue.activity_changed_eh(v, m_activity[v] > activity);
}
}
if (m_config.m_anti_exploration) {
m_canceled[v] = m_stats.m_conflict;
}
}
m_trail.shrink(old_sz);
m_qhead = old_sz;
@ -2799,6 +2922,8 @@ namespace sat {
m_probing.updt_params(p);
m_scc.updt_params(p);
m_rand.set_seed(m_config.m_random_seed);
m_step_size = m_config.m_step_size_init;
}
void solver::collect_param_descrs(param_descrs & d) {
@ -2836,6 +2961,7 @@ namespace sat {
// -----------------------
void solver::rescale_activity() {
SASSERT(m_config.m_branching_heuristic == BH_VSIDS);
svector<unsigned>::iterator it = m_activity.begin();
svector<unsigned>::iterator end = m_activity.end();
for (; it != end; ++it) {
@ -2844,6 +2970,18 @@ namespace sat {
m_activity_inc >>= 14;
}
void solver::update_chb_activity(bool is_sat, unsigned qhead) {
SASSERT(m_config.m_branching_heuristic == BH_CHB);
double multiplier = m_config.m_reward_offset * (is_sat ? m_config.m_reward_multiplier : 1.0);
for (unsigned i = qhead; i < m_trail.size(); ++i) {
auto v = m_trail[i].var();
auto reward = multiplier / (m_stats.m_conflict - m_last_conflict[v] + 1);
auto activity = m_activity[v];
m_activity[v] = static_cast<unsigned>(m_step_size * reward + ((1.0 - m_step_size) * activity));
m_case_split_queue.activity_changed_eh(v, m_activity[v] > activity);
}
}
// -----------------------
//
// Iterators

15
src/sat/sat_solver.h
View file

@ -110,8 +110,17 @@ namespace sat {
svector<char> m_eliminated;
svector<char> m_external;
svector<unsigned> m_level;
// branch variable selection:
svector<unsigned> m_activity;
unsigned m_activity_inc;
svector<uint64> m_last_conflict;
svector<uint64> m_last_propagation;
svector<uint64> m_participated;
svector<uint64> m_canceled;
svector<uint64> m_reasoned;
int m_action;
double m_step_size;
// phase
svector<char> m_phase;
svector<char> m_prev_phase;
svector<char> m_assigned_since_gc;
@ -555,6 +564,12 @@ namespace sat {
private:
void rescale_activity();
void update_chb_activity(bool is_sat, unsigned qhead);
void update_lrb_reasoned();
void update_lrb_reasoned(literal lit);
// -----------------------
//
// Iterators

11
src/sat/sat_var_queue.h
View file

@ -39,6 +39,15 @@ namespace sat {
m_queue.decreased(v);
}
void activity_changed_eh(bool_var v, bool up) {
if (m_queue.contains(v)) {
if (up)
m_queue.decreased(v);
else
m_queue.increased(v);
}
}
void mk_var_eh(bool_var v) {
m_queue.reserve(v+1);
m_queue.insert(v);
@ -61,6 +70,8 @@ namespace sat {
bool empty() const { return m_queue.empty(); }
bool_var next_var() { SASSERT(!empty()); return m_queue.erase_min(); }
bool_var min_var() { SASSERT(!empty()); return m_queue.min_value(); }
};
};

392
src/smt/asserted_formulas.cpp
View file

@ -43,7 +43,7 @@ Revision History:
#include"quasi_macros.h"
asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
m_manager(m),
m(m),
m_params(p),
m_pre_simplifier(m),
m_simplifier(m),
@ -63,7 +63,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
setup_simplifier_plugins(m_simplifier, m_bsimp, arith_simp, m_bvsimp);
SASSERT(m_bsimp != 0);
SASSERT(arith_simp != 0);
m_macro_finder = alloc(macro_finder, m_manager, m_macro_manager);
m_macro_finder = alloc(macro_finder, m, m_macro_manager);
basic_simplifier_plugin * basic_simp = 0;
bv_simplifier_plugin * bv_simp = 0;
@ -90,16 +90,16 @@ void asserted_formulas::setup() {
}
void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp) {
bsimp = alloc(basic_simplifier_plugin, m_manager);
bsimp = alloc(basic_simplifier_plugin, m);
s.register_plugin(bsimp);
asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, m_params);
asimp = alloc(arith_simplifier_plugin, m, *bsimp, m_params);
s.register_plugin(asimp);
s.register_plugin(alloc(array_simplifier_plugin, m_manager, *bsimp, s, m_params));
bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, m_params);
s.register_plugin(alloc(array_simplifier_plugin, m, *bsimp, s, m_params));
bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, m_params);
s.register_plugin(bvsimp);
s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(fpa_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(seq_simplifier_plugin, m_manager, *bsimp));
s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp));
s.register_plugin(alloc(fpa_simplifier_plugin, m, *bsimp));
s.register_plugin(alloc(seq_simplifier_plugin, m, *bsimp));
}
void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) {
@ -108,7 +108,7 @@ void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, pro
SASSERT(!m_inconsistent);
SASSERT(m_scopes.empty());
m_asserted_formulas.append(num_formulas, formulas);
if (m_manager.proofs_enabled())
if (m.proofs_enabled())
m_asserted_formula_prs.append(num_formulas, prs);
}
@ -125,9 +125,9 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, expr_ref_vector & r
SASSERT(!result.empty());
return;
}
if (m_manager.is_false(e))
if (m.is_false(e))
m_inconsistent = true;
::push_assertion(m_manager, e, pr, result, result_prs);
::push_assertion(m, e, pr, result, result_prs);
}
void asserted_formulas::set_eliminate_and(bool flag) {
@ -145,13 +145,13 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
push_assertion(e, _in_pr, m_asserted_formulas, m_asserted_formula_prs);
return;
}
proof_ref in_pr(_in_pr, m_manager);
expr_ref r1(m_manager);
proof_ref pr1(m_manager);
expr_ref r2(m_manager);
proof_ref pr2(m_manager);
TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m_manager) << "\n";);
TRACE("assert_expr_bug", tout << mk_pp(e, m_manager) << "\n";);
proof_ref in_pr(_in_pr, m);
expr_ref r1(m);
proof_ref pr1(m);
expr_ref r2(m);
proof_ref pr2(m);
TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m) << "\n";);
TRACE("assert_expr_bug", tout << mk_pp(e, m) << "\n";);
if (m_params.m_pre_simplifier) {
m_pre_simplifier(e, r1, pr1);
}
@ -161,14 +161,14 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
}
set_eliminate_and(false); // do not eliminate and before nnf.
m_simplifier(r1, r2, pr2);
TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m_manager) << "\n";);
if (m_manager.proofs_enabled()) {
TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m) << "\n";);
if (m.proofs_enabled()) {
if (e == r2)
pr2 = in_pr;
else
pr2 = m_manager.mk_modus_ponens(in_pr, m_manager.mk_transitivity(pr1, pr2));
pr2 = m.mk_modus_ponens(in_pr, m.mk_transitivity(pr1, pr2));
}
TRACE("assert_expr_after_simp", tout << mk_ll_pp(r1, m_manager) << "\n";);
TRACE("assert_expr_after_simp", tout << mk_ll_pp(r1, m) << "\n";);
push_assertion(r2, pr2, m_asserted_formulas, m_asserted_formula_prs);
TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout););
}
@ -176,7 +176,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
void asserted_formulas::assert_expr(expr * e) {
if (inconsistent())
return;
assert_expr(e, m_manager.mk_asserted(e));
assert_expr(e, m.mk_asserted(e));
}
void asserted_formulas::get_assertions(ptr_vector<expr> & result) {
@ -184,13 +184,13 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) {
}
void asserted_formulas::push_scope() {
SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m_manager.canceled());
SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m.canceled());
TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout););
m_scopes.push_back(scope());
m_macro_manager.push_scope();
scope & s = m_scopes.back();
s.m_asserted_formulas_lim = m_asserted_formulas.size();
SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m_manager.canceled());
SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m.canceled());
s.m_inconsistent_old = m_inconsistent;
m_defined_names.push();
m_bv_sharing.push_scope();
@ -206,7 +206,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) {
m_inconsistent = s.m_inconsistent_old;
m_defined_names.pop(num_scopes);
m_asserted_formulas.shrink(s.m_asserted_formulas_lim);
if (m_manager.proofs_enabled())
if (m.proofs_enabled())
m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim);
m_asserted_qhead = s.m_asserted_formulas_lim;
m_scopes.shrink(new_lvl);
@ -228,7 +228,7 @@ void asserted_formulas::reset() {
#ifdef Z3DEBUG
bool asserted_formulas::check_well_sorted() const {
for (unsigned i = 0; i < m_asserted_formulas.size(); i++) {
if (!is_well_sorted(m_manager, m_asserted_formulas.get(i))) return false;
if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false;
}
return true;
}
@ -322,7 +322,7 @@ void asserted_formulas::display(std::ostream & out) const {
for (unsigned i = 0; i < m_asserted_formulas.size(); i++) {
if (i == m_asserted_qhead)
out << "[HEAD] ==>\n";
out << mk_pp(m_asserted_formulas.get(i), m_manager) << "\n";
out << mk_pp(m_asserted_formulas.get(i), m) << "\n";
}
out << "inconsistent: " << inconsistent() << "\n";
}
@ -331,7 +331,7 @@ void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) co
if (!m_asserted_formulas.empty()) {
unsigned sz = m_asserted_formulas.size();
for (unsigned i = 0; i < sz; i++)
ast_def_ll_pp(out, m_manager, m_asserted_formulas.get(i), pp_visited, true, false);
ast_def_ll_pp(out, m, m_asserted_formulas.get(i), pp_visited, true, false);
out << "asserted formulas:\n";
for (unsigned i = 0; i < sz; i++)
out << "#" << m_asserted_formulas[i]->get_id() << " ";
@ -346,23 +346,23 @@ void asserted_formulas::reduce_asserted_formulas() {
if (inconsistent()) {
return;
}
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
for (; i < sz && !inconsistent(); i++) {
expr * n = m_asserted_formulas.get(i);
SASSERT(n != 0);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref new_n(m_manager);
proof_ref new_pr(m_manager);
expr_ref new_n(m);
proof_ref new_pr(m);
m_simplifier(n, new_n, new_pr);
TRACE("reduce_asserted_formulas", tout << mk_pp(n, m_manager) << " -> " << mk_pp(new_n, m_manager) << "\n";);
TRACE("reduce_asserted_formulas", tout << mk_pp(n, m) << " -> " << mk_pp(new_n, m) << "\n";);
if (n == new_n.get()) {
push_assertion(n, pr, new_exprs, new_prs);
}
else {
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
new_pr = m.mk_modus_ponens(pr, new_pr);
push_assertion(new_n, new_pr, new_exprs, new_prs);
}
if (canceled()) {
@ -376,15 +376,15 @@ void asserted_formulas::swap_asserted_formulas(expr_ref_vector & new_exprs, proo
SASSERT(!inconsistent() || !new_exprs.empty());
m_asserted_formulas.shrink(m_asserted_qhead);
m_asserted_formulas.append(new_exprs);
if (m_manager.proofs_enabled()) {
if (m.proofs_enabled()) {
m_asserted_formula_prs.shrink(m_asserted_qhead);
m_asserted_formula_prs.append(new_prs);
}
}
void asserted_formulas::find_macros_core() {
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
unsigned sz = m_asserted_formulas.size();
m_macro_finder->operator()(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead,
m_asserted_formula_prs.c_ptr() + m_asserted_qhead, new_exprs, new_prs);
@ -407,9 +407,9 @@ void asserted_formulas::expand_macros() {
void asserted_formulas::apply_quasi_macros() {
IF_VERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";);
TRACE("before_quasi_macros", display(tout););
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
quasi_macros proc(m_manager, m_macro_manager, m_simplifier);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
quasi_macros proc(m, m_macro_manager, m_simplifier);
while (proc(m_asserted_formulas.size() - m_asserted_qhead,
m_asserted_formulas.c_ptr() + m_asserted_qhead,
m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
@ -423,28 +423,29 @@ void asserted_formulas::apply_quasi_macros() {
}
void asserted_formulas::nnf_cnf() {
IF_VERBOSE(10, verbose_stream() << "(smt.nnf)\n";);
nnf apply_nnf(m_manager, m_defined_names);
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
expr_ref_vector push_todo(m_manager);
proof_ref_vector push_todo_prs(m_manager);
nnf apply_nnf(m, m_defined_names);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
expr_ref_vector push_todo(m);
proof_ref_vector push_todo_prs(m);
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";);
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m_manager) << "\n";);
TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref r1(m_manager);
proof_ref pr1(m_manager);
CASSERT("well_sorted",is_well_sorted(m_manager, n));
expr_ref r1(m);
proof_ref pr1(m);
CASSERT("well_sorted",is_well_sorted(m, n));
push_todo.reset();
push_todo_prs.reset();
apply_nnf(n, push_todo, push_todo_prs, r1, pr1);
CASSERT("well_sorted",is_well_sorted(m_manager, r1));
pr = m_manager.mk_modus_ponens(pr, pr1);
CASSERT("well_sorted",is_well_sorted(m, r1));
pr = m.mk_modus_ponens(pr, pr1);
push_todo.push_back(r1);
push_todo_prs.push_back(pr);
@ -456,13 +457,13 @@ void asserted_formulas::nnf_cnf() {
expr * n = push_todo.get(k);
proof * pr = 0;
m_simplifier(n, r1, pr1);
CASSERT("well_sorted",is_well_sorted(m_manager, r1));
CASSERT("well_sorted",is_well_sorted(m, r1));
if (canceled()) {
return;
}
if (m_manager.proofs_enabled())
pr = m_manager.mk_modus_ponens(push_todo_prs.get(k), pr1);
if (m.proofs_enabled())
pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1);
else
pr = 0;
push_assertion(r1, pr, new_exprs, new_prs);
@ -476,23 +477,23 @@ void asserted_formulas::NAME() {
IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE(LABEL, tout << "before:\n"; display(tout);); \
FUNCTOR_DEF; \
expr_ref_vector new_exprs(m_manager); \
proof_ref_vector new_prs(m_manager); \
expr_ref_vector new_exprs(m); \
proof_ref_vector new_prs(m); \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m_manager); \
expr_ref new_n(m); \
functor(n, new_n); \
TRACE("simplifier_simple_step", tout << mk_pp(n, m_manager) << "\n" << mk_pp(new_n, m_manager) << "\n";); \
TRACE("simplifier_simple_step", tout << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";); \
if (n == new_n.get()) { \
push_assertion(n, pr, new_exprs, new_prs); \
} \
else if (m_manager.proofs_enabled()) { \
proof_ref new_pr(m_manager); \
new_pr = m_manager.mk_rewrite_star(n, new_n, 0, 0); \
new_pr = m_manager.mk_modus_ponens(pr, new_pr); \
else if (m.proofs_enabled()) { \
proof_ref new_pr(m); \
new_pr = m.mk_rewrite_star(n, new_n, 0, 0); \
new_pr = m.mk_modus_ponens(pr, new_pr); \
push_assertion(new_n, new_pr, new_exprs, new_prs); \
} \
else { \
@ -505,7 +506,7 @@ void asserted_formulas::NAME() {
TRACE(LABEL, display(tout);); \
}
MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m_manager, *m_bsimp), "distribute_forall", "distribute-forall");
MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m), "distribute_forall", "distribute-forall");
void asserted_formulas::reduce_and_solve() {
IF_VERBOSE(10, verbose_stream() << "(smt.reducing)\n";);
@ -516,22 +517,22 @@ void asserted_formulas::reduce_and_solve() {
void asserted_formulas::infer_patterns() {
IF_VERBOSE(10, verbose_stream() << "(smt.pattern-inference)\n";);
TRACE("before_pattern_inference", display(tout););
pattern_inference infer(m_manager, m_params);
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
pattern_inference infer(m, m_params);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref new_n(m_manager);
proof_ref new_pr(m_manager);
expr_ref new_n(m);
proof_ref new_pr(m);
infer(n, new_n, new_pr);
if (n == new_n.get()) {
push_assertion(n, pr, new_exprs, new_prs);
}
else if (m_manager.proofs_enabled()) {
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
else if (m.proofs_enabled()) {
new_pr = m.mk_modus_ponens(pr, new_pr);
push_assertion(new_n, new_pr, new_exprs, new_prs);
}
else {
@ -554,16 +555,16 @@ void asserted_formulas::commit(unsigned new_qhead) {
void asserted_formulas::eliminate_term_ite() {
IF_VERBOSE(10, verbose_stream() << "(smt.eliminating-ite-term)\n";);
TRACE("before_elim_term_ite", display(tout););
elim_term_ite elim(m_manager, m_defined_names);
expr_ref_vector new_exprs(m_manager);
proof_ref_vector new_prs(m_manager);
elim_term_ite elim(m, m_defined_names);
expr_ref_vector new_exprs(m);
proof_ref_vector new_prs(m);
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref new_n(m_manager);
proof_ref new_pr(m_manager);
expr_ref new_n(m);
proof_ref new_pr(m);
elim(n, new_exprs, new_prs, new_n, new_pr);
SASSERT(new_n.get() != 0);
DEBUG_CODE({
@ -574,8 +575,8 @@ void asserted_formulas::eliminate_term_ite() {
if (n == new_n.get()) {
push_assertion(n, pr, new_exprs, new_prs);
}
else if (m_manager.proofs_enabled()) {
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
else if (m.proofs_enabled()) {
new_pr = m.mk_modus_ponens(pr, new_pr);
push_assertion(new_n, new_pr, new_exprs, new_prs);
}
else {
@ -602,31 +603,31 @@ void asserted_formulas::propagate_values() {
// - new_exprs2 is the set R
//
// The loop also updates the m_cache. It adds the entries x -> n to it.
expr_ref_vector new_exprs1(m_manager);
proof_ref_vector new_prs1(m_manager);
expr_ref_vector new_exprs2(m_manager);
proof_ref_vector new_prs2(m_manager);
expr_ref_vector new_exprs1(m);
proof_ref_vector new_prs1(m);
expr_ref_vector new_exprs2(m);
proof_ref_vector new_prs2(m);
unsigned sz = m_asserted_formulas.size();
for (unsigned i = 0; i < sz; i++) {
expr_ref n(m_asserted_formulas.get(i), m_manager);
proof_ref pr(m_asserted_formula_prs.get(i, 0), m_manager);
TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";);
expr_ref n(m_asserted_formulas.get(i), m);
proof_ref pr(m_asserted_formula_prs.get(i, 0), m);
TRACE("simplifier", tout << mk_pp(n, m) << "\n";);
expr* lhs, *rhs;
if (m_manager.is_eq(n, lhs, rhs) &&
(m_manager.is_value(lhs) || m_manager.is_value(rhs))) {
if (m_manager.is_value(lhs)) {
if (m.is_eq(n, lhs, rhs) &&
(m.is_value(lhs) || m.is_value(rhs))) {
if (m.is_value(lhs)) {
std::swap(lhs, rhs);
n = m_manager.mk_eq(lhs, rhs);
pr = m_manager.mk_symmetry(pr);
n = m.mk_eq(lhs, rhs);
pr = m.mk_symmetry(pr);
}
if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
if (!m.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
if (i >= m_asserted_qhead) {
new_exprs1.push_back(n);
if (m_manager.proofs_enabled())
if (m.proofs_enabled())
new_prs1.push_back(pr);
}
TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";
if (pr) tout << "proof: " << mk_pp(pr, m_manager) << "\n";);
TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m) << "\n->\n" << mk_pp(rhs, m) << "\n";
if (pr) tout << "proof: " << mk_pp(pr, m) << "\n";);
m_simplifier.cache_result(lhs, rhs, pr);
found = true;
continue;
@ -634,7 +635,7 @@ void asserted_formulas::propagate_values() {
}
if (i >= m_asserted_qhead) {
new_exprs2.push_back(n);
if (m_manager.proofs_enabled())
if (m.proofs_enabled())
new_prs2.push_back(pr);
}
}
@ -646,14 +647,14 @@ void asserted_formulas::propagate_values() {
for (unsigned i = 0; i < sz; i++) {
expr * n = new_exprs2.get(i);
proof * pr = new_prs2.get(i, 0);
expr_ref new_n(m_manager);
proof_ref new_pr(m_manager);
expr_ref new_n(m);
proof_ref new_pr(m);
m_simplifier(n, new_n, new_pr);
if (n == new_n.get()) {
push_assertion(n, pr, new_exprs1, new_prs1);
}
else {
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
new_pr = m.mk_modus_ponens(pr, new_pr);
push_assertion(new_n, new_pr, new_exprs1, new_prs1);
}
}
@ -677,25 +678,25 @@ void asserted_formulas::propagate_booleans() {
cont = false;
unsigned i = m_asserted_qhead;
unsigned sz = m_asserted_formulas.size();
#define PROCESS() { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m_manager); \
proof_ref new_pr(m_manager); \
m_simplifier(n, new_n, new_pr); \
m_asserted_formulas.set(i, new_n); \
if (m_manager.proofs_enabled()) { \
new_pr = m_manager.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
if (n != new_n) { \
cont = true; \
modified = true; \
} \
if (m_manager.is_not(new_n)) \
m_simplifier.cache_result(to_app(new_n)->get_arg(0), m_manager.mk_false(), m_manager.mk_iff_false(new_pr)); \
else \
m_simplifier.cache_result(new_n, m_manager.mk_true(), m_manager.mk_iff_true(new_pr)); \
#define PROCESS() { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
m_simplifier(n, new_n, new_pr); \
m_asserted_formulas.set(i, new_n); \
if (m.proofs_enabled()) { \
new_pr = m.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
if (n != new_n) { \
cont = true; \
modified = true; \
} \
if (m.is_not(new_n)) \
m_simplifier.cache_result(to_app(new_n)->get_arg(0), m.mk_false(), m.mk_iff_false(new_pr)); \
else \
m_simplifier.cache_result(new_n, m.mk_true(), m.mk_iff_true(new_pr)); \
}
for (; i < sz; i++) {
PROCESS();
@ -715,57 +716,58 @@ void asserted_formulas::propagate_booleans() {
}
#define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE) \
bool asserted_formulas::NAME() { \
IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
FUNCTOR; \
bool changed = false; \
expr_ref_vector new_exprs(m_manager); \
proof_ref_vector new_prs(m_manager); \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m_manager); \
proof_ref new_pr(m_manager); \
functor(n, new_n, new_pr); \
if (n == new_n.get()) { \
push_assertion(n, pr, new_exprs, new_prs); \
} \
else if (m_manager.proofs_enabled()) { \
changed = true; \
if (!new_pr) new_pr = m_manager.mk_rewrite(n, new_n); \
new_pr = m_manager.mk_modus_ponens(pr, new_pr); \
push_assertion(new_n, new_pr, new_exprs, new_prs); \
} \
else { \
changed = true; \
push_assertion(new_n, 0, new_exprs, new_prs); \
} \
} \
swap_asserted_formulas(new_exprs, new_prs); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
if (changed && REDUCE) { \
reduce_and_solve(); \
bool asserted_formulas::NAME() { \
IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
} \
return changed; \
}
FUNCTOR; \
bool changed = false; \
expr_ref_vector new_exprs(m); \
proof_ref_vector new_prs(m); \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
functor(n, new_n, new_pr); \
if (n == new_n.get()) { \
push_assertion(n, pr, new_exprs, new_prs); \
} \
else if (m.proofs_enabled()) { \
changed = true; \
if (!new_pr) new_pr = m.mk_rewrite(n, new_n); \
new_pr = m.mk_modus_ponens(pr, new_pr); \
push_assertion(new_n, new_pr, new_exprs, new_prs); \
} \
else { \
changed = true; \
push_assertion(new_n, 0, new_exprs, new_prs); \
} \
} \
swap_asserted_formulas(new_exprs, new_prs); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
if (changed && REDUCE) { \
reduce_and_solve(); \
TRACE(TAG, ast_mark visited; display_ll(tout, visited);); \
} \
return changed; \
}
MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m_manager, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false);
MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m_manager), "pull_nested_quantifiers", "pull-nested-quantifiers", false);
MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false);
MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m), "pull_nested_quantifiers", "pull-nested-quantifiers", false);
proof * asserted_formulas::get_inconsistency_proof() const {
if (!inconsistent())
return 0;
if (!m_manager.proofs_enabled())
if (!m.proofs_enabled())
return 0;
unsigned sz = m_asserted_formulas.size();
for (unsigned i = 0; i < sz; i++) {
expr * f = m_asserted_formulas.get(i);
if (m_manager.is_false(f))
if (m.is_false(f))
return m_asserted_formula_prs.get(i);
}
UNREACHABLE();
@ -780,14 +782,14 @@ void asserted_formulas::refine_inj_axiom() {
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref new_n(m_manager);
if (is_quantifier(n) && simplify_inj_axiom(m_manager, to_quantifier(n), new_n)) {
TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m_manager) << "\n" << mk_pp(new_n, m_manager) << "\n";);
expr_ref new_n(m);
if (is_quantifier(n) && simplify_inj_axiom(m, to_quantifier(n), new_n)) {
TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";);
m_asserted_formulas.set(i, new_n);
if (m_manager.proofs_enabled()) {
proof_ref new_pr(m_manager);
new_pr = m_manager.mk_rewrite(n, new_n);
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
if (m.proofs_enabled()) {
proof_ref new_pr(m);
new_pr = m.mk_rewrite(n, new_n);
new_pr = m.mk_modus_ponens(pr, new_pr);
m_asserted_formula_prs.set(i, new_pr);
}
}
@ -797,36 +799,36 @@ void asserted_formulas::refine_inj_axiom() {
MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate-bit-vector-over-integers", true);
MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap-fourier-motzkin", true);
MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m), "elim_bounds", "cheap-fourier-motzkin", true);
MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true);
MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true);
#define LIFT_ITE(NAME, FUNCTOR, MSG) \
void asserted_formulas::NAME() { \
IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE("lift_ite", display(tout);); \
FUNCTOR; \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m_manager); \
proof_ref new_pr(m_manager); \
functor(n, new_n, new_pr); \
TRACE("lift_ite_step", tout << mk_pp(n, m_manager) << "\n";); \
IF_VERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \
m_asserted_formulas.set(i, new_n); \
if (m_manager.proofs_enabled()) { \
new_pr = m_manager.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
} \
TRACE("lift_ite", display(tout);); \
reduce_and_solve(); \
}
#define LIFT_ITE(NAME, FUNCTOR, MSG) \
void asserted_formulas::NAME() { \
IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";); \
TRACE("lift_ite", display(tout);); \
FUNCTOR; \
unsigned i = m_asserted_qhead; \
unsigned sz = m_asserted_formulas.size(); \
for (; i < sz; i++) { \
expr * n = m_asserted_formulas.get(i); \
proof * pr = m_asserted_formula_prs.get(i, 0); \
expr_ref new_n(m); \
proof_ref new_pr(m); \
functor(n, new_n, new_pr); \
TRACE("lift_ite_step", tout << mk_pp(n, m) << "\n";); \
IF_VERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n) << ", after: " << get_num_exprs(new_n) << "\n";); \
m_asserted_formulas.set(i, new_n); \
if (m.proofs_enabled()) { \
new_pr = m.mk_modus_ponens(pr, new_pr); \
m_asserted_formula_prs.set(i, new_pr); \
} \
} \
TRACE("lift_ite", display(tout);); \
reduce_and_solve(); \
}
LIFT_ITE(lift_ite, push_app_ite functor(m_simplifier, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite");
LIFT_ITE(ng_lift_ite, ng_push_app_ite functor(m_simplifier, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite");
@ -848,12 +850,12 @@ void asserted_formulas::max_bv_sharing() {
for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i);
proof * pr = m_asserted_formula_prs.get(i, 0);
expr_ref new_n(m_manager);
proof_ref new_pr(m_manager);
expr_ref new_n(m);
proof_ref new_pr(m);
m_bv_sharing(n, new_n, new_pr);
m_asserted_formulas.set(i, new_n);
if (m_manager.proofs_enabled()) {
new_pr = m_manager.mk_modus_ponens(pr, new_pr);
if (m.proofs_enabled()) {
new_pr = m.mk_modus_ponens(pr, new_pr);
m_asserted_formula_prs.set(i, new_pr);
}
}

6
src/smt/asserted_formulas.h
View file

@ -35,7 +35,7 @@ class arith_simplifier_plugin;
class bv_simplifier_plugin;
class asserted_formulas {
ast_manager & m_manager;
ast_manager & m;
smt_params & m_params;
simplifier m_pre_simplifier;
simplifier m_simplifier;
@ -94,7 +94,7 @@ class asserted_formulas {
unsigned get_total_size() const;
bool has_bv() const;
void max_bv_sharing();
bool canceled() { return m_manager.canceled(); }
bool canceled() { return m.canceled(); }
public:
asserted_formulas(ast_manager & m, smt_params & p);
@ -115,7 +115,7 @@ public:
void commit();
void commit(unsigned new_qhead);
expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); }
proof * get_formula_proof(unsigned idx) const { return m_manager.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); }
proof * const * get_formula_proofs() const { return m_asserted_formula_prs.c_ptr(); }
void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);

1
src/smt/params/smt_params_helper.pyg
View file

@ -44,6 +44,7 @@ def_module_params(module_name='smt',
('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'),
('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'),
('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
('arith.ignore_int', BOOL, False, 'treat integer variables as real'),

3
src/smt/params/theory_arith_params.cpp
View file

@ -35,6 +35,7 @@ void theory_arith_params::updt_params(params_ref const & _p) {
m_arith_ignore_int = p.arith_ignore_int();
m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
m_arith_dump_lemmas = p.arith_dump_lemmas();
m_arith_reflect = p.arith_reflect();
}
@ -85,4 +86,4 @@ void theory_arith_params::display(std::ostream & out) const {
DISPLAY_PARAM(m_nl_arith_branching);
DISPLAY_PARAM(m_nl_arith_rounds);
DISPLAY_PARAM(m_arith_euclidean_solver);
}
}

4
src/smt/theory_str.cpp
View file

@ -7304,7 +7304,7 @@ namespace smt {
TRACE("str", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;);
}
}
} else if (ex_sort == bool_sort) {
} else if (ex_sort == bool_sort && !is_quantifier(ex)) {
TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
": expr is of sort Bool" << std::endl;);
// set up axioms for boolean terms
@ -7351,7 +7351,7 @@ namespace smt {
// if expr is an application, recursively inspect all arguments
if (is_app(ex)) {
app * term = (app*)ex;
app * term = to_app(ex);
unsigned num_args = term->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
set_up_axioms(term->get_arg(i));

16
src/test/lp.cpp
View file

@ -1159,12 +1159,14 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite
lp_solver<double, double> * solver = reader.create_solver(dual);
setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver);
int begin = get_millisecond_count();
stopwatch sw;
sw.start();
if (dual) {
std::cout << "solving for dual" << std::endl;
}
solver->find_maximal_solution();
int span = get_millisecond_span(begin);
sw.stop();
double span = sw.get_seconds();
std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl;
if (solver->get_status() == lp_status::OPTIMAL) {
if (reader.column_names().size() < 20) {
@ -1213,7 +1215,8 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i
if (reader.is_ok()) {
auto * solver = reader.create_solver(dual);
setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver);
int begin = get_millisecond_count();
stopwatch sw;
sw.start();
solver->find_maximal_solution();
std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl;
@ -1227,7 +1230,7 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i
}
std::cout << "cost = " << cost.get_double() << std::endl;
}
std::cout << "processed in " << get_millisecond_span(begin) / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << std::endl;
std::cout << "processed in " << sw.get_current_seconds() / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << std::endl;
delete solver;
} else {
std::cout << "cannot process " << file_name << std::endl;
@ -2426,9 +2429,10 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read
std::cout << "status = " << lp_status_to_string(solver->get_status()) << std::endl;
return;
}
int begin = get_millisecond_count();
stopwatch sw;
sw.start();
lp_status status = solver->solve();
std::cout << "status is " << lp_status_to_string(status) << ", processed for " << get_millisecond_span(begin) / 1000.0 <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl;
std::cout << "status is " << lp_status_to_string(status) << ", processed for " << sw.get_current_seconds() <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl;
if (solver->get_status() == INFEASIBLE) {
vector<std::pair<lean::mpq, constraint_index>> evidence;
solver->get_infeasibility_explanation(evidence);

4
src/util/lp/lp_primal_simplex.h
View file

@ -55,10 +55,6 @@ public:
void set_core_solver_bounds();
void update_time_limit_from_starting_time(int start_time) {
this->m_settings.time_limit -= (get_millisecond_span(start_time) / 1000.);
}
void find_maximal_solution();
void fill_A_x_and_basis_for_stage_one_total_inf();

2
src/util/lp/lp_primal_simplex.hpp
View file

@ -152,7 +152,6 @@ template <typename T, typename X> void lp_primal_simplex<T, X>::set_core_solver_
template <typename T, typename X> void lp_primal_simplex<T, X>::find_maximal_solution() {
int preprocessing_start_time = get_millisecond_count();
if (this->problem_is_empty()) {
this->m_status = lp_status::EMPTY;
return;
@ -169,7 +168,6 @@ template <typename T, typename X> void lp_primal_simplex<T, X>::find_maximal_sol
fill_acceptable_values_for_x();
this->count_slacks_and_artificials();
set_core_solver_bounds();
update_time_limit_from_starting_time(preprocessing_start_time);
solve_with_total_inf();
}

15
src/util/lp/lp_settings.h
View file

@ -8,9 +8,9 @@
#include <string>
#include <algorithm>
#include <limits>
#include <sys/timeb.h>
#include <iomanip>
#include "util/lp/lp_utils.h"
#include "util/stopwatch.h"
namespace lean {
typedef unsigned var_index;
@ -69,10 +69,6 @@ enum non_basic_column_value_position { at_low_bound, at_upper_bound, at_fixed, f
template <typename X> bool is_epsilon_small(const X & v, const double& eps); // forward definition
int get_millisecond_count();
int get_millisecond_span(int start_time);
class lp_resource_limit {
public:
virtual bool get_cancel_flag() = 0;
@ -92,12 +88,13 @@ struct lp_settings {
private:
class default_lp_resource_limit : public lp_resource_limit {
lp_settings& m_settings;
int m_start_time;
stopwatch m_sw;
public:
default_lp_resource_limit(lp_settings& s): m_settings(s), m_start_time(get_millisecond_count()) {}
default_lp_resource_limit(lp_settings& s): m_settings(s) {
m_sw.start();
}
virtual bool get_cancel_flag() {
int span_in_mills = get_millisecond_span(m_start_time);
return (span_in_mills / 1000.0 > m_settings.time_limit);
return (m_sw.get_current_seconds() > m_settings.time_limit);
}
};

13
src/util/lp/lp_settings.hpp
View file

@ -52,19 +52,6 @@ lp_status lp_status_from_string(std::string status) {
lean_unreachable();
return lp_status::UNKNOWN; // it is unreachable
}
int get_millisecond_count() {
timeb tb;
ftime(&tb);
return tb.millitm + (tb.time & 0xfffff) * 1000;
}
int get_millisecond_span(int start_time) {
int span = get_millisecond_count() - start_time;
if (span < 0)
span += 0x100000 * 1000;
return span;
}
template <typename T>

8
src/util/lp/matrix.hpp
View file

@ -58,8 +58,8 @@ unsigned get_width_of_column(unsigned j, vector<vector<std::string>> & A) {
unsigned r = 0;
for (unsigned i = 0; i < A.size(); i++) {
vector<std::string> & t = A[i];
std::string str= t[j];
unsigned s = str.size();
std::string str = t[j];
unsigned s = static_cast<unsigned>(str.size());
if (r < s) {
r = s;
}
@ -69,8 +69,8 @@ unsigned get_width_of_column(unsigned j, vector<vector<std::string>> & A) {
void print_matrix_with_widths(vector<vector<std::string>> & A, vector<unsigned> & ws, std::ostream & out) {
for (unsigned i = 0; i < A.size(); i++) {
for (unsigned j = 0; j < A[i].size(); j++) {
print_blanks(ws[j] - A[i][j].size(), out);
for (unsigned j = 0; j < static_cast<unsigned>(A[i].size()); j++) {
print_blanks(ws[j] - static_cast<unsigned>(A[i][j].size()), out);
out << A[i][j] << " ";
}
out << std::endl;

6
src/util/lp/sparse_matrix.hpp
View file

@ -1050,8 +1050,8 @@ bool sparse_matrix<T, X>::get_pivot_for_column(unsigned &i, unsigned &j, int c_p
if (i_inv < k) continue;
unsigned j_inv = adjust_column_inverse(j);
if (j_inv < k) continue;
int small = elem_is_too_small(i, j, c_partial_pivoting);
if (!small) {
int _small = elem_is_too_small(i, j, c_partial_pivoting);
if (!_small) {
#ifdef LEAN_DEBUG
// if (!really_best_pivot(i, j, c_partial_pivoting, k)) {
// print_active_matrix(k);
@ -1063,7 +1063,7 @@ bool sparse_matrix<T, X>::get_pivot_for_column(unsigned &i, unsigned &j, int c_p
j = j_inv;
return true;
}
if (small != 2) { // 2 means that the pair is not in the matrix
if (_small != 2) { // 2 means that the pair is not in the matrix
pivots_candidates_that_are_too_small.push_back(std::make_pair(i, j));
}
}