diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 999ebab6b..5c945d168 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1058,6 +1058,8 @@ extern "C" { case OP_SPECIAL_RELATION_PO : return Z3_OP_SPECIAL_RELATION_PO; case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO; case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO; + case OP_SPECIAL_RELATION_TC : return Z3_OP_SPECIAL_RELATION_TC; + case OP_SPECIAL_RELATION_TRC : return Z3_OP_SPECIAL_RELATION_TRC; default: UNREACHABLE(); } } diff --git a/src/api/api_special_relations.cpp b/src/api/api_special_relations.cpp index e852c2b34..497ac15e0 100644 --- a/src/api/api_special_relations.cpp +++ b/src/api/api_special_relations.cpp @@ -27,47 +27,7 @@ Revision History: extern "C" { -#if 0 - bool Z3_API Z3_is_sr_lo(Z3_context c, Z3_ast s) { - Z3_TRY; - LOG_Z3_is_sr_lo(c, s); - RESET_ERROR_CODE(); - RETURN_Z3(mk_c(c)->sr_util().is_lo( to_expr(s) )); - Z3_CATCH_RETURN(false); - } - bool Z3_API Z3_is_sr_po(Z3_context c, Z3_ast s) { - Z3_TRY; - LOG_Z3_is_sr_po(c, s); - RESET_ERROR_CODE(); - RETURN_Z3(mk_c(c)->sr_util().is_po( to_expr(s) )); - Z3_CATCH_RETURN(false); - } - - bool Z3_API Z3_is_sr_po_ao(Z3_context c, Z3_ast s) { - Z3_TRY; - LOG_Z3_is_sr_po_ao(c, s); - RESET_ERROR_CODE(); - RETURN_Z3(mk_c(c)->sr_util().is_po_ao( to_expr(s) )); - Z3_CATCH_RETURN(false); - } - - bool Z3_API Z3_is_sr_plo(Z3_context c, Z3_ast s) { - Z3_TRY; - LOG_Z3_is_sr_plo(c, s); - RESET_ERROR_CODE(); - RETURN_Z3(mk_c(c)->sr_util().is_plo( to_expr(s) )); - Z3_CATCH_RETURN(false); - } - - bool Z3_API Z3_is_sr_to(Z3_context c, Z3_ast s) { - Z3_TRY; - LOG_Z3_is_sr_to(c, s); - RESET_ERROR_CODE(); - RETURN_Z3(mk_c(c)->sr_util().is_to( to_expr(s) )); - Z3_CATCH_RETURN(false); - } -#endif #define MK_TERN(NAME, FID) \ Z3_ast Z3_API NAME(Z3_context c, unsigned index, Z3_ast a, Z3_ast b) { \ LOG_ ##NAME(c, index, a, b); \ @@ -85,4 +45,22 @@ extern "C" { MK_TERN(Z3_mk_piecewise_linear_order, OP_SPECIAL_RELATION_PLO); MK_TERN(Z3_mk_tree_order, OP_SPECIAL_RELATION_TO); + +#define MK_DECL(NAME, FID) \ + Z3_func_decl Z3_API NAME(Z3_context c,Z3_func_decl f) { \ + Z3_TRY; \ + LOG_ ##NAME(c, f); \ + RESET_ERROR_CODE(); \ + ast_manager & m = mk_c(c)->m(); \ + func_decl* _f = to_func_decl(f); \ + parameter param(_f); \ + sort* domain[2] = { _f->get_domain(0), _f->get_domain(1) }; \ + func_decl * d = m.mk_func_decl(mk_c(c)->get_special_relations_fid(), FID, 1, ¶m, 2, domain); \ + mk_c(c)->save_ast_trail(d); \ + RETURN_Z3(of_func_decl(d)); \ + Z3_CATCH_RETURN(nullptr); \ +} + + MK_DECL(Z3_mk_transitive_closure, OP_SPECIAL_RELATION_TC); + MK_DECL(Z3_mk_transitive_reflexive_closure, OP_SPECIAL_RELATION_TRC); }; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e1fe76175..78a6247ed 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -875,6 +875,18 @@ typedef enum - Z3_OP_PB_EQ: Generalized Pseudo-Boolean equality constraint. Example 2*x + 1*y + 2*z + 1*u = 4 + - Z3_OP_SPECIAL_RELATION_LO: A relation that is a total linear order + + - Z3_OP_SPECIAL_RELATION_PO: A relation that is a partial order + + - Z3_OP_SPECIAL_RELATION_PLO: A relation that is a piecewise linear order + + - Z3_OP_SPECIAL_RELATION_TO: A relation that is a tree order + + - Z3_OP_SPECIAL_RELATION_TC: Transitive closure of a relation + + - Z3_OP_SPECIAL_RELATION_TRC: Transitive reflexive closure of a relation + - Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN: Floating-point rounding mode RNE - Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY: Floating-point rounding mode RNA @@ -1101,12 +1113,6 @@ typedef enum { Z3_OP_BUREM_I, Z3_OP_BSMOD_I, - // Special relations - Z3_OP_SPECIAL_RELATION_LO, - Z3_OP_SPECIAL_RELATION_PO, - Z3_OP_SPECIAL_RELATION_PLO, - Z3_OP_SPECIAL_RELATION_TO, - // Proofs Z3_OP_PR_UNDEF = 0x500, Z3_OP_PR_TRUE, @@ -1216,8 +1222,17 @@ typedef enum { Z3_OP_PB_GE, Z3_OP_PB_EQ, + // Special relations + Z3_OP_SPECIAL_RELATION_LO = 0xa000, + Z3_OP_SPECIAL_RELATION_PO, + Z3_OP_SPECIAL_RELATION_PLO, + Z3_OP_SPECIAL_RELATION_TO, + Z3_OP_SPECIAL_RELATION_TC, + Z3_OP_SPECIAL_RELATION_TRC, + + // Floating-Point Arithmetic - Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN, + Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN = 0xb000, Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY, Z3_OP_FPA_RM_TOWARD_POSITIVE, Z3_OP_FPA_RM_TOWARD_NEGATIVE, @@ -3643,6 +3658,20 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_tree_order(Z3_context c, unsigned id, Z3_ast a, Z3_ast b); + /** + \brief create transitive closure of binary relation. + + def_API('Z3_mk_transitive_closure', FUNC_DECL ,(_in(CONTEXT), _in(FUNC_DECL))) + */ + Z3_func_decl Z3_API Z3_mk_transitive_closure(Z3_context c,Z3_func_decl f); + + /** + \brief create transitive reflexive closure of binary relation. + + def_API('Z3_mk_transitive_reflexive_closure', FUNC_DECL ,(_in(CONTEXT), _in(FUNC_DECL))) + */ + Z3_func_decl Z3_API Z3_mk_transitive_reflexive_closure(Z3_context c,Z3_func_decl f); + /*@}*/ /** @name Quantifiers */ diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp index 6dd0af1b4..b1254552c 100644 --- a/src/ast/special_relations_decl_plugin.cpp +++ b/src/ast/special_relations_decl_plugin.cpp @@ -21,13 +21,13 @@ Revision History: #include "ast/ast.h" #include "ast/special_relations_decl_plugin.h" - - special_relations_decl_plugin::special_relations_decl_plugin(): m_lo("linear-order"), m_po("partial-order"), m_plo("piecewise-linear-order"), - m_to("tree-order") + m_to("tree-order"), + m_tc("transitive-closure"), + m_trc("transitive-reflexive-closure") {} func_decl * special_relations_decl_plugin::mk_func_decl( @@ -39,9 +39,12 @@ func_decl * special_relations_decl_plugin::mk_func_decl( return nullptr; } if (domain[0] != domain[1]) { - m_manager->raise_exception("argument sort missmatch"); + m_manager->raise_exception("argument sort missmatch. The two arguments should have the same sort"); return nullptr; } + if (!range) { + range = m_manager->mk_bool_sort(); + } func_decl_info info(m_family_id, k, num_parameters, parameters); symbol name; switch(k) { @@ -49,8 +52,11 @@ func_decl * special_relations_decl_plugin::mk_func_decl( case OP_SPECIAL_RELATION_LO: name = m_lo; break; case OP_SPECIAL_RELATION_PLO: name = m_plo; break; case OP_SPECIAL_RELATION_TO: name = m_to; break; + case OP_SPECIAL_RELATION_TC: name = m_tc; break; + case OP_SPECIAL_RELATION_TRC: name = m_trc; break; + case OP_SPECIAL_RELATION_NEXT: name = symbol("next"); break; } - return m_manager->mk_func_decl(name, arity, domain, m_manager->mk_bool_sort(), info); + return m_manager->mk_func_decl(name, arity, domain, range, info); } void special_relations_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { @@ -59,6 +65,8 @@ void special_relations_decl_plugin::get_op_names(svector & op_name op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO)); op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO)); op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO)); + op_names.push_back(builtin_name(m_tc.bare_str(), OP_SPECIAL_RELATION_TC)); + op_names.push_back(builtin_name(m_trc.bare_str(), OP_SPECIAL_RELATION_TRC)); } } @@ -68,6 +76,9 @@ sr_property special_relations_util::get_property(func_decl* f) const { case OP_SPECIAL_RELATION_LO: return sr_lo; case OP_SPECIAL_RELATION_PLO: return sr_plo; case OP_SPECIAL_RELATION_TO: return sr_to; + case OP_SPECIAL_RELATION_TC: return sr_tc; + case OP_SPECIAL_RELATION_TRC: return sr_trc; + case OP_SPECIAL_RELATION_NEXT: return sr_none; default: UNREACHABLE(); return sr_po; diff --git a/src/ast/special_relations_decl_plugin.h b/src/ast/special_relations_decl_plugin.h index 5926057f5..8e32e9817 100644 --- a/src/ast/special_relations_decl_plugin.h +++ b/src/ast/special_relations_decl_plugin.h @@ -28,6 +28,9 @@ enum special_relations_op_kind { OP_SPECIAL_RELATION_PO, OP_SPECIAL_RELATION_PLO, OP_SPECIAL_RELATION_TO, + OP_SPECIAL_RELATION_TC, + OP_SPECIAL_RELATION_TRC, + OP_SPECIAL_RELATION_NEXT, LAST_SPECIAL_RELATIONS_OP }; @@ -36,6 +39,8 @@ class special_relations_decl_plugin : public decl_plugin { symbol m_po; symbol m_plo; symbol m_to; + symbol m_tc; + symbol m_trc; public: special_relations_decl_plugin(); @@ -65,11 +70,17 @@ enum sr_property { sr_to = 0x01 | 0x02 | 0x04 | 0x10, // right-tree sr_plo = 0x01 | 0x02 | 0x04 | 0x08 | 0x10, // piecewise linear order sr_lo = 0x01 | 0x02 | 0x04 | 0x20, // linear order + sr_tc = 0x40, // transitive closure of relation + sr_trc = 0x42 // transitive reflexive closure of relation }; class special_relations_util { ast_manager& m; family_id m_fid; + func_decl* mk_rel_decl(func_decl* f, decl_kind k) { + parameter p(f); SASSERT(f->get_arity() == 2); + return m.mk_func_decl(m_fid, k, 1, &p, 2, f->get_domain(), f->get_range()); + } public: special_relations_util(ast_manager& m) : m(m), m_fid(m.get_family_id("special_relations")) {} @@ -78,15 +89,26 @@ public: sr_property get_property(func_decl* f) const; sr_property get_property(app* e) const { return get_property(e->get_decl()); } - func_decl* mk_to_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_TO, 1, &p, 2, f->get_domain(), f->get_range()); } - func_decl* mk_po_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_PO, 1, &p, 2, f->get_domain(), f->get_range()); } - func_decl* mk_plo_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_PLO, 1, &p, 2, f->get_domain(), f->get_range()); } - func_decl* mk_lo_decl(func_decl* f) { parameter p(f); SASSERT(f->get_arity() == 2); return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_LO, 1, &p, 2, f->get_domain(), f->get_range()); } + func_decl* mk_to_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TO); } + func_decl* mk_po_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_PO); } + func_decl* mk_plo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_PLO); } + func_decl* mk_lo_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_LO); } + func_decl* mk_tc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TC); } + func_decl* mk_trc_decl(func_decl* f) { return mk_rel_decl(f, OP_SPECIAL_RELATION_TRC); } + func_decl* mk_next(func_decl* f) { + sort* s = f->get_domain(0); + sort* domain[2] = { s, s }; + parameter p(f); SASSERT(f->get_arity() == 2); + return m.mk_func_decl(m_fid, OP_SPECIAL_RELATION_NEXT, 1, &p, 2, domain, s); + } bool is_lo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_LO); } bool is_po(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PO); } bool is_plo(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_PLO); } bool is_to(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TO); } + bool is_tc(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TC); } + bool is_trc(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_TRC); } + bool is_next(expr const * e) const { return is_app_of(e, m_fid, OP_SPECIAL_RELATION_NEXT); } app * mk_lo (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_LO, arg1, arg2); } app * mk_po (expr * arg1, expr * arg2) { return m.mk_app( m_fid, OP_SPECIAL_RELATION_PO, arg1, arg2); } diff --git a/src/model/model_pp.cpp b/src/model/model_pp.cpp index 08d63803b..727d2e1da 100644 --- a/src/model/model_pp.cpp +++ b/src/model/model_pp.cpp @@ -30,8 +30,7 @@ static void display_uninterp_sorts(std::ostream & out, model_core const & md) { for (unsigned i = 0; i < sz; i++) { sort * s = md.get_uninterpreted_sort(i); out << "(define-sort " << mk_pp(s, m); - ptr_vector const & univ = md.get_universe(s); - for (expr* e : univ) { + for (expr* e : md.get_universe(s)) { out << " " << mk_ismt2_pp(e, m); } out << ")\n"; diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 85330de87..0e8bd47e1 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -468,8 +468,9 @@ public: // That is init_var receives the id as an argument. void init_var(dl_var v) { TRACE("diff_logic_bug", tout << "init_var " << v << "\n";); - SASSERT(static_cast(v) >= m_out_edges.size() || - m_out_edges[v].empty()); + if (static_cast(v) < m_out_edges.size() && (!m_out_edges[v].empty() || !m_in_edges[v].empty())) { + return; + } SASSERT(check_invariant()); while (static_cast(v) >= m_out_edges.size()) { m_assignment .push_back(numeral()); @@ -649,6 +650,10 @@ public: } bool can_reach(dl_var src, dl_var dst) { + if (static_cast(src) >= m_out_edges.size() || + static_cast(dst) >= m_out_edges.size()) { + return false; + } uint_set target, visited; target.insert(dst); return reachable(src, target, visited, dst); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index d4d4ec6fb..cd909cf03 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -301,6 +301,10 @@ namespace smt { return m_expr2bool_var[n->get_id()]; } + bool_var get_bool_var(enode const * n) const { + return get_bool_var(n->get_owner()); + } + bool_var get_bool_var_of_id(unsigned id) const { return m_expr2bool_var[id]; } diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index b791991f2..9fec0e1d3 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -188,5 +188,9 @@ namespace smt { out.flush(); } + theory_var theory::get_th_var(expr* e) const { + return get_th_var(get_context().get_enode(e)); + } + }; diff --git a/src/smt/smt_theory.h b/src/smt/smt_theory.h index 92aa87163..e5798f6c3 100644 --- a/src/smt/smt_theory.h +++ b/src/smt/smt_theory.h @@ -66,6 +66,13 @@ namespace smt { m_var2enode.push_back(n); return v; } + + theory_var get_th_var(expr* e) const; + + theory_var get_th_var(enode* n) const { + return n->get_th_var(get_id()); + } + public: /** @@ -317,6 +324,10 @@ namespace smt { return m_var2enode[v]; } + app * get_expr(theory_var v) const { + return get_enode(v)->get_owner(); + } + /** \brief Return the equivalence class representative of the given theory variable. diff --git a/src/smt/theory_array.cpp b/src/smt/theory_array.cpp index ffeb1b274..3398d0894 100644 --- a/src/smt/theory_array.cpp +++ b/src/smt/theory_array.cpp @@ -297,6 +297,12 @@ namespace smt { void theory_array::new_eq_eh(theory_var v1, theory_var v2) { m_find.merge(v1, v2); +#if 0 + if (is_lambda(get_enode(v1)->get_owner()) || + is_lambda(get_enode(v2)->get_owner())) { + instantiate_extensionality(get_enode(v1), get_enode(v2)); + } +#endif } void theory_array::new_diseq_eh(theory_var v1, theory_var v2) { diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index d7ba74a87..0995458d5 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -85,7 +85,8 @@ namespace smt { theory_special_relations::theory_special_relations(ast_manager& m): theory(m.mk_family_id("special_relations")), - m_util(m) { + m_util(m), + m_can_propagate(false) { } theory_special_relations::~theory_special_relations() { @@ -99,6 +100,7 @@ namespace smt { bool theory_special_relations::internalize_atom(app * atm, bool gate_ctx) { SASSERT(m_util.is_special_relation(atm)); relation* r = 0; + ast_manager& m = get_manager(); if (!m_relations.find(atm->get_decl(), r)) { r = alloc(relation, m_util.get_property(atm), atm->get_decl()); m_relations.insert(atm->get_decl(), r); @@ -113,7 +115,7 @@ namespace smt { ctx.set_var_theory(v, get_id()); atom* a = alloc(atom, v, *r, v0, v1); m_atoms.push_back(a); - TRACE("special_relations", tout << mk_pp(atm, get_manager()) << " : bv" << v << " v" << a->v1() << " v" << a->v2() << ' ' << gate_ctx << "\n";); + TRACE("special_relations", tout << mk_pp(atm, m) << " : bv" << v << " v" << a->v1() << " v" << a->v2() << ' ' << gate_ctx << "\n";); m_bool_var2atom.insert(v, a); return true; } @@ -127,14 +129,15 @@ namespace smt { theory_var v = n->get_th_var(get_id()); if (null_theory_var == v) { v = theory::mk_var(n); + TRACE("special_relations", tout << "v" << v << " := " << mk_pp(e, get_manager()) << "\n";); ctx.attach_th_var(n, this, v); } return v; } void theory_special_relations::new_eq_eh(theory_var v1, theory_var v2) { - app* t1 = get_enode(v1)->get_owner(); - app* t2 = get_enode(v2)->get_owner(); + app* t1 = get_expr(v1); + app* t2 = get_expr(v2); literal eq = mk_eq(t1, t2, false); for (auto const& kv : m_relations) { relation& r = *kv.m_value; @@ -162,7 +165,6 @@ namespace smt { for (auto const& kv : m_relations) { if (extract_equalities(*kv.m_value)) { new_equality = true; - //return FC_CONTINUE; } if (get_context().inconsistent()) { return FC_CONTINUE; @@ -224,6 +226,137 @@ namespace smt { return res; } + + lbool theory_special_relations::final_check_tc(relation& r) { + // + // Ensure that Rxy -> TC(R)xy + // + func_decl* tcf = r.decl(); + func_decl* f = to_func_decl(tcf->get_parameter(0).get_ast()); + context& ctx = get_context(); + ast_manager& m = get_manager(); + bool new_assertion = false; + graph r_graph; + for (enode* n : ctx.enodes_of(f)) { + literal lit = ctx.enode2literal(n); + if (l_true == ctx.get_assignment(lit)) { + expr* e = ctx.bool_var2expr(lit.var()); + expr* arg1 = to_app(e)->get_arg(0); + expr* arg2 = to_app(e)->get_arg(1); + expr_ref tc_app(m.mk_app(tcf, arg1, arg2), m); + enode* tcn = ensure_enode(tc_app); + if (ctx.get_assignment(tcn) != l_true) { + literal consequent = ctx.get_literal(tc_app); + justification* j = ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), 1, &lit, consequent)); + TRACE("special_relations", tout << "propagate: " << tc_app << "\n";); + ctx.assign(consequent, j); + new_assertion = true; + } + else { + theory_var v1 = get_representative(get_th_var(arg1)); + theory_var v2 = get_representative(get_th_var(arg2)); + r_graph.init_var(v1); + r_graph.init_var(v2); + literal_vector ls; + r_graph.enable_edge(r_graph.add_edge(v1, v2, s_integer(0), ls)); + } + } + } + + // + // Ensure that TC(R)xy -> Rxz1 Rz1z2 .. Rzky + // + // if not Rxy and no path in graph: + // Find z reachable from x and u that an creach y, such that not Ruz is not forced + // introduce Ruy + // If no such element for infinite domains, then introduce z + // Rxz & Rzy + // For finite domains extract conflict. + // TBD: + // - infinite/large domain version is naive. + // It could be made fair by finding cut-points between x and y + // quantified axioms could prevent + // + unsigned sz = r.m_asserted_atoms.size(); + for (unsigned i = 0; i < sz; ++i) { + atom& a = *r.m_asserted_atoms[i]; + if (a.phase()) { + bool_var bv = a.var(); + TRACE("special_relations", tout << bv << " is positive\n";); + expr* arg1 = get_expr(a.v1()); + expr* arg2 = get_expr(a.v2()); + + // we need reachability in the R graph not R* graph + theory_var r1 = get_representative(a.v1()); + theory_var r2 = get_representative(a.v2()); + if (r_graph.can_reach(r1, r2)) { + TRACE("special_relations", + tout << a.v1() << ": " << mk_pp(arg1, m) << " -> " + << a.v2() << ": " << mk_pp(arg2, m) << " is positive reachable\n"; + r.m_graph.display(tout); + ); + continue; + } + expr_ref f_app(m.mk_app(f, arg1, arg2), m); + enode* fn = ensure_enode(f_app); + literal f_lit = ctx.get_literal(f_app); + switch (ctx.get_assignment(f_lit)) { + case l_true: + UNREACHABLE(); + // it should already be the case that v1 and reach v2 in the graph. + // whenever f(n1, n2) is asserted. + break; + case l_false: { + // TBD: perhaps replace by recursion unfolding similar to theory_rec_fun + expr_ref next(m.mk_app(m_util.mk_next(f), arg1, arg2), m); + expr_ref a2next(m.mk_app(f, arg1, next), m); + expr_ref next2b(m.mk_app(tcf, next, arg2), m); + expr_ref next_b(m.mk_app(f, next, arg2), m); + ensure_enode(a2next); + ensure_enode(next2b); + ensure_enode(next_b); + literal next2b_l = ctx.get_literal(next2b); + literal a2next_l = ctx.get_literal(a2next); + if (ctx.get_assignment(next2b_l) == l_true && ctx.get_assignment(a2next_l) == l_true) { + break; + } + ctx.mk_th_axiom(get_id(), ~literal(bv), f_lit, a2next_l); + ctx.mk_th_axiom(get_id(), ~literal(bv), f_lit, next2b_l); + expr* nxt = next; + while (m_util.is_next(nxt)) { + expr* left = to_app(nxt)->get_arg(0); + expr* right = to_app(nxt)->get_arg(1); + ctx.assign(~mk_eq(next, left, false), nullptr); + ctx.assign(~mk_eq(next, right, false), nullptr); + nxt = left; + } + ctx.set_true_first_flag(ctx.get_literal(next_b).var()); + new_assertion = true; + break; + } + case l_undef: + ctx.set_true_first_flag(bv); + TRACE("special_relations", tout << f_app << " is undefined\n";); + new_assertion = true; + break; + } + } + } + if (new_assertion) { + TRACE("special_relations", tout << "new assertion\n";); + return l_false; + } + return final_check_po(r); + } + + lbool theory_special_relations::final_check_trc(relation& r) { + // + // reflexivity is enforced from propagation. + // enforce transitivity. + // + return final_check_tc(r); + } + lbool theory_special_relations::final_check_to(relation& r) { uint_set visited, target; for (atom* ap : r.m_asserted_atoms) { @@ -310,15 +443,29 @@ namespace smt { case sr_to: res = final_check_to(r); break; + case sr_tc: + res = final_check_tc(r); + break; + case sr_trc: + res = final_check_trc(r); + break; default: UNREACHABLE(); res = l_undef; + break; } - TRACE("special_relations", r.display(*this, tout);); + TRACE("special_relations", r.display(*this, tout << res << "\n");); return res; } bool theory_special_relations::extract_equalities(relation& r) { + switch (r.m_property) { + case sr_tc: + case sr_trc: + return false; + default: + break; + } bool new_eq = false; int_vector scc_id; u_map roots; @@ -374,14 +521,47 @@ namespace smt { lbool theory_special_relations::propagate_po(atom& a) { lbool res = l_true; - relation& r = a.get_relation(); if (a.phase()) { + relation& r = a.get_relation(); r.m_uf.merge(a.v1(), a.v2()); res = enable(a); } return res; } + /** + \brief ensure that reflexivity is enforce for Transitive Reflexive closures + !TRC(R)xy => x != y + */ + lbool theory_special_relations::propagate_trc(atom& a) { + lbool res = l_true; + if (a.phase()) { + VERIFY(a.enable()); + relation& r = a.get_relation(); + r.m_uf.merge(a.v1(), a.v2()); + } + else { + literal lit(a.var(), true); + context& ctx = get_context(); + expr* arg1 = get_expr(a.v1()); + expr* arg2 = get_expr(a.v2()); + literal consequent = ~mk_eq(arg1, arg2, false); + justification* j = ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), 1, &lit, consequent)); + ctx.assign(consequent, j); + res = l_false; + } + return res; + } + + lbool theory_special_relations::propagate_tc(atom& a) { + if (a.phase()) { + VERIFY(a.enable()); + relation& r = a.get_relation(); + r.m_uf.merge(a.v1(), a.v2()); + } + return l_true; + } + lbool theory_special_relations::final_check_po(relation& r) { for (atom* ap : r.m_asserted_atoms) { atom& a = *ap; @@ -392,6 +572,7 @@ namespace smt { unsigned timestamp = r.m_graph.get_timestamp(); bool found_path = r.m_graph.find_shortest_reachable_path(a.v1(), a.v2(), timestamp, r); if (found_path) { + TRACE("special_relations", tout << "check po conflict\n";); r.m_explanation.push_back(a.explanation()); set_conflict(r); return l_false; @@ -401,6 +582,15 @@ namespace smt { return l_true; } + void theory_special_relations::propagate() { + if (m_can_propagate) { + for (auto const& kv : m_relations) { + propagate(*kv.m_value); + } + m_can_propagate = false; + } + } + lbool theory_special_relations::propagate(relation& r) { lbool res = l_true; while (res == l_true && r.m_asserted_qhead < r.m_asserted_atoms.size()) { @@ -415,6 +605,12 @@ namespace smt { case sr_po: res = propagate_po(a); break; + case sr_tc: + res = propagate_trc(a); + break; + case sr_trc: + res = propagate_tc(a); + break; default: if (a.phase()) { res = enable(a); @@ -439,9 +635,11 @@ namespace smt { atom* a = m_bool_var2atom[v]; a->set_phase(is_true); a->get_relation().m_asserted_atoms.push_back(a); + m_can_propagate = true; } void theory_special_relations::push_scope_eh() { + theory::push_scope_eh(); for (auto const& kv : m_relations) { kv.m_value->push(); } @@ -455,6 +653,7 @@ namespace smt { unsigned new_lvl = m_atoms_lim.size() - num_scopes; del_atoms(m_atoms_lim[new_lvl]); m_atoms_lim.shrink(new_lvl); + theory::pop_scope_eh(num_scopes); } void theory_special_relations::del_atoms(unsigned old_size) { @@ -562,7 +761,7 @@ namespace smt { func_interp* fi = alloc(func_interp, m, 1); for (unsigned i = 0; i < sz; ++i) { s_integer val = r.m_graph.get_assignment(i); - expr* arg = get_enode(i)->get_owner(); + expr* arg = get_expr(i); fi->insert_new_entry(&arg, arith.mk_numeral(val.to_rational(), true)); } TRACE("special_relations", r.m_graph.display(tout);); @@ -584,7 +783,7 @@ namespace smt { unsigned sz = r.m_graph.get_num_nodes(); for (unsigned i = 0; i < sz; ++i) { unsigned val = r.m_uf.find(i); - expr* arg = get_enode(i)->get_owner(); + expr* arg = get_expr(i); fi->insert_new_entry(&arg, arith.mk_numeral(rational(val), true)); } fi->set_else(arith.mk_numeral(rational(0), true)); @@ -606,7 +805,7 @@ namespace smt { hifn = m.mk_fresh_func_decl("hi", 1, ty, arith.mk_int()); unsigned sz = g.get_num_nodes(); for (unsigned i = 0; i < sz; ++i) { - expr* arg = get_enode(i)->get_owner(); + expr* arg = get_expr(i); lofi->insert_new_entry(&arg, arith.mk_numeral(rational(lo[i]), true)); hifi->insert_new_entry(&arg, arith.mk_numeral(rational(hi[i]), true)); } @@ -655,7 +854,7 @@ namespace smt { */ - void theory_special_relations::init_model_po(relation& r, model_generator& mg) { + void theory_special_relations::init_model_po(relation& r, model_generator& mg, bool is_reflexive) { ast_manager& m = get_manager(); sort* s = r.m_decl->get_domain(0); datatype_util dt(m); @@ -735,6 +934,7 @@ namespace smt { connected_rec_body = m.mk_ite(m.mk_app(snd, Sr), ST, Sc); } var* vars3[3] = { xV, yV, SV }; + IF_VERBOSE(0, verbose_stream() << connected_rec_body << "\n"); p.set_definition(rep, c2, 3, vars3, connected_rec_body); // r.m_decl(x,y) -> snd(connected2(x,y,nil)) @@ -743,7 +943,11 @@ namespace smt { x = xV, y = yV; func_interp* fi = alloc(func_interp, m, 2); - fi->set_else(m.mk_app(snd, m.mk_app(conn2, x, y, m.mk_app(cons, x, m.mk_const(nil))))); + expr_ref pred(m.mk_app(snd, m.mk_app(conn2, x, y, m.mk_app(cons, y, m.mk_const(nil)))), m); + if (is_reflexive) { + pred = m.mk_or(pred, m.mk_eq(x, y)); + } + fi->set_else(pred); mg.get_model().register_decl(r.decl(), fi); } @@ -881,7 +1085,11 @@ namespace smt { init_model_to(*kv.m_value, m); break; case sr_po: - init_model_po(*kv.m_value, m); + init_model_po(*kv.m_value, m, true); + break; + case sr_tc: + break; + case sr_trc: break; default: // other 28 combinations of 0x1F diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index 81a968e54..dfcc3adb9 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -130,6 +130,7 @@ namespace smt { unsigned_vector m_atoms_lim; obj_map m_relations; bool_var2atom m_bool_var2atom; + bool m_can_propagate; void del_atoms(unsigned old_size); @@ -138,6 +139,8 @@ namespace smt { lbool final_check_lo(relation& r); lbool final_check_plo(relation& r); lbool final_check_to(relation& r); + lbool final_check_tc(relation& r); + lbool final_check_trc(relation& r); lbool propagate(relation& r); lbool enable(atom& a); bool extract_equalities(relation& r); @@ -145,6 +148,8 @@ namespace smt { void set_conflict(relation& r); lbool propagate_plo(atom& a); lbool propagate_po(atom& a); + lbool propagate_tc(atom& a); + lbool propagate_trc(atom& a); theory_var mk_var(expr* e); void count_children(graph const& g, unsigned_vector& num_children); void ensure_strict(graph& g); @@ -155,7 +160,7 @@ namespace smt { expr_ref mk_interval(relation& r, model_generator& mg, unsigned_vector & lo, unsigned_vector& hi); void init_model_lo(relation& r, model_generator& m); void init_model_to(relation& r, model_generator& m); - void init_model_po(relation& r, model_generator& m); + void init_model_po(relation& r, model_generator& m, bool is_reflexive); void init_model_plo(relation& r, model_generator& m); bool is_neighbour_edge(graph const& g, edge_id id) const; bool is_strict_neighbour_edge(graph const& g, edge_id id) const; @@ -174,7 +179,7 @@ namespace smt { theory * mk_fresh(context * new_ctx) override; bool internalize_atom(app * atom, bool gate_ctx) override; - bool internalize_term(app * term) override { UNREACHABLE(); return false; } + bool internalize_term(app * term) override { return false; } void new_eq_eh(theory_var v1, theory_var v2) override; void new_diseq_eh(theory_var v1, theory_var v2) override {} bool use_diseqs() const override { return false; } @@ -189,8 +194,8 @@ namespace smt { void collect_statistics(::statistics & st) const override; model_value_proc * mk_value(enode * n, model_generator & mg) override; void init_model(model_generator & m) override; - bool can_propagate() override { return false; } - void propagate() override {} + bool can_propagate() override { return m_can_propagate; } + void propagate() override; void display(std::ostream & out) const override; };