add API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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

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;

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<datatype_decl_plugin*>(m().get_plugin(m_dt_fid));
     
         install_tactics(*this);

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();

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 <iostream>
+#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);
+
+};

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<typename T> class cast_ast;
 
     template<> class cast_ast<ast> {

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 */
     /*@{*/
     /**

src/smt/diff_logic.h

@@ -683,9 +683,12 @@ private:
     svector<int> 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;
+        bfs_todo.reset();
-        int_vector dfs_todo;
+        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);

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();
+            // the nodes visited from v1 become target for v2
-            if (r.m_graph.reachable(a.v2(), target, visited, w)) {
+            if (r.m_graph.reachable(a.v2(), visited, target, w)) {
-                // there is a common successor
+                // 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<unsigned> 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<dl_var> nodes;
         num_children.resize(sz, 0);
-        svector<bool>   processed(sz, false);
+        svector<bool> 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) {
+            for (edge_id e_id : edges) {
-                is_root = !g.is_enabled(edges[j]);
+                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";
     }
     

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<int_ext> {
             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_default_ctx> union_find_t;
 
         struct relation {
-            sr_property           m_property;
+            sr_property            m_property;
-            func_decl*            m_decl;
+            func_decl*             m_decl;
-            atoms                 m_asserted_atoms;   // set of asserted atoms
+            atoms                  m_asserted_atoms;   // set of asserted atoms
-            unsigned              m_asserted_qhead;
+            unsigned               m_asserted_qhead;
-            svector<scope>        m_scopes;
+            svector<scope>         m_scopes;
-            graph                 m_graph;
+            graph                  m_graph;
             union_find_default_ctx m_ufctx;
             union_find_t           m_uf;
             literal_vector         m_explanation;