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

fix #3758

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-05 12:01:17 -07:00
parent 1949a978ce
commit efc02282f4
3 changed files with 56 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_dense_diff_logic.h
View file

@ -162,7 +162,7 @@ namespace smt {
struct var_value_eq {
theory_dense_diff_logic & m_th;
var_value_eq(theory_dense_diff_logic & th):m_th(th) {}
bool operator()(theory_var v1, theory_var v2) const { return m_th.m_assignment[v1] == m_th.m_assignment[v2] && m_th.is_int(v1) == m_th.is_int(v2); }
bool operator()(theory_var v1, theory_var v2) const { return m_th.m_assignment[v1] == m_th.m_assignment[v2]; }
};
typedef int_hashtable<var_value_hash, var_value_eq> var_value_table;

27
src/smt/theory_utvpi.h
View file

@ -159,6 +159,25 @@ namespace smt {
arith_factory * m_factory;
rational m_delta;
struct var_value_hash;
friend struct var_value_hash;
struct var_value_hash {
theory_utvpi & m_th;
var_value_hash(theory_utvpi & th):m_th(th) {}
unsigned operator()(theory_var v) const { return m_th.mk_value(v, false).hash(); }
};
struct var_value_eq;
friend struct var_value_eq;
struct var_value_eq {
theory_utvpi & m_th;
var_value_eq(theory_utvpi & th):m_th(th) {}
bool operator()(theory_var v1, theory_var v2) const { return m_th.mk_value(v1, false) == m_th.mk_value(v2, false) && m_th.is_int(v1) == m_th.is_int(v2); }
};
typedef int_hashtable<var_value_hash, var_value_eq> var_value_table;
var_value_table m_var_value_table;
// Set a conflict due to a negative cycle.
void set_conflict();
@ -257,6 +276,10 @@ namespace smt {
private:
void init_model();
bool assume_eqs_core();
rational mk_value(theory_var v, bool is_int);
bool is_parity_ok(unsigned v) const;
@ -271,6 +294,8 @@ namespace smt {
bool check_z_consistency();
bool has_shared();
virtual void new_eq_eh(th_var v1, th_var v2, justification& j) {
m_stats.m_num_core2th_eqs++;
new_eq_or_diseq(true, v1, v2, j);
@ -299,6 +324,8 @@ namespace smt {
void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
bool is_int(theory_var v) const { return a.is_int(get_enode(v)->get_owner()); }
th_var get_zero(sort* s) { return a.is_int(s) ? m_izero : m_rzero; }
th_var get_zero(expr* e) { return get_zero(get_manager().get_sort(e)); }

29
src/smt/theory_utvpi_def.h
View file

@ -69,6 +69,7 @@ namespace smt {
m_lia(false),
m_lra(false),
m_non_utvpi_exprs(false),
m_var_value_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
m_test(m),
m_factory(nullptr) {
}
@ -203,7 +204,7 @@ namespace smt {
inc_conflicts();
literal_vector const& lits = m_nc_functor.get_lits();
context & ctx = get_context();
IF_VERBOSE(2, ctx.display_literals_smt2(verbose_stream() << "conflict:\n", lits));
IF_VERBOSE(20, ctx.display_literals_smt2(verbose_stream() << "conflict:\n", lits));
TRACE("utvpi", ctx.display_literals_smt2(tout << "conflict:\n", lits););
if (m_params.m_arith_dump_lemmas) {
@ -410,6 +411,9 @@ namespace smt {
else if (!check_z_consistency()) {
return FC_CONTINUE;
}
else if (has_shared() && assume_eqs_core()) {
return FC_CONTINUE;
}
else if (m_non_utvpi_exprs) {
return FC_GIVEUP;
}
@ -418,6 +422,17 @@ namespace smt {
}
}
template<typename Ext>
bool theory_utvpi<Ext>::has_shared() {
auto sz = static_cast<theory_var>(get_num_vars());
for (theory_var v = 0; v < sz; ++v) {
if (is_relevant_and_shared(get_enode(v)))
return true;
}
return false;
}
template<typename Ext>
bool theory_utvpi<Ext>::check_z_consistency() {
int_vector scc_id;
@ -789,6 +804,11 @@ namespace smt {
void theory_utvpi<Ext>::init_model(model_generator & m) {
m_factory = alloc(arith_factory, get_manager());
m.register_factory(m_factory);
init_model();
}
template<typename Ext>
void theory_utvpi<Ext>::init_model() {
enforce_parity();
init_zero();
dl_var vs[4] = { to_var(m_izero), neg(to_var(m_izero)), to_var(m_rzero), neg(to_var(m_rzero)) };
@ -797,6 +817,13 @@ namespace smt {
DEBUG_CODE(model_validate(););
}
template<typename Ext>
bool theory_utvpi<Ext>::assume_eqs_core() {
init_model();
return assume_eqs(m_var_value_table);
}
template<typename Ext>
void theory_utvpi<Ext>::model_validate() {
context& ctx = get_context();