mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix #3945

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-13 10:46:41 -07:00
parent 5c4f775b1b
commit 5dafd1fe25
3 changed files with 31 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/diff_logic.h
View file

@ -371,7 +371,9 @@ private:
SASSERT(m_gamma[target].is_neg());
acc_assignment(target, gamma);
TRACE("arith", display(tout << id << "\n"););
TRACE("arith", display(tout << id << " " << gamma << "\n");
display_edge(tout, last_e);
);
dl_var source = target;
while (true) {

10
src/smt/theory_diff_logic.h
View file

@ -164,6 +164,8 @@ namespace smt {
};
typedef dl_graph<GExt> Graph;
enum lia_or_lra { not_set, is_lia, is_lra };
smt_params & m_params;
arith_util m_util;
arith_eq_adapter m_arith_eq_adapter;
@ -175,7 +177,7 @@ namespace smt {
ptr_vector<eq_prop_info> m_eq_prop_infos;
app_ref_vector m_terms;
bool_vector m_signs;
bool_vector m_signs;
ptr_vector<atom> m_atoms;
ptr_vector<atom> m_asserted_atoms; // set of asserted atoms
@ -186,7 +188,7 @@ namespace smt {
unsigned m_num_core_conflicts;
unsigned m_num_propagation_calls;
double m_agility;
bool m_is_lia;
lia_or_lra m_lia_or_lra;
bool m_non_diff_logic_exprs;
arith_factory * m_factory;
@ -220,6 +222,8 @@ namespace smt {
return get_family_id() == n->get_family_id();
}
void set_sort(expr* n);
public:
theory_diff_logic(ast_manager& m, smt_params & params):
theory(m.mk_family_id("arith")),
@ -233,7 +237,7 @@ namespace smt {
m_num_core_conflicts(0),
m_num_propagation_calls(0),
m_agility(0.5),
m_is_lia(true),
m_lia_or_lra(not_set),
m_non_diff_logic_exprs(false),
m_factory(nullptr),
m_nc_functor(*this),

25
src/smt/theory_diff_logic_def.h
View file

@ -252,7 +252,6 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
k -= numeral(1);
}
else {
m_is_lia = false;
k -= this->m_epsilon;
}
edge_id neg = m_graph.add_edge(target, source, k, ~l);
@ -647,7 +646,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
}
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, nullptr);
if (dump_lemmas()) {
symbol logic(m_is_lia ? "QF_LIA" : "QF_LRA");
symbol logic(m_lia_or_lra == is_lia ? "QF_LIA" : "QF_LRA");
ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);
}
@ -693,7 +692,7 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
);
if (dump_lemmas()) {
symbol logic(m_is_lia ? "QF_LIA" : "QF_LRA");
symbol logic(m_lia_or_lra == is_lia ? "QF_LIA" : "QF_LRA");
ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);
}
@ -743,6 +742,7 @@ theory_var theory_diff_logic<Ext>::mk_term(app* n) {
TRACE("arith", tout << mk_pp(n, get_manager()) << "\n";);
rational r;
if (m_util.is_numeral(n, r)) {
return mk_num(n, r);
@ -808,9 +808,26 @@ theory_var theory_diff_logic<Ext>::mk_var(enode* n) {
TRACE("diff_logic_vars", tout << "mk_var: " << v << "\n";);
m_graph.init_var(v);
get_context().attach_th_var(n, this, v);
set_sort(n->get_owner());
return v;
}
template<typename Ext>
theory_var theory_diff_logic<Ext>::set_sort(exir* n) {
if (m_util.is_int(n->get_owner())) {
if (m_lia_or_lra == is_lra) {
throw default_exception("difference logic does not work with mixed sorts");
}
m_lia_or_lra = is_lia;
}
else {
if (m_lia_or_lra == is_lia) {
throw default_exception("difference logic does not work with mixed sorts");
}
m_lia_or_lra = is_lra;
}
}
template<typename Ext>
theory_var theory_diff_logic<Ext>::mk_var(app* n) {
@ -853,7 +870,7 @@ void theory_diff_logic<Ext>::reset_eh() {
m_num_core_conflicts = 0;
m_num_propagation_calls = 0;
m_agility = 0.5;
m_is_lia = true;
m_lia_or_lra = not_set;
m_non_diff_logic_exprs = false;
m_objectives .reset();
m_objective_consts.reset();