mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-05 23:43:59 +00:00
Code Activity

Merge branch 'master' into polysat

Browse source
This commit is contained in:
Jakob Rath 2022-08-01 11:27:49 +02:00
commit 220a63e8bd
223 changed files with 508 additions and 505 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/arith_eq_adapter.cpp
View file

@ -67,8 +67,6 @@ namespace smt {
m_ge(ge) {
}
~arith_eq_relevancy_eh() override {}
void operator()(relevancy_propagator & rp) override {
if (!rp.is_relevant(m_n1))
return;

1
src/smt/database.h
View file

@ -3,6 +3,7 @@
Copyright (c) 2015 Microsoft Corporation
--*/
#pragma once
static char const g_pattern_database[] =
"(benchmark patterns \n"

1
src/smt/dyn_ack.cpp
View file

@ -346,7 +346,6 @@ namespace smt {
dyn_ack_clause_del_eh(dyn_ack_manager & m):
m(m) {
}
~dyn_ack_clause_del_eh() override {}
void operator()(ast_manager & _m, clause * cls) override {
m.del_clause_eh(cls);
dealloc(this);

1
src/smt/proto_model/proto_model.h
View file

@ -59,7 +59,6 @@ class proto_model : public model_core {
public:
proto_model(ast_manager & m, params_ref const & p = params_ref());
~proto_model() override {}
void register_factory(value_factory * f) { m_factories.register_plugin(f); }

4
src/smt/smt_case_split_queue.cpp
View file

@ -150,8 +150,6 @@ namespace {
if (!first)
out << "\n";
}
~act_case_split_queue() override {};
};
/**
@ -1244,8 +1242,6 @@ namespace {
out << "\n";
}
~theory_aware_branching_queue() override {};
};
}

3
src/smt/smt_context.cpp
View file

@ -821,6 +821,8 @@ namespace smt {
SASSERT(t2 != null_theory_id);
theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t2) : r1->get_th_var(t2);
TRACE("merge_theory_vars", tout << get_theory(t2)->get_name() << ": " << v2 << " == " << v1 << "\n");
if (v1 != null_theory_var) {
// only send the equality to the theory, if the equality was not propagated by it.
if (t2 != from_th)
@ -839,6 +841,7 @@ namespace smt {
SASSERT(v1 != null_theory_var);
SASSERT(t1 != null_theory_id);
theory_var v2 = r2->get_th_var(t1);
TRACE("merge_theory_vars", tout << get_theory(t1)->get_name() << ": " << v2 << " == " << v1 << "\n");
if (v2 == null_theory_var) {
r2->add_th_var(v1, t1, m_region);
push_new_th_diseqs(r2, v1, get_theory(t1));

2
src/smt/smt_for_each_relevant_expr.h
View file

@ -92,7 +92,6 @@ namespace smt {
for_each_relevant_expr(ctx),
m_buffer(b) {
}
~collect_relevant_label_lits() override {}
void operator()(expr * n) override;
};
@ -103,7 +102,6 @@ namespace smt {
for_each_relevant_expr(ctx),
m_buffer(b) {
}
~collect_relevant_labels() override {}
void operator()(expr * n) override;
};

3
src/smt/smt_justification.h
View file

@ -239,7 +239,6 @@ namespace smt {
unsigned num_params, parameter* params):
simple_justification(r, num_lits, lits),
m_th_id(fid), m_params(num_params, params) {}
~simple_theory_justification() override {}
bool has_del_eh() const override { return !m_params.empty(); }
@ -323,8 +322,6 @@ namespace smt {
unsigned num_eqs, enode_pair const * eqs,
unsigned num_params = 0, parameter* params = nullptr):
ext_simple_justification(r, num_lits, lits, num_eqs, eqs), m_th_id(fid), m_params(num_params, params) {}
~ext_theory_simple_justification() override {}
bool has_del_eh() const override { return !m_params.empty(); }

8
src/smt/smt_model_finder.cpp
View file

@ -464,7 +464,7 @@ namespace smt {
m.limit().inc();
}
virtual ~auf_solver() {
~auf_solver() override {
flush_nodes();
reset_eval_cache();
}
@ -1180,7 +1180,6 @@ namespace smt {
unsigned m_var_j;
public:
f_var(ast_manager& m, func_decl* f, unsigned i, unsigned j) : qinfo(m), m_f(f), m_arg_i(i), m_var_j(j) {}
~f_var() override {}
char const* get_kind() const override {
return "f_var";
@ -1261,7 +1260,6 @@ namespace smt {
f_var(m, f, i, j),
m_offset(offset, m) {
}
~f_var_plus_offset() override {}
char const* get_kind() const override {
return "f_var_plus_offset";
@ -1427,7 +1425,6 @@ namespace smt {
public:
select_var(ast_manager& m, app* s, unsigned i, unsigned j) :qinfo(m), m_array(m), m_select(s), m_arg_i(i), m_var_j(j) {}
~select_var() override {}
char const* get_kind() const override {
return "select_var";
@ -1497,8 +1494,6 @@ namespace smt {
std::swap(m_var_i, m_var_j);
}
~var_pair() override {}
bool is_equal(qinfo const* qi) const override {
if (qi->get_kind() != get_kind())
return false;
@ -1577,7 +1572,6 @@ namespace smt {
var_expr_pair(ast_manager& m, unsigned i, expr* t) :
qinfo(m),
m_var_i(i), m_t(t, m) {}
~var_expr_pair() override {}
bool is_equal(qinfo const* qi) const override {
if (qi->get_kind() != get_kind())

3
src/smt/smt_quantifier.cpp
View file

@ -606,9 +606,6 @@ namespace smt {
m_active(false) {
}
~default_qm_plugin() override {
}
void set_manager(quantifier_manager & qm) override {
SASSERT(m_qm == nullptr);
m_qm = &qm;

4
src/smt/smt_relevancy.cpp
View file

@ -52,7 +52,6 @@ namespace smt {
app * m_parent;
public:
and_relevancy_eh(app * p):m_parent(p) {}
~and_relevancy_eh() override {}
void operator()(relevancy_propagator & rp) override;
};
@ -60,7 +59,6 @@ namespace smt {
app * m_parent;
public:
or_relevancy_eh(app * p):m_parent(p) {}
~or_relevancy_eh() override {}
void operator()(relevancy_propagator & rp) override;
};
@ -68,7 +66,6 @@ namespace smt {
app * m_parent;
public:
ite_relevancy_eh(app * p):m_parent(p) {}
~ite_relevancy_eh() override {}
void operator()(relevancy_propagator & rp) override;
};
@ -78,7 +75,6 @@ namespace smt {
app * m_else_eq;
public:
ite_term_relevancy_eh(app * p, app * then_eq, app * else_eq):m_parent(p), m_then_eq(then_eq), m_else_eq(else_eq) {}
~ite_term_relevancy_eh() override {}
void operator()(relevancy_propagator & rp) override;
};

4
src/smt/theory_arith.h
View file

@ -319,7 +319,6 @@ namespace smt {
public:
atom(bool_var bv, theory_var v, inf_numeral const & k, atom_kind kind);
atom_kind get_atom_kind() const { return static_cast<atom_kind>(m_atom_kind); }
~atom() override {}
inline inf_numeral const & get_k() const { return m_k; }
bool_var get_bool_var() const { return m_bvar; }
bool is_true() const { return m_is_true; }
@ -341,7 +340,6 @@ namespace smt {
m_rhs(rhs) {
SASSERT(m_lhs->get_root() == m_rhs->get_root());
}
~eq_bound() override {}
bool has_justification() const override { return true; }
void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) override {
SASSERT(m_lhs->get_root() == m_rhs->get_root());
@ -357,7 +355,6 @@ namespace smt {
friend class theory_arith;
public:
derived_bound(theory_var v, inf_numeral const & val, bound_kind k):bound(v, val, k, false) {}
~derived_bound() override {}
literal_vector const& lits() const { return m_lits; }
eq_vector const& eqs() const { return m_eqs; }
bool has_justification() const override { return true; }
@ -374,7 +371,6 @@ namespace smt {
friend class theory_arith;
public:
justified_derived_bound(theory_var v, inf_numeral const & val, bound_kind k):derived_bound(v, val, k) {}
~justified_derived_bound() override {}
bool has_justification() const override { return true; }
void push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) override;
void push_lit(literal l, numeral const& coeff) override;

1
src/smt/theory_array_bapa.cpp
View file

@ -450,7 +450,6 @@ namespace smt {
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() override { m.dec_ref(m_obj); dealloc(m_table[m_obj]); m_table.remove(m_obj); }
};

2
src/smt/theory_array_base.cpp
View file

@ -890,8 +890,6 @@ namespace smt {
m_unspecified_else(true) {
}
~array_value_proc() override {}
void add_entry(unsigned num_args, enode * const * args, enode * value) {
SASSERT(num_args > 0);
SASSERT(m_dim == 0 || m_dim == num_args);

2
src/smt/theory_bv.h
View file

@ -56,7 +56,6 @@ namespace smt {
struct bit_atom : public atom {
var_pos_occ * m_occs;
bit_atom():m_occs(nullptr) {}
~bit_atom() override {}
bool is_bit() const override { return true; }
};
@ -64,7 +63,6 @@ namespace smt {
literal m_var;
literal m_def;
le_atom(literal v, literal d):m_var(v), m_def(d) {}
~le_atom() override {}
bool is_bit() const override { return false; }
};

1
src/smt/theory_datatype.cpp
View file

@ -823,7 +823,6 @@ namespace smt {
public:
datatype_value_proc(func_decl * d):m_constructor(d) {}
void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); }
~datatype_value_proc() override {}
void get_dependencies(buffer<model_value_dependency> & result) override {
result.append(m_dependencies.size(), m_dependencies.data());
}

1
src/smt/theory_dummy.h
View file

@ -46,7 +46,6 @@ namespace smt {
public:
theory_dummy(context& ctx, family_id fid, char const * name);
~theory_dummy() override {}
theory * mk_fresh(context * new_ctx) override { return alloc(theory_dummy, *new_ctx, get_family_id(), m_name); }

3
src/smt/theory_fpa.h
View file

@ -47,8 +47,6 @@ namespace smt {
m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util),
m_ebits(ebits), m_sbits(sbits) {}
~fpa_value_proc() override {}
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
void get_dependencies(buffer<model_value_dependency> & result) override {
@ -75,7 +73,6 @@ namespace smt {
result.append(m_deps);
}
~fpa_rm_value_proc() override {}
app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
};

3
src/smt/theory_lra.cpp
View file

@ -1113,7 +1113,7 @@ public:
}
{
scoped_trace_stream ts(th, dgez, neg);
mk_axiom( dgez, neg);
mk_axiom( dgez, neg);
}
}
@ -1224,7 +1224,6 @@ public:
return;
}
expr_ref mod_r(a.mk_add(a.mk_mul(q, div), mod), m);
ctx().get_rewriter()(mod_r);
expr_ref eq_r(th.mk_eq_atom(mod_r, p), m);
ctx().internalize(eq_r, false);
literal eq = ctx().get_literal(eq_r);

1
src/smt/theory_pb.h
View file

@ -19,6 +19,7 @@ Notes:
It performs unit propagation and switches to creating
sorting circuits if it keeps having to propagate (create new clauses).
--*/
#pragma once
#include "smt/smt_theory.h"
#include "ast/pb_decl_plugin.h"

1
src/smt/theory_seq.cpp
View file

@ -1923,7 +1923,6 @@ public:
seq_value_proc(theory_seq& th, enode* n, sort* s): th(th), m_node(n), m_sort(s) {
(void)m_node;
}
~seq_value_proc() override {}
void add_unit(enode* n) {
m_dependencies.push_back(model_value_dependency(n));
m_source.push_back(unit_source);

5
src/smt/theory_seq.h
View file

@ -230,7 +230,6 @@ namespace smt {
expr_ref m_e;
public:
replay_length_coherence(ast_manager& m, expr* e) : m_e(e, m) {}
~replay_length_coherence() override {}
void operator()(theory_seq& th) override {
th.check_length_coherence(m_e);
m_e.reset();
@ -241,7 +240,6 @@ namespace smt {
expr_ref m_e;
public:
replay_fixed_length(ast_manager& m, expr* e) : m_e(e, m) {}
~replay_fixed_length() override {}
void operator()(theory_seq& th) override {
th.fixed_length(m_e, false, false);
m_e.reset();
@ -252,7 +250,6 @@ namespace smt {
expr_ref m_e;
public:
replay_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
~replay_axiom() override {}
void operator()(theory_seq& th) override {
th.enque_axiom(m_e);
m_e.reset();
@ -264,7 +261,6 @@ namespace smt {
bool m_sign;
public:
replay_unit_literal(ast_manager& m, expr* e, bool sign) : m_e(e, m), m_sign(sign) {}
~replay_unit_literal() override {}
void operator()(theory_seq& th) override {
literal lit = th.mk_literal(m_e);
if (m_sign) lit.neg();
@ -278,7 +274,6 @@ namespace smt {
expr_ref m_e;
public:
replay_is_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
~replay_is_axiom() override {}
void operator()(theory_seq& th) override {
th.check_int_string(m_e);
m_e.reset();

2
src/smt/theory_str.h
View file

@ -51,7 +51,6 @@ public:
str_value_factory(ast_manager & m, family_id fid) :
value_factory(m, fid),
u(m), delim("!"), m_next(0) {}
~str_value_factory() override {}
expr * get_some_value(sort * s) override {
return u.str.mk_string("some value");
}
@ -93,7 +92,6 @@ class binary_search_trail : public trail {
public:
binary_search_trail(obj_map<expr, ptr_vector<expr> > & target, expr * entry) :
target(target), entry(entry) {}
~binary_search_trail() override {}
void undo() override {
TRACE("t_str_binary_search", tout << "in binary_search_trail::undo()" << std::endl;);
if (target.contains(entry)) {

12
src/smt/theory_str_regex.cpp
View file

@ -724,8 +724,7 @@ namespace smt {
unsigned cx = estimate_regex_complexity(sub1);
return _qadd(lo, cx);
} else if (u.re.is_range(re, sub1, sub2)) {
SASSERT(u.str.is_string(sub1));
SASSERT(u.str.is_string(sub2));
if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals");
zstring str1, str2;
u.str.is_string(sub1, str1);
u.str.is_string(sub2, str2);
@ -767,8 +766,7 @@ namespace smt {
unsigned cx = estimate_regex_complexity_under_complement(sub1);
return _qmul(2, cx);
} else if (u.re.is_range(re, sub1, sub2)) {
SASSERT(u.str.is_string(sub1));
SASSERT(u.str.is_string(sub2));
if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals");
zstring str1, str2;
u.str.is_string(sub1, str1);
u.str.is_string(sub2, str2);
@ -874,8 +872,7 @@ namespace smt {
// this is bad -- term generation requires this not to appear
lens.reset();
} else if (u.re.is_range(re, sub1, sub2)) {
SASSERT(u.str.is_string(sub1));
SASSERT(u.str.is_string(sub2));
if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals");
zstring str1, str2;
u.str.is_string(sub1, str1);
u.str.is_string(sub2, str2);
@ -1006,8 +1003,7 @@ namespace smt {
SASSERT(retval);
return retval;
} else if (u.re.is_range(re, sub1, sub2)) {
SASSERT(u.str.is_string(sub1));
SASSERT(u.str.is_string(sub2));
if (!u.re.is_range(re, lo, hi)) throw default_exception("regular expressions must be built from string literals");
zstring str1, str2;
u.str.is_string(sub1, str1);
u.str.is_string(sub2, str2);

16
src/smt/theory_user_propagator.cpp
View file

@ -146,7 +146,9 @@ final_check_status theory_user_propagator::final_check_eh() {
catch (...) {
throw default_exception("Exception thrown in \"final\"-callback");
}
CTRACE("user_propagate", can_propagate(), tout << "can propagate\n");
propagate();
CTRACE("user_propagate", ctx.inconsistent(), tout << "inconsistent\n");
// check if it became inconsistent or something new was propagated/registered
bool done = (sz1 == m_prop.size()) && (sz2 == m_expr2var.size()) && !ctx.inconsistent();
return done ? FC_DONE : FC_CONTINUE;
@ -298,13 +300,17 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) {
m_eqs.reset();
for (expr* id : prop.m_ids)
m_lits.append(m_id2justification[expr2var(id)]);
for (auto const& p : prop.m_eqs)
m_eqs.push_back(enode_pair(get_enode(expr2var(p.first)), get_enode(expr2var(p.second))));
DEBUG_CODE(for (auto const& p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()););
for (auto const& [a,b] : prop.m_eqs)
if (a != b)
m_eqs.push_back(enode_pair(get_enode(expr2var(a)), get_enode(expr2var(b))));
DEBUG_CODE(for (auto const& [a, b] : m_eqs) VERIFY(a->get_root() == b->get_root()););
DEBUG_CODE(for (expr* e : prop.m_ids) VERIFY(m_fixed.contains(expr2var(e))););
DEBUG_CODE(for (literal lit : m_lits) VERIFY(ctx.get_assignment(lit) == l_true););
TRACE("user_propagate", tout << "propagating #" << prop.m_conseq->get_id() << ": " << prop.m_conseq << "\n");
TRACE("user_propagate", tout << "propagating #" << prop.m_conseq->get_id() << ": " << prop.m_conseq << "\n";
for (auto const& [a,b] : m_eqs) tout << enode_pp(a, ctx) << " == " << enode_pp(b, ctx) << "\n";
for (expr* e : prop.m_ids) tout << mk_pp(e, m) << "\n";
for (literal lit : m_lits) tout << lit << "\n");
if (m.is_false(prop.m_conseq)) {
js = ctx.mk_justification(
@ -341,9 +347,9 @@ void theory_user_propagator::propagate_new_fixed(prop_info const& prop) {
void theory_user_propagator::propagate() {
TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n");
if (m_qhead == m_prop.size() && m_to_add_qhead == m_to_add.size())
return;
TRACE("user_propagate", tout << "propagating queue head: " << m_qhead << " prop queue: " << m_prop.size() << "\n");
force_push();
unsigned qhead = m_to_add_qhead;

5
src/smt/theory_user_propagator.h
View file

@ -140,10 +140,11 @@ namespace smt {
bool get_case_split(bool_var& var, bool& is_pos);
theory * mk_fresh(context * new_ctx) override;
char const* get_name() const override { return "user_propagate"; }
bool internalize_atom(app* atom, bool gate_ctx) override;
bool internalize_term(app* term) override;
void new_eq_eh(theory_var v1, theory_var v2) override { if (m_eq_eh) m_eq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); }
void new_diseq_eh(theory_var v1, theory_var v2) override { if (m_diseq_eh) m_diseq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); }
void new_eq_eh(theory_var v1, theory_var v2) override { force_push(); if (m_eq_eh) m_eq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); }
void new_diseq_eh(theory_var v1, theory_var v2) override { force_push(); if (m_diseq_eh) m_diseq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); }
bool use_diseqs() const override { return ((bool)m_diseq_eh); }
bool build_models() const override { return false; }
final_check_status final_check_eh() override;

5
src/smt/theory_wmaxsat.h
View file

@ -74,10 +74,7 @@ namespace smt {
m_old_values(old) {
old.push_back(value);
}
~numeral_trail() override {
}
void undo() override {
m_value = m_old_values.back();
m_old_values.shrink(m_old_values.size() - 1);