Merge branch 'master' of https://github.com/Z3Prover/z3

contrib/cmake/src/CMakeLists.txt

@@ -117,14 +117,16 @@ else()
   set(lib_type "STATIC")
 endif()
 add_library(libz3 ${lib_type} ${object_files})
-# FIXME: Set "VERSION" and "SOVERSION" properly
 set_target_properties(libz3 PROPERTIES
-  # FIXME: Should we be using ${Z3_VERSION} here?
+  # VERSION determines the version in the filename of the shared library.
-  # VERSION: Sets up symlinks, does it do anything else?
+  # SOVERSION determines the value of the DT_SONAME field on ELF platforms.
+  # On ELF platforms the final compiled filename will be libz3.so.W.X.Y.Z
+  # but symlinks will be made to this file from libz3.so and also from
+  # libz3.so.W.X.
+  # This indicates that no breaking API changes will be made within a single
+  # minor version.
   VERSION ${Z3_VERSION}
-  # SOVERSION: On platforms that use ELF this sets the API version
+  SOVERSION ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR})
-  # and should be incremented everytime the API changes
-  SOVERSION ${Z3_VERSION})
 
 if (NOT MSVC)
   # On UNIX like platforms if we don't change the OUTPUT_NAME

contrib/cmake/src/tactic/CMakeLists.txt

