From 48e0626ffebc97e0bcacd08b07deb1a22051b302 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Mar 2019 17:42:27 -0700 Subject: [PATCH] add API Signed-off-by: Nikolaj Bjorner --- src/api/CMakeLists.txt | 1 + src/api/api_ast.cpp | 12 +++++ src/api/api_context.cpp | 1 + src/api/api_context.h | 3 ++ src/api/api_special_relations.cpp | 78 ++++++++++++++++++++++++++++ src/api/c++/z3++.h | 36 +++++++++++++ src/api/z3_api.h | 57 +++++++++++++++++++- src/smt/diff_logic.h | 9 ++-- src/smt/theory_special_relations.cpp | 31 ++++++----- src/smt/theory_special_relations.h | 22 ++++---- 10 files changed, 223 insertions(+), 27 deletions(-) create mode 100644 src/api/api_special_relations.cpp diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 4a5514a7b..247d0a14c 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -61,6 +61,7 @@ z3_add_component(api api_rcf.cpp api_seq.cpp api_solver.cpp + api_special_relations.cpp api_stats.cpp api_tactic.cpp z3_replayer.cpp diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index cabfdb101..a8f62572a 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1052,6 +1052,18 @@ extern "C" { } } + if (mk_c(c)->get_special_relations_fid() == _d->get_family_id()) { + switch(_d->get_decl_kind()) { + case OP_SPECIAL_RELATION_LO : return Z3_OP_SPECIAL_RELATION_LO; + case OP_SPECIAL_RELATION_PO : return Z3_OP_SPECIAL_RELATION_PO; + case OP_SPECIAL_RELATION_PO_AO : return Z3_OP_SPECIAL_RELATION_PO_AO; + case OP_SPECIAL_RELATION_PLO: return Z3_OP_SPECIAL_RELATION_PLO; + case OP_SPECIAL_RELATION_TO : return Z3_OP_SPECIAL_RELATION_TO; + default: UNREACHABLE(); + } + } + + if (mk_c(c)->get_bv_fid() == _d->get_family_id()) { switch(_d->get_decl_kind()) { case OP_BV_NUM: return Z3_OP_BNUM; diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 71bebef73..811cb30ee 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -101,6 +101,7 @@ namespace api { m_datalog_fid = m().mk_family_id("datalog_relation"); m_fpa_fid = m().mk_family_id("fpa"); m_seq_fid = m().mk_family_id("seq"); + m_special_relations_fid = m().mk_family_id("special_relations"); m_dt_plugin = static_cast(m().get_plugin(m_dt_fid)); install_tactics(*this); diff --git a/src/api/api_context.h b/src/api/api_context.h index 8bd75aaa0..1c4145810 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -30,6 +30,7 @@ Revision History: #include "ast/dl_decl_plugin.h" #include "ast/fpa_decl_plugin.h" #include "ast/recfun_decl_plugin.h" +#include "ast/special_relations_decl_plugin.h" #include "smt/smt_kernel.h" #include "smt/params/smt_params.h" #include "util/event_handler.h" @@ -106,6 +107,7 @@ namespace api { family_id m_pb_fid; family_id m_fpa_fid; family_id m_seq_fid; + family_id m_special_relations_fid; datatype_decl_plugin * m_dt_plugin; std::string m_string_buffer; // temporary buffer used to cache strings sent to the "external" world. @@ -162,6 +164,7 @@ namespace api { family_id get_fpa_fid() const { return m_fpa_fid; } family_id get_seq_fid() const { return m_seq_fid; } datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; } + family_id get_special_relations_fid() const { return m_special_relations_fid; } Z3_error_code get_error_code() const { return m_error_code; } void reset_error_code(); diff --git a/src/api/api_special_relations.cpp b/src/api/api_special_relations.cpp new file mode 100644 index 000000000..40fde5083 --- /dev/null +++ b/src/api/api_special_relations.cpp @@ -0,0 +1,78 @@ +/*++ +Copyright (c) 2019 Microsoft Corporation + +Module Name: + + api_special_relations.cpp + +Abstract: + Basic API for Special relations + +Author: + + Nikolaj Bjorner (nbjorner) 2019-03-25 + Ashutosh Gupta 2016 + +Revision History: + +--*/ + +#include +#include "api/z3.h" +#include "api/api_log_macros.h" +#include "api/api_context.h" +#include "api/api_util.h" +#include "ast/ast_pp.h" +#include "ast/special_relations_decl_plugin.h" + +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 + + MK_BINARY(Z3_mk_sr_lo , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_LO, SKIP); + MK_BINARY(Z3_mk_sr_po , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PO, SKIP); + MK_BINARY(Z3_mk_sr_po_ao,mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PO_AO,SKIP); + MK_BINARY(Z3_mk_sr_plo, mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_PLO, SKIP); + MK_BINARY(Z3_mk_sr_to , mk_c(c)->get_special_relations_fid(), OP_SPECIAL_RELATION_TO, SKIP); + +}; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4992015de..e18ca9204 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1707,6 +1707,42 @@ namespace z3 { */ inline expr sext(expr const & a, unsigned i) { return to_expr(a.ctx(), Z3_mk_sign_ext(a.ctx(), i, a)); } + inline expr sr_lo(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast r = Z3_mk_sr_lo(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } + + inline expr sr_po(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast r = Z3_mk_sr_po(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } + + inline expr sr_po_ao(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast r = Z3_mk_sr_po_ao(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } + + inline expr sr_plo(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast r = Z3_mk_sr_plo(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } + + inline expr sr_to(expr const& a, expr const& b) { + check_context(a, b); + Z3_ast r = Z3_mk_sr_to(a.ctx(), a, b); + a.check_error(); + return expr(a.ctx(), r); + } + + template class cast_ast; template<> class cast_ast { diff --git a/src/api/z3_api.h b/src/api/z3_api.h index e17378d94..6d1db22b3 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1101,6 +1101,13 @@ 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_PO_AO, + Z3_OP_SPECIAL_RELATION_PLO, + Z3_OP_SPECIAL_RELATION_TO, + // Proofs Z3_OP_PR_UNDEF = 0x500, Z3_OP_PR_TRUE, @@ -3595,10 +3602,58 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_re_full(Z3_context c, Z3_sort re); - /*@}*/ + /** @name Special relations */ + /*@{*/ + /** + \brief declare \c a and \c b are in linear order. + + \pre a and b are of same type. + + def_API('Z3_mk_sr_lo', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sr_lo(Z3_context c, Z3_ast a, Z3_ast b); + + /** + \brief declare \c a and \c b are in partial order. + + \pre a and b are of same type. + + def_API('Z3_mk_sr_po', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sr_po(Z3_context c, Z3_ast a, Z3_ast b); + + /** + \brief declare \c a and \c b are already partial ordered. + + \pre a and b are of same type. + + def_API('Z3_mk_sr_po_ao', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sr_po_ao(Z3_context c, Z3_ast a, Z3_ast b); + + /** + \brief declare \c a and \c b are in piecewise linear order. + + \pre a and b are of same type. + + def_API('Z3_mk_sr_plo', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sr_plo(Z3_context c, Z3_ast a, Z3_ast b); + + /** + \brief declare \c a and \c b are in total order. + + \pre a and b are of same type. + + def_API('Z3_mk_sr_to', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_sr_to(Z3_context c, Z3_ast a, Z3_ast b); + + /*@}*/ + /** @name Quantifiers */ /*@{*/ /** diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 8332baaf4..605390cf1 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -683,9 +683,12 @@ private: svector m_hybrid_visited, m_hybrid_parent; bool is_connected(numeral const& gamma, bool zero_edge, edge const& e, unsigned timestamp) const { - return (gamma.is_one() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp; + return (gamma.is_zero() || (!zero_edge && gamma.is_neg())) && e.get_timestamp() < timestamp; } + int_vector bfs_todo; + int_vector dfs_todo; + public: @@ -693,8 +696,8 @@ public: bool find_path(dl_var source, dl_var target, unsigned timestamp, Functor & f) { auto zero_edge = true; unsigned bfs_head = 0; - int_vector bfs_todo; - int_vector dfs_todo; + bfs_todo.reset(); + dfs_todo.reset(); m_hybrid_visited.resize(m_assignment.size(), m_run_counter++); m_hybrid_parent.resize(m_assignment.size(), -1); bfs_todo.push_back(source); diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 3750ce967..a4c73028e 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -213,17 +213,21 @@ namespace smt { theory_var w; // v2 !<= v1 is asserted target.insert(a.v2()); - if (r.m_graph.reachable(a.v1(), visited, target, w)) { + if (r.m_graph.reachable(a.v1(), target, visited, w)) { // we already have v1 <= v2 continue; } - target.reset(); - if (r.m_graph.reachable(a.v2(), target, visited, w)) { - // there is a common successor + // the nodes visited from v1 become target for v2 + if (r.m_graph.reachable(a.v2(), visited, target, w)) { + // we have the following: // v1 <= w // v2 <= w // v1 !<= v2 - // -> v1 <= w & v2 <= w & v1 !<= v2 -> v2 <= v1 + // + // enforce the assertion + // + // v1 <= w & v2 <= w & v1 !<= v2 -> v2 <= v1 + // unsigned timestamp = r.m_graph.get_timestamp(); r.m_explanation.reset(); r.m_graph.find_shortest_reachable_path(a.v1(), w, timestamp, r); @@ -297,7 +301,7 @@ namespace smt { u_map roots; context& ctx = get_context(); r.m_graph.compute_zero_edge_scc(scc_id); - for (unsigned i = 0, j = 0; i < scc_id.size(); ++i) { + for (unsigned i = 0, j = 0; !ctx.inconsistent() && i < scc_id.size(); ++i) { if (scc_id[i] == -1) { continue; } @@ -635,11 +639,11 @@ namespace smt { bool theory_special_relations::is_neighbour_edge(graph const& g, edge_id edge) const { CTRACE("special_relations_verbose", g.is_enabled(edge), tout << edge << ": " << g.get_source(edge) << " " << g.get_target(edge) << " "; - tout << (g.get_assignment(g.get_source(edge)) - g.get_assignment(g.get_target(edge))) << "\n";); + tout << (g.get_assignment(g.get_target(edge)) - g.get_assignment(g.get_source(edge))) << "\n";); return g.is_enabled(edge) && - g.get_assignment(g.get_source(edge)) - g.get_assignment(g.get_target(edge)) == s_integer(1); + g.get_assignment(g.get_source(edge)) + s_integer(1) == g.get_assignment(g.get_target(edge)); } bool theory_special_relations::is_strict_neighbour_edge(graph const& g, edge_id e) const { @@ -650,7 +654,7 @@ namespace smt { unsigned sz = g.get_num_nodes(); svector nodes; num_children.resize(sz, 0); - svector processed(sz, false); + svector processed(sz, false); for (unsigned i = 0; i < sz; ++i) nodes.push_back(i); while (!nodes.empty()) { dl_var v = nodes.back(); @@ -692,8 +696,8 @@ namespace smt { for (unsigned i = 0; i < sz; ++i) { bool is_root = true; int_vector const& edges = g.get_in_edges(i); - for (unsigned j = 0; is_root && j < edges.size(); ++j) { - is_root = !g.is_enabled(edges[j]); + for (edge_id e_id : edges) { + is_root &= !g.is_enabled(e_id); } if (is_root) { lo[i] = offset; @@ -739,7 +743,8 @@ namespace smt { init_model_po(*kv.m_value, m); break; default: - UNREACHABLE(); //ASHU: added to remove warning! Should be supported! + // other 28 combinations of 0x1F + NOT_IMPLEMENTED_YET(); } } } @@ -770,7 +775,7 @@ namespace smt { void theory_special_relations::display_atom(std::ostream & out, atom& a) const { context& ctx = get_context(); - expr* e = ctx.bool_var2expr( a.var() ); + expr* e = ctx.bool_var2expr(a.var()); out << (a.phase() ? "" : "(not ") << mk_pp(e, get_manager()) << (a.phase() ? "" : ")") << "\n"; } diff --git a/src/smt/theory_special_relations.h b/src/smt/theory_special_relations.h index 01314b362..312d0d20b 100644 --- a/src/smt/theory_special_relations.h +++ b/src/smt/theory_special_relations.h @@ -52,9 +52,9 @@ namespace smt { r.ensure_var(v2); literal_vector ls; ls.push_back(literal(b, false)); - m_pos = r.m_graph.add_edge(v1, v2, s_integer(1), ls); // v2 <= v1 + m_pos = r.m_graph.add_edge(v1, v2, s_integer(0), ls); // v1 <= v2 ls[0] = literal(b, true); - m_neg = r.m_graph.add_edge(v2, v1, s_integer(-2), ls); // v1 <= v2 - 1 + m_neg = r.m_graph.add_edge(v2, v1, s_integer(-1), ls); // v2 + 1 <= v1 } bool_var var() const { return m_bvar;} relation& get_relation() const { return m_relation; } @@ -80,22 +80,24 @@ namespace smt { }; struct graph : public dl_graph { bool add_strict_edge(theory_var v1, theory_var v2, literal_vector const& j) { - return enable_edge(add_edge(v1, v2, s_integer(1), j)); + // v1 + 1 <= v2 + return enable_edge(add_edge(v1, v2, s_integer(-1), j)); } bool add_non_strict_edge(theory_var v1, theory_var v2, literal_vector const& j) { - return enable_edge(add_edge(v1, v2, s_integer(-2), j)); + // v1 <= v2 + return enable_edge(add_edge(v1, v2, s_integer(0), j)); } }; typedef union_find union_find_t; struct relation { - sr_property m_property; - func_decl* m_decl; - atoms m_asserted_atoms; // set of asserted atoms - unsigned m_asserted_qhead; - svector m_scopes; - graph m_graph; + sr_property m_property; + func_decl* m_decl; + atoms m_asserted_atoms; // set of asserted atoms + unsigned m_asserted_qhead; + svector m_scopes; + graph m_graph; union_find_default_ctx m_ufctx; union_find_t m_uf; literal_vector m_explanation;