merge

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

src/api/api_ast.cpp

@@ -249,6 +249,68 @@ extern "C" {
     MK_NARY(Z3_mk_and, mk_c(c)->get_basic_fid(), OP_AND, SKIP);
     MK_NARY(Z3_mk_or, mk_c(c)->get_basic_fid(), OP_OR, SKIP);
 
+    Z3_sort Z3_API Z3_mk_refinement_sort(Z3_context c, Z3_ast f) {
+        Z3_TRY;
+        LOG_Z3_mk_refinement_sort(c, f);
+        sort* s = nullptr;
+        if (to_ast(f)->get_kind() == AST_FUNC_DECL) {
+            func_decl* g = to_func_decl(to_ast(f));
+            s = mk_c(c)->rsutil().mk_sort(g);            
+        }
+        else {
+            CHECK_IS_EXPR(f, nullptr);
+            expr* e = to_expr(f);
+            s = mk_c(c)->rsutil().mk_sort(e);
+        }
+        mk_c(c)->save_ast_trail(s);
+        RETURN_Z3(of_sort(s));
+        Z3_CATCH_RETURN(nullptr);        
+    }
+
+    Z3_sort Z3_API Z3_refine_sort_basis(Z3_context c, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_refine_sort_basis(c, s);
+        sort* s0 = nullptr;
+        RESET_ERROR_CODE();
+        if (!mk_c(c)->rsutil().is_refine_sort(to_sort(s), s0)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+            RETURN_Z3(nullptr);
+        }
+        RETURN_Z3(of_sort(s0));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_refine_sort_predicate(Z3_context c, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_refine_sort_predicate(c, s);
+        RESET_ERROR_CODE();
+        sort* s0 = nullptr;
+        expr* e = nullptr;
+        func_decl* f = nullptr;
+        if (mk_c(c)->rsutil().is_refine_sort(to_sort(s), s0, e)) {
+            RETURN_Z3(of_ast(e));
+        }
+        if (mk_c(c)->rsutil().is_refine_sort(to_sort(s), s0, f)) {
+            RETURN_Z3(of_ast(f));
+        }
+        SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+        RETURN_Z3(nullptr);
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    MK_UNARY(Z3_mk_relax, mk_c(c)->rsutil().fid(), OP_RS_RELAX, SKIP);
+
+    Z3_ast Z3_API Z3_mk_restrict(Z3_context c, Z3_ast e, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_mk_restrict(c, e, s);
+        RESET_ERROR_CODE();
+        CHECK_IS_EXPR(e, nullptr);
+        expr* result = mk_c(c)->rsutil().mk_restrict(to_expr(e), to_sort(s));
+        mk_c(c)->save_ast_trail(result);
+        RETURN_Z3(of_ast(result));
+        Z3_CATCH_RETURN(nullptr);        
+    }
+
     Z3_ast mk_ite_core(Z3_context c, Z3_ast t1, Z3_ast t2, Z3_ast t3) {
         expr * result = mk_c(c)->m().mk_ite(to_expr(t1), to_expr(t2), to_expr(t3));
         mk_c(c)->save_ast_trail(result);
@@ -714,6 +776,9 @@ extern "C" {
         else if (fid == mk_c(c)->get_seq_fid() && k == RE_SORT) {
             return Z3_RE_SORT;
         }
+        else if (fid == mk_c(c)->rsutil().fid() && k == REFINE_SORT) {
+            return Z3_REFINE_SORT;
+        }
         else {
             return Z3_UNKNOWN_SORT;
         }
@@ -1290,6 +1355,14 @@ extern "C" {
             }
         }
 
+        if (mk_c(c)->get_rs_fid() == _d->get_family_id()) {
+            switch (_d->get_decl_kind()) {
+            case OP_RS_RELAX: return Z3_OP_RELAX;
+            case OP_RS_RESTRICT: return Z3_OP_RESTRICT;
+            default: break;
+            }
+        }
+
         return Z3_OP_UNINTERPRETED;
         Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED);
     }

src/api/api_context.cpp

@@ -81,6 +81,7 @@ namespace api {
         m_fpa_util(m()),
         m_sutil(m()),
         m_recfun(m()),
+        m_rs_util(m()),
         m_last_result(m()),
         m_ast_trail(m()),
         m_pmanager(m_limit) {

src/api/api_context.h

@@ -33,6 +33,7 @@ Revision History:
 #include "ast/fpa_decl_plugin.h"
 #include "ast/recfun_decl_plugin.h"
 #include "ast/special_relations_decl_plugin.h"
+#include "ast/refinement_sort_decl_plugin.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "smt/params/smt_params.h"
 #include "smt/smt_kernel.h"
@@ -89,6 +90,7 @@ namespace api {
         fpa_util                   m_fpa_util;
         seq_util                   m_sutil;
         recfun::util               m_recfun;
+        refinement_sort_util       m_rs_util;
 
         // Support for old solver API
         smt_params                 m_fparams;
@@ -157,6 +159,7 @@ namespace api {
         datatype_util& dtutil() { return m_dt_plugin->u(); }
         seq_util& sutil() { return m_sutil; }
         recfun::util& recfun() { return m_recfun; }
+        refinement_sort_util& rsutil() { return m_rs_util; }
         family_id get_basic_fid() const { return m_basic_fid; }
         family_id get_array_fid() const { return m_array_fid; }
         family_id get_arith_fid() const { return m_arith_fid; }
@@ -166,6 +169,7 @@ namespace api {
         family_id get_pb_fid() const { return m_pb_fid; }
         family_id get_fpa_fid() const { return m_fpa_fid; }
         family_id get_seq_fid() const { return m_seq_fid; }
+        family_id get_rs_fid() const { return m_rs_util.fid(); }
         datatype_decl_plugin * get_dt_plugin() const { return m_dt_plugin; }
         family_id get_special_relations_fid() const { return m_special_relations_fid; }
 

src/api/python/z3/z3.py

@@ -629,6 +629,8 @@ def _to_sort_ref(s, ctx):
         return ReSortRef(s, ctx)
     elif k == Z3_SEQ_SORT:
         return SeqSortRef(s, ctx)
+    elif k == Z3_REFINE_SORT:
+        return RefinementSortRef(s, ctx)
     return SortRef(s, ctx)
 
 def _sort(ctx, a):
@@ -10465,3 +10467,23 @@ def TransitiveClosure(f):
     The transitive closure R+ is a new relation.
     """
     return FuncDeclRef(Z3_mk_transitive_closure(f.ctx_ref(), f.ast), f.ctx)
+
+# Refinement sorts
+
+class RefinementSortRef(SortRef):
+    """Refinement sort."""
+
+    def basis(self):
+        return _to_sort_ref(Z3_refine_sort_basis(self.ctx_ref(), self.ast), self.ctx)
+
+    def predicate(self):
+        return _to_expr_ref(Z3_refine_sort_predicate(self.ctx_ref(), self.ast), self.ctx)
+    
+def Relax(e):
+    return _to_expr_ref(Z3_mk_relax(e.ctx_ref(), e.as_ast()), e.ctx)
+
+def Restrict(e, s):
+    return _to_expr_ref(Z3_mk_restrict(e.ctx_ref(), e.as_ast(), s.as_ast()), e.ctx)
+
+def RefineSort(p):
+    return _to_sort_ref(Z3_mk_refinement_sort(p.ctx_ref(), p.as_ast()), p.ctx)

src/api/python/z3/z3printer.py

@@ -566,6 +566,14 @@ class Formatter:
             return seq1('FPSort', (to_format(s.ebits()), to_format(s.sbits())))
         elif isinstance(s, z3.ReSortRef):
             return seq1('ReSort', (self.pp_sort(s.basis()), ))
+        elif isinstance(s, z3.RefinementSortRef):
+            f1 = self.pp_sort(s.basis())
+            p = s.predicate()
+            if isinstance(p, z3.ExprRef):
+                s2 = self.pp_expr(p, 0, [])
+            else:
+                s2 = self.pp_fdecl(p, 0, [])                
+            return seq1('RefineSort', [f1, to_format(s2)])
         elif isinstance(s, z3.SeqSortRef):
             if s.is_string():
                 return to_format("String")

src/api/z3_api.h

@@ -159,6 +159,7 @@ typedef enum
     Z3_ROUNDING_MODE_SORT,
     Z3_SEQ_SORT,
     Z3_RE_SORT,
+    Z3_REFINE_SORT,
     Z3_UNKNOWN_SORT = 1000
 } Z3_sort_kind;
 
@@ -998,6 +999,11 @@ typedef enum
             3 = 011 = Z3_OP_FPA_RM_TOWARD_NEGATIVE,
             4 = 100 = Z3_OP_FPA_RM_TOWARD_ZERO.
 
+      - Z3_OP_RELAX: takes a term of refinement sort s | p, and injects to sort s.
+      
+      - Z3_OP_RESTRCIT: takes a term of sort s and projects to refinement sort s | p
+
+
       - Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional
         information is exposed. Tools may use the string representation of the
         function declaration to obtain more information.
@@ -1302,6 +1308,10 @@ typedef enum {
     Z3_OP_FPA_BVWRAP,
     Z3_OP_FPA_BV2RM,
 
+    // injection and projection to refinement sorts
+    Z3_OP_RELAX = 0xc000,
+    Z3_OP_RESTRICT,
+
     Z3_OP_INTERNAL,
 
     Z3_OP_UNINTERPRETED
@@ -3771,6 +3781,48 @@ extern "C" {
 
     /*@}*/
 
+    /** @name Refinement sort */
+    /*@{*/
+
+    /** 
+        \brief creates refinement sort given lambda expression f (of sort Array(s, Bool))
+        or given function f with signature s -> Bool
+
+        def_API('Z3_mk_refinement_sort', SORT, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_sort Z3_API Z3_mk_refinement_sort(Z3_context c, Z3_ast f);
+    
+
+    /**
+       \brief retrieve base sort from refinement sort
+
+       def_API('Z3_refine_sort_basis', SORT, (_in(CONTEXT), _in(SORT)))
+    */
+    Z3_sort Z3_API Z3_refine_sort_basis(Z3_context c, Z3_sort s);
+
+    /**
+       \brief retrieve predicate from refinement sort
+
+       def_API('Z3_refine_sort_predicate', AST, (_in(CONTEXT), _in(SORT)))
+    */
+    Z3_ast Z3_API Z3_refine_sort_predicate(Z3_context c, Z3_sort s);
+
+
+    /**
+       \brief takes term e of refinement sort s | p and produces injection into s.
+
+       def_API('Z3_mk_relax', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_relax(Z3_context c, Z3_ast e);
+
+    /**
+       \brief takes term e of refinement sort s | p and produces injection into s.
+
+       def_API('Z3_mk_restrict', AST, (_in(CONTEXT), _in(AST), _in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_restrict(Z3_context c, Z3_ast e, Z3_sort s);
+    /*@}*/
+
     /** @name Quantifiers */
     /*@{*/
     /**

src/ast/CMakeLists.txt

@@ -38,6 +38,7 @@ z3_add_component(ast
     pb_decl_plugin.cpp
     pp.cpp
     recfun_decl_plugin.cpp
+    refinement_sort_decl_plugin.cpp
     reg_decl_plugins.cpp
     seq_decl_plugin.cpp
     shared_occs.cpp

src/ast/reg_decl_plugins.cpp

@@ -28,6 +28,7 @@ Revision History:
 #include "ast/pb_decl_plugin.h"
 #include "ast/fpa_decl_plugin.h"
 #include "ast/special_relations_decl_plugin.h"
+#include "ast/refinement_sort_decl_plugin.h"
 
 void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("arith")))) {
@@ -60,4 +61,7 @@ void reg_decl_plugins(ast_manager & m) {
     if (!m.get_plugin(m.mk_family_id(symbol("special_relations")))) {
         m.register_plugin(symbol("special_relations"), alloc(special_relations_decl_plugin));
     }
+    if (!m.get_plugin(m.mk_family_id(symbol("refinement_sort")))) {
+        m.register_plugin(symbol("refinement_sort"), alloc(refinement_sort_decl_plugin));
+    }
 }

src/ast/static_features.cpp

@@ -26,6 +26,7 @@ static_features::static_features(ast_manager & m):
     m_arrayutil(m),
     m_fpautil(m),
     m_sequtil(m),
+    m_rsutil(m),
     m_bfid(m.get_basic_family_id()),
     m_afid(m.mk_family_id("arith")),
     m_lfid(m.mk_family_id("label")),
@@ -80,6 +81,7 @@ void static_features::reset() {
     m_has_bv                               = false;
     m_has_fpa                              = false;
     m_has_sr                               = false;
+    m_has_rs                               = false;
     m_has_str                              = false;
     m_has_seq_non_str                      = false;
     m_has_arrays                           = false;
@@ -279,6 +281,8 @@ void static_features::update_core(expr * e) {
         m_has_fpa = true;
     if (is_app(e) && to_app(e)->get_family_id() == m_srfid) 
         m_has_sr = true;
+    if (m_rsutil.is_refine_sort(e))
+        m_has_rs = true;
     if (!m_has_arrays && m_arrayutil.is_array(e)) 
         m_has_arrays = true;
     if (!m_has_ext_arrays && m_arrayutil.is_array(e) && 

src/ast/static_features.h

@@ -26,12 +26,14 @@ Revision History:
 #include "ast/fpa_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/special_relations_decl_plugin.h"
+#include "ast/refinement_sort_decl_plugin.h"
 #include "util/map.h"
 
 struct static_features {
     ast_manager &            m;
     arith_util               m_autil;
     bv_util                  m_bvutil;
+    refinement_sort_util     m_rsutil;
     array_util               m_arrayutil;
     fpa_util                 m_fpautil;
     seq_util                 m_sequtil;
@@ -82,6 +84,7 @@ struct static_features {
     bool                     m_has_bv;          //
     bool                     m_has_fpa;         //
     bool                     m_has_sr;          // has special relations
+    bool                     m_has_rs;          // has refinement sorts
     bool                     m_has_str;         // has String-typed terms
     bool                     m_has_seq_non_str; // has non-String-typed Sequence terms
     bool                     m_has_arrays;      //

src/smt/CMakeLists.txt

@@ -65,6 +65,7 @@ z3_add_component(smt
     theory_opt.cpp
     theory_pb.cpp
     theory_recfun.cpp
+    theory_refinement_sort.cpp
     theory_seq.cpp
     theory_special_relations.cpp
     theory_str.cpp

src/smt/smt_internalizer.cpp

@@ -840,7 +840,8 @@ namespace smt {
        \brief Internalize an uninterpreted function application or constant.
     */
     void context::internalize_uninterpreted(app * n) {
-        SASSERT(!e_internalized(n));
+        if (e_internalized(n))
+            return;
         // process args
         for (expr * arg : *n) {
             internalize_rec(arg, false);

src/smt/smt_setup.cpp

@@ -34,6 +34,7 @@ Revision History:
 #include "smt/theory_seq_empty.h"
 #include "smt/theory_seq.h"
 #include "smt/theory_special_relations.h"
+#include "smt/theory_refinement_sort.h"
 #include "smt/theory_pb.h"
 #include "smt/theory_fpa.h"
 #include "smt/theory_str.h"
@@ -942,6 +943,10 @@ namespace smt {
         m_context.register_plugin(alloc(smt::theory_special_relations, m_manager));
     }
 
+    void setup::setup_refinement_sort() {
+        m_context.register_plugin(alloc(smt::theory_refinement_sort, m_manager));
+    }
+
     void setup::setup_unknown() {
         static_features st(m_manager);
         ptr_vector<expr> fmls;
@@ -958,6 +963,7 @@ namespace smt {
         setup_card();
         setup_fpa();
         if (st.m_has_sr) setup_special_relations();
+        if (st.m_has_rs) setup_refinement_sort();
     }
 
     void setup::setup_unknown(static_features & st) {
@@ -975,6 +981,7 @@ namespace smt {
             setup_fpa();
             setup_recfuns();
             if (st.m_has_sr) setup_special_relations();
+            if (st.m_has_rs) setup_refinement_sort();
             return;
         }
 

src/smt/smt_setup.h

@@ -83,6 +83,7 @@ namespace smt {
         void setup_LRA();
         void setup_CSP();
         void setup_special_relations();
+        void setup_refinement_sort();
         void setup_AUFLIA(bool simple_array = true);
         void setup_AUFLIA(static_features const & st);
         void setup_AUFLIRA(bool simple_array = true);

src/solver/tactic2solver.cpp

@@ -188,7 +188,7 @@ lbool tactic2solver::check_sat_core2(unsigned num_assumptions, expr * const * as
             }
             break;
         }
-        m_mc = concat(g->mc(), m_mc.get());
+        m_mc = concat(m_mc.get(), g->mc());
         if (m_mc && md) {
             (*m_mc)(md);
         }

src/tactic/bv/bv_size_reduction_tactic.cpp

@@ -178,7 +178,7 @@ public:
     void run(goal & g, model_converter_ref & mc) {
         if (g.inconsistent())
             return;
-        TRACE("before_bv_size_reduction", g.display(tout););
+        TRACE("goal", g.display(tout););
         m_produce_models = g.models_enabled();
         mc = nullptr;
         m_mc = nullptr;
@@ -365,7 +365,7 @@ public:
             m_fmc = nullptr;
         }
         report_tactic_progress(":bv-reduced", num_reduced);
-        TRACE("after_bv_size_reduction", g.display(tout); if (m_mc) m_mc->display(tout););
+        TRACE("goal", g.display(tout); if (m_mc) m_mc->display(tout););
     }
 
 };

src/tactic/core/elim_uncnstr_tactic.cpp

@@ -779,7 +779,7 @@ class elim_uncnstr_tactic : public tactic {
     void run(goal_ref const & g, goal_ref_buffer & result) {
         bool produce_proofs = g->proofs_enabled();
         
-        TRACE("elim_uncnstr_bug", g->display(tout););
+        TRACE("goal", g->display(tout););
         tactic_report report("elim-uncnstr", *g);
         m_vars.reset();
         collect_occs p;
@@ -826,7 +826,7 @@ class elim_uncnstr_tactic : public tactic {
                 m_rw = nullptr;                    
                 result.push_back(g.get());
                 g->inc_depth();
-                TRACE("elim_uncnstr_bug", g->display(tout););
+                TRACE("goal", g->display(tout););
                 return;
             }
             modified = false;