Merge branch 'master' of https://github.com/z3prover/z3 into polysat

src/api/api_ast.cpp

@@ -159,7 +159,7 @@ extern "C" {
             return;
         }
         recfun_replace replace(m);
-        p.set_definition(replace, pd, n, _vars.data(), abs_body);
+        p.set_definition(replace, pd, true, n, _vars.data(), abs_body);
         Z3_CATCH;
     }
 
@@ -1202,7 +1202,8 @@ extern "C" {
 
             case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
             case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;
-	    case OP_STRING_UBVTOS: return Z3_OP_UBV_TO_STR;
+            case OP_STRING_UBVTOS: return Z3_OP_UBV_TO_STR;
+            case OP_STRING_SBVTOS: return Z3_OP_SBV_TO_STR;
             case OP_STRING_LT: return Z3_OP_STRING_LT;
             case OP_STRING_LE: return Z3_OP_STRING_LE;
 

src/api/api_seq.cpp

@@ -245,6 +245,7 @@ extern "C" {
     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);
     MK_UNARY(Z3_mk_ubv_to_str, mk_c(c)->get_seq_fid(), OP_STRING_UBVTOS, SKIP);
+    MK_UNARY(Z3_mk_sbv_to_str, mk_c(c)->get_seq_fid(), OP_STRING_SBVTOS, SKIP);
 
 
     Z3_ast Z3_API Z3_mk_re_loop(Z3_context c, Z3_ast r, unsigned lo, unsigned hi) {

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

@@ -506,7 +506,7 @@ namespace z3 {
     public:
         ast(context & c):object(c), m_ast(0) {}
         ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
-        ast(ast const & s):object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
+        ast(ast const & s) :object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
         ast(ast && s) noexcept : object(std::forward<object>(s)), m_ast(s.m_ast) { s.m_ast = nullptr; }
         ~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
         operator Z3_ast() const { return m_ast; }
@@ -519,14 +519,6 @@ namespace z3 {
             m_ast = s.m_ast;
             return *this;
         }
-        ast & operator=(ast && s) noexcept {
-            if (this != &s) {
-                object::operator=(std::forward<object>(s));
-                m_ast = s.m_ast;
-                s.m_ast = nullptr;
-            }
-            return *this;
-        }
         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);
@@ -1447,6 +1439,11 @@ namespace z3 {
             check_error();
             return expr(ctx(), r);
         }
+        expr sbvtos() const {
+            Z3_ast r = Z3_mk_sbv_to_str(ctx(), *this);
+            check_error();
+            return expr(ctx(), r);
+        }
  
         friend expr range(expr const& lo, expr const& hi);
         /**
@@ -1874,11 +1871,15 @@ namespace z3 {
         Z3_ast r;
         if (a.is_int()) {
             expr zero = a.ctx().int_val(0);
-            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
+	    expr ge = a >= zero;
+	    expr na = -a;
+            r = Z3_mk_ite(a.ctx(), ge, a, na);	    
         }
         else if (a.is_real()) {
             expr zero = a.ctx().real_val(0);
-            r = Z3_mk_ite(a.ctx(), Z3_mk_ge(a.ctx(), a, zero), a, -a);
+	    expr ge = a >= zero;
+	    expr na = -a;
+            r = Z3_mk_ite(a.ctx(), ge, a, na);
         }
         else {
             r = Z3_mk_fpa_abs(a.ctx(), a); 

src/api/dotnet/Context.cs

@@ -556,18 +556,18 @@ namespace Microsoft.Z3
 
         /// <summary>
         /// Bind a definition to a recursive function declaration.
-	/// The function must have previously been created using
-	/// MkRecFuncDecl. The body may contain recursive uses of the function or
-	/// other mutually recursive functions. 
+        /// The function must have previously been created using
+        /// MkRecFuncDecl. The body may contain recursive uses of the function or
+        /// other mutually recursive functions. 
         /// </summary>
-	public void AddRecDef(FuncDecl f, Expr[] args, Expr body) 
-	{
-	    CheckContextMatch(f);
-	    CheckContextMatch<Expr>(args);
-	    CheckContextMatch(body);
+    public void AddRecDef(FuncDecl f, Expr[] args, Expr body) 
+    {
+        CheckContextMatch(f);
+        CheckContextMatch<Expr>(args);
+        CheckContextMatch(body);
             IntPtr[] argsNative = AST.ArrayToNative(args);
-	    Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
-	}	
+        Native.Z3_add_rec_def(nCtx, f.NativeObject, (uint)args.Length, argsNative, body.NativeObject);
+    }	
 
         /// <summary>
         /// Creates a new function declaration.
@@ -2405,6 +2405,15 @@ namespace Microsoft.Z3
             return new SeqExpr(this, Native.Z3_mk_ubv_to_str(nCtx, e.NativeObject));
         }
 
+        /// <summary>
+        /// Convert a bit-vector expression, represented as an signed number, to a string.
+        /// </summary>
+        public SeqExpr SbvToString(Expr e) {
+            Debug.Assert(e != null);
+            Debug.Assert(e is ArithExpr);
+            return new SeqExpr(this, Native.Z3_mk_sbv_to_str(nCtx, e.NativeObject));
+        }
+
         /// <summary>
         /// Convert an integer expression to a string.
         /// </summary>
@@ -2474,7 +2483,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Check if the string s1 is lexicographically strictly less than s2.
         /// </summary>
-	public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2) 
+        public BoolExpr MkStringLt(SeqExpr s1, SeqExpr s2) 
         {
             Debug.Assert(s1 != null);
             Debug.Assert(s2 != null);
@@ -2485,7 +2494,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Check if the string s1 is lexicographically strictly less than s2.
         /// </summary>
-	public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2) 
+        public BoolExpr MkStringLe(SeqExpr s1, SeqExpr s2) 
         {
             Debug.Assert(s1 != null);
             Debug.Assert(s2 != null);
@@ -2655,7 +2664,7 @@ namespace Microsoft.Z3
 
         /// <summary>
         /// Create the empty regular expression.
-	/// The sort s should be a regular expression.
+        /// The sort s should be a regular expression.
         /// </summary>
         public ReExpr MkEmptyRe(Sort s) 
         {
@@ -2665,7 +2674,7 @@ namespace Microsoft.Z3
 
         /// <summary>
         /// Create the full regular expression.
-	/// The sort s should be a regular expression.
+        /// The sort s should be a regular expression.
         /// </summary>
         public ReExpr MkFullRe(Sort s) 
         {
@@ -3399,7 +3408,7 @@ namespace Microsoft.Z3
         {
             Debug.Assert(t1 != null);
             Debug.Assert(t2 != null);
-	    //  Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
+            //  Debug.Assert(ts == null || Contract.ForAll(0, ts.Length, j => ts[j] != null));
 
             return AndThen(t1, t2, ts);
         }
@@ -4696,7 +4705,7 @@ namespace Microsoft.Z3
             {
                 foreach (Z3Object a in arr)
                 {
-	            Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
+                    Debug.Assert(a != null); // It was an assume, now we added the precondition, and we made it into an assert
                     CheckContextMatch(a);
                 }
             }

src/api/java/Context.java

@@ -2035,7 +2035,15 @@ public class Context implements AutoCloseable {
     {
 	return (SeqExpr<CharSort>) Expr.create(this, Native.mkUbvToStr(nCtx(), e.getNativeObject()));
     }
-
+    
+    /**
+     * Convert an signed bitvector expression to a string.
+     */
+    public SeqExpr<CharSort> sbvToString(Expr<BitVecSort> e)
+    {
+    return (SeqExpr<CharSort>) Expr.create(this, Native.mkSbvToStr(nCtx(), e.getNativeObject()));
+    }
+    
     /**
      * Convert an integer expression to a string.
      */

src/api/z3_api.h

@@ -1203,6 +1203,7 @@ typedef enum {
     Z3_OP_STR_TO_INT,
     Z3_OP_INT_TO_STR,
     Z3_OP_UBV_TO_STR,
+    Z3_OP_SBV_TO_STR,
     Z3_OP_STRING_LT,
     Z3_OP_STRING_LE,
 
@@ -3655,6 +3656,12 @@ extern "C" {
     */
     Z3_ast Z3_API Z3_mk_ubv_to_str(Z3_context c, Z3_ast s);
   
+    /**
+       \brief Signed bit-vector to string conversion.
+
+       def_API('Z3_mk_sbv_to_str' ,AST ,(_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_sbv_to_str(Z3_context c, Z3_ast s);
 
     /**
        \brief Create a regular expression that accepts the sequence \c seq.

src/ast/ast_ll_pp.cpp

@@ -248,8 +248,7 @@ public:
         }
     }
 
-    void operator()(quantifier * n) {
-        display_def_header(n);
+    void display_quantifier_header(quantifier* n) {
         m_out << "(" << (n->get_kind() == forall_k ? "forall" : (n->get_kind() == exists_k ? "exists" : "lambda")) << " ";
         unsigned num_decls = n->get_num_decls();
         m_out << "(vars ";
@@ -272,6 +271,12 @@ public:
             display_children(n->get_num_no_patterns(), n->get_no_patterns());
             m_out << ") ";
         }
+
+  }
+
+    void operator()(quantifier * n) {
+        display_def_header(n);
+        display_quantifier_header(n);
         display_child(n->get_expr());
         m_out << ")\n";
     }
@@ -281,6 +286,12 @@ public:
             m_out << "(:var " << to_var(n)->get_idx() << ")";
             return;
         }
+        if (is_quantifier(n)) {
+            display_quantifier_header(to_quantifier(n));
+            display(to_quantifier(n)->get_expr(), depth - 1);
+            m_out << ")";
+            return;
+        }
 
         if (!is_app(n) || depth == 0 || to_app(n)->get_num_args() == 0) {
             display_child(n);
@@ -304,16 +315,11 @@ public:
 
     void display_bounded(ast * n, unsigned depth) {
         if (!n)
-   	     m_out << "null";    
-        else if (is_app(n)) {
-            display(to_expr(n), depth);
-        }
-        else if (is_var(n)) {
-            m_out << "(:var " << to_var(n)->get_idx() << ")";
-        }
-        else {
-            m_out << "#" << n->get_id();
-        }
+            m_out << "null";    
+        else if (is_expr(n)) 
+            display(to_expr(n), depth);               
+        else 
+            m_out << "#" << n->get_id();        
     }
 };
 

src/ast/ast_pp.h

@@ -31,6 +31,7 @@ struct mk_pp : public mk_ismt2_pp {
     }
 };
 
+
 //<! print vector of ASTs
 class mk_pp_vec {
     ast_manager &   m;
@@ -54,3 +55,16 @@ inline std::ostream& operator<<(std::ostream & out, mk_pp_vec const & pp) {
 }
 
 
+inline std::string operator+(char const* s, mk_pp const& pp) {
+    std::ostringstream strm;
+    strm << s << pp;
+    return strm.str();
+}
+
+inline std::string operator+(std::string const& s, mk_pp const& pp) {
+    std::ostringstream strm;
+    strm << s << pp;
+    return strm.str();
+}
+
+

src/ast/bv_decl_plugin.h

@@ -423,6 +423,7 @@ public:
 
     app * mk_ule(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_ULEQ, arg1, arg2); }
     app * mk_sle(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLEQ, arg1, arg2); }
+    app * mk_slt(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_SLT, arg1, arg2); }
     app * mk_extract(unsigned high, unsigned low, expr * n) {
         parameter params[2] = { parameter(high), parameter(low) };
         return m_manager.mk_app(get_fid(), OP_EXTRACT, 2, params, 1, &n);

src/ast/euf/euf_egraph.cpp

@@ -129,7 +129,7 @@ namespace euf {
         return n;
     }
 
-    egraph::egraph(ast_manager& m) : m(m), m_table(m), m_exprs(m) {
+    egraph::egraph(ast_manager& m) : m(m), m_table(m), m_tmp_app(2), m_exprs(m) {
         m_tmp_eq = enode::mk_tmp(m_region, 2);
     }
 
@@ -417,6 +417,7 @@ namespace euf {
             std::swap(r1, r2);
             std::swap(n1, n2);
         }
+
         if (j.is_congruence() && (m.is_false(r2->get_expr()) || m.is_true(r2->get_expr())))
             add_literal(n1, false);
         if (n1->is_equality() && n1->value() == l_false)
@@ -594,6 +595,12 @@ namespace euf {
         return false;
     }
 
+    enode* egraph::get_enode_eq_to(func_decl* f, unsigned num_args, enode* const* args) {
+        m_tmp_app.set_decl(f);
+        m_tmp_app.set_num_args(num_args);
+        return find(m_tmp_app.get_app(), num_args, args);
+    }
+
     /**
        \brief generate an explanation for a congruence.
        Each pair of children under a congruence have the same roots

src/ast/euf/euf_egraph.h

@@ -156,26 +156,27 @@ namespace euf {
         svector<update_record> m_updates;
         unsigned_vector        m_scopes;
         enode_vector           m_expr2enode;
-        enode*                 m_tmp_eq { nullptr };
-        enode*                 m_tmp_node { nullptr };
-        unsigned               m_tmp_node_capacity { 0 };
+        enode*                 m_tmp_eq = nullptr;
+        enode*                 m_tmp_node = nullptr;
+        unsigned               m_tmp_node_capacity = 0;
+        tmp_app                m_tmp_app;
         enode_vector           m_nodes;
         expr_ref_vector        m_exprs;
         vector<enode_vector>   m_decl2enodes;
         enode_vector           m_empty_enodes;
-        unsigned               m_num_scopes { 0 };
-        bool                   m_inconsistent { false };
-        enode                  *m_n1 { nullptr };
-        enode                  *m_n2 { nullptr };
+        unsigned               m_num_scopes = 0;
+        bool                   m_inconsistent = false;
+        enode                  *m_n1 = nullptr;
+        enode                  *m_n2 = nullptr;
         justification          m_justification;
-        unsigned               m_new_lits_qhead { 0 };
-        unsigned               m_new_th_eqs_qhead { 0 };
+        unsigned               m_new_lits_qhead = 0;
+        unsigned               m_new_th_eqs_qhead = 0;
         svector<enode_bool_pair>  m_new_lits;
         svector<th_eq>         m_new_th_eqs;
         bool_vector            m_th_propagates_diseqs;
         enode_vector           m_todo;
         stats                  m_stats;
-        bool                   m_uses_congruence { false };
+        bool                   m_uses_congruence = false;
         std::function<void(enode*,enode*)>     m_on_merge;
         std::function<void(enode*)>            m_on_make;
         std::function<void(expr*,expr*,expr*)> m_used_eq;
@@ -261,7 +262,7 @@ namespace euf {
         */
         bool are_diseq(enode* a, enode* b) const;
 
-        enode * get_enode_eq_to(func_decl * f, unsigned num_args, enode * const * args) { UNREACHABLE(); return nullptr; }
+        enode* get_enode_eq_to(func_decl* f, unsigned num_args, enode* const* args);
 
         /**
            \brief Maintain and update cursor into propagated consequences.
@@ -326,6 +327,7 @@ namespace euf {
         void collect_statistics(statistics& st) const;
 
         unsigned num_scopes() const { return m_scopes.size() + m_num_scopes; }
+        unsigned num_nodes() const { return m_nodes.size(); }
     };
 
     inline std::ostream& operator<<(std::ostream& out, egraph const& g) { return g.display(out); }

src/ast/euf/euf_etable.h

@@ -125,7 +125,7 @@ namespace euf {
 
 
         ast_manager &                 m_manager;
-        bool                          m_commutativity{ false }; //!< true if the last found congruence used commutativity
+        bool                          m_commutativity = false; //!< true if the last found congruence used commutativity
         ptr_vector<void>              m_tables;
         map<decl_info, unsigned, decl_hash, decl_eq>  m_func_decl2id;
 

src/ast/macros/macro_util.cpp

@@ -467,7 +467,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl
    See normalize_expr
 */
 void macro_util::mk_macro_interpretation(app * head, unsigned num_decls, expr * def, expr_ref & interp) const {
-    TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n";);
+    TRACE("macro_util", tout << mk_pp(head, m_manager) << "\n" << mk_pp(def, m_manager) << "\n";);
     SASSERT(is_macro_head(head, head->get_num_args()) ||
             is_quasi_macro_ok(head, head->get_num_args(), def));
     SASSERT(!occurs(head->get_decl(), def));

src/ast/macros/quasi_macros.cpp

@@ -110,10 +110,9 @@ bool quasi_macros::fully_depends_on(app * a, quantifier * q) const {
     // direct argument of a, i.e., a->get_arg(i) == v for some i
     bit_vector bitset;
     bitset.resize(q->get_num_decls(), false);
-    for (unsigned i = 0 ; i < a->get_num_args() ; i++) {
-        if (is_var(a->get_arg(i)))
-            bitset.set(to_var(a->get_arg(i))->get_idx(), true);
-    }
+    for (expr* arg : *a)
+        if (is_var(arg))
+             bitset.set(to_var(arg)->get_idx(), true);
 
     for (unsigned i = 0; i < bitset.size() ; i++) {
         if (!bitset.get(i))
@@ -198,6 +197,7 @@ bool quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
 
     bit_vector v_seen;
     v_seen.resize(q->get_num_decls(), false);
+    unsigned num_seen = 0;
     for (unsigned i = 0; i < a->get_num_args(); ++i) {
         expr* arg = a->get_arg(i);
         if (!is_var(arg) && !is_ground(arg))
@@ -215,8 +215,11 @@ bool quasi_macros::quasi_macro_to_macro(quantifier * q, app * a, expr * t, quant
             var * v = to_var(arg);
             m_new_vars.push_back(v);
             v_seen.set(v->get_idx(), true);
+            ++num_seen;
         }
     }
+    if (num_seen < q->get_num_decls())
+        return false;
 
     // Reverse the new variable names and sorts. [CMW: There is a smarter way to do this.]
     vector<symbol> new_var_names_rev;

src/ast/normal_forms/pull_quant.cpp

@@ -281,9 +281,9 @@ struct pull_quant::imp {
                     m.mk_rewrite(old_q, result);
                 return true;
             }
-            if (is_lambda(old_q)) {
-                return false;
-            }
+
+            if (is_lambda(old_q)) 
+                return false;            
 
             if (!is_forall(new_body))
                 return false;

src/ast/recfun_decl_plugin.cpp

@@ -209,6 +209,7 @@ namespace recfun {
     void def::compute_cases(util& u,
                             replace& subst, 
                             is_immediate_pred & is_i, 
+                            bool is_macro,
                             unsigned n_vars, var *const * vars, expr* rhs)
     {
         VERIFY(m_cases.empty() && "cases cannot already be computed");
@@ -227,7 +228,7 @@ namespace recfun {
         expr_ref_vector conditions(m);
 
         // is the function a macro (unconditional body)?
-        if (n_vars == 0 || !contains_ite(u, rhs)) {
+        if (is_macro || n_vars == 0 || !contains_ite(u, rhs)) {
             // constant function or trivial control flow, only one (dummy) case
             add_case(name, 0, conditions, rhs);
             return;
@@ -335,10 +336,11 @@ namespace recfun {
         return alloc(def, m(), m_fid, name, n, domain, range, is_generated);
     }
 
-
-    void util::set_definition(replace& subst, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
-        expr_ref rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs);        
-        d.set_definition(subst, n_vars, vars, rhs1);
+    void util::set_definition(replace& subst, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) {
+        expr_ref rhs1(rhs, m());
+        if (!is_macro)
+            rhs1 = get_plugin().redirect_ite(subst, n_vars, vars, rhs);        
+        d.set_definition(subst, is_macro, n_vars, vars, rhs1);
     }
 
     app_ref util::mk_num_rounds_pred(unsigned d) {
@@ -369,11 +371,11 @@ namespace recfun {
     };
 
     // set definition 
-    void promise_def::set_definition(replace& r, unsigned n_vars, var * const * vars, expr * rhs) {
+    void promise_def::set_definition(replace& r, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) {
         SASSERT(n_vars == d->get_arity());
                     
         is_imm_pred is_i(*u);
-        d->compute_cases(*u, r, is_i, n_vars, vars, rhs);
+        d->compute_cases(*u, r, is_i, is_macro, n_vars, vars, rhs);
     }
 
     namespace decl {
@@ -426,8 +428,8 @@ namespace recfun {
             }
         }
         
-        void plugin::set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
-            u().set_definition(r, d, n_vars, vars, rhs);
+        void plugin::set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) {
+            u().set_definition(r, d, is_macro, n_vars, vars, rhs);
             for (case_def & c : d.get_def()->get_cases()) {
                 m_case_defs.insert(c.get_decl(), &c);
             }
@@ -437,12 +439,12 @@ namespace recfun {
             return !m_case_defs.empty();            
         }
 
-        def* plugin::mk_def(replace& subst, 
+        def* plugin::mk_def(replace& subst, bool is_macro,
                             symbol const& name, unsigned n, sort ** params, sort * range,
                             unsigned n_vars, var ** vars, expr * rhs) {
             promise_def d = mk_def(name, n, params, range);
             SASSERT(! m_defs.contains(d.get_def()->get_decl()));
-            set_definition(subst, d, n_vars, vars, rhs);
+            set_definition(subst, d, is_macro, n_vars, vars, rhs);
             return d.get_def();
         }
 
@@ -520,7 +522,7 @@ namespace recfun {
                 auto pd = mk_def(fresh_name, n, domain.data(), max_expr->get_sort());
                 func_decl* f = pd.get_def()->get_decl();
                 expr_ref new_body(m().mk_app(f, n, args.data()), m());
-                set_definition(subst, pd, n, vars, max_expr);
+                set_definition(subst, pd, false, n, vars, max_expr);
                 subst.reset();
                 subst.insert(max_expr, new_body);
                 result = subst(result);                
@@ -528,7 +530,6 @@ namespace recfun {
             }
             return result;
         }
-
     }
 
     case_expansion::case_expansion(recfun::util& u, app * n) : 

src/ast/recfun_decl_plugin.h

@@ -114,7 +114,7 @@ namespace recfun {
 
         // compute cases for a function, given its RHS (possibly containing `ite`).
         void compute_cases(util& u, replace& subst, is_immediate_pred &, 
-                           unsigned n_vars, var *const * vars, expr* rhs);
+                           bool is_macro, unsigned n_vars, var *const * vars, expr* rhs);
         void add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr* rhs, bool is_imm = false);
         bool contains_ite(util& u, expr* e); // expression contains a test over a def?
         bool contains_def(util& u, expr* e); // expression contains a def
@@ -138,7 +138,7 @@ namespace recfun {
         friend class util;
         util * u;
         def * d;
-        void set_definition(replace& r, unsigned n_vars, var * const * vars, expr * rhs); // call only once
+        void set_definition(replace& r, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs); // call only once
     public:
         promise_def(util * u, def * d) : u(u), d(d) {}
         promise_def(promise_def const & from) : u(from.u), d(from.d) {}
@@ -182,9 +182,9 @@ namespace recfun {
 
             promise_def ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated = false);
             
-            void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
+            void set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs);
             
-            def* mk_def(replace& subst, symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs);
+            def* mk_def(replace& subst, bool is_macro, symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs);
 
             void erase_def(func_decl* f);
 
@@ -216,7 +216,7 @@ namespace recfun {
         decl::plugin *          m_plugin;
 
         bool compute_is_immediate(expr * rhs);
-        void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
+        void set_definition(replace& r, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs);
 
     public:
         util(ast_manager &m);

src/ast/rewriter/seq_axioms.cpp

@@ -776,48 +776,84 @@ namespace seq {
         rational pow(1);
         for (unsigned i = 0; i < k; ++i)
             pow *= 10;
-        if (k == 0) {
-            ge10k = m.mk_true();            
-        }
-        else {
-            ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b);
-        }
+        ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b);        
         ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b);
         unsigned sz = bv.get_bv_size(b);
         expr_ref_vector es(m);
         expr_ref bb(b, m), ten(bv.mk_numeral(10, sz), m);
-        pow = 1;
+        rational p(1);
         for (unsigned i = 0; i <= k; ++i) {
-            if (pow > 1)
-                bb = bv.mk_bv_udiv(b, bv.mk_numeral(pow, bv_sort));
+            if (p > 1)
+                bb = bv.mk_bv_udiv(b, bv.mk_numeral(p, bv_sort));
             es.push_back(seq.str.mk_unit(m_sk.mk_ubv2ch(bv.mk_bv_urem(bb, ten))));
-            pow *= 10;
+            p *= 10;
         }
         es.reverse();
         eq = m.mk_eq(seq.str.mk_ubv2s(b), seq.str.mk_concat(es, seq.str.mk_string_sort()));
-        add_clause(~ge10k, ge10k1, eq);
+        SASSERT(pow < rational::power_of_two(sz));
+        if (k == 0)
+            add_clause(ge10k1, eq);
+        else if (pow * 10 >= rational::power_of_two(sz))
+            add_clause(~ge10k, eq);
+        else 
+            add_clause(~ge10k, ge10k1, eq);
+    }
+
+    /*
+    * 1 <= len(ubv2s(b)) <= k, where k is min such that 10^k > 2^sz
+    */
+    void axioms::ubv2s_len_axiom(expr* b) {
+        bv_util bv(m);
+        sort* bv_sort = b->get_sort();
+        unsigned sz = bv.get_bv_size(bv_sort);
+        unsigned k = 1;
+        rational pow(10);
+        while (pow <= rational::power_of_two(sz))
+            ++k, pow *= 10;
+        expr_ref len(seq.str.mk_length(seq.str.mk_ubv2s(b)), m);
+        expr_ref ge(a.mk_ge(len, a.mk_int(1)), m);
+        expr_ref le(a.mk_le(len, a.mk_int(k)), m);
+        add_clause(le);
+        add_clause(ge);
     }
 
     /*
     *   len(ubv2s(b)) = k => 10^k-1 <= b < 10^{k}   k > 1
     *   len(ubv2s(b)) = 1 =>  b < 10^{1}   k = 1
+    *   len(ubv2s(b)) >= k => is_digit(nth(ubv2s(b), 0)) & ... & is_digit(nth(ubv2s(b), k-1))
     */
     void axioms::ubv2s_len_axiom(expr* b, unsigned k) {
-        expr_ref ge10k(m), ge10k1(m), eq(m);
+        expr_ref ge10k(m), ge10k1(m), eq(m), is_digit(m);
+        expr_ref ubvs(seq.str.mk_ubv2s(b), m);
+        expr_ref len(seq.str.mk_length(ubvs), m);
+        expr_ref ge_len(a.mk_ge(len, a.mk_int(k)), m);
         bv_util bv(m);
         sort* bv_sort = b->get_sort();
         unsigned sz = bv.get_bv_size(bv_sort);
         rational pow(1);
         for (unsigned i = 1; i < k; ++i)
             pow *= 10;
-        if (pow * 10 >= rational::power_of_two(sz))
-            return; // TODO: add conflict when k is too large or avoid overflow bounds and limits
+
+        if (pow >= rational::power_of_two(sz)) {
+            expr_ref ge(a.mk_ge(len, a.mk_int(k)), m);
+            add_clause(~ge);
+            return;
+        }
+
         ge10k = bv.mk_ule(bv.mk_numeral(pow, bv_sort), b);        
         ge10k1 = bv.mk_ule(bv.mk_numeral(pow * 10, bv_sort), b);
-        eq = m.mk_eq(seq.str.mk_length(seq.str.mk_ubv2s(b)), a.mk_int(k));
-        add_clause(~eq, ~ge10k1);
+        eq = m.mk_eq(len, a.mk_int(k));
+
+        if (pow * 10 < rational::power_of_two(sz))
+            add_clause(~eq, ~ge10k1);
         if (k > 1)
             add_clause(~eq, ge10k);
+
+        for (unsigned i = 0; i < k; ++i) {
+            expr* ch = seq.str.mk_nth_i(ubvs, i);
+            is_digit = seq.mk_char_is_digit(ch);
+            add_clause(~ge_len, is_digit);
+        }
     }
 
     void axioms::ubv2ch_axiom(sort* bv_sort) {

src/ast/rewriter/seq_axioms.h

@@ -96,6 +96,7 @@ namespace seq {
         void itos_axiom(expr* s, unsigned k);
         void ubv2s_axiom(expr* b, unsigned k);
         void ubv2s_len_axiom(expr* b, unsigned k);
+        void ubv2s_len_axiom(expr* b);
         void ubv2ch_axiom(sort* bv_sort);
         void lt_axiom(expr* n);
         void le_axiom(expr* n);

src/ast/rewriter/seq_rewriter.cpp

@@ -672,6 +672,14 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 3);
         st = mk_seq_replace_all(args[0], args[1], args[2], result);
         break;
+    case OP_SEQ_REPLACE_RE:
+        SASSERT(num_args == 3);
+        st = mk_seq_replace_re(args[0], args[1], args[2], result);
+        break;
+    case OP_SEQ_REPLACE_RE_ALL:
+        SASSERT(num_args == 3);
+        st = mk_seq_replace_re_all(args[0], args[1], args[2], result);
+        break;
     case OP_SEQ_TO_RE:
         SASSERT(num_args == 1);
         st = mk_str_to_regexp(args[0], result);
@@ -718,6 +726,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 1);
         st = mk_str_ubv2s(args[0], result);
         break;
+    case OP_STRING_SBVTOS:
+      SASSERT(num_args == 1);
+      st = mk_str_sbv2s(args[0], result);
+      break;
     case _OP_STRING_CONCAT:
     case _OP_STRING_PREFIX:
     case _OP_STRING_SUFFIX:
@@ -1900,6 +1912,8 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref&
         result = str().mk_concat(strs, a->get_sort());
         return BR_REWRITE_FULL;
     }
+    // TBD: add case when a, b are concatenation of units that are values.
+    // in this case we can use a similar loop as for strings.
     return BR_FAILED;
 }
 
@@ -1911,7 +1925,6 @@ br_status seq_rewriter::mk_seq_replace_re(expr* a, expr* b, expr* c, expr_ref& r
     return BR_FAILED;
 }
 
-
 br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     TRACE("seq", tout << mk_pp(a, m()) << " " << mk_pp(b, m()) << "\n";);
     zstring s1, s2;
@@ -2218,6 +2231,30 @@ br_status seq_rewriter::mk_str_ubv2s(expr* a, expr_ref& result) {
     return BR_FAILED;
 }
 
+br_status seq_rewriter::mk_str_sbv2s(expr *a, expr_ref &result) {
+    bv_util bv(m());
+    rational val;
+    unsigned bv_size = 0;
+    if (bv.is_numeral(a, val, bv_size)) {
+        rational r = mod(val, rational::power_of_two(bv_size));
+        SASSERT(!r.is_neg());
+        if (r >= rational::power_of_two(bv_size - 1)) {
+            r -= rational::power_of_two(bv_size);
+        }
+        result = str().mk_string(zstring(r));
+        return BR_DONE;
+    }
+    
+    bv_size = bv.get_bv_size(a);
+    result = m().mk_ite(
+        bv.mk_slt(a,bv.mk_numeral(0, bv_size)),
+        str().mk_concat(
+            str().mk_string(zstring("-")),
+            str().mk_ubv2s(bv.mk_bv_neg(a))
+        ),
+        str().mk_ubv2s(a));
+    return BR_REWRITE_FULL;
+}
 
 br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
     rational r;
@@ -3158,7 +3195,7 @@ expr_ref seq_rewriter::mk_der_cond(expr* cond, expr* ele, sort* seq_sort) {
     expr *c1 = nullptr, *c2 = nullptr, *ch1 = nullptr, *ch2 = nullptr;
     unsigned ch = 0;
     expr_ref result(m()), r1(m()), r2(m());
-    if (m().is_eq(cond, ch1, ch2)) {
+    if (m().is_eq(cond, ch1, ch2) && u().is_char(ch1)) {
         r1 = u().mk_le(ch1, ch2);
         r1 = mk_der_cond(r1, ele, seq_sort);
         r2 = u().mk_le(ch2, ch1);
@@ -3219,11 +3256,17 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
         }
         expr_ref dr2 = mk_derivative(ele, r2);
         is_n = re_predicate(is_n, seq_sort);
-        // Instead of mk_der_union here, we use mk_der_antimorov_union to
-        // force the two cases to be considered separately and lifted to
-        // the top level. This avoids blowup in cases where determinization
-        // is expensive.
-        return mk_der_antimorov_union(result, mk_der_concat(is_n, dr2));
+        if (re().is_empty(dr2)) {
+            //do not concatenate [], it is a deade-end 
+            return result;
+        }
+        else {
+            // Instead of mk_der_union here, we use mk_der_antimorov_union to
+            // force the two cases to be considered separately and lifted to
+            // the top level. This avoids blowup in cases where determinization
+            // is expensive.
+            return mk_der_antimorov_union(result, mk_der_concat(is_n, dr2));
+        }
     }
     else if (re().is_star(r, r1)) {
         return mk_der_concat(mk_derivative(ele, r1), r);
@@ -3256,8 +3299,15 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
         if (lo > 0) {
             lo--;
         }
-        result = re().mk_loop(r1, lo);
-        return mk_der_concat(mk_derivative(ele, r1), result);
+        result = mk_derivative(ele, r1);
+        //do not concatenate with [] (emptyset)
+        if (re().is_empty(result)) {
+            return result;
+        }
+        else {
+            //do not create loop r1{0,}, instead create r1*
+            return mk_der_concat(result, (lo == 0 ? re().mk_star(r1) : re().mk_loop(r1, lo)));
+        }
     }
     else if (re().is_loop(r, r1, lo, hi)) {
         if (hi == 0) {
@@ -3267,8 +3317,14 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
         if (lo > 0) {
             lo--;
         }
-        result = re().mk_loop(r1, lo, hi);
-        return mk_der_concat(mk_derivative(ele, r1), result);
+        result = mk_derivative(ele, r1);
+        //do not concatenate with [] (emptyset) or handle the rest of the loop if no more iterations remain
+        if (re().is_empty(result) || hi == 0) {
+            return result;
+        }
+        else {
+            return mk_der_concat(result, re().mk_loop(r1, lo, hi));
+        }
     }
     else if (re().is_full_seq(r) ||
              re().is_empty(r)) {
@@ -3288,20 +3344,23 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
             return result;
         }
         else if (str().is_empty(r1)) {
+            //observe: str().is_empty(r1) checks that r = () = epsilon
+            //while mk_empty() = [], because deriv(epsilon) = [] = nothing
             return mk_empty();
         }
-#if 0
-        else {
+        else if (str().is_itos(r1, r2)) {
+            //
+            // here r1 = (str.from_int r2) and r2 is non-ground 
+            // or else the expression would have been simplified earlier
+            // so r1 must be nonempty and must consists of decimal digits 
+            // '0' <= elem <= '9'
+            // if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else []
+            //
             hd = str().mk_nth_i(r1, m_autil.mk_int(0));
-            tl = str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1)));
-            result = re().mk_to_re(tl);
-            result = 
-                m().mk_ite(m_br.mk_eq_rw(r1, str().mk_empty(m().get_sort(r1))), 
-                           mk_empty(),
-                           re_and(m_br.mk_eq_rw(ele, hd), result));
-            return result;
+            m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')), m().mk_eq(hd, ele), result); 
+            tl = re().mk_to_re(str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1))));            
+            return re_and(result, tl);
         }
-#endif
     }
     else if (re().is_reverse(r, r1) && re().is_to_re(r1, r2)) {
         // Reverses are rewritten so that the only derivative case is
@@ -3342,6 +3401,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
         }
         expr* e1 = nullptr, *e2 = nullptr;
         if (str().is_unit(r1, e1) && str().is_unit(r2, e2)) {
+  	    SASSERT(u().is_char(e1));
             // Use mk_der_cond to normalize
             STRACE("seq_verbose", tout << "deriv range str" << std::endl;);
             expr_ref p1(u().mk_le(e1, ele), m());
@@ -3900,6 +3960,7 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
     comp(none) -> all
     comp(all) -> none
     comp(comp(e1)) -> e1
+    comp(epsilon) -> .+
 */
 br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
     expr *e1 = nullptr, *e2 = nullptr;
@@ -3923,6 +3984,10 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
         result = e1;
         return BR_DONE;
     }
+    if (re().is_to_re(a, e1) && str().is_empty(e1)) {
+        result = re().mk_plus(re().mk_full_char(a->get_sort()));
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
 
@@ -4110,6 +4175,7 @@ br_status seq_rewriter::mk_re_power(func_decl* f, expr* a, expr_ref& result) {
    a+* = a*
    emp* = ""
    all* = all   
+   .+* = all
 */
 br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
     expr* b, *c, *b1, *c1;
@@ -4132,7 +4198,10 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
         return BR_DONE;
     }
     if (re().is_plus(a, b)) {
-        result = re().mk_star(b);
+        if (re().is_full_char(b))
+            result = re().mk_full_seq(a->get_sort());
+        else
+            result = re().mk_star(b);
         return BR_DONE;
     }
     if (re().is_union(a, b, c)) {

src/ast/rewriter/seq_rewriter.h

@@ -229,6 +229,7 @@ class seq_rewriter {
     br_status mk_str_itos(expr* a, expr_ref& result);
     br_status mk_str_stoi(expr* a, expr_ref& result);
     br_status mk_str_ubv2s(expr* a, expr_ref& result);
+    br_status mk_str_sbv2s(expr* a, expr_ref& result);
     br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result);
     br_status mk_str_to_regexp(expr* a, expr_ref& result);
     br_status mk_str_le(expr* a, expr* b, expr_ref& result);

src/ast/seq_decl_plugin.cpp

@@ -350,7 +350,7 @@ func_decl* seq_decl_plugin::mk_left_assoc_fun(decl_kind k, unsigned arity, sort*
     return mk_assoc_fun(k, arity, domain, range, k_seq, k_string, false);
 }
 
-func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) {
+func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) const {
     ast_manager& m = *m_manager;
     if (arity != 1)
         m.raise_exception("Invalid str.from_ubv expects one bit-vector argument");
@@ -361,6 +361,17 @@ func_decl* seq_decl_plugin::mk_ubv2s(unsigned arity, sort* const* domain) {
     return m.mk_func_decl(symbol("str.from_ubv"), arity, domain, rng, func_decl_info(m_family_id, OP_STRING_UBVTOS));    
 }
 
+func_decl* seq_decl_plugin::mk_sbv2s(unsigned arity, sort* const* domain) const {
+    ast_manager &m = *m_manager;
+    if (arity != 1)
+        m.raise_exception("Invalid str.from_sbv expects one bit-vector argument");
+    bv_util bv(m);
+    if (!bv.is_bv_sort(domain[0]))
+        m.raise_exception("Invalid str.from_sbv expects one bit-vector argument");
+    sort *rng = m_string;
+    return m.mk_func_decl(symbol("str.from_sbv"), arity, domain, rng, func_decl_info(m_family_id, OP_STRING_SBVTOS));
+}
+
 func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq, decl_kind k_string, bool is_right) {
     ast_manager& m = *m_manager;
     sort_ref rng(m);
@@ -376,7 +387,7 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons
 }
 
 
-func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
+func_decl* seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
                                           unsigned arity, sort * const * domain, sort * range) {
     init();
     m_has_seq = true;
@@ -416,8 +427,12 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_STRING_FROM_CODE:
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+
     case OP_STRING_UBVTOS:
-        return mk_ubv2s(arity, domain);        
+        return mk_ubv2s(arity, domain);
+
+    case OP_STRING_SBVTOS:
+        return mk_sbv2s(arity, domain);
 
     case _OP_REGEXP_FULL_CHAR:
         m_has_re = true;
@@ -627,6 +642,7 @@ void seq_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol cons
     op_names.push_back(builtin_name("re.nostr",  _OP_REGEXP_EMPTY));
     op_names.push_back(builtin_name("re.complement", OP_RE_COMPLEMENT));
     op_names.push_back(builtin_name("str.from_ubv", OP_STRING_UBVTOS));
+    op_names.push_back(builtin_name("str.from_sbv", OP_STRING_SBVTOS));
 }
 
 void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

src/ast/seq_decl_plugin.h

@@ -80,6 +80,7 @@ enum seq_op_kind {
     OP_STRING_ITOS,
     OP_STRING_STOI,
     OP_STRING_UBVTOS,
+    OP_STRING_SBVTOS,
     OP_STRING_LT,
     OP_STRING_LE,
     OP_STRING_IS_DIGIT,
@@ -150,7 +151,8 @@ class seq_decl_plugin : public decl_plugin {
     func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq);
     func_decl* mk_left_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq);
     func_decl* mk_assoc_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string, decl_kind k_seq, bool is_right);
-    func_decl* mk_ubv2s(unsigned arity, sort* const* domain);
+    func_decl* mk_ubv2s(unsigned arity, sort* const* domain) const;
+    func_decl* mk_sbv2s(unsigned arity, sort* const* domain) const;
 
 
     void init();
@@ -297,6 +299,7 @@ public:
         app* mk_itos(expr* i) const { return m.mk_app(m_fid, OP_STRING_ITOS, 1, &i); }
         app* mk_stoi(expr* s) const { return m.mk_app(m_fid, OP_STRING_STOI, 1, &s); }
         app* mk_ubv2s(expr* b) const { return m.mk_app(m_fid, OP_STRING_UBVTOS, 1, &b); }
+        app* mk_sbv2s(expr* b) const { return m.mk_app(m_fid, OP_STRING_SBVTOS, 1, &b); }
         app* mk_is_empty(expr* s) const;
         app* mk_lex_lt(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LT, 2, es); }
         app* mk_lex_le(expr* a, expr* b) const { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_LE, 2, es); }
@@ -336,6 +339,7 @@ public:
         bool is_itos(expr const* n)     const { return is_app_of(n, m_fid, OP_STRING_ITOS); }
         bool is_stoi(expr const* n)     const { return is_app_of(n, m_fid, OP_STRING_STOI); }
         bool is_ubv2s(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_UBVTOS); }
+        bool is_sbv2s(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_SBVTOS); }
         bool is_in_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
         bool is_unit(expr const* n)     const { return is_app_of(n, m_fid, OP_SEQ_UNIT); }
         bool is_lt(expr const* n)       const { return is_app_of(n, m_fid, OP_STRING_LT); }
