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

remove template Context dependency in every trail object

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-08 15:41:57 -08:00
parent df0a449f70
commit a152bb1e80
65 changed files with 413 additions and 413 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/ast_trail.h
View file

@ -56,8 +56,8 @@ public:
}
};
template<typename Ctx, typename S, typename T>
class ast2ast_trail : public trail<Ctx> {
template<typename S, typename T>
class ast2ast_trail : public trail {
ast2ast_trailmap<S,T>& m_map;
public:
ast2ast_trail(ast2ast_trailmap<S,T>& m, S* s, T* t) :
@ -65,7 +65,7 @@ public:
m.insert(s,t);
}
void undo(Ctx& ctx) override {
void undo() override {
m_map.pop();
}
};

2
src/ast/euf/euf_egraph.h
View file

@ -74,7 +74,7 @@ namespace euf {
class egraph {
typedef ptr_vector<trail<egraph> > trail_stack;
typedef ptr_vector<trail> trail_stack;
struct to_merge {
enode* a, * b;

13
src/muz/base/dl_context.cpp
View file

@ -148,36 +148,37 @@ namespace datalog {
//
// -----------------------------------
class context::restore_rules : public trail<context> {
class context::restore_rules : public trail {
context& ctx;
rule_set* m_old_rules;
void reset() {
dealloc(m_old_rules);
m_old_rules = nullptr;
}
public:
restore_rules(rule_set& r): m_old_rules(alloc(rule_set, r)) {}
restore_rules(context& ctx, rule_set& r): ctx(ctx), m_old_rules(alloc(rule_set, r)) {}
~restore_rules() override {}
void undo(context& ctx) override {
void undo() override {
ctx.replace_rules(*m_old_rules);
reset();
}
};
template<typename Ctx, typename Vec>
class restore_vec_size_trail : public trail<Ctx> {
class restore_vec_size_trail : public trail {
Vec& m_vector;
unsigned m_old_size;
public:
restore_vec_size_trail(Vec& v): m_vector(v), m_old_size(v.size()) {}
~restore_vec_size_trail() override {}
void undo(Ctx& ctx) override { m_vector.shrink(m_old_size); }
void undo() override { m_vector.shrink(m_old_size); }
};
void context::push() {
m_trail.push_scope();
m_trail.push(restore_rules(m_rule_set));
m_trail.push(restore_rules(*this, m_rule_set));
m_trail.push(restore_vec_size_trail<context,expr_ref_vector>(m_rule_fmls));
m_trail.push(restore_vec_size_trail<context,expr_ref_vector>(m_background));
}

8
src/muz/fp/dl_cmds.cpp
View file

@ -99,7 +99,7 @@ struct dl_context {
void register_predicate(func_decl* pred, unsigned num_kinds, symbol const* kinds) {
if (m_collected_cmds) {
m_collected_cmds->m_rels.push_back(pred);
m_trail.push(push_back_vector<dl_context, func_decl_ref_vector>(m_collected_cmds->m_rels));
m_trail.push(push_back_vector<func_decl_ref_vector>(m_collected_cmds->m_rels));
}
dlctx().register_predicate(pred, false);
dlctx().set_predicate_representation(pred, num_kinds, kinds);
@ -111,8 +111,8 @@ struct dl_context {
expr_ref rl = m_context->bind_vars(rule, true);
m_collected_cmds->m_rules.push_back(rl);
m_collected_cmds->m_names.push_back(name);
m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_rules));
m_trail.push(push_back_vector<dl_context, svector<symbol> >(m_collected_cmds->m_names));
m_trail.push(push_back_vector<expr_ref_vector>(m_collected_cmds->m_rules));
m_trail.push(push_back_vector<svector<symbol> >(m_collected_cmds->m_names));
}
else {
m_context->add_rule(rule, name, bound);
@ -130,7 +130,7 @@ struct dl_context {
qr = m.mk_app(q, args.size(), args.c_ptr());
qr = m_context->bind_vars(qr, false);
m_collected_cmds->m_queries.push_back(qr);
m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_queries));
m_trail.push(push_back_vector<expr_ref_vector>(m_collected_cmds->m_queries));
return true;
}
else {

2
src/qe/qe.cpp
View file

@ -1310,7 +1310,7 @@ namespace qe {
typedef ref_vector_ptr_hash<expr, ast_manager> expr_ref_vector_hash;
typedef ref_vector_ptr_eq<expr, ast_manager> expr_ref_vector_eq;
typedef hashtable<expr_ref_vector*, expr_ref_vector_hash, expr_ref_vector_eq> clause_table;
typedef value_trail<smt::context, unsigned> _value_trail;
typedef value_trail<unsigned> _value_trail;
class quant_elim_plugin : public i_solver_context {

6
src/sat/smt/arith_internalize.cpp
View file

@ -47,7 +47,7 @@ namespace arith {
get_one(false);
get_zero(true);
get_zero(false);
ctx.push(value_trail<euf::solver, bool>(m_internalize_initialized));
ctx.push(value_trail<bool>(m_internalize_initialized));
m_internalize_initialized = true;
}
}
@ -89,7 +89,7 @@ namespace arith {
}
void solver::found_unsupported(expr* n) {
ctx.push(value_trail<euf::solver, expr*>(m_not_handled));
ctx.push(value_trail<expr*>(m_not_handled));
TRACE("arith", tout << "unsupported " << mk_pp(n, m) << "\n";);
m_not_handled = n;
}
@ -125,7 +125,7 @@ namespace arith {
if (var != UINT_MAX) {
return var;
}
ctx.push(value_trail<euf::solver, lpvar>(var));
ctx.push(value_trail<lpvar>(var));
app_ref cnst(a.mk_numeral(rational(c), is_int), m);
mk_enode(cnst);
theory_var v = mk_evar(cnst);

10
src/sat/smt/arith_solver.cpp
View file

@ -423,7 +423,7 @@ namespace arith {
if (b.first == UINT_MAX || (is_lower ? b.second < v : b.second > v)) {
TRACE("arith", tout << "tighter bound " << tv.to_string() << "\n";);
m_history.push_back(vec[ti]);
ctx.push(history_trail<euf::solver, constraint_bound>(vec, ti, m_history));
ctx.push(history_trail<constraint_bound>(vec, ti, m_history));
b.first = ci;
b.second = v;
}
@ -765,7 +765,7 @@ namespace arith {
void solver::updt_unassigned_bounds(theory_var v, int inc) {
TRACE("arith_verbose", tout << "v" << v << " " << m_unassigned_bounds[v] << " += " << inc << "\n";);
ctx.push(vector_value_trail<euf::solver, unsigned, false>(m_unassigned_bounds, v));
ctx.push(vector_value_trail<unsigned, false>(m_unassigned_bounds, v));
m_unassigned_bounds[v] += inc;
}
@ -792,7 +792,7 @@ namespace arith {
void solver::init_model() {
if (m.inc() && m_solver.get() && get_num_vars() > 0) {
TRACE("arith", display(tout << "update variable values\n"););
ctx.push(value_trail<euf::solver, bool>(m_model_is_initialized));
ctx.push(value_trail<bool>(m_model_is_initialized));
m_model_is_initialized = true;
lp().init_model();
}
@ -895,7 +895,7 @@ namespace arith {
}
if (m_assume_eq_candidates.size() > old_sz)
ctx.push(restore_size_trail<euf::solver, std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
ctx.push(restore_size_trail<std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
return delayed_assume_eqs();
}
@ -904,7 +904,7 @@ namespace arith {
if (m_assume_eq_head == m_assume_eq_candidates.size())
return false;
ctx.push(value_trail<euf::solver, unsigned>(m_assume_eq_head));
ctx.push(value_trail<unsigned>(m_assume_eq_head));
while (m_assume_eq_head < m_assume_eq_candidates.size()) {
std::pair<theory_var, theory_var> const& p = m_assume_eq_candidates[m_assume_eq_head];
theory_var v1 = p.first;

12
src/sat/smt/array_axioms.cpp
View file

@ -28,14 +28,14 @@ namespace array {
if (m_axioms.contains(idx))
m_axiom_trail.pop_back();
else
ctx.push(push_back_vector<euf::solver, svector<axiom_record>>(m_axiom_trail));
ctx.push(push_back_vector<svector<axiom_record>>(m_axiom_trail));
}
bool solver::propagate_axiom(unsigned idx) {
if (m_axioms.contains(idx))
return false;
m_axioms.insert(idx);
ctx.push(insert_map<euf::solver, axiom_table_t, unsigned>(m_axioms, idx));
ctx.push(insert_map<axiom_table_t, unsigned>(m_axioms, idx));
return assert_axiom(idx);
}
@ -75,11 +75,11 @@ namespace array {
return false;
}
struct solver::set_delay_bit : trail<euf::solver> {
struct solver::set_delay_bit : trail {
solver& s;
unsigned m_idx;
set_delay_bit(solver& s, unsigned idx) : s(s), m_idx(idx) {}
void undo(euf::solver& euf) override {
void undo(/*euf::solver& euf*/) override {
s.m_axiom_trail[m_idx].m_delayed = false;
}
};
@ -458,11 +458,11 @@ namespace array {
func_decl* diag = nullptr;
if (!m_sort2epsilon.find(s, eps)) {
eps = m.mk_fresh_const("epsilon", s);
ctx.push(ast2ast_trail<euf::solver, sort, app>(m_sort2epsilon, s, eps));
ctx.push(ast2ast_trail<sort, app>(m_sort2epsilon, s, eps));
}
if (!m_sort2diag.find(s, diag)) {
diag = m.mk_fresh_func_decl("diag", 1, &s, s);
ctx.push(ast2ast_trail<euf::solver, sort, func_decl>(m_sort2diag, s, diag));
ctx.push(ast2ast_trail<sort, func_decl>(m_sort2diag, s, diag));
}
return std::make_pair(eps, diag);
}

4
src/sat/smt/array_internalize.cpp
View file

@ -210,8 +210,8 @@ namespace array {
for (unsigned i = 0; i < dimension; ++i)
result->push_back(a.mk_array_ext(s, i));
m_sort2diff.insert(s, result);
ctx.push(insert_map<euf::solver, obj_map<sort, func_decl_ref_vector*>, sort*>(m_sort2diff, s));
ctx.push(new_obj_trail<euf::solver,func_decl_ref_vector>(result));
ctx.push(insert_map<obj_map<sort, func_decl_ref_vector*>, sort*>(m_sort2diff, s));
ctx.push(new_obj_trail<func_decl_ref_vector>(result));
return *result;
}

4
src/sat/smt/array_solver.cpp
View file

@ -176,7 +176,7 @@ namespace array {
return false;
force_push();
bool prop = false;
ctx.push(value_trail<euf::solver, unsigned>(m_qhead));
ctx.push(value_trail<unsigned>(m_qhead));
for (; m_qhead < m_axiom_trail.size() && !s().inconsistent(); ++m_qhead)
if (propagate_axiom(m_qhead))
prop = true;
@ -269,7 +269,7 @@ namespace array {
auto& d = get_var_data(find(v));
if (d.m_prop_upward)
return;
ctx.push(reset_flag_trail<euf::solver>(d.m_prop_upward));
ctx.push(reset_flag_trail(d.m_prop_upward));
d.m_prop_upward = true;
if (should_prop_upward(d))
propagate_parent_select_axioms(v);

4
src/sat/smt/bv_delay_internalize.cpp
View file

@ -345,9 +345,9 @@ namespace bv {
void solver::set_delay_internalize(expr* e, internalize_mode mode) {
if (!m_delay_internalize.contains(e))
ctx.push(insert_obj_map<euf::solver, expr, internalize_mode>(m_delay_internalize, e));
ctx.push(insert_obj_map<expr, internalize_mode>(m_delay_internalize, e));
else
ctx.push(remove_obj_map<euf::solver, expr, internalize_mode>(m_delay_internalize, e, m_delay_internalize[e]));
ctx.push(remove_obj_map<expr, internalize_mode>(m_delay_internalize, e, m_delay_internalize[e]));
m_delay_internalize.insert(e, mode);
}

16
src/sat/smt/bv_internalize.cpp
View file

@ -23,21 +23,21 @@ Author:
namespace bv {
class solver::add_var_pos_trail : public trail<euf::solver> {
class solver::add_var_pos_trail : public trail {
solver::atom* m_atom;
public:
add_var_pos_trail(solver::atom* a) :m_atom(a) {}
void undo(euf::solver& euf) override {
void undo() override {
SASSERT(m_atom->m_occs);
m_atom->m_occs = m_atom->m_occs->m_next;
}
};
class solver::add_eq_occurs_trail : public trail<euf::solver> {
class solver::add_eq_occurs_trail : public trail {
atom* m_atom;
public:
add_eq_occurs_trail(atom* a) :m_atom(a) {}
void undo(euf::solver& euf) override {
void undo() override {
SASSERT(m_atom->m_eqs);
m_atom->m_eqs = m_atom->m_eqs->m_next;
if (m_atom->m_eqs)
@ -45,12 +45,12 @@ namespace bv {
}
};
class solver::del_eq_occurs_trail : public trail<euf::solver> {
class solver::del_eq_occurs_trail : public trail {
atom* m_atom;
eq_occurs* m_node;
public:
del_eq_occurs_trail(atom* a, eq_occurs* n) : m_atom(a), m_node(n) {}
void undo(euf::solver& euf) override {
void undo() override {
if (m_node->m_next)
m_node->m_next->m_prev = m_node;
if (m_node->m_prev)
@ -71,12 +71,12 @@ namespace bv {
ctx.push(del_eq_occurs_trail(a, occ));
}
class solver::mk_atom_trail : public trail<euf::solver> {
class solver::mk_atom_trail : public trail {
solver& th;
sat::bool_var m_var;
public:
mk_atom_trail(sat::bool_var v, solver& th) : th(th), m_var(v) {}
void undo(euf::solver& euf) override {
void undo() override {
solver::atom* a = th.get_bv2a(m_var);
a->~atom();
th.erase_bv2a(m_var);

10
src/sat/smt/bv_solver.cpp
View file

@ -24,7 +24,7 @@ Author:
namespace bv {
class solver::bit_trail : public trail<euf::solver> {
class solver::bit_trail : public trail {
solver& s;
solver::var_pos vp;
sat::literal lit;
@ -36,14 +36,14 @@ namespace bv {
}
};
class solver::bit_occs_trail : public trail<euf::solver> {
class solver::bit_occs_trail : public trail {
atom& a;
var_pos_occ* m_occs;
public:
bit_occs_trail(solver& s, atom& a): a(a), m_occs(a.m_occs) {}
virtual void undo(euf::solver& euf) {
virtual void undo() {
a.m_occs = m_occs;
}
};
@ -413,7 +413,7 @@ namespace bv {
if (m_prop_queue_head == m_prop_queue.size())
return false;
force_push();
ctx.push(value_trail<euf::solver, unsigned>(m_prop_queue_head));
ctx.push(value_trail<unsigned>(m_prop_queue_head));
for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) {
auto const p = m_prop_queue[m_prop_queue_head];
if (p.m_atom) {
@ -559,7 +559,7 @@ namespace bv {
SASSERT(l2.var() == l.var());
VERIFY(l2.var() == l.var());
sat::literal r2 = (l.sign() == l2.sign()) ? r : ~r;
ctx.push(vector2_value_trail<euf::solver, bits_vector, sat::literal>(m_bits, vp.first, vp.second));
ctx.push(vector2_value_trail<bits_vector, sat::literal>(m_bits, vp.first, vp.second));
m_bits[vp.first][vp.second] = r2;
set_bit_eh(vp.first, r2, vp.second);
}

4
src/sat/smt/dt_solver.cpp
View file

@ -372,7 +372,7 @@ namespace dt {
}
SASSERT(val == l_undef || (val == l_false && d->m_constructor == nullptr));
d->m_recognizers[c_idx] = recognizer;
ctx.push(set_vector_idx_trail<euf::solver, enode>(d->m_recognizers, c_idx));
ctx.push(set_vector_idx_trail<enode>(d->m_recognizers, c_idx));
if (val == l_false)
propagate_recognizer(v, recognizer);
}
@ -455,7 +455,7 @@ namespace dt {
auto* con2 = d2->m_constructor;
if (con2 != nullptr) {
if (con1 == nullptr) {
ctx.push(set_ptr_trail<euf::solver, enode>(con1));
ctx.push(set_ptr_trail<enode>(con1));
// check whether there is a recognizer in d1 that conflicts with con2;
if (!d1->m_recognizers.empty()) {
unsigned c_idx = dt.get_constructor_idx(con2->get_decl());

4
src/sat/smt/euf_proof.cpp
View file

@ -42,7 +42,7 @@ namespace euf {
get_drat().def_add_arg(arg->get_id());
get_drat().def_end();
m_drat_asts.insert(e);
push(insert_obj_trail<solver, ast>(m_drat_asts, e));
push(insert_obj_trail<ast>(m_drat_asts, e));
}
else {
IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n");
@ -82,7 +82,7 @@ namespace euf {
if (m_drat_asts.contains(f))
return;
m_drat_asts.insert(f);
push(insert_obj_trail<solver, ast>(m_drat_asts, f));
push(insert_obj_trail< ast>(m_drat_asts, f));
std::ostringstream strm;
smt2_pp_environment_dbg env(m);
ast_smt2_pp(strm, f, env);

2
src/sat/smt/euf_solver.cpp
View file

@ -141,7 +141,7 @@ namespace euf {
if (m.is_model_value(f))
return;
m_unhandled_functions.push_back(f);
m_trail.push(push_back_vector<solver, func_decl_ref_vector>(m_unhandled_functions));
m_trail.push(push_back_vector<func_decl_ref_vector>(m_unhandled_functions));
IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n");
}

4
src/sat/smt/euf_solver.h
View file

@ -247,12 +247,12 @@ namespace euf {
template <typename V>
void push_vec(ptr_vector<V>& vec, V* val) {
vec.push_back(val);
push(push_back_trail<solver, V*, false>(vec));
push(push_back_trail< V*, false>(vec));
}
template <typename V>
void push_vec(svector<V>& vec, V val) {
vec.push_back(val);
push(push_back_trail<solver, V, false>(vec));
push(push_back_trail< V, false>(vec));
}
euf_trail_stack& get_trail_stack() { return m_trail; }

2
src/sat/smt/fpa_solver.cpp
View file

@ -64,7 +64,7 @@ namespace fpa {
m.inc_ref(e);
m.inc_ref(res);
ctx.push(insert_ref2_map<euf::solver, ast_manager, expr, expr>(m, m_conversions, e, res.get()));
ctx.push(insert_ref2_map<ast_manager, expr, expr>(m, m_conversions, e, res.get()));
}
return res;
}

26
src/sat/smt/q_ematch.cpp
View file

@ -120,12 +120,12 @@ namespace q {
return out;
}
struct restore_watch : public trail<euf::solver> {
struct restore_watch : public trail {
vector<unsigned_vector>& v;
unsigned idx, offset;
restore_watch(vector<unsigned_vector>& v, unsigned idx):
v(v), idx(idx), offset(v[idx].size()) {}
void undo(euf::solver& ctx) override {
void undo() override {
v[idx].shrink(offset);
}
};
@ -191,20 +191,20 @@ namespace q {
}
}
struct ematch::remove_binding : public trail<euf::solver> {
struct ematch::remove_binding : public trail {
clause& c;
binding* b;
remove_binding(clause& c, binding* b): c(c), b(b) {}
void undo(euf::solver& ctx) override {
void undo() override {
binding::remove_from(c.m_bindings, b);
}
};
struct ematch::insert_binding : public trail<euf::solver> {
struct ematch::insert_binding : public trail {
clause& c;
binding* b;
insert_binding(clause& c, binding* b): c(c), b(b) {}
void undo(euf::solver& ctx) override {
void undo() override {
binding::push_to_front(c.m_bindings, b);
}
};
@ -306,7 +306,7 @@ namespace q {
return nullptr;
fingerprint* f = new (ctx.get_region()) fingerprint(c, b, max_generation);
m_fingerprints.insert(f);
ctx.push(insert_map<euf::solver, fingerprints, fingerprint*>(m_fingerprints, f));
ctx.push(insert_map<fingerprints, fingerprint*>(m_fingerprints, f));
return f;
}
@ -328,11 +328,11 @@ namespace q {
return l.sign ? ~ctx.mk_literal(fml) : ctx.mk_literal(fml);
}
struct ematch::reset_in_queue : public trail<euf::solver> {
struct ematch::reset_in_queue : public trail {
ematch& e;
reset_in_queue(ematch& e) :e(e) {}
void undo(euf::solver& ctx) override {
void undo() override {
e.m_node_in_queue.reset();
e.m_clause_in_queue.reset();
e.m_in_queue_set = false;
@ -362,7 +362,7 @@ namespace q {
if (!m_clause_in_queue.contains(idx)) {
m_clause_in_queue.insert(idx);
m_clause_queue.push_back(idx);
ctx.push(push_back_vector<euf::solver, unsigned_vector>(m_clause_queue));
ctx.push(push_back_vector<unsigned_vector>(m_clause_queue));
}
}
@ -418,10 +418,10 @@ namespace q {
}
}
struct ematch::pop_clause : public trail<euf::solver> {
struct ematch::pop_clause : public trail {
ematch& em;
pop_clause(ematch& em): em(em) {}
void undo(euf::solver& ctx) override {
void undo() override {
em.m_q2clauses.remove(em.m_clauses.back()->q());
dealloc(em.m_clauses.back());
em.m_clauses.pop_back();
@ -472,7 +472,7 @@ namespace q {
bool propagated = false;
if (m_qhead >= m_clause_queue.size())
return m_inst_queue.propagate();
ctx.push(value_trail<euf::solver, unsigned>(m_qhead));
ctx.push(value_trail<unsigned>(m_qhead));
ptr_buffer<binding> to_remove;
for (; m_qhead < m_clause_queue.size(); ++m_qhead) {
unsigned idx = m_clause_queue[m_qhead];

42
src/sat/smt/q_mam.cpp
View file

@ -75,9 +75,9 @@ namespace q {
template<typename T>
class mam_value_trail : public value_trail<euf::solver, T> {
class mam_value_trail : public value_trail<T> {
public:
mam_value_trail(T & value):value_trail<euf::solver, T>(value) {}
mam_value_trail(T & value):value_trail<T>(value) {}
};
unsigned get_max_generation(unsigned n, enode* const* nodes) {
@ -2812,12 +2812,12 @@ namespace q {
egraph * m_egraph;
#endif
class mk_tree_trail : public trail<euf::solver> {
class mk_tree_trail : public trail {
ptr_vector<code_tree> & m_trees;
unsigned m_lbl_id;
public:
mk_tree_trail(ptr_vector<code_tree> & t, unsigned id):m_trees(t), m_lbl_id(id) {}
void undo(euf::solver & m) override {
void undo() override {
dealloc(m_trees[m_lbl_id]);
m_trees[m_lbl_id] = nullptr;
}
@ -2871,7 +2871,7 @@ namespace q {
}
}
DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(mp);
ctx.push(push_back_trail<euf::solver, app*, false>(m_trees[lbl_id]->get_patterns())););
ctx.push(push_back_trail<app*, false>(m_trees[lbl_id]->get_patterns())););
TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););
}
@ -3067,11 +3067,11 @@ namespace q {
enode * m_other { nullptr }; // temp field
bool m_check_missing_instances { false };
class reset_to_match : public trail<euf::solver> {
class reset_to_match : public trail {
mam_impl& i;
public:
reset_to_match(mam_impl& i):i(i) {}
void undo(euf::solver& ctx) override {
void undo() override {
if (i.m_to_match.empty())
return;
for (code_tree* t : i.m_to_match)
@ -3080,11 +3080,11 @@ namespace q {
}
};
class reset_new_patterns : public trail<euf::solver> {
class reset_new_patterns : public trail {
mam_impl& i;
public:
reset_new_patterns(mam_impl& i):i(i) {}
void undo(euf::solver& ctx) override {
void undo() override {
i.m_new_patterns.reset();
}
};
@ -3139,7 +3139,7 @@ namespace q {
TRACE("mam_bug", tout << "update_clbls: " << lbl->get_name() << " is already clbl: " << m_is_clbl[lbl_id] << "\n";);
if (m_is_clbl[lbl_id])
return;
ctx.push(set_bitvector_trail<euf::solver>(m_is_clbl, lbl_id));
ctx.push(set_bitvector_trail(m_is_clbl, lbl_id));
SASSERT(m_is_clbl[lbl_id]);
unsigned h = m_lbl_hasher(lbl);
for (enode* app : m_egraph.enodes_of(lbl)) {
@ -3180,7 +3180,7 @@ namespace q {
TRACE("mam_bug", tout << "update_plbls: " << lbl->get_name() << " is already plbl: " << m_is_plbl[lbl_id] << "\n";);
if (m_is_plbl[lbl_id])
return;
ctx.push(set_bitvector_trail<euf::solver>(m_is_plbl, lbl_id));
ctx.push(set_bitvector_trail(m_is_plbl, lbl_id));
SASSERT(m_is_plbl[lbl_id]);
SASSERT(is_plbl(lbl));
unsigned h = m_lbl_hasher(lbl);
@ -3227,7 +3227,7 @@ namespace q {
p = p->m_child;
}
curr->m_code = mk_code(qa, mp, pat_idx);
ctx.push(new_obj_trail<euf::solver, code_tree>(curr->m_code));
ctx.push(new_obj_trail<code_tree>(curr->m_code));
return head;
}
@ -3250,7 +3250,7 @@ namespace q {
insert_code(t, qa, mp, p->m_pattern_idx);
}
else {
ctx.push(set_ptr_trail<euf::solver, path_tree>(t->m_first_child));
ctx.push(set_ptr_trail<path_tree>(t->m_first_child));
t->m_first_child = mk_path_tree(p->m_child, qa, mp);
}
}
@ -3260,9 +3260,9 @@ namespace q {
insert_code(t, qa, mp, p->m_pattern_idx);
}
else {
ctx.push(set_ptr_trail<euf::solver, code_tree>(t->m_code));
ctx.push(set_ptr_trail<code_tree>(t->m_code));
t->m_code = mk_code(qa, mp, p->m_pattern_idx);
ctx.push(new_obj_trail<euf::solver, code_tree>(t->m_code));
ctx.push(new_obj_trail<code_tree>(t->m_code));
}
}
else {
@ -3275,10 +3275,10 @@ namespace q {
prev_sibling = t;
t = t->m_sibling;
}
ctx.push(set_ptr_trail<euf::solver, path_tree>(prev_sibling->m_sibling));
ctx.push(set_ptr_trail<path_tree>(prev_sibling->m_sibling));
prev_sibling->m_sibling = mk_path_tree(p, qa, mp);
if (!found_label) {
ctx.push(value_trail<euf::solver, approx_set>(head->m_filter));
ctx.push(value_trail<approx_set>(head->m_filter));
head->m_filter.insert(m_lbl_hasher(p->m_label));
}
}
@ -3288,7 +3288,7 @@ namespace q {
insert(m_pc[h1][h2], p, qa, mp);
}
else {
ctx.push(set_ptr_trail<euf::solver, path_tree>(m_pc[h1][h2]));
ctx.push(set_ptr_trail<path_tree>(m_pc[h1][h2]));
m_pc[h1][h2] = mk_path_tree(p, qa, mp);
}
TRACE("mam_path_tree_updt",
@ -3305,7 +3305,7 @@ namespace q {
insert(m_pp[h1][h2].first, p2, qa, mp);
}
else {
ctx.push(set_ptr_trail<euf::solver, path_tree>(m_pp[h1][h2].first));
ctx.push(set_ptr_trail<path_tree>(m_pp[h1][h2].first));
m_pp[h1][h2].first = mk_path_tree(p1, qa, mp);
insert(m_pp[h1][h2].first, p2, qa, mp);
}
@ -3323,8 +3323,8 @@ namespace q {
}
else {
SASSERT(m_pp[h1][h2].second == nullptr);
ctx.push(set_ptr_trail<euf::solver, path_tree>(m_pp[h1][h2].first));
ctx.push(set_ptr_trail<euf::solver, path_tree>(m_pp[h1][h2].second));
ctx.push(set_ptr_trail<path_tree>(m_pp[h1][h2].first));
ctx.push(set_ptr_trail<path_tree>(m_pp[h1][h2].second));
m_pp[h1][h2].first = mk_path_tree(p1, qa, mp);
m_pp[h1][h2].second = mk_path_tree(p2, qa, mp);
}

4
src/sat/smt/q_mbi.cpp
View file

@ -247,8 +247,8 @@ namespace q {
var_subst subst(m);
result = alloc(q_body, m);
m_q2body.insert(q, result);
ctx.push(new_obj_trail<euf::solver, q_body>(result));
ctx.push(insert_obj_map<euf::solver, quantifier, q_body*>(m_q2body, q));
ctx.push(new_obj_trail<q_body>(result));
ctx.push(insert_obj_map<quantifier, q_body*>(m_q2body, q));
app_ref_vector& vars = result->vars;
vars.resize(sz, nullptr);
for (unsigned i = 0; i < sz; ++i) {

8
src/sat/smt/q_model_fixer.cpp
View file

@ -98,8 +98,8 @@ namespace q {
if (!m_q2info.find(q, info)) {
info = alloc(quantifier_macro_info, m, m_qs.flatten(q));
m_q2info.insert(q, info);
ctx.push(new_obj_trail<euf::solver, quantifier_macro_info>(info));
ctx.push(insert_obj_map<euf::solver, quantifier, quantifier_macro_info*>(m_q2info, q));
ctx.push(new_obj_trail<quantifier_macro_info>(info));
ctx.push(insert_obj_map<quantifier, quantifier_macro_info*>(m_q2info, q));
}
return info;
}
@ -200,8 +200,8 @@ namespace q {
if (!proj)
return nullptr;
m_projections.insert(srt, proj);
ctx.push(new_obj_trail<euf::solver, projection_function>(proj));
ctx.push(insert_obj_map<euf::solver, sort, projection_function*>(m_projections, srt));
ctx.push(new_obj_trail<projection_function>(proj));
ctx.push(insert_obj_map<sort, projection_function*>(m_projections, srt));
return proj;
}

10
src/sat/smt/q_queue.cpp
View file

@ -121,10 +121,10 @@ namespace q {
return std::max(f.m_max_generation + 1, static_cast<unsigned>(r));
}
struct queue::reset_new_entries : public trail<euf::solver> {
struct queue::reset_new_entries : public trail {
svector<entry>& m_entries;
reset_new_entries(svector<entry>& e): m_entries(e) {}
void undo(euf::solver& ctx) override {
void undo() override {
m_entries.reset();
}
};
@ -189,18 +189,18 @@ namespace q {
else {
TRACE("q", tout << "delaying quantifier instantiation... " << f << "\n" << mk_pp(f.q(), m) << "\ncost: " << curr.m_cost << "\n";);
m_delayed_entries.push_back(curr);
ctx.push(push_back_vector<euf::solver,svector<entry>>(m_delayed_entries));
ctx.push(push_back_vector<svector<entry>>(m_delayed_entries));
}
}
m_new_entries.reset();
return true;
}
struct queue::reset_instantiated : public trail<euf::solver> {
struct queue::reset_instantiated : public trail {
queue& q;
unsigned idx;
reset_instantiated(queue& q, unsigned idx): q(q), idx(idx) {}
void undo(euf::solver& ctx) override {
void undo() override {
q.m_delayed_entries[idx].m_instantiated = false;
}
};

6
src/sat/smt/q_solver.cpp
View file

@ -173,7 +173,7 @@ namespace q {
m.inc_ref(q_flat);
m.inc_ref(q);
m_flat.insert(q, q_flat);
ctx.push(insert_ref2_map<euf::solver, ast_manager, quantifier, quantifier>(m, m_flat, q, q_flat));
ctx.push(insert_ref2_map<ast_manager, quantifier, quantifier>(m, m_flat, q, q_flat));
return q_flat;
}
@ -188,7 +188,7 @@ namespace q {
if (m_unit_table.contains(s))
continue;
m_unit_table.insert(s, e);
ctx.push(insert_map<euf::solver, obj_map<sort, expr*>, sort*>(m_unit_table, s));
ctx.push(insert_map<obj_map<sort, expr*>, sort*>(m_unit_table, s));
}
}
@ -203,7 +203,7 @@ namespace q {
expr* val = mdl.get_some_value(s);
m.inc_ref(val);
m.inc_ref(s);
ctx.push(insert_ref2_map<euf::solver, ast_manager, sort, expr>(m, m_unit_table, s, val));
ctx.push(insert_ref2_map<ast_manager, sort, expr>(m, m_unit_table, s, val));
return val;
}

2
src/sat/smt/user_solver.cpp
View file

@ -92,7 +92,7 @@ namespace user {
if (m_qhead == m_prop.size())
return false;
force_push();
ctx.push(value_trail<euf::solver, unsigned>(m_qhead));
ctx.push(value_trail<unsigned>(m_qhead));
unsigned np = m_stats.m_num_propagations;
for (; m_qhead < m_prop.size() && !s().inconsistent(); ++m_qhead) {
auto const& prop = m_prop[m_qhead];

4
src/smt/arith_eq_adapter.cpp
View file

@ -26,7 +26,7 @@ Revision History:
namespace smt {
class already_processed_trail : public trail<context> {
class already_processed_trail : public trail {
// Remark: it is safer to use a trail object, because it guarantees that the enodes
// are still alive when the undo operation is performed.
//
@ -42,7 +42,7 @@ namespace smt {
m_n2(n2) {
}
void undo(context & ctx) override {
void undo() override {
m_already_processed.erase(m_n1, m_n2);
TRACE("arith_eq_adapter_profile", tout << "del #" << m_n1->get_owner_id() << " #" << m_n2->get_owner_id() << "\n";);
}

41
src/smt/mam.cpp
View file

@ -66,12 +66,12 @@ namespace {
typedef trail_stack<mam_impl> mam_trail_stack;
typedef trail<mam_impl> mam_trail;
typedef trail mam_trail;
template<typename T>
class mam_value_trail : public value_trail<mam_impl, T> {
class mam_value_trail : public value_trail<T> {
public:
mam_value_trail(T & value):value_trail<mam_impl, T>(value) {}
mam_value_trail(T & value):value_trail<T>(value) {}
};
@ -2883,7 +2883,7 @@ namespace {
unsigned m_lbl_id;
public:
mk_tree_trail(ptr_vector<code_tree> & t, unsigned id):m_trees(t), m_lbl_id(id) {}
void undo(mam_impl & m) override {
void undo() override {
dealloc(m_trees[m_lbl_id]);
m_trees[m_lbl_id] = nullptr;
}
@ -2936,7 +2936,7 @@ namespace {
}
}
DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(mp);
m_trail_stack.push(push_back_trail<mam_impl, app*, false>(m_trees[lbl_id]->get_patterns())););
m_trail_stack.push(push_back_trail<app*, false>(m_trees[lbl_id]->get_patterns())););
TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout););
}
@ -3140,10 +3140,11 @@ namespace {
friend class add_shared_enode_trail;
class add_shared_enode_trail : public mam_trail {
mam_impl& m;
enode * m_enode;
public:
add_shared_enode_trail(enode * n):m_enode(n) {}
void undo(mam_impl & m) override { m.m_shared_enodes.erase(m_enode); }
add_shared_enode_trail(mam_impl& m, enode * n):m(m), m_enode(n) {}
void undo() override { m.m_shared_enodes.erase(m_enode); }
};
#ifdef Z3DEBUG
@ -3198,7 +3199,7 @@ namespace {
TRACE("mam_bug", tout << "update_clbls: " << lbl->get_name() << " is already clbl: " << m_is_clbl[lbl_id] << "\n";);
if (m_is_clbl[lbl_id])
return;
m_trail_stack.push(set_bitvector_trail<mam_impl>(m_is_clbl, lbl_id));
m_trail_stack.push(set_bitvector_trail(m_is_clbl, lbl_id));
SASSERT(m_is_clbl[lbl_id]);
unsigned h = m_lbl_hasher(lbl);
for (enode* app : m_context.enodes_of(lbl)) {
@ -3239,7 +3240,7 @@ namespace {
TRACE("mam_bug", tout << "update_plbls: " << lbl->get_name() << " is already plbl: " << m_is_plbl[lbl_id] << "\n";);
if (m_is_plbl[lbl_id])
return;
m_trail_stack.push(set_bitvector_trail<mam_impl>(m_is_plbl, lbl_id));
m_trail_stack.push(set_bitvector_trail(m_is_plbl, lbl_id));
SASSERT(m_is_plbl[lbl_id]);
SASSERT(is_plbl(lbl));
unsigned h = m_lbl_hasher(lbl);
@ -3286,7 +3287,7 @@ namespace {
p = p->m_child;
}
curr->m_code = mk_code(qa, mp, pat_idx);
m_trail_stack.push(new_obj_trail<mam_impl, code_tree>(curr->m_code));
m_trail_stack.push(new_obj_trail<code_tree>(curr->m_code));
return head;
}
@ -3309,7 +3310,7 @@ namespace {
insert_code(t, qa, mp, p->m_pattern_idx);
}
else {
m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(t->m_first_child));
m_trail_stack.push(set_ptr_trail<path_tree>(t->m_first_child));
t->m_first_child = mk_path_tree(p->m_child, qa, mp);
}
}
@ -3319,9 +3320,9 @@ namespace {
insert_code(t, qa, mp, p->m_pattern_idx);
}
else {
m_trail_stack.push(set_ptr_trail<mam_impl, code_tree>(t->m_code));
m_trail_stack.push(set_ptr_trail<code_tree>(t->m_code));
t->m_code = mk_code(qa, mp, p->m_pattern_idx);
m_trail_stack.push(new_obj_trail<mam_impl, code_tree>(t->m_code));
m_trail_stack.push(new_obj_trail< code_tree>(t->m_code));
}
}
else {
@ -3334,10 +3335,10 @@ namespace {
prev_sibling = t;
t = t->m_sibling;
}
m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(prev_sibling->m_sibling));
m_trail_stack.push(set_ptr_trail<path_tree>(prev_sibling->m_sibling));
prev_sibling->m_sibling = mk_path_tree(p, qa, mp);
if (!found_label) {
m_trail_stack.push(value_trail<mam_impl, approx_set>(head->m_filter));
m_trail_stack.push(value_trail<approx_set>(head->m_filter));
head->m_filter.insert(m_lbl_hasher(p->m_label));
}
}
@ -3347,7 +3348,7 @@ namespace {
insert(m_pc[h1][h2], p, qa, mp);
}
else {
m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(m_pc[h1][h2]));
m_trail_stack.push(set_ptr_trail<path_tree>(m_pc[h1][h2]));
m_pc[h1][h2] = mk_path_tree(p, qa, mp);
}
TRACE("mam_path_tree_updt",
@ -3364,7 +3365,7 @@ namespace {
insert(m_pp[h1][h2].first, p2, qa, mp);
}
else {
m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(m_pp[h1][h2].first));
m_trail_stack.push(set_ptr_trail<path_tree>(m_pp[h1][h2].first));
m_pp[h1][h2].first = mk_path_tree(p1, qa, mp);
insert(m_pp[h1][h2].first, p2, qa, mp);
}
@ -3382,8 +3383,8 @@ namespace {
}
else {
SASSERT(m_pp[h1][h2].second == 0);
m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(m_pp[h1][h2].first));
m_trail_stack.push(set_ptr_trail<mam_impl, path_tree>(m_pp[h1][h2].second));
m_trail_stack.push(set_ptr_trail<path_tree>(m_pp[h1][h2].first));
m_trail_stack.push(set_ptr_trail<path_tree>(m_pp[h1][h2].second));
m_pp[h1][h2].first = mk_path_tree(p1, qa, mp);
m_pp[h1][h2].second = mk_path_tree(p2, qa, mp);
}
@ -3796,7 +3797,7 @@ namespace {
todo.pop_back();
if (n->is_ground()) {
enode * e = mk_enode(m_context, qa, n);
m_trail_stack.push(add_shared_enode_trail(e));
m_trail_stack.push(add_shared_enode_trail(*this, e));
m_shared_enodes.insert(e);
}
else {

2
src/smt/seq_axioms.cpp
View file

@ -719,7 +719,7 @@ void seq_axioms::ensure_digit_axiom() {
expr_ref cnst(seq.mk_char('0'+i), m);
add_axiom(mk_eq(m_sk.mk_digit2int(cnst), a.mk_int(i)));
}
ctx().push_trail(value_trail<context, bool>(m_digits_initialized));
ctx().push_trail(value_trail<bool>(m_digits_initialized));
m_digits_initialized = true;
}
}

8
src/smt/seq_eq_solver.cpp
View file

@ -1148,7 +1148,7 @@ bool theory_seq::branch_variable_eq(eq const& e) {
void theory_seq::insert_branch_start(unsigned k, unsigned s) {
m_branch_start.insert(k, s);
m_trail_stack.push(pop_branch(k));
m_trail_stack.push(pop_branch(*this, k));
}
unsigned theory_seq::find_branch_start(unsigned k) {
@ -1365,7 +1365,7 @@ bool theory_seq::check_length_coherence0(expr* e) {
if (p || assume_equality(e, emp)) {
if (!ctx.at_base_level()) {
m_trail_stack.push(push_replay(alloc(replay_length_coherence, m, e)));
m_trail_stack.push(push_replay(*this, alloc(replay_length_coherence, m, e)));
}
return true;
}
@ -1577,12 +1577,12 @@ bool theory_seq::is_ternary_eq_lhs(expr_ref_vector const& ls, expr_ref_vector co
return false;
}
struct remove_obj_pair_map : public trail<context> {
struct remove_obj_pair_map : public trail {
obj_pair_hashtable<expr, expr> & m_map;
expr* a, *b;
remove_obj_pair_map(obj_pair_hashtable<expr, expr> & map, expr* a, expr* b):
m_map(map), a(a), b(b) {}
void undo(context& ctx) override {
void undo() override {
m_map.erase(std::make_pair(a, b));
}
};

4
src/smt/seq_regex.cpp
View file

@ -379,7 +379,7 @@ namespace smt {
if (entry.m_re == regex)
continue;
th.m_trail_stack.push(vector_value_trail<theory_seq, s_in_re, true>(m_s_in_re, i));
th.m_trail_stack.push(vector_value_trail<s_in_re, true>(m_s_in_re, i));
m_s_in_re[i].m_active = false;
IF_VERBOSE(11, verbose_stream() << "Intersect " << regex << " " <<
mk_pp(entry.m_re, m) << " " << mk_pp(s, m) << " " << mk_pp(entry.m_s, m) << std::endl;);
@ -390,7 +390,7 @@ namespace smt {
lits.push_back(~th.mk_eq(n1->get_owner(), n2->get_owner(), false));
}
m_s_in_re.push_back(s_in_re(lit, s, regex));
th.get_trail_stack().push(push_back_vector<theory_seq, vector<s_in_re>>(m_s_in_re));
th.get_trail_stack().push(push_back_vector<vector<s_in_re>>(m_s_in_re));
if (lits.empty())
return false;
lits.push_back(~lit);

70
src/smt/smt_context.cpp
View file

@ -66,19 +66,8 @@ namespace smt {
m_e_internalized_stack(m),
m_l_internalized_stack(m),
m_final_check_idx(0),
m_is_auxiliary(false),
m_par(nullptr),
m_par_index(0),
m_cg_table(m),
m_is_diseq_tmp(nullptr),
m_units_to_reassert(m),
m_qhead(0),
m_simp_qhead(0),
m_simp_counter(0),
m_bvar_inc(1.0),
m_phase_cache_on(true),
m_phase_counter(0),
m_phase_default(false),
m_conflict(null_b_justification),
m_not_l(null_literal),
m_conflict_resolution(mk_conflict_resolution(m, *this, m_dyn_ack_manager, p, m_assigned_literals, m_watches)),
@ -86,16 +75,9 @@ namespace smt {
m_dyn_ack_manager(*this, p),
m_unknown("unknown"),
m_unsat_core(m),
#ifdef Z3DEBUG
m_trail_enabled(true),
#endif
m_scope_lvl(0),
m_base_lvl(0),
m_search_lvl(0),
m_generation(0),
m_last_search_result(l_undef),
m_last_search_failure(UNKNOWN),
m_searching(false) {
m_mk_bool_var_trail(*this),
m_mk_enode_trail(*this),
m_mk_lambda_trail(*this) {
SASSERT(m_scope_lvl == 0);
SASSERT(m_base_lvl == 0);
@ -447,18 +429,20 @@ namespace smt {
m_th_diseq_propagation_queue.push_back(new_th_eq(th, lhs, rhs));
}
class add_eq_trail : public trail<context> {
class add_eq_trail : public trail {
context& ctx;
enode * m_r1;
enode * m_n1;
unsigned m_r2_num_parents;
public:
add_eq_trail(enode * r1, enode * n1, unsigned r2_num_parents):
add_eq_trail(context& ctx, enode * r1, enode * n1, unsigned r2_num_parents):
ctx(ctx),
m_r1(r1),
m_n1(n1),
m_r2_num_parents(r2_num_parents) {
}
void undo(context & ctx) override {
void undo() override {
ctx.undo_add_eq(m_r1, m_n1, m_r2_num_parents);
}
};
@ -526,7 +510,7 @@ namespace smt {
mark_as_relevant(r1);
}
push_trail(add_eq_trail(r1, n1, r2->get_num_parents()));
push_trail(add_eq_trail(*this, r1, n1, r2->get_num_parents()));
m_qmanager->add_eq_eh(r1, r2);
@ -1064,7 +1048,7 @@ namespace smt {
);
DEBUG_CODE(
push_trail(push_back_trail<context, enode_pair, false>(m_diseq_vector));
push_trail(push_back_trail<enode_pair, false>(m_diseq_vector));
m_diseq_vector.push_back(enode_pair(n1, n2)););
if (r1 == r2) {
@ -1379,11 +1363,12 @@ namespace smt {
return true;
}
class set_var_theory_trail : public trail<context> {
class set_var_theory_trail : public trail {
context& ctx;
bool_var m_var;
public:
set_var_theory_trail(bool_var v):m_var(v) {}
void undo(context & ctx) override {
set_var_theory_trail(context& ctx, bool_var v): ctx(ctx), m_var(v) {}
void undo() override {
bool_var_data & d = ctx.m_bdata[m_var];
d.reset_notify_theory();
}
@ -1394,7 +1379,7 @@ namespace smt {
SASSERT(tid > 0 && tid <= 255);
SASSERT(get_intern_level(v) <= m_scope_lvl);
if (m_scope_lvl > get_intern_level(v))
push_trail(set_var_theory_trail(v));
push_trail(set_var_theory_trail(*this, v));
bool_var_data & d = m_bdata[v];
d.set_notify_theory(tid);
}
@ -1642,7 +1627,7 @@ namespace smt {
SASSERT(th);
th->new_eq_eh(curr.m_lhs, curr.m_rhs);
DEBUG_CODE(
push_trail(push_back_trail<context, new_th_eq, false>(m_propagated_th_eqs));
push_trail(push_back_trail<new_th_eq, false>(m_propagated_th_eqs));
m_propagated_th_eqs.push_back(curr););
}
m_th_eq_propagation_queue.reset();
@ -1655,7 +1640,7 @@ namespace smt {
SASSERT(th);
th->new_diseq_eh(curr.m_lhs, curr.m_rhs);
DEBUG_CODE(
push_trail(push_back_trail<context, new_th_eq, false>(m_propagated_th_diseqs));
push_trail(push_back_trail<new_th_eq, false>(m_propagated_th_diseqs));
m_propagated_th_diseqs.push_back(curr););
}
m_th_diseq_propagation_queue.reset();
@ -2997,13 +2982,15 @@ namespace smt {
assert_expr_core(e, pr);
}
class case_split_insert_trail : public trail<context> {
class case_split_insert_trail : public trail {
context& ctx;
literal l;
public:
case_split_insert_trail(literal l):
case_split_insert_trail(context& ctx, literal l):
ctx(ctx),
l(l) {
}
void undo(context & ctx) override {
void undo() override {
ctx.undo_th_case_split(l);
}
};
@ -3029,11 +3016,11 @@ namespace smt {
literal l = lits[i];
SASSERT(!m_all_th_case_split_literals.contains(l.index()));
m_all_th_case_split_literals.insert(l.index());
push_trail(case_split_insert_trail(l));
push_trail(case_split_insert_trail(*this, l));
new_case_split.push_back(l);
}
m_th_case_split_sets.push_back(new_case_split);
push_trail(push_back_vector<context, vector<literal_vector> >(m_th_case_split_sets));
push_trail(push_back_vector<vector<literal_vector> >(m_th_case_split_sets));
for (unsigned i = 0; i < num_lits; ++i) {
literal l = lits[i];
if (!m_literal2casesplitsets.contains(l.index())) {
@ -4348,17 +4335,18 @@ namespace smt {
/**
\brief Undo object for bool var m_true_first field update.
*/
class set_true_first_trail : public trail<context> {
class set_true_first_trail : public trail {
context& ctx;
bool_var m_var;
public:
set_true_first_trail(bool_var v):m_var(v) {}
void undo(context & ctx) override {
set_true_first_trail(context& ctx, bool_var v): ctx(ctx), m_var(v) {}
void undo() override {
ctx.m_bdata[m_var].reset_true_first_flag();
}
};
void context::set_true_first_flag(bool_var v) {
push_trail(set_true_first_trail(v));
push_trail(set_true_first_trail(*this, v));
bool_var_data & d = m_bdata[v];
d.set_true_first_flag();
}

60
src/smt/smt_context.h
View file

@ -110,9 +110,9 @@ namespace smt {
unsigned m_final_check_idx; // circular counter used for implementing fairness
bool m_is_auxiliary; // used to prevent unwanted information from being logged.
class parallel* m_par;
unsigned m_par_index;
bool m_is_auxiliary { false }; // used to prevent unwanted information from being logged.
class parallel* m_par { nullptr };
unsigned m_par_index { 0 };
// -----------------------------------
//
@ -151,7 +151,7 @@ namespace smt {
svector<new_th_eq> m_propagated_th_diseqs;
svector<enode_pair> m_diseq_vector;
#endif
enode * m_is_diseq_tmp; // auxiliary enode used to find congruent equality atoms.
enode * m_is_diseq_tmp { nullptr }; // auxiliary enode used to find congruent equality atoms.
tmp_enode m_tmp_enode;
ptr_vector<almost_cg_table> m_almost_cg_tables; // temporary field for is_ext_diseq
@ -180,15 +180,15 @@ namespace smt {
literal_vector m_assigned_literals;
typedef std::pair<clause*, literal_vector> tmp_clause;
vector<tmp_clause> m_tmp_clauses;
unsigned m_qhead;
unsigned m_simp_qhead;
int m_simp_counter; //!< can become negative
unsigned m_qhead { 0 };
unsigned m_simp_qhead { 0 };
int m_simp_counter { 0 }; //!< can become negative
scoped_ptr<case_split_queue> m_case_split_queue;
scoped_ptr<induction> m_induction;
double m_bvar_inc;
bool m_phase_cache_on;
unsigned m_phase_counter; //!< auxiliary variable used to decide when to turn on/off phase caching
bool m_phase_default; //!< default phase when using phase caching
double m_bvar_inc { 1.0 };
bool m_phase_cache_on { true };
unsigned m_phase_counter { 0 }; //!< auxiliary variable used to decide when to turn on/off phase caching
bool m_phase_default { false }; //!< default phase when using phase caching
// A conflict is usually a single justification. That is, a justification
// for false. If m_not_l is not null_literal, then m_conflict is a
@ -600,10 +600,10 @@ namespace smt {
//
// -----------------------------------
protected:
typedef ptr_vector<trail<context> > trail_stack;
typedef ptr_vector<trail > trail_stack;
trail_stack m_trail_stack;
#ifdef Z3DEBUG
bool m_trail_enabled;
bool m_trail_enabled { true };
#endif
public:
@ -613,15 +613,15 @@ namespace smt {
m_trail_stack.push_back(new (m_region) TrailObject(obj));
}
void push_trail_ptr(trail<context> * ptr) {
void push_trail_ptr(trail * ptr) {
m_trail_stack.push_back(ptr);
}
protected:
unsigned m_scope_lvl;
unsigned m_base_lvl;
unsigned m_search_lvl; // It is greater than m_base_lvl when assumptions are used. Otherwise, it is equals to m_base_lvl
unsigned m_scope_lvl { 0 };
unsigned m_base_lvl { 0 };
unsigned m_search_lvl { 0 }; // It is greater than m_base_lvl when assumptions are used. Otherwise, it is equals to m_base_lvl
struct scope {
unsigned m_assigned_literals_lim;
unsigned m_trail_stack_lim;
@ -724,7 +724,7 @@ namespace smt {
}
protected:
unsigned m_generation; //!< temporary variable used during internalization
unsigned m_generation { 0 }; //!< temporary variable used during internalization
public:
bool binary_clause_opt_enabled() const {
@ -793,25 +793,31 @@ namespace smt {
void internalize_uninterpreted(app * n);
friend class mk_bool_var_trail;
class mk_bool_var_trail : public trail<context> {
class mk_bool_var_trail : public trail {
context& ctx;
public:
void undo(context & ctx) override { ctx.undo_mk_bool_var(); }
mk_bool_var_trail(context& ctx) :ctx(ctx) {}
void undo() override { ctx.undo_mk_bool_var(); }
};
mk_bool_var_trail m_mk_bool_var_trail;
void undo_mk_bool_var();
friend class mk_enode_trail;
class mk_enode_trail : public trail<context> {
class mk_enode_trail : public trail {
context& ctx;
public:
void undo(context & ctx) override { ctx.undo_mk_enode(); }
mk_enode_trail(context& ctx) :ctx(ctx) {}
void undo() override { ctx.undo_mk_enode(); }
};
mk_enode_trail m_mk_enode_trail;
void undo_mk_enode();
friend class mk_lambda_trail;
class mk_lambda_trail : public trail<context> {
class mk_lambda_trail : public trail {
context& ctx;
public:
void undo(context & ctx) override { ctx.undo_mk_lambda(); }
mk_lambda_trail(context& ctx) :ctx(ctx) {}
void undo() override { ctx.undo_mk_lambda(); }
};
mk_lambda_trail m_mk_lambda_trail;
void undo_mk_lambda();
@ -970,10 +976,10 @@ namespace smt {
//
// -----------------------------------
protected:
lbool m_last_search_result;
failure m_last_search_failure;
lbool m_last_search_result { l_undef };
failure m_last_search_failure { UNKNOWN };
ptr_vector<theory> m_incomplete_theories; //!< theories that failed to produce a model
bool m_searching;
bool m_searching { false };
unsigned m_num_conflicts;
unsigned m_num_conflicts_since_restart;
unsigned m_num_conflicts_since_lemma_gc;

6
src/smt/smt_enode.cpp
View file

@ -137,7 +137,7 @@ namespace smt {
void enode::set_generation(context & ctx, unsigned generation) {
if (m_generation == generation)
return;
ctx.push_trail(value_trail<context, unsigned>(m_generation));
ctx.push_trail(value_trail<unsigned>(m_generation));
m_generation = generation;
}
@ -147,13 +147,13 @@ namespace smt {
// m_lbl_hash should be different from -1, if and only if,
// there is a pattern that contains the enode. So,
// I use a trail to restore the value of m_lbl_hash to -1.
ctx.push_trail(value_trail<context, signed char>(m_lbl_hash));
ctx.push_trail(value_trail<signed char>(m_lbl_hash));
unsigned h = hash_u(get_owner_id());
m_lbl_hash = h & (APPROX_SET_CAPACITY - 1);
// propagate modification to the root m_lbls set.
approx_set & r_lbls = m_root->m_lbls;
if (!r_lbls.may_contain(m_lbl_hash)) {
ctx.push_trail(value_trail<context, approx_set>(r_lbls));
ctx.push_trail(value_trail<approx_set>(r_lbls));
r_lbls.insert(m_lbl_hash);
}
}

2
src/smt/smt_induction.cpp
View file

@ -58,7 +58,7 @@ literal_vector collect_induction_literals::pre_select() {
}
TRACE("induction", ctx.display(tout << "literal index: " << m_literal_index << "\n" << result << "\n"););
ctx.push_trail(value_trail<context, unsigned>(m_literal_index));
ctx.push_trail(value_trail<unsigned>(m_literal_index));
m_literal_index = ctx.assigned_literals().size();
return result;
}

24
src/smt/smt_internalizer.cpp
View file

@ -701,13 +701,13 @@ namespace smt {
/**
\brief Trail object to disable the m_merge_tf flag of an enode.
*/
class set_merge_tf_trail : public trail<context> {
class set_merge_tf_trail : public trail {
enode * m_node;
public:
set_merge_tf_trail(enode * n):
m_node(n) {
}
void undo(context & ctx) override {
void undo() override {
m_node->m_merge_tf = false;
}
};
@ -747,13 +747,15 @@ namespace smt {
variable. The flag m_enode is true for a Boolean variable v,
if there is an enode n associated with it.
*/
class set_enode_flag_trail : public trail<context> {
class set_enode_flag_trail : public trail {
context& ctx;
bool_var m_var;
public:
set_enode_flag_trail(bool_var v):
set_enode_flag_trail(context& ctx, bool_var v):
ctx(ctx),
m_var(v) {
}
void undo(context & ctx) override {
void undo() override {
bool_var_data & data = ctx.m_bdata[m_var];
data.reset_enode_flag();
}
@ -770,7 +772,7 @@ namespace smt {
bool_var_data & data = m_bdata[v];
if (!data.is_enode()) {
if (!is_new_var)
push_trail(set_enode_flag_trail(v));
push_trail(set_enode_flag_trail(*this, v));
data.set_enode_flag();
}
}
@ -1681,7 +1683,7 @@ namespace smt {
/**
\brief Trail for add_th_var
*/
class add_th_var_trail : public trail<context> {
class add_th_var_trail : public trail {
enode * m_enode;
theory_id m_th_id;
#ifdef Z3DEBUG
@ -1695,7 +1697,7 @@ namespace smt {
SASSERT(m_th_var != null_theory_var);
}
void undo(context & ctx) override {
void undo() override {
theory_var v = m_enode->get_th_var(m_th_id);
SASSERT(v != null_theory_var);
SASSERT(m_th_var == v);
@ -1709,7 +1711,7 @@ namespace smt {
/**
\brief Trail for replace_th_var
*/
class replace_th_var_trail : public trail<context> {
class replace_th_var_trail : public trail {
enode * m_enode;
unsigned m_th_id:8;
unsigned m_old_th_var:24;
@ -1720,7 +1722,7 @@ namespace smt {
m_old_th_var(old_var) {
}
void undo(context & ctx) override {
void undo() override {
SASSERT(m_enode->get_th_var(m_th_id) != null_theory_var);
m_enode->replace_th_var(m_old_th_var, m_th_id);
}
@ -1762,7 +1764,7 @@ namespace smt {
SASSERT(th->get_enode(old_v) != n); // this varialbe is not owned by n
SASSERT(n->get_root()->get_th_var(th_id) != null_theory_var); // the root has also a variable in its var-list.
n->replace_th_var(v, th_id);
push_trail(replace_th_var_trail(n, th_id, old_v));
push_trail(replace_th_var_trail( n, th_id, old_v));
push_new_th_eq(th_id, v, old_v);
}
SASSERT(th->is_attached_to_var(n));

4
src/smt/smt_quantifier.cpp
View file

@ -754,7 +754,7 @@ namespace smt {
ptr_vector<enode>::const_iterator end = m_context->end_enodes();
unsigned sz = static_cast<unsigned>(end - it);
if (sz > m_new_enode_qhead) {
m_context->push_trail(value_trail<context, unsigned>(m_new_enode_qhead));
m_context->push_trail(value_trail<unsigned>(m_new_enode_qhead));
it += m_new_enode_qhead;
while (m_new_enode_qhead < sz) {
enode * e = *it;
@ -799,7 +799,7 @@ namespace smt {
if (use_ematching()) {
if (m_lazy_matching_idx < m_fparams->m_qi_max_lazy_multipattern_matching) {
m_lazy_mam->rematch();
m_context->push_trail(value_trail<context, unsigned>(m_lazy_matching_idx));
m_context->push_trail(value_trail<unsigned>(m_lazy_matching_idx));
m_lazy_matching_idx++;
}
}

4
src/smt/theory_arith_aux.h
View file

@ -2228,7 +2228,7 @@ namespace smt {
}
if (result)
ctx.push_trail(restore_size_trail<context, std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
ctx.push_trail(restore_size_trail<std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
return delayed_assume_eqs();
}
@ -2237,7 +2237,7 @@ namespace smt {
if (m_assume_eq_head == m_assume_eq_candidates.size())
return false;
ctx.push_trail(value_trail<context, unsigned>(m_assume_eq_head));
ctx.push_trail(value_trail<unsigned>(m_assume_eq_head));
while (m_assume_eq_head < m_assume_eq_candidates.size()) {
std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head];
theory_var v1 = p.first;

8
src/smt/theory_arith_core.h
View file

@ -31,7 +31,7 @@ namespace smt {
void theory_arith<Ext>::found_unsupported_op(app * n) {
if (!m_found_unsupported_op) {
TRACE("arith", tout << "found non supported expression:\n" << mk_pp(n, m) << "\n";);
ctx.push_trail(value_trail<context, bool>(m_found_unsupported_op));
ctx.push_trail(value_trail<bool>(m_found_unsupported_op));
m_found_unsupported_op = true;
}
}
@ -39,10 +39,10 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::found_underspecified_op(app * n) {
m_underspecified_ops.push_back(n);
ctx.push_trail(push_back_vector<context, ptr_vector<app>>(m_underspecified_ops));
ctx.push_trail(push_back_vector<ptr_vector<app>>(m_underspecified_ops));
if (!m_found_underspecified_op) {
TRACE("arith", tout << "found underspecified expression:\n" << mk_pp(n, m) << "\n";);
ctx.push_trail(value_trail<context, bool>(m_found_underspecified_op));
ctx.push_trail(value_trail<bool>(m_found_underspecified_op));
m_found_underspecified_op = true;
}
@ -1492,7 +1492,7 @@ namespace smt {
return FC_CONTINUE;
if (delayed_assume_eqs())
return FC_CONTINUE;
ctx.push_trail(value_trail<context, unsigned>(m_final_check_idx));
ctx.push_trail(value_trail<unsigned>(m_final_check_idx));
m_liberal_final_check = true;
m_changed_assignment = false;
final_check_status result = final_check_core();

6
src/smt/theory_arith_nl.h
View file

@ -2138,7 +2138,7 @@ void theory_arith<Ext>::update_statistics(grobner & gb) {
template<typename Ext>
void theory_arith<Ext>::set_gb_exhausted() {
IF_VERBOSE(3, verbose_stream() << "Grobner basis computation interrupted. Increase threshold using NL_ARITH_GB_THRESHOLD=<limit>\n";);
ctx.push_trail(value_trail<context, bool>(m_nl_gb_exhausted));
ctx.push_trail(value_trail<bool>(m_nl_gb_exhausted));
m_nl_gb_exhausted = true;
}
@ -2314,7 +2314,7 @@ final_check_status theory_arith<Ext>::process_non_linear() {
return FC_GIVEUP;
}
ctx.push_trail(value_trail<context, unsigned>(m_nl_rounds));
ctx.push_trail(value_trail<unsigned>(m_nl_rounds));
m_nl_rounds++;
elim_quasi_base_rows();
@ -2338,7 +2338,7 @@ final_check_status theory_arith<Ext>::process_non_linear() {
bool progress;
unsigned old_idx = m_nl_strategy_idx;
ctx.push_trail(value_trail<context, unsigned>(m_nl_strategy_idx));
ctx.push_trail(value_trail<unsigned>(m_nl_strategy_idx));
do {
progress = false;

8
src/smt/theory_array.cpp
View file

@ -90,7 +90,7 @@ namespace smt {
var_data * d = m_var_data[v];
d->m_parent_selects.push_back(s);
TRACE("array", tout << v << " " << mk_pp(s->get_owner(), m) << " " << mk_pp(get_enode(v)->get_owner(), m) << "\n";);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_selects));
m_trail_stack.push(push_back_trail<enode *, false>(d->m_parent_selects));
for (enode* n : d->m_stores) {
instantiate_axiom2a(s, n);
}
@ -111,7 +111,7 @@ namespace smt {
v = find(v);
var_data * d = m_var_data[v];
d->m_parent_stores.push_back(s);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_parent_stores));
m_trail_stack.push(push_back_trail<enode *, false>(d->m_parent_stores));
if (d->m_prop_upward && !m_params.m_array_delay_exp_axiom) {
for (enode* n : d->m_parent_selects) {
if (!m_params.m_array_cg || n->is_cgr()) {
@ -143,7 +143,7 @@ namespace smt {
return;
}
TRACE("array", tout << "#" << v << "\n";);
m_trail_stack.push(reset_flag_trail<theory_array>(d->m_prop_upward));
m_trail_stack.push(reset_flag_trail(d->m_prop_upward));
d->m_prop_upward = true;
if (!m_params.m_array_delay_exp_axiom)
instantiate_axiom2b_for(v);
@ -186,7 +186,7 @@ namespace smt {
set_prop_upward(v, d);
}
d->m_stores.push_back(s);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d->m_stores));
m_trail_stack.push(push_back_trail<enode *, false>(d->m_stores));
for (enode * n : d->m_parent_selects) {
SASSERT(is_select(n));
instantiate_axiom2a(n, s);

10
src/smt/theory_array_bapa.cpp
View file

@ -278,8 +278,8 @@ namespace smt {
if (tns == sz2) {
std::cout << "SEEN " << smt << "\n";
}
ctx().push_trail(value_trail<context, bool>(i1.m_is_leaf, false));
ctx().push_trail(value_trail<context, bool>(i2.m_is_leaf, false));
ctx().push_trail(value_trail<bool>(i1.m_is_leaf, false));
ctx().push_trail(value_trail<bool>(i2.m_is_leaf, false));
expr_ref k1(m), k2(m), k3(m);
expr_ref sz_tms(m), sz_tns(m), sz_smt(m);
k1 = m_autil.mk_card(tms);
@ -332,7 +332,7 @@ namespace smt {
}
literal lit = mk_eq(sz, m_arith.mk_int(value));
if (lit != true_literal && is_true(lit)) {
ctx().push_trail(value_trail<context, rational>(i.m_size, value));
ctx().push_trail(value_trail<rational>(i.m_size, value));
continue;
}
ctx().set_true_first_flag(lit.var());
@ -442,14 +442,14 @@ namespace smt {
return l_true;
}
class remove_sz : public trail<context> {
class remove_sz : public trail {
ast_manager& m;
obj_map<app, sz_info*> & m_table;
app* m_obj;
public:
remove_sz(ast_manager& m, obj_map<app, sz_info*>& tab, app* t): m(m), m_table(tab), m_obj(t) { }
~remove_sz() override {}
void undo(context& ctx) override { m.dec_ref(m_obj); dealloc(m_table[m_obj]); m_table.remove(m_obj); }
void undo() override { m.dec_ref(m_obj); dealloc(m_table[m_obj]); m_table.remove(m_obj); }
};
std::ostream& display(std::ostream& out) {

6
src/smt/theory_array_base.cpp
View file

@ -34,14 +34,14 @@ namespace smt {
}
void theory_array_base::add_weak_var(theory_var v) {
ctx.push_trail(push_back_vector<context, svector<theory_var>>(m_array_weak_trail));
ctx.push_trail(push_back_vector<svector<theory_var>>(m_array_weak_trail));
m_array_weak_trail.push_back(v);
}
void theory_array_base::found_unsupported_op(expr * n) {
if (!ctx.get_fparams().m_array_fake_support && !m_found_unsupported_op) {
TRACE("array", tout << mk_ll_pp(n, m) << "\n";);
ctx.push_trail(value_trail<context, bool>(m_found_unsupported_op));
ctx.push_trail(value_trail<bool>(m_found_unsupported_op));
m_found_unsupported_op = true;
}
}
@ -430,7 +430,7 @@ namespace smt {
m_extensionality_todo.reset();
m_congruent_todo.reset();
if (!ctx.get_fparams().m_array_weak && has_propagate_up_trail()) {
ctx.push_trail(value_trail<context, unsigned>(m_array_weak_head));
ctx.push_trail(value_trail<unsigned>(m_array_weak_head));
for (; m_array_weak_head < m_array_weak_trail.size(); ++m_array_weak_head) {
set_prop_upward(m_array_weak_trail[m_array_weak_head]);
}

14
src/smt/theory_array_full.cpp
View file

@ -54,7 +54,7 @@ namespace smt {
// instead apply stratified filter.
set_prop_upward(v,d);
d_full->m_maps.push_back(s);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d_full->m_maps));
m_trail_stack.push(push_back_trail<enode *, false>(d_full->m_maps));
for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) {
enode* n = d->m_parent_selects[i];
SASSERT(is_select(n));
@ -88,7 +88,7 @@ namespace smt {
var_data * d = m_var_data[v];
var_data_full * d_full = m_var_data_full[v];
d_full->m_parent_maps.push_back(s);
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(d_full->m_parent_maps));
m_trail_stack.push(push_back_trail<enode *, false>(d_full->m_parent_maps));
if (!m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) {
enode * n = d->m_parent_selects[i];
@ -110,7 +110,7 @@ namespace smt {
add_weak_var(v);
return;
}
m_trail_stack.push(reset_flag_trail<theory_array>(d->m_prop_upward));
m_trail_stack.push(reset_flag_trail(d->m_prop_upward));
d->m_prop_upward = true;
TRACE("array", tout << "#" << v << "\n";);
if (!m_params.m_array_delay_exp_axiom) {
@ -171,7 +171,7 @@ namespace smt {
set_prop_upward(v, d);
}
ptr_vector<enode> & consts = m_var_data_full[v]->m_consts;
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(consts));
m_trail_stack.push(push_back_trail<enode *, false>(consts));
consts.push_back(cnst);
instantiate_default_const_axiom(cnst);
for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) {
@ -188,7 +188,7 @@ namespace smt {
set_prop_upward(v, d);
}
ptr_vector<enode> & as_arrays = m_var_data_full[v]->m_as_arrays;
m_trail_stack.push(push_back_trail<theory_array, enode *, false>(as_arrays));
m_trail_stack.push(push_back_trail<enode *, false>(as_arrays));
as_arrays.push_back(arr);
instantiate_default_as_array_axiom(arr);
for (unsigned i = 0; i < d->m_parent_selects.size(); ++i) {
@ -744,11 +744,11 @@ namespace smt {
func_decl* diag = nullptr;
if (!m_sort2epsilon.find(s, eps)) {
eps = m.mk_fresh_const("epsilon", s);
m_trail_stack.push(ast2ast_trail<theory_array, sort, app>(m_sort2epsilon, s, eps));
m_trail_stack.push(ast2ast_trail<sort, app>(m_sort2epsilon, s, eps));
}
if (!m_sort2diag.find(s, diag)) {
diag = m.mk_fresh_func_decl("diag", 1, &s, s);
m_trail_stack.push(ast2ast_trail<theory_array, sort, func_decl>(m_sort2diag, s, diag));
m_trail_stack.push(ast2ast_trail<sort, func_decl>(m_sort2diag, s, diag));
}
return std::make_pair(eps, diag);
}

25
src/smt/theory_bv.cpp
View file

@ -72,11 +72,12 @@ namespace smt {
}
class mk_atom_trail : public trail<theory_bv> {
class mk_atom_trail : public trail {
theory_bv& th;
bool_var m_var;
public:
mk_atom_trail(bool_var v):m_var(v) {}
void undo(theory_bv & th) override {
mk_atom_trail(theory_bv& th, bool_var v):th(th), m_var(v) {}
void undo() override {
theory_bv::atom * a = th.get_bv2a(m_var);
a->~atom();
th.erase_bv2a(m_var);
@ -123,7 +124,7 @@ namespace smt {
ctx.set_var_theory(bv, get_id());
bit_atom * a = new (get_region()) bit_atom();
insert_bv2a(bv, a);
m_trail_stack.push(mk_atom_trail(bv));
m_trail_stack.push(mk_atom_trail(*this, bv));
unsigned idx = n->get_decl()->get_parameter(0).get_int();
SASSERT(a->m_occs == 0);
a->m_occs = new (get_region()) var_pos_occ(v_arg, idx);
@ -212,11 +213,11 @@ namespace smt {
get_bits(ctx.get_enode(arg), r);
}
class add_var_pos_trail : public trail<theory_bv> {
class add_var_pos_trail : public trail {
theory_bv::bit_atom * m_atom;
public:
add_var_pos_trail(theory_bv::bit_atom * a):m_atom(a) {}
void undo(theory_bv & th) override {
void undo() override {
SASSERT(m_atom->m_occs);
m_atom->m_occs = m_atom->m_occs->m_next;
}
@ -226,7 +227,7 @@ namespace smt {
if (!params().m_bv_eq_axioms)
return;
m_prop_diseqs.push_back(bv_diseq(v1, v2, idx));
ctx.push_trail(push_back_vector<context, svector<bv_diseq>>(m_prop_diseqs));
ctx.push_trail(push_back_vector<svector<bv_diseq>>(m_prop_diseqs));
}
/**
@ -302,7 +303,7 @@ namespace smt {
SASSERT(ctx.get_var_theory(l.var()) == get_id());
bit_atom * b = new (get_region()) bit_atom();
insert_bv2a(l.var(), b);
m_trail_stack.push(mk_atom_trail(l.var()));
m_trail_stack.push(mk_atom_trail(*this, l.var()));
SASSERT(b->m_occs == 0);
b->m_occs = new (get_region()) var_pos_occ(v, idx);
}
@ -947,7 +948,7 @@ namespace smt {
ctx.set_var_theory(l.var(), get_id()); \
le_atom * a = new (get_region()) le_atom(l, def); /* abuse le_atom */ \
insert_bv2a(l.var(), a); \
m_trail_stack.push(mk_atom_trail(l.var())); \
m_trail_stack.push(mk_atom_trail(*this, l.var())); \
/* smul_no_overflow and umul_no_overflow are using the le_atom (THIS IS A BIG HACK)... */ \
/* the connection between the l and def was never realized when */ \
/* relevancy() is true and m_bv_lazy_le is false (the default configuration). */ \
@ -983,7 +984,7 @@ namespace smt {
ctx.set_var_theory(l.var(), get_id());
le_atom * a = new (get_region()) le_atom(l, def);
insert_bv2a(l.var(), a);
m_trail_stack.push(mk_atom_trail(l.var()));
m_trail_stack.push(mk_atom_trail(*this, l.var()));
if (!ctx.relevancy() || !params().m_bv_lazy_le) {
ctx.mk_th_axiom(get_id(), l, ~def);
ctx.mk_th_axiom(get_id(), ~l, def);
@ -1090,7 +1091,7 @@ namespace smt {
if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > params().m_bv_blast_max_size) {
if (!m_approximates_large_bvs) {
TRACE("bv", tout << "found large size bit-vector:\n" << mk_pp(n, m) << "\n";);
ctx.push_trail(value_trail<context, bool>(m_approximates_large_bvs));
ctx.push_trail(value_trail<bool>(m_approximates_large_bvs));
m_approximates_large_bvs = true;
}
return true;
@ -1577,7 +1578,7 @@ namespace smt {
void theory_bv::propagate() {
if (!can_propagate())
return;
ctx.push_trail(value_trail<context, unsigned>(m_prop_diseqs_qhead));
ctx.push_trail(value_trail<unsigned>(m_prop_diseqs_qhead));
for (; m_prop_diseqs_qhead < m_prop_diseqs.size() && !ctx.inconsistent(); ++m_prop_diseqs_qhead) {
auto p = m_prop_diseqs[m_prop_diseqs_qhead];
assert_new_diseq_axiom(p.v1, p.v2, p.idx);

4
src/smt/theory_char.cpp
View file

@ -30,7 +30,7 @@ namespace smt {
m_bits2char = symbol("bits2char");
}
struct theory_char::reset_bits : public trail<context> {
struct theory_char::reset_bits : public trail {
theory_char& s;
unsigned idx;
@ -39,7 +39,7 @@ namespace smt {
idx(idx)
{}
void undo(context& ctx) override {
void undo() override {
s.m_bits[idx].reset();
s.m_ebits[idx].reset();
}

4
src/smt/theory_datatype.cpp
View file

@ -794,7 +794,7 @@ namespace smt {
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, 1, &p)));
}
if (d1->m_constructor == nullptr) {
m_trail_stack.push(set_ptr_trail<theory_datatype, enode>(d1->m_constructor));
m_trail_stack.push(set_ptr_trail<enode>(d1->m_constructor));
// check whether there is a recognizer in d1 that conflicts with d2->m_constructor;
if (!d1->m_recognizers.empty()) {
unsigned c_idx = m_util.get_constructor_idx(d2->m_constructor->get_decl());
@ -847,7 +847,7 @@ namespace smt {
}
SASSERT(val == l_undef || (val == l_false && d->m_constructor == 0));
d->m_recognizers[c_idx] = recognizer;
m_trail_stack.push(set_vector_idx_trail<theory_datatype, enode>(d->m_recognizers, c_idx));
m_trail_stack.push(set_vector_idx_trail<enode>(d->m_recognizers, c_idx));
if (val == l_false) {
propagate_recognizer(v, recognizer);
}

2
src/smt/theory_dense_diff_logic_def.h
View file

@ -124,7 +124,7 @@ namespace smt {
void theory_dense_diff_logic<Ext>::found_non_diff_logic_expr(expr * n) {
if (!m_non_diff_logic_exprs) {
TRACE("non_diff_logic", tout << "found non diff logic expression:\n" << mk_pp(n, m) << "\n";);
ctx.push_trail(value_trail<context, bool>(m_non_diff_logic_exprs));
ctx.push_trail(value_trail<bool>(m_non_diff_logic_exprs));
IF_VERBOSE(0, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";);
m_non_diff_logic_exprs = true;
}

4
src/smt/theory_diff_logic_def.h
View file

@ -171,7 +171,7 @@ void theory_diff_logic<Ext>::found_non_diff_logic_expr(expr * n) {
if (!m_non_diff_logic_exprs) {
TRACE("non_diff_logic", tout << "found non diff logic expression:\n" << mk_pp(n, m) << "\n";);
IF_VERBOSE(0, verbose_stream() << "(smt.diff_logic: non-diff logic expression " << mk_pp(n, m) << ")\n";);
ctx.push_trail(value_trail<context, bool>(m_non_diff_logic_exprs));
ctx.push_trail(value_trail<bool>(m_non_diff_logic_exprs));
m_non_diff_logic_exprs = true;
}
}
@ -557,7 +557,7 @@ void theory_diff_logic<Ext>::propagate() {
template<typename Ext>
void theory_diff_logic<Ext>::inc_conflicts() {
ctx.push_trail(value_trail<context, bool>(m_consistent));
ctx.push_trail(value_trail<bool>(m_consistent));
m_consistent = false;
m_stats.m_num_conflicts++;
if (m_params.m_arith_adaptive) {

6
src/smt/theory_dl.cpp
View file

@ -209,8 +209,8 @@ namespace smt {
m_vals.insert(s, v);
add_trail(r);
add_trail(v);
ctx.push_trail(insert_obj_map<context,sort,func_decl*>(m_reps, s));
ctx.push_trail(insert_obj_map<context,sort,func_decl*>(m_vals, s));
ctx.push_trail(insert_obj_map<sort,func_decl*>(m_reps, s));
ctx.push_trail(insert_obj_map<sort,func_decl*>(m_vals, s));
}
}
@ -283,7 +283,7 @@ namespace smt {
void add_trail(ast* a) {
m_trail.push_back(a);
ctx.push_trail(push_back_vector<context,ast_ref_vector>(m_trail));
ctx.push_trail(push_back_vector<ast_ref_vector>(m_trail));
}
};

2
src/smt/theory_dummy.cpp
View file

@ -24,7 +24,7 @@ namespace smt {
void theory_dummy::found_theory_expr() {
if (!m_theory_exprs) {
get_context().push_trail(value_trail<context, bool>(m_theory_exprs));
get_context().push_trail(value_trail<bool>(m_theory_exprs));
m_theory_exprs = true;
}
}

2
src/smt/theory_fpa.cpp
View file

@ -188,7 +188,7 @@ namespace smt {
m_conversions.insert(e, res);
m.inc_ref(e);
m.inc_ref(res);
m_trail_stack.push(insert_ref2_map<theory_fpa, ast_manager, expr, expr>(m, m_conversions, e, res.get()));
m_trail_stack.push(insert_ref2_map<ast_manager, expr, expr>(m, m_conversions, e, res.get()));
}
return res;

12
src/smt/theory_lra.cpp
View file

@ -298,7 +298,7 @@ class theory_lra::imp {
}
void found_unsupported(expr* n) {
ctx().push_trail(value_trail<context, expr*>(m_not_handled));
ctx().push_trail(value_trail<expr*>(m_not_handled));
TRACE("arith", tout << "unsupported " << mk_pp(n, m) << "\n";);
m_not_handled = n;
}
@ -733,7 +733,7 @@ class theory_lra::imp {
void updt_unassigned_bounds(theory_var v, int inc) {
TRACE("arith", tout << "v" << v << " " << m_unassigned_bounds[v] << " += " << inc << "\n";);
ctx().push_trail(vector_value_trail<smt::context, unsigned, false>(m_unassigned_bounds, v));
ctx().push_trail(vector_value_trail<unsigned, false>(m_unassigned_bounds, v));
m_unassigned_bounds[v] += inc;
}
@ -1422,7 +1422,7 @@ public:
void init_variable_values() {
m_model_is_initialized = false;
if (m.inc() && m_solver.get() && th.get_num_vars() > 0) {
ctx().push_trail(value_trail<smt::context, bool>(m_model_is_initialized));
ctx().push_trail(value_trail<bool>(m_model_is_initialized));
m_model_is_initialized = lp().init_model();
TRACE("arith", display(tout << "update variable values " << m_model_is_initialized << "\n"););
}
@ -1507,7 +1507,7 @@ public:
}
if (num_candidates > 0) {
ctx().push_trail(restore_size_trail<context, std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
ctx().push_trail(restore_size_trail<std::pair<theory_var, theory_var>, false>(m_assume_eq_candidates, old_sz));
}
return delayed_assume_eqs();
@ -1517,7 +1517,7 @@ public:
if (m_assume_eq_head == m_assume_eq_candidates.size())
return false;
ctx().push_trail(value_trail<context, unsigned>(m_assume_eq_head));
ctx().push_trail(value_trail<unsigned>(m_assume_eq_head));
while (m_assume_eq_head < m_assume_eq_candidates.size()) {
std::pair<theory_var, theory_var> const & p = m_assume_eq_candidates[m_assume_eq_head];
theory_var v1 = p.first;
@ -2960,7 +2960,7 @@ public:
if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) {
TRACE("arith", tout << "tighter bound " << tv.to_string() << "\n";);
m_history.push_back(vec[ti]);
ctx().push_trail(history_trail<context, constraint_bound>(vec, ti, m_history));
ctx().push_trail(history_trail<constraint_bound>(vec, ti, m_history));
b.first = ci;
b.second = v;
}

14
src/smt/theory_pb.cpp
View file

@ -1093,11 +1093,11 @@ namespace smt {
return lits;
}
class theory_pb::negate_ineq : public trail<context> {
class theory_pb::negate_ineq : public trail {
ineq& c;
public:
negate_ineq(ineq& c): c(c) {}
void undo(context& ctx) override {
void undo() override {
c.negate();
}
};
@ -1111,9 +1111,9 @@ namespace smt {
void theory_pb::assign_ineq(ineq& c, bool is_true) {
m_mpz_trail.push_back(c.m_max_sum);
m_mpz_trail.push_back(c.m_min_sum);
ctx.push_trail(scoped_value_trail<context, scoped_mpz, scoped_mpz_vector>(c.m_max_sum, m_mpz_trail));
ctx.push_trail(scoped_value_trail<context, scoped_mpz, scoped_mpz_vector>(c.m_min_sum, m_mpz_trail));
ctx.push_trail(value_trail<context, unsigned>(c.m_nfixed));
ctx.push_trail(scoped_value_trail<scoped_mpz, scoped_mpz_vector>(c.m_max_sum, m_mpz_trail));
ctx.push_trail(scoped_value_trail<scoped_mpz, scoped_mpz_vector>(c.m_min_sum, m_mpz_trail));
ctx.push_trail(value_trail<unsigned>(c.m_nfixed));
SASSERT(c.is_ge());
unsigned sz = c.size();
@ -1437,13 +1437,13 @@ namespace smt {
c.m_min_sum.reset();
}
class theory_pb::unwatch_ge : public trail<context> {
class theory_pb::unwatch_ge : public trail {
theory_pb& pb;
ineq& c;
public:
unwatch_ge(theory_pb& p, ineq& c): pb(p), c(c) {}
void undo(context& ctx) override {
void undo() override {
for (unsigned i = 0; i < c.watch_size(); ++i) {
pb.unwatch_literal(c.lit(i), &c);
}

32
src/smt/theory_seq.cpp
View file

@ -476,7 +476,7 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
return false;
}
m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_fixed, e));
m_trail_stack.push(insert_obj_trail<expr>(m_fixed, e));
m_fixed.insert(e);
expr_ref seq(e, m), head(m), tail(m);
@ -501,7 +501,7 @@ bool theory_seq::fixed_length(expr* len_e, bool is_zero) {
return false;
add_axiom(~a, b);
if (!ctx.at_base_level()) {
m_trail_stack.push(push_replay(alloc(replay_fixed_length, m, len_e)));
m_trail_stack.push(push_replay(*this, alloc(replay_fixed_length, m, len_e)));
}
return true;
}
@ -620,7 +620,7 @@ bool theory_seq::check_lts() {
return false;
}
unsigned sz = m_lts.size();
m_trail_stack.push(value_trail<theory_seq, bool>(m_lts_checked));
m_trail_stack.push(value_trail<bool>(m_lts_checked));
m_lts_checked = true;
expr* a = nullptr, *b = nullptr, *c = nullptr, *d = nullptr;
bool is_strict1, is_strict2;
@ -941,7 +941,7 @@ bool theory_seq::solve_itos(expr* n, expr_ref_vector const& rs, dependency* dep)
for (expr* r : rs) {
if (m_util.str.is_unit(r, u) && !m_is_digit.contains(u)) {
m_is_digit.insert(u);
m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_is_digit, u));
m_trail_stack.push(insert_obj_trail<expr>(m_is_digit, u));
literal is_digit = m_ax.is_digit(u);
if (ctx.get_assignment(is_digit) != l_true) {
propagate_lit(dep, 0, nullptr, is_digit);
@ -1508,8 +1508,8 @@ void theory_seq::add_length(expr* e, expr* l) {
SASSERT(!m_has_length.contains(l));
m_length.push_back(l);
m_has_length.insert(e);
m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_has_length, e));
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_length));
m_trail_stack.push(insert_obj_trail<expr>(m_has_length, e));
m_trail_stack.push(push_back_vector<expr_ref_vector>(m_length));
}
/**
@ -1529,11 +1529,11 @@ void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
}
m_length_limit_map.insert(s, k);
m_length_limit.push_back(lim_e);
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_length_limit));
m_trail_stack.push(push_back_vector<expr_ref_vector>(m_length_limit));
if (k0 != 0) {
m_trail_stack.push(remove_obj_map<theory_seq, expr, unsigned>(m_length_limit_map, s, k0));
m_trail_stack.push(remove_obj_map<expr, unsigned>(m_length_limit_map, s, k0));
}
m_trail_stack.push(insert_obj_map<theory_seq, expr, unsigned>(m_length_limit_map, s));
m_trail_stack.push(insert_obj_map<expr, unsigned>(m_length_limit_map, s));
if (is_searching) {
expr_ref dlimit = m_sk.mk_max_unfolding_depth(m_max_unfolding_depth);
add_axiom(~mk_literal(dlimit), mk_literal(lim_e));
@ -1564,7 +1564,7 @@ bool theory_seq::add_length_to_eqc(expr* e) {
void theory_seq::add_int_string(expr* e) {
m_int_string.push_back(e);
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_int_string));
m_trail_stack.push(push_back_vector<expr_ref_vector>(m_int_string));
}
bool theory_seq::check_int_string() {
@ -2514,8 +2514,8 @@ void theory_seq::enque_axiom(expr* e) {
TRACE("seq", tout << "add axiom " << mk_bounded_pp(e, m) << "\n";);
m_axioms.push_back(e);
m_axiom_set.insert(e);
m_trail_stack.push(push_back_vector<theory_seq, expr_ref_vector>(m_axioms));
m_trail_stack.push(insert_obj_trail<theory_seq, expr>(m_axiom_set, e));;
m_trail_stack.push(push_back_vector<expr_ref_vector>(m_axioms));
m_trail_stack.push(insert_obj_trail<expr>(m_axiom_set, e));;
}
}
@ -2524,7 +2524,7 @@ void theory_seq::deque_axiom(expr* n) {
if (m_util.str.is_length(n)) {
m_ax.add_length_axiom(n);
if (!ctx.at_base_level()) {
m_trail_stack.push(push_replay(alloc(replay_axiom, m, n)));
m_trail_stack.push(push_replay(*this, alloc(replay_axiom, m, n)));
}
}
else if (m_util.str.is_empty(n) && !has_length(n) && !m_has_length.empty()) {
@ -3034,7 +3034,7 @@ void theory_seq::push_scope_eh() {
m_exclude.push_scope();
m_dm.push_scope();
m_trail_stack.push_scope();
m_trail_stack.push(value_trail<theory_seq, unsigned>(m_axioms_head));
m_trail_stack.push(value_trail<unsigned>(m_axioms_head));
m_eqs.push_scope();
m_nqs.push_scope();
m_ncs.push_scope();
@ -3108,7 +3108,7 @@ void theory_seq::relevant_eh(app* n) {
void theory_seq::add_unhandled_expr(expr* n) {
if (!m_unhandled_expr) {
ctx.push_trail(value_trail<context, expr*>(m_unhandled_expr));
ctx.push_trail(value_trail<expr*>(m_unhandled_expr));
m_unhandled_expr = n;
}
}
@ -3118,7 +3118,7 @@ void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {
if (m_has_seq) {
TRACE("seq", tout << "add_theory_assumption\n";);
expr_ref dlimit = m_sk.mk_max_unfolding_depth(m_max_unfolding_depth);
m_trail_stack.push(value_trail<theory_seq, literal>(m_max_unfolding_lit));
m_trail_stack.push(value_trail<literal>(m_max_unfolding_lit));
m_max_unfolding_lit = mk_literal(dlimit);
assumptions.push_back(dlimit);
for (auto const& kv : m_length_limit_map) {

14
src/smt/theory_seq.h
View file

@ -281,20 +281,22 @@ namespace smt {
}
};
class push_replay : public trail<theory_seq> {
class push_replay : public trail {
theory_seq& th;
apply* m_apply;
public:
push_replay(apply* app): m_apply(app) {}
void undo(theory_seq& th) override {
push_replay(theory_seq& th, apply* app): th(th), m_apply(app) {}
void undo() override {
th.m_replay.push_back(m_apply);
}
};
class pop_branch : public trail<theory_seq> {
class pop_branch : public trail {
theory_seq& th;
unsigned k;
public:
pop_branch(unsigned k): k(k) {}
void undo(theory_seq& th) override {
pop_branch(theory_seq& th, unsigned k): th(th), k(k) {}
void undo() override {
th.m_branch_start.erase(k);
}
};

2
src/smt/theory_seq_empty.h
View file

@ -28,7 +28,7 @@ namespace smt {
class theory_seq_empty : public theory {
bool m_used;
final_check_status final_check_eh() override { return m_used?FC_GIVEUP:FC_DONE; }
bool internalize_atom(app*, bool) override { if (!m_used) { get_context().push_trail(value_trail<context,bool>(m_used)); m_used = true; } return false; }
bool internalize_atom(app*, bool) override { if (!m_used) { get_context().push_trail(value_trail<bool>(m_used)); m_used = true; } return false; }
bool internalize_term(app*) override { return internalize_atom(nullptr,false); }
void new_eq_eh(theory_var, theory_var) override { }
void new_diseq_eh(theory_var, theory_var) override {}

18
src/smt/theory_str.cpp
View file

@ -6827,12 +6827,12 @@ namespace smt {
m_concat_eval_todo.push_back(n);
} else if (u.str.is_at(ap) || u.str.is_extract(ap) || u.str.is_replace(ap)) {
m_library_aware_axiom_todo.push_back(n);
m_library_aware_trail_stack.push(push_back_trail<theory_str, enode*, false>(m_library_aware_axiom_todo));
m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo));
} else if (u.str.is_itos(ap)) {
TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;);
string_int_conversion_terms.push_back(ap);
m_library_aware_axiom_todo.push_back(n);
m_library_aware_trail_stack.push(push_back_trail<theory_str, enode*, false>(m_library_aware_axiom_todo));
m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo));
} else if (is_var(ex)) {
// if ex is a variable, add it to our list of variables
TRACE("str", tout << "tracking variable " << mk_ismt2_pp(ap, get_manager()) << std::endl;);
@ -6858,7 +6858,7 @@ namespace smt {
app * ap = to_app(ex);
if (u.str.is_prefix(ap) || u.str.is_suffix(ap) || u.str.is_contains(ap) || u.str.is_in_re(ap)) {
m_library_aware_axiom_todo.push_back(n);
m_library_aware_trail_stack.push(push_back_trail<theory_str, enode*, false>(m_library_aware_axiom_todo));
m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo));
}
}
} else {
@ -6878,12 +6878,12 @@ namespace smt {
app * ap = to_app(ex);
if (u.str.is_index(ap)) {
m_library_aware_axiom_todo.push_back(n);
m_library_aware_trail_stack.push(push_back_trail<theory_str, enode*, false>(m_library_aware_axiom_todo));
m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo));
} else if (u.str.is_stoi(ap)) {
TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;);
string_int_conversion_terms.push_back(ap);
m_library_aware_axiom_todo.push_back(n);
m_library_aware_trail_stack.push(push_back_trail<theory_str, enode*, false>(m_library_aware_axiom_todo));
m_library_aware_trail_stack.push(push_back_trail<enode*, false>(m_library_aware_axiom_todo));
}
}
} else {
@ -8151,7 +8151,7 @@ namespace smt {
if (!string_int_axioms.contains(axiom)) {
string_int_axioms.insert(axiom);
assert_axiom(axiom);
m_trail_stack.push(insert_obj_trail<theory_str, expr>(string_int_axioms, axiom));
m_trail_stack.push(insert_obj_trail<expr>(string_int_axioms, axiom));
axiomAdd = true;
}
} else {
@ -8185,7 +8185,7 @@ namespace smt {
if (!string_int_axioms.contains(axiom)) {
string_int_axioms.insert(axiom);
assert_axiom(axiom);
m_trail_stack.push(insert_obj_trail<theory_str, expr>(string_int_axioms, axiom));
m_trail_stack.push(insert_obj_trail<expr>(string_int_axioms, axiom));
axiomAdd = true;
}
} else {
@ -8195,7 +8195,7 @@ namespace smt {
if (!string_int_axioms.contains(axiom)) {
string_int_axioms.insert(axiom);
assert_axiom(axiom);
m_trail_stack.push(insert_obj_trail<theory_str, expr>(string_int_axioms, axiom));
m_trail_stack.push(insert_obj_trail<expr>(string_int_axioms, axiom));
axiomAdd = true;
}
}
@ -8239,7 +8239,7 @@ namespace smt {
if (!string_int_axioms.contains(axiom)) {
string_int_axioms.insert(axiom);
assert_axiom(axiom);
m_trail_stack.push(insert_obj_trail<theory_str, expr>(string_int_axioms, axiom));
m_trail_stack.push(insert_obj_trail<expr>(string_int_axioms, axiom));
axiomAdd = true;
}
} else {

4
src/smt/theory_str.h
View file

@ -86,14 +86,14 @@ public:
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {};
template<typename Ctx>
class binary_search_trail : public trail<Ctx> {
class binary_search_trail : public trail {
obj_map<expr, ptr_vector<expr> > & target;
expr * entry;
public:
binary_search_trail(obj_map<expr, ptr_vector<expr> > & target, expr * entry) :
target(target), entry(entry) {}
~binary_search_trail() override {}
void undo(Ctx & ctx) override {
void undo() override {
TRACE("t_str_binary_search", tout << "in binary_search_trail::undo()" << std::endl;);
if (target.contains(entry)) {
if (!target[entry].empty()) {

4
src/smt/theory_str_regex.cpp
View file

@ -107,7 +107,7 @@ namespace smt {
}
regex_terms_with_length_constraints.insert(str_in_re);
m_trail_stack.push(insert_obj_trail<theory_str, expr>(regex_terms_with_length_constraints, str_in_re));
m_trail_stack.push(insert_obj_trail<expr>(regex_terms_with_length_constraints, str_in_re));
regex_axiom_add = true;
}
} // re not in regex_terms_with_length_constraints
@ -179,7 +179,7 @@ namespace smt {
expr_ref rhs(ctx.mk_eq_atom(str, mk_string("")), m);
assert_implication(lhs, rhs);
regex_terms_with_path_constraints.insert(str_in_re);
m_trail_stack.push(insert_obj_trail<theory_str, expr>(regex_terms_with_path_constraints, str_in_re));
m_trail_stack.push(insert_obj_trail<expr>(regex_terms_with_path_constraints, str_in_re));
} else {
TRACE("str", tout << "zero-length solution not admitted by this automaton -- asserting conflict clause" << std::endl;);
expr_ref_vector lhs_terms(m);

4
src/smt/theory_utvpi_def.h
View file

@ -190,7 +190,7 @@ namespace smt {
template<typename Ext>
void theory_utvpi<Ext>::inc_conflicts() {
ctx.push_trail(value_trail<context, bool>(m_consistent));
ctx.push_trail(value_trail<bool>(m_consistent));
m_consistent = false;
m_stats.m_num_conflicts++;
if (m_params.m_arith_adaptive) {
@ -238,7 +238,7 @@ namespace smt {
auto str = msg.str();
TRACE("utvpi", tout << str;);
warning_msg("%s", str.c_str());
ctx.push_trail(value_trail<context, bool>(m_non_utvpi_exprs));
ctx.push_trail(value_trail<bool>(m_non_utvpi_exprs));
m_non_utvpi_exprs = true;
}

6
src/smt/theory_wmaxsat.cpp
View file

@ -161,8 +161,8 @@ namespace smt {
scoped_mpz w(m_mpz);
w = m_zweights[tv];
ctx.push_trail(numeral_trail(m_zcost, m_old_values));
ctx.push_trail(push_back_vector<context, svector<theory_var> >(m_costs));
ctx.push_trail(value_trail<context, bool>(m_assigned[tv]));
ctx.push_trail(push_back_vector<svector<theory_var> >(m_costs));
ctx.push_trail(value_trail<bool>(m_assigned[tv]));
m_zcost += w;
TRACE("opt", tout << "Assign v" << tv << " weight: " << w << " cost: " << m_zcost << " " << mk_pp(m_vars[m_bool2var[v]].get(), get_manager()) << "\n";);
m_costs.push_back(tv);
@ -299,7 +299,7 @@ namespace smt {
}
//
if (max_unassigned > m_max_unassigned_index) {
ctx.push_trail(value_trail<context, unsigned>(m_max_unassigned_index));
ctx.push_trail(value_trail<unsigned>(m_max_unassigned_index));
m_max_unassigned_index = max_unassigned;
}
if (max_unassigned < m_sorted_vars.size() &&

4
src/smt/theory_wmaxsat.h
View file

@ -64,7 +64,7 @@ namespace smt {
rational get_cost();
void init_min_cost(rational const& r);
class numeral_trail : public trail<context> {
class numeral_trail : public trail {
typedef scoped_mpz T;
T & m_value;
scoped_mpz_vector& m_old_values;
@ -78,7 +78,7 @@ namespace smt {
~numeral_trail() override {
}
void undo(context & ctx) override {
void undo() override {
m_value = m_old_values.back();
m_old_values.shrink(m_old_values.size() - 1);
}

4
src/smt/user_propagator.cpp
View file

@ -84,7 +84,7 @@ void user_propagator::new_fixed_eh(theory_var v, expr* value, unsigned num_lits,
if (m_fixed.contains(v))
return;
m_fixed.insert(v);
ctx.push_trail(insert_map<context, uint_set, unsigned>(m_fixed, v));
ctx.push_trail(insert_map<uint_set, unsigned>(m_fixed, v));
m_id2justification.setx(v, literal_vector(num_lits, jlits), literal_vector());
m_fixed_eh(m_user_context, this, v, value);
}
@ -142,7 +142,7 @@ void user_propagator::propagate() {
++m_stats.m_num_propagations;
++qhead;
}
ctx.push_trail(value_trail<context, unsigned>(m_qhead));
ctx.push_trail(value_trail<unsigned>(m_qhead));
m_qhead = qhead;
}

159
src/util/trail.h
View file

@ -23,16 +23,16 @@ Revision History:
#include "util/obj_ref.h"
#include "util/vector.h"
template<typename Ctx>
class trail {
public:
virtual ~trail() {
}
virtual void undo(Ctx & ctx) = 0;
virtual void undo() = 0;
};
template<typename Ctx, typename T>
class value_trail : public trail<Ctx> {
template<typename T>
class value_trail : public trail {
T & m_value;
T m_old_value;
@ -51,15 +51,15 @@ public:
~value_trail() override {
}
void undo(Ctx & ctx) override {
void undo() override {
m_value = m_old_value;
}
};
template<typename Ctx, typename T, typename Ts>
class scoped_value_trail : public trail<Ctx> {
template<typename T, typename Ts>
class scoped_value_trail : public trail {
T & m_value;
Ts & m_values;
@ -72,15 +72,14 @@ public:
~scoped_value_trail() override {
}
void undo(Ctx & ctx) override {
void undo() override {
m_value = m_values.back();
m_values.pop_back();
}
};
template<typename Ctx>
class reset_flag_trail : public trail<Ctx> {
class reset_flag_trail : public trail {
bool & m_value;
public:
reset_flag_trail(bool & value):
@ -90,13 +89,13 @@ public:
~reset_flag_trail() override {
}
void undo(Ctx & ctx) override {
void undo() override {
m_value = false;
}
};
template<typename Ctx, typename T>
class set_ptr_trail : public trail<Ctx> {
template<typename T>
class set_ptr_trail : public trail {
T * & m_ptr;
public:
set_ptr_trail(T * & ptr):
@ -104,13 +103,13 @@ public:
SASSERT(m_ptr == 0);
}
void undo(Ctx & ctx) override {
void undo() override {
m_ptr = nullptr;
}
};
template<typename Ctx, typename T, bool CallDestructors=true>
class restore_size_trail : public trail<Ctx> {
template<typename T, bool CallDestructors=true>
class restore_size_trail : public trail {
vector<T, CallDestructors> & m_vector;
unsigned m_old_size;
public:
@ -124,13 +123,13 @@ public:
}
~restore_size_trail() override {
}
void undo(Ctx & ctx) override {
void undo() override {
m_vector.shrink(m_old_size);
}
};
template<typename Ctx, typename T, bool CallDestructors=true>
class vector_value_trail : public trail<Ctx> {
template<typename T, bool CallDestructors=true>
class vector_value_trail : public trail {
vector<T, CallDestructors> & m_vector;
unsigned m_idx;
T m_old_value;
@ -144,13 +143,13 @@ public:
~vector_value_trail() override {
}
void undo(Ctx & ctx) override {
void undo() override {
m_vector[m_idx] = m_old_value;
}
};
template<typename Ctx, typename V, typename T>
class vector2_value_trail : public trail<Ctx> {
template<typename V, typename T>
class vector2_value_trail : public trail {
V & m_vector;
unsigned m_i;
unsigned m_j;
@ -166,57 +165,57 @@ public:
~vector2_value_trail() override {
}
void undo(Ctx & ctx) override {
void undo() override {
m_vector[m_i][m_j] = m_old_value;
}
};
template<typename Ctx, typename D, typename R>
class insert_obj_map : public trail<Ctx> {
template<typename D, typename R>
class insert_obj_map : public trail {
obj_map<D,R>& m_map;
D* m_obj;
public:
insert_obj_map(obj_map<D,R>& t, D* o) : m_map(t), m_obj(o) {}
~insert_obj_map() override {}
void undo(Ctx & ctx) override { m_map.remove(m_obj); }
void undo() override { m_map.remove(m_obj); }
};
template<typename Ctx, typename D, typename R>
class remove_obj_map : public trail<Ctx> {
template<typename D, typename R>
class remove_obj_map : public trail {
obj_map<D,R>& m_map;
D* m_obj;
R m_value;
public:
remove_obj_map(obj_map<D,R>& t, D* o, R v) : m_map(t), m_obj(o), m_value(v) {}
~remove_obj_map() override {}
void undo(Ctx & ctx) override { m_map.insert(m_obj, m_value); }
void undo() override { m_map.insert(m_obj, m_value); }
};
template<typename Ctx, typename M, typename D>
class insert_map : public trail<Ctx> {
template<typename M, typename D>
class insert_map : public trail {
M& m_map;
D m_obj;
public:
insert_map(M& t, D o) : m_map(t), m_obj(o) {}
~insert_map() override {}
void undo(Ctx & ctx) override { m_map.remove(m_obj); }
void undo() override { m_map.remove(m_obj); }
};
template<typename Ctx, typename M, typename Mgr, typename D>
class insert_ref_map : public trail<Ctx> {
template<typename M, typename Mgr, typename D>
class insert_ref_map : public trail {
Mgr& m;
M& m_map;
D m_obj;
public:
insert_ref_map(Mgr& m, M& t, D o) : m(m), m_map(t), m_obj(o) {}
virtual ~insert_ref_map() {}
virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); }
virtual void undo() { m_map.remove(m_obj); m.dec_ref(m_obj); }
};
template<typename Ctx, typename Mgr, typename D, typename R>
class insert_ref2_map : public trail<Ctx> {
template<typename Mgr, typename D, typename R>
class insert_ref2_map : public trail {
Mgr& m;
obj_map<D,R*>& m_map;
D* m_obj;
@ -224,25 +223,25 @@ class insert_ref2_map : public trail<Ctx> {
public:
insert_ref2_map(Mgr& m, obj_map<D,R*>& t, D*o, R*r) : m(m), m_map(t), m_obj(o), m_val(r) {}
virtual ~insert_ref2_map() {}
virtual void undo(Ctx & ctx) { m_map.remove(m_obj); m.dec_ref(m_obj); m.dec_ref(m_val); }
virtual void undo() { m_map.remove(m_obj); m.dec_ref(m_obj); m.dec_ref(m_val); }
};
template<typename Ctx, typename V>
class push_back_vector : public trail<Ctx> {
template<typename V>
class push_back_vector : public trail {
V & m_vector;
public:
push_back_vector(V & v):
m_vector(v) {
}
void undo(Ctx & ctx) override {
void undo() override {
m_vector.pop_back();
}
};
template<typename Ctx, typename T>
class set_vector_idx_trail : public trail<Ctx> {
template<typename T>
class set_vector_idx_trail : public trail {
ptr_vector<T> & m_vector;
unsigned m_idx;
public:
@ -254,13 +253,13 @@ public:
~set_vector_idx_trail() override {
}
void undo(Ctx & ctx) override {
void undo() override {
m_vector[m_idx] = 0;
}
};
template<typename Ctx, typename T, bool CallDestructors=true>
class pop_back_trail : public trail<Ctx> {
template<typename T, bool CallDestructors=true>
class pop_back_trail : public trail {
vector<T, CallDestructors> & m_vector;
T m_value;
public:
@ -269,13 +268,13 @@ public:
m_value(m_vector.back()) {
}
virtual void undo(Ctx & ctx) {
virtual void undo() {
m_vector.push_back(m_value);
}
};
template<typename Ctx, typename T, bool CallDestructors=true>
class pop_back2_trail : public trail<Ctx> {
template<typename T, bool CallDestructors=true>
class pop_back2_trail : public trail {
vector<T, CallDestructors> & m_vector;
typedef vector<vector<T, CallDestructors>, true> vector_t;
unsigned m_index;
@ -287,28 +286,28 @@ public:
m_value(m_vector[index].back()) {
}
virtual void undo(Ctx & ctx) {
virtual void undo() {
m_vector[m_index].push_back(m_value);
}
};
template<typename Ctx, typename T, bool CallDestructors=true>
class push_back_trail : public trail<Ctx> {
template<typename T, bool CallDestructors=true>
class push_back_trail : public trail {
vector<T, CallDestructors> & m_vector;
public:
push_back_trail(vector<T, CallDestructors> & v):
m_vector(v) {
}
void undo(Ctx & ctx) override {
void undo() override {
m_vector.pop_back();
}
};
template<typename Ctx, typename T, bool CallDestructors=true>
class push_back2_trail : public trail<Ctx> {
template<typename T, bool CallDestructors=true>
class push_back2_trail : public trail {
typedef vector<vector<T, CallDestructors>, true> vector_t;
vector_t & m_vector;
unsigned m_index;
@ -318,13 +317,13 @@ public:
m_index(index) {
}
virtual void undo(Ctx & ctx) {
virtual void undo() {
m_vector[m_index].pop_back();
}
};
template<typename Ctx>
class set_bitvector_trail : public trail<Ctx> {
class set_bitvector_trail : public trail {
bool_vector & m_vector;
unsigned m_idx;
public:
@ -335,14 +334,14 @@ public:
m_vector[m_idx] = true;
}
void undo(Ctx & ctx) override {
void undo() override {
m_vector[m_idx] = false;
}
};
template<typename Ctx, typename T, bool CallDestructors = true>
class history_trail : public trail<Ctx> {
template<typename T, bool CallDestructors = true>
class history_trail : public trail {
vector<T, CallDestructors>& m_dst;
unsigned m_idx;
vector<T, CallDestructors>& m_hist;
@ -355,69 +354,69 @@ public:
~history_trail() override {
}
void undo(Ctx& ctx) override {
void undo() override {
m_dst[m_idx] = m_hist.back();
m_hist.pop_back();
}
};
template<typename Ctx, typename T>
class new_obj_trail : public trail<Ctx> {
template<typename T>
class new_obj_trail : public trail {
T * m_obj;
public:
new_obj_trail(T * obj):
m_obj(obj) {
}
void undo(Ctx & ctx) override {
void undo() override {
dealloc(m_obj);
}
};
template<typename Ctx, typename M, typename T>
class obj_ref_trail : public trail<Ctx> {
template<typename M, typename T>
class obj_ref_trail : public trail {
obj_ref<T,M> m_obj;
public:
obj_ref_trail(obj_ref<T,M>& obj):
m_obj(obj) {
}
virtual void undo(Ctx & ctx) {
virtual void undo() {
m_obj.reset();
}
};
template<typename Ctx, typename T>
class insert_obj_trail : public trail<Ctx> {
template<typename T>
class insert_obj_trail : public trail {
obj_hashtable<T>& m_table;
T* m_obj;
public:
insert_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
~insert_obj_trail() override {}
void undo(Ctx & ctx) override { m_table.remove(m_obj); }
void undo() override { m_table.remove(m_obj); }
};
template<typename Ctx, typename T>
class remove_obj_trail : public trail<Ctx> {
template<typename T>
class remove_obj_trail : public trail {
obj_hashtable<T>& m_table;
T* m_obj;
public:
remove_obj_trail(obj_hashtable<T>& t, T* o) : m_table(t), m_obj(o) {}
virtual ~remove_obj_trail() {}
virtual void undo(Ctx & ctx) { m_table.insert(m_obj); }
virtual void undo() { m_table.insert(m_obj); }
};
template<typename Ctx>
void undo_trail_stack(Ctx & ctx, ptr_vector<trail<Ctx> > & s, unsigned old_size) {
void undo_trail_stack(Ctx & ctx, ptr_vector<trail> & s, unsigned old_size) {
SASSERT(old_size <= s.size());
typename ptr_vector<trail<Ctx> >::iterator begin = s.begin() + old_size;
typename ptr_vector<trail<Ctx> >::iterator it = s.end();
typename ptr_vector<trail >::iterator begin = s.begin() + old_size;
typename ptr_vector<trail >::iterator it = s.end();
while (it != begin) {
--it;
(*it)->undo(ctx);
(*it)->undo();
}
s.shrink(old_size);
}
@ -425,7 +424,7 @@ void undo_trail_stack(Ctx & ctx, ptr_vector<trail<Ctx> > & s, unsigned old_size)
template<typename Ctx>
class trail_stack {
Ctx & m_ctx;
ptr_vector<trail<Ctx> > m_trail_stack;
ptr_vector<trail> m_trail_stack;
unsigned_vector m_scopes;
region m_region;
public:
@ -441,7 +440,7 @@ public:
undo_trail_stack(m_ctx, m_trail_stack, 0);
}
void push_ptr(trail<Ctx> * t) { m_trail_stack.push_back(t); }
void push_ptr(trail * t) { m_trail_stack.push_back(t); }
template<typename TrailObject>
void push(TrailObject const & obj) { m_trail_stack.push_back(new (m_region) TrailObject(obj)); }

8
src/util/union_find.h
View file

@ -47,12 +47,12 @@ class union_find {
class mk_var_trail;
friend class mk_var_trail;
class mk_var_trail : public trail<StackCtx> {
class mk_var_trail : public trail {
union_find & m_owner;
public:
mk_var_trail(union_find & o):m_owner(o) {}
~mk_var_trail() override {}
void undo(StackCtx& ctx) override {
void undo() override {
m_owner.m_find.pop_back();
m_owner.m_size.pop_back();
m_owner.m_next.pop_back();
@ -64,13 +64,13 @@ class union_find {
class merge_trail;
friend class merge_trail;
class merge_trail : public trail<StackCtx> {
class merge_trail : public trail {
union_find & m_owner;
unsigned m_r1;
public:
merge_trail(union_find & o, unsigned r1):m_owner(o), m_r1(r1) {}
~merge_trail() override {}
void undo(StackCtx& ctx) override { m_owner.unmerge(m_r1); }
void undo() override { m_owner.unmerge(m_r1); }
};
void unmerge(unsigned r1) {