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

fix justification for implied equalities in special relations

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-04-03 17:08:10 -07:00
parent ff6d703c05
commit 56ac3f86a5
3 changed files with 34 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

20
examples/python/union_sort.py Normal file
View file

@ -0,0 +1,20 @@
# Copyright Microsoft Corporation 2019
# This example illustrates the use of union types
# from the Python API. It is given as an example
# as response to #2215.
from z3 import *
u = Datatype('IntOrString')
u.declare('IntV', ('int', IntSort()))
u.declare('StringV', ('string', StringSort()))
IntOrString = u.create()
StringV = IntOrString.StringV
IntV = IntOrString.IntV
print(IntV(1))
print(StringV(StringVal("abc")))
print(IntV(1).sort())
print(IntV(1) == StringV(StringVal("abc")))
s = String('s')
print(simplify(IntV(1) == StringV(s)))

5
src/smt/smt_context.cpp
View file

@ -1330,10 +1330,11 @@ namespace smt {
for (; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) { for (; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) {
new_eq & entry = m_eq_propagation_queue[i]; new_eq & entry = m_eq_propagation_queue[i];
add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification); add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification);
if (inconsistent()) if (inconsistent()) {
m_eq_propagation_queue.reset();
return false; return false;
} }
TRACE("add_eq", tout << m_eq_propagation_queue.size() << " " << i << "\n";); }
m_eq_propagation_queue.reset(); m_eq_propagation_queue.reset();
return true; return true;
} }

14
src/smt/theory_special_relations.cpp
View file

@ -162,6 +162,10 @@ namespace smt {
for (auto const& kv : m_relations) { for (auto const& kv : m_relations) {
if (extract_equalities(*kv.m_value)) { if (extract_equalities(*kv.m_value)) {
new_equality = true; new_equality = true;
//return FC_CONTINUE;
}
if (get_context().inconsistent()) {
return FC_CONTINUE;
} }
} }
if (new_equality) { if (new_equality) {
@ -322,7 +326,9 @@ namespace smt {
ast_manager& m = get_manager(); ast_manager& m = get_manager();
(void)m; (void)m;
r.m_graph.compute_zero_edge_scc(scc_id); r.m_graph.compute_zero_edge_scc(scc_id);
for (unsigned i = 0, j = 0; !ctx.inconsistent() && i < scc_id.size(); ++i) { int start = ctx.get_random_value();
for (unsigned idx = 0, j = 0; !ctx.inconsistent() && idx < scc_id.size(); ++idx) {
unsigned i = (start + idx) % scc_id.size();
if (scc_id[i] == -1) { if (scc_id[i] == -1) {
continue; continue;
} }
@ -336,8 +342,10 @@ namespace smt {
r.m_graph.find_shortest_zero_edge_path(i, j, timestamp, r); r.m_graph.find_shortest_zero_edge_path(i, j, timestamp, r);
r.m_graph.find_shortest_zero_edge_path(j, i, timestamp, r); r.m_graph.find_shortest_zero_edge_path(j, i, timestamp, r);
literal_vector const& lits = r.m_explanation; literal_vector const& lits = r.m_explanation;
TRACE("special_relations", ctx.display_literals_verbose(tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << " ", lits) << "\n";); TRACE("special_relations", ctx.display_literals_verbose(tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n", lits) << "\n";);
eq_justification js(ctx.mk_justification(theory_axiom_justification(get_id(), ctx.get_region(), lits.size(), lits.c_ptr()))); IF_VERBOSE(20, ctx.display_literals_verbose(verbose_stream() << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n", lits) << "\n";);
eq_justification js(ctx.mk_justification(ext_theory_eq_propagation_justification(get_id(), ctx.get_region(), lits.size(), lits.c_ptr(), 0, nullptr,
x, y)));
ctx.assign_eq(x, y, js); ctx.assign_eq(x, y, js);
} }
} }