@@ -374,6 +378,7 @@ public:
         MATCH_UNARY(is_itos);
         MATCH_UNARY(is_stoi);
         MATCH_UNARY(is_ubv2s);
+        MATCH_UNARY(is_sbv2s);
         MATCH_UNARY(is_is_digit);
         MATCH_UNARY(is_from_code);
         MATCH_UNARY(is_to_code);

src/cmd_context/cmd_context.cpp

@@ -365,7 +365,7 @@ void cmd_context::insert_macro(symbol const& s, unsigned arity, sort*const* doma
     // recursive functions have opposite calling convention from macros!
     var_subst sub(m(), true);
     expr_ref tt = sub(t, rvars);
-    p.set_definition(replace, d, vars.size(), vars.data(), tt);
+    p.set_definition(replace, d, true, vars.size(), vars.data(), tt);
     register_fun(s, d.get_def()->get_decl());
 }
 
@@ -1004,7 +1004,7 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
     
     recfun::promise_def d = p.get_promise_def(f);
     recfun_replace replace(m());
-    p.set_definition(replace, d, vars.size(), vars.data(), rhs);
+    p.set_definition(replace, d, false, vars.size(), vars.data(), rhs);
 }
 
 func_decl * cmd_context::find_func_decl(symbol const & s) const {

src/math/simplex/model_based_opt.cpp

@@ -134,7 +134,15 @@ namespace opt {
     }
 
     void model_based_opt::def::normalize() {
-        SASSERT(m_div.is_int());
+        if (!m_div.is_int()) {
+            rational den = denominator(m_div);
+            SASSERT(den > 1);
+            for (var& v : m_vars)
+                v.m_coeff *= den;
+            m_coeff *= den;
+            m_div *= den;
+
+        }
         if (m_div.is_neg()) {
             for (var& v : m_vars)
                 v.m_coeff.neg();
@@ -528,6 +536,13 @@ namespace opt {
         }
     }
 
+    /**
+    * a1 > 0
+    * a1*x + r1 = value
+    * a2*x + r2 <= 0
+    * ------------------
+    * a1*r2 - a2*r1 <= value
+    */
     void model_based_opt::solve(unsigned row_src, rational const& a1, unsigned row_dst, unsigned x) {
         SASSERT(a1 == get_coefficient(row_src, x));
         SASSERT(a1.is_pos());
@@ -1195,22 +1210,25 @@ namespace opt {
     model_based_opt::def model_based_opt::solve_for(unsigned row_id1, unsigned x, bool compute_def) {
         TRACE("opt", tout << "v" << x << " := " << eval(x) << "\n" << m_rows[row_id1] << "\n";);
         rational a = get_coefficient(row_id1, x), b;
-        ineq_type ty = m_rows[row_id1].m_type;
+        row& r1 = m_rows[row_id1];
+        ineq_type ty = r1.m_type;
         SASSERT(!a.is_zero());
-        SASSERT(m_rows[row_id1].m_alive);
+        SASSERT(r1.m_alive);
         if (a.is_neg()) {
             a.neg();
-            m_rows[row_id1].neg();
+            r1.neg();
         }
         SASSERT(a.is_pos());
         if (ty == t_lt) {
             SASSERT(compute_def);
-            m_rows[row_id1].m_coeff += a;      
-            m_rows[row_id1].m_type = t_le;
-            m_rows[row_id1].m_value += a;
-        }
-        if (m_var2is_int[x] && !a.is_one()) {
-            row& r1 = m_rows[row_id1];
+            r1.m_coeff -= r1.m_value;
+            r1.m_type = t_le;
+            r1.m_value = 0;
+        }        
+
+        if (m_var2is_int[x] && !a.is_one()) {            
+            r1.m_coeff -= r1.m_value;
+            r1.m_value = 0;
             vector<var> coeffs;
             mk_coeffs_without(coeffs, r1.m_vars, x);
             rational c = mod(-eval(coeffs), a);

src/model/model.cpp

@@ -22,6 +22,7 @@ Revision History:
 #include "ast/ast_ll_pp.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/rewriter/th_rewriter.h"
+#include "ast/rewriter/expr_safe_replace.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/recfun_decl_plugin.h"
@@ -605,12 +606,13 @@ void model::add_rec_funs() {
                 
         func_interp* fi = alloc(func_interp, m, f->get_arity());
         // reverse argument order so that variable 0 starts at the beginning.
-        expr_ref_vector subst(m);
-        for (unsigned i = 0; i < f->get_arity(); ++i) {
-            subst.push_back(m.mk_var(i, f->get_domain(i)));
+        expr_safe_replace subst(m);
+        unsigned arity = f->get_arity();
+        for (unsigned i = 0; i < arity; ++i) {
+            subst.insert(m.mk_var(arity - i - 1, f->get_domain(i)), m.mk_var(i, f->get_domain(i)));            
         }
-        var_subst sub(m, true);
-        expr_ref bodyr = sub(rhs, subst);
+        expr_ref bodyr(m);
+        subst(rhs, bodyr);
         
         fi->set_else(bodyr);
         register_decl(f, fi);

src/model/model_evaluator.cpp

@@ -150,9 +150,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
     br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
         auto st = reduce_app_core(f, num, args, result, result_pr);
         CTRACE("model_evaluator", st != BR_FAILED, 
-               tout << f->get_name() << "\n";
-               for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << "\n";
-               tout << result << "\n";);
+               tout << f->get_name() << "  ";
+               for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << " ";
+               tout << "\n--> " << result << "\n";);
                
         return st;
     }

src/muz/spacer/spacer_manager.cpp

@@ -247,7 +247,7 @@ bool is_zk_const (const app *a, int &n) {
 }
 bool sk_lt_proc::operator()(const app *a1, const app *a2) {
     if (a1 == a2) return false;
-    int n1, n2;
+    int n1 = 0, n2 = 0;
     bool z1, z2;
     z1 = is_zk_const(a1, n1);
     z2 = is_zk_const(a2, n2);

src/opt/maxres.cpp

@@ -871,6 +871,8 @@ public:
         m_dump_benchmarks =         p.dump_benchmarks();
         m_enable_lns =              p.enable_lns(); 
         m_lns_conflicts =           p.lns_conflicts();
+	if (m_c.num_objectives() > 1)
+	  m_add_upper_bound_block = false;
     }
 
     lbool init_local() {

src/parsers/smt2/smt2parser.cpp

@@ -3118,6 +3118,23 @@ namespace smt2 {
             return sexpr_ref(nullptr, sm());
         }
 
+        sort_ref parse_sort_ref(char const* context) {
+            m_num_bindings    = 0;
+            m_num_open_paren = 0;
+
+            try {
+                scan_core();
+                parse_sort(context);
+                if (!sort_stack().empty()) 
+                    return sort_ref(sort_stack().back(), m());
+            }
+            catch (z3_exception & ex) {
+                error(ex.msg());
+            }
+            return sort_ref(nullptr, m());
+        }
+
+
         bool operator()() {
             m_num_bindings    = 0;
             unsigned found_errors = 0;
@@ -3190,6 +3207,11 @@ bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive,
     return p();
 }
 
+sort_ref parse_smt2_sort(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename) {
+    smt2::parser p(ctx, is, interactive, ps, filename);
+    return p.parse_sort_ref(filename);
+}
+
 sexpr_ref parse_sexpr(cmd_context& ctx, std::istream& is, params_ref const& ps, char const* filename) {
     smt2::parser p(ctx, is, false, ps, filename);
     return p.parse_sexpr_ref();

src/parsers/smt2/smt2parser.h

@@ -24,3 +24,4 @@ bool parse_smt2_commands(cmd_context & ctx, std::istream & is, bool interactive
 
 sexpr_ref parse_sexpr(cmd_context& ctx, std::istream& is, params_ref const& ps, char const* filename);
 
+sort_ref parse_smt2_sort(cmd_context & ctx, std::istream & is, bool interactive, params_ref const & ps, char const * filename);

src/qe/mbp/mbp_arith.cpp

@@ -47,7 +47,6 @@ namespace mbp {
         ~imp() {}
 
         void insert_mul(expr* x, rational const& v, obj_map<expr, rational>& ts) {
-            // TRACE("qe", tout << "Adding variable " << mk_pp(x, m) << " " << v << "\n";);
             rational w;
             if (ts.find(x, w)) 
                 ts.insert(x, w + v);            
@@ -320,6 +319,14 @@ namespace mbp {
                     tids.insert(v, mbo.add_var(r, a.is_int(v)));
                 }
             }
+
+            // bail on variables in non-linear sub-terms
+            for (auto& kv : tids) {
+                expr* e = kv.m_key;
+                if (is_arith(e) && !var_mark.is_marked(e)) 
+                    mark_rec(fmls_mark, e);                
+            }
+
             if (m_check_purified) {
                 for (expr* fml : fmls) 
                     mark_rec(fmls_mark, fml);                
@@ -362,6 +369,10 @@ namespace mbp {
                 optdefs2mbpdef(defs, index2expr, real_vars, result);     
             if (m_apply_projection)
                 apply_projection(result, fmls);
+            TRACE("qe",
+                for (auto [v, t] : result)
+                    tout << v << " := " << t << "\n";
+                tout << "fmls:" << fmls << "\n";);
             return result;
         }        
 

src/qe/mbp/mbp_plugin.cpp

@@ -95,6 +95,97 @@ namespace mbp {
             lits.push_back(e);
     }
 
+    bool project_plugin::reduce(model_evaluator& eval, model& model, expr* fml, expr_ref_vector& fmls) {
+        expr* nfml, * f1, * f2, * f3;
+        expr_ref val(m);
+        if (m.is_not(fml, nfml) && m.is_distinct(nfml))
+            push_back(fmls, pick_equality(m, model, nfml));
+        else if (m.is_or(fml)) {
+            for (expr* arg : *to_app(fml)) {
+                val = eval(arg);
+                if (m.is_true(val)) {
+                    fmls.push_back(arg);
+                    break;
+                }
+            }
+        }
+        else if (m.is_and(fml)) {
+            fmls.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
+        }
+        else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) {
+            val = eval(f1);
+            if (m.is_false(val)) {
+                push_back(fmls, mk_not(m, f1));
+                push_back(fmls, mk_not(m, f2));
+            }
+            else {
+                push_back(fmls, f1);
+                push_back(fmls, f2);
+            }
+        }
+        else if (m.is_implies(fml, f1, f2)) {
+            val = eval(f2);
+            if (m.is_true(val))
+                push_back(fmls, f2);
+            else
+                push_back(fmls, mk_not(m, f1));
+        }
+        else if (m.is_ite(fml, f1, f2, f3)) {
+            val = eval(f1);
+            if (m.is_true(val)) {
+                push_back(fmls, f1);
+                push_back(fmls, f2);
+            }
+            else {
+                push_back(fmls, mk_not(m, f1));
+                push_back(fmls, f3);
+            }
+        }
+        else if (m.is_not(fml, nfml) && m.is_not(nfml, nfml)) {
+            push_back(fmls, nfml);
+        }
+        else if (m.is_not(fml, nfml) && m.is_and(nfml)) {
+            for (expr* arg : *to_app(nfml)) {
+                val = eval(arg);
+                if (m.is_false(val)) {
+                    push_back(fmls, mk_not(m, arg));
+                    break;
+                }
+            }
+        }
+        else if (m.is_not(fml, nfml) && m.is_or(nfml)) {
+            for (expr* arg : *to_app(nfml))
+                push_back(fmls, mk_not(m, arg));
+        }
+        else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) {
+            val = eval(f1);
+            if (m.is_true(val))
+                f2 = mk_not(m, f2);
+            else
+                f1 = mk_not(m, f1);
+            push_back(fmls, f1);
+            push_back(fmls, f2);
+        }
+        else if (m.is_not(fml, nfml) && m.is_implies(nfml, f1, f2)) {
+            push_back(fmls, f1);
+            push_back(fmls, mk_not(m, f2));
+        }
+        else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) {
+            val = eval(f1);
+            if (m.is_true(val)) {
+                push_back(fmls, f1);
+                push_back(fmls, mk_not(m, f2));
+            }
+            else {
+                push_back(fmls, mk_not(m, f1));
+                push_back(fmls, mk_not(m, f3));
+            }
+        }
+        else
+            return false;
+        return true;
+    }
+
     void project_plugin::extract_literals(model& model, app_ref_vector const& vars, expr_ref_vector& fmls) {
         m_cache.reset();
         m_bool_visited.reset();
@@ -105,100 +196,9 @@ namespace mbp {
         DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n" << model;); SASSERT(!m.is_false(eval(fml))); });
 
         for (unsigned i = 0; i < fmls.size(); ++i) {
-            expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3;
-            SASSERT(m.is_bool(fml));
-            if (m.is_not(fml, nfml) && m.is_distinct(nfml))
-                fmls[i--] = pick_equality(m, model, nfml);
-            else if (m.is_or(fml)) {
-                for (expr* arg : *to_app(fml)) {
-                    val = eval(arg);
-                    if (m.is_true(val)) {
-                        fmls[i] = arg;
-                        --i;
-                        break;
-                    }
-                }
-            }
-            else if (m.is_and(fml)) {
-                fmls.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
-                erase(fmls, i);
-            }
-            else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) {
-                val = eval(f1);
-                if (m.is_false(val)) {
-                    f1 = mk_not(m, f1);
-                    f2 = mk_not(m, f2);
-                }
-                fmls[i--] = f1;
-                push_back(fmls, f2);
-            }
-            else if (m.is_implies(fml, f1, f2)) {
-                val = eval(f2);
-                if (m.is_true(val)) {
-                    fmls[i] = f2;
-                }
-                else {
-                    fmls[i] = mk_not(m, f1);
-                }
-                --i;
-            }
-            else if (m.is_ite(fml, f1, f2, f3)) {
-                val = eval(f1);
-                if (m.is_true(val)) {
-                    push_back(fmls, f1);
-                    push_back(fmls, f2);
-                }
-                else {
-                    push_back(fmls, mk_not(m, f1));
-                    push_back(fmls, f3);
-                }
-                erase(fmls, i);
-            }
-            else if (m.is_not(fml, nfml) && m.is_not(nfml, nfml)) {
-                push_back(fmls, nfml);
-                erase(fmls, i);
-            }
-            else if (m.is_not(fml, nfml) && m.is_and(nfml)) {
-                for (expr* arg : *to_app(nfml)) {
-                    val = eval(arg);
-                    if (m.is_false(val)) {
-                        fmls[i--] = mk_not(m, arg);
-                        break;
-                    }
-                }
-            }
-            else if (m.is_not(fml, nfml) && m.is_or(nfml)) {
-                for (expr* arg : *to_app(nfml))
-                    push_back(fmls, mk_not(m, arg));
-                erase(fmls, i);
-            }
-            else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) {
-                val = eval(f1);
-                if (m.is_true(val)) 
-                    f2 = mk_not(m, f2);                
-                else 
-                    f1 = mk_not(m, f1);                
-                push_back(fmls, f1);
-                push_back(fmls, f2);
-                erase(fmls, i);
-            }
-            else if (m.is_not(fml, nfml) && m.is_implies(nfml, f1, f2)) {
-                push_back(fmls, f1);
-                push_back(fmls, mk_not(m, f2));
-                erase(fmls, i);
-            }
-            else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) {
-                val = eval(f1);
-                if (m.is_true(val)) {
-                    push_back(fmls, f1);
-                    push_back(fmls, mk_not(m, f2));
-                }
-                else {
-                    push_back(fmls, mk_not(m, f1));
-                    push_back(fmls, mk_not(m, f3));
-                }
-                erase(fmls, i);
-            }
+            expr* nfml, * fml = fmls.get(i);
+            if (reduce(eval, model, fml, fmls)) 
+                erase(fmls, i);            
             else if (m.is_not(fml, nfml))
                 extract_bools(eval, fmls, i, nfml, false);
             else

src/qe/mbp/mbp_plugin.h

@@ -43,6 +43,7 @@ namespace mbp {
         expr_mark        m_non_ground;
         expr_ref_vector  m_cache, m_args, m_pure_eqs;
 
+        bool reduce(model_evaluator& eval, model& model, expr* fml, expr_ref_vector& fmls);
         void extract_bools(model_evaluator& eval, expr_ref_vector& fmls, unsigned i, expr* fml, bool is_true);
         void visit_app(expr* e);
         bool visit_ite(model_evaluator& eval, expr* e, expr_ref_vector& fmls);

src/sat/dimacs.cpp

@@ -165,6 +165,10 @@ namespace dimacs {
             return out << "f " << r.m_node_id << " " << r.m_name << " " << r.m_args << "0\n";
         case drat_record::tag_t::is_bool_def:
             return out << "b " << r.m_node_id << " " << r.m_args << "0\n";
+        case drat_record::tag_t::is_var:
+            return out << "v " << r.m_node_id << " " << r.m_name << " " << r.m_args << "0\n";
+        case drat_record::tag_t::is_quantifier:
+            return out << "q " << r.m_node_id << " " << r.m_name << " " << r.m_args << "0\n";
         }
         return out;
     }
@@ -256,6 +260,23 @@ namespace dimacs {
                 m_record.m_args.push_back(n);
             }
         };
+        auto parse_var = [&]() {
+            ++in;
+            skip_whitespace(in);
+            n = parse_int(in, err);                    
+            skip_whitespace(in);
+            m_record.m_name = parse_sexpr();
+            m_record.m_tag = drat_record::tag_t::is_var;
+            m_record.m_node_id = n;
+            m_record.m_args.reset();
+            n = parse_int(in, err);
+            if (n < 0)
+                throw lex_error();
+            m_record.m_args.push_back(n);
+            n = parse_int(in, err);
+            if (n != 0)
+                throw lex_error();
+        };
         try {
         loop:
             skip_whitespace(in);
@@ -290,6 +311,12 @@ namespace dimacs {
                 // parse expression definition
                 parse_ast(drat_record::tag_t::is_node);
                 break;
+            case 'v':
+                parse_var();
+                break;
+            case 'q':
+                parse_ast(drat_record::tag_t::is_quantifier);
+                break;
             case 'f':
                 // parse function declaration
                 parse_ast(drat_record::tag_t::is_decl);

src/sat/dimacs.h

@@ -53,7 +53,7 @@ namespace dimacs {
     };
 
     struct drat_record {
-        enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def };
+        enum class tag_t { is_clause, is_node, is_decl, is_sort, is_bool_def, is_var, is_quantifier };
         tag_t            m_tag{ tag_t::is_clause };
         // a clause populates m_lits and m_status
         // a node populates m_node_id, m_name, m_args

src/sat/sat_drat.cpp

@@ -37,9 +37,8 @@ namespace sat {
         if (s.get_config().m_drat && s.get_config().m_drat_file.is_non_empty_string()) {
             auto mode = s.get_config().m_drat_binary ? (std::ios_base::binary | std::ios_base::out | std::ios_base::trunc) : std::ios_base::out;
             m_out = alloc(std::ofstream, s.get_config().m_drat_file.str(), mode);
-            if (s.get_config().m_drat_binary) {
-                std::swap(m_out, m_bout);
-            }
+            if (s.get_config().m_drat_binary) 
+                std::swap(m_out, m_bout);            
         }
     }
 
@@ -50,9 +49,8 @@ namespace sat {
         dealloc(m_bout);
         for (unsigned i = 0; i < m_proof.size(); ++i) {
             clause* c = m_proof[i];
-            if (c) {
-                m_alloc.del_clause(c);
-            }
+            if (c) 
+                m_alloc.del_clause(c);            
         }
         m_proof.reset();
         m_out = nullptr;
@@ -133,7 +131,7 @@ namespace sat {
             memcpy(buffer + len, d, lastd - d);
             len += static_cast<unsigned>(lastd - d);
             buffer[len++] = ' ';
-            if (len + 50 > sizeof(buffer)) {
+            if (static_cast<size_t>(len) + 50 > sizeof(buffer)) {
                 m_out->write(buffer, len);
                 len = 0;
             }
@@ -208,15 +206,14 @@ namespace sat {
 
         declare(l);
         IF_VERBOSE(20, trace(verbose_stream(), 1, &l, st););
-        if (st.is_redundant() && st.is_sat()) {
+        if (st.is_redundant() && st.is_sat()) 
             verify(1, &l);
-        }
-        if (st.is_deleted()) {
+        
+        if (st.is_deleted()) 
             return;
-        }
-        if (m_check_unsat) {
-            assign_propagate(l);
-        }
+        
+        if (m_check_unsat) 
+            assign_propagate(l);        
 
         m_units.push_back(l);
     }
@@ -233,9 +230,9 @@ namespace sat {
             // don't record binary as deleted.
         }
         else {
-            if (st.is_redundant() && st.is_sat()) {
+            if (st.is_redundant() && st.is_sat()) 
                 verify(2, lits);
-            }
+            
             clause* c = m_alloc.mk_clause(2, lits, st.is_redundant());
             m_proof.push_back(c);
             m_status.push_back(st);
@@ -245,15 +242,12 @@ namespace sat {
             m_watches[(~l1).index()].push_back(idx);
             m_watches[(~l2).index()].push_back(idx);
 
-            if (value(l1) == l_false && value(l2) == l_false) {
-                m_inconsistent = true;
-            }
-            else if (value(l1) == l_false) {
-                assign_propagate(l2);
-            }
-            else if (value(l2) == l_false) {
-                assign_propagate(l1);
-            }
+            if (value(l1) == l_false && value(l2) == l_false) 
+                m_inconsistent = true;            
+            else if (value(l1) == l_false) 
+                assign_propagate(l2);            
+            else if (value(l2) == l_false) 
+                assign_propagate(l1);            
         }
     }
 
@@ -403,16 +397,14 @@ namespace sat {
         if (n == 0)
             return false;
         unsigned num_units = m_units.size();
-        for (unsigned i = 0; !m_inconsistent && i < n; ++i) {
+        for (unsigned i = 0; !m_inconsistent && i < n; ++i) 
             assign_propagate(~c[i]);
-        }
-        if (!m_inconsistent) {
-            DEBUG_CODE(validate_propagation(););
-        }
+        
+        DEBUG_CODE(if (!m_inconsistent) validate_propagation(););        
         DEBUG_CODE(
-            for (literal u : m_units) {
+            for (literal u : m_units) 
                 SASSERT(m_assignment[u.var()] != l_undef);
-            });
+            );
 
 #if 0
         if (!m_inconsistent) {
@@ -465,9 +457,9 @@ namespace sat {
         }
 #endif
 
-        for (unsigned i = num_units; i < m_units.size(); ++i) {
+        for (unsigned i = num_units; i < m_units.size(); ++i) 
             m_assignment[m_units[i].var()] = l_undef;
-        }
+        
         m_units.shrink(num_units);
         bool ok = m_inconsistent;
         m_inconsistent = false;

src/sat/sat_simplifier.cpp

@@ -656,6 +656,7 @@ namespace sat {
         s.propagate_core(false); // must not use propagate(), since s.m_clauses is not in a consistent state.
         if (s.inconsistent())
             return;
+        m_use_list.reserve(s.num_vars());
         unsigned new_trail_sz = s.m_trail.size();
         for (unsigned i = old_trail_sz; i < new_trail_sz; i++) {
             literal l = s.m_trail[i];

src/sat/sat_simplifier.h

@@ -40,15 +40,17 @@ namespace sat {
 
     class use_list {
         vector<clause_use_list> m_use_list;
+        
     public:
         void init(unsigned num_vars);
+        void reserve(unsigned num_vars) { while (m_use_list.size() <= 2*num_vars) m_use_list.push_back(clause_use_list()); }
         void insert(clause & c);
         void block(clause & c);
         void unblock(clause & c);
         void erase(clause & c);
         void erase(clause & c, literal l);
-        clause_use_list & get(literal l) { return m_use_list[l.index()]; }
-        clause_use_list const & get(literal l) const { return m_use_list[l.index()]; }
+        clause_use_list& get(literal l) { return m_use_list[l.index()]; }
+        clause_use_list const& get(literal l) const { return m_use_list[l.index()]; }
         void finalize() { m_use_list.finalize(); }
         std::ostream& display(std::ostream& out, literal l) const { return m_use_list[l.index()].display(out); }
     };

src/sat/sat_solver.cpp

@@ -1304,7 +1304,8 @@ namespace sat {
         flet<bool> _searching(m_searching, true);
         m_clone = nullptr;
         if (m_mc.empty() && gparams::get_ref().get_bool("model_validate", false)) {
-            m_clone = alloc(solver, m_params, m_rlimit);
+            
+            m_clone = alloc(solver, m_no_drat_params, m_rlimit);
             m_clone->copy(*this);
             m_clone->set_extension(nullptr);
         }

src/sat/sat_solver.h

@@ -82,6 +82,10 @@ namespace sat {
         void reset();
         void collect_statistics(statistics & st) const;
     };
+
+    struct no_drat_params : public params_ref {
+        no_drat_params() { set_sym("drat.file", symbol()); }        
+    };
     
     class solver : public solver_core {
     public:
@@ -183,6 +187,7 @@ namespace sat {
         scoped_limit_trail      m_vars_lim;
         stopwatch               m_stopwatch;
         params_ref              m_params;
+        no_drat_params          m_no_drat_params;
         scoped_ptr<solver>      m_clone; // for debugging purposes
         literal_vector          m_assumptions;      // additional assumptions during check
         literal_set             m_assumption_set;   // set of enabled assumptions

src/sat/smt/array_axioms.cpp

@@ -427,9 +427,11 @@ namespace array {
             app_ref sel1(m), sel2(m);
             sel1 = a.mk_select(args1);
             sel2 = a.mk_select(args2);
+            prop |= !ctx.get_enode(sel1) || !ctx.get_enode(sel2);
             if (ctx.propagate(e_internalize(sel1), e_internalize(sel2), array_axiom()))
                 prop = true;
         }
+        prop |= !ctx.get_enode(def1) || !ctx.get_enode(def2);
         if (ctx.propagate(e_internalize(def1), e_internalize(def2), array_axiom()))
             prop = true;
         return prop;
@@ -538,7 +540,7 @@ namespace array {
             for (euf::enode* p : euf::enode_parents(n))
                 has_default |= a.is_default(p->get_expr());
             if (has_default)
-                propagate_parent_default(v);            
+                propagate_parent_default(v);      
         }
         bool change = false;
         unsigned sz = m_axiom_trail.size();

src/sat/smt/array_internalize.cpp

@@ -177,6 +177,8 @@ namespace array {
         auto set_index = [&](euf::enode* arg) { if (arg->get_root() == r) is_index = true; };
         auto set_value = [&](euf::enode* arg) { if (arg->get_root() == r) is_value = true; };
 
+        if (a.is_ext(n->get_expr()))
+            return true;
         for (euf::enode* parent : euf::enode_parents(r)) {
             app* p = parent->get_app();
             unsigned num_args = parent->num_args();
@@ -193,7 +195,7 @@ namespace array {
             }
             else if (a.is_const(p)) {
                 set_value(parent->get_arg(0));
-            }
+            }            
             if (is_array + is_index + is_value > 1)
                 return true;
         }

src/sat/smt/array_model.cpp

@@ -26,8 +26,8 @@ namespace array {
         if (!a.is_array(n->get_expr())) {
             dep.insert(n, nullptr);
             return true;
-        }
-        for (euf::enode* p : euf::enode_parents(n)) {
+        }       
+        for (euf::enode* p : euf::enode_parents(n->get_root())) {
             if (a.is_default(p->get_expr())) {
                 dep.add(n, p);
                 continue;
@@ -51,6 +51,7 @@ namespace array {
         SASSERT(a.is_array(n->get_expr()));
         ptr_vector<expr> args;
         sort* srt = n->get_sort();
+        n = n->get_root();
         unsigned arity = get_array_arity(srt);
         func_decl * f    = mk_aux_decl_for_array_sort(m, srt);
         func_interp * fi = alloc(func_interp, m, arity);
@@ -70,7 +71,7 @@ namespace array {
             expr* else_value = nullptr;
             unsigned max_occ_num = 0;
             obj_map<expr, unsigned> num_occ;
-            for (euf::enode* p : euf::enode_parents(n)) {
+            for (euf::enode* p : euf::enode_parents(n->get_root())) {
                 if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n->get_root()) {
                     expr* v = values.get(p->get_root_id());
                     if (!v)
@@ -90,7 +91,7 @@ namespace array {
         }
 
         for (euf::enode* p : euf::enode_parents(n)) {
-            if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n->get_root()) {
+            if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n) {
                 expr* value = values.get(p->get_root_id());
                 if (!value || value == fi->get_else())
                     continue;
@@ -102,7 +103,7 @@ namespace array {
         }
         
         parameter p(f);
-        values.set(n->get_root_id(), m.mk_app(get_id(), OP_AS_ARRAY, 1, &p));
+        values.set(n->get_expr_id(), m.mk_app(get_id(), OP_AS_ARRAY, 1, &p));
     }
 
 

src/sat/smt/array_solver.cpp

@@ -174,8 +174,10 @@ namespace array {
         ctx.push_vec(get_var_data(v_child).m_parent_selects, select);
         euf::enode* child = var2enode(v_child);
         TRACE("array", tout << "v" << v_child << " - " << ctx.bpp(select) << " " << ctx.bpp(child) << " prop: " << should_prop_upward(get_var_data(v_child)) << "\n";);
+        TRACE("array", tout << "can beta reduce " << can_beta_reduce(child) << "\n";);
         if (can_beta_reduce(child)) 
             push_axiom(select_axiom(select, child));
+        propagate_parent_select_axioms(v_child);
     }
 
     void solver::add_lambda(theory_var v, euf::enode* lambda) {
@@ -226,6 +228,12 @@ namespace array {
         
         auto& d = get_var_data(v);
 
+        for (euf::enode* lambda : d.m_lambdas) {
+            expr* e = lambda->get_expr();
+            if (a.is_const(e) || a.is_map(e)) 
+                propagate_select_axioms(d, lambda);
+        }
+        
         for (euf::enode* lambda : d.m_parent_lambdas)
             propagate_select_axioms(d, lambda);
     }

src/sat/smt/bv_internalize.cpp

@@ -653,9 +653,8 @@ namespace bv {
         if (!argn->is_attached_to(get_id())) {
             mk_var(argn);
         }        
-        theory_var v_arg = argn->get_th_var(get_id());
-        unsigned arg_sz = get_bv_size(v_arg);
-        SASSERT(idx < arg_sz);
+        theory_var v_arg = argn->get_th_var(get_id());        
+        SASSERT(idx < get_bv_size(v_arg));
         sat::literal lit = expr2literal(n);
         sat::literal lit0 = m_bits[v_arg][idx];
         if (lit0 == sat::null_literal) {

src/sat/smt/bv_solver.cpp

@@ -478,6 +478,9 @@ namespace bv {
             if (!assign_bit(bit2, v1, v2, idx, bit1, false))
                 break;
         }
+        if (s().value(m_bits[v1][m_wpos[v1]]) != l_undef)
+            find_wpos(v1);
+
         return num_assigned > 0;
     }
 

src/sat/smt/dt_solver.cpp

@@ -714,6 +714,7 @@ namespace dt {
         if (v == euf::null_theory_var) 
             return false;
         euf::enode* con = m_var_data[m_find.find(v)]->m_constructor;
+        CTRACE("dt", !con, display(tout) << ctx.bpp(n) << "\n";);
         if (con->num_args() == 0)
             dep.insert(n, nullptr);
         for (enode* arg : euf::enode_args(con))

src/sat/smt/euf_internalize.cpp

@@ -34,7 +34,11 @@ namespace euf {
 
     sat::literal solver::mk_literal(expr* e) {
         expr_ref _e(e, m);
-        return internalize(e, false, false, m_is_redundant);
+        bool is_not = m.is_not(e, e);
+        sat::literal lit = internalize(e, false, false, m_is_redundant);
+        if (is_not)
+            lit.neg();
+        return lit;
     }
 
     sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) {
@@ -129,8 +133,7 @@ namespace euf {
     sat::literal solver::attach_lit(literal lit, expr* e) {
         sat::bool_var v = lit.var();       
         s().set_external(v);
-        s().set_eliminated(v, false);   
-
+        s().set_eliminated(v, false);           
 
         if (lit.sign()) {
             v = si.add_bool_var(e);
@@ -281,17 +284,11 @@ namespace euf {
                 s().add_clause(1, &lit_th, st);
             }
             else {
-                sat::bool_var v = si.to_bool_var(c);
-                s().set_external(v);
-                VERIFY(v != sat::null_bool_var);
-                VERIFY(s().is_external(v));
-                SASSERT(v != sat::null_bool_var);
-                VERIFY(!s().was_eliminated(v));
+                sat::literal lit_c = mk_literal(c);
                 expr_ref eq_el = mk_eq(e, el);
-
                 sat::literal lit_el = mk_literal(eq_el);
-                literal lits1[2] = { literal(v, true),  lit_th };
-                literal lits2[2] = { literal(v, false), lit_el };
+                literal lits1[2] = { ~lit_c,  lit_th };
+                literal lits2[2] = { lit_c, lit_el };
                 s().add_clause(2, lits1, st);
                 s().add_clause(2, lits2, st);
             }

src/sat/smt/euf_model.cpp

@@ -61,6 +61,7 @@ namespace euf {
     };
 
     void solver::update_model(model_ref& mdl) {
+        mdl->reset_eval_cache();
         for (auto* mb : m_solvers)
             mb->init_model();
         m_values.reset();
@@ -178,6 +179,10 @@ namespace euf {
                 mbS->add_value(n, *mdl, m_values);
             else if (auto* mbE = expr2solver(e))
                 mbE->add_value(n, *mdl, m_values);
+            else if (is_app(e) && to_app(e)->get_family_id() != m.get_basic_family_id()) {
+                m_values.set(id, e);
+                IF_VERBOSE(1, verbose_stream() << "creating self-value for " << mk_pp(e, m) << "\n");
+            }
             else {
                 IF_VERBOSE(1, verbose_stream() << "no model values created for " << mk_pp(e, m) << "\n");
             }                
@@ -212,9 +217,10 @@ namespace euf {
                 args.reset();                
                 for (expr* arg : *a) {
                     enode* earg = get_enode(arg); 
-                    args.push_back(m_values.get(earg->get_root_id()));                
-                    CTRACE("euf", !args.back(), tout << "no value for " << bpp(earg) << "\n";);
-                    SASSERT(args.back());
+                    expr* val = m_values.get(earg->get_root_id());
+                    args.push_back(val);                
+                    CTRACE("euf", !val, tout << "no value for " << bpp(earg) << "\n";);
+                    SASSERT(val);
                 }
                 SASSERT(args.size() == arity);
                 if (!fi->get_entry(args.data()))
@@ -278,6 +284,7 @@ namespace euf {
                    tout << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
                    s().display(tout);
                    tout << mdl << "\n";);
+            (void)first;
             first = false;
         }
         

src/sat/smt/euf_proof.cpp

@@ -33,20 +33,32 @@ namespace euf {
             drat_log_decl(a->get_decl());
             std::stringstream strm;
             strm << mk_ismt2_func(a->get_decl(), m);
-            if (a->get_num_parameters() == 0)
-                get_drat().def_begin('e', e->get_id(), strm.str());
-            else {
-                get_drat().def_begin('e', e->get_id(), strm.str());
-            }
+            get_drat().def_begin('e', e->get_id(), strm.str());
             for (expr* arg : *a)
                 get_drat().def_add_arg(arg->get_id());
             get_drat().def_end();
-            m_drat_asts.insert(e);
-            push(insert_obj_trail<ast>(m_drat_asts, e));
         }
-        else {
-            IF_VERBOSE(0, verbose_stream() << "logging binders is TBD\n");
+        else if (is_var(e)) {
+            var* v = to_var(e);
+            get_drat().def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
+            get_drat().def_add_arg(v->get_idx());
+            get_drat().def_end();
         }
+        else if (is_quantifier(e)) {
+            quantifier* q = to_quantifier(e);
+            std::stringstream strm;           
+            strm << "(" << (is_forall(q) ? "forall" : (is_exists(q) ? "exists" : "lambda"));
+            for (unsigned i = 0; i < q->get_num_decls(); ++i) 
+                strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")";            
+            strm << ")";
+            get_drat().def_begin('q', q->get_id(), strm.str());
+            get_drat().def_add_arg(q->get_expr()->get_id());
+            get_drat().def_end();
+        }
+        else 
+            UNREACHABLE();
+        m_drat_asts.insert(e);
+        push(insert_obj_trail<ast>(m_drat_asts, e));
     }
 
     void solver::drat_log_expr(expr* e) {
@@ -61,9 +73,15 @@ namespace euf {
                 for (expr* arg : *to_app(e))
                     if (!m_drat_asts.contains(arg))
                         m_drat_todo.push_back(arg);
+            if (is_quantifier(e)) {
+                expr* arg = to_quantifier(e)->get_expr();
+                if (!m_drat_asts.contains(arg))
+                    m_drat_todo.push_back(arg);                
+            }                
             if (m_drat_todo.size() != sz)
                 continue;
-            drat_log_expr1(e);
+            if (!m_drat_asts.contains(e))
+                drat_log_expr1(e);
             m_drat_todo.pop_back();                   
         }
     }
@@ -154,6 +172,8 @@ namespace euf {
     void solver::drat_eq_def(literal lit, expr* eq) {
         expr *a = nullptr, *b = nullptr;
         VERIFY(m.is_eq(eq, a, b));
+        drat_log_expr(a);
+        drat_log_expr(b);
         get_drat().def_begin('e', eq->get_id(), std::string("="));
         get_drat().def_add_arg(a->get_id());
         get_drat().def_add_arg(b->get_id());

src/sat/smt/euf_relevancy.cpp

@@ -38,12 +38,22 @@ namespace euf {
         }
     }
 
+    /**
+     * Add a root clause. Root clauses must all be satisfied by the 
+     * final assignment. If a clause is added above search level it
+     * is subject to removal on backtracking. These clauses are therefore
+     * not tracked.
+     */
     void solver::add_root(unsigned n, sat::literal const* lits) {
+        if (!relevancy_enabled())
+            return;
         ensure_dual_solver();
         m_dual_solver->add_root(n, lits);
     }
 
     void solver::add_aux(unsigned n, sat::literal const* lits) {
+        if (!relevancy_enabled())
+            return;
         ensure_dual_solver();
         m_dual_solver->add_aux(n, lits);
     }

src/sat/smt/euf_solver.cpp

@@ -211,7 +211,7 @@ namespace euf {
         for (sat::literal lit : r) 
             if (s().lvl(lit) > 0) r[j++] = lit;
         r.shrink(j);
-        TRACE("euf", tout << "eplain " << l << " <- " << r << " " << probing << "\n";);
+        TRACE("euf", tout << "explain " << l << " <- " << r << " " << probing << "\n";);
         DEBUG_CODE(for (auto lit : r) SASSERT(s().value(lit) == l_true););
 
         if (!probing)
@@ -236,7 +236,7 @@ namespace euf {
         sat::bool_var v = get_egraph().explain_diseq(m_explain, a, b);
         SASSERT(v == sat::null_bool_var || s().value(v) == l_false);
         if (v != sat::null_bool_var) 
-            m_explain.push_back(to_ptr(sat::literal(v, false)));
+            m_explain.push_back(to_ptr(sat::literal(v, true)));
     }
 
     bool solver::propagate(enode* a, enode* b, ext_justification_idx idx) {
@@ -286,13 +286,13 @@ namespace euf {
 
     void solver::asserted(literal l) {
         expr* e = m_bool_var2expr.get(l.var(), nullptr);
-	TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
+        TRACE("euf", tout << "asserted: " << l << "@" << s().scope_lvl() << " := " << mk_bounded_pp(e, m) << "\n";);
         if (!e) 
-            return;        
+            return;                
         euf::enode* n = m_egraph.find(e);
         if (!n)
             return;
-        bool sign = l.sign();       
+        bool sign = l.sign();   
         m_egraph.set_value(n, sign ? l_false : l_true);
         for (auto th : enode_th_vars(n))
             m_id2solver[th.get_id()]->asserted(l);
@@ -302,20 +302,25 @@ namespace euf {
         SASSERT(l == get_literal(c));
 	    if (n->value_conflict()) {
             euf::enode* nb = sign ? mk_false() : mk_true();
+            euf::enode* r = n->get_root();
+            euf::enode* rb = sign ? mk_true() : mk_false();
+            sat::literal rl(r->bool_var(), r->value() == l_false);
             m_egraph.merge(n, nb, c);
+            m_egraph.merge(r, rb, to_ptr(rl));
+            SASSERT(m_egraph.inconsistent());
+            return;
 	    }
-        else if (!sign && n->is_equality()) {
-            SASSERT(!m.is_iff(e));
-            euf::enode* na = n->get_arg(0);
-            euf::enode* nb = n->get_arg(1);
-            m_egraph.merge(na, nb, c);
-        }
-        else if (n->merge_tf()) {
+        if (n->merge_tf()) {
             euf::enode* nb = sign ? mk_false() : mk_true();
             m_egraph.merge(n, nb, c);
         }
-        else if (sign && n->is_equality()) 
-            m_egraph.new_diseq(n);        
+        if (n->is_equality()) {
+            SASSERT(!m.is_iff(e));
+            if (sign)
+                m_egraph.new_diseq(n);
+            else                 
+                m_egraph.merge(n->get_arg(0), n->get_arg(1), c);            
+        }    
     }
 
 
@@ -342,21 +347,19 @@ namespace euf {
                 break;
             propagated = true;             
         }
-        DEBUG_CODE(if (!s().inconsistent()) check_missing_eq_propagation(););
+        DEBUG_CODE(if (!propagated && !s().inconsistent()) check_missing_eq_propagation(););
         return propagated;
     }
 
     void solver::propagate_literals() {
         for (; m_egraph.has_literal() && !s().inconsistent() && !m_egraph.inconsistent(); m_egraph.next_literal()) {
-            euf::enode_bool_pair p = m_egraph.get_literal();
-            euf::enode* n = p.first;
-            bool is_eq = p.second;
+            auto [n, is_eq] = m_egraph.get_literal();
             expr* e = n->get_expr();
             expr* a = nullptr, *b = nullptr;
             bool_var v = n->bool_var();
             SASSERT(m.is_bool(e));
             size_t cnstr;
-            literal lit;            
+            literal lit;  
             if (is_eq) {
                 VERIFY(m.is_eq(e, a, b));
                 cnstr = eq_constraint().to_index();
@@ -364,6 +367,10 @@ namespace euf {
             }
             else {
                 lbool val = n->get_root()->value();
+                if (val == l_undef && m.is_false(n->get_root()->get_expr()))
+                    val = l_false;
+                if (val == l_undef && m.is_true(n->get_root()->get_expr()))
+                    val = l_true;
                 a = e;
                 b = (val == l_true) ? m.mk_true() : m.mk_false();
                 SASSERT(val != l_undef);
@@ -449,8 +456,8 @@ namespace euf {
 
         if (!init_relevancy())
             give_up = true;
-
-
+        
+        unsigned num_nodes = m_egraph.num_nodes();
         for (auto* e : m_solvers) {
             if (!m.inc())
                 return sat::check_result::CR_GIVEUP;
@@ -468,6 +475,10 @@ namespace euf {
             return sat::check_result::CR_CONTINUE;
         if (give_up)
             return sat::check_result::CR_GIVEUP;
+        if (num_nodes < m_egraph.num_nodes()) {
+            IF_VERBOSE(1, verbose_stream() << "new nodes created, but not detected\n");
+            return sat::check_result::CR_CONTINUE;           
+        }
         if (m_qsolver)
             return m_qsolver->check();
         TRACE("after_search", s().display(tout););
@@ -483,6 +494,8 @@ namespace euf {
         for (auto* e : m_solvers)
             e->push();
         m_egraph.push();
+        if (m_dual_solver)
+            m_dual_solver->push();
     }
 
     void solver::pop(unsigned n) {
@@ -500,20 +513,18 @@ namespace euf {
         }
         m_var_trail.shrink(sc.m_var_lim);        
         m_scopes.shrink(m_scopes.size() - n);
+        if (m_dual_solver)
+            m_dual_solver->pop(n);
         SASSERT(m_egraph.num_scopes() == m_scopes.size());
         TRACE("euf_verbose", display(tout << "pop to: " << m_scopes.size() << "\n"););
     }
 
     void solver::user_push() {
-        push();
-        if (m_dual_solver)
-            m_dual_solver->push();        
+        push();      
     }
 
     void solver::user_pop(unsigned n) {
         pop(n);
-        if (m_dual_solver)
-            m_dual_solver->pop(n);
     }
 
     void solver::start_reinit(unsigned n) {
@@ -547,14 +558,11 @@ namespace euf {
         scoped_set_replay replay(*this);
         scoped_suspend_rlimit suspend_rlimit(m.limit());
 
-        for (auto const& t : m_reinit) 
-            replay.m.insert(std::get<0>(t), std::get<2>(t));
-        
+        for (auto const& [e, generation, v] : m_reinit) 
+            replay.m.insert(e, v);
+    
         TRACE("euf", for (auto const& kv : replay.m) tout << kv.m_value << "\n";);
-        for (auto const& t : m_reinit) {
-            expr_ref e          = std::get<0>(t);
-            unsigned generation = std::get<1>(t);
-            sat::bool_var v     = std::get<2>(t);
+        for (auto const& [e, generation, v] : m_reinit) {
             scoped_generation _sg(*this, generation);
             TRACE("euf", tout << "replay: " << v << " " << mk_bounded_pp(e, m) << "\n";);
             sat::literal lit;
@@ -565,9 +573,112 @@ namespace euf {
             VERIFY(lit.var() == v);
             attach_lit(lit, e);            
         }
+        
+        if (relevancy_enabled())
+            for (auto const& [e, generation, v] : m_reinit)
+                if (si.is_bool_op(e))
+                    relevancy_reinit(e);
         TRACE("euf", display(tout << "replay done\n"););
     }
 
+    /**
+    * Boolean structure needs to be replayed for relevancy tracking.
+    * Main cases for replaying Boolean functions are included. When a replay
+    * is not supported, we just disable relevancy.
+    */
+    void solver::relevancy_reinit(expr* e) {
+        TRACE("euf", tout << "internalize again " << mk_pp(e, m) << "\n";);
+        if (to_app(e)->get_family_id() != m.get_basic_family_id()) {
+            disable_relevancy(e);
+            return;
+        }
+        auto lit = si.internalize(e, true);
+        switch (to_app(e)->get_decl_kind()) {
+        case OP_NOT: {
+            auto lit2 = si.internalize(to_app(e)->get_arg(0), true);
+            add_aux(lit, lit2);
+            add_aux(~lit, ~lit2);
+            break;
+        }
+        case OP_EQ: {
+            if (to_app(e)->get_num_args() != 2) {
+                disable_relevancy(e);
+                return;
+            }
+            auto lit1 = si.internalize(to_app(e)->get_arg(0), true);
+            auto lit2 = si.internalize(to_app(e)->get_arg(1), true);
+            add_aux(~lit, ~lit1, lit2);
+            add_aux(~lit, lit1, ~lit2);
+            add_aux(lit, lit1, lit2);
+            add_aux(lit, ~lit1, ~lit2);
+            break;
+        }
+        case OP_OR: {
+            sat::literal_vector lits;
+            for (expr* arg : *to_app(e))
+                lits.push_back(si.internalize(arg, true));
+            for (auto lit2 : lits)
+                add_aux(~lit2, lit);
+            lits.push_back(~lit);
+            add_aux(lits);
+            break;
+        }
+        case OP_AND: {
+            sat::literal_vector lits;
+            for (expr* arg : *to_app(e))
+                lits.push_back(~si.internalize(arg, true));
+            for (auto nlit2 : lits)
+                add_aux(~lit, ~nlit2);
+            lits.push_back(lit);
+            add_aux(lits);
+            break;
+        }
+        case OP_TRUE:
+            add_root(lit);
+            break;
+        case OP_FALSE:
+            add_root(~lit);
+            break;
+        case OP_ITE: {
+            auto lit1 = si.internalize(to_app(e)->get_arg(0), true);
+            auto lit2 = si.internalize(to_app(e)->get_arg(1), true);
+            auto lit3 = si.internalize(to_app(e)->get_arg(2), true);
+            add_aux(~lit, ~lit1, lit2);
+            add_aux(~lit, lit1, lit3);
+            add_aux(lit, ~lit1, ~lit2);
+            add_aux(lit, lit1, ~lit3);
+            break;
+        }
+        case OP_XOR: {
+            if (to_app(e)->get_num_args() != 2) {
+                disable_relevancy(e);
+                break;
+            }
+            auto lit1 = si.internalize(to_app(e)->get_arg(0), true);
+            auto lit2 = si.internalize(to_app(e)->get_arg(1), true);
+            add_aux(lit, ~lit1, lit2);
+            add_aux(lit, lit1, ~lit2);
+            add_aux(~lit, lit1, lit2);
+            add_aux(~lit, ~lit1, ~lit2);
+            break;
+        }
+        case OP_IMPLIES: {
+            if (to_app(e)->get_num_args() != 2) {
+                disable_relevancy(e);
+                break;
+            }
+            auto lit1 = si.internalize(to_app(e)->get_arg(0), true);
+            auto lit2 = si.internalize(to_app(e)->get_arg(1), true);
+            add_aux(~lit, ~lit1, lit2);
+            add_aux(lit, lit1);
+            add_aux(lit, ~lit2);
+            break;
+        }
+        default:
+            UNREACHABLE();
+        }
+    }
+
     void solver::pre_simplify() {
         for (auto* e : m_solvers)
             e->pre_simplify();

src/sat/smt/euf_solver.h

@@ -96,27 +96,27 @@ namespace euf {
         stats                  m_stats;
         th_rewriter            m_rewriter;
         func_decl_ref_vector   m_unhandled_functions;
-        sat::lookahead*        m_lookahead{ nullptr };
+        sat::lookahead*        m_lookahead = nullptr;
         ast_manager*           m_to_m;
         sat::sat_internalizer* m_to_si;
         scoped_ptr<euf::ackerman>    m_ackerman;
         scoped_ptr<sat::dual_solver> m_dual_solver;
-        user::solver*          m_user_propagator{ nullptr };
-        th_solver*             m_qsolver { nullptr };
-        unsigned               m_generation { 0 };
+        user::solver*          m_user_propagator = nullptr;
+        th_solver*             m_qsolver = nullptr;
+        unsigned               m_generation = 0;
         mutable ptr_vector<expr> m_todo;
 
         ptr_vector<expr>                                m_bool_var2expr;
         ptr_vector<size_t>                              m_explain;
-        unsigned                                        m_num_scopes{ 0 };
+        unsigned                                        m_num_scopes = 0;
         unsigned_vector                                 m_var_trail;
         svector<scope>                                  m_scopes;
         scoped_ptr_vector<th_solver>                    m_solvers;
         ptr_vector<th_solver>                           m_id2solver;
 
-        constraint* m_conflict{ nullptr };
-        constraint* m_eq{ nullptr };
-        constraint* m_lit{ nullptr };
+        constraint* m_conflict = nullptr;
+        constraint* m_eq = nullptr;
+        constraint* m_lit = nullptr;
 
         // internalization
         bool visit(expr* e) override;
@@ -134,8 +134,9 @@ namespace euf {
         typedef std::tuple<expr_ref, unsigned, sat::bool_var> reinit_t;
         vector<reinit_t>    m_reinit;
 
-        void start_reinit(unsigned num_scopes);
+        void start_reinit(unsigned num_scopes);        
         void finish_reinit();
+        void relevancy_reinit(expr* e);
 
         // extensions
         th_solver* get_solver(family_id fid, func_decl* f);
@@ -356,13 +357,17 @@ namespace euf {
         bool is_shared(euf::enode* n) const;
 
         // relevancy
-        bool relevancy_enabled() const { return get_config().m_relevancy_lvl > 0; }
+        bool m_relevancy = true;
+        bool relevancy_enabled() const { return m_relevancy && get_config().m_relevancy_lvl > 0; }
+        void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy = false;  }
         void add_root(unsigned n, sat::literal const* lits);
         void add_root(sat::literal_vector const& lits) { add_root(lits.size(), lits.data()); }
         void add_root(sat::literal lit) { add_root(1, &lit); }
         void add_root(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_root(2, lits); }
+        void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); }
         void add_aux(unsigned n, sat::literal const* lits);
         void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } 
+        void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); }
         void track_relevancy(sat::bool_var v);
         bool is_relevant(expr* e) const;
         bool is_relevant(enode* n) const;

src/sat/smt/fpa_solver.cpp

@@ -15,6 +15,8 @@ Author:
 
 Revision History:
 
+    Ported from theory_fpa by nbjorner in 2020.
+
 --*/
 
 #include "sat/smt/fpa_solver.h"
@@ -91,7 +93,10 @@ namespace fpa {
         SASSERT(m.is_bool(e));
         if (!visit_rec(m, e, sign, root, redundant))
             return sat::null_literal;
-        return expr2literal(e);
+        sat::literal lit = expr2literal(e);
+        if (sign)
+           lit.neg();
+        return lit;
     }
 
     void solver::internalize(expr* e, bool redundant) {
@@ -116,12 +121,11 @@ namespace fpa {
 
     bool solver::post_visit(expr* e, bool sign, bool root) {
         euf::enode* n = expr2enode(e);
-        app* a = to_app(e);
         SASSERT(!n || !n->is_attached_to(get_id()));
         if (!n)
             n = mk_enode(e, false);
         SASSERT(!n->is_attached_to(get_id()));
-        mk_var(n);
+        attach_new_th_var(n);
         TRACE("fp", tout << "post: " << mk_bounded_pp(e, m) << "\n";);
         m_nodes.push_back(std::tuple(n, sign, root));
         ctx.push(push_back_trail(m_nodes));
@@ -310,7 +314,9 @@ namespace fpa {
             if (!wrapped) wrapped = m_converter.wrap(e);
             return expr2enode(wrapped) != nullptr;
         };
-        if (m_fpa_util.is_fp(e)) {
+        if (m_fpa_util.is_rm_numeral(e) || m_fpa_util.is_numeral(e)) 
+            value = e;
+        else if (m_fpa_util.is_fp(e)) {
             SASSERT(n->num_args() == 3);
             expr* a = values.get(n->get_arg(0)->get_root_id());
             expr* b = values.get(n->get_arg(1)->get_root_id());

src/sat/smt/q_clause.cpp

@@ -23,9 +23,9 @@ namespace q {
     std::ostream& lit::display(std::ostream& out) const {
         ast_manager& m = lhs.m();
         if (m.is_true(rhs) && !sign) 
-            return out << mk_bounded_pp(lhs, m, 2);
+            return out << lhs;
         if (m.is_false(rhs) && !sign) 
-            return out << "(not " << mk_bounded_pp(lhs, m, 2) << ")";
+            return out << "(not " << lhs << ")";
         return 
             out << mk_bounded_pp(lhs, m, 2) 
                 << (sign ? " != " : " == ") 
@@ -43,13 +43,13 @@ namespace q {
         for (auto const& lit : m_lits)
             lit.display(out) << "\n";
         binding* b = m_bindings;
-        if (b) {
-            do {
-                b->display(ctx, num_decls(), out) << "\n";
-                b = b->next();
-            }
-            while (b != m_bindings);
-        }
+        if (!b)
+            return out;
+        do {
+            b->display(ctx, num_decls(), out) << "\n";
+            b = b->next();
+        } 
+        while (b != m_bindings);
         return out;
     }
 

src/sat/smt/q_clause.h

@@ -29,7 +29,9 @@ namespace q {
         expr_ref rhs;
         bool     sign;
         lit(expr_ref const& lhs, expr_ref const& rhs, bool sign):
-            lhs(lhs), rhs(rhs), sign(sign) {}
+            lhs(lhs), rhs(rhs), sign(sign) {
+            SASSERT(!rhs.m().is_false(rhs) || !sign);
+        }
         std::ostream& display(std::ostream& out) const;
     };
 
@@ -57,10 +59,12 @@ namespace q {
         unsigned            m_index;
         vector<lit>         m_lits;
         quantifier_ref      m_q;
-        sat::literal        m_literal;
+        unsigned            m_watch = 0;
+        sat::literal        m_literal = sat::null_literal;
         q::quantifier_stat* m_stat = nullptr;
         binding*            m_bindings = nullptr;
 
+
         clause(ast_manager& m, unsigned idx): m_index(idx), m_q(m) {}
 
         std::ostream& display(euf::solver& ctx, std::ostream& out) const;
@@ -75,10 +79,12 @@ namespace q {
     struct justification {
         expr*     m_lhs, *m_rhs;
         bool      m_sign;
+        unsigned  m_num_ev;
+        euf::enode_pair* m_evidence;
         clause&   m_clause;
         euf::enode* const* m_binding;
-        justification(lit const& l, clause& c, euf::enode* const* b):
-            m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_clause(c), m_binding(b) {}
+        justification(lit const& l, clause& c, euf::enode* const* b, unsigned n, euf::enode_pair* ev):
+            m_lhs(l.lhs), m_rhs(l.rhs), m_sign(l.sign), m_num_ev(n), m_evidence(ev), m_clause(c), m_binding(b) {}
         sat::ext_constraint_idx to_index() const { 
             return sat::constraint_base::mem2base(this); 
         }

src/sat/smt/q_ematch.cpp

@@ -94,7 +94,10 @@ namespace q {
         lit lit(expr_ref(l, m), expr_ref(r, m), sign); 
         if (idx != UINT_MAX)
             lit = c[idx];
-        auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(lit, c, b);
+        auto* ev = static_cast<euf::enode_pair*>(ctx.get_region().allocate(sizeof(euf::enode_pair) * m_evidence.size()));
+        for (unsigned i = m_evidence.size(); i-- > 0; )
+            ev[i] = m_evidence[i];
+        auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(lit, c, b, m_evidence.size(), ev);
         return constraint->to_index();
     }
 
@@ -251,7 +254,8 @@ namespace q {
     bool ematch::propagate(bool is_owned, euf::enode* const* binding, unsigned max_generation, clause& c, bool& propagated) {
         TRACE("q", c.display(ctx, tout) << "\n";);
         unsigned idx = UINT_MAX;
-        lbool ev = m_eval(binding, c, idx);
+        m_evidence.reset();
+        lbool ev = m_eval(binding, c, idx, m_evidence);
         if (ev == l_true) {
             ++m_stats.m_num_redundant;
             return true;
@@ -267,17 +271,39 @@ namespace q {
         if (ev == l_undef && max_generation > m_generation_propagation_threshold)
             return false;
         if (!is_owned) 
-            binding = alloc_binding(c, binding);        
-        auto j_idx = mk_justification(idx, c, binding);       
-        if (ev == l_false) {
+            binding = alloc_binding(c, binding); 
+
+        auto j_idx = mk_justification(idx, c, binding);     
+
+        if (is_owned)
+            propagate(ev == l_false, idx, j_idx);
+        else
+            m_prop_queue.push_back(prop(ev == l_false, idx, j_idx));
+        propagated = true;
+        return true;
+    }
+
+    void ematch::propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx) {
+        if (is_conflict) {
             ++m_stats.m_num_conflicts;
             ctx.set_conflict(j_idx);
         }
         else {
             ++m_stats.m_num_propagations;
-            ctx.propagate(instantiate(c, binding, c[idx]), j_idx);
+            auto& j = justification::from_index(j_idx);
+            auto lit = instantiate(j.m_clause, j.m_binding, j.m_clause[idx]);
+            ctx.propagate(lit, j_idx);
         }
-        propagated = true;
+    }
+
+    bool ematch::flush_prop_queue() {
+        if (m_prop_queue.empty())
+            return false;
+        for (unsigned i = 0; i < m_prop_queue.size(); ++i) {
+            auto [is_conflict, idx, j_idx] = m_prop_queue[i];
+            propagate(is_conflict, idx, j_idx);
+        }
+        m_prop_queue.reset();
         return true;
     }
 
@@ -295,6 +321,7 @@ namespace q {
     }
 
     void ematch::add_instantiation(clause& c, binding& b, sat::literal lit) {
+        m_evidence.reset();
         ctx.propagate(lit, mk_justification(UINT_MAX, c, b.nodes()));
     }
 
@@ -411,6 +438,16 @@ namespace q {
                 r = sign ? m.mk_false() : m.mk_true();
                 sign = false;
             }
+            if (m.is_true(l) || m.is_false(l))
+                std::swap(l, r);
+            if (sign && m.is_false(r)) {
+                r = m.mk_true();
+                sign = false;
+            }
+            else if (sign && m.is_true(r)) {
+                r = m.mk_false();
+                sign = false;
+            }
             cl->m_lits.push_back(lit(expr_ref(l, m), expr_ref(r, m), sign));
         }
         if (q->get_num_patterns() == 0) {
@@ -490,7 +527,7 @@ namespace q {
 
     bool ematch::propagate(bool flush) {
         m_mam->propagate();
-        bool propagated = false;
+        bool propagated = flush_prop_queue();
         if (m_qhead >= m_clause_queue.size())
             return m_inst_queue.propagate();
         ctx.push(value_trail<unsigned>(m_qhead));

src/sat/smt/q_ematch.h

@@ -49,6 +49,13 @@ namespace q {
             }
         };
 
+        struct prop {
+            bool is_conflict;
+            unsigned idx;
+            sat::ext_justification_idx j;
+            prop(bool is_conflict, unsigned idx, sat::ext_justification_idx j) : is_conflict(is_conflict), idx(idx), j(j) {}
+        };
+
         struct remove_binding;
         struct insert_binding;
         struct pop_clause;
@@ -63,8 +70,9 @@ namespace q {
         quantifier_stat_gen           m_qstat_gen;
         fingerprints                  m_fingerprints;
         scoped_ptr<binding>           m_tmp_binding;
-        unsigned                      m_tmp_binding_capacity { 0 };
+        unsigned                      m_tmp_binding_capacity = 0;
         queue                         m_inst_queue;
+        svector<prop>                 m_prop_queue;
         pattern_inference_rw          m_infer_patterns;
         scoped_ptr<q::mam>            m_mam, m_lazy_mam;
         ptr_vector<clause>            m_clauses;
@@ -72,13 +80,14 @@ namespace q {
         vector<unsigned_vector>       m_watch;     // expr_id -> clause-index*
         stats                         m_stats;
         expr_fast_mark1               m_mark;
-        unsigned                      m_generation_propagation_threshold{ 3 };
+        unsigned                      m_generation_propagation_threshold = 3;
         ptr_vector<app>               m_ground;
-        bool                          m_in_queue_set{ false };
+        bool                          m_in_queue_set = false;
         nat_set                       m_node_in_queue;
         nat_set                       m_clause_in_queue;
-        unsigned                      m_qhead { 0 };
+        unsigned                      m_qhead = 0;
         unsigned_vector               m_clause_queue;
+        euf::enode_pair_vector        m_evidence;
 
         binding* alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top);
         euf::enode* const* alloc_binding(clause& c, euf::enode* const* _binding);
@@ -107,6 +116,9 @@ namespace q {
         fingerprint* add_fingerprint(clause& c, binding& b, unsigned max_generation);
         void set_tmp_binding(fingerprint& fp);
 
+        bool flush_prop_queue();
+        void propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx);
+
     public:
         
         ematch(euf::solver& ctx, solver& s);
@@ -115,7 +127,7 @@ namespace q {
 
         bool propagate(bool flush);
 
-        void init_search();
+        // void init_search();
 
         void add(quantifier* q);
 
@@ -127,7 +139,7 @@ namespace q {
         void on_binding(quantifier* q, app* pat, euf::enode* const* binding, unsigned max_generation, unsigned min_gen, unsigned max_gen);
 
         // callbacks from queue
-        lbool evaluate(euf::enode* const* binding, clause& c) { return m_eval(binding, c); }
+        lbool evaluate(euf::enode* const* binding, clause& c) { m_evidence.reset();  return m_eval(binding, c, m_evidence); }
 
         void add_instantiation(clause& c, binding& b, sat::literal lit);
 

src/sat/smt/q_eval.cpp

@@ -15,6 +15,7 @@ Author:
 
 --*/
 
+#include "ast/has_free_vars.h"
 #include "sat/smt/q_eval.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/q_solver.h"
@@ -32,89 +33,96 @@ namespace q {
         m(ctx.get_manager())
     {}
 
-    lbool eval::operator()(euf::enode* const* binding, clause& c, unsigned& idx) {
+    lbool eval::operator()(euf::enode* const* binding, clause& c, unsigned& idx, euf::enode_pair_vector& evidence) {
         scoped_mark_reset _sr(*this);
         idx = UINT_MAX;
         unsigned sz = c.m_lits.size();
         unsigned n = c.num_decls();
         m_indirect_nodes.reset();
-        for (unsigned i = 0; i < sz; ++i) {
+        for (unsigned j = 0; j < sz; ++j) {
+            unsigned i = (j + c.m_watch) % sz;
             unsigned lim = m_indirect_nodes.size();
             lit l = c[i];
-            lbool cmp = compare(n, binding, l.lhs, l.rhs);
+            lbool cmp = compare(n, binding, l.lhs, l.rhs, evidence);
             switch (cmp) {
             case l_false:
                 m_indirect_nodes.shrink(lim);
                 if (!l.sign)
                     break;
-                if (i > 0)
-                    std::swap(c[0], c[i]);
+                c.m_watch = i;
                 return l_true;
             case l_true:
                 m_indirect_nodes.shrink(lim);
                 if (l.sign)
                     break;
-                if (i > 0)
-                    std::swap(c[0], c[i]);
+                c.m_watch = i;
                 return l_true;
             case l_undef:
                 TRACE("q", tout << l.lhs << " ~~ " << l.rhs << " is undef\n";);
-                if (idx == 0) {
+                if (idx != UINT_MAX) {
                     idx = UINT_MAX;
                     return l_undef;
                 }
-                if (i > 0)
-                    std::swap(c[0], c[i]);
-                idx = 0;
+                idx = i;
                 break;
             }
         }
         if (idx == UINT_MAX)
             return l_false;
-        
+        c.m_watch = idx;
         return l_undef;
     }
 
-    lbool eval::operator()(euf::enode* const* binding, clause& c) {
+    lbool eval::operator()(euf::enode* const* binding, clause& c, euf::enode_pair_vector& evidence) {
         unsigned idx = 0;
-        return (*this)(binding, c, idx);
+        return (*this)(binding, c, idx, evidence);
     }
 
-    lbool eval::compare(unsigned n, euf::enode* const* binding, expr* s, expr* t) {
+    lbool eval::compare(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence) {
         if (s == t)
             return l_true;
         if (m.are_distinct(s, t))
             return l_false;
 
-        euf::enode* sn = (*this)(n, binding, s);
-        euf::enode* tn = (*this)(n, binding, t);
-        if (sn) sn = sn->get_root();
-        if (tn) tn = tn->get_root();
+        euf::enode* sn = (*this)(n, binding, s, evidence);
+        euf::enode* tn = (*this)(n, binding, t, evidence);
+        euf::enode* sr = sn ? sn->get_root() : sn;
+        euf::enode* tr = tn ? tn->get_root() : tn;
+        if (sn != sr) evidence.push_back(euf::enode_pair(sn, sr)), sn = sr;
+        if (tn != tr) evidence.push_back(euf::enode_pair(tn, tr)), tn = tr;
         TRACE("q", tout << mk_pp(s, m) << " ~~ " << mk_pp(t, m) << "\n";
               tout << ctx.bpp(sn) << " " << ctx.bpp(tn) << "\n";);
         
         lbool c;
-        if (sn && sn == tn)
+        if (sn && sn == tn) 
             return l_true;
-        if (sn && tn && ctx.get_egraph().are_diseq(sn, tn))
+        
+        if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) {
+            evidence.push_back(euf::enode_pair(sn, tn));
             return l_false;
+        }
         if (sn && tn)
             return l_undef;
         if (!sn && !tn) 
-            return compare_rec(n, binding, s, t);
+            return compare_rec(n, binding, s, t, evidence);
         if (!tn && sn) {
             std::swap(tn, sn);
             std::swap(t, s);
         }
-        for (euf::enode* t1 : euf::enode_class(tn)) 
-            if (c = compare_rec(n, binding, s, t1->get_expr()), c != l_undef)
+        unsigned sz = evidence.size();
+        for (euf::enode* t1 : euf::enode_class(tn)) {            
+            if (c = compare_rec(n, binding, s, t1->get_expr(), evidence), c != l_undef) {
+                evidence.push_back(euf::enode_pair(t1, tn));
                 return c;
+            }
+            evidence.shrink(sz);
+        }
         return l_undef;
     }
 
     // f(p1) = f(p2)  if p1 = p2
     // f(p1) != f(p2) if p1 != p2 and f is injective
-    lbool eval::compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t) {
+    lbool eval::compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence) {
         if (m.are_equal(s, t))
             return l_true;
         if (m.are_distinct(s, t))
@@ -127,14 +135,20 @@ namespace q {
             return l_undef;
         bool is_injective = to_app(s)->get_decl()->is_injective();
         bool has_undef = false;
+        unsigned sz = evidence.size();
         for (unsigned i = to_app(s)->get_num_args(); i-- > 0; ) {
-            switch (compare(n, binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i))) {
+            unsigned sz1 = evidence.size(), sz2;
+            switch (compare(n, binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i), evidence)) {
             case l_true:
                 break;
-            case l_false:
-                if (is_injective)
-                    return l_false;
-                return l_undef;
+            case l_false:                                
+                if (!is_injective)
+                    return l_undef;
+                sz2 = evidence.size();
+                for (unsigned i = 0; i < sz2 - sz1; ++i)
+                    evidence[sz + i] = evidence[sz1 + i];
+                evidence.shrink(sz + sz2 - sz1);
+                return l_false;
             case l_undef:
                 if (!is_injective)
                     return l_undef;
@@ -142,10 +156,15 @@ namespace q {
                 break;
             }
         }
-        return has_undef ? l_undef : l_true;
+
+        if (!has_undef)
+            return l_true;
+
+        evidence.shrink(sz);
+        return l_undef;
     }
 
-    euf::enode* eval::operator()(unsigned n, euf::enode* const* binding, expr* e) {
+    euf::enode* eval::operator()(unsigned n, euf::enode* const* binding, expr* e, euf::enode_pair_vector& evidence) {
         if (is_ground(e))
             return ctx.get_egraph().find(e);
         if (m_mark.is_marked(e))
@@ -156,10 +175,11 @@ namespace q {
         while (!todo.empty()) {
             expr* t = todo.back();
             SASSERT(!is_ground(t) || ctx.get_egraph().find(t));
-            if (is_ground(t)) {
+            if (is_ground(t) || (has_quantifiers(t) && !has_free_vars(t))) {
                 m_mark.mark(t);
-                m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr);
-                SASSERT(m_eval[t->get_id()]);
+                m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr);                
+                if (!m_eval[t->get_id()])
+                    return nullptr;
                 todo.pop_back();
                 continue;
             }
@@ -186,6 +206,15 @@ namespace q {
                 euf::enode* n = ctx.get_egraph().find(t, args.size(), args.data());
                 if (!n)
                     return nullptr;
+                for (unsigned i = args.size(); i-- > 0; ) {
+                    if (args[i] != n->get_arg(i)) {
+                        // roots could be different when using commutativity
+                        // instead of compensating for this, we just bail out
+                        if (args[i]->get_root() != n->get_arg(i)->get_root())
+                            return nullptr;
+                        evidence.push_back(euf::enode_pair(args[i], n->get_arg(i)));
+                    }
+                }
                 m_indirect_nodes.push_back(n);
                 m_eval.setx(t->get_id(), n, nullptr);
                 m_mark.mark(t);
@@ -195,99 +224,18 @@ namespace q {
         return m_eval[e->get_id()];
     }
 
-    void eval::explain(clause& c, unsigned literal_idx, euf::enode* const* b) {
-        unsigned n = c.num_decls();
-        for (unsigned i = c.size(); i-- > 0; ) {
-            if (i == literal_idx) 
-                continue;
-            auto const& lit = c[i];
-            if (lit.sign) 
-                explain_eq(n, b, lit.lhs, lit.rhs);
-            else 
-                explain_diseq(n, b, lit.lhs, lit.rhs);
-        }
-    }
-
-    void eval::explain_eq(unsigned n, euf::enode* const* binding, expr* s, expr* t) {
-        SASSERT(l_true == compare(n, binding, s, t));
-        if (s == t)
-            return;
-        euf::enode* sn = (*this)(n, binding, s);
-        euf::enode* tn = (*this)(n, binding, t);
-        if (sn && tn) {
-            SASSERT(sn->get_root() == tn->get_root());
-            ctx.add_antecedent(sn, tn);
-            return;
-        }
-        if (!sn && tn) {
-            std::swap(sn, tn);
-            std::swap(s, t);
-        }
-        if (sn && !tn) {
-            for (euf::enode* s1 : euf::enode_class(sn)) {
-                if (l_true == compare_rec(n, binding, t, s1->get_expr())) {
-                    ctx.add_antecedent(sn, s1);
-                    explain_eq(n, binding, t, s1->get_expr());
-                    return;
-                }
-            }
-            UNREACHABLE();
-        }
-        SASSERT(is_app(s) && is_app(t));
-        SASSERT(to_app(s)->get_decl() == to_app(t)->get_decl());
-        for (unsigned i = to_app(s)->get_num_args(); i-- > 0; ) 
-            explain_eq(n, binding, to_app(s)->get_arg(i), to_app(t)->get_arg(i));
-    }
-
-    void eval::explain_diseq(unsigned n, euf::enode* const* binding, expr* s, expr* t) {
-        SASSERT(l_false == compare(n, binding, s, t));
-        if (m.are_distinct(s, t))
-            return;
-        euf::enode* sn = (*this)(n, binding, s);
-        euf::enode* tn = (*this)(n, binding, t);
-        if (sn && tn && ctx.get_egraph().are_diseq(sn, tn)) {
-            ctx.add_diseq_antecedent(sn, tn);
-            return;
-        }
-        if (!sn && tn) {
-            std::swap(sn, tn);
-            std::swap(s, t);
-        }
-        if (sn && !tn) {
-            for (euf::enode* s1 : euf::enode_class(sn)) {
-                if (l_false == compare_rec(n, binding, t, s1->get_expr())) {
-                    ctx.add_antecedent(sn, s1);
-                    explain_diseq(n, binding, t, s1->get_expr());
-                    return;
-                }
-            }
-            UNREACHABLE();
-        }
-        SASSERT(is_app(s) && is_app(t));
-        app* at = to_app(t);
-        app* as = to_app(s);
-        SASSERT(as->get_decl() == at->get_decl());
-        for (unsigned i = as->get_num_args(); i-- > 0; ) {
-            if (l_false == compare_rec(n, binding, as->get_arg(i), at->get_arg(i))) {                
-                explain_eq(n, binding, as->get_arg(i), at->get_arg(i));
-                return;
-            }
-        }
-        UNREACHABLE();
-    }
-
-
     void eval::explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing) {
-        scoped_mark_reset _sr(*this);
-        unsigned l_idx = 0;
         clause& c = j.m_clause;
-        for (; l_idx < c.size(); ++l_idx) {
-            if (c[l_idx].lhs == j.m_lhs && c[l_idx].rhs == j.m_rhs && c[l_idx].sign == j.m_sign)
-                break;
+        for (unsigned i = 0; i < j.m_num_ev; ++i) {
+            auto [a, b] = j.m_evidence[i];
+            SASSERT(a->get_root() == b->get_root() || ctx.get_egraph().are_diseq(a, b));
+            if (a->get_root() == b->get_root())
+                ctx.add_antecedent(a, b);
+            else
+                ctx.add_diseq_antecedent(a, b);                            
         }
-        explain(c, l_idx, j.m_binding);
         r.push_back(c.m_literal);
-        (void)probing; // ignored
+        (void)probing; // ignored        
     }
 
     

src/sat/smt/q_eval.h

@@ -30,25 +30,20 @@ namespace q {
         expr_fast_mark1    m_mark;
         euf::enode_vector  m_eval;
         euf::enode_vector  m_indirect_nodes;
-        ptr_vector<size_t> m_explain;
 
         struct scoped_mark_reset;
 
-        void explain(clause& c, unsigned literal_idx, euf::enode* const* binding);
-        void explain_eq(unsigned n, euf::enode* const* binding, expr* s, expr* t);
-        void explain_diseq(unsigned n, euf::enode* const* binding, expr* s, expr* t);
-
         // compare s, t modulo binding
-        lbool compare(unsigned n, euf::enode* const* binding, expr* s, expr* t);
-        lbool compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t);
+        lbool compare(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence);
+        lbool compare_rec(unsigned n, euf::enode* const* binding, expr* s, expr* t, euf::enode_pair_vector& evidence);
         
     public:
         eval(euf::solver& ctx);
         void explain(sat::literal l, justification& j, sat::literal_vector& r, bool probing);
 
-        lbool operator()(euf::enode* const* binding, clause& c);        
-        lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx);
-        euf::enode* operator()(unsigned n, euf::enode* const* binding, expr* e);
+        lbool operator()(euf::enode* const* binding, clause& c, euf::enode_pair_vector& evidence);
+        lbool operator()(euf::enode* const* binding, clause& c, unsigned& idx, euf::enode_pair_vector& evidence);
+        euf::enode* operator()(unsigned n, euf::enode* const* binding, expr* e, euf::enode_pair_vector& evidence);
 
         euf::enode_vector const& get_watch() { return m_indirect_nodes; }
     };

src/sat/smt/q_mbi.cpp

@@ -42,6 +42,7 @@ namespace q {
         add_plugin(ap);
         add_plugin(alloc(mbp::datatype_project_plugin, m));
         add_plugin(alloc(mbp::array_project_plugin, m));
+        
     }
 
     lbool mbqi::operator()() {
@@ -66,10 +67,11 @@ namespace q {
             }
         }
         m_max_cex += ctx.get_config().m_mbqi_max_cexs;
-        for (auto p : m_instantiations) {
-            unsigned generation = std::get<2>(p);
+        for (auto [qlit, fml, generation] : m_instantiations) {
             euf::solver::scoped_generation sg(ctx, generation + 1);
-            m_qs.add_clause(~std::get<0>(p), ~ctx.mk_literal(std::get<1>(p)));
+            sat::literal lit = ctx.mk_literal(fml);
+            m_qs.add_clause(~qlit, ~lit);
+            ctx.add_root(~qlit, ~lit);
         }
         m_instantiations.reset();
         return result;
@@ -162,12 +164,13 @@ namespace q {
                 return r;
             if (r == l_true) {
                 model_ref mdl;
-                expr_ref proj(m);
                 m_solver->get_model(mdl);
                 if (check_forall_subst(q, *qb, *mdl))
                     return l_false;
                 if (check_forall_default(q, *qb, *mdl))
                     return l_false;
+                else 
+                    return l_undef;                
             }
             if (m_generation_bound >= m_generation_max)
                 return l_true;
@@ -279,8 +282,9 @@ namespace q {
         bool fmls_extracted = false;
         TRACE("q",
               tout << "Project\n";
-              tout << *m_model << "\n";
               tout << fmls << "\n";
+              tout << "model\n";
+              tout << *m_model << "\n";
               tout << "model of projection\n" << mdl << "\n";
               tout << "var args: " << qb.var_args.size() << "\n";
               tout << "domain eqs: " << qb.domain_eqs << "\n";
@@ -294,8 +298,13 @@ namespace q {
             app* v = vars.get(i);
             auto* p = get_plugin(v);
             if (p && !fmls_extracted) {
+                TRACE("q", tout << "domain eqs\n" << qb.domain_eqs << "\n";);
+                                
                 fmls.append(qb.domain_eqs);
                 eliminate_nested_vars(fmls, qb);
+                for (expr* e : fmls)
+                    if (!m_model->is_true(e))
+                        return expr_ref(nullptr, m);
                 mbp::project_plugin proj(m);
                 proj.extract_literals(*m_model, vars, fmls);
                 fmls_extracted = true;
@@ -312,6 +321,7 @@ namespace q {
             eqs.push_back(m.mk_eq(v, val));
         }
         rep(fmls);
+        TRACE("q", tout << "generated formulas\n" << fmls << "\ngenerated eqs:\n" << eqs;);
         return mk_and(fmls);
     }
 
@@ -326,8 +336,8 @@ namespace q {
         qb.domain_eqs.reset();
         var_subst subst(m);
 
-        for (auto p : qb.var_args) {
-            expr_ref bounds = m_model_fixer.restrict_arg(p.first, p.second);  
+        for (auto [t, idx] : qb.var_args) {
+            expr_ref bounds = m_model_fixer.restrict_arg(t, idx);  
             if (m.is_true(bounds))
                 continue;
             expr_ref vbounds = subst(bounds, qb.vars);
@@ -382,11 +392,11 @@ namespace q {
         if (qb.var_args.empty())
             return;
         var_subst subst(m);
-        for (auto p : qb.var_args) {
-            expr_ref _term = subst(p.first, qb.vars);
+        for (auto [t, idx] : qb.var_args) {
+            expr_ref _term = subst(t, qb.vars);
             app_ref  term(to_app(_term), m);
-            expr_ref value = (*m_model)(term->get_arg(p.second));
-            m_model_fixer.invert_arg(term, p.second, value, qb.domain_eqs);
+            expr_ref value = (*m_model)(term->get_arg(idx));
+            m_model_fixer.invert_arg(term, idx, value, qb.domain_eqs);
         }
     }
 
@@ -555,7 +565,7 @@ namespace q {
 
     void mbqi::init_solver() {
         if (!m_solver)
-            m_solver = mk_smt2_solver(m, ctx.s().params());
+            m_solver = mk_smt2_solver(m, m_no_drat_params);
     }
 
     void mbqi::init_search() {

src/sat/smt/q_mbi.h

@@ -20,6 +20,7 @@ Author:
 #include "qe/mbp/mbp_plugin.h"
 #include "sat/smt/sat_th.h"
 #include "sat/smt/q_model_fixer.h"
+#include "sat/sat_solver.h"
 
 namespace euf {
     class solver;
@@ -60,6 +61,7 @@ namespace q {
         stats                                  m_stats;
         model_fixer                            m_model_fixer;
         model_ref                              m_model;
+        sat::no_drat_params                    m_no_drat_params;
         ref<::solver>                          m_solver;
         scoped_ptr_vector<obj_hashtable<expr>> m_values;
         scoped_ptr_vector<mbp::project_plugin> m_plugins;

src/sat/smt/q_model_fixer.cpp

@@ -111,6 +111,18 @@ namespace q {
             add_projection_functions(mdl, f);
     }
 
+    /**
+    *  we are given f with interpretation:
+    *      if x = v0 and y = w0 then f0
+    *      else if x = v1 and y = w1 then f1
+    *      ...
+    * Create a new interpretation for f as follows:
+    * f := f_aux(project1(x), project2(y))
+    * f_aux uses the original interpretation of f
+    * project1 sorts the values of v0, v1, ..., and maps arguments below v0 to v0, between v0, v1 to v1 etc.
+    * project2 sorts values of w0, w1, ... and maps argument y to values w0, w1, ..
+    * 
+    */
     void model_fixer::add_projection_functions(model& mdl, func_decl* f) {
         // update interpretation of f so that the graph of f is fully determined by the
         // ground values of its arguments.
@@ -141,6 +153,19 @@ namespace q {
         mdl.register_decl(f_new, fi);
     }
 
+    /*
+    * For function f(...,t_idx, ..) collect the values of terms at position idx of f 
+    * as "values". 
+    * Map t_idx |-> mdl(t_idx)
+    * and mdl(t_idx) |-> t_idx
+    * Sort the values as [v_1, v_2, ..., v_n] with corresponding terms
+    * [t_1, t_2, ..., t_n]
+    * 
+    * Create the term if p(x) = if x <= v_1 then t_1 else if x <= v_2 then t_2 else ...  t_n
+    * where p is a fresh function 
+    * and return p(x)
+    */
+
     expr_ref model_fixer::add_projection_function(model& mdl, func_decl* f, unsigned idx) {
         sort* srt = f->get_domain(idx);
         projection_function* proj = get_projection(srt);
@@ -230,6 +255,15 @@ namespace q {
         return value;
     }
 
+    /**
+    * We are given a term f(...,arg_i,..) and value = mdl(arg_i)
+    * Create 
+    * 1 the bounds t_j <= arg_i < t_{j+1} where 
+    *   v_j <= value < v_{j+1} for the corresponding values of t_j, t_{j+1}
+    * 2 or the bound arg_i < t_0     if value < v_0
+    * 3 or the bound arg_i >= t_last if value > v_last
+    */
+
     void model_fixer::invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits) {
         TRACE("q", tout << "invert-arg " << mk_pp(t, m) << " " << i << " " << mk_pp(value, m) << "\n";);
         auto const* md = get_projection_data(t->get_decl(), i);

src/sat/smt/q_solver.cpp

@@ -40,35 +40,30 @@ namespace q {
             return;
         quantifier* q = to_quantifier(e);
 
-        auto const& exp = expand(q);
-        if (exp.size() > 1 && is_forall(q) && !l.sign()) {
-            for (expr* e : exp) {
-                sat::literal lit = ctx.internalize(e, l.sign(), false, false); 
-                add_clause(~l, lit);                    
-                if (ctx.relevancy_enabled())
-                    ctx.add_root(~l, lit);
-            }
-            return;
-        }
-        if (exp.size() > 1 && is_exists(q) && l.sign()) {
-            sat::literal_vector lits;
-            lits.push_back(~l);
-            for (expr* e : exp)
-                lits.push_back(ctx.internalize(e, l.sign(), false, false));
-            add_clause(lits);
-            ctx.add_root(lits);
-            return;
-        }
-
         if (l.sign() == is_forall(e)) {
             sat::literal lit = skolemize(q);
             add_clause(~l, lit);
             ctx.add_root(~l, lit);
         }
         else {
-            ctx.push_vec(m_universal, l);
-            if (ctx.get_config().m_ematching)
-                m_ematch.add(q);
+            auto const& exp = expand(q);
+            if (exp.size() > 1) {
+                for (expr* e : exp) {
+                    sat::literal lit = ctx.internalize(e, l.sign(), false, false); 
+                    add_clause(~l, lit);                    
+                    ctx.add_root(~l, lit);
+                }
+            }
+            else if (is_ground(q->get_expr())) {
+                auto lit = ctx.internalize(q->get_expr(), l.sign(), false, false);
+                add_clause(~l, lit);
+                ctx.add_root(~l, lit);
+            }
+            else {
+                ctx.push_vec(m_universal, l);
+                if (ctx.get_config().m_ematching)
+                    m_ematch.add(q);
+            }
         }
         m_stats.m_num_quantifier_asserts++;
     }
@@ -88,8 +83,7 @@ namespace q {
     }
 
     std::ostream& solver::display(std::ostream& out) const {
-        m_ematch.display(out);
-        return out;
+        return m_ematch.display(out);
     }
 
     std::ostream& solver::display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const {
@@ -147,9 +141,9 @@ namespace q {
     }
 
     /*
-    * Find initial values to instantiate quantifier with so to make it as hard as possible for solver
-    * to find values to free variables. 
-    */
+     * Find initial values to instantiate quantifier with so to make it as hard as possible for solver
+     * to find values to free variables. 
+     */
     sat::literal solver::specialize(quantifier* q) {
         std::function<expr* (quantifier*, unsigned)> mk_var = [&](quantifier* q, unsigned i) {
             return get_unit(q->get_decl_sort(i));
@@ -244,46 +238,11 @@ namespace q {
                 ctx.get_rewriter()(tmp);
                 m_expanded[i] = tmp;
             }
-            return m_expanded;
         }
-
-#if 0
-        m_expanded.reset();
-        m_expanded2.reset();
-        if (is_forall(q)) 
-            flatten_or(q->get_expr(), m_expanded2);
-        else if (is_exists(q)) 
-            flatten_and(q->get_expr(), m_expanded2);
-        else
-            UNREACHABLE();
-        for (unsigned i = m_expanded2.size(); i-- > 0; ) {
-            expr* lit = m_expanded2.get(i);
-            if (!is_ground(lit) && is_and(lit) && is_forall(q)) {
-
-                // get free vars of lit
-                // create fresh predicate over free vars
-                // replace in expanded, pack and push on m_expanded
-                
-                expr_ref p(m);
-                // TODO introduce fresh p.
-                flatten_and(lit, m_expanded);
-                for (unsigned i = m_expanded.size(); i-- > 0; ) {
-                    tmp = m.mk_or(m.mk_not(p), m_expanded.get(i));
-                    expr_ref tmp(m.update_quantifier(q, tmp), m);
-                    ctx.get_rewriter()(tmp);
-                    m_expanded[i] = tmp;
-                }
-                m_expanded2[i] = p;
-                tmp = m.mk_or(m_expanded2);
-                expr_ref tmp(m.update_quantifier(q, tmp), m);
-                ctx.get_rewriter()(tmp);                
-                m_expanded.push_back(tmp);
-                return m_expanded;
-            }
+        else {
+            m_expanded.reset();
+            m_expanded.push_back(q);
         }
-#endif
-        m_expanded.reset();
-        m_expanded.push_back(q);
         return m_expanded;
     }
 

src/sat/smt/sat_dual_solver.cpp

@@ -18,25 +18,34 @@ Author:
 
 namespace sat {
 
-    dual_solver::no_drat_params::no_drat_params() {
-        set_sym("drat.file", symbol());
-    }
-
     dual_solver::dual_solver(reslimit& l):
         m_solver(m_params, l)
     {
         SASSERT(!m_solver.get_config().m_drat);
     }
 
-    void dual_solver::push() {
-        m_solver.user_push(); 
-        m_roots.push_scope();
-        m_tracked_vars.push_scope();
-        m_units.push_scope();
-        m_vars.push_scope();
+    void dual_solver::flush() {
+        while (m_num_scopes > 0) {
+            m_solver.user_push();
+            m_roots.push_scope();
+            m_tracked_vars.push_scope();
+            m_units.push_scope();
+            m_vars.push_scope();
+            --m_num_scopes;
+        }
     }
 
-    void dual_solver::pop(unsigned num_scopes) {
+    void dual_solver::push() {
+        ++m_num_scopes;
+    }
+
+    void dual_solver::pop(unsigned num_scopes) {        
+        if (m_num_scopes >= num_scopes) {
+            m_num_scopes -= num_scopes;
+            return;
+        }
+        num_scopes -= m_num_scopes;
+        m_num_scopes = 0;
         m_solver.user_pop(num_scopes);
         unsigned old_sz = m_tracked_vars.old_size(num_scopes);
         for (unsigned i = m_tracked_vars.size(); i-- > old_sz; )
@@ -66,6 +75,7 @@ namespace sat {
     }
 
     void dual_solver::track_relevancy(bool_var w) {
+        flush();
         bool_var v = ext2var(w);
         if (!m_is_tracked.get(v, false)) {
             m_is_tracked.setx(v, true, false);
@@ -81,27 +91,36 @@ namespace sat {
         return literal(m_var2ext[lit.var()], lit.sign());
     }
 
-    void dual_solver::add_root(unsigned sz, literal const* clause) {
-        TRACE("dual", tout << "root: " << literal_vector(sz, clause) << "\n";);
-        if (sz == 1) {
+    void dual_solver::add_root(unsigned sz, literal const* clause) {      
+        flush();
+        if (false && sz == 1) {
+            TRACE("dual", tout << "unit: " << clause[0] << "\n";);
             m_units.push_back(clause[0]);
             return;
         }
-        literal root(m_solver.mk_var(), false);
-        for (unsigned i = 0; i < sz; ++i)
-            m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
+        literal root;
+        if (sz == 1) 
+            root = ext2lit(clause[0]);
+        else {
+            root = literal(m_solver.mk_var(), false);
+            for (unsigned i = 0; i < sz; ++i)
+                m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
+        }
         m_roots.push_back(~root);
+        TRACE("dual", tout << "root: " << ~root << " => " << literal_vector(sz, clause) << "\n";);
     }
 
     void dual_solver::add_aux(unsigned sz, literal const* clause) {
-        TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << "\n";);
+        flush();        
         m_lits.reset();
         for (unsigned i = 0; i < sz; ++i) 
             m_lits.push_back(ext2lit(clause[i]));
+        TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << " -> " << m_lits << "\n";);
         m_solver.mk_clause(sz, m_lits.data(), status::input());
     }
 
     void dual_solver::add_assumptions(solver const& s) {
+        flush();
         m_lits.reset();
         for (bool_var v : m_tracked_vars)
             m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
@@ -112,7 +131,7 @@ namespace sat {
         }
     }
 
-    bool dual_solver::operator()(solver const& s) {
+    bool dual_solver::operator()(solver const& s) {        
         m_core.reset();
         m_core.append(m_units);
         if (m_roots.empty())

src/sat/smt/sat_dual_solver.h

@@ -23,9 +23,6 @@ Author:
 namespace sat {
 
     class dual_solver {
-        struct no_drat_params : public params_ref {
-            no_drat_params();
-        };
         no_drat_params  m_params;
         solver          m_solver;
         lim_svector<literal> m_units, m_roots;
@@ -35,6 +32,7 @@ namespace sat {
         unsigned_vector m_ext2var;
         unsigned_vector m_var2ext;
         lim_svector<unsigned> m_vars;
+        unsigned        m_num_scopes = 0;
         void add_literal(literal lit);
 
         bool_var ext2var(bool_var v);
@@ -46,6 +44,8 @@ namespace sat {
 
         std::ostream& display(solver const& s, std::ostream& out) const;
 
+        void flush();
+
     public:
         dual_solver(reslimit& l);
         void push();

src/sat/tactic/goal2sat.cpp

@@ -69,7 +69,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
     atom2bool_var &             m_map;
     dep2asm_map &               m_dep2asm;
     obj_map<expr, sat::bool_var>* m_expr2var_replay { nullptr };
-    sat::literal                m_true;
     bool                        m_ite_extra;
     unsigned long long          m_max_memory;
     expr_ref_vector             m_trail;
@@ -92,7 +91,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_unhandled_funs(m),
         m_default_external(default_external) {
         updt_params(p);
-        m_true = sat::null_literal;
     }
 
     ~imp() override {
@@ -198,16 +196,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
             ensure_euf()->drat_bool_def(v, n);
     }
 
-    sat::literal mk_true() {
-        if (m_true == sat::null_literal) {
-            // create fake variable to represent true;
-            m_true = sat::literal(add_var(false, m.mk_true()), false);
-            mk_clause(m_true); // v is true
-            add_dual_root(1, &m_true);
-        }
-        return m_true;
-    }
-
     sat::bool_var to_bool_var(expr* e) override {
         sat::literal l;
         sat::bool_var v = m_map.to_bool_var(e);
@@ -228,8 +216,10 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (!m_expr2var_replay || !m_expr2var_replay->find(t, v))  
             v = add_var(true, t);
         m_map.insert(t, v);
-        if (relevancy_enabled() && (m.is_true(t) || m.is_false(t))) 
+        if (relevancy_enabled() && (m.is_true(t) || m.is_false(t))) {
             add_dual_root(sat::literal(v, m.is_false(t)));
+            ensure_euf()->track_relevancy(v);
+        }
         return v;
     }
 
@@ -285,7 +275,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }     
     }
 
-
     void cache(app* t, sat::literal l) override {
         force_push();
         SASSERT(!m_app2lit.contains(t));
@@ -294,36 +283,40 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_lit2app.insert(l.index(), t);
         m_cache_trail.push_back(t);
     }
-
-   void convert_atom(expr * t, bool root, bool sign) {
+    
+    void convert_atom(expr * t, bool root, bool sign) {
         SASSERT(m.is_bool(t));
         sat::literal  l;
         sat::bool_var v = m_map.to_bool_var(t);
         if (v == sat::null_bool_var) {
             if (m.is_true(t)) {
-                l = sign ? ~mk_true() : mk_true();
+                sat::literal tt = sat::literal(mk_bool_var(t), false);
+                mk_root_clause(tt);
+                l = sign ? ~tt : tt;
             }
             else if (m.is_false(t)) {
-                l = sign ? mk_true() : ~mk_true();
+                sat::literal ff = sat::literal(mk_bool_var(t), false);
+                mk_root_clause(~ff);
+                l = sign ? ~ff : ff;
             }
-            else {                
-                if (m_euf) {
-                    convert_euf(t, root, sign);  
-                    return;
-                } 
+            else if (m_euf) {
+                convert_euf(t, root, sign);
+                return;
+            }
+            else {
                 if (!is_uninterp_const(t)) {
                     if (!is_app(t)) {
                         std::ostringstream strm;
                         strm << mk_ismt2_pp(t, m);
                         throw_op_not_handled(strm.str());
                     }
-                    else
-                        m_unhandled_funs.push_back(to_app(t)->get_decl());
+                    m_unhandled_funs.push_back(to_app(t)->get_decl());
                 }
+
                 v = mk_bool_var(t);
                 l = sat::literal(v, sign);
                 bool ext = m_default_external || !is_uninterp_const(t) || m_interface_vars.contains(t);
-                if (ext) 
+                if (ext)
                     m_solver.set_external(v);
                 TRACE("sat", tout << "new_var: " << v << ": " << mk_bounded_pp(t, m, 2) << " " << is_uninterp_const(t) << "\n";);
             }
@@ -550,6 +543,29 @@ struct goal2sat::imp : public sat::sat_internalizer {
         }
     }
 
+    void convert_not(app* t, bool root, bool sign) {
+        SASSERT(t->get_num_args() == 1);
+        unsigned sz = m_result_stack.size();
+        SASSERT(sz >= 1);
+        sat::literal  lit = m_result_stack[sz - 1];
+        m_result_stack.shrink(sz - 1);
+        if (root) {
+            SASSERT(sz == 1);
+            mk_root_clause(sign ? lit : ~lit);            
+        }
+        else {
+            sat::bool_var k = add_var(false, t);
+            sat::literal  l(k, false);
+            cache(t, l);
+            // l <=> ~lit
+            mk_clause(lit, l);
+            mk_clause(~lit, ~l);
+            if (sign)
+                l.neg();
+            m_result_stack.push_back(l);
+        }
+    }
+
     void convert_implies(app* t, bool root, bool sign) {
         SASSERT(t->get_num_args() == 2);
         unsigned sz = m_result_stack.size();
@@ -582,8 +598,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     void convert_iff(app * t, bool root, bool sign) {
-        if (t->get_num_args() != 2)
-            throw default_exception("unexpected number of arguments to xor");
+        if (t->get_num_args() != 2)            
+            throw default_exception("unexpected number of arguments to " + mk_pp(t, m));
         SASSERT(t->get_num_args() == 2);
         unsigned sz = m_result_stack.size();
         SASSERT(sz >= 2);
@@ -591,6 +607,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
         sat::literal  l2 = m_result_stack[sz-2];
         m_result_stack.shrink(sz - 2);
         if (root) {
+            if (m.is_xor(t))
+                sign = !sign;
             SASSERT(sz == 2);
             if (sign) {
                 mk_root_clause(l1, l2);
@@ -599,17 +617,20 @@ struct goal2sat::imp : public sat::sat_internalizer {
             else {
                 mk_root_clause(l1, ~l2);
                 mk_root_clause(~l1, l2);
-            }            
+            }                  
         }
         else {
             sat::bool_var k = add_var(false, t);
             sat::literal  l(k, false);
+            if (m.is_xor(t))
+                l1.neg();
             mk_clause(~l, l1, ~l2);
             mk_clause(~l, ~l1, l2);
-            mk_clause(l,  l1, l2);
+            mk_clause(l, l1, l2);
             mk_clause(l, ~l1, ~l2);
-            if (aig()) aig()->add_iff(l, l1, l2);            
-            cache(t, m.is_xor(t) ? ~l : l);
+            if (aig()) aig()->add_iff(l, l1, l2);
+
+            cache(t, l);
             if (sign)
                 l.neg();
             m_result_stack.push_back(l);
@@ -703,11 +724,14 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 convert_iff(t, root, sign);
                 break;
             case OP_XOR:
-                convert_iff(t, root, !sign);
+                convert_iff(t, root, sign);
                 break;
             case OP_IMPLIES:
                 convert_implies(t, root, sign);
                 break;
+            case OP_NOT:
+                convert_not(t, root, sign);
+                break;
             default:
                 UNREACHABLE();
             }
@@ -773,7 +797,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
                 m_frame_stack.pop_back();
                 continue;
             }
-            if (m.is_not(t)) {
+            if (m.is_not(t) && (root || (!m.is_not(t->get_arg(0)) && fsz != sz + 1))) {
                 m_frame_stack.pop_back();
                 visit(t->get_arg(0), root, !sign);
                 continue;
@@ -808,6 +832,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         process(n, false, redundant);
         SASSERT(m_result_stack.size() == sz + 1);
         sat::literal result = m_result_stack.back();
+        TRACE("goal2sat", tout << "done internalize " << result << " " << mk_bounded_pp(n, m, 2) << "\n";);
         m_result_stack.pop_back();
         if (!result.sign() && m_map.to_bool_var(n) == sat::null_bool_var) {
             force_push();
@@ -932,7 +957,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     void user_pop(unsigned n) {
-        m_true = sat::null_literal;   
     }
 
 };
@@ -1006,6 +1030,10 @@ bool goal2sat::has_interpreted_funs() const {
     return m_imp && !m_imp->interpreted_funs().empty(); 
 }
 
+bool goal2sat::has_euf() const {
+    return m_imp && m_imp->m_euf;
+}
+
 void goal2sat::update_model(model_ref& mdl) {
     if (m_imp) 
         m_imp->update_model(mdl);

src/sat/tactic/goal2sat.h

@@ -66,6 +66,8 @@ public:
 
     bool has_interpreted_funs() const;
 
+    bool has_euf() const;
+
     sat::sat_internalizer& si(ast_manager& m, params_ref const& p, sat::solver_core& t, atom2bool_var& a2b, dep2asm_map& dep2asm, bool default_external = false);
 
     void update_model(model_ref& mdl);

src/sat/tactic/sat_tactic.cpp

@@ -113,8 +113,11 @@ class sat_tactic : public tactic {
                             break;
                         }
                     }
+
+                    bool euf = m_goal2sat.has_euf();
+		    
                     for (auto* f : fmls_to_validate) 
-                        if (md->is_false(f)) 
+                        if (!euf && md->is_false(f)) 
                             IF_VERBOSE(0, verbose_stream() << "failed to validate: " << mk_pp(f, m) << "\n";);
                     
                     m_goal2sat.update_model(md);

src/shell/drat_frontend.cpp

@@ -122,12 +122,17 @@ class smt_checker {
             m_input_solver->assert_expr(lit2expr(~lit));
         lbool is_sat = m_input_solver->check_sat();
         if (is_sat != l_false) {
-            std::cout << "did not verify: " << lits << "\n";
-            for (sat::literal lit : lits) {
-                std::cout << lit2expr(lit) << "\n";
-            }
+            std::cout << "did not verify: " << is_sat << " " << lits << "\n";
+            for (sat::literal lit : lits) 
+                std::cout << lit2expr(lit) << "\n";            
             std::cout << "\n";
             m_input_solver->display(std::cout);
+            if (is_sat == l_true) {
+                model_ref mdl;
+                m_input_solver->get_model(mdl);
+                std::cout << *mdl << "\n";
+            }
+                
             exit(0);
         }
         m_input_solver->pop(1);
@@ -171,6 +176,49 @@ public:
     unsigned_vector params;
     ptr_vector<sort> sorts;
 
+    void parse_quantifier(sexpr_ref const& sexpr, cmd_context& ctx, quantifier_kind& k, sort_ref_vector& domain, svector<symbol>& names) {
+        k = quantifier_kind::forall_k;
+        symbol q;
+        unsigned sz;
+        if (sexpr->get_kind() != sexpr::kind_t::COMPOSITE)
+            goto bail;
+        sz = sexpr->get_num_children();
+        if (sz == 0)
+            goto bail;
+        q = sexpr->get_child(0)->get_symbol();
+        if (q == "forall")
+            k = quantifier_kind::forall_k;
+        else if (q == "exists")
+            k = quantifier_kind::exists_k;
+        else if (q == "lambda")            
+            k = quantifier_kind::lambda_k;
+        else
+            goto bail;
+        for (unsigned i = 1; i < sz; ++i) {
+            auto* e = sexpr->get_child(i);
+            if (e->get_kind() != sexpr::kind_t::COMPOSITE)
+                goto bail;
+            if (2 != e->get_num_children())
+                goto bail;
+            symbol name = e->get_child(0)->get_symbol();
+            std::ostringstream ostrm;
+            e->get_child(1)->display(ostrm);            
+            std::istringstream istrm(ostrm.str());
+            params_ref p;
+            auto srt = parse_smt2_sort(ctx, istrm, false, p, "quantifier");
+            if (!srt)
+                goto bail;
+            names.push_back(name);
+            domain.push_back(srt);            
+        }
+        return;
+    bail:
+        std::cout << "Could not parse expression\n";
+        sexpr->display(std::cout);
+        std::cout << "\n";
+        exit(0);        
+    }
+
     void parse_sexpr(sexpr_ref const& sexpr, cmd_context& ctx, expr_ref_vector const& args, expr_ref& result) {
         params.reset();
         sorts.reset();
@@ -310,7 +358,17 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
             std::istringstream strm(r.m_name);
             auto sexpr = parse_sexpr(ctx, strm, p, drat_file);
             checker.parse_sexpr(sexpr, ctx, args, e);
-            exprs.reserve(r.m_node_id+1);
+            exprs.reserve(r.m_node_id + 1);
+            exprs.set(r.m_node_id, e);
+            break;
+        }
+        case dimacs::drat_record::tag_t::is_var: {
+            var_ref e(m);
+            SASSERT(r.m_args.size() == 1);
+            std::istringstream strm(r.m_name);
+            auto srt = parse_smt2_sort(ctx, strm, false, p, drat_file);
+            e = m.mk_var(r.m_args[0], srt);
+            exprs.reserve(r.m_node_id + 1);
             exprs.set(r.m_node_id, e);
             break;
         }
@@ -331,12 +389,26 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
                 srt = pd->instantiate(ctx.pm(), sargs.size(), sargs.data());
             else 
                 srt = m.mk_uninterpreted_sort(name);
-            sorts.reserve(r.m_node_id+1);
+            sorts.reserve(r.m_node_id + 1);
             sorts.set(r.m_node_id, srt);
             break;
         }
+        case dimacs::drat_record::tag_t::is_quantifier: {
+            VERIFY(r.m_args.size() == 1);          
+            quantifier_ref q(m);      
+            std::istringstream strm(r.m_name);
+            auto sexpr = parse_sexpr(ctx, strm, p, drat_file);
+            sort_ref_vector domain(m);
+            svector<symbol> names;
+            quantifier_kind k;
+            checker.parse_quantifier(sexpr, ctx, k, domain, names);
+            q = m.mk_quantifier(k, domain.size(), domain.data(), names.data(), exprs.get(r.m_args[0]));
+            exprs.reserve(r.m_node_id + 1);
+            exprs.set(r.m_node_id, q);
+            break;
+        }
         case dimacs::drat_record::tag_t::is_bool_def:
-            bool_var2expr.reserve(r.m_node_id+1);
+            bool_var2expr.reserve(r.m_node_id + 1);
             bool_var2expr.set(r.m_node_id, exprs.get(r.m_args[0]));
             break;
         default:
@@ -347,7 +419,6 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
     statistics st;
     drat_checker.collect_statistics(st);
     std::cout << st << "\n";
-
 }
 
 
@@ -359,5 +430,3 @@ unsigned read_drat(char const* drat_file, char const* problem_file) {
     verify_smt(drat_file, problem_file);
     return 0;
 }
-
-

src/smt/mam.cpp

@@ -121,7 +121,7 @@ namespace {
 
     struct instruction {
         opcode         m_opcode;
-        instruction *  m_next;
+        instruction* m_next = nullptr;
 #ifdef _PROFILE_MAM
         unsigned       m_counter; // how often it was executed
 #endif
@@ -1224,9 +1224,10 @@ namespace {
                     return;
 
             SASSERT(head->m_next == 0);
+
             m_seq.push_back(m_ct_manager.mk_yield(m_qa, m_mp, m_qa->get_num_decls(), reinterpret_cast<unsigned*>(m_vars.begin())));
 
-            for (instruction * curr : m_seq) {
+            for (instruction* curr : m_seq) {
                 head->m_next = curr;
                 head = curr;
             }
@@ -2309,7 +2310,10 @@ namespace {
 
     main_loop:
 
+        if (!m_pc)
+            goto backtrack;
         TRACE("mam_int", display_pc_info(tout););
+        
 #ifdef _PROFILE_MAM
         const_cast<instruction*>(m_pc)->m_counter++;
 #endif

src/smt/proto_model/proto_model.cpp

@@ -213,11 +213,12 @@ void proto_model::cleanup() {
     TRACE("model_bug", model_v2_pp(tout, *this););
     func_decl_set found_aux_fs;
     expr_ref_vector trail(m);
-    for (auto const& kv : m_finterp) {
-        TRACE("model_bug", tout << kv.m_key->get_name() << "\n";);
-        func_interp * fi = kv.m_value;
+    ptr_buffer<func_interp> finterps;
+    for (auto const& kv : m_finterp)
+        finterps.push_back(kv.m_value);
+    for (auto* fi : finterps)         
         cleanup_func_interp(trail, fi, found_aux_fs);
-    }
+    
     for (unsigned i = 0; i < m_const_decls.size(); ++i) {
         func_decl* d = m_const_decls[i];
         expr* e = m_interp[d].second;

src/smt/seq_axioms.h

@@ -81,6 +81,7 @@ namespace smt {
         void add_itos_axiom(expr* s, unsigned k) { m_ax.itos_axiom(s, k); }
         void add_ubv2s_axiom(expr* b, unsigned k) { m_ax.ubv2s_axiom(b, k); }
         void add_ubv2s_len_axiom(expr* b, unsigned k) { m_ax.ubv2s_len_axiom(b, k); }
+        void add_ubv2s_len_axiom(expr* b) { m_ax.ubv2s_len_axiom(b); }
         void add_ubv2ch_axioms(sort* s) { m_ax.ubv2ch_axiom(s); }
         void add_lt_axiom(expr* n) { m_ax.lt_axiom(n); }
         void add_le_axiom(expr* n) { m_ax.le_axiom(n); }

src/smt/seq_regex.cpp

@@ -272,13 +272,15 @@ namespace smt {
                                        << "PA(" << mk_pp(s, m) << "@" << idx
                                        << "," << state_str(r) << ") ";);
 
-        if (re().is_empty(r)) {
+        auto info = re().get_info(r);
+
+        //if the minlength of the regex is UINT_MAX then the regex is a deadend
+        if (re().is_empty(r) || info.min_length == UINT_MAX) {
             STRACE("seq_regex_brief", tout << "(empty) ";);
             th.add_axiom(~lit);
             return;
         }
 
-        auto info = re().get_info(r);
         if (info.interpreted) {
             update_state_graph(r);
             

src/smt/smt_conflict_resolution.cpp

@@ -315,7 +315,7 @@ namespace smt {
     void conflict_resolution::process_antecedent(literal antecedent, unsigned & num_marks) {
         bool_var var = antecedent.var();
         unsigned lvl = m_ctx.get_assign_level(var);
-        SASSERT(var < static_cast<int>(m_ctx.get_num_bool_vars()));
+        SASSERT(var < m_ctx.get_num_bool_vars());
         TRACE("conflict_", tout << "processing antecedent (level " << lvl << "):";
               m_ctx.display_literal(tout, antecedent);
               m_ctx.display_detailed_literal(tout << " ", antecedent) << "\n";);

src/smt/smt_model_generator.cpp

@@ -389,8 +389,7 @@ namespace smt {
         if (fid == null_family_id) return !m_hidden_ufs.contains(f); 
         if (fid == m.get_basic_family_id()) return false;
         theory * th = m_context->get_theory(fid);
-        if (!th) return true;
-        return th->include_func_interp(f);
+        return !th || th->include_func_interp(f);
     }
     
     /**

src/smt/theory_seq.cpp

@@ -1542,6 +1542,7 @@ void theory_seq::add_ubv_string(expr* e) {
     }
     if (!has_sort)
         m_ax.add_ubv2ch_axioms(b->get_sort());
+    m_ax.add_ubv2s_len_axiom(b);
     m_ubv_string.push_back(e);
     m_trail_stack.push(push_back_vector<expr_ref_vector>(m_ubv_string));
     add_length_to_eqc(e);
@@ -1557,7 +1558,6 @@ bool theory_seq::check_ubv_string() {
 }
 
 bool theory_seq::check_ubv_string(expr* e) {
-    expr* n = nullptr;
     if (ctx.inconsistent())
         return true;
     if (m_has_ubv_axiom.contains(e))

src/smt/theory_special_relations.cpp

@@ -903,7 +903,7 @@ namespace smt {
                                          m.mk_app(memf, x, m.mk_app(tl, S))));            
             recfun_replace rep(m);
             var* vars[2] = { xV, SV };
-            p.set_definition(rep, mem, 2, vars, mem_body);
+            p.set_definition(rep, mem, false, 2, vars, mem_body);
         }
 
         sort_ref tup(dt.mk_pair_datatype(listS, listS, fst, snd, pair), m);
@@ -926,7 +926,7 @@ namespace smt {
 
             recfun_replace rep(m);
             var* vars[5] = { aV, bV, AV, SV, tupV };
-            p.set_definition(rep, nxt, 5, vars, next_body);
+            p.set_definition(rep, nxt, false, 5, vars, next_body);
         }
 
         {
@@ -961,7 +961,7 @@ namespace smt {
             TRACE("special_relations", tout << connected_body << "\n";);
             recfun_replace rep(m);
             var* vars[3] = { AV, dstV, SV };
-            p.set_definition(rep, connected, 3, vars, connected_body);            
+            p.set_definition(rep, connected, false, 3, vars, connected_body);
         }
 
         {

src/smt/theory_str.cpp

@@ -1859,18 +1859,18 @@ namespace smt {
         axiomatized_terms.insert(ex);
         TRACE("str", tout << "instantiate str.from_code axiom for " << mk_pp(ex, m) << std::endl;);
 
-        expr * arg;
-        u.str.is_from_code(ex, arg);
+        expr * arg = nullptr;
+        VERIFY(u.str.is_from_code(ex, arg));
         // (str.from_code N) == "" if N is not in the range [0, max_char].
         {
-	        expr_ref premise(m.mk_or(m_autil.mk_le(arg, mk_int(-1)), m_autil.mk_ge(arg, mk_int(u.max_char() + 1))), m);
+            expr_ref premise(m.mk_or(m_autil.mk_le(arg, mk_int(-1)), m_autil.mk_ge(arg, mk_int(u.max_char() + 1))), m);
             expr_ref conclusion(ctx.mk_eq_atom(ex, mk_string("")), m);
             expr_ref axiom(rewrite_implication(premise, conclusion), m);
             assert_axiom_rw(axiom);
         }
         // len (str.from_code N) == 1 if N is in the range [0, max_char].
         {
-	        expr_ref premise(m.mk_and(m_autil.mk_ge(arg, mk_int(0)), m_autil.mk_le(arg, mk_int(u.max_char() + 1))), m);
+            expr_ref premise(m.mk_and(m_autil.mk_ge(arg, mk_int(0)), m_autil.mk_le(arg, mk_int(u.max_char() + 1))), m);
             expr_ref conclusion(ctx.mk_eq_atom(mk_strlen(ex), mk_int(1)), m);
             expr_ref axiom(rewrite_implication(premise, conclusion), m);
             assert_axiom_rw(axiom);
@@ -1895,8 +1895,8 @@ namespace smt {
         axiomatized_terms.insert(ex);
         TRACE("str", tout << "instantiate str.to_code axiom for " << mk_pp(ex, m) << std::endl;);
 
-        expr * arg;
-        u.str.is_to_code(ex, arg);
+        expr * arg = nullptr;
+        VERIFY(u.str.is_to_code(ex, arg));
         // (str.to_code S) == -1 if len(S) != 1.
         {
             expr_ref premise(m.mk_not(ctx.mk_eq_atom(mk_strlen(arg), mk_int(1))), m);
@@ -5523,6 +5523,7 @@ namespace smt {
         TRACE("str", tout << mk_pp(node, get_manager()) << std::endl;);
         if (groundedMap.find(node) != groundedMap.end()) {
             for (auto const &itor : groundedMap[node]) {
+                (void) itor;
                 TRACE("str",
                       tout << "\t[grounded] ";
                       for (auto const &vIt : itor.first) {

src/solver/assertions/CMakeLists.txt

@@ -2,7 +2,6 @@ z3_add_component(solver_assertions
   SOURCES
     asserted_formulas.cpp
   COMPONENT_DEPENDENCIES
-    solver
     smt2parser
     smt_params
 )

src/solver/assertions/asserted_formulas.cpp

@@ -424,7 +424,8 @@ void asserted_formulas::apply_quasi_macros() {
     TRACE("before_quasi_macros", display(tout););
     vector<justified_expr> new_fmls;
     quasi_macros proc(m, m_macro_manager);
-    while (proc(m_formulas.size() - m_qhead,
+    while (m_qhead == 0 && 
+           proc(m_formulas.size() - m_qhead,
                 m_formulas.data() + m_qhead,
                 new_fmls)) {
         swap_asserted_formulas(new_fmls);

src/solver/solver.cpp

@@ -202,12 +202,6 @@ bool solver::is_literal(ast_manager& m, expr* e) {
 
 void solver::assert_expr(expr* f) {
     expr_ref fml(f, get_manager());
-    if (m_enforce_model_conversion) {
-        model_converter_ref mc = get_model_converter();
-        if (mc) {
-            (*mc)(fml);        
-        }
-    }
     assert_expr_core(fml);    
 }
 
@@ -215,13 +209,6 @@ void solver::assert_expr(expr* f, expr* t) {
     ast_manager& m = get_manager();
     expr_ref fml(f, m);    
     expr_ref a(t, m);
-    if (m_enforce_model_conversion) {
-        model_converter_ref mc = get_model_converter();
-        if (mc) {
-            (*mc)(fml);        
-            // (*mc)(a);        
-        }
-    }
     assert_expr_core2(fml, a);    
 }
 
@@ -241,14 +228,12 @@ void solver::collect_param_descrs(param_descrs & r) {
 void solver::reset_params(params_ref const & p) {
     m_params = p;
     solver_params sp(m_params);
-    m_enforce_model_conversion = sp.enforce_model_conversion();
     m_cancel_backup_file = sp.cancel_backup_file();
 }
 
 void solver::updt_params(params_ref const & p) {
     m_params.copy(p);
     solver_params sp(m_params);
-    m_enforce_model_conversion = sp.enforce_model_conversion();
     m_cancel_backup_file = sp.cancel_backup_file();
 }
 

src/solver/solver.h

@@ -49,10 +49,9 @@ solver* mk_smt2_solver(ast_manager& m, params_ref const& p);
 */
 class solver : public check_sat_result {
     params_ref  m_params;
-    bool        m_enforce_model_conversion;
     symbol      m_cancel_backup_file;
 public:
-    solver(): m_enforce_model_conversion(false) {}
+     solver() {}
     ~solver() override {}
 
     /**

src/solver/solver_params.pyg

@@ -2,8 +2,7 @@
 def_module_params('solver', 
                   description='solver parameters',
                   export=True,
-                  params=(('enforce_model_conversion', BOOL, False, "apply model transformation on new assertions"),
-                          ('smtlib2_log', SYMBOL, '', "file to save solver interaction"),
+                  params=(('smtlib2_log', SYMBOL, '', "file to save solver interaction"),
                           ('cancel_backup_file', SYMBOL, '', "file to save partial search state if search is canceled"),
                           ('timeout', UINT, UINT_MAX, "timeout on the solver object; overwrites a global timeout"),
                           ))

src/tactic/CMakeLists.txt

@@ -12,7 +12,6 @@ z3_add_component(tactic
     probe.cpp
     proof_converter.cpp
     replace_proof_converter.cpp
-    sine_filter.cpp
     tactical.cpp
     tactic.cpp
   COMPONENT_DEPENDENCIES
@@ -20,7 +19,6 @@ z3_add_component(tactic
     model
   TACTIC_HEADERS
     probe.h
-    sine_filter.h
     tactic.h
   PYG_FILES
     tactic_params.pyg

src/tactic/arith/fm_tactic.cpp

@@ -93,7 +93,8 @@ class fm_tactic : public tactic {
                     expr * lhs = to_app(l)->get_arg(0);
                     expr * rhs = to_app(l)->get_arg(1);
                     rational c;
-                    u.is_numeral(rhs, c);
+                    if (!u.is_numeral(rhs, c))
+                        return NONE;
                     if (neg)
                         c.neg();
                     unsigned num_mons;
@@ -112,7 +113,8 @@ class fm_tactic : public tactic {
                         expr * xi;
                         rational ai_val;
                         if (u.is_mul(monomial, ai, xi)) {
-                            u.is_numeral(ai, ai_val);
+                            if (!u.is_numeral(ai, ai_val))
+                                return NONE;
                         }
                         else {
                             xi     = monomial;
@@ -120,7 +122,8 @@ class fm_tactic : public tactic {
                         }
                         if (u.is_to_real(xi))
                             xi = to_app(xi)->get_arg(0);
-                        SASSERT(is_uninterp_const(xi));
+                        if (!is_uninterp_const(xi))
+                            return NONE;
                         if (x == to_app(xi)->get_decl()) {
                             a_val = ai_val;
                             if (neg)
@@ -129,9 +132,9 @@ class fm_tactic : public tactic {
                         else {
                             expr_ref val(m);
                             val = ev(monomial);
-                            SASSERT(u.is_numeral(val));
                             rational tmp;
-                            u.is_numeral(val, tmp);
+                            if (!u.is_numeral(val, tmp))
+                                return NONE;
                             if (neg)
                                 tmp.neg();
                             c -= tmp;
@@ -162,11 +165,9 @@ class fm_tactic : public tactic {
         fm_model_converter(ast_manager & _m):m(_m) {}
 
         ~fm_model_converter() override {
-            m.dec_array_ref(m_xs.size(), m_xs.data());
-            vector<clauses>::iterator it  = m_clauses.begin();
-            vector<clauses>::iterator end = m_clauses.end();
-            for (; it != end; ++it)
-                m.dec_array_ref(it->size(), it->data());
+            m.dec_array_ref(m_xs.size(), m_xs.data());     
+            for (auto& c : m_clauses)
+                m.dec_array_ref(c.size(), c.data());
         }
         
         void insert(func_decl * x, clauses & c) {
@@ -177,6 +178,7 @@ class fm_tactic : public tactic {
             m_clauses.back().swap(c);
         }
 
+
         void get_units(obj_map<expr, bool>& units) override { units.reset(); }
 
         void operator()(model_ref & md) override {
@@ -252,11 +254,8 @@ class fm_tactic : public tactic {
             for (unsigned i = 0; i < sz; i++) {
                 out << "\n(" << m_xs[i]->get_name();
                 clauses const & cs = m_clauses[i];
-                clauses::const_iterator it  = cs.begin();
-                clauses::const_iterator end = cs.end();
-                for (; it != end; ++it) {
-                    out << "\n  " << mk_ismt2_pp(*it, m, 2);
-                }
+                for (auto& c : cs)
+                    out << "\n  " << mk_ismt2_pp(c, m, 2);                
                 out << ")";
             }
             out << ")\n";
@@ -274,10 +273,8 @@ class fm_tactic : public tactic {
                 clauses const & cs = m_clauses[i];
                 res->m_clauses.push_back(clauses());
                 clauses & new_cs = res->m_clauses.back();
-                clauses::const_iterator it  = cs.begin();
-                clauses::const_iterator end = cs.end();
-                for (; it != end; ++it) {
-                    app * new_c = translator(*it);
+                for (auto& c : cs) {
+                    app * new_c = translator(c);
                     to_m.inc_ref(new_c);
                     new_cs.push_back(new_c);
                 }
@@ -1598,7 +1595,7 @@ class fm_tactic : public tactic {
                 report_tactic_progress(":fm-cost", m_counter);
                 if (!m_inconsistent) {
                     copy_remaining();
-                    m_new_goal->add(concat(g->mc(), m_mc.get()));
+                    m_new_goal->add(m_mc.get());
                 }
             }
             reset_constraints();

src/tactic/arith/recover_01_tactic.cpp

@@ -321,8 +321,6 @@ class recover_01_tactic : public tactic {
             SASSERT(new_goal->depth() == g->depth());
             SASSERT(new_goal->prec() == g->prec());
             new_goal->inc_depth();
-            new_goal->add(g->mc());
-            new_goal->add(g->pc());
 
             for (unsigned i = 0; i < g->size(); i++) {
                 expr * f = g->form(i);
@@ -375,7 +373,7 @@ class recover_01_tactic : public tactic {
                 new_goal->update(idx, new_curr);
             }
             result.push_back(new_goal.get());
-            TRACE("recover_01", new_goal->display(tout););
+            TRACE("recover_01", new_goal->display(tout); if (new_goal->mc()) new_goal->mc()->display(tout););
             SASSERT(new_goal->is_well_formed());
         }
         

src/tactic/core/pb_preprocess_tactic.cpp

@@ -139,7 +139,8 @@ public:
         }
         
         for (unsigned i = 0; i < m_ge.size(); ++i) {
-            classify_vars(i, to_app(g->form(m_ge[i])));
+            if (!classify_vars(i, to_app(g->form(m_ge[i]))))
+                return false;
         }
         
         declassifier dcl(m_vars);
@@ -199,7 +200,7 @@ public:
             expr* fml = g->form(m_ge[i]);
             if (!to_ge(fml, args1, coeffs1, k1)) continue;
             if (args1.empty()) continue;
-            expr* arg = args1[0].get();
+            expr* arg = args1.get(0);
             bool neg = m.is_not(arg, arg);
             if (!is_uninterp_const(arg)) continue;
             if (!m_vars.contains(to_app(arg))) continue;
@@ -377,15 +378,15 @@ private:
         }
     }
 
-    void classify_vars(unsigned idx, app* e) {
+    bool classify_vars(unsigned idx, app* e) {
         expr* r;
         if (m.is_not(e, r) && is_uninterp_const(r)) {
             insert(idx, to_app(r), false);
-            return;
+            return true;
         }
         if (is_uninterp_const(e)) {
             insert(idx, e, true);
-            return;
+            return true;
         }
         for (unsigned i = 0; i < e->get_num_args(); ++i) {
             expr* arg = e->get_arg(i);
@@ -393,14 +394,17 @@ private:
                 // no-op
             }
             else if (m.is_not(arg, r)) {
-                SASSERT(is_uninterp_const(r));
+                if (!is_uninterp_const(r))
+                    return false;
                 insert(idx, to_app(r), false);
             }
             else {
-                SASSERT(is_uninterp_const(arg));
+                if (!is_uninterp_const(arg))
+                    return false;
                 insert(idx, to_app(arg), true);
             }
         }
+        return true;
     }
 
     void insert(unsigned i, app* e, bool pos) {
@@ -478,24 +482,28 @@ private:
         expr_ref_vector args1(m), args2(m);
         vector<rational> coeffs1, coeffs2;        
         rational k1, k2;
-        if (!to_ge(fml1, args1, coeffs1, k1)) return;
-        if (!k1.is_one()) return;
-        if (!to_ge(g->form(idx2), args2, coeffs2, k2)) return;
+        if (!to_ge(fml1, args1, coeffs1, k1) || !k1.is_one()) 
+            return;
+        if (!to_ge(fml2, args2, coeffs2, k2)) 
+            return;
         // check that each variable in idx1 occurs only in idx2
         unsigned min_index = 0;
         rational min_coeff(0);
         unsigned_vector indices;
         for (unsigned i = 0; i < args1.size(); ++i) {
-            expr* x = args1[i].get();
+            expr* x = args1.get(i);
             m.is_not(x, x);
-            if (!is_app(x)) return;
-            if (!m_vars.contains(to_app(x))) return;            
+            if (!is_app(x) || !m_vars.contains(to_app(x))) 
+                return;            
             TRACE("pb", tout << mk_pp(x, m) << "\n";);
             rec const& r = m_vars.find(to_app(x));
-            if (r.pos.size() != 1 || r.neg.size() != 1) return;
-            if (r.pos[0] != idx2 && r.neg[0] != idx2) return;
+            if (r.pos.size() != 1 || r.neg.size() != 1) 
+                return;
+            if (r.pos[0] != idx2 && r.neg[0] != idx2) 
+                return;
+            bool found = false;
             for (unsigned j = 0; j < args2.size(); ++j) {
-                if (is_complement(args1[i].get(), args2[j].get())) {
+                if (is_complement(args1.get(i), args2.get(j))) {
                     if (i == 0) {
                         min_coeff = coeffs2[j];
                     }
@@ -504,12 +512,15 @@ private:
                         min_index = j;
                     }
                     indices.push_back(j);
+                    found = true;
                 }                
             }
+            if (!found)
+                return;
         }
         for (unsigned i = 0; i < indices.size(); ++i) {
             unsigned j = indices[i];
-            expr* arg = args2[j].get();
+            expr* arg = args2.get(j);
             if (j == min_index) {
                 args2[j] = m.mk_false();
             }
@@ -521,9 +532,7 @@ private:
         
         tmp1 = pb.mk_ge(args2.size(), coeffs2.data(), args2.data(), k2);
         IF_VERBOSE(3, verbose_stream() << " " << tmp1 << "\n";
-                   for (unsigned i = 0; i < args2.size(); ++i) {
-                       verbose_stream() << mk_pp(args2[i].get(), m) << " ";
-                   }
+                   verbose_stream() << args2 << "\n";
                    verbose_stream() << "\n";
                    );
         m_r(tmp1, tmp2);

src/tactic/generic_model_converter.cpp

@@ -139,68 +139,6 @@ void generic_model_converter::set_env(ast_pp_util* visitor) {
     }
 }
 
-struct min_app_idx_proc {
-    unsigned m_min;
-    obj_map<func_decl, unsigned>& m_idxs;
-    min_app_idx_proc(obj_map<func_decl, unsigned>& idxs) : m_min(UINT_MAX), m_idxs(idxs) {}
-    void operator()(app * n) {
-        unsigned idx;
-        if (m_idxs.find(n->get_decl(), idx)) {
-            m_min = std::min(m_min, idx);
-        }
-    }
-    void operator()(var * n) {}
-    void operator()(quantifier * n) {}
-};
-
-void generic_model_converter::operator()(expr_ref& fml) {
-    min_app_idx_proc min_proc(m_first_idx);
-    for_each_expr(min_proc, fml);
-    unsigned min_idx = min_proc.m_min;
-    if (min_idx == UINT_MAX) return;
-    expr_ref_vector fmls(m);
-    fmls.push_back(fml);
-    for (unsigned i = m_entries.size(); i-- > min_idx;) {
-        entry const& e = m_entries[i];
-        if (e.m_instruction != instruction::ADD) {
-            continue;
-        }
-        unsigned arity = e.m_f->get_arity();
-        if (arity == 0) {
-            fmls.push_back(simplify_def(e));
-        }
-        else {
-            expr_ref_vector args(m);
-            sort_ref_vector sorts(m);
-            svector<symbol> names;
-            for (unsigned i = 0; i < arity; ++i) {
-                sorts.push_back(e.m_f->get_domain(i));
-                names.push_back(symbol(i));
-                args.push_back(m.mk_var(i, sorts.back()));
-            }
-            // TBD: check if order is correct with respect to quantifier binding ordering
-            expr_ref lhs(m.mk_app(e.m_f, arity, args.data()), m);
-            expr_ref body(m.mk_eq(lhs, e.m_def), m);
-            fmls.push_back(m.mk_forall(arity, sorts.data(), names.data(), body));
-        }
-        if (m_first_idx[e.m_f] == i) {
-            m_first_idx.remove(e.m_f);
-        }
-    }
-    unsigned j = min_idx;
-    for (unsigned i = min_idx; i < m_entries.size(); ++i) {
-        entry& e = m_entries[i];
-        if (e.m_instruction == instruction::HIDE) {
-            if (i != j) {
-                m_entries[j] = e;
-            }
-            ++j;
-        }
-    }
-    m_entries.shrink(j);
-    fml = mk_and(fmls);
-}
-
 void generic_model_converter::get_units(obj_map<expr, bool>& units) {
     th_rewriter rw(m);
     expr_safe_replace rep(m);

src/tactic/generic_model_converter.h

@@ -54,6 +54,8 @@ public:
     
     void operator()(model_ref & md) override;
 
+    void operator()(expr_ref& fml) override { UNREACHABLE(); }
+
     void cancel() override {}
 
     void display(std::ostream & out) override;
@@ -64,8 +66,6 @@ public:
 
     void set_env(ast_pp_util* visitor) override;
 
-    void operator()(expr_ref& fml) override; 
-
     void get_units(obj_map<expr, bool>& units) override;
 };
 

src/tactic/horn_subsume_model_converter.cpp

@@ -169,10 +169,6 @@ void horn_subsume_model_converter::add_default_false_interpretation(expr* e, mod
 }
 
 
-void horn_subsume_model_converter::operator()(expr_ref& fml) {
-    NOT_IMPLEMENTED_YET();
-}
-
 void horn_subsume_model_converter::operator()(model_ref& mr) {
 
     func_decl_ref pred(m);

src/tactic/horn_subsume_model_converter.h

@@ -72,8 +72,6 @@ public:
     
     void operator()(model_ref& _m) override;
 
-    void operator()(expr_ref& fml) override;
-
     model_converter * translate(ast_translation & translator) override;
 
     ast_manager& get_manager() { return m; }

src/tactic/model_converter.h

@@ -76,6 +76,8 @@ public:
     virtual void operator()(model_ref & m) = 0;
 
     virtual void operator()(labels_vec & r) {}
+
+    virtual void operator()(expr_ref& fml) { UNREACHABLE(); }
     
     virtual model_converter * translate(ast_translation & translator) = 0;
     
@@ -86,7 +88,6 @@ public:
        The operator has as side effect of adding definitions as assertions to the
        formula and removing these definitions from the model converter.
      */
-    virtual void operator()(expr_ref& formula) { UNREACHABLE(); }
 
     virtual void get_units(obj_map<expr, bool>& fmls) { UNREACHABLE(); }
 };

src/tactic/portfolio/CMakeLists.txt

@@ -3,6 +3,7 @@ z3_add_component(portfolio
     default_tactic.cpp
     smt_strategic_solver.cpp
     solver2lookahead.cpp
+    solver_subsumption_tactic.cpp
   COMPONENT_DEPENDENCIES
     aig_tactic
     fp
@@ -16,4 +17,6 @@ z3_add_component(portfolio
     fd_solver
   TACTIC_HEADERS
     default_tactic.h
+    solver_subsumption_tactic.h
+
 )

src/tactic/portfolio/solver_subsumption_tactic.cpp

@@ -0,0 +1,172 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    solver_subsumption_tactic.cpp
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-7-23
+
+--*/
+#include "ast/ast_util.h"
+#include "tactic/tactical.h"
+#include "tactic/portfolio/solver_subsumption_tactic.h"
+#include "solver/solver.h"
+
+class solver_subsumption_tactic : public tactic {
+    ast_manager& m;
+    params_ref    m_params;
+    solver_ref    m_solver;
+
+    void push() {
+        m_solver->push();
+    }
+
+    void pop() {
+        m_solver->pop(1);
+    }
+
+    void assert_expr(expr* f) {
+        m_solver->assert_expr(f);
+    }
+
+    bool subsumed(expr* f) {
+        expr_ref_vector fmls(m);
+        fmls.push_back(m.mk_not(f));
+        lbool is_sat = m_solver->check_sat(fmls);
+        return (is_sat == l_false);
+    }
+
+    /**
+    * Check subsumption (a \/ b \/ c)
+    * if (a \/ b) is already implied
+    * Use a naive algorithm (not binary disection here)
+    */
+
+    bool simplify(expr_ref& f) {
+        if (!m.is_or(f))
+            return false;
+        expr_ref_vector ors(m);
+        ors.append(to_app(f)->get_num_args(), to_app(f)->get_args());
+        expr_ref_vector prefix(m);
+        for (unsigned i = 0; i < ors.size(); ++i) {
+            expr_ref_vector fmls(m);
+            fmls.append(prefix);
+            for (unsigned k = i + 1; k < ors.size(); ++k)
+                fmls.push_back(m.mk_not(ors.get(k)));
+            lbool is_sat = m_solver->check_sat(fmls);
+            if (is_sat == l_false)
+                continue;
+            fmls.reset();
+            fmls.push_back(ors.get(i));
+            
+            is_sat = m_solver->check_sat(fmls);
+            if (is_sat == l_false)
+                continue;
+            prefix.push_back(ors.get(i));                
+        }
+        if (ors.size() != prefix.size()) {
+            ors.reset();
+            ors.append(prefix.size(), prefix.data());
+            f = mk_or(ors);
+            return true;
+        }
+        return false;
+    }
+
+    void simplify(vector<std::pair<unsigned, expr_ref>>& fmls, unsigned_vector& change) {
+
+        if (fmls.size() == 0)
+            return;
+
+        if (fmls.size() == 1) {
+            if (subsumed(fmls[0].second)) {                
+                change.push_back(fmls[0].first);
+                fmls[0].second = m.mk_true();                
+            }
+            else if (simplify(fmls[0].second)) 
+                change.push_back(fmls[0].first);            
+            return;
+        }
+        unsigned mid = fmls.size() / 2;
+
+        vector<std::pair<unsigned, expr_ref>> pre(mid, fmls.data());
+        vector<std::pair<unsigned, expr_ref>> post(fmls.size() - mid, fmls.data() + mid);
+        push();
+        for (auto [p, f] : post)
+            assert_expr(f);
+        simplify(pre, change);
+        pop();
+        push();
+        for (auto [p, f] : pre)
+            assert_expr(f);
+        simplify(post, change);
+        pop();
+        if (!change.empty()) {
+            fmls.reset();
+            fmls.append(pre);
+            fmls.append(post);
+        }
+    }
+
+public:
+    solver_subsumption_tactic(ast_manager& m, params_ref const& p) :
+        m(m),
+        m_params(p) {
+    }
+
+    tactic* translate(ast_manager& other_m) override {
+        return alloc(solver_subsumption_tactic, other_m, m_params);
+    }
+
+    ~solver_subsumption_tactic() override {}
+
+    void updt_params(params_ref const& p) override { 
+        m_params = p; 
+        unsigned max_conflicts = p.get_uint("max_conflicts", 2);
+        m_params.set_uint("sat.max_conflicts", max_conflicts);
+        m_params.set_uint("smt.max_conflicts", max_conflicts);
+    }
+
+    void collect_param_descrs(param_descrs& r) override { 
+        r.insert("max_conflicts", CPK_UINT, "(default: 10) maximal number of conflicts allowed per solver call.");
+    }
+
+    void operator()(goal_ref const& g, goal_ref_buffer& result) override {
+        TRACE("tactic", tout << "params: " << m_params << "\n"; g->display(tout););
+        tactic_report report("subsumption", *g);
+
+        vector<std::pair<unsigned, expr_ref>> fmls;
+        unsigned_vector change;
+        unsigned sz = g->size();
+        if (sz == 1) {
+            result.push_back(g.get());
+            return;
+        }
+        for (unsigned i = 0; i < sz; i++)
+            fmls.push_back(std::make_pair(i, expr_ref(g->form(i), m)));
+        if (!m_solver) {
+            scoped_ptr<solver_factory> f = mk_smt_strategic_solver_factory();
+            m_solver = (*f)(m, m_params, false, false, true, symbol::null);
+        }
+        simplify(fmls, change);
+        if (change.empty()) {
+            result.push_back(g.get());
+            return;
+        }
+        g->inc_depth();
+        for (unsigned idx : change)
+            g->update(idx, fmls[idx].second);
+        g->elim_true();
+        result.push_back(g.get());
+    }
+
+    void cleanup() override {}
+};
+
+tactic* mk_solver_subsumption_tactic(ast_manager& m, params_ref const& p) {
+    return alloc(solver_subsumption_tactic, m, p);
+}
+

src/tactic/portfolio/solver_subsumption_tactic.h

@@ -0,0 +1,25 @@
+/*++
+Copyright (c) 2011 Microsoft Corporation
+
+Module Name:
+
+    solver_subsumption_tactic.h
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-7-23
+
+--*/
+#pragma once
+
+#include "util/params.h"
+class ast_manager;
+class tactic;
+
+tactic * mk_solver_subsumption_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+/*
+  ADD_TACTIC("solver_subsumption", "remove assertions that are subsumed.", "mk_solver_subsumption_tactic(m, p)")
+*/
+
+

src/tactic/sine_filter.cpp

@@ -1,236 +0,0 @@
-/*++
-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 "tactic/sine_filter.h"
-#include "tactic/tactical.h"
-#include "tactic/generic_model_converter.h"
-#include "ast/datatype_decl_plugin.h"
-#include "ast/rewriter/rewriter_def.h"
-#include "ast/rewriter/var_subst.h"
-#include "ast/ast_util.h"
-#include "util/obj_pair_hashtable.h"
-#include "ast/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) {}
-
-    tactic * translate(ast_manager & m) override {
-        return alloc(sine_tactic, m, m_params);
-    }
-
-    void updt_params(params_ref const & p) override {
-    }
-
-    void collect_param_descrs(param_descrs & r) override {
-    }
-
-    void operator()(goal_ref const & g, goal_ref_buffer& result) override {
-        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), nullptr, nullptr);
-        }
-        g->inc_depth();
-        g->updt_prec(goal::OVER);
-        result.push_back(g.get());
-        TRACE("sine", result[0]->display(tout););
-        SASSERT(g->is_well_formed());
-    }
-
-    void cleanup() override {
-    }
-
-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) && is_uninterp(curr)) {
-                app *a = to_app(curr);
-                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 (func_decl* f : consts) tout << f->get_name() << "\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;
-        t_work_item curr;
-
-        for (unsigned i = 0; i < g->size(); i++)
-            stack.push_back(work_item(g->form(i), g->form(i)));
-
-        while (!stack.empty()) {
-            curr = stack.back();
-            stack.pop_back();
-            if (is_app(curr.first) && is_uninterp(curr.first)) {
-                app * a = to_app(curr.first);
-                func_decl * f = a->get_decl();
-                if (!consts.contains(f)) {
-                    consts.insert(f);
-                    if (const2quantifier.contains(f)) {
-                        for (auto const& p : const2quantifier[f]) 
-                            stack.push_back(p);
-                        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 (is_forall(q)) {
-                    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 (is_exists(q)) {
-                    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);
-            if (!exp2const.contains(visiting))
-                continue;
-            for (func_decl* f : exp2const[visiting]) 
-                for (expr* e : const2exp[f]) {
-                    if (!visited.contains(e))
-                        to_visit.push_back(e);
-                }
-        }
-
-        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

@@ -1,30 +0,0 @@
-/*++
-Copyright (c) 2016 Microsoft Corporation
-
-Module Name:
-
-    sine_filter.h
-
-Abstract:
-
-    Tactic that performs Sine Qua Non premise selection
-
-Author:
-
-    Doug Woos
-
-Revision History:
-
---*/
-#pragma once
-
-#include "util/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)")
-*/
-

src/util/mpq.cpp

@@ -260,6 +260,7 @@ void mpq_manager<SYNCH>::set(mpq & a, char const * val) {
             if (exp > 0) {
                 _scoped_numeral<mpq_manager<SYNCH>> _exp(*this);
                 _scoped_numeral<mpq_manager<SYNCH>> _qten(*this);
+                _qten = 10;
                 power(_qten, static_cast<unsigned>(exp), _exp);
                 TRACE("mpq_set", tout << "a: " << to_string(a) << ", exp_sign:" << exp_sign << ", exp: " << exp << " " << to_string(_exp) << std::endl;);
                 if (exp_sign)