@@ -12,6 +12,7 @@ z3_add_component(tactic
     probe.cpp
     proof_converter.cpp
     replace_proof_converter.cpp
+    sine_filter.cpp
     tactical.cpp
     tactic.cpp
   COMPONENT_DEPENDENCIES

scripts/mk_util.py

@@ -881,8 +881,8 @@ def is_CXX_gpp():
     return is_compiler(CXX, 'g++')
 
 def is_clang_in_gpp_form(cc):
-    version_string = check_output([cc, '--version'])
+    version_string = check_output([cc, '--version']).encode('utf-8').decode('utf-8')
-    return str(version_string).find('clang') != -1
+    return version_string.find('clang') != -1
 
 def is_CXX_clangpp():
     if is_compiler(CXX, 'g++'):

src/api/api_ast.cpp

@@ -1110,29 +1110,32 @@ extern "C" {
 
         if (mk_c(c)->get_seq_fid() == _d->get_family_id()) {
             switch (_d->get_decl_kind()) {
-            case Z3_OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT;
+            case OP_SEQ_UNIT: return Z3_OP_SEQ_UNIT;
-            case Z3_OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
+            case OP_SEQ_EMPTY: return Z3_OP_SEQ_EMPTY;
-            case Z3_OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
+            case OP_SEQ_CONCAT: return Z3_OP_SEQ_CONCAT;
-            case Z3_OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
+            case OP_SEQ_PREFIX: return Z3_OP_SEQ_PREFIX;
-            case Z3_OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
+            case OP_SEQ_SUFFIX: return Z3_OP_SEQ_SUFFIX;
-            case Z3_OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
+            case OP_SEQ_CONTAINS: return Z3_OP_SEQ_CONTAINS;
-            case Z3_OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
+            case OP_SEQ_EXTRACT: return Z3_OP_SEQ_EXTRACT;
-            case Z3_OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
+            case OP_SEQ_REPLACE: return Z3_OP_SEQ_REPLACE;
-            case Z3_OP_SEQ_AT: return Z3_OP_SEQ_AT;
+            case OP_SEQ_AT: return Z3_OP_SEQ_AT;
-            case Z3_OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
+            case OP_SEQ_LENGTH: return Z3_OP_SEQ_LENGTH;
-            case Z3_OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
+            case OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX;
-            case Z3_OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
+            case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
-            case Z3_OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
+            case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
 
-            case Z3_OP_RE_PLUS: return Z3_OP_RE_PLUS;
+            case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
-            case Z3_OP_RE_STAR: return Z3_OP_RE_STAR;
+            case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
-            case Z3_OP_RE_OPTION: return Z3_OP_RE_OPTION;
+
-            case Z3_OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
+            case OP_RE_PLUS: return Z3_OP_RE_PLUS;
-            case Z3_OP_RE_UNION: return Z3_OP_RE_UNION;
+            case OP_RE_STAR: return Z3_OP_RE_STAR;
-            case Z3_OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT;
+            case OP_RE_OPTION: return Z3_OP_RE_OPTION;
-            case Z3_OP_RE_LOOP: return Z3_OP_RE_LOOP;
+            case OP_RE_CONCAT: return Z3_OP_RE_CONCAT;
-            case Z3_OP_RE_FULL_SET: return Z3_OP_RE_FULL_SET;
+            case OP_RE_UNION: return Z3_OP_RE_UNION;
-            case Z3_OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET;
+            case OP_RE_INTERSECT: return Z3_OP_RE_INTERSECT;
+            case OP_RE_LOOP: return Z3_OP_RE_LOOP;
+            case OP_RE_FULL_SET: return Z3_OP_RE_FULL_SET;
+            case OP_RE_EMPTY_SET: return Z3_OP_RE_EMPTY_SET;
             default:
                 return Z3_OP_INTERNAL;
             }

src/api/api_seq.cpp

@@ -141,6 +141,10 @@ extern "C" {
     MK_UNARY(Z3_mk_seq_to_re, mk_c(c)->get_seq_fid(), OP_SEQ_TO_RE, SKIP);
     MK_BINARY(Z3_mk_seq_in_re, mk_c(c)->get_seq_fid(), OP_SEQ_IN_RE, SKIP);
 
+    MK_UNARY(Z3_mk_int_to_str, mk_c(c)->get_seq_fid(), OP_STRING_ITOS, SKIP);
+    MK_UNARY(Z3_mk_str_to_int, mk_c(c)->get_seq_fid(), OP_STRING_STOI, SKIP);
+
+
     Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) {
         Z3_TRY;
         LOG_Z3_mk_re_loop(c, r, lo, hi);

src/api/c++/z3++.h

@@ -435,6 +435,8 @@ namespace z3 {
         Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }
         unsigned hash() const { unsigned r = Z3_get_ast_hash(ctx(), m_ast); check_error(); return r; }
         friend std::ostream & operator<<(std::ostream & out, ast const & n);
+        std::string to_string() const { return std::string(Z3_ast_to_string(ctx(), m_ast)); }
+
 
         /**
            \brief Return true if the ASTs are structurally identical.
@@ -757,7 +759,25 @@ namespace z3 {
             }
             return result;
         }
-           
+
+        Z3_lbool bool_value() const {
+            return Z3_get_bool_value(ctx(), m_ast);
+        }
+
+        expr numerator() const { 
+            assert(is_numeral());
+            Z3_ast r = Z3_get_numerator(ctx(), m_ast);
+            check_error();
+            return expr(ctx(),r);
+        }
+
+
+        expr denominator() const { 
+            assert(is_numeral());
+            Z3_ast r = Z3_get_denominator(ctx(), m_ast);
+            check_error();
+            return expr(ctx(),r);
+        }
 
         operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
 
@@ -875,13 +895,23 @@ namespace z3 {
         friend expr operator*(expr const & a, int b);
         friend expr operator*(int a, expr const & b);
 
-        /**
+        /*  \brief Power operator  */
-           \brief Power operator
-        */
         friend expr pw(expr const & a, expr const & b);
         friend expr pw(expr const & a, int b);
         friend expr pw(int a, expr const & b);
 
+        /* \brief mod operator */
+        friend expr mod(expr const& a, expr const& b);
+        friend expr mod(expr const& a, int b);
+        friend expr mod(int a, expr const& b);
+
+        /* \brief rem operator */
+        friend expr rem(expr const& a, expr const& b);
+        friend expr rem(expr const& a, int b);
+        friend expr rem(int a, expr const& b);
+
+        friend expr is_int(expr const& e);
+
         friend expr operator/(expr const & a, expr const & b);
         friend expr operator/(expr const & a, int b);
         friend expr operator/(int a, expr const & b);
@@ -964,6 +994,17 @@ namespace z3 {
             check_error();
             return expr(ctx(), r);
         }
+        expr stoi() const {
+            Z3_ast r = Z3_mk_str_to_int(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
+        expr itos() const {
+            Z3_ast r = Z3_mk_int_to_str(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
+
         friend expr range(expr const& lo, expr const& hi);       
         /**
            \brief create a looping regular expression.
@@ -1001,34 +1042,46 @@ namespace z3 {
 
    };
 
+#define _Z3_MK_BIN_(a, b, binop)                        \
+    check_context(a, b);                                \
+    Z3_ast r = binop(a.ctx(), a, b);                    \
+    a.check_error();                                    \
+    return expr(a.ctx(), r);                            \
+
+
     inline expr implies(expr const & a, expr const & b) {
-        check_context(a, b);
+        assert(a.is_bool() && b.is_bool());     
-        assert(a.is_bool() && b.is_bool());
+        _Z3_MK_BIN_(a, b, Z3_mk_implies);
-        Z3_ast r = Z3_mk_implies(a.ctx(), a, b);
-        a.check_error();
-        return expr(a.ctx(), r);
     }
     inline expr implies(expr const & a, bool b) { return implies(a, a.ctx().bool_val(b)); }
     inline expr implies(bool a, expr const & b) { return implies(b.ctx().bool_val(a), b); }
 
 
-    inline expr pw(expr const & a, expr const & b) {
+    inline expr pw(expr const & a, expr const & b) { _Z3_MK_BIN_(a, b, Z3_mk_power);   }
-        assert(a.is_arith() && b.is_arith());
-        check_context(a, b);
-        Z3_ast r = Z3_mk_power(a.ctx(), a, b);
-        a.check_error();
-        return expr(a.ctx(), r);
-    }
     inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); }
     inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); }
 
+    inline expr mod(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_mod);   }
+    inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); }
+    inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); }
 
-    inline expr operator!(expr const & a) {
+    inline expr rem(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_rem);   }
-        assert(a.is_bool());
+    inline expr rem(expr const & a, int b) { return rem(a, a.ctx().num_val(b, a.get_sort())); }
-        Z3_ast r = Z3_mk_not(a.ctx(), a);
+    inline expr rem(int a, expr const & b) { return rem(b.ctx().num_val(a, b.get_sort()), b); }
-        a.check_error();
+
-        return expr(a.ctx(), r);
+#undef _Z3_MK_BIN_
-    }
+
+#define _Z3_MK_UN_(a, mkun)                     \
+    Z3_ast r = mkun(a.ctx(), a);                \
+    a.check_error();                            \
+    return expr(a.ctx(), r);                    \
+
+
+    inline expr operator!(expr const & a) { assert(a.is_bool()); _Z3_MK_UN_(a, Z3_mk_not); }
+
+    inline expr is_int(expr const& e) { _Z3_MK_UN_(e, Z3_mk_is_int); }
+
+#undef _Z3_MK_UN_
 
     inline expr operator&&(expr const & a, expr const & b) {
         check_context(a, b);

src/api/dotnet/Context.cs

@@ -2420,6 +2420,29 @@ namespace Microsoft.Z3
             return new SeqExpr(this, Native.Z3_mk_string(nCtx, s));
         }
 
+        /// <summary>
+        /// Convert an integer expression to a string.
+        /// </summary>
+        public SeqExpr IntToString(Expr e) 
+        {
+            Contract.Requires(e != null);
+	    Contract.Requires(e is ArithExpr);
+            Contract.Ensures(Contract.Result<SeqExpr>() != null);
+            return new SeqExpr(this, Native.Z3_mk_int_to_str(nCtx, e.NativeObject));
+        }
+
+        /// <summary>
+        /// Convert an integer expression to a string.
+        /// </summary>
+        public IntExpr StringToInt(Expr e) 
+        {
+            Contract.Requires(e != null);
+            Contract.Requires(e is SeqExpr);
+            Contract.Ensures(Contract.Result<IntExpr>() != null);
+            return new IntExpr(this, Native.Z3_mk_str_to_int(nCtx, e.NativeObject));
+        }
+
+
         /// <summary>
         /// Concatentate sequences.
         /// </summary>

src/api/python/z3/z3.py

@@ -868,6 +868,9 @@ class ExprRef(AstRef):
         _args, sz = _to_ast_array((a, b))
         return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx)
 
+    def params(self):
+        return self.decl().params()
+
     def decl(self):
         """Return the Z3 function declaration associated with a Z3 application.
 
@@ -1011,6 +1014,7 @@ def _coerce_exprs(a, b, ctx=None):
     b = s.cast(b)
     return (a, b)
 
+
 def _reduce(f, l, a):
     r = a
     for e in l:
@@ -1296,7 +1300,7 @@ class BoolSortRef(SortRef):
         if isinstance(val, bool):
             return BoolVal(val, self.ctx)
         if __debug__:
-            _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected")
+            _z3_assert(is_expr(val), "True, False or Z3 Boolean expression expected. Received %s" % val)
             _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
         return val
 
@@ -2012,7 +2016,7 @@ class ArithSortRef(SortRef):
             if self.is_real():
                 return RealVal(val, self.ctx)
             if __debug__:
-                _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected")
+                _z3_assert(False, "int, long, float, string (numeral), or Z3 Integer/Real expression expected. Got %s" % self)
 
 def is_arith_sort(s):
     """Return `True` if s is an arithmetical sort (type).
@@ -9660,6 +9664,29 @@ def Length(s):
     s = _coerce_seq(s)
     return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx)
 
+def StrToInt(s):
+    """Convert string expression to integer
+    >>> a = StrToInt("1")
+    >>> simplify(1 == a)
+    True
+    >>> b = StrToInt("2")
+    >>> simplify(1 == b)
+    False
+    >>> c = StrToInt(IntToStr(2))
+    >>> simplify(1 == c)
+    False
+    """
+    s = _coerce_seq(s)
+    return ArithRef(Z3_mk_str_to_int(s.ctx_ref(), s.as_ast()), s.ctx)
+
+
+def IntToStr(s):
+    """Convert integer expression to string"""
+    if not is_expr(s):
+        s = _py2expr(s)
+    return SeqRef(Z3_mk_int_to_str(s.ctx_ref(), s.as_ast()), s.ctx)
+
+
 def Re(s, ctx=None):
     """The regular expression that accepts sequence 's'
     >>> s1 = Re("ab")

src/api/z3_api.h

@@ -1152,6 +1152,10 @@ typedef enum {
     Z3_OP_SEQ_TO_RE,
     Z3_OP_SEQ_IN_RE,
 
+    // strings
+    Z3_OP_STR_TO_INT,
+    Z3_OP_INT_TO_STR,
+
     // regular expressions
     Z3_OP_RE_PLUS,
     Z3_OP_RE_STAR,
@@ -3325,6 +3329,21 @@ extern "C" {
      */
     Z3_ast Z3_API Z3_mk_seq_index(Z3_context c, Z3_ast s, Z3_ast substr, Z3_ast offset);
 
+    /**
+       \brief Convert string to integer.
+
+       def_API('Z3_mk_str_to_int' ,AST ,(_in(CONTEXT), _in(AST)))
+     */    
+    Z3_ast Z3_API Z3_mk_str_to_int(Z3_context c, Z3_ast s);
+
+
+    /**
+       \brief Integer to string conversion.
+
+       def_API('Z3_mk_int_to_str' ,AST ,(_in(CONTEXT), _in(AST)))
+     */    
+    Z3_ast Z3_API Z3_mk_int_to_str(Z3_context c, Z3_ast s);
+
     /**
        \brief Create a regular expression that accepts the sequence \c seq.
 

src/ast/ast.cpp

@@ -2326,6 +2326,22 @@ bool ast_manager::is_pattern(expr const * n) const {
     return true;
 }
 
+
+bool ast_manager::is_pattern(expr const * n, ptr_vector<expr> &args) {
+    if (!is_app_of(n, m_pattern_family_id, OP_PATTERN)) {
+        return false;
+    }
+    for (unsigned i = 0; i < to_app(n)->get_num_args(); ++i) {
+        expr *arg = to_app(n)->get_arg(i);
+        if (!is_app(arg)) {
+            return false;
+        }
+        args.push_back(arg);
+    }
+    return true;
+}
+
+
 quantifier * ast_manager::mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names,
                                         expr * body, int weight , symbol const & qid, symbol const & skid,
                                         unsigned num_patterns, expr * const * patterns,

src/ast/ast.h

@@ -1840,6 +1840,8 @@ public:
 
     bool is_pattern(expr const * n) const;
 
+    bool is_pattern(expr const *n, ptr_vector<expr> &args);
+
 public:
 
     quantifier * mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,

src/cmd_context/tactic_cmds.cpp

@@ -165,7 +165,21 @@ public:
     }
 };
 
-typedef simple_check_sat_result check_sat_tactic_result;
+struct check_sat_tactic_result : public simple_check_sat_result {
+public:
+  labels_vec labels;
+
+  check_sat_tactic_result(ast_manager & m) : simple_check_sat_result(m) {
+  }
+
+  virtual void get_labels(svector<symbol> & r) {
+    r.append(labels);
+  }
+
+  virtual void add_labels(svector<symbol> & r) {
+    labels.append(r);
+  }
+};
 
 class check_sat_using_tactict_cmd : public exec_given_tactic_cmd {
 public:
@@ -189,6 +203,7 @@ public:
         ast_manager & m = ctx.m();
         unsigned timeout   = p.get_uint("timeout", ctx.params().m_timeout);
         unsigned rlimit  =   p.get_uint("rlimit", ctx.params().m_rlimit);
+        labels_vec labels;
         goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores());
         assert_exprs_from(ctx, *g);
         TRACE("check_sat_using", g->display(tout););
@@ -208,7 +223,7 @@ public:
                 cmd_context::scoped_watch sw(ctx);
                 lbool r = l_undef;
                 try {
-                    r = check_sat(t, g, md, pr, core, reason_unknown);
+                    r = check_sat(t, g, md, result->labels, pr, core, reason_unknown);
                     ctx.display_sat_result(r);
                     result->set_status(r);
                     if (r == l_undef) {

src/smt/tactic/smt_tactic.cpp

@@ -204,7 +204,9 @@ public:
                 if (in->models_enabled()) {
                     model_ref md;
                     m_ctx->get_model(md);
-                    mc = model2model_converter(md.get());
+                    buffer<symbol> r;
+                    m_ctx->get_relevant_labels(0, r);
+                    mc = model_and_labels2model_converter(md.get(), r);
                     mc = concat(fmc.get(), mc.get());
                 }
                 return;
@@ -251,7 +253,9 @@ public:
                         if (in->models_enabled()) {
                             model_ref md;
                             m_ctx->get_model(md);
-                            mc = model2model_converter(md.get());
+                            buffer<symbol> r;
+                            m_ctx->get_relevant_labels(0, r);
+                            mc = model_and_labels2model_converter(md.get(), r);
                         }
                         return;
                     default:

src/smt/theory_arith.h

@@ -946,6 +946,7 @@ namespace smt {
         //
         // -----------------------------------
         typedef int_hashtable<int_hash, default_eq<int> > row_set;
+        bool            m_model_depends_on_computed_epsilon;
         unsigned        m_nl_rounds;
         bool            m_nl_gb_exhausted;
         unsigned        m_nl_strategy_idx; // for fairness

src/smt/theory_arith_core.h

@@ -1405,6 +1405,7 @@ namespace smt {
 
     template<typename Ext>
     final_check_status theory_arith<Ext>::final_check_core() {
+        m_model_depends_on_computed_epsilon = false;
         unsigned old_idx = m_final_check_idx;
         final_check_status result = FC_DONE;
         final_check_status ok;
@@ -1669,6 +1670,7 @@ namespace smt {
         m_liberal_final_check(true),
         m_changed_assignment(false),
         m_assume_eq_head(0),
+        m_model_depends_on_computed_epsilon(false),
         m_nl_rounds(0),
         m_nl_gb_exhausted(false),
         m_nl_new_exprs(m),
@@ -3220,7 +3222,9 @@ namespace smt {
         m_factory = alloc(arith_factory, get_manager());
         m.register_factory(m_factory);
         compute_epsilon();
-        refine_epsilon();
+        if (!m_model_depends_on_computed_epsilon) {
+            refine_epsilon();
+        }
     }
 
     template<typename Ext>

src/smt/theory_arith_nl.h

@@ -638,6 +638,7 @@ namespace smt {
         if (!val.get_infinitesimal().is_zero() && !computed_epsilon) {
             compute_epsilon();
             computed_epsilon = true;
+            m_model_depends_on_computed_epsilon = true;
         }
         return  val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
     }
@@ -652,14 +653,18 @@ namespace smt {
     bool theory_arith<Ext>::check_monomial_assignment(theory_var v, bool & computed_epsilon) {
         SASSERT(is_pure_monomial(var2expr(v)));
         expr * m      = var2expr(v);
-        rational val(1);
+        rational val(1), v_val;
         for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) {
             expr * arg = to_app(m)->get_arg(i);
             theory_var curr = expr2var(arg);
             SASSERT(curr != null_theory_var);
-            val *= get_value(curr, computed_epsilon);
+            v_val = get_value(curr, computed_epsilon);
+            TRACE("non_linear", tout << mk_pp(arg, get_manager()) << " = " << v_val << "\n";);
+            val *= v_val;
         }
-        return get_value(v, computed_epsilon) == val;
+        v_val = get_value(v, computed_epsilon);
+        TRACE("non_linear", tout << "v" << v << " := " << v_val << " == " << val << "\n";);
+        return v_val == val;
     }
 
 
@@ -2356,6 +2361,7 @@ namespace smt {
     */
     template<typename Ext>
     final_check_status theory_arith<Ext>::process_non_linear() {
+        m_model_depends_on_computed_epsilon = false;
         if (m_nl_monomials.empty())
             return FC_DONE;
 

src/solver/tactic2solver.cpp

@@ -146,8 +146,9 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
     proof_ref           pr(m);
     expr_dependency_ref core(m);
     std::string         reason_unknown = "unknown";
+    labels_vec labels;
     try {
-        switch (::check_sat(*m_tactic, g, md, pr, core, reason_unknown)) {
+        switch (::check_sat(*m_tactic, g, md, labels, pr, core, reason_unknown)) {
         case l_true: 
             m_result->set_status(l_true);
             break;

src/tactic/filter_model_converter.cpp

@@ -51,6 +51,9 @@ void filter_model_converter::operator()(model_ref & old_model, unsigned goal_idx
     TRACE("filter_mc", tout << "after filter_model_converter\n"; model_v2_pp(tout, *old_model););
 }
 
+void filter_model_converter::operator()(svector<symbol> & labels, unsigned goal_idx) {
+}
+
 void filter_model_converter::display(std::ostream & out) {
     out << "(filter-model-converter";
     for (unsigned i = 0; i < m_decls.size(); i++) {

src/tactic/filter_model_converter.h

@@ -32,6 +32,8 @@ public:
     
     virtual void operator()(model_ref & md, unsigned goal_idx);
 
+    virtual void operator()(svector<symbol> & labels, unsigned goal_idx);
+    
     virtual void operator()(model_ref & md) { operator()(md, 0); } // TODO: delete
 
     virtual void cancel() {}

src/tactic/model_converter.cpp

@@ -33,6 +33,12 @@ public:
         this->m_c1->operator()(m, 0);
     }
 
+    virtual void operator()(labels_vec & r, unsigned goal_idx) {
+        this->m_c2->operator()(r, goal_idx);
+        this->m_c1->operator()(r, 0);
+    }
+
+  
     virtual char const * get_name() const { return "concat-model-converter"; }
 
     virtual model_converter * translate(ast_translation & translator) {
@@ -76,6 +82,24 @@ public:
         }
         UNREACHABLE();
     }
+
+    virtual void operator()(labels_vec & r, unsigned goal_idx) {
+        unsigned num = this->m_c2s.size();
+        for (unsigned i = 0; i < num; i++) {
+            if (goal_idx < this->m_szs[i]) {
+                // found the model converter that should be used
+                model_converter * c2 = this->m_c2s[i];
+                if (c2)
+                  c2->operator()(r, goal_idx);
+                if (m_c1)
+                  this->m_c1->operator()(r, i);
+                return;
+            }
+            // invalid goal
+            goal_idx -= this->m_szs[i];
+        }
+        UNREACHABLE();
+    }
     
     virtual char const * get_name() const { return "concat-star-model-converter"; }
 
@@ -102,8 +126,12 @@ model_converter * concat(model_converter * mc1, unsigned num, model_converter *
 
 class model2mc : public model_converter {
     model_ref m_model;
+    buffer<symbol> m_labels;
 public:
     model2mc(model * m):m_model(m) {}
+
+    model2mc(model * m, buffer<symbol> const & r):m_model(m), m_labels(r) {}
+
     virtual ~model2mc() {}
 
     virtual void operator()(model_ref & m) {
@@ -114,7 +142,11 @@ public:
         m = m_model;
     }
 
-    virtual void cancel() {
+    virtual void operator()(labels_vec & r, unsigned goal_idx) {
+      r.append(m_labels.size(), m_labels.c_ptr());
+    }
+
+  virtual void cancel() {
     }
     
     virtual void display(std::ostream & out) {
@@ -135,6 +167,12 @@ model_converter * model2model_converter(model * m) {
     return alloc(model2mc, m);
 }
 
+model_converter * model_and_labels2model_converter(model * m, buffer<symbol> & r) {
+    if (m == 0)
+        return 0;
+    return alloc(model2mc, m, r);
+}
+
 void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m) {
     if (mc) {
         m = alloc(model, mng);

src/tactic/model_converter.h

@@ -23,6 +23,8 @@ Notes:
 #include"converter.h"
 #include"ref.h"
 
+class labels_vec : public svector<symbol> {};
+
 class model_converter : public converter {
 public:
     virtual void operator()(model_ref & m) {}  // TODO: delete
@@ -32,6 +34,8 @@ public:
         SASSERT(goal_idx == 0);
         operator()(m);
     }
+
+    virtual void operator()(labels_vec & r, unsigned goal_idx) {}
     
     virtual model_converter * translate(ast_translation & translator) = 0;
 };
@@ -49,6 +53,8 @@ model_converter * concat(model_converter * mc1, unsigned num, model_converter *
 
 model_converter * model2model_converter(model * m);
 
+model_converter * model_and_labels2model_converter(model * m, buffer<symbol> &r);
+
 void model_converter2model(ast_manager & mng, model_converter * mc, model_ref & m);
 
 void apply(model_converter_ref & mc, model_ref & m, unsigned gidx);

src/tactic/sine_filter.cpp

@@ -0,0 +1,245 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+  sine_filter.cpp
+
+Abstract:
+
+  Tactic that performs Sine Qua Non premise selection
+
+Author:
+
+  Doug Woos
+
+Revision History:
+--*/
+
+#include "sine_filter.h"
+#include "tactical.h"
+#include "filter_model_converter.h"
+#include "datatype_decl_plugin.h"
+#include "rewriter_def.h"
+#include "filter_model_converter.h"
+#include "extension_model_converter.h"
+#include "var_subst.h"
+#include "ast_util.h"
+#include "obj_pair_hashtable.h"
+#include "ast_pp.h"
+
+class sine_tactic : public tactic {
+
+    ast_manager&  m;
+    params_ref    m_params;
+
+public:
+
+    sine_tactic(ast_manager& m, params_ref const& p): 
+        m(m), m_params(p) {}
+    
+    virtual tactic * translate(ast_manager & m) {
+        return alloc(sine_tactic, m, m_params);
+    }
+
+    virtual void updt_params(params_ref const & p) {
+    }
+
+    virtual void collect_param_descrs(param_descrs & r) {
+    }
+
+    virtual void operator()(goal_ref const & g,
+                            goal_ref_buffer & result,
+                            model_converter_ref & mc,
+                            proof_converter_ref & pc,
+                            expr_dependency_ref & core) {
+        mc = 0; pc = 0; core = 0;
+
+        TRACE("sine", g->display(tout););
+        TRACE("sine", tout << g->size(););
+        ptr_vector<expr> new_forms;
+        filter_expressions(g, new_forms);
+        TRACE("sine", tout << new_forms.size(););
+        g->reset();
+        for (unsigned i = 0; i < new_forms.size(); i++) {
+            g->assert_expr(new_forms.get(i), 0, 0);
+        }
+        g->inc_depth();
+        g->updt_prec(goal::OVER);
+        result.push_back(g.get());
+        TRACE("sine", result[0]->display(tout););
+        SASSERT(g->is_well_sorted());
+        filter_model_converter * fmc = alloc(filter_model_converter, m);
+        mc = fmc;
+    }
+    
+    virtual void cleanup() {
+    }
+
+private:
+
+    typedef std::pair<expr*,expr*> t_work_item;
+
+    t_work_item work_item(expr *e, expr *root) {
+        return std::pair<expr*, expr*>(e, root);
+    }
+
+    void find_constants(expr *e, obj_hashtable<func_decl> &consts) {
+        ptr_vector<expr> stack;
+        stack.push_back(e);
+        expr *curr;
+        while (!stack.empty()) {
+            curr = stack.back();
+            stack.pop_back();
+            if (is_app(curr)) {
+                app *a = to_app(curr);
+                if (is_uninterp(a)) {
+                    func_decl *f = a->get_decl();
+                    consts.insert_if_not_there(f);
+                }
+            }
+        }
+    }
+
+    bool quantifier_matches(quantifier *q,
+                            obj_hashtable<func_decl> const & consts,
+                            ptr_vector<func_decl> & next_consts) {
+        TRACE("sine", tout << "size of consts is "; tout << consts.size(); tout << "\n";);
+        for (obj_hashtable<func_decl>::iterator constit = consts.begin(), constend = consts.end(); constit != constend; constit++) {
+            TRACE("sine", tout << *constit; tout << "\n";);
+        }
+        bool matched = false;
+        for (unsigned i = 0; i < q->get_num_patterns(); i++) {
+            bool p_matched = true;
+            ptr_vector<expr> stack;
+            expr *curr;
+            // patterns are wrapped with "pattern"
+            if (!m.is_pattern(q->get_pattern(i), stack)) {
+                continue;
+            }
+            while (!stack.empty()) {
+                curr = stack.back();
+                stack.pop_back();
+                if (is_app(curr)) {
+                    app *a = to_app(curr);
+                    func_decl *f = a->get_decl();
+                    if (!consts.contains(f)) {
+                        TRACE("sine", tout << mk_pp(f, m) << "\n";);
+                        p_matched = false;
+                        next_consts.push_back(f);
+                        break;
+                    }
+                    for (unsigned j = 0; j < a->get_num_args(); j++) {
+                        stack.push_back(a->get_arg(j));
+                    }
+                }
+            }
+            if (p_matched) {
+                matched = true;
+                break;
+            }
+        }
+        return matched;
+    }
+  
+    void filter_expressions(goal_ref const & g, ptr_vector<expr> & new_exprs) {
+        obj_map<func_decl, obj_hashtable<expr> > const2exp;
+        obj_map<expr, obj_hashtable<func_decl> > exp2const;
+        obj_map<func_decl, obj_pair_hashtable<expr, expr> > const2quantifier;
+        obj_hashtable<func_decl> consts;
+        vector<t_work_item> stack;
+        for (unsigned i = 0; i < g->size(); i++) {
+            stack.push_back(work_item(g->form(i), g->form(i)));
+        }
+        t_work_item curr;
+        while (!stack.empty()) {
+            curr = stack.back();
+            stack.pop_back();
+            if (is_app(curr.first)) {
+                app *a = to_app(curr.first);
+                if (is_uninterp(a)) {
+                    func_decl *f = a->get_decl();
+                    if (!consts.contains(f)) {
+                        consts.insert(f);
+                        if (const2quantifier.contains(f)) {
+                            for (obj_pair_hashtable<expr, expr>::iterator it = const2quantifier[f].begin(), end = const2quantifier[f].end(); it != end; it++) {
+                                stack.push_back(*it);
+                            }
+                            const2quantifier.remove(f);
+                        }
+                    }
+                    if (!const2exp.contains(f)) {
+                        const2exp.insert(f, obj_hashtable<expr>());
+                    }
+                    if (!const2exp[f].contains(curr.second)) {
+                        const2exp[f].insert(curr.second);
+                    }
+                    if (!exp2const.contains(curr.second)) {
+                        exp2const.insert(curr.second, obj_hashtable<func_decl>());
+                    }
+                    if (!exp2const[curr.second].contains(f)) {
+                        exp2const[curr.second].insert(f);
+                    }
+                }
+                for (unsigned i = 0; i < a->get_num_args(); i++) {
+                    stack.push_back(work_item(a->get_arg(i), curr.second));
+                }
+            }
+            else if (is_quantifier(curr.first)) {
+                quantifier *q = to_quantifier(curr.first);
+                if (q->is_forall()) {
+                    if (q->has_patterns()) {
+                        ptr_vector<func_decl> next_consts;
+                        if (quantifier_matches(q, consts, next_consts)) {
+                            stack.push_back(work_item(q->get_expr(), curr.second));
+                        }
+                        else {
+                            for (unsigned i = 0; i < next_consts.size(); i++) {
+                                func_decl *c = next_consts.get(i);
+                                if (!const2quantifier.contains(c)) {
+                                    const2quantifier.insert(c, obj_pair_hashtable<expr, expr>());
+                                }
+                                if (!const2quantifier[c].contains(curr)) {
+                                    const2quantifier[c].insert(curr);
+                                }
+                            }
+                        }
+                    }
+                    else {
+                        stack.push_back(work_item(q->get_expr(), curr.second));
+                    }
+                }
+                else if (q->is_exists()) {
+                    stack.push_back(work_item(q->get_expr(), curr.second));
+                }
+            }
+        }
+        // ok, now we just need to find the connected component of the last term
+    
+        obj_hashtable<expr> visited;
+        ptr_vector<expr> to_visit;
+        to_visit.push_back(g->form(g->size() - 1));
+        expr *visiting;
+        while (!to_visit.empty()) {
+            visiting = to_visit.back();
+            to_visit.pop_back();
+            visited.insert(visiting);
+            for (obj_hashtable<func_decl>::iterator constit = exp2const[visiting].begin(), constend = exp2const[visiting].end(); constit != constend; constit++) {
+                for (obj_hashtable<expr>::iterator exprit = const2exp[*constit].begin(), exprend = const2exp[*constit].end(); exprit != exprend; exprit++) {
+                    if (!visited.contains(*exprit)) {
+                        to_visit.push_back(*exprit);
+                    }
+                }
+            }
+        }
+        for (unsigned i = 0; i < g->size(); i++) {
+            if (visited.contains(g->form(i))) {
+                new_exprs.push_back(g->form(i));
+            }
+        }
+    }
+};
+
+tactic * mk_sine_tactic(ast_manager & m, params_ref const & p) {
+    return alloc(sine_tactic, m, p);
+}

src/tactic/sine_filter.h

@@ -0,0 +1,32 @@
+/*++
+Copyright (c) 2016 Microsoft Corporation
+
+Module Name:
+
+    sine_filter.h
+
+Abstract:
+
+    Tactic that performs Sine Qua Non premise selection
+
+Author:
+
+    Doug Woos
+
+Revision History:
+
+--*/
+#ifndef SINE_TACTIC_H_
+#define SINE_TACTIC_H_
+
+#include"params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_sine_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+/*
+    ADD_TACTIC("sine-filter", "eliminate premises using Sine Qua Non", "mk_sine_tactic(m, p)")
+*/
+
+#endif

src/tactic/tactic.cpp

@@ -175,7 +175,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_conve
     }
 }
 
-lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) {
+lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown) {
     bool models_enabled = g->models_enabled();
     bool proofs_enabled = g->proofs_enabled();
     bool cores_enabled  = g->unsat_core_enabled();
@@ -200,6 +200,8 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_d
 
     if (is_decided_sat(r)) {
         if (models_enabled) {
+            if (mc)
+                (*mc)(labels, 0);
             model_converter2model(m, mc.get(), md);
             if (!md) {
                 // create empty model.
@@ -216,7 +218,11 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_d
         return l_false;
     }
     else {
-        if (models_enabled) model_converter2model(m, mc.get(), md);
+        if (models_enabled) {
+          model_converter2model(m, mc.get(), md);
+          if (mc)
+              (*mc)(labels, 0);
+        }
         reason_unknown = "incomplete";
         return l_undef;
     }

src/tactic/tactic.h

@@ -153,7 +153,7 @@ public:
 #define MK_SIMPLE_TACTIC_FACTORY(NAME, ST)  MK_TACTIC_FACTORY(NAME, return ST;)
 
 void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result, model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core);
-lbool check_sat(tactic & t, goal_ref & g, model_ref & md, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);
+lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, proof_ref & pr, expr_dependency_ref & core, std::string & reason_unknown);
 
 // Throws an exception if goal \c in requires proof generation.
 void fail_if_proof_generation(char const * tactic_name, goal_ref const & in);