merge

RELEASE_NOTES.md

@@ -7,6 +7,15 @@ Version 4.next
     - CDCL core for SMT queries. It extends the SAT engine with theory solver plugins.
   - add global incremental pre-processing for the legacy core.
 
+Version 4.15.3
+==============
+- Add UserPropagator callback option for quantifier instantiations. It allows the user propagator to
+  intercept quantifier instantiations. It can then inspect these in the callback. By returning false, 
+  the callback signals that the instantiation should be discarded by the solver. The user propagator 
+  is then able to apply finer control over instantiations. It can also use this mechanism to delay
+  instantiations.
+- Deprecate z3str3
+
 Version 4.15.2
 ==============
 - #7690, #7691 - fix leak introduced in arithmetic solver.

scripts/find_non_defined_param_eval_patterns.py

@@ -0,0 +1,41 @@
+#!/usr/bin/env python3
+"""
+sus.py: Search for function calls with three function-call arguments (ambiguous parameter evaluation order)
+and print matches in grep-like format: file:line:match
+"""
+import os
+import re
+# skip chain calls like obj.method(...)
+chain_pattern = re.compile(r"\.\s*[A-Za-z_]\w*\s*\(")
+
+# pattern: identifier(... foo(...), ... bar(...)) with two function-call args
+pattern = re.compile(
+    r"\b[A-Za-z_]\w*"             # function name
+    r"\s*\(\s*"                 # '('
+    r"[^)]*?[A-Za-z_]\w*\([^)]*\)"  # first func-call arg anywhere
+    r"[^)]*?,[^)]*?[A-Za-z_]\w*\([^)]*\)"  # second func-call arg
+    r"[^)]*?\)"                   # up to closing ')'
+)
+
+# file extensions to include
+excl = ('TRACE', 'ASSERT', 'VERIFY', )
+
+for root, dirs, files in os.walk('src/smt'):
+    # skip hidden dirs
+    dirs[:] = [d for d in dirs if not d.startswith('.')]
+    for file in files:
+        path = os.path.join(root, file)
+        try:
+            with open(path, 'r', encoding='utf-8', errors='ignore') as f:
+                for i, line in enumerate(f, 1):
+                    if pattern.search(line):
+                        # skip lines with TRACE or ASSERT in all caps
+                        if 'TRACE' in line or 'ASSERT' in line or 'VERIFY' in line:
+                            continue
+                        # skip chain calls (method-style chaining)
+                        if chain_pattern.search(line):
+                            continue
+                        full_path = os.path.abspath(path)
+                        print(f"{full_path}:{i}:{line.rstrip()}")
+        except OSError:
+            pass

scripts/mk_project.py

@@ -19,14 +19,13 @@ def init_project_def():
     add_lib('dd', ['util', 'interval'], 'math/dd')
     add_lib('simplex', ['util'], 'math/simplex')
     add_lib('hilbert', ['util'], 'math/hilbert')
-    add_lib('automata', ['util'], 'math/automata')
     add_lib('realclosure', ['interval'], 'math/realclosure')
     add_lib('subpaving', ['interval'], 'math/subpaving')
     add_lib('ast', ['util', 'polynomial'])
     add_lib('params', ['util', 'ast'])
     add_lib('parser_util', ['ast'], 'parsers/util')
     add_lib('grobner', ['ast', 'dd', 'simplex'], 'math/grobner')    
-    add_lib('rewriter', ['ast', 'polynomial', 'interval', 'automata', 'params'], 'ast/rewriter')
+    add_lib('rewriter', ['ast', 'polynomial', 'interval', 'params'], 'ast/rewriter')
     add_lib('euf', ['ast', 'rewriter'], 'ast/euf')
     add_lib('normal_forms', ['rewriter'], 'ast/normal_forms')
     add_lib('macros', ['rewriter'], 'ast/macros')

scripts/update_api.py

@@ -641,6 +641,7 @@ def mk_java(java_src, java_dir, package_name):
   public static native void propagateRegisterEq(Object o, long ctx, long solver);
   public static native void propagateRegisterDecide(Object o, long ctx, long solver);
   public static native void propagateRegisterFinal(Object o, long ctx, long solver);
+  public static native void propagateRegisterOnBinding(Object o, long ctx, long solver);
   public static native void propagateAdd(Object o, long ctx, long solver, long javainfo, long e);
   public static native boolean propagateConsequence(Object o, long ctx, long solver, long javainfo, int num_fixed, long[] fixed, long num_eqs, long[] eq_lhs, long[] eq_rhs, long conseq);
   public static native boolean propagateNextSplit(Object o, long ctx, long solver, long javainfo, long e, long idx, int phase);
@@ -685,6 +686,10 @@ def mk_java(java_src, java_dir, package_name):
         Native.propagateRegisterFinal(this, ctx, solver);
     }
     
+    protected final void registerOnBinding() {
+        Native.propagateRegisterOnBinding(this, ctx, solver);
+    }
+
     protected abstract void pushWrapper();
 
     protected abstract void popWrapper(int number);
@@ -700,6 +705,8 @@ def mk_java(java_src, java_dir, package_name):
     protected abstract void fixedWrapper(long lvar, long lvalue);
 
     protected abstract void decideWrapper(long lvar, int bit, boolean is_pos);
+
+    protected abstract boolean onBindingWrapper(long q, long inst);
   }
     """)
     java_native.write('\n')
@@ -1392,6 +1399,7 @@ z3_ml_callbacks = frozenset([
     'Z3_solver_propagate_diseq',
     'Z3_solver_propagate_created',
     'Z3_solver_propagate_decide',
+    'Z3_solver_propagate_on_binding',
     'Z3_solver_register_on_clause'
     ])
 
@@ -1944,6 +1952,7 @@ Z3_eq_eh    = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_
 
 Z3_created_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
 Z3_decide_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint, ctypes.c_int)
+Z3_on_binding_eh = ctypes.CFUNCTYPE(ctypes.c_bool, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
 
 _lib.Z3_solver_register_on_clause.restype = None
 _lib.Z3_solver_propagate_init.restype = None

src/CMakeLists.txt

@@ -39,7 +39,6 @@ add_subdirectory(math/polynomial)
 add_subdirectory(math/dd)
 add_subdirectory(math/hilbert)
 add_subdirectory(math/simplex)
-add_subdirectory(math/automata)
 add_subdirectory(math/interval)
 add_subdirectory(math/realclosure)
 add_subdirectory(math/subpaving)

src/api/api_ast.cpp

@@ -800,12 +800,11 @@ extern "C" {
         unsigned timeout     = p.get_uint("timeout", mk_c(c)->get_timeout());
         bool     use_ctrl_c  = p.get_bool("ctrl_c", false);
         th_rewriter m_rw(m, p);
-        m_rw.set_solver(alloc(api::seq_expr_solver, m, p));
         expr_ref    result(m);
         cancel_eh<reslimit> eh(m.limit());
         api::context::set_interruptable si(*(mk_c(c)), eh);
         {
-            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_ctrl_c ctrlc(eh, use_ctrl_c);
             scoped_timer timer(timeout, &eh);
             try {
                 m_rw(a, result);

src/api/api_context.h

@@ -57,23 +57,6 @@ namespace smt2 {
 
 namespace api {
        
-    class seq_expr_solver : public expr_solver {
-        ast_manager& m;
-        params_ref const& p;
-        solver_ref   s;
-    public:
-        seq_expr_solver(ast_manager& m, params_ref const& p): m(m), p(p) {}
-        lbool check_sat(expr* e) override {
-            if (!s) {
-                s = mk_smt_solver(m, p, symbol("ALL"));
-            }
-            s->push();
-            s->assert_expr(e);
-            lbool r = s->check_sat();
-            s->pop(1);
-            return r;
-        }
-    };
 
 
     class context : public tactic_manager {

src/api/api_datalog.cpp

@@ -287,7 +287,7 @@ extern "C" {
             cancel_eh<reslimit> eh(mk_c(c)->m().limit());
             api::context::set_interruptable si(*(mk_c(c)), eh);        
             scoped_timer timer(timeout, &eh);
-            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_ctrl_c ctrlc(eh, use_ctrl_c);
             try {
                 r = to_fixedpoint_ref(d)->ctx().query(to_expr(q));
             }

src/api/api_model.cpp

@@ -160,9 +160,6 @@ extern "C" {
         model * _m = to_model_ref(m);
         params_ref p;
         ast_manager& mgr = mk_c(c)->m();
-        if (!_m->has_solver()) {
-            _m->set_solver(alloc(api::seq_expr_solver, mgr, p));
-        }
         expr_ref result(mgr);
         model::scoped_model_completion _scm(*_m, model_completion);
         result = (*_m)(to_expr(t));

src/api/api_opt.cpp

@@ -154,7 +154,7 @@ extern "C" {
         bool     use_ctrl_c  = to_optimize_ptr(o)->get_params().get_bool("ctrl_c", true);
         api::context::set_interruptable si(*(mk_c(c)), eh);        
         {
-            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_ctrl_c ctrlc(eh, use_ctrl_c);
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {

src/api/api_solver.cpp

@@ -650,7 +650,7 @@ extern "C" {
         api::context::set_interruptable si(*(mk_c(c)), eh);
         lbool result = l_undef;
         {
-            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_ctrl_c ctrlc(eh, use_ctrl_c);
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
@@ -748,7 +748,7 @@ extern "C" {
         cancel_eh<reslimit> eh(mk_c(c)->m().limit());
         to_solver(s)->set_eh(&eh);
         {
-            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_ctrl_c ctrlc(eh, use_ctrl_c);
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
@@ -871,7 +871,7 @@ extern "C" {
         to_solver(s)->set_eh(&eh);
         api::context::set_interruptable si(*(mk_c(c)), eh);
         {
-            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_ctrl_c ctrlc(eh, use_ctrl_c);
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
@@ -919,7 +919,7 @@ extern "C" {
         to_solver(s)->set_eh(&eh);
         api::context::set_interruptable si(*(mk_c(c)), eh);
         {
-            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_ctrl_c ctrlc(eh, use_ctrl_c);
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
@@ -1160,6 +1160,14 @@ extern "C" {
         Z3_CATCH;
     }
 
+    void Z3_API Z3_solver_propagate_on_binding(Z3_context c, Z3_solver s, Z3_on_binding_eh binding_eh) {
+        Z3_TRY;
+        RESET_ERROR_CODE();
+        user_propagator::binding_eh_t c = (bool(*)(void*, user_propagator::callback*, expr*, expr*))binding_eh;
+        to_solver_ref(s)->user_propagate_register_on_binding(c);
+        Z3_CATCH;
+    }
+
     bool Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb,  Z3_ast t, unsigned idx, Z3_lbool phase) {
         Z3_TRY;
         LOG_Z3_solver_next_split(c, cb, t, idx, phase);

src/api/api_tactic.cpp

@@ -427,7 +427,7 @@ extern "C" {
 
         api::context::set_interruptable si(*(mk_c(c)), eh);
         {
-            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_ctrl_c ctrlc(eh, use_ctrl_c);
             scoped_timer timer(timeout, &eh);
             try {
                 exec(*to_tactic_ref(t), new_goal, ref->m_subgoals);

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

@@ -4295,12 +4295,14 @@ namespace z3 {
         typedef std::function<void(expr const&, expr const&)> eq_eh_t;
         typedef std::function<void(expr const&)> created_eh_t;
         typedef std::function<void(expr, unsigned, bool)> decide_eh_t;
+        typedef std::function<bool(expr const&, expr const&)> on_binding_eh_t;
 
         final_eh_t m_final_eh;
         eq_eh_t    m_eq_eh;
         fixed_eh_t m_fixed_eh;
         created_eh_t m_created_eh;
         decide_eh_t m_decide_eh;
+        on_binding_eh_t m_on_binding_eh;
         solver*    s;
         context*   c;
         std::vector<z3::context*> subcontexts;
@@ -4373,6 +4375,13 @@ namespace z3 {
             p->m_decide_eh(val, bit, is_pos);
         }
 
+        static bool on_binding_eh(void* _p, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst) {
+            user_propagator_base* p = static_cast<user_propagator_base*>(_p);
+            scoped_cb _cb(p, cb);
+            expr q(p->ctx(), _q), inst(p->ctx(), _inst);
+            return p->m_on_binding_eh(q, inst);
+        }
+        
     public:
         user_propagator_base(context& c) : s(nullptr), c(&c) {}
         
@@ -4498,6 +4507,14 @@ namespace z3 {
             }
         }
 
+        void register_on_binding() {
+            m_on_binding_eh = [this](expr const& q, expr const& inst) {
+                return on_binding(q, inst);
+            };
+            if (s) 
+                Z3_solver_propagate_on_binding(ctx(), *s, on_binding_eh);
+        }
+
         virtual void fixed(expr const& /*id*/, expr const& /*e*/) { }
 
         virtual void eq(expr const& /*x*/, expr const& /*y*/) { }
@@ -4508,6 +4525,8 @@ namespace z3 {
         
         virtual void decide(expr const& /*val*/, unsigned /*bit*/, bool /*is_pos*/) {}
 
+        virtual bool on_binding(expr const& /*q*/, expr const& /*inst*/) { return true; }
+
         bool next_split(expr const& e, unsigned idx, Z3_lbool phase) {
             assert(cb);
             return Z3_solver_next_split(ctx(), cb, e, idx, phase);

src/api/dotnet/UserPropagator.cs

@@ -65,6 +65,14 @@ namespace Microsoft.Z3
         /// <param name="phase">The tentative truth-value</param>
         public delegate void DecideEh(Expr term, uint idx, bool phase);
 
+        /// <summary>
+        /// Delegate type for callback when a quantifier is bound to an instance.
+        /// </summary>
+        /// <param name="q">Quantifier</param>
+        /// <param name="inst">Instance</param>
+        /// <returns>true if binding is allowed to take effect in the solver, false if blocked by callback</returns>
+        public delegate bool OnBindingEh(Expr q, Expr inst);
+
         // access managed objects through a static array.
         // thread safety is ignored for now.
         GCHandle gch;
@@ -78,6 +86,7 @@ namespace Microsoft.Z3
         EqEh diseq_eh;
         CreatedEh created_eh;
         DecideEh decide_eh;
+        OnBindingEh on_binding_eh;
 
         Native.Z3_push_eh push_eh;
         Native.Z3_pop_eh pop_eh;
@@ -89,6 +98,7 @@ namespace Microsoft.Z3
         Native.Z3_eq_eh diseq_wrapper;
         Native.Z3_decide_eh decide_wrapper;
         Native.Z3_created_eh created_wrapper;
+        Native.Z3_on_binding_eh on_binding_wrapper;
 
         void Callback(Action fn, Z3_solver_callback cb)
         {
@@ -175,6 +185,19 @@ namespace Microsoft.Z3
             prop.Callback(() => prop.decide_eh(t, idx, phase), cb);
         }
 
+        static bool _on_binding(voidp _ctx, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst)
+        {
+            var prop = (UserPropagator)GCHandle.FromIntPtr(_ctx).Target;
+            using var q = Expr.Create(prop.ctx, _q);
+            using var inst = Expr.Create(prop.ctx, _inst);
+            bool result = true;
+            prop.Callback(() => {
+                if (prop.on_binding_wrapper != null)
+                    result = prop.on_binding_eh(q, inst);
+            }, cb);
+            return result;
+        }
+
         /// <summary>
         /// Propagator constructor from a solver class.
         /// </summary>        
@@ -362,6 +385,20 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Set binding callback
+        /// </summary>
+        public OnBindingEh OnBinding
+        {
+            set
+            {
+                this.on_binding_wrapper = _on_binding;
+                this.on_binding_eh = value;
+                if (solver != null)
+                    Native.Z3_solver_propagate_on_binding(ctx.nCtx, solver.NativeObject, on_binding_wrapper);
+            }
+        }
+
 
         /// <summary>
         /// Set the next decision
@@ -378,6 +415,8 @@ namespace Microsoft.Z3
             return Native.Z3_solver_next_split(ctx.nCtx, this.callback, e?.NativeObject ?? IntPtr.Zero, idx, phase) != 0;
         }
 
+        
+
         /// <summary>
         /// Track assignments to a term
         /// </summary>

src/api/java/NativeStatic.txt

@@ -92,6 +92,7 @@ struct JavaInfo {
   jmethodID eq = nullptr;
   jmethodID final = nullptr;
   jmethodID decide = nullptr;
+  jmethodID on_binding = nullptr;
 
   Z3_solver_callback cb = nullptr;
 };
@@ -153,6 +154,12 @@ static void decide_eh(void* _p, Z3_solver_callback cb, Z3_ast _val, unsigned bit
   info->jenv->CallVoidMethod(info->jobj, info->decide, (jlong)_val, bit, is_pos);
 }
 
+static jboolean on_binding_eh(void* _p, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst) {
+  JavaInfo *info = static_cast<JavaInfo*>(_p);
+  ScopedCB scoped(info, cb);
+  return info->jenv->CallBooleanMethod(info->jobj, info->on_binding, (jlong)_q, (jlong)_inst);
+}
+
 DLL_VIS JNIEXPORT jlong JNICALL Java_com_microsoft_z3_Native_propagateInit(JNIEnv *jenv, jclass cls, jobject jobj, jlong ctx, jlong solver) {
   JavaInfo *info = new JavaInfo;
 
@@ -167,6 +174,7 @@ DLL_VIS JNIEXPORT jlong JNICALL Java_com_microsoft_z3_Native_propagateInit(JNIEn
   info->eq = jenv->GetMethodID(jcls, "eqWrapper", "(JJ)V");
   info->final = jenv->GetMethodID(jcls, "finWrapper", "()V");
   info->decide = jenv->GetMethodID(jcls, "decideWrapper", "(JIZ)V");
+  info->on_binding = jenv->GetMethodID(jcls, "onBindingWrapper", "(JIZ)V");
 
   if (!info->push || !info->pop || !info->fresh || !info->created || !info->fixed || !info->eq || !info->final || !info->decide) {
     assert(false);

src/api/java/UserPropagatorBase.java

@@ -43,6 +43,13 @@ public abstract class UserPropagatorBase extends Native.UserPropagatorBase {
         eq(x, y);
     }
 
+    @Override
+    protected final boolean onBindingWrapper(long lq, long linst) {
+        Expr q = new Expr(ctx, lq);
+        Expr inst = new Expr(ctx, linst);
+        return on_binding(q, inst);
+    }
+
     @Override
     protected final UserPropagatorBase freshWrapper(long lctx) {
         return fresh(new Context(lctx));
@@ -78,6 +85,8 @@ public abstract class UserPropagatorBase extends Native.UserPropagatorBase {
 
     public void eq(Expr<?> x, Expr<?> y) {}
     
+    public boolean on_binding(Expr<?> q, Expr<?> inst) { return true; }
+
     public void decide(Expr<?> var, int bit, boolean is_pos) {}
 
     public void fin() {}

src/api/js/scripts/parse-api.ts

@@ -56,6 +56,7 @@ const types = {
   Z3_final_eh: 'Z3_final_eh',
   Z3_created_eh: 'Z3_created_eh',
   Z3_decide_eh: 'Z3_decide_eh',
+  Z3_on_binding_eh: 'Z3_on_binding_eh',
   Z3_on_clause_eh: 'Z3_on_clause_eh',
 } as unknown as Record<string, string>;
 

src/api/python/z3/z3.py

@@ -11815,6 +11815,16 @@ def user_prop_decide(ctx, cb, t_ref, idx, phase):
     prop.decide(t, idx, phase)
     prop.cb = old_cb
 
+def user_prop_binding(ctx, cb, q_ref, inst_ref):
+    prop = _prop_closures.get(ctx)
+    old_cb = prop.cb
+    prop.cb = cb
+    q = _to_expr_ref(to_Ast(q_ref), prop.ctx())
+    inst = _to_expr_ref(to_Ast(inst_ref), prop.ctx())
+    r = prop.binding(q, inst)
+    prop.cb = old_cb
+    return r
+    
 
 _user_prop_push = Z3_push_eh(user_prop_push)
 _user_prop_pop = Z3_pop_eh(user_prop_pop)
@@ -11825,6 +11835,7 @@ _user_prop_final = Z3_final_eh(user_prop_final)
 _user_prop_eq = Z3_eq_eh(user_prop_eq)
 _user_prop_diseq = Z3_eq_eh(user_prop_diseq)
 _user_prop_decide = Z3_decide_eh(user_prop_decide)
+_user_prop_binding = Z3_on_binding_eh(user_prop_binding)
 
 
 def PropagateFunction(name, *sig):
@@ -11873,6 +11884,7 @@ class UserPropagateBase:
         self.diseq = None
         self.decide = None
         self.created = None
+        self.binding = None
         if ctx:
             self.fresh_ctx = ctx
         if s:
@@ -11938,6 +11950,13 @@ class UserPropagateBase:
             Z3_solver_propagate_decide(self.ctx_ref(), self.solver.solver, _user_prop_decide)
         self.decide = decide   
         
+    def add_on_binding(self, binding):
+        assert not self.binding
+        assert not self._ctx
+        if self.solver:
+            Z3_solver_propagate_on_binding(self.ctx_ref(), self.solver.solver, _user_prop_binding)
+        self.binding = binding
+
     def push(self):
         raise Z3Exception("push needs to be overwritten")
 

src/api/z3_api.h

@@ -1440,6 +1440,7 @@ Z3_DECLARE_CLOSURE(Z3_eq_eh,      void, (void* ctx, Z3_solver_callback cb, Z3_as
 Z3_DECLARE_CLOSURE(Z3_final_eh,   void, (void* ctx, Z3_solver_callback cb));
 Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t));
 Z3_DECLARE_CLOSURE(Z3_decide_eh,  void, (void* ctx, Z3_solver_callback cb, Z3_ast t, unsigned idx, bool phase));
+Z3_DECLARE_CLOSURE(Z3_on_binding_eh, bool, (void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst));
 Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals));
 
 
@@ -7225,6 +7226,17 @@ extern "C" {
     */
     void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh);
 
+
+    /**
+       \brief register a callback when the solver instantiates a quantifier.
+       If the callback returns false, the actual instantiation of the quantifier is blocked.
+       This allows the user propagator selectively prioritize instantiations without relying on default
+       or configured weights.
+       
+       def_API('Z3_solver_propagate_on_binding', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_on_binding_eh)))
+    */
+
+    void Z3_API Z3_solver_propagate_on_binding(Z3_context c, Z3_solver s, Z3_on_binding_eh on_binding_eh);
     /**
         Sets the next (registered) expression to split on.
         The function returns false and ignores the given expression in case the expression is already assigned internally

src/ast/rewriter/CMakeLists.txt

@@ -46,7 +46,6 @@ z3_add_component(rewriter
   COMPONENT_DEPENDENCIES
     ast
     params
-    automata
     interval
     polynomial
 )

src/ast/rewriter/seq_rewriter.cpp

@@ -29,8 +29,6 @@ Authors:
 #include "ast/rewriter/var_subst.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "params/seq_rewriter_params.hpp"
-#include "math/automata/automaton.h"
-#include "math/automata/symbolic_automata_def.h"
 
 
 expr_ref sym_expr::accept(expr* e) {
@@ -83,320 +81,6 @@ struct display_expr1 {
     }
 };
 
-class sym_expr_boolean_algebra : public boolean_algebra<sym_expr*> {
-    ast_manager& m;
-    expr_solver& m_solver;
-    expr_ref     m_var;
-    typedef sym_expr* T;
-public:
-    sym_expr_boolean_algebra(ast_manager& m, expr_solver& s): 
-        m(m), m_solver(s), m_var(m) {}
-
-    T mk_false() override {
-        expr_ref fml(m.mk_false(), m);
-        return sym_expr::mk_pred(fml, m.mk_bool_sort()); // use of Bool sort for bound variable is arbitrary
-    }
-    T mk_true() override {
-        expr_ref fml(m.mk_true(), m);
-        return sym_expr::mk_pred(fml, m.mk_bool_sort());
-    }
-    T mk_and(T x, T y) override {
-        seq_util u(m);
-        if (x->is_char() && y->is_char()) {
-            if (x->get_char() == y->get_char()) {
-                return x;
-            }
-            if (m.are_distinct(x->get_char(), y->get_char())) {
-                expr_ref fml(m.mk_false(), m);
-                return sym_expr::mk_pred(fml, x->get_sort());
-            }
-        }
-        unsigned lo1, hi1, lo2, hi2;
-        if (x->is_range() && y->is_range() &&
-            u.is_const_char(x->get_lo(), lo1) && u.is_const_char(x->get_hi(), hi1) &&
-            u.is_const_char(y->get_lo(), lo2) && u.is_const_char(y->get_hi(), hi2)) {
-            lo1 = std::max(lo1, lo2);
-            hi1 = std::min(hi1, hi2);
-            if (lo1 > hi1) {
-                expr_ref fml(m.mk_false(), m);
-                return sym_expr::mk_pred(fml, x->get_sort());
-            }
-            expr_ref _start(u.mk_char(lo1), m);
-            expr_ref _stop(u.mk_char(hi1), m);
-            return sym_expr::mk_range(_start, _stop);
-        }
-
-        sort* s = x->get_sort();
-        if (m.is_bool(s)) s = y->get_sort();
-        var_ref v(m.mk_var(0, s), m);
-        expr_ref fml1 = x->accept(v);
-        expr_ref fml2 = y->accept(v);
-        if (m.is_true(fml1)) {
-            return y;
-        }
-        if (m.is_true(fml2)) {
-            return x;
-        }
-        if (fml1 == fml2) {
-            return x;   
-        }
-        if (is_complement(fml1, fml2)) {
-            expr_ref ff(m.mk_false(), m);
-            return sym_expr::mk_pred(ff, x->get_sort());
-        }
-        expr_ref fml(m);
-        bool_rewriter br(m);
-        br.mk_and(fml1, fml2, fml);
-        return sym_expr::mk_pred(fml, x->get_sort());
-    }
-
-    bool is_complement(expr* f1, expr* f2) {
-        expr* f = nullptr;
-        return 
-            (m.is_not(f1, f) && f == f2) ||
-            (m.is_not(f2, f) && f == f1);
-    }
-
-    T mk_or(T x, T y) override {
-        if (x->is_char() && y->is_char() &&
-            x->get_char() == y->get_char()) {
-            return x;
-        }
-        if (x == y) return x;
-        var_ref v(m.mk_var(0, x->get_sort()), m);
-        expr_ref fml1 = x->accept(v);
-        expr_ref fml2 = y->accept(v);        
-        if (m.is_false(fml1)) return y;
-        if (m.is_false(fml2)) return x;
-        bool_rewriter br(m);
-        expr_ref fml(m);
-        br.mk_or(fml1, fml2, fml);
-        return sym_expr::mk_pred(fml, x->get_sort());
-    }
-
-    T mk_and(unsigned sz, T const* ts) override {
-        switch (sz) {
-        case 0: return mk_true();
-        case 1: return ts[0];
-        default: {
-            T t = ts[0];
-            for (unsigned i = 1; i < sz; ++i) {
-                t = mk_and(t, ts[i]);
-            }
-            return t;
-        }
-        }
-    }
-
-    T mk_or(unsigned sz, T const* ts) override {
-        switch (sz) {
-        case 0: return mk_false();
-        case 1: return ts[0];
-        default: {
-            T t = ts[0];
-            for (unsigned i = 1; i < sz; ++i) {
-                t = mk_or(t, ts[i]);
-            }
-            return t;
-        }
-        }
-    }
-
-    lbool is_sat(T x) override {
-        unsigned lo, hi;
-        seq_util u(m);
-
-        if (x->is_char()) {
-            return l_true;
-        }
-        if (x->is_range() && u.is_const_char(x->get_lo(), lo) && u.is_const_char(x->get_hi(), hi)) {
-            return (lo <= hi) ? l_true : l_false; 
-        }
-        if (x->is_not() && x->get_arg()->is_range() && u.is_const_char(x->get_arg()->get_lo(), lo) && 0 < lo) {
-            return l_true;
-        }            
-        if (!m_var || m_var->get_sort() != x->get_sort()) {
-            m_var = m.mk_fresh_const("x", x->get_sort()); 
-        }
-        expr_ref fml = x->accept(m_var);
-        if (m.is_true(fml)) {
-            return l_true;
-        }
-        if (m.is_false(fml)) {
-            return l_false;
-        }
-        return m_solver.check_sat(fml);
-    }
-
-    T mk_not(T x) override {
-        return sym_expr::mk_not(m, x);    
-    }
-
-};
-
-re2automaton::re2automaton(ast_manager& m): m(m), u(m), m_ba(nullptr), m_sa(nullptr) {}
-
-void re2automaton::set_solver(expr_solver* solver) {
-    m_solver = solver;
-    m_ba = alloc(sym_expr_boolean_algebra, m, *solver);
-    m_sa = alloc(symbolic_automata_t, sm, *m_ba.get());
-}
-
-eautomaton* re2automaton::mk_product(eautomaton* a1, eautomaton* a2) {
-    return m_sa->mk_product(*a1, *a2);
-}
-
-eautomaton* re2automaton::operator()(expr* e) { 
-    eautomaton* r = re2aut(e); 
-    if (r) {        
-        r->compress(); 
-        bool_rewriter br(m);
-        TRACE(seq, display_expr1 disp(m); r->display(tout << mk_pp(e, m) << " -->\n", disp););
-    }
-    return r;
-} 
-
-bool re2automaton::is_unit_char(expr* e, expr_ref& ch) {
-    zstring s;
-    expr* c = nullptr;
-    if (u.str.is_string(e, s) && s.length() == 1) {
-        ch = u.mk_char(s[0]);
-        return true;
-    }
-    if (u.str.is_unit(e, c)) {
-        ch = c;
-        return true;
-    }
-    return false;
-}
-
-eautomaton* re2automaton::re2aut(expr* e) {
-    SASSERT(u.is_re(e));
-    expr *e0, *e1, *e2;
-    scoped_ptr<eautomaton> a, b;
-    unsigned lo, hi;
-    zstring s1, s2;
-    if (u.re.is_to_re(e, e1)) {
-        return seq2aut(e1);
-    }
-    else if (u.re.is_concat(e, e1, e2) && (a = re2aut(e1)) && (b = re2aut(e2))) {
-        return eautomaton::mk_concat(*a, *b);
-    }
-    else if (u.re.is_union(e, e1, e2) && (a = re2aut(e1)) && (b = re2aut(e2))) {
-        return eautomaton::mk_union(*a, *b);
-    }
-    else if (u.re.is_star(e, e1) && (a = re2aut(e1))) {
-        a->add_final_to_init_moves();
-        a->add_init_to_final_states();        
-        return a.detach();            
-    }
-    else if (u.re.is_plus(e, e1) && (a = re2aut(e1))) {
-        a->add_final_to_init_moves();
-        return a.detach();            
-    }
-    else if (u.re.is_opt(e, e1) && (a = re2aut(e1))) {
-        a = eautomaton::mk_opt(*a);
-        return a.detach();                    
-    }
-    else if (u.re.is_range(e, e1, e2)) {
-        expr_ref _start(m), _stop(m);
-        if (is_unit_char(e1, _start) &&
-            is_unit_char(e2, _stop)) {
-            TRACE(seq, tout << "Range: " << _start << " " << _stop << "\n";);
-            a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
-            return a.detach();            
-        }
-        else {
-            // if e1/e2 are not unit, (re.range e1 e2) is defined to be the empty language
-            return alloc(eautomaton, sm);
-        }
-    }
-    else if (u.re.is_complement(e, e0) && (a = re2aut(e0)) && m_sa) {
-        return m_sa->mk_complement(*a);
-    }
-    else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) {
-        scoped_ptr<eautomaton> eps = eautomaton::mk_epsilon(sm);
-        b = eautomaton::mk_epsilon(sm);
-        while (hi > lo) {
-            scoped_ptr<eautomaton> c = eautomaton::mk_concat(*a, *b);
-            b = eautomaton::mk_union(*eps, *c);
-            --hi;
-        }
-        while (lo > 0) {
-            b = eautomaton::mk_concat(*a, *b);
-            --lo;
-        }
-        return b.detach();        
-    }
-    else if (u.re.is_loop(e, e1, lo) && (a = re2aut(e1))) {
-        b = eautomaton::clone(*a);
-        b->add_final_to_init_moves();
-        b->add_init_to_final_states();        
-        while (lo > 0) {
-            b = eautomaton::mk_concat(*a, *b);
-            --lo;
-        }
-        return b.detach();        
-    }
-    else if (u.re.is_empty(e)) {
-        return alloc(eautomaton, sm);
-    }
-    else if (u.re.is_full_seq(e)) {
-        expr_ref tt(m.mk_true(), m);
-        sort *seq_s = nullptr, *char_s = nullptr;
-        VERIFY (u.is_re(e->get_sort(), seq_s));
-        VERIFY (u.is_seq(seq_s, char_s));
-        sym_expr* _true = sym_expr::mk_pred(tt, char_s);
-        return eautomaton::mk_loop(sm, _true);
-    }
-    else if (u.re.is_full_char(e)) {
-        expr_ref tt(m.mk_true(), m);
-        sort *seq_s = nullptr, *char_s = nullptr;
-        VERIFY (u.is_re(e->get_sort(), seq_s));
-        VERIFY (u.is_seq(seq_s, char_s));
-        sym_expr* _true = sym_expr::mk_pred(tt, char_s);
-        a = alloc(eautomaton, sm, _true);
-        return a.detach();
-    }
-    else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
-        eautomaton* r = m_sa->mk_product(*a, *b);
-        TRACE(seq, display_expr1 disp(m); a->display(tout << "a:", disp); b->display(tout << "b:", disp); r->display(tout << "intersection:", disp););
-        return r;
-    }
-    else {        
-        TRACE(seq, tout << "not handled " << mk_pp(e, m) << "\n";);
-    }
-    
-    return nullptr;
-}
-
-eautomaton* re2automaton::seq2aut(expr* e) {
-    SASSERT(u.is_seq(e));
-    zstring s;
-    expr* e1, *e2;
-    scoped_ptr<eautomaton> a, b;
-    if (u.str.is_concat(e, e1, e2) && (a = seq2aut(e1)) && (b = seq2aut(e2))) {
-        return eautomaton::mk_concat(*a, *b);
-    }
-    else if (u.str.is_unit(e, e1)) {
-        return alloc(eautomaton, sm, sym_expr::mk_char(m, e1));
-    }
-    else if (u.str.is_empty(e)) {
-        return eautomaton::mk_epsilon(sm);
-    }
-    else if (u.str.is_string(e, s)) {        
-        unsigned init = 0;
-        eautomaton::moves mvs;        
-        unsigned_vector final;
-        final.push_back(s.length());
-        for (unsigned k = 0; k < s.length(); ++k) {
-            // reference count?
-            mvs.push_back(eautomaton::move(sm, k, k+1, sym_expr::mk_char(m, u.str.mk_char(s, k))));
-        }
-        return alloc(eautomaton, sm, init, final, mvs);
-    }
-    return nullptr;
-}
 
 void seq_rewriter::updt_params(params_ref const & p) {
     seq_rewriter_params sp(p);
@@ -2721,46 +2405,6 @@ void seq_rewriter::add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned
 
 }
 
-bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
-    seq.reset();
-    unsigned state = aut.init();
-    uint_set visited;
-    eautomaton::moves mvs;
-    unsigned_vector states;
-    aut.get_epsilon_closure(state, states);
-    bool has_final = false;
-    for (unsigned i = 0; !has_final && i < states.size(); ++i) {
-        has_final = aut.is_final_state(states[i]);
-    }
-    aut.get_moves_from(state, mvs, true);       
-    while (!has_final) {
-        if (mvs.size() != 1) {
-            return false;
-        }
-        if (visited.contains(state)) {
-            return false;
-        }
-        if (aut.is_final_state(mvs[0].src())) {
-            return false;
-        }
-        visited.insert(state);
-        sym_expr* t = mvs[0].t();
-        if (!t || !t->is_char()) {
-            return false;
-        }
-        seq.push_back(str().mk_unit(t->get_char()));
-        state = mvs[0].dst();
-        mvs.reset();
-        aut.get_moves_from(state, mvs, true);
-        states.reset();
-        has_final = false;
-        aut.get_epsilon_closure(state, states);
-        for (unsigned i = 0; !has_final && i < states.size(); ++i) {
-            has_final = aut.is_final_state(states[i]);
-        }
-    }
-    return mvs.empty();
-}
 
 bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
     seq.reset();

src/ast/rewriter/seq_rewriter.h

@@ -26,8 +26,6 @@ Notes:
 #include "util/params.h"
 #include "util/lbool.h"
 #include "util/sign.h"
-#include "math/automata/automaton.h"
-#include "math/automata/symbolic_automata.h"
 
 
 inline std::ostream& operator<<(std::ostream& out, expr_ref_pair_vector const& es) {
@@ -81,33 +79,15 @@ public:
     void dec_ref(sym_expr* s) { if (s) s->dec_ref(); }
 };
 
+#if 0
+
 class expr_solver {
 public:
     virtual ~expr_solver() = default;
     virtual lbool check_sat(expr* e) = 0;
 };
+#endif
 
-typedef automaton<sym_expr, sym_expr_manager> eautomaton;
-class re2automaton {
-    typedef boolean_algebra<sym_expr*> boolean_algebra_t;
-    typedef symbolic_automata<sym_expr, sym_expr_manager> symbolic_automata_t;
-    ast_manager& m;
-    sym_expr_manager sm;
-    seq_util     u;     
-    scoped_ptr<expr_solver>         m_solver;
-    scoped_ptr<boolean_algebra_t>   m_ba;
-    scoped_ptr<symbolic_automata_t> m_sa;
-
-    bool is_unit_char(expr* e, expr_ref& ch);
-    eautomaton* re2aut(expr* e);
-    eautomaton* seq2aut(expr* e);
-public:
-    re2automaton(ast_manager& m);
-    eautomaton* operator()(expr* e);
-    void set_solver(expr_solver* solver);
-    bool has_solver() const { return m_solver; }
-    eautomaton* mk_product(eautomaton *a1, eautomaton *a2);
-};
 
 /**
    \brief Cheap rewrite rules for seq constraints
@@ -150,7 +130,7 @@ class seq_rewriter {
     seq_util       m_util;
     arith_util     m_autil;
     bool_rewriter  m_br;
-    re2automaton   m_re2aut;
+    // re2automaton   m_re2aut;
     op_cache       m_op_cache;
     expr_ref_vector m_es, m_lhs, m_rhs;
     bool           m_coalesce_chars;    
@@ -340,7 +320,7 @@ class seq_rewriter {
 
     void add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned idx, expr* cond);
     bool is_sequence(expr* e, expr_ref_vector& seq);
-    bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
+//    bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
     bool get_lengths(expr* e, expr_ref_vector& lens, rational& pos);
     bool reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
     bool reduce_back(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
@@ -360,7 +340,8 @@ class seq_rewriter {
 
 public:
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
-        m_util(m), m_autil(m), m_br(m, p), m_re2aut(m), m_op_cache(m), m_es(m), 
+        m_util(m), m_autil(m), m_br(m, p), // m_re2aut(m), 
+        m_op_cache(m), m_es(m), 
         m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
     }
     ast_manager & m() const { return m_util.get_manager(); }
@@ -371,8 +352,6 @@ public:
     void updt_params(params_ref const & p);
     static void get_param_descrs(param_descrs & r);
 
-    void set_solver(expr_solver* solver) { m_re2aut.set_solver(solver); }
-    bool has_solver() { return m_re2aut.has_solver(); }
 
     bool coalesce_chars() const { return m_coalesce_chars; }
 

src/ast/rewriter/th_rewriter.cpp

@@ -933,9 +933,6 @@ struct th_rewriter::imp : public rewriter_tpl<th_rewriter_cfg> {
         return m_cfg.mk_eq(a, b);
     }
 
-    void set_solver(expr_solver* solver) {
-        m_cfg.m_seq_rw.set_solver(solver);
-    }
 };
 
 th_rewriter::th_rewriter(ast_manager & m, params_ref const & p):
@@ -1057,10 +1054,6 @@ expr_ref th_rewriter::mk_eq(expr* a, expr* b) {
     return m_imp->mk_eq(a, b);
 }
 
-void th_rewriter::set_solver(expr_solver* solver) {
-    m_imp->set_solver(solver);
-}
-
 
 bool th_rewriter::reduce_quantifier(quantifier * old_q, 
                                     expr * new_body, 

src/ast/rewriter/th_rewriter.h

@@ -74,7 +74,6 @@ public:
     expr_dependency * get_used_dependencies();
     void reset_used_dependencies();
 
-    void set_solver(expr_solver* solver);
 
 };
 

src/ast/simplifiers/euf_completion.cpp

@@ -253,10 +253,14 @@ namespace euf {
         auto n = m_egraph.find(t);
         if (!n)
             return;
-        ptr_vector<expr> args;
+        expr_ref_vector args(m);
+        expr_mark visited;
         for (auto s : enode_class(n)) {
             expr_ref r(s->get_expr(), m);
             m_rewriter(r);
+            if (visited.is_marked(r))
+                continue;
+            visited.mark(r);
             args.push_back(r);
         }
         expr_ref cong(m);
@@ -288,6 +292,8 @@ namespace euf {
             propagate_rules();
             propagate_closures();
             IF_VERBOSE(11, verbose_stream() << "propagate " << m_stats.m_num_instances << "\n");
+            if (!should_stop())
+                propagate_arithmetic();
             if (!m_should_propagate && !should_stop())
                 propagate_all_rules();            
         }
@@ -310,16 +316,14 @@ namespace euf {
             for (auto* ch : enode_args(n))
                 m_nodes_to_canonize.push_back(ch);
             };
-        expr* x = nullptr, * y = nullptr;
+        expr* x = nullptr, * y = nullptr, * nf = nullptr;
         if (m.is_eq(f, x, y)) {
-            expr_ref x1(x, m);
             expr_ref y1(y, m);
-            m_rewriter(x1);
             m_rewriter(y1);
 
-            add_quantifiers(x1);
+            add_quantifiers(x);
             add_quantifiers(y1);
-            enode* a = mk_enode(x1);
+            enode* a = mk_enode(x);
             enode* b = mk_enode(y1);
 
             if (a->get_root() == b->get_root())
@@ -332,41 +336,27 @@ namespace euf {
             m_egraph.propagate();
             m_should_propagate = true; 
             
-#if 0
-            auto a1 = mk_enode(x);
-            auto b1 = mk_enode(y);
-
-            if (a->get_root() != a1->get_root()) {
-                add_children(a1);;
-                m_egraph.merge(a, a1, nullptr);
-                m_egraph.propagate();
-            }
-
-            if (b->get_root() != b1->get_root()) {
-                add_children(b1);
-                m_egraph.merge(b, b1, nullptr);
-                m_egraph.propagate();
-            }
-#endif
-            
             if (m_side_condition_solver && a->get_root() != b->get_root())
                 m_side_condition_solver->add_constraint(f, pr, d);
             IF_VERBOSE(1, verbose_stream() << "eq: " << a->get_root_id() << " " << b->get_root_id() << " " 
-                 << x1 << " == " << y1 << "\n");
+                 << mk_pp(x, m) << " == " << y1 << "\n");
         }
-        else if (m.is_not(f, f)) {
+        else if (m.is_not(f, nf)) {
-            enode* n = mk_enode(f);
+            expr_ref f1(nf, m);
+            m_rewriter(f1);
+            enode* n = mk_enode(f1);
             if (m.is_false(n->get_root()->get_expr()))
                 return;
-            add_quantifiers(f);
+            add_quantifiers(f1);
+            auto n_false = mk_enode(m.mk_false());
             auto j = to_ptr(push_pr_dep(pr, d));
-            m_egraph.new_diseq(n, j);
+            m_egraph.merge(n, n_false, j);
             m_egraph.propagate();
             add_children(n);
             m_should_propagate = true;
             if (m_side_condition_solver)
                 m_side_condition_solver->add_constraint(f, pr, d);
-            IF_VERBOSE(1, verbose_stream() << "not: " << mk_pp(f, m) << "\n");
+            IF_VERBOSE(1, verbose_stream() << "not: " << nf << "\n");
         }
         else {
             enode* n = mk_enode(f);
@@ -631,6 +621,88 @@ namespace euf {
         }
     }
 
+    //
+    // extract shared arithmetic terms T
+    // extract shared variables V
+    // add t = rewriter(t) to E-graph
+    // solve for V by solver producing theta
+    // add theta to E-graph
+    // add theta to canonize (?)
+    //
+    void completion::propagate_arithmetic() {
+        ptr_vector<expr> shared_terms, shared_vars;
+        expr_mark visited;
+        arith_util a(m);
+        bool merged = false;
+        for (auto n : m_egraph.nodes()) {
+            expr* e = n->get_expr();
+            if (!is_app(e))
+                continue;
+            app* t = to_app(e);
+            bool is_arith = a.is_arith_expr(t);
+            for (auto arg : *t) {
+                bool is_arith_arg = a.is_arith_expr(arg);
+                if (is_arith_arg == is_arith)
+                    continue;
+                if (visited.is_marked(arg))
+                    continue;
+                visited.mark(arg);
+                if (is_arith_arg)
+                    shared_terms.push_back(arg);
+                else
+                    shared_vars.push_back(arg);
+            }           
+        }
+        for (auto t : shared_terms) {
+            auto tn = m_egraph.find(t);
+            
+            if (!tn)
+                continue;
+            expr_ref r(t, m);
+            m_rewriter(r);
+            if (r == t)
+                continue;
+            auto n = m_egraph.find(t);
+            auto t_root = tn->get_root();
+            if (n && n->get_root() == t_root) 
+                continue;
+            
+            if (!n)
+                n = mk_enode(r);
+            TRACE(euf_completion, tout << "propagate-arith: " << mk_pp(t, m) << " -> " << r << "\n");
+            
+            m_egraph.merge(tn, n, nullptr);
+            merged = true;
+        }
+        visited.reset();
+        for (auto v : shared_vars) {
+            if (visited.is_marked(v))
+                continue;
+            visited.mark(v);
+            vector<side_condition_solver::solution> sol;
+            expr_ref term(m), guard(m);
+            sol.push_back({ v, term, guard });
+            m_side_condition_solver->solve_for(sol);
+            for (auto [v, t, g] : sol) {
+                if (!t)
+                    continue;
+                visited.mark(v);
+                auto a = mk_enode(v);
+                auto b = mk_enode(t);
+                if (a->get_root() == b->get_root())
+                    continue;
+                TRACE(euf_completion, tout << "propagate-arith: " << m_egraph.bpp(a) << " -> " << m_egraph.bpp(b) << "\n");
+                IF_VERBOSE(1, verbose_stream() << "propagate-arith: " << m_egraph.bpp(a) << " -> " << m_egraph.bpp(b) << "\n");
+                m_egraph.merge(a, b, nullptr); // TODO guard justifies reason.
+                merged = true;
+            }
+        }
+        if (merged) {
+            m_egraph.propagate();
+            m_should_propagate = true;
+        }
+    }
+
     void completion::propagate_closures() {
         for (auto [q, clos] : m_closures) {
             expr* body = clos.second;

src/ast/simplifiers/euf_completion.h

@@ -187,6 +187,7 @@ namespace euf {
         expr_ref get_canonical(quantifier* q, proof_ref& pr, expr_dependency_ref& d);
         obj_map<quantifier, std::pair<ptr_vector<expr>, expr*>> m_closures;
 
+        void propagate_arithmetic();
         expr_dependency* explain_eq(enode* a, enode* b);
         proof_ref prove_eq(enode* a, enode* b);
         proof_ref prove_conflict();

src/cmd_context/cmd_context.h

@@ -575,22 +575,3 @@ public:
 std::ostream & operator<<(std::ostream & out, cmd_context::status st);
 
 
-class th_solver : public expr_solver {
-    cmd_context& m_ctx;
-    params_ref   m_params;
-    ref<solver> m_solver;
-public:
-    th_solver(cmd_context& ctx): m_ctx(ctx) {}
-    
-    lbool check_sat(expr* e) override {
-        if (!m_solver) {
-            m_solver = m_ctx.get_solver_factory()(m_ctx.m(), m_params, false, true, false, symbol::null);
-        }
-        m_solver->push();
-        m_solver->assert_expr(e);
-        lbool r = m_solver->check_sat(0,nullptr);
-        m_solver->pop(1);
-        return r;
-    }
-};
-

src/cmd_context/eval_cmd.cpp

@@ -75,7 +75,6 @@ public:
         unsigned rlimit  = m_params.get_uint("rlimit", 0);
         // md->compress();
         model_evaluator ev(*(md.get()), m_params);
-        ev.set_solver(alloc(th_solver, ctx));
         cancel_eh<reslimit> eh(ctx.m().limit());
         { 
             scoped_ctrl_c ctrlc(eh);

src/cmd_context/simplify_cmd.cpp

@@ -69,8 +69,6 @@ public:
         if (m_params.get_bool("som", false))
             m_params.set_bool("flat", true);
         th_rewriter s(ctx.m(), m_params);
-        th_solver solver(ctx);
-        s.set_solver(alloc(th_solver, ctx));
         unsigned cache_sz;
         unsigned num_steps = 0;
         unsigned timeout   = m_params.get_uint("timeout", UINT_MAX);

src/math/automata/CMakeLists.txt

@@ -1,6 +0,0 @@
-z3_add_component(automata
-  SOURCES
-    automaton.cpp
-  COMPONENT_DEPENDENCIES
-    util
-)

src/math/automata/automaton.cpp

@@ -1,23 +0,0 @@
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
-Module Name:
-
-    automaton.cpp
-
-Abstract:
-
-    Symbolic Automaton, a la Margus Veanes Automata library.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2015-12-23.
-
-Revision History:
-
-
---*/
-
-#include "math/automata/automaton.h"
-
-template class automaton<unsigned>;

src/math/automata/automaton.h

@@ -1,751 +0,0 @@
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
-Module Name:
-
-    automaton.h
-
-Abstract:
-
-    Symbolic Automaton, a la Margus Veanes Automata library.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2015-12-23.
-
-Revision History:
-
-
---*/
-
-#pragma once
-
-
-#include "util/util.h"
-#include "util/vector.h"
-#include "util/uint_set.h"
-#include "util/trace.h"
-
-template<class T>
-class default_value_manager {
-public:
-    void inc_ref(T* t) {}
-    void dec_ref(T* t) {}
-};
-
-template<class T, class M = default_value_manager<T> >
-class automaton {
-public:
-    class move {
-        M&       m;
-        T*       m_t;
-        unsigned m_src;
-        unsigned m_dst;        
-    public:
-        move(M& m, unsigned s, unsigned d, T* t = nullptr): m(m), m_t(t), m_src(s), m_dst(d) {
-            if (t) m.inc_ref(t);
-        }
-        ~move() {
-            if (m_t) m.dec_ref(m_t);
-        }
-
-        move(move const& other): m(other.m), m_t(other.m_t), m_src(other.m_src), m_dst(other.m_dst) {
-            if (m_t) m.inc_ref(m_t);
-        }
-
-        move(move &&other) noexcept : m(other.m), m_t(nullptr), m_src(other.m_src), m_dst(other.m_dst) {
-            std::swap(m_t, other.m_t);
-        }
-
-        move& operator=(move const& other) {
-            SASSERT(&m == &other.m);
-            T* t = other.m_t;
-            if (t) m.inc_ref(t);
-            if (m_t) m.dec_ref(m_t);
-            m_t = t;
-            m_src = other.m_src;
-            m_dst = other.m_dst;
-            return *this;
-        }
-
-        unsigned dst() const { return m_dst; }
-        unsigned src() const { return m_src; }
-        T* t() const { return m_t; }
-
-        bool is_epsilon() const { return m_t == nullptr; }
-    };
-    typedef vector<move> moves;
-private:
-    M&              m;
-    vector<moves>   m_delta;
-    vector<moves>   m_delta_inv;
-    unsigned        m_init;
-    uint_set        m_final_set;
-    unsigned_vector m_final_states;
-    
-
-    // local data-structures
-    mutable uint_set        m_visited;
-    mutable unsigned_vector m_todo;
-
-    struct default_display {
-        std::ostream& display(std::ostream& out, T* t) {
-            return out << t;
-        }
-    };
-
-public:
-
-    // The empty automaton:
-    automaton(M& m):
-        m(m), 
-        m_init(0)
-    {
-        m_delta.push_back(moves());
-        m_delta_inv.push_back(moves());
-    }
-
-
-    // create an automaton from initial state, final states, and moves
-    automaton(M& m, unsigned init, unsigned_vector const& final, moves const& mvs): m(m) {
-        m_init = init;
-        m_delta.push_back(moves());
-        m_delta_inv.push_back(moves());
-        for (unsigned f : final) {
-            add_to_final_states(f);
-        }
-        for (move const& mv : mvs) {
-            unsigned n = std::max(mv.src(), mv.dst());
-            if (n >= m_delta.size()) {
-                m_delta.resize(n+1, moves());
-                m_delta_inv.resize(n+1, moves());
-            }
-            add(mv);
-        }
-    }
-
-    // create an automaton that accepts a sequence.
-    automaton(M& m, ptr_vector<T> const& seq):
-        m(m),
-        m_init(0) {
-        m_delta.resize(seq.size()+1, moves());
-        m_delta_inv.resize(seq.size()+1, moves());
-        for (unsigned i = 0; i < seq.size(); ++i) {
-            m_delta[i].push_back(move(m, i, i + 1, seq[i]));
-            m_delta[i + 1].push_back(move(m, i, i + 1, seq[i]));
-        }
-        add_to_final_states(seq.size());
-    }
-
-    // The automaton that accepts t
-    automaton(M& m, T* t):
-        m(m), 
-        m_init(0) {
-        m_delta.resize(2, moves());
-        m_delta_inv.resize(2, moves());
-        add_to_final_states(1);
-        add(move(m, 0, 1, t));
-    }    
-
-    automaton(automaton const& other):
-        m(other.m), 
-        m_delta(other.m_delta),
-        m_delta_inv(other.m_delta_inv),        
-        m_init(other.m_init),
-        m_final_set(other.m_final_set),
-        m_final_states(other.m_final_states)
-    {}
-
-    // create the automaton that accepts the empty string/sequence only.
-    static automaton* mk_epsilon(M& m) {
-        moves mvs;
-        unsigned_vector final;
-        final.push_back(0);        
-        return alloc(automaton, m, 0, final, mvs);
-    }
-
-    // create the automaton with a single state on condition t.
-    static automaton* mk_loop(M& m, T* t) {
-        moves mvs;
-        unsigned_vector final;
-        final.push_back(0);       
-        mvs.push_back(move(m, 0, 0, t));
-        return alloc(automaton, m, 0, final, mvs);
-    }
-
-    static automaton* clone(automaton const& a) {
-        moves mvs;
-        unsigned_vector final;
-        append_moves(0, a, mvs);
-        append_final(0, a, final);
-        return alloc(automaton, a.m, a.init(), final, mvs);
-    }
-
-    automaton* clone() const {
-        return clone(*this);
-    }
-
-    // create the sum of disjoint automata
-    static automaton* mk_union(automaton const& a, automaton const& b) {
-        SASSERT(&a.m == &b.m);
-        M& m = a.m;
-        if (a.is_empty()) {
-            return b.clone();
-        }
-        if (b.is_empty()) {
-            return a.clone();
-        }
-        moves mvs;
-        unsigned_vector final;
-        unsigned offset1 = 1;
-        unsigned offset2 = a.num_states() + 1;
-        mvs.push_back(move(m, 0, a.init() + offset1));
-        mvs.push_back(move(m, 0, b.init() + offset2));
-        append_moves(offset1, a, mvs);
-        append_moves(offset2, b, mvs);
-        append_final(offset1, a, final);
-        append_final(offset2, b, final);
-        return alloc(automaton, m, 0, final, mvs);
-    }
-
-    static automaton* mk_opt(automaton const& a) {       
-        M& m = a.m;
-        moves mvs;
-        unsigned_vector final;
-        unsigned offset = 0;
-        unsigned init = a.init();
-        if (!a.initial_state_is_source()) {
-            offset = 1;
-            init = 0;
-            mvs.push_back(move(m, 0, a.init() + offset));
-        }
-        if (a.is_empty()) {
-            return a.clone();
-        }
-
-        mvs.push_back(move(m, init, a.final_state() + offset));
-        append_moves(offset, a, mvs);
-        append_final(offset, a, final);
-        return alloc(automaton, m, init, final, mvs);        
-    }
-
-    // concatenate accepting languages
-    static automaton* mk_concat(automaton const& a, automaton const& b) {
-        SASSERT(&a.m == &b.m);
-        M& m = a.m;
-        if (a.is_empty()) {
-            return a.clone();
-        }
-        if (b.is_empty()) {
-            return b.clone();
-        }
-        if (a.is_epsilon()) {
-            return b.clone();
-        }
-        if (b.is_epsilon()) {
-            return a.clone();
-        }
-
-        moves mvs;
-        unsigned_vector final;
-        unsigned init = 0;
-        unsigned offset1 = 1;
-        unsigned offset2 = a.num_states() + offset1;
-        mvs.push_back(move(m, 0, a.init() + offset1));
-        append_moves(offset1, a, mvs);
-        for (unsigned i = 0; i < a.m_final_states.size(); ++i) {
-            mvs.push_back(move(m, a.m_final_states[i] + offset1, b.init() + offset2));
-        }
-        append_moves(offset2, b, mvs);
-        append_final(offset2, b, final);
-        
-        return alloc(automaton, m, init, final, mvs);
-    }
-
-    static automaton* mk_reverse(automaton const& a) {
-        M& m = a.m;
-        if (a.is_empty()) {
-            return alloc(automaton, m);
-        }
-        moves mvs;
-        for (unsigned i = 0; i < a.m_delta.size(); ++i) {
-            moves const& mvs1 = a.m_delta[i];
-            for (unsigned j = 0; j < mvs1.size(); ++j) {
-                move const& mv = mvs1[j];
-                mvs.push_back(move(m, mv.dst(), mv.src(), mv.t()));
-            }
-        }
-        unsigned_vector final;
-        unsigned init;
-        final.push_back(a.init());
-        if (a.m_final_states.size() == 1) {
-            init = a.m_final_states[0];
-        }
-        else {
-            init = a.num_states();
-            for (unsigned st : a.m_final_states) {
-                mvs.push_back(move(m, init, st));
-            }
-        }
-        return alloc(automaton, m, init, final, mvs);        
-    }
-
-    void add_to_final_states(unsigned s) {
-        if (!is_final_state(s)) {
-            m_final_set.insert(s);
-            m_final_states.push_back(s);
-        }
-    }
-
-    void remove_from_final_states(unsigned s) {
-        if (is_final_state(s)) {
-            m_final_set.remove(s);
-            m_final_states.erase(s);
-        }
-    }
-
-    bool is_sink_state(unsigned s) const {
-        if (is_final_state(s)) return false;
-        moves mvs;
-        get_moves_from(s, mvs);
-        for (move const& m : mvs) {
-            if (s != m.dst()) return false;
-        }
-        return true;
-    }
-
-    void add_init_to_final_states() {
-        add_to_final_states(init());
-    }
-
-    void add_final_to_init_moves() {
-        for (unsigned i = 0; i < m_final_states.size(); ++i) {
-            unsigned state = m_final_states[i];
-            bool found = false;
-            moves const& mvs = m_delta[state];
-            for (unsigned j = 0; found && j < mvs.size(); ++j) {
-                found = (mvs[j].dst() == m_init) && mvs[j].is_epsilon();
-            }
-            if (!found && state != m_init) {
-                add(move(m, state, m_init));
-            }
-        }
-    }
-
-    // remove epsilon transitions
-    // src - e -> dst
-    // in_degree(src) = 1, final(src) => final(dst), src0 != src
-    //    src0 - t -> src - e -> dst => src0 - t -> dst
-    // out_degree(dst) = 1, final(dst) => final(src), dst != dst1
-    //    src - e -> dst - t -> dst1 => src - t -> dst1
-
-    // Generalized: 
-    // Src - E -> dst - t -> dst1 => Src - t -> dst1   if dst is final => each Src is final
-    //
-    // src - e -> dst - ET -> Dst1 => src - ET -> Dst1  if in_degree(dst) = 1, src != dst
-    // Src - E -> dst - et -> dst1 => Src - et -> dst1  if out_degree(dst) = 1, src != dst
-    // 
-    // Some missing: 
-    //  src - et -> dst - E -> Dst1 => src - et -> Dst1   if in_degree(dst) = 1
-    //  Src - ET -> dst - e -> dst1 => Src - ET -> dst1  if out_degree(dst) = 1, 
-    //
-    void compress() {
-        SASSERT(!m_delta.empty());
-        TRACE(seq, display(tout););
-        for (unsigned i = 0; i < m_delta.size(); ++i) {
-            for (unsigned j = 0; j < m_delta[i].size(); ++j) {
-                move const& mv = m_delta[i][j];
-                unsigned src = mv.src();
-                unsigned dst = mv.dst();
-                SASSERT(src == i);
-                if (mv.is_epsilon()) {
-                    if (src == dst) {
-                        // just remove this edge.                        
-                    }
-                    else if (1 == in_degree(src) && 1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
-                        move const& mv0 = m_delta_inv[src][0];
-                        unsigned src0 = mv0.src();                        
-                        T* t = mv0.t();
-                        SASSERT(mv0.dst() == src);
-                        if (src0 == src) {
-                            continue;
-                        }
-                        add(move(m, src0, dst, t));
-                        remove(src0, src, t);
-
-                    }
-                    else if (1 == out_degree(dst) && 1 == in_degree(dst) && init() != dst && (!is_final_state(dst) || is_final_state(src))) {
-                        move const& mv1 = m_delta[dst][0];
-                        unsigned dst1 = mv1.dst();
-                        T* t = mv1.t();
-                        SASSERT(mv1.src() == dst);
-                        if (dst1 == dst) {
-                            continue;
-                        }
-                        add(move(m, src, dst1, t));
-                        remove(dst, dst1, t);
-                    }
-                    else if (1 == in_degree(dst) && (!is_final_state(dst) || is_final_state(src)) && init() != dst) {
-                        moves const& mvs = m_delta[dst];
-                        moves mvs1;
-                        for (move const& mv : mvs) {
-                            mvs1.push_back(move(m, src, mv.dst(), mv.t()));
-                        }
-                        for (move const& mv : mvs1) {
-                            remove(dst, mv.dst(), mv.t());
-                            add(mv);
-                        }
-                    }
-                    //
-                    // Src - E -> dst - et -> dst1 => Src - et -> dst1  if out_degree(dst) = 1, src != dst
-                    //
-                    else if (1 == out_degree(dst) && all_epsilon_in(dst) && init() != dst && !is_final_state(dst)) {
-                        move const& mv = m_delta[dst][0];
-                        unsigned dst1 = mv.dst();
-                        T* t = mv.t();
-                        unsigned_vector src0s;
-                        moves const& mvs = m_delta_inv[dst];
-                        moves mvs1;
-                        for (move const& mv1 : mvs) {
-                            SASSERT(mv1.is_epsilon());
-                            mvs1.push_back(move(m, mv1.src(), dst1, t));
-                        }
-                        for (move const& mv1 : mvs1) {
-                            remove(mv1.src(), dst, nullptr);
-                            add(mv1);
-                        }
-                        remove(dst, dst1, t);    
-                        --j;
-                        continue;
-                    }
-                    //
-                    // Src1 - ET -> src - e -> dst => Src1 - ET -> dst  if out_degree(src) = 1, src != init() 
-                    //
-                    else if (1 == out_degree(src) && init() != src && (!is_final_state(src) || is_final_state(dst))) {
-                        moves const& mvs = m_delta_inv[src];
-                        moves mvs1;
-                        for (move const& mv : mvs) {
-                            mvs1.push_back(move(m, mv.src(), dst, mv.t()));
-                        }
-                        for (move const& mv : mvs1) {
-                            remove(mv.src(), src, mv.t());
-                            add(mv);
-                        }
-                    }
-                    else if (1 == out_degree(src) && (is_final_state(src) || !is_final_state(dst))) {
-                        moves const& mvs = m_delta[dst];
-                        moves mvs1;
-                        for (move const& mv : mvs) {
-                            mvs1.push_back(move(m, src, mv.dst(), mv.t()));
-                        }
-                        for (move const& mv : mvs1) {
-                            add(mv);
-                        }
-                    }
-                    else {
-                        TRACE(seq, tout << "epsilon not removed " << out_degree(src) << " " << is_final_state(src) << " " << is_final_state(dst) << "\n";);
-                        continue;
-                    }                    
-                    remove(src, dst, nullptr);
-                    --j;
-                }
-            }
-        }
-        SASSERT(!m_delta.empty());
-        while (true) {
-            SASSERT(!m_delta.empty());
-            unsigned src = m_delta.size() - 1;            
-            if (in_degree(src) == 0 && init() != src) {
-                remove_from_final_states(src);
-                m_delta.pop_back();
-            }
-            else {
-                break;
-            }
-        }
-        sinkify_dead_states();
-        TRACE(seq, display(tout););
-    }
-
-    bool is_sequence(unsigned& length) const {
-        if (is_final_state(m_init) && (out_degree(m_init) == 0 || (out_degree(m_init) == 1 && is_loop_state(m_init)))) {
-            length = 0;
-            return true;
-        }
-        if (is_empty() || in_degree(m_init) != 0 || out_degree(m_init) != 1) {
-            return false;
-        }
-        
-        length = 1;
-        unsigned s = get_move_from(m_init).dst();
-        while (!is_final_state(s)) {  
-            if (out_degree(s) != 1 || in_degree(s) != 1) {
-                return false;
-            }
-            s = get_move_from(s).dst();
-            ++length;
-        }
-        return out_degree(s) == 0 || (out_degree(s) == 1 && is_loop_state(s));
-    }
-
-    unsigned init() const { return m_init; }
-    unsigned_vector const& final_states() const { return m_final_states; }
-    unsigned in_degree(unsigned state) const { return m_delta_inv[state].size(); }
-    unsigned out_degree(unsigned state) const { return m_delta[state].size(); }
-    move const& get_move_from(unsigned state) const { SASSERT(m_delta[state].size() == 1); return m_delta[state][0]; }
-    move const& get_move_to(unsigned state) const { SASSERT(m_delta_inv[state].size() == 1); return m_delta_inv[state][0]; }
-    moves const& get_moves_from(unsigned state) const { return m_delta[state]; }
-    moves const& get_moves_to(unsigned state) const { return m_delta_inv[state]; }
-    bool initial_state_is_source() const { return m_delta_inv[m_init].empty(); }
-    bool is_final_state(unsigned s) const { return m_final_set.contains(s); }
-    bool is_final_configuration(uint_set const& s) const {
-        for (unsigned i : s) {
-            if (is_final_state(i))
-                return true;
-        }
-        return false; 
-    }
-    bool is_epsilon_free() const {
-        for (moves const& mvs : m_delta) {
-            for (move const & m : mvs) {
-                if (!m.t()) return false;
-            }
-        }
-        return true;
-    }
-
-    bool all_epsilon_in(unsigned s) {
-        moves const& mvs = m_delta_inv[s];
-        for (move const& m : mvs) {
-            if (m.t()) return false;
-        }
-        return true;
-    }
-
-    bool is_empty() const { return m_final_states.empty(); }
-    bool is_epsilon() const { return m_final_states.size() == 1 && m_final_states.back() == init() && m_delta.empty(); }
-    unsigned final_state() const { return m_final_states[0]; }
-    bool has_single_final_sink() const { return m_final_states.size() == 1 && m_delta[final_state()].empty(); }
-    unsigned num_states() const { return m_delta.size(); }
-    bool is_loop_state(unsigned s) const {
-        moves mvs;
-        get_moves_from(s, mvs);
-        for (move const& m : mvs) {
-            if (s == m.dst()) return true;
-        }
-        return false;
-    }
-
-    unsigned move_count() const {
-        unsigned result = 0;
-        for (moves const& mvs : m_delta) result += mvs.size();
-        return result;
-    }
-    void get_epsilon_closure(unsigned state, unsigned_vector& states) {
-        get_epsilon_closure(state, m_delta, states);
-    }
-    void get_inv_epsilon_closure(unsigned state, unsigned_vector& states) {
-        get_epsilon_closure(state, m_delta_inv, states);
-    }
-    void get_moves_from(unsigned state, moves& mvs, bool epsilon_closure = true) const {
-        get_moves(state, m_delta, mvs, epsilon_closure);
-    }
-    void get_moves_from_states(uint_set const& states, moves& mvs, bool epsilon_closure = true) const {
-        for (unsigned i : states) {
-            moves curr;
-            get_moves(i, m_delta, curr, epsilon_closure);
-            mvs.append(curr);
-        }
-    }
-    void get_moves_to(unsigned state, moves& mvs, bool epsilon_closure = true) {
-        get_moves(state, m_delta_inv, mvs, epsilon_closure);
-    }
-
-    template<class D>
-    std::ostream& display(std::ostream& out, D& displayer = D()) const {
-        out << "init: " << init() << "\n";
-        out << "final: " << m_final_states << "\n";
-
-        for (unsigned i = 0; i < m_delta.size(); ++i) {
-            moves const& mvs = m_delta[i];
-            for (move const& mv : mvs) {
-                out << i << " -> " << mv.dst() << " ";
-                if (mv.t()) {
-                    out << "if "; 
-                    displayer.display(out, mv.t());
-                }
-                out << "\n";
-            }
-        }
-        return out;
-    }
-private:
-
-    std::ostream& display(std::ostream& out) const {
-        out << "init: " << init() << "\n";
-        out << "final: " << m_final_states << "\n";
-
-        for (unsigned i = 0; i < m_delta.size(); ++i) {
-            moves const& mvs = m_delta[i];
-            for (move const& mv : mvs) {
-                out << i << " -> " << mv.dst() << " ";
-                if (mv.t()) {
-                    out << "if *** "; 
-                }
-                out << "\n";
-            }
-        }
-        return out;
-    }
-    void sinkify_dead_states() {
-        uint_set dead_states;
-        for (unsigned i = 0; i < m_delta.size(); ++i) {
-            if (!m_final_states.contains(i)) {
-                dead_states.insert(i);
-            }
-        }
-        bool change = true;
-        unsigned_vector to_remove;
-        while (change) {
-            change = false;
-            to_remove.reset();
-            for (unsigned s : dead_states) {
-                moves const& mvs = m_delta[s];
-                for (move const& mv : mvs) {
-                    if (!dead_states.contains(mv.dst())) {
-                        to_remove.push_back(s);
-                        break;
-                    }
-                }
-            }
-            change = !to_remove.empty();
-            for (unsigned s : to_remove) {
-                dead_states.remove(s);
-            }
-            to_remove.reset();
-        }
-        TRACE(seq, tout << "remove: " << dead_states << "\n"; 
-              tout << "final: " << m_final_states << "\n";
-              );
-        for (unsigned s : dead_states) {
-            CTRACE(seq, !m_delta[s].empty(), tout << "live state " << s << "\n";); 
-            m_delta[s].reset();
-        }
-    }
-
-#if 0
-    void remove_dead_states() {
-        unsigned_vector remap;
-        for (unsigned i = 0; i < m_delta.size(); ++i) {
-            
-        }
-    }    
-#endif
-
-    void add(move const& mv) {
-        if (!is_duplicate_cheap(mv)) {
-            m_delta[mv.src()].push_back(mv);
-            m_delta_inv[mv.dst()].push_back(mv);
-        }
-    }
-
-    bool is_duplicate_cheap(move const& mv) const {
-        if (m_delta[mv.src()].empty()) return false;
-        move const& mv0 = m_delta[mv.src()].back();
-        return mv0.src() == mv.src() && mv0.dst() == mv.dst() && mv0.t() == mv.t();
-    }
-
-
-    unsigned find_move(unsigned src, unsigned dst, T* t, moves const& mvs) {
-        for (unsigned i = 0; i < mvs.size(); ++i) {
-            move const& mv = mvs[i];
-            if (mv.src() == src && mv.dst() == dst && t == mv.t()) {
-                return i;
-            }
-        }
-        UNREACHABLE();
-        return UINT_MAX;
-    }
-
-    void remove(unsigned src, unsigned dst, T* t, moves& mvs) {
-        remove(find_move(src, dst, t, mvs), mvs);
-    }
-
-    void remove(unsigned src, unsigned dst, T* t) {
-        remove(src, dst, t, m_delta[src]);
-        remove(src, dst, t, m_delta_inv[dst]);
-    }
-
-    void remove(unsigned index, moves& mvs) {
-        mvs[index] = mvs.back();
-        mvs.pop_back();
-    }     
-
-    mutable unsigned_vector m_states1, m_states2;
-    
-    void get_moves(unsigned state, vector<moves> const& delta, moves& mvs, bool epsilon_closure) const {
-        m_states1.reset(); 
-        m_states2.reset();
-        get_epsilon_closure(state, delta, m_states1);
-        for (unsigned i = 0; i < m_states1.size(); ++i) {
-            state = m_states1[i];
-            moves const& mv1 = delta[state];
-            for (unsigned j = 0; j < mv1.size(); ++j) {
-                move const& mv = mv1[j];
-                if (!mv.is_epsilon()) {
-                    if (epsilon_closure) {
-                        m_states2.reset();
-                        get_epsilon_closure(mv.dst(), delta, m_states2);
-                        for (unsigned k = 0; k < m_states2.size(); ++k) {
-                            mvs.push_back(move(m, state, m_states2[k], mv.t()));                            
-                        }
-                    }
-                    else {
-                        mvs.push_back(move(m, state, mv.dst(), mv.t()));
-                    }
-                }
-            }
-        }
-    }
-
-    void get_epsilon_closure(unsigned state, vector<moves> const& delta, unsigned_vector& states) const {
-        m_todo.push_back(state);
-        m_visited.insert(state);
-        while (!m_todo.empty()) {
-            state = m_todo.back();
-            states.push_back(state);
-            m_todo.pop_back();
-            moves const& mvs = delta[state];
-            for (unsigned i = 0; i < mvs.size(); ++i) {
-                unsigned tgt = mvs[i].dst();
-                if (mvs[i].is_epsilon() && !m_visited.contains(tgt)) {
-                    m_visited.insert(tgt);
-                    m_todo.push_back(tgt);
-                }
-            }
-        }
-        m_visited.reset();
-        SASSERT(m_todo.empty());   
-    }
-
-    static void append_moves(unsigned offset, automaton const& a, moves& mvs) {
-        for (unsigned i = 0; i < a.num_states(); ++i) {
-            moves const& mvs1 = a.m_delta[i];
-            for (unsigned j = 0; j < mvs1.size(); ++j) {
-                move const& mv = mvs1[j];
-                mvs.push_back(move(a.m, mv.src() + offset, mv.dst() + offset, mv.t()));
-            }
-        }
-    }
-
-    static void append_final(unsigned offset, automaton const& a, unsigned_vector& final) {
-        for (unsigned s : a.m_final_states) {
-            final.push_back(s+offset);
-        }
-    }
- 
-};
-
-typedef automaton<unsigned> uautomaton;
-
-

src/math/automata/boolean_algebra.h

@@ -1,43 +0,0 @@
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
-Module Name:
-
-    boolean_algebra.h
-
-Abstract:
-
-    Boolean Algebra, a la Margus Veanes Automata library.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2016-2-27
-
-Revision History:
-
-
---*/
-
-#pragma once
-
-#include "util/util.h"
-
-template<class T>
-class positive_boolean_algebra {
-public:
-    virtual ~positive_boolean_algebra() = default;
-    virtual T mk_false() = 0;
-    virtual T mk_true() = 0;
-    virtual T mk_and(T x, T y) = 0;
-    virtual T mk_or(T x, T y) = 0;
-    virtual T mk_and(unsigned sz, T const* ts) = 0;
-    virtual T mk_or(unsigned sz, T const* ts) = 0;
-    virtual lbool is_sat(T x) = 0;
-};
-
-template<class T>
-class boolean_algebra : public positive_boolean_algebra<T> {
-public:
-    virtual T mk_not(T x) = 0;
-};
-

src/math/automata/symbolic_automata.h

@@ -1,152 +0,0 @@
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
-Module Name:
-
-    symbolic_automata.h
-
-Abstract:
-
-    Symbolic Automata over Boolean Algebras, a la Margus Veanes Automata library.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2016-02-27.
-
-Revision History:
-
-
---*/
-
-#pragma once
-
-
-#include "math/automata/automaton.h"
-#include "math/automata/boolean_algebra.h"
-
-
-template<class T, class M = default_value_manager<T> >
-class symbolic_automata {
-    typedef automaton<T, M>    automaton_t;
-    typedef boolean_algebra<T*> ba_t;
-    typedef typename automaton_t::move  move_t;
-    typedef vector<move_t>     moves_t;
-    typedef obj_ref<T, M>      ref_t;
-    typedef ref_vector<T, M>   refs_t;
-    typedef std::pair<unsigned, unsigned> unsigned_pair;
-    template<class V> class u2_map : public map<unsigned_pair, V, pair_hash<unsigned_hash, unsigned_hash>, default_eq<unsigned_pair> > {};
-
-
-    M&    m;
-    ba_t& m_ba;
-
-
-    class block {
-        uint_set m_set;
-        unsigned m_rep;
-        bool     m_rep_chosen;
-    public:
-
-        block(): m_rep(0), m_rep_chosen(false) {}
-
-        block(uint_set const& s):
-            m_set(s),
-            m_rep(0),
-            m_rep_chosen(false) {
-        }
-
-        block(unsigned_vector const& vs) {
-            for (unsigned i = 0; i < vs.size(); ++i) {
-                m_set.insert(vs[i]);               
-            }
-            m_rep_chosen = false;
-            m_rep = 0;
-        }
-
-        block& operator=(block const& b) {
-            m_set = b.m_set;
-            m_rep = 0;
-            m_rep_chosen = false;
-            return *this;
-        }
-
-        unsigned get_representative() {
-            if (!m_rep_chosen) {
-                uint_set::iterator it = m_set.begin();
-                if (m_set.end() != it) {
-                    m_rep = *it;                    
-                }
-                m_rep_chosen = true;
-            }
-            return m_rep;
-        }
-
-        void insert(unsigned i) { m_set.insert(i); }
-        bool contains(unsigned i) const { return m_set.contains(i); }        
-        bool is_empty() const { return m_set.empty(); }
-        unsigned size() const { return m_set.num_elems(); }
-        void remove(unsigned i) { m_set.remove(i); m_rep_chosen = false; }        
-        void clear() { m_set.reset(); m_rep_chosen = false; }
-        uint_set::iterator begin() const { return m_set.begin(); }
-        uint_set::iterator end() const { return m_set.end(); }
-    };
-
-    void add_block(block const& p1, unsigned p0_index, unsigned_vector& blocks, vector<block>& pblocks, unsigned_vector& W);
-
-public:
-    symbolic_automata(M& m, ba_t& ba): m(m), m_ba(ba) {}
-    automaton_t* mk_determinstic(automaton_t& a);
-    automaton_t* mk_complement(automaton_t& a);
-    automaton_t* remove_epsilons(automaton_t& a);
-    automaton_t* mk_total(automaton_t& a);
-    automaton_t* mk_minimize(automaton_t& a);
-    automaton_t* mk_minimize_total(automaton_t& a);
-    automaton_t* mk_difference(automaton_t& a, automaton_t& b);
-    automaton_t* mk_product(automaton_t& a, automaton_t& b);
-
-private:
-    automaton_t* mk_determinstic_param(automaton_t& a, bool flip_acceptance);
-    
-    vector<std::pair<vector<bool>, ref_t> > generate_min_terms(vector<ref_t> &constraints) {
-        vector<std::pair<vector<bool>, ref_t> > min_terms;
-        
-        ref_t curr_pred(m_ba.mk_true(), m);
-        vector<bool> curr_bv;
-        
-        generate_min_terms_rec(constraints, min_terms, 0, curr_bv, curr_pred);
-        
-        return min_terms;
-    }
-    void generate_min_terms_rec(vector<ref_t> &constraints, vector<std::pair<vector<bool>, ref_t> > &min_terms, unsigned i, vector<bool> &curr_bv, ref_t &curr_pred) {
-        lbool is_sat = m_ba.is_sat(curr_pred);
-        if (is_sat == l_undef)
-            throw default_exception("incomplete theory: unable to generate min-terms");
-
-        if (is_sat != l_true) {
-            return;
-        }
-        
-        if (i == constraints.size()) {
-            min_terms.push_back(std::pair<vector<bool>, ref_t>(curr_bv, curr_pred));
-        }
-        else {
-            //true case
-            curr_bv.push_back(true);
-            ref_t new_pred_pos(m_ba.mk_and(curr_pred, constraints[i]), m);
-            generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_pos);
-            curr_bv.pop_back();
-            
-            //false case
-            curr_bv.push_back(false);
-            ref_t neg(m_ba.mk_not(constraints[i]), m);
-            ref_t new_pred_neg(m_ba.mk_and(curr_pred, neg), m);
-            generate_min_terms_rec(constraints, min_terms, i + 1, curr_bv, new_pred_neg);
-            curr_bv.pop_back();
-        }
-    }
-
-};
-
-
-
-

src/math/automata/symbolic_automata_def.h

@@ -1,490 +0,0 @@
-/*++
-Copyright (c) 2015 Microsoft Corporation
-
-Module Name:
-
-    symbolic_automata_def.h
-
-Abstract:
-
-    Symbolic Automata over Boolean Algebras, a la Margus Veanes Automata library.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2016-02-27.
-
-Revision History:
-
-
---*/
-
-#pragma once
-
-
-#include "math/automata/symbolic_automata.h"
-#include "util/hashtable.h"
-#include "util/vector.h"
-
-
-
-
-template<class T, class M>
-typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_total(automaton_t& a) {
-    unsigned dead_state = a.num_states();
-    moves_t mvs, new_mvs;
-    for (unsigned i = 0; i < dead_state; ++i) {
-        mvs.reset();
-        a.get_moves_from(i, mvs, true);
-        refs_t vs(m);
-        
-        for (unsigned j = 0; j < mvs.size(); ++j) {
-            vs.push_back(mvs[j].t());
-        }
-        ref_t cond(m_ba.mk_not(m_ba.mk_or(vs.size(), vs.data())), m);
-        lbool is_sat = m_ba.is_sat(cond);
-        if (is_sat == l_undef) {
-            return nullptr;
-        }
-        if (is_sat == l_true) {
-            new_mvs.push_back(move_t(m, i, dead_state, cond));
-        }
-    }
-    if (new_mvs.empty()) {
-        return a.clone();
-    }
-    new_mvs.push_back(move_t(m, dead_state, dead_state, m_ba.mk_true()));
-
-    // TBD private: automaton_t::append_moves(0, a, new_mvs);
-    
-    return alloc(automaton_t, m, a.init(), a.final_states(), new_mvs);        
-}
-
-template<class T, class M>
-typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minimize(automaton_t& a) {
-    if (a.is_empty()) {
-        return a.clone();
-    }
-
-    if (a.is_epsilon()) {
-        return a.clone();
-    }
-    // SASSERT(a.is_deterministic());
-    
-    scoped_ptr<automaton_t> fa = mk_total(a);
-    if (!fa) {
-        return 0;
-    }
-    return mk_minimize_total(*fa.get());
-}
-
-
-template<class T, class M>
-void symbolic_automata<T, M>::add_block(block const& p1, unsigned p0_index, unsigned_vector& blocks, vector<block>& pblocks, unsigned_vector& W) {
-    block& p0 = pblocks[p0_index];
-    if (p1.size() < p0.size()) {
-        unsigned p1_index = pblocks.size();
-        pblocks.push_back(p1);
-        for (uint_set::iterator it = p1.begin(), end = p1.end(); it != end; ++it) {
-            p0.remove(*it);
-            blocks[*it] = p1_index;
-        }
-        if (W.contains(p0_index)) {
-            W.push_back(p1_index);
-        }
-        else if (p0.size() <= p1.size()) {
-            W.push_back(p0_index);
-        }
-        else {
-            W.push_back(p1_index);
-        }
-    }                
-}
-
-template<class T, class M>
-typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_minimize_total(automaton_t& a) {    
-    vector<block> pblocks;
-    unsigned_vector blocks;
-    unsigned_vector non_final;
-    for (unsigned i = 0; i < a.num_states(); ++i) {
-        if (!a.is_final_state(i)) {
-            non_final.push_back(i);
-            blocks.push_back(1);
-        }
-        else {
-            blocks.push_back(0);
-        }
-    }
-    pblocks.push_back(block(a.final_states()));      // 0 |-> final states
-    pblocks.push_back(block(non_final));             // 1 |-> non-final states
-
-    unsigned_vector W;
-    W.push_back(pblocks[0].size() > pblocks[1].size() ? 1 : 0);
-        
-    refs_t trail(m);
-    u_map<T*> gamma;
-    moves_t mvs;
-    while (!W.empty()) {
-        block R(pblocks[W.back()]);
-        W.pop_back();
-        gamma.reset();
-        uint_set::iterator it = R.begin(), end = R.end();
-        for (; it != end; ++it) {
-            unsigned dst = *it;
-            mvs.reset();
-            a.get_moves_to(dst, mvs);
-            for (unsigned i = 0; i < mvs.size(); ++i) {
-                unsigned src = mvs[i].src();
-                if (pblocks[src].size() > 1) {
-                    T* t = mvs[i].t();
-                    T* t1;
-                    if (gamma.find(src, t1)) {
-                        t = m_ba.mk_or(t, t1);
-                        trail.push_back(t);
-                    }
-                    gamma.insert(src, t);
-                }
-            }
-        }
-        uint_set relevant1;
-        typedef typename u_map<T*>::iterator gamma_iterator;
-        gamma_iterator gend = gamma.end();
-        for (gamma_iterator git = gamma.begin(); git != gend; ++git) {
-            unsigned p0A_index = blocks[git->m_key];
-            if (relevant1.contains(p0A_index)) {
-                continue;
-            }
-            relevant1.insert(p0A_index);
-            block& p0A = pblocks[p0A_index];
-            block p1;
-            for (gamma_iterator it = gamma.begin(); it != gend; ++it) {
-                if (p0A.contains(it->m_key)) p1.insert(it->m_key);
-            }
-            
-            add_block(p1, p0A_index, blocks, pblocks, W);
-
-            bool iterate = true;
-            while (iterate) {
-                iterate = false;
-                uint_set relevant2;
-                for (gamma_iterator it = gamma.begin(); it != gend; ++it) {
-                    unsigned p0B_index = blocks[it->m_key];
-                    if (pblocks[p0B_index].size() <= 1 || relevant2.contains(p0B_index)) {
-                        continue;
-                    }
-                    relevant2.insert(p0B_index);
-                    block const& p0B = pblocks[p0B_index];
-                    uint_set::iterator bi = p0B.begin(), be = p0B.end();
-
-                    block p1;
-                    p1.insert(*bi);
-                    bool split_found = false;
-                    ref_t psi(gamma[*bi], m); 
-                    ++bi;
-                    for (; bi != be; ++bi) {
-                        unsigned q = *bi;
-                        ref_t phi(gamma[q], m);
-                        if (split_found) {
-                            ref_t phi_and_psi(m_ba.mk_and(phi, psi), m);
-                            switch (m_ba.is_sat(phi_and_psi)) {
-                            case l_true:
-                                p1.insert(q);
-                                break;
-                            case l_undef:
-                                return nullptr;
-                            default:
-                                break;
-                            }                            
-                        }
-                        else {
-                            ref_t psi_min_phi(m_ba.mk_and(psi, m_ba.mk_not(phi)), m);
-                            lbool is_sat = m_ba.is_sat(psi_min_phi);
-                            if (is_sat == l_undef) {
-                                return nullptr;
-                            }
-                            if (is_sat == l_true) {
-                                psi = psi_min_phi;
-                                split_found = true;
-                                continue;
-                            }
-                            // psi is a subset of phi
-                            ref_t phi_min_psi(m_ba.mk_and(phi, m_ba.mk_not(psi)), m);
-                            is_sat = m_ba.is_sat(phi_min_psi);
-                            if (is_sat == l_undef) {
-                                return nullptr;
-                            }
-                            else if (is_sat == l_false) {
-                                p1.insert(q); // psi and phi are equivalent
-                            }
-                            else {
-                                p1.clear();
-                                p1.insert(q);
-                                psi = phi_min_psi;
-                                split_found = true;
-                            }
-                        }
-                    }
-                    if (p1.size() < p0B.size() && p0B.size() > 2) iterate = true;
-                    add_block(p1, p0B_index, blocks, pblocks, W);
-                }
-            }
-        }
-    }
-
-    unsigned new_init = pblocks[blocks[a.init()]].get_representative();
-
-    // set moves
-    u2_map<T*> conds;
-    svector<unsigned_pair> keys;
-    moves_t new_moves;
-
-    for (unsigned i = 0; i < a.num_states(); ++i) {
-        unsigned src = pblocks[blocks[i]].get_representative();
-        typename automaton_t::moves const& mvs = a.get_moves_from(i);
-        for (unsigned j = 0; j < mvs.size(); ++j) {
-            unsigned dst = pblocks[blocks[mvs[j].dst()]].get_representative();
-            unsigned_pair st(src, dst);
-            T* t = 0;
-            if (conds.find(st, t)) {
-                t = m_ba.mk_or(t, mvs[j].t());
-                trail.push_back(t);
-                conds.insert(st, t);
-            }
-            else {
-                conds.insert(st, mvs[j].t());
-                keys.push_back(st);
-            }
-        }
-    }    
-    for (unsigned i = 0; i < keys.size(); ++i) {
-        unsigned_pair st = keys[i];
-        new_moves.push_back(move_t(m, st.first, st.second, conds[st]));
-    }
-    // set final states.
-    unsigned_vector new_final;
-    uint_set new_final_set;
-    for (unsigned i = 0; i < a.final_states().size(); ++i) {
-        unsigned f = pblocks[blocks[a.final_states()[i]]].get_representative();
-        if (!new_final_set.contains(f)) {
-            new_final_set.insert(f);
-            new_final.push_back(f);
-        }
-    }
-
-    return alloc(automaton_t, m, new_init, new_final, new_moves);
-}
-
-template<class T, class M>
-typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_determinstic(automaton_t& a) {
-    return mk_determinstic_param(a);
-}
-
-template<class T, class M>
-typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_complement(automaton_t& a) {
-    return mk_determinstic_param(a, true);
-}
-
-template<class T, class M>
-typename symbolic_automata<T, M>::automaton_t* 
-symbolic_automata<T, M>::mk_determinstic_param(automaton_t& a, bool flip_acceptance) {
-    vector<std::pair<vector<bool>, ref_t> > min_terms;
-    vector<ref_t> predicates;
-
-    map<uint_set, unsigned, uint_set::hash, uint_set::eq> s2id; // set of states to unique id
-    vector<uint_set> id2s;                           // unique id to set of b-states
-    uint_set set;
-    unsigned_vector vector;
-    moves_t new_mvs;                                 // moves in the resulting automaton
-    unsigned_vector new_final_states;                // new final states
-    unsigned p_state_id = 0;                         // next state identifier
-
-    TRACE(seq, tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);    
-    // adds non-final states of a to final if flipping and final otherwise
-    unsigned_vector init_states;
-    a.get_epsilon_closure(a.init(), init_states);    
-    for (unsigned s : init_states) {
-        set.insert(s);
-    }
-    if (a.is_final_configuration(set) != flip_acceptance) {
-        new_final_states.push_back(p_state_id);
-    }
-    
-    s2id.insert(set, p_state_id++);               // the index to the initial state is 0
-    id2s.push_back(set);
-    
-    ::vector<uint_set> todo; //States to visit
-    todo.push_back(set);
-    
-    uint_set state;
-    moves_t mvsA;
-    
-    new_mvs.reset();
-    
-    // or just make todo a vector whose indices coincide with state_id.
-    while (!todo.empty()) {
-        uint_set state = todo.back();
-        
-        unsigned state_id = s2id[state];
-        todo.pop_back();
-        mvsA.reset();
-        
-        min_terms.reset();
-        predicates.reset();
-        
-        a.get_moves_from_states(state, mvsA);
-        
-        for (unsigned j = 0; j < mvsA.size(); ++j) {
-            ref_t mv_guard(mvsA[j].t(),m);
-            predicates.push_back(mv_guard);
-        }
-        
-        min_terms = generate_min_terms(predicates);
-        for (unsigned j = 0; j < min_terms.size(); ++j) {
-            set = uint_set();
-            for (unsigned i = 0; i < mvsA.size(); ++i) {
-                if (min_terms[j].first[i])
-                    set.insert(mvsA[i].dst());
-            }
-            
-            bool is_new = !s2id.contains(set);
-            if (is_new) {
-                TRACE(seq, tout << "mk-deterministic " << flip_acceptance << " " << set << " " << a.is_final_configuration(set) << "\n";);    
-                if (a.is_final_configuration(set) != flip_acceptance) {
-                    new_final_states.push_back(p_state_id);
-                }
-                
-                s2id.insert(set, p_state_id++);
-                id2s.push_back(set);
-                todo.push_back(set);
-            }
-            new_mvs.push_back(move_t(m, state_id, s2id[set], min_terms[j].second));
-        }
-    }
-    
-    if (new_final_states.empty()) {
-        return alloc(automaton_t, m);
-    }
-    
-    return alloc(automaton_t, m, 0, new_final_states, new_mvs);
-}
-
-
-
-template<class T, class M>
-typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_product(automaton_t& a, automaton_t& b) {
-    u2_map<unsigned> pair2id;
-    unsigned_pair init_pair(a.init(), b.init());
-    svector<unsigned_pair> todo;
-    todo.push_back(init_pair);
-    pair2id.insert(init_pair, 0);
-    moves_t mvs;
-    unsigned_vector final;
-    unsigned_vector a_init, b_init;
-    a.get_epsilon_closure(a.init(), a_init);
-    bool a_init_is_final = false, b_init_is_final = false;
-    for (unsigned ia : a_init) {
-        if (a.is_final_state(ia)) {
-            a_init_is_final = true;
-            b.get_epsilon_closure(b.init(), b_init);
-            for (unsigned ib : b_init) {
-                if (b.is_final_state(ib)) {
-                    b_init_is_final = true;
-                    final.push_back(0);
-                    break;
-                }
-            }
-            break;
-        }
-    }
-    
-    unsigned n = 1;
-    moves_t mvsA, mvsB;
-    while (!todo.empty()) {
-        unsigned_pair curr_pair = todo.back();
-        todo.pop_back();
-        unsigned src = pair2id[curr_pair];
-        mvsA.reset(); mvsB.reset();
-        a.get_moves_from(curr_pair.first,  mvsA, true);
-        b.get_moves_from(curr_pair.second, mvsB, true);
-        for (unsigned i = 0; i < mvsA.size(); ++i) {
-            for (unsigned j = 0; j < mvsB.size(); ++j) {
-                ref_t ab(m_ba.mk_and(mvsA[i].t(), mvsB[j].t()), m);   
-                lbool is_sat = m_ba.is_sat(ab);
-                if (is_sat == l_false) {
-                    continue;
-                }
-                else if (is_sat == l_undef) {
-                    return nullptr;
-                }
-                unsigned_pair tgt_pair(mvsA[i].dst(), mvsB[j].dst());
-                unsigned tgt;
-                if (!pair2id.find(tgt_pair, tgt)) {
-                    tgt = n++;
-                    pair2id.insert(tgt_pair, tgt);
-                    todo.push_back(tgt_pair);
-                    if (a.is_final_state(tgt_pair.first) && b.is_final_state(tgt_pair.second)) {
-                        final.push_back(tgt);
-                    }
-                }
-                mvs.push_back(move_t(m, src, tgt, ab));
-            }
-        }
-    }
-    
-    if (final.empty()) {
-        return alloc(automaton_t, m);
-    }
-    vector<moves_t> inv(n, moves_t());
-    for (unsigned i = 0; i < mvs.size(); ++i) {
-        move_t const& mv = mvs[i];
-        inv[mv.dst()].push_back(move_t(m, mv.dst(), mv.src(), mv.t())); 
-    }
-    
-    bool_vector back_reachable(n, false);
-    for (unsigned f : final) {
-        back_reachable[f] = true;
-    }
-    
-    unsigned_vector stack(final);
-    while (!stack.empty()) {
-        unsigned state = stack.back();
-        stack.pop_back();
-        moves_t const& mv = inv[state];
-        for (unsigned i = 0; i < mv.size(); ++i) {
-            state = mv[i].dst();
-            if (!back_reachable[state]) {
-                back_reachable[state] = true;
-                stack.push_back(state);
-            }
-        }
-    }
-    
-    moves_t mvs1;
-    for (unsigned i = 0; i < mvs.size(); ++i) {
-        move_t const& mv = mvs[i];
-        if (back_reachable[mv.dst()]) {
-            mvs1.push_back(mv);
-        }
-    }
-    if (mvs1.empty()) {
-        if (a_init_is_final && b_init_is_final) {
-            // special case: automaton has no moves, but the initial state is final on both sides
-            // this results in the automaton which accepts the empty sequence and nothing else
-            final.clear();
-            final.push_back(0);
-            return alloc(automaton_t, m, 0, final, mvs1);
-        } else {
-            return alloc(automaton_t, m);
-        }
-    }
-    else {
-        return alloc(automaton_t, m, 0, final, mvs1);
-    }
-} 
-
-
-
-template<class T, class M>
-typename symbolic_automata<T, M>::automaton_t* symbolic_automata<T, M>::mk_difference(automaton_t& a, automaton_t& b) {
-    return mk_product(a,mk_complement(b));
-}
-

src/model/model.cpp

@@ -572,13 +572,6 @@ expr_ref model::operator()(expr* t) {
     return m_mev(t);
 }
 
-void model::set_solver(expr_solver* s) {
-    m_mev.set_solver(s);
-}
-
-bool model::has_solver() {
-    return m_mev.has_solver();
-}
 
 expr_ref_vector model::operator()(expr_ref_vector const& ts) {
     expr_ref_vector rs(m);

src/model/model.h

@@ -110,8 +110,6 @@ public:
     bool is_false(expr_ref_vector const& ts);
     bool are_equal(expr* s, expr* t);
     void reset_eval_cache();
-    bool has_solver(); 
-    void set_solver(expr_solver* solver);
     void add_rec_funs();
 
     class scoped_model_completion {

src/model/model_evaluator.cpp

@@ -864,14 +864,6 @@ bool model_evaluator::eval(expr_ref_vector const& ts, expr_ref& r, bool model_co
     return eval(tmp, r, model_completion);
 }
 
-void model_evaluator::set_solver(expr_solver* solver) {
-    m_imp->m_cfg.m_seq_rw.set_solver(solver);
-}
-
-bool model_evaluator::has_solver() {
-    return m_imp->m_cfg.m_seq_rw.has_solver();
-}
-
 model_core const & model_evaluator::get_model() const {
     return m_imp->cfg().m_model;
 }

src/model/model_evaluator.h

@@ -57,10 +57,6 @@ public:
     bool is_true(expr_ref_vector const& ts);
     bool are_equal(expr* s, expr* t);
 
-
-    void set_solver(expr_solver* solver);
-    bool has_solver();
-
     /**
      * best effort evaluator of extensional array equality.
      */

src/nlsat/nlsat_explain.cpp

@@ -593,7 +593,7 @@ namespace nlsat {
         /**
            \brief Add factors of p to todo
         */
-        void add_factors(polynomial_ref & p) {
+        void insert_fresh_factors_in_todo(polynomial_ref & p) {
             if (is_const(p))
                 return;
             elim_vanishing(p);
@@ -646,27 +646,21 @@ namespace nlsat {
             return true;
         }
         
-	// For each p in ps add the leading or all the coefficients of p to the projection,
+	// For each p in ps add the leading coefficent to the projection,
-        // depending on the well-orientedness of ps.
+        void add_lc(polynomial_ref_vector &ps, var x) {
-        void add_lcs(polynomial_ref_vector &ps, var x) {
             polynomial_ref p(m_pm);
             polynomial_ref coeff(m_pm);
 
-            bool sqf = is_square_free_at_sample(ps, x);
             // Add coefficients based on well-orientedness
             for (unsigned i = 0; i < ps.size(); i++) {
                 p = ps.get(i);
                 unsigned k_deg = m_pm.degree(p, x);
                 if (k_deg == 0) continue;
                 // p depends on x
-                TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p); tout << (sqf ? " (sqf)" : " (!sqf)") << "\n";);
+                TRACE(nlsat_explain, tout << "processing poly of degree " << k_deg << " w.r.t x" << x << ": "; display(tout, p) << "\n";);
-                for (unsigned j_coeff_deg = k_deg; j_coeff_deg >= 1; j_coeff_deg--) { 
+                coeff = m_pm.coeff(p, x, k_deg);
-                    coeff = m_pm.coeff(p, x, j_coeff_deg);
+                TRACE(nlsat_explain, tout << "    coeff deg " << k_deg << ": "; display(tout, coeff) << "\n";);
-                    TRACE(nlsat_explain, tout << "    coeff deg " << j_coeff_deg << ": "; display(tout, coeff) << "\n";);
+                insert_fresh_factors_in_todo(coeff);
-                    add_factors(coeff);
-                    if (sqf)
-                        break;
-                }
                 
             }
         }
@@ -772,7 +766,7 @@ namespace nlsat {
                       display(tout, s);
                       tout << "\n";);
                 // s did not vanish completely, but its leading coefficient may have vanished
-                add_factors(s);
+                insert_fresh_factors_in_todo(s);
                 return; 
             }
         }
@@ -1209,7 +1203,7 @@ namespace nlsat {
                 TRACE(nlsat_explain,  tout << "project loop, processing var "; display_var(tout, x);
                       tout << "\npolynomials\n";
                       display(tout, ps); tout << "\n";);
-                add_lcs(ps, x);
+                add_lc(ps, x);
                 psc_discriminant(ps, x);
                 psc_resultant(ps, x);
                 if (m_todo.empty())
@@ -1231,18 +1225,24 @@ namespace nlsat {
                 return;
 
             m_todo.reset();
-            for (poly* p : ps) {
+            for (unsigned i = 0; i < ps.size(); i++) {
-                m_todo.insert(p);
+                polynomial_ref p(m_pm);
+                p = ps.get(i);
+                insert_fresh_factors_in_todo(p);
             }
+            // replace ps by the fresh factors
+            ps.reset();
+            for (auto p: m_todo.m_set)
+                ps.push_back(p);
+            
             var x = m_todo.extract_max_polys(ps);
             // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
             
             polynomial_ref_vector samples(m_pm);
 
             
-            if (x < max_x){
+            if (x < max_x)
                 cac_add_cell_lits(ps, x, samples);
-            }
 
             while (true) {
                 if (all_univ(ps, x) && m_todo.empty()) {
@@ -1251,7 +1251,7 @@ namespace nlsat {
                 }
                 TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
                       display(tout, ps); tout << "\n";);
-                add_lcs(ps, x);
+                add_lc(ps, x);
                 psc_discriminant(ps, x);
                 psc_resultant(ps, x);
                 

src/params/CMakeLists.txt

@@ -11,7 +11,6 @@ z3_add_component(params
     theory_bv_params.cpp
     theory_pb_params.cpp
     theory_seq_params.cpp       
-    theory_str_params.cpp        
   COMPONENT_DEPENDENCIES
     util
     ast

src/params/smt_params.cpp

@@ -80,7 +80,6 @@ void smt_params::updt_params(params_ref const & p) {
     theory_pb_params::updt_params(p);
     // theory_array_params::updt_params(p);
     theory_datatype_params::updt_params(p);
-    theory_str_params::updt_params(p);
     updt_local_params(p);
 }
 
@@ -100,7 +99,6 @@ void smt_params::display(std::ostream & out) const {
     theory_bv_params::display(out);
     theory_pb_params::display(out);
     theory_datatype_params::display(out);
-    theory_str_params::display(out);
 
     DISPLAY_PARAM(m_display_proof);
     DISPLAY_PARAM(m_display_dot_proof);

src/params/smt_params.h

@@ -24,7 +24,6 @@ Revision History:
 #include "params/theory_arith_params.h"
 #include "params/theory_array_params.h"
 #include "params/theory_bv_params.h"
-#include "params/theory_str_params.h"
 #include "params/theory_seq_params.h"
 #include "params/theory_pb_params.h"
 #include "params/theory_datatype_params.h"
@@ -79,7 +78,6 @@ struct smt_params : public preprocessor_params,
                     public theory_arith_params,
                     public theory_array_params,
                     public theory_bv_params,
-                    public theory_str_params,
                     public theory_seq_params,
                     public theory_pb_params,
                     public theory_datatype_params {

src/params/theory_str_params.cpp

@@ -1,57 +0,0 @@
-/*++
-Module Name:
-
-    theory_str_params.cpp
-
-Abstract:
-
-    Parameters for string theory plugin
-
-Author:
-
-    Murphy Berzish (mtrberzi) 2016-12-13
-
-Revision History:
-
---*/
-
-#include "params/theory_str_params.h"
-#include "params/smt_params_helper.hpp"
-
-void theory_str_params::updt_params(params_ref const & _p) {
-    smt_params_helper p(_p);
-    m_StrongArrangements = p.str_strong_arrangements();
-    m_AggressiveLengthTesting = p.str_aggressive_length_testing();
-    m_AggressiveValueTesting = p.str_aggressive_value_testing();
-    m_AggressiveUnrollTesting = p.str_aggressive_unroll_testing();
-    m_UseFastLengthTesterCache = p.str_fast_length_tester_cache();
-    m_UseFastValueTesterCache = p.str_fast_value_tester_cache();
-    m_StringConstantCache = p.str_string_constant_cache();
-    m_OverlapTheoryAwarePriority = p.str_overlap_priority();
-    m_RegexAutomata_DifficultyThreshold = p.str_regex_automata_difficulty_threshold();
-    m_RegexAutomata_IntersectionDifficultyThreshold = p.str_regex_automata_intersection_difficulty_threshold();
-    m_RegexAutomata_FailedAutomatonThreshold = p.str_regex_automata_failed_automaton_threshold();
-    m_RegexAutomata_FailedIntersectionThreshold = p.str_regex_automata_failed_intersection_threshold();
-    m_RegexAutomata_LengthAttemptThreshold = p.str_regex_automata_length_attempt_threshold();
-    m_FixedLengthRefinement = p.str_fixed_length_refinement();
-    m_FixedLengthNaiveCounterexamples = p.str_fixed_length_naive_cex();
-}
-
-#define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
-
-void theory_str_params::display(std::ostream & out) const {
-    DISPLAY_PARAM(m_StrongArrangements);
-    DISPLAY_PARAM(m_AggressiveLengthTesting);
-    DISPLAY_PARAM(m_AggressiveValueTesting);
-    DISPLAY_PARAM(m_AggressiveUnrollTesting);
-    DISPLAY_PARAM(m_UseFastLengthTesterCache);
-    DISPLAY_PARAM(m_UseFastValueTesterCache);
-    DISPLAY_PARAM(m_StringConstantCache);
-    DISPLAY_PARAM(m_OverlapTheoryAwarePriority);
-    DISPLAY_PARAM(m_RegexAutomata_DifficultyThreshold);
-    DISPLAY_PARAM(m_RegexAutomata_IntersectionDifficultyThreshold);
-    DISPLAY_PARAM(m_RegexAutomata_FailedAutomatonThreshold);
-    DISPLAY_PARAM(m_RegexAutomata_FailedIntersectionThreshold);
-    DISPLAY_PARAM(m_RegexAutomata_LengthAttemptThreshold);
-    DISPLAY_PARAM(m_FixedLengthNaiveCounterexamples);
-}

src/params/theory_str_params.h

@@ -1,122 +0,0 @@
-/*++
-Module Name:
-
-    theory_str_params.h
-
-Abstract:
-
-    Parameters for string theory plugin
-
-Author:
-
-    Murphy Berzish (mtrberzi) 2016-12-13
-
-Revision History:
-
---*/
-
-#pragma once
-
-#include "util/params.h"
-
-struct theory_str_params {
-    /*
-     * If AssertStrongerArrangements is set to true,
-     * the implications that would normally be asserted during arrangement generation
-     * will instead be asserted as equivalences.
-     * This is a stronger version of the standard axiom.
-     * The Z3str2 axioms can be simulated by setting this to false.
-     */
-    bool m_StrongArrangements = true;
-
-    /*
-     * If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities
-     * to prioritize trying concrete length options over choosing the "more" option.
-     */
-    bool m_AggressiveLengthTesting = false;
-
-    /*
-     * Similarly, if AggressiveValueTesting is true, we manipulate the phase of value tester equalities
-     * to prioritize trying concrete value options over choosing the "more" option.
-     */
-    bool m_AggressiveValueTesting = false;
-
-    /*
-     * If AggressiveUnrollTesting is true, we manipulate the phase of regex unroll tester equalities
-     * to prioritize trying concrete unroll counts over choosing the "more" option.
-     */
-    bool m_AggressiveUnrollTesting = true;
-
-    /*
-     * If UseFastLengthTesterCache is set to true,
-     * length tester terms will not be generated from scratch each time they are needed,
-     * but will be saved in a map and looked up.
-     */
-    bool m_UseFastLengthTesterCache = false;
-
-    /*
-     * If UseFastValueTesterCache is set to true,
-     * value tester terms will not be generated from scratch each time they are needed,
-     * but will be saved in a map and looked up.
-     */
-    bool m_UseFastValueTesterCache = true;
-
-    /*
-     * If StringConstantCache is set to true,
-     * all string constants in theory_str generated from anywhere will be cached and saved.
-     */
-    bool m_StringConstantCache = true;
-
-    double m_OverlapTheoryAwarePriority = -0.1;
-
-    /*
-     * RegexAutomata_DifficultyThreshold is the lowest difficulty above which Z3str3
-     * will not eagerly construct an automaton for a regular expression term.
-     */
-    unsigned m_RegexAutomata_DifficultyThreshold = 1000;
-
-    /*
-     * RegexAutomata_IntersectionDifficultyThreshold is the lowest difficulty above which Z3str3
-     * will not eagerly intersect automata to check unsatisfiability.
-     */
-    unsigned m_RegexAutomata_IntersectionDifficultyThreshold = 1000;
-
-    /*
-     * RegexAutomata_FailedAutomatonThreshold is the number of failed attempts to build an automaton
-     * after which a full automaton (i.e. with no length information) will be built regardless of difficulty.
-     */
-    unsigned m_RegexAutomata_FailedAutomatonThreshold = 10;
-
-    /*
-     * RegexAutomaton_FailedIntersectionThreshold is the number of failed attempts to perform automaton
-     * intersection after which intersection will always be performed regardless of difficulty.
-     */
-    unsigned m_RegexAutomata_FailedIntersectionThreshold = 10;
-
-    /*
-     * RegexAutomaton_LengthAttemptThreshold is the number of attempts to satisfy length/path constraints
-     * before which we begin checking unsatisfiability of a regex term.
-     */
-    unsigned m_RegexAutomata_LengthAttemptThreshold = 10;
-    /*
-     * If FixedLengthRefinement is true and the fixed-length equation solver is enabled,
-     * Z3str3 will use abstraction refinement to handle formulas that would result in disjunctions or expensive
-     * reductions to fixed-length formulas.
-     */
-    bool m_FixedLengthRefinement = false;
-
-    /*
-     * If FixedLengthNaiveCounterexamples is true and the fixed-length equation solver is enabled,
-     * Z3str3 will only construct simple counterexamples to block unsatisfiable length assignments
-     * instead of attempting to learn more complex lessons.
-     */
-    bool m_FixedLengthNaiveCounterexamples = true;
-
-    theory_str_params(params_ref const & p = params_ref()) {
-        updt_params(p);
-    }
-
-    void updt_params(params_ref const & p);
-    void display(std::ostream & out) const;
-};
-

src/sat/sat_solver/sat_smt_solver.cpp

@@ -566,6 +566,10 @@ public:
         ensure_euf()->user_propagate_register_diseq(diseq_eh);
     }
 
+    void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh) override {
+        ensure_euf()->user_propagate_register_on_binding(binding_eh);
+    }
+    
     void user_propagate_register_expr(expr* e) override { 
         ensure_euf()->user_propagate_register_expr(e);
     }

src/sat/smt/euf_solver.h

@@ -554,6 +554,10 @@ namespace euf {
             check_for_user_propagator();
             m_user_propagator->register_decide(ceh);
         }
+        void user_propagate_register_on_binding(user_propagator::binding_eh_t& on_binding_eh) {
+            check_for_user_propagator();
+            NOT_IMPLEMENTED_YET();
+        }
         void user_propagate_register_expr(expr* e) {
             check_for_user_propagator();
             m_user_propagator->add_expr(e);

src/smt/CMakeLists.txt

@@ -69,9 +69,6 @@ z3_add_component(smt
     theory_seq.cpp
     theory_sls.cpp
     theory_special_relations.cpp    
-    theory_str.cpp
-    theory_str_mc.cpp
-    theory_str_regex.cpp
     theory_user_propagator.cpp
     theory_utvpi.cpp
     theory_wmaxsat.cpp

src/smt/qi_queue.cpp

@@ -263,6 +263,11 @@ namespace smt {
         if (stat->get_num_instances() % m_params.m_qi_profile_freq == 0) {
             m_qm.display_stats(verbose_stream(), q);
         }
+
+        if (m_on_binding && !m_on_binding(q, instance)) {
+            verbose_stream() << "qi_queue: on_binding returned false, skipping instance.\n";
+            return;
+        }
         expr_ref lemma(m);
         if (m.is_or(s_instance)) {
             ptr_vector<expr> args;

src/smt/qi_queue.h

@@ -28,6 +28,7 @@ Revision History:
 #include "params/qi_params.h"
 #include "ast/cost_evaluator.h"
 #include "util/statistics.h"
+#include "tactic/user_propagator_base.h"
 
 namespace smt {
     class context;
@@ -52,6 +53,7 @@ namespace smt {
         cached_var_subst              m_subst;
         svector<float>                m_vals;
         double                        m_eager_cost_threshold = 0;
+        std::function<bool(quantifier*,expr*)> m_on_binding;
         struct entry {
             fingerprint * m_qb;
             float         m_cost;
@@ -95,6 +97,9 @@ namespace smt {
         void reset();
         void display_delayed_instances_stats(std::ostream & out) const;
         void collect_statistics(::statistics & st) const;
+        void register_on_binding(std::function<bool(quantifier* q, expr* e)> & on_binding) {
+            m_on_binding = on_binding;
+        }
     };
 };
 

src/smt/seq_eq_solver.cpp

@@ -459,7 +459,8 @@ bool theory_seq::branch_binary_variable(depeq const& e) {
     }
     if (lenX + rational(xs.size()) != lenY + rational(ys.size())) {
         // |x| - |y| = |ys| - |xs|
-        expr_ref a(mk_sub(mk_len(x), mk_len(y)), m);
+        auto p0 = mk_len(x);
+        expr_ref a(mk_sub(p0, mk_len(y)), m);
         expr_ref b(m_autil.mk_int(rational(ys.size())-rational(xs.size())), m);
         propagate_lit(e.dep(), 0, nullptr, mk_eq(a, b, false));
         return true;
@@ -702,7 +703,8 @@ bool theory_seq::branch_quat_variable(depeq const& e) {
     
     literal_vector lits;
     if (xs == ys) {
-        literal lit = mk_eq(mk_len(x1), mk_len(y1), false);
+        auto p0 = mk_len(x1);
+        literal lit = mk_eq(p0, mk_len(y1), false);
         if (ctx.get_assignment(lit) == l_undef) {
             TRACE(seq, tout << mk_pp(x1, m) << " = " << mk_pp(y1, m) << "?\n";);
             ctx.mark_as_relevant(lit);
@@ -1007,7 +1009,8 @@ bool theory_seq::propagate_length_coherence(expr* e) {
         // len(e) <= hi => len(tail) <= hi - lo
         expr_ref high1(m_autil.mk_le(len_e, m_autil.mk_numeral(hi, true)), m);
         if (hi == lo) {
-            add_axiom(~mk_literal(high1), mk_seq_eq(seq, emp));
+            auto p0 = ~mk_literal(high1);
+            add_axiom(p0, mk_seq_eq(seq, emp));
             added = true;
         }
         else {

src/smt/smt_context.h

@@ -1838,6 +1838,14 @@ namespace smt {
             m_user_propagator->register_decide(r);
         }
 
+        void user_propagate_register_on_binding(user_propagator::binding_eh_t& t) {
+            m_user_propagator->register_on_binding(t);
+        }
+
+        void register_on_binding(std::function<bool(quantifier* q, expr* inst)>& f) {
+            m_qmanager->register_on_binding(f);
+        }
+
         void user_propagate_initialize_value(expr* var, expr* value);
 
         bool watches_fixed(enode* n) const;

src/smt/smt_kernel.cpp

@@ -308,6 +308,10 @@ namespace smt {
         m_imp->m_kernel.user_propagate_register_fixed(fixed_eh);
     }
 
+    void kernel::user_propagate_register_on_binding(user_propagator::binding_eh_t& on_binding) {
+        m_imp->m_kernel.user_propagate_register_on_binding(on_binding);
+    }
+    
     void kernel::user_propagate_register_final(user_propagator::final_eh_t& final_eh) {
         m_imp->m_kernel.user_propagate_register_final(final_eh);
     }

src/smt/smt_kernel.h

@@ -319,6 +319,8 @@ namespace smt {
         
         void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh);
 
+        void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh);
+
         void user_propagate_register_expr(expr* e);
         
         void user_propagate_register_created(user_propagator::created_eh_t& r);

src/smt/smt_parallel.cpp

@@ -88,10 +88,14 @@ namespace smt {
                         // If the unsat core only contains assumptions, 
                         // unsatisfiability does not depend on the current cube and the entire problem is unsat.
                         if (all_of(unsat_core, [&](expr* e) { return asms.contains(e); })) {
-                            IF_VERBOSE(0, verbose_stream() << "Worker " << id << " determined formula unsat");
+                            IF_VERBOSE(0, verbose_stream() << "Worker " << id << " determined formula unsat\n");
                             b.set_unsat(l2g, unsat_core);
                             return;
                         }
+                        for (expr * e : unsat_core)
+                            if (asms.contains(e))
+                                b.report_assumption_used(l2g, e); // report assumptions used in unsat core, so they can be used in final core
+
                         // TODO: can share lemmas here, such as new units and not(and(unsat_core)), binary clauses, etc.
                         // TODO: remember assumptions used in core so that they get used for the final core.
                         IF_VERBOSE(0, verbose_stream() << "Worker " << id << " found unsat cube\n");
@@ -225,9 +229,11 @@ namespace smt {
         if (m_state != state::is_running)
             return;
         m_state = state::is_unsat;    
-        p.ctx.m_unsat_core.reset(); // need to reset the unsat core in the main context bc every time we do a check_sat call, don't want to have old info coming from a prev check_sat call
+
-        // actually, it gets reset internally in the context after each check_sat, so we don't need to do it here -- replace with assertion
+        // every time we do a check_sat call, don't want to have old info coming from a prev check_sat call
+        // the unsat core gets reset internally in the context after each check_sat, so we assert this property here
         // takeaway: each call to check_sat needs to have a fresh unsat core
+        SASSERT(p.ctx.m_unsat_core.empty());
         for (expr* e : unsat_core)
             p.ctx.m_unsat_core.push_back(l2g(e));
         cancel_workers();
@@ -251,6 +257,11 @@ namespace smt {
         cancel_workers();
     }
 
+    void parallel::batch_manager::report_assumption_used(ast_translation& l2g, expr* assumption) {
+        std::scoped_lock lock(mux);
+        m_used_assumptions.insert(l2g(assumption))
+    }
+
     lbool parallel::batch_manager::get_result() const {
         if (m.limit().is_canceled())
             return l_undef; // the main context was cancelled, so we return undef.
@@ -258,7 +269,12 @@ namespace smt {
             case state::is_running: // batch manager is still running, but all threads have processed their cubes, which means all cubes were unsat
                 if (!m_cubes.empty())
                     throw default_exception("inconsistent end state");
-                // TODO collect unsat core from assumptions, if any. -- this is for the version where asms are passed in (currently, asms are empty)
+                if (!m_assumptions_used.empty()) {
+                    // collect unsat core from assumptions used, if any.
+                    SASSERT(p.ctx.m_unsat_core.empty());
+                    for (auto a : m_assumptions_used)
+                        p.ctx.m_unsat_core.push_back(a);
+                }
                 return l_false;
             case state::is_unsat:
                 return l_false;
@@ -335,9 +351,9 @@ namespace smt {
         auto add_split_atom = [&](expr* atom, unsigned start) {
             unsigned stop = m_cubes.size();
             for (unsigned i = start; i < stop; ++i) {
-                m_cubes.push_back(m_cubes[i]); // push copy of m_cubes[i]
+                m_cubes.push_back(m_cubes[i]);
-                m_cubes.back().push_back(m.mk_not(atom)); // add ¬atom to the copy
+                m_cubes.back().push_back(m.mk_not(atom));
-                m_cubes[i].push_back(atom); // add atom to the original
+                m_cubes[i].push_back(atom);
             }
         };
 
@@ -443,6 +459,13 @@ namespace smt {
         if (m.has_trace_stream())
             throw default_exception("trace streams have to be off in parallel mode");
 
+        struct scoped_clear_table {
+            obj_hashtable& ht;
+            scoped_clear(obj_hashtable& ht) : ht(ht) {}
+            ~scoped_clear() { ht.reset(); }
+        };
+        scoped_clear_table clear(m_batch_manager.m_used_assumptions);
+
         {
             m_batch_manager.initialize();
             m_workers.reset();

src/smt/smt_parallel.h

@@ -46,6 +46,7 @@ namespace smt {
             unsigned m_max_batch_size = 10;
             unsigned m_exception_code = 0;
             std::string m_exception_msg;
+            obj_hashtable<expr> m_assumptions_used; // assumptions used in unsat cores, to be used in final core
 
             // called from batch manager to cancel other workers if we've reached a verdict
             void cancel_workers() {
@@ -76,6 +77,7 @@ namespace smt {
             // the batch manager re-enqueues unprocessed cubes and optionally splits them using the split_atoms returned by this and workers.
             // 
             void return_cubes(ast_translation& l2g, vector<expr_ref_vector>const& cubes, expr_ref_vector const& split_atoms);
+            void report_assumption_used(ast_translation& l2g, expr* assumption);
             void share_lemma(ast_translation& l2g, expr* lemma);
             lbool get_result() const;
         };

src/smt/smt_quantifier.cpp

@@ -339,6 +339,10 @@ namespace smt {
             m_plugin->add_eq_eh(n1, n2);
         }
 
+        void register_on_binding(std::function<bool(quantifier*, expr*)>& on_binding) {
+            m_qi_queue.register_on_binding(on_binding);
+        }
+
         void relevant_eh(enode * n) {
             m_plugin->relevant_eh(n);
         }
@@ -493,6 +497,10 @@ namespace smt {
         m_imp->add_eq_eh(n1, n2);
     }
 
+    void quantifier_manager::register_on_binding(std::function<bool(quantifier*, expr*)>& on_binding) {
+        m_imp->register_on_binding(on_binding);
+    }
+
     void quantifier_manager::relevant_eh(enode * n) {
         m_imp->relevant_eh(n);
     }

src/smt/smt_quantifier.h

@@ -23,6 +23,7 @@ Revision History:
 #include "util/statistics.h"
 #include "util/params.h"
 #include "smt/smt_types.h"
+#include "tactic/user_propagator_base.h"
 #include <tuple>
 
 class proto_model;
@@ -96,6 +97,8 @@ namespace smt {
         void collect_statistics(::statistics & st) const;
         void reset_statistics();
 
+        void register_on_binding(std::function<bool(quantifier*, expr*)> & f);
+
         ptr_vector<quantifier>::const_iterator begin_quantifiers() const;
         ptr_vector<quantifier>::const_iterator end_quantifiers() const;
         ptr_vector<quantifier>::const_iterator begin() const { return begin_quantifiers(); }

src/smt/smt_setup.cpp

@@ -39,7 +39,6 @@ Revision History:
 #include "smt/theory_sls.h"
 #include "smt/theory_pb.h"
 #include "smt/theory_fpa.h"
-#include "smt/theory_str.h"
 #include "smt/theory_polymorphism.h"
 
 namespace smt {
@@ -561,10 +560,7 @@ namespace smt {
     }
 
     void setup::setup_QF_S() {
-        if (m_params.m_string_solver == "z3str3") {
+        if (m_params.m_string_solver == "seq") {
-            setup_str();
-        }
-        else if (m_params.m_string_solver == "seq") {
             setup_unknown();
         }
         else if (m_params.m_string_solver == "char") {
@@ -582,7 +578,7 @@ namespace smt {
             // don't register any solver.
         }
         else {
-            throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
+            throw default_exception("invalid parameter for smt.string_solver, valid options are 'seq', 'auto'");
         }
     }
 
@@ -748,10 +744,7 @@ namespace smt {
 
     void setup::setup_seq_str(static_features const & st) {
         // check params for what to do here when it's ambiguous
-        if (m_params.m_string_solver == "z3str3") {
+        if (m_params.m_string_solver == "seq") {
-            setup_str();
-        } 
-        else if (m_params.m_string_solver == "seq") {
             setup_seq();
         } 
         else if (m_params.m_string_solver == "empty") {
@@ -761,15 +754,10 @@ namespace smt {
             // don't register any solver.
         }
         else if (m_params.m_string_solver == "auto") {            
-            if (st.m_has_seq_non_str) {
                 setup_seq();
-            } 
-            else {
-                setup_str();
-            }
         } 
         else {
-            throw default_exception("invalid parameter for smt.string_solver, valid options are 'z3str3', 'seq', 'auto'");
+            throw default_exception("invalid parameter for smt.string_solver, valid options are 'seq', 'auto'");
         }
     }
 
@@ -787,11 +775,6 @@ namespace smt {
         m_context.register_plugin(alloc(theory_fpa, m_context));
     }
 
-    void setup::setup_str() {
-        setup_arith();
-        m_context.register_plugin(alloc(theory_str, m_context, m_manager, m_params));
-    }
-
     void setup::setup_seq() {
         m_context.register_plugin(alloc(smt::theory_seq, m_context));
         setup_char();

src/smt/smt_setup.h

@@ -108,7 +108,6 @@ namespace smt {
         void setup_mi_arith();
         void setup_lra_arith();
         void setup_fpa();
-        void setup_str();
         void setup_relevancy(static_features& st);
 
     public:

src/smt/smt_solver.cpp

@@ -244,6 +244,10 @@ namespace {
             m_context.user_propagate_register_expr(e);
         }
 
+        void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh) override {
+            m_context.user_propagate_register_on_binding(binding_eh);
+        }
+
         void user_propagate_register_created(user_propagator::created_eh_t& c) override {
             m_context.user_propagate_register_created(c);
         }

src/smt/smt_theory.h

@@ -283,7 +283,6 @@ namespace smt {
         /**
            \brief This method is called by smt_context before the search starts
            to get any extra assumptions the theory wants to use.
-           (See theory_str for an example)
         */
         virtual void add_theory_assumptions(expr_ref_vector & assumptions) {
         }

src/smt/tactic/smt_tactic_core.cpp

@@ -402,6 +402,10 @@ public:
         m_diseq_eh = diseq_eh;
     }
 
+    void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh) override {
+        m_ctx.load()->user_propagate_register_on_binding(binding_eh);
+    }
+
     void user_propagate_register_expr(expr* e) override {
         m_vars.push_back(e);
     }

src/smt/theory_seq.cpp

@@ -440,7 +440,11 @@ final_check_status theory_seq::final_check_eh() {
 
 
 bool theory_seq::set_empty(expr* x) {
-    add_axiom(~mk_eq(m_autil.mk_int(0), mk_len(x), false), mk_eq_empty(x));
+    // pre-calculate literals to enforce evaluation order
+    auto zero = m_autil.mk_int(0);
+    literal zero_len_lit = mk_eq(zero, mk_len(x), false);
+    literal empty_lit    = mk_eq_empty(x);
+    add_axiom(~zero_len_lit, empty_lit);
     return true;
 }
 
@@ -1587,7 +1591,8 @@ void theory_seq::add_length_limit(expr* s, unsigned k, bool is_searching) {
     m_trail_stack.push(insert_obj_map<expr, unsigned>(m_length_limit_map, s));
     if (is_searching) {
         expr_ref dlimit = m_sk.mk_max_unfolding_depth(m_max_unfolding_depth);
-        add_axiom(~mk_literal(dlimit), mk_literal(lim_e));
+        auto p0 = ~mk_literal(dlimit);
+        add_axiom(p0, mk_literal(lim_e));
     }
 }
 
@@ -2905,7 +2910,8 @@ void theory_seq::ensure_nth(literal lit, expr* s, expr* idx) {
         m_sk.decompose(s2, head, tail);
         elems.push_back(head);
         len1 = mk_len(s2);
-        len2 = m_autil.mk_add(m_autil.mk_int(1), mk_len(tail));
+        auto one = m_autil.mk_int(1);
+        len2 = m_autil.mk_add(one, mk_len(tail));
         propagate_eq(lit, len1, len2, false);
         s2 = tail;
     }
@@ -3062,7 +3068,8 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             f = m_sk.mk_prefix_inv(se1, se2);
             f = mk_concat(se1, f);
             propagate_eq(lit, f, se2, true);
-            propagate_eq(lit, mk_len(f), mk_len(se2), false);
+            auto p0 = mk_len(f);
+            propagate_eq(lit, p0, mk_len(se2), false);
         }
         else {
             propagate_not_prefix(e);
@@ -3076,7 +3083,8 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             f = m_sk.mk_suffix_inv(se1, se2);
             f = mk_concat(f, se1);
             propagate_eq(lit, f, se2, true);
-            propagate_eq(lit, mk_len(f), mk_len(se2), false);
+            auto p0 = mk_len(f);
+            propagate_eq(lit, p0, mk_len(se2), false);
         }
         else {
             propagate_not_suffix(e);
@@ -3096,13 +3104,15 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
             expr_ref f2 = m_sk.mk_contains_right(se1, se2);
             f = mk_concat(f1, se2, f2);
             propagate_eq(lit, f, e1, true);
-            propagate_eq(lit, mk_len(f), mk_len(e1), false);
+            auto p0 = mk_len(f);
+            propagate_eq(lit, p0, mk_len(e1), false);
         }
         else {
             propagate_non_empty(lit, se2);
             dependency* dep = m_dm.mk_leaf(assumption(lit));
             // |e1| - |e2| <= -1
-            literal len_gt = m_ax.mk_le(mk_sub(mk_len(se1), mk_len(se2)), -1);
+            auto e1e = mk_len(se1);
+            literal len_gt = m_ax.mk_le(mk_sub(e1e, mk_len(se2)), -1);
             ctx.force_phase(len_gt);
             m_ncs.push_back(nc(expr_ref(e, m), len_gt, dep));
         }

src/smt/theory_str.h

@@ -1,779 +0,0 @@
-/*++
-  Module Name:
-
-  theory_str.h
-
-  Abstract:
-
-  String Theory Plugin
-
-  Author:
-
-  Murphy Berzish and Yunhui Zheng
-
-  Revision History:
-
-  --*/
-#pragma once
-
-#include "util/trail.h"
-#include "util/union_find.h"
-#include "util/scoped_ptr_vector.h"
-#include "util/hashtable.h"
-#include "ast/ast_pp.h"
-#include "ast/arith_decl_plugin.h"
-#include "ast/rewriter/th_rewriter.h"
-#include "ast/rewriter/seq_rewriter.h"
-#include "ast/seq_decl_plugin.h"
-#include "model/value_factory.h"
-#include "smt/smt_theory.h"
-#include "params/theory_str_params.h"
-#include "smt/smt_model_generator.h"
-#include "smt/smt_arith_value.h"
-#include "smt/smt_kernel.h"
-#include<set>
-#include<stack>
-#include<vector>
-#include<map>
-#include<functional>
-
-namespace smt {
-
-typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
-typedef int_hashtable<int_hash, default_eq<int> > integer_set;
-
-class str_value_factory : public value_factory {
-    seq_util u;
-    symbol_set m_strings;
-    std::string delim;
-    unsigned m_next;
-public:
-    str_value_factory(ast_manager & m, family_id fid) :
-        value_factory(m, fid),
-        u(m), delim("!"), m_next(0) {}
-    expr * get_some_value(sort * s) override {
-        return u.str.mk_string("some value");
-    }
-    bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) override {
-        v1 = u.str.mk_string("value 1");
-        v2 = u.str.mk_string("value 2");
-        return true;
-    }
-    expr * get_fresh_value(sort * s) override {
-        if (u.is_string(s)) {
-            while (true) {
-                std::ostringstream strm;
-                strm << delim << std::hex << (m_next++) << std::dec << delim;
-                std::string s(strm.str());
-                symbol sym(s);
-                if (m_strings.contains(sym)) continue;
-                m_strings.insert(sym);
-                return u.str.mk_string(s);
-            }
-        }
-        sort* seq = nullptr;
-        if (u.is_re(s, seq)) {
-            expr* v0 = get_fresh_value(seq);
-            return u.re.mk_to_re(v0);
-        }
-        TRACE(t_str, tout << "unexpected sort in get_fresh_value(): " << mk_pp(s, m_manager) << std::endl;);
-        UNREACHABLE(); return nullptr;
-    }
-    void register_value(expr * n) override { /* Ignore */ }
-};
-
-// NSB: added operator[] and contains to obj_pair_hashtable
-class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {};
-
-template<typename Ctx>
-class binary_search_trail : public trail {
-    obj_map<expr, ptr_vector<expr> > & target;
-    expr * entry;
-public:
-    binary_search_trail(obj_map<expr, ptr_vector<expr> > & target, expr * entry) :
-        target(target), entry(entry) {}
-    void undo() override {
-        TRACE(t_str_binary_search, tout << "in binary_search_trail::undo()" << std::endl;);
-        if (target.contains(entry)) {
-            if (!target[entry].empty()) {
-                target[entry].pop_back();
-            } else {
-                TRACE(t_str_binary_search, tout << "WARNING: attempt to remove length tester from an empty stack" << std::endl;);
-            }
-        } else {
-            TRACE(t_str_binary_search, tout << "WARNING: attempt to access length tester map via invalid key" << std::endl;);
-        }
-    }
-};
-
-class regex_automaton_under_assumptions {
-protected:
-    expr * re_term;
-    eautomaton * aut;
-    bool polarity;
-
-    bool assume_lower_bound;
-    rational lower_bound;
-
-    bool assume_upper_bound;
-    rational upper_bound;
-public:
-    regex_automaton_under_assumptions() :
-        re_term(nullptr), aut(nullptr), polarity(false),
-        assume_lower_bound(false), assume_upper_bound(false) {}
-
-    regex_automaton_under_assumptions(expr * re_term, eautomaton * aut, bool polarity) :
-        re_term(re_term), aut(aut), polarity(polarity),
-        assume_lower_bound(false), assume_upper_bound(false) {}
-
-    void set_lower_bound(rational & lb) {
-        lower_bound = lb;
-        assume_lower_bound = true;
-    }
-    void unset_lower_bound() {
-        assume_lower_bound = false;
-    }
-
-    void set_upper_bound(rational & ub) {
-        upper_bound = ub;
-        assume_upper_bound = true;
-    }
-    void unset_upper_bound() {
-        assume_upper_bound = false;
-    }
-
-    bool get_lower_bound(rational & lb) const {
-        if (assume_lower_bound) {
-            lb = lower_bound;
-            return true;
-        } else {
-            return false;
-        }
-    }
-
-    bool get_upper_bound(rational & ub) const {
-        if (assume_upper_bound) {
-            ub = upper_bound;
-            return true;
-        } else {
-            return false;
-        }
-    }
-
-    eautomaton * get_automaton() const { return aut; }
-    expr * get_regex_term() const { return re_term; }
-    bool get_polarity() const { return polarity; }
-};
-
-class char_union_find {
-    unsigned_vector   m_find;
-    unsigned_vector   m_size;
-    unsigned_vector   m_next;
-
-    integer_set char_const_set;
-
-    u_map<svector<expr*> > m_justification; // representative -> list of formulas justifying EQC
-
-    void ensure_size(unsigned v) {
-        while (v >= get_num_vars()) {
-            mk_var();
-        }
-    }
- public:
-    unsigned mk_var() {
-        unsigned r = m_find.size();
-        m_find.push_back(r);
-        m_size.push_back(1);
-        m_next.push_back(r);
-        return r;
-    }
-    unsigned get_num_vars() const { return m_find.size(); }
-    void mark_as_char_const(unsigned r) {
-        char_const_set.insert((int)r);
-    }
-    bool is_char_const(unsigned r) {
-        return char_const_set.contains((int)r);
-    }
-
-    unsigned find(unsigned v) const {
-        if (v >= get_num_vars()) {
-            return v;
-        }
-        while (true) {
-            unsigned new_v = m_find[v];
-            if (new_v == v)
-                return v;
-            v = new_v;
-        }
-    }
-
-    unsigned next(unsigned v) const {
-        if (v >= get_num_vars()) {
-            return v;
-        }
-        return m_next[v];
-    }
-
-    bool is_root(unsigned v) const {
-        return v >= get_num_vars() || m_find[v] == v;
-    }
-
-    svector<expr*> get_justification(unsigned v) {
-        unsigned r = find(v);
-        svector<expr*> retval;
-        if (m_justification.find(r, retval)) {
-            return retval;
-        } else {
-            return svector<expr*>();
-        }
-    }
-
-    void merge(unsigned v1, unsigned v2, expr * justification) {
-        unsigned r1 = find(v1);
-        unsigned r2 = find(v2);
-        if (r1 == r2)
-            return;
-        ensure_size(v1);
-        ensure_size(v2);
-        // swap r1 and r2 if:
-        // 1. EQC of r1 is bigger than EQC of r2
-        // 2. r1 is a character constant and r2 is not.
-        // this maintains the invariant that if a character constant is in an eqc then it is the root of that eqc
-        if (m_size[r1] > m_size[r2] || (is_char_const(r1) && !is_char_const(r2))) {
-            std::swap(r1, r2);
-        }
-        m_find[r1] = r2;
-        m_size[r2] += m_size[r1];
-        std::swap(m_next[r1], m_next[r2]);
-
-        if (m_justification.contains(r1)) {
-            // add r1's justifications to r2
-            if (!m_justification.contains(r2)) {
-                m_justification.insert(r2, m_justification[r1]);
-            } else {
-                m_justification[r2].append(m_justification[r1]);
-            }
-            m_justification.remove(r1);
-        }
-        if (justification != nullptr) {
-            if (!m_justification.contains(r2)) {
-                m_justification.insert(r2, svector<expr*>());
-            }
-            m_justification[r2].push_back(justification);
-        }
-    }
-
-    void reset() {
-        m_find.reset();
-        m_next.reset();
-        m_size.reset();
-        char_const_set.reset();
-        m_justification.reset();
-    }
-};
-
-class theory_str : public theory {
-    struct T_cut
-    {
-        int level;
-        obj_map<expr, int> vars;
-
-        T_cut() {
-            level = -100;
-        }
-    };
-
-    typedef union_find<theory_str> th_union_find;
-
-    typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map;
-    struct zstring_hash_proc {
-        unsigned operator()(zstring const & s) const {
-            auto str = s.encode();
-            return string_hash(str.c_str(), static_cast<unsigned>(s.length()), 17);
-        }
-    };
-    typedef map<zstring, expr*, zstring_hash_proc, default_eq<zstring> > string_map;
-
-    struct stats {
-        stats() { reset(); }
-        void reset() { memset(this, 0, sizeof(stats)); }
-        unsigned m_refine_eq;
-        unsigned m_refine_neq;
-        unsigned m_refine_f;
-        unsigned m_refine_nf;
-        unsigned m_solved_by;
-        unsigned m_fixed_length_iterations;
-    };
-
-protected:
-    theory_str_params const & m_params;
-
-    /*
-     * Setting EagerStringConstantLengthAssertions to true allows some methods,
-     * in particular internalize_term(), to add
-     * length assertions about relevant string constants.
-     * Note that currently this should always be set to 'true', or else *no* length assertions
-     * will be made about string constants.
-     */
-    bool opt_EagerStringConstantLengthAssertions;
-
-    /*
-     * If VerifyFinalCheckProgress is set to true, continuing after final check is invoked
-     * without asserting any new axioms is considered a bug and will throw an exception.
-     */
-    bool opt_VerifyFinalCheckProgress;
-
-    /*
-     * This constant controls how eagerly we expand unrolls in unbounded regex membership tests.
-     */
-    int opt_LCMUnrollStep;
-
-    /*
-     * If NoQuickReturn_IntegerTheory is set to true,
-     * integer theory integration checks that assert axioms
-     * will not return from the function after asserting their axioms.
-     * The default behaviour of Z3str2 is to set this to 'false'. This may be incorrect.
-     */
-    bool opt_NoQuickReturn_IntegerTheory;
-
-    /*
-     * If DisableIntegerTheoryIntegration is set to true,
-     * ALL calls to the integer theory integration methods
-     * (get_arith_value, get_len_value, lower_bound, upper_bound)
-     * will ignore what the arithmetic solver believes about length terms,
-     * and will return no information.
-     *
-     * This reduces performance significantly, but can be useful to enable
-     * if it is suspected that string-integer integration, or the arithmetic solver itself,
-     * might have a bug.
-     *
-     * The default behaviour of Z3str2 is to set this to 'false'.
-     */
-    bool opt_DisableIntegerTheoryIntegration;
-
-    /*
-     * If DeferEQCConsistencyCheck is set to true,
-     * expensive calls to new_eq_check() will be deferred until final check,
-     * at which time the consistency of *all* string equivalence classes will be validated.
-     */
-    bool opt_DeferEQCConsistencyCheck;
-
-    /*
-     * If CheckVariableScope is set to true,
-     * pop_scope_eh() and final_check_eh() will run extra checks
-     * to determine whether the current assignment
-     * contains references to any internal variables that are no longer in scope.
-     */
-    bool opt_CheckVariableScope;
-
-    /*
-     * If ConcatOverlapAvoid is set to true,
-     * the check to simplify Concat = Concat in handle_equality() will
-     * avoid simplifying wrt. pairs of Concat terms that will immediately
-     * result in an overlap. (false = Z3str2 behaviour)
-     */
-    bool opt_ConcatOverlapAvoid;
-
-    bool search_started;
-    arith_util m_autil;
-    seq_util u;
-    int sLevel;
-
-    bool finalCheckProgressIndicator;
-
-    expr_ref_vector m_trail; // trail for generated terms
-
-    str_value_factory * m_factory;
-
-    re2automaton m_mk_aut;
-
-    // Unique identifier appended to unused variables to ensure that model construction
-    // does not introduce equalities when they weren't enforced.
-    unsigned m_unused_id;
-
-    const char* newOverlapStr = "!!NewOverlapAssumption!!";
-
-    // terms we couldn't go through set_up_axioms() with because they weren't internalized
-    expr_ref_vector m_delayed_axiom_setup_terms;
-
-    ptr_vector<enode> m_basicstr_axiom_todo;
-    ptr_vector<enode> m_concat_axiom_todo;
-    ptr_vector<enode> m_string_constant_length_todo;
-    ptr_vector<enode> m_concat_eval_todo;
-    expr_ref_vector m_delayed_assertions_todo;
-
-    // enode lists for library-aware/high-level string terms (e.g. substr, contains)
-    ptr_vector<enode> m_library_aware_axiom_todo;
-
-    // list of axioms that are re-asserted every time the scope is popped
-    expr_ref_vector m_persisted_axioms;
-    expr_ref_vector m_persisted_axiom_todo;
-
-    // hashtable of all exprs for which we've already set up term-specific axioms --
-    // this prevents infinite recursive descent with respect to axioms that
-    // include an occurrence of the term for which axioms are being generated
-    obj_hashtable<expr> axiomatized_terms;
-
-    // hashtable of all top-level exprs for which set_up_axioms() has been called
-    obj_hashtable<expr> existing_toplevel_exprs;
-
-    int tmpStringVarCount;
-    int tmpXorVarCount;
-    // obj_pair_map<expr, expr, std::map<int, expr*> > varForBreakConcat;
-    std::map<std::pair<expr*,expr*>, std::map<int, expr*> > varForBreakConcat;
-    bool avoidLoopCut;
-    bool loopDetected;
-    obj_map<expr, std::stack<T_cut*> > cut_var_map;
-    scoped_ptr_vector<T_cut> m_cut_allocs;
-    expr_ref m_theoryStrOverlapAssumption_term;
-
-    obj_hashtable<expr> variable_set;
-    obj_hashtable<expr> internal_variable_set;
-    std::map<int, obj_hashtable<expr> > internal_variable_scope_levels;
-
-    expr_ref_vector contains_map;
-
-    theory_str_contain_pair_bool_map_t contain_pair_bool_map;
-    obj_map<expr, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
-
-    // regex automata
-    scoped_ptr_vector<eautomaton> m_automata;
-    ptr_vector<eautomaton> regex_automata;
-    obj_hashtable<expr> regex_terms;
-    obj_map<expr, ptr_vector<expr> > regex_terms_by_string; // S --> [ (str.in.re S *) ]
-    obj_map<expr, svector<regex_automaton_under_assumptions> > regex_automaton_assumptions; // RegEx --> [ aut+assumptions ]
-    obj_hashtable<expr> regex_terms_with_path_constraints; // set of string terms which have had path constraints asserted in the current scope
-    obj_hashtable<expr> regex_terms_with_length_constraints; // set of regex terms which had had length constraints asserted in the current scope
-    obj_map<expr, expr*> regex_term_to_length_constraint; // (str.in.re S R) -> (length constraint over S wrt. R)
-    obj_map<expr, ptr_vector<expr> > regex_term_to_extra_length_vars; // extra length vars used in regex_term_to_length_constraint entries
-
-    // keep track of the last lower/upper bound we saw for each string term
-    // so we don't perform duplicate work
-    obj_map<expr, rational> regex_last_lower_bound;
-    obj_map<expr, rational> regex_last_upper_bound;
-
-    // each counter maps a (str.in.re) expression to an integer.
-    // use helper functions regex_inc_counter() and regex_get_counter() to access
-    obj_map<expr, unsigned> regex_length_attempt_count;
-    obj_map<expr, unsigned> regex_fail_count;
-    obj_map<expr, unsigned> regex_intersection_fail_count;
-
-    obj_map<expr, ptr_vector<expr> > string_chars; // S --> [S_0, S_1, ...] for character terms S_i
-
-    obj_pair_map<expr, expr, expr*> concat_astNode_map;
-
-    // all (str.to-int) and (int.to-str) terms
-    expr_ref_vector string_int_conversion_terms;
-    obj_hashtable<expr> string_int_axioms;
-
-    string_map stringConstantCache;
-    unsigned long totalCacheAccessCount;
-    unsigned long cacheHitCount;
-    unsigned long cacheMissCount;
-
-    unsigned m_fresh_id;
-
-    // cache mapping each string S to Length(S)
-    obj_map<expr, app*> length_ast_map;
-
-    trail_stack m_trail_stack;
-    trail_stack m_library_aware_trail_stack;
-    th_union_find m_find;
-    theory_var get_var(expr * n) const;
-    expr * get_eqc_next(expr * n);
-    app * get_ast(theory_var i);
-
-    // fixed length model construction
-    expr_ref_vector fixed_length_subterm_trail; // trail for subterms generated *in the subsolver*
-    expr_ref_vector fixed_length_assumptions; // cache of boolean terms to assert *into the subsolver*, unsat core is a subset of these
-    obj_map<expr, rational> fixed_length_used_len_terms; // constraints used in generating fixed length model
-    obj_map<expr, expr_ref_vector* > var_to_char_subterm_map; // maps a var to a list of character terms *in the subsolver*
-    obj_map<expr, expr_ref_vector* > uninterpreted_to_char_subterm_map; // maps an "uninterpreted" string term to a list of character terms *in the subsolver*
-    obj_map<expr, std::tuple<rational, expr*, expr*>> fixed_length_lesson; //keep track of information for the lesson
-    unsigned preprocessing_iteration_count; // number of attempts we've made to solve by preprocessing length information
-    obj_map<expr, zstring> candidate_model;
-
-    stats m_stats;
-
-protected:
-    void reset_internal_data_structures();
-
-    void assert_axiom(expr * e);
-    void assert_implication(expr * premise, expr * conclusion);
-    expr * rewrite_implication(expr * premise, expr * conclusion);
-    // Use the rewriter to simplify an axiom, then assert it.
-    void assert_axiom_rw(expr * e);
-
-    expr * mk_string(zstring const& str);
-    expr * mk_string(const char * str);
-
-    app * mk_strlen(expr * e);
-    expr * mk_concat(expr * n1, expr * n2);
-    expr * mk_concat_const_str(expr * n1, expr * n2);
-    app * mk_contains(expr * haystack, expr * needle);
-    app * mk_indexof(expr * haystack, expr * needle);
-    app * mk_fresh_const(char const* name, sort* s);
-
-    literal mk_literal(expr* _e);
-    app * mk_int(int n);
-    app * mk_int(rational & q);
-
-    void check_and_init_cut_var(expr * node);
-    void add_cut_info_one_node(expr * baseNode, int slevel, expr * node);
-    void add_cut_info_merge(expr * destNode, int slevel, expr * srcNode);
-    bool has_self_cut(expr * n1, expr * n2);
-
-    // for ConcatOverlapAvoid
-    bool will_result_in_overlap(expr * lhs, expr * rhs);
-
-    void track_variable_scope(expr * var);
-    app * mk_str_var(std::string name);
-    app * mk_int_var(std::string name);
-    app_ref mk_nonempty_str_var();
-    app * mk_internal_xor_var();
-    void add_nonempty_constraint(expr * s);
-
-    void instantiate_concat_axiom(enode * cat);
-    void try_eval_concat(enode * cat);
-    void instantiate_basic_string_axioms(enode * str);
-    void instantiate_str_eq_length_axiom(enode * lhs, enode * rhs);
-
-    // for count abstraction and refinement
-    expr* refine(expr* lhs, expr* rhs, rational offset);
-    expr* refine_eq(expr* lhs, expr* rhs, unsigned offset);
-    expr* refine_dis(expr* lhs, expr* rhs);
-    expr* refine_function(expr* f);
-    bool flatten(expr* ex, expr_ref_vector & flat);
-    rational get_refine_length(expr* ex, expr_ref_vector& extra_deps);
-
-    void instantiate_axiom_CharAt(enode * e);
-    void instantiate_axiom_prefixof(enode * e);
-    void instantiate_axiom_suffixof(enode * e);
-    void instantiate_axiom_Contains(enode * e);
-    void instantiate_axiom_Indexof(enode * e);
-    void instantiate_axiom_Indexof_extended(enode * e);
-    void instantiate_axiom_LastIndexof(enode * e);
-    void instantiate_axiom_Substr(enode * e);
-    void instantiate_axiom_Replace(enode * e);
-    void instantiate_axiom_str_to_int(enode * e);
-    void instantiate_axiom_int_to_str(enode * e);
-    void instantiate_axiom_is_digit(enode * e);
-    void instantiate_axiom_str_to_code(enode * e);
-    void instantiate_axiom_str_from_code(enode * e);
-
-    void add_persisted_axiom(expr * a);
-
-    expr * mk_RegexIn(expr * str, expr * regexp);
-    void instantiate_axiom_RegexIn(enode * e);
-
-    // regex automata and length-aware regex
-    bool solve_regex_automata();
-    unsigned estimate_regex_complexity(expr * re);
-    unsigned estimate_regex_complexity_under_complement(expr * re);
-    unsigned estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2);
-    bool check_regex_length_linearity(expr * re);
-    bool check_regex_length_linearity_helper(expr * re, bool already_star);
-    expr_ref infer_all_regex_lengths(expr * lenVar, expr * re, expr_ref_vector & freeVariables);
-    void check_subterm_lengths(expr * re, integer_set & lens);
-    void find_automaton_initial_bounds(expr * str_in_re, eautomaton * aut);
-    bool refine_automaton_lower_bound(eautomaton * aut, rational current_lower_bound, rational & refined_lower_bound);
-    bool refine_automaton_upper_bound(eautomaton * aut, rational current_upper_bound, rational & refined_upper_bound);
-    expr_ref generate_regex_path_constraints(expr * stringTerm, eautomaton * aut, rational lenVal, expr_ref & characterConstraints);
-    void aut_path_add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned idx, expr* cond);
-    expr_ref aut_path_rewrite_constraint(expr * cond, expr * ch_var);
-    void regex_inc_counter(obj_map<expr, unsigned> & counter_map, expr * key);
-    unsigned regex_get_counter(obj_map<expr, unsigned> & counter_map, expr * key);
-
-    void set_up_axioms(expr * ex);
-    void handle_equality(expr * lhs, expr * rhs);
-
-    app * mk_value_helper(app * n);
-    expr * get_eqc_value(expr * n, bool & hasEqcValue);
-    bool get_string_constant_eqc(expr * n, zstring & stringVal);
-    expr * z3str2_get_eqc_value(expr * n , bool & hasEqcValue);
-    bool in_same_eqc(expr * n1, expr * n2);
-    expr * collect_eq_nodes(expr * n, expr_ref_vector & eqcSet);
-    bool is_var(expr * e) const;
-
-    bool get_arith_value(expr* e, rational& val) const;
-    bool get_len_value(expr* e, rational& val);
-    bool lower_bound(expr* _e, rational& lo);
-    bool upper_bound(expr* _e, rational& hi);
-
-    bool can_two_nodes_eq(expr * n1, expr * n2);
-    bool can_concat_eq_str(expr * concat, zstring& str);
-    bool can_concat_eq_concat(expr * concat1, expr * concat2);
-    bool check_concat_len_in_eqc(expr * concat);
-    void check_eqc_empty_string(expr * lhs, expr * rhs);
-    void check_eqc_concat_concat(std::set<expr*> & eqc_concat_lhs, std::set<expr*> & eqc_concat_rhs);
-    bool check_length_consistency(expr * n1, expr * n2);
-    bool check_length_const_string(expr * n1, expr * constStr);
-    bool check_length_eq_var_concat(expr * n1, expr * n2);
-    bool check_length_concat_concat(expr * n1, expr * n2);
-    bool check_length_concat_var(expr * concat, expr * var);
-    bool check_length_var_var(expr * var1, expr * var2);
-    void check_contain_in_new_eq(expr * n1, expr * n2);
-    void check_contain_by_eqc_val(expr * varNode, expr * constNode);
-    void check_contain_by_substr(expr * varNode, expr_ref_vector & willEqClass);
-    void check_contain_by_eq_nodes(expr * n1, expr * n2);
-    bool in_contain_idx_map(expr * n);
-    void compute_contains(std::map<expr*, expr*> & varAliasMap,
-            std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr *> & varConstMap,
-            std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap);
-    expr * dealias_node(expr * node, std::map<expr*, expr*> & varAliasMap, std::map<expr*, expr*> & concatAliasMap);
-    void get_grounded_concats(unsigned depth,
-                              expr* node, std::map<expr*, expr*> & varAliasMap,
-                              std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
-                              std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
-                              std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
-    void print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
-    void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar,
-            std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
-    bool is_partial_in_grounded_concat(const std::vector<expr*> & strVec, const std::vector<expr*> & subStrVec);
-
-    void get_nodes_in_concat(expr * node, ptr_vector<expr> & nodeList);
-    expr * simplify_concat(expr * node);
-
-    void simplify_parent(expr * nn, expr * eq_str);
-
-    void simplify_concat_equality(expr * lhs, expr * rhs);
-    void solve_concat_eq_str(expr * concat, expr * str);
-
-    void infer_len_concat_equality(expr * nn1, expr * nn2);
-    bool infer_len_concat(expr * n, rational & nLen);
-    void infer_len_concat_arg(expr * n, rational len);
-
-    bool is_concat_eq_type1(expr * concatAst1, expr * concatAst2);
-    bool is_concat_eq_type2(expr * concatAst1, expr * concatAst2);
-    bool is_concat_eq_type3(expr * concatAst1, expr * concatAst2);
-    bool is_concat_eq_type4(expr * concatAst1, expr * concatAst2);
-    bool is_concat_eq_type5(expr * concatAst1, expr * concatAst2);
-    bool is_concat_eq_type6(expr * concatAst1, expr * concatAst2);
-
-    void process_concat_eq_type1(expr * concatAst1, expr * concatAst2);
-    void process_concat_eq_type2(expr * concatAst1, expr * concatAst2);
-    void process_concat_eq_type3(expr * concatAst1, expr * concatAst2);
-    void process_concat_eq_type4(expr * concatAst1, expr * concatAst2);
-    void process_concat_eq_type5(expr * concatAst1, expr * concatAst2);
-    void process_concat_eq_type6(expr * concatAst1, expr * concatAst2);
-
-    void print_cut_var(expr * node, std::ofstream & xout);
-
-    void generate_mutual_exclusion(expr_ref_vector & exprs);
-    void add_theory_aware_branching_info(expr * term, double priority, lbool phase);
-
-    bool new_eq_check(expr * lhs, expr * rhs);
-    void group_terms_by_eqc(expr * n, std::set<expr*> & concats, std::set<expr*> & vars, std::set<expr*> & consts);
-
-    void check_consistency_prefix(expr * e, bool is_true);
-    void check_consistency_suffix(expr * e, bool is_true);
-    void check_consistency_contains(expr * e, bool is_true);
-
-    int ctx_dep_analysis(std::map<expr*, int> & strVarMap, std::map<expr*, int> & freeVarMap,
-            std::map<expr*, std::map<expr*, int> > & var_eq_concat_map);
-    void trace_ctx_dep(std::ofstream & tout,
-            std::map<expr*, expr*> & aliasIndexMap,
-            std::map<expr*, expr*> & var_eq_constStr_map,
-            std::map<expr*, std::map<expr*, int> > & var_eq_concat_map,
-            std::map<expr*, std::map<expr*, int> > & var_eq_unroll_map,
-            std::map<expr*, expr*> & concat_eq_constStr_map,
-            std::map<expr*, std::map<expr*, int> > & concat_eq_concat_map);
-
-    bool term_appears_as_subterm(expr * needle, expr * haystack);
-    void classify_ast_by_type(expr * node, std::map<expr*, int> & varMap,
-            std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap);
-    void classify_ast_by_type_in_positive_context(std::map<expr*, int> & varMap,
-            std::map<expr*, int> & concatMap, std::map<expr*, int> & unrollMap);
-
-    expr * get_alias_index_ast(std::map<expr*, expr*> & aliasIndexMap, expr * node);
-    expr * getMostLeftNodeInConcat(expr * node);
-    expr * getMostRightNodeInConcat(expr * node);
-    void get_var_in_eqc(expr * n, std::set<expr*> & varSet);
-    void get_concats_in_eqc(expr * n, std::set<expr*> & concats);
-    void get_const_str_asts_in_node(expr * node, expr_ref_vector & constList);
-    expr * eval_concat(expr * n1, expr * n2);
-
-    bool finalcheck_str2int(app * a);
-    bool finalcheck_int2str(app * a);
-    bool string_integer_conversion_valid(zstring str, rational& converted) const;
-
-    lbool fixed_length_model_construction(expr_ref_vector formulas, expr_ref_vector &precondition,
-            expr_ref_vector& free_variables,
-            obj_map<expr, zstring> &model, expr_ref_vector &cex);
-    bool fixed_length_reduce_string_term(smt::kernel & subsolver, expr * term, expr_ref_vector & term_chars, expr_ref & cex);
-    bool fixed_length_get_len_value(expr * e, rational & val);
-    bool fixed_length_reduce_eq(smt::kernel & subsolver, expr_ref lhs, expr_ref rhs, expr_ref & cex);
-    bool fixed_length_reduce_diseq(smt::kernel & subsolver, expr_ref lhs, expr_ref rhs, expr_ref & cex);
-    bool fixed_length_reduce_contains(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
-    bool fixed_length_reduce_negative_contains(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
-    bool fixed_length_reduce_prefix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
-    bool fixed_length_reduce_negative_prefix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
-    bool fixed_length_reduce_suffix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
-    bool fixed_length_reduce_negative_suffix(smt::kernel & subsolver, expr_ref f, expr_ref & cex);
-    bool fixed_length_reduce_regex_membership(smt::kernel & subsolver, expr_ref f, expr_ref & cex, bool polarity);
-
-    void dump_assignments();
-
-    void check_variable_scope();
-    void recursive_check_variable_scope(expr * ex);
-
-    void collect_var_concat(expr * node, std::set<expr*> & varSet, std::set<expr*> & concatSet);
-    bool propagate_length(std::set<expr*> & varSet, std::set<expr*> & concatSet, std::map<expr*, int> & exprLenMap);
-    void get_unique_non_concat_nodes(expr * node, std::set<expr*> & argSet);
-    bool propagate_length_within_eqc(expr * var);
-
-
-    const rational NEQ = rational(-1); // negative word equation lesson
-    const rational PFUN = rational(-2); // positive function lesson
-    const rational NFUN = rational(-3); // negative function lesson
-
-    // TESTING
-    void refresh_theory_var(expr * e);
-
-public:
-    theory_str(context& ctx, ast_manager & m, theory_str_params const & params);
-    ~theory_str() override;
-
-    char const * get_name() const override { return "seq"; }
-    void init() override;
-    void display(std::ostream & out) const override;
-
-    void collect_statistics(::statistics & st) const override;
-
-    bool overlapping_variables_detected() const { return loopDetected; }
-
-    trail_stack& get_trail_stack() { return m_trail_stack; }
-    void merge_eh(theory_var, theory_var, theory_var v1, theory_var v2) {}
-    void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) { }
-    void unmerge_eh(theory_var v1, theory_var v2) {}
-protected:
-    bool internalize_atom(app * atom, bool gate_ctx) override;
-    bool internalize_term(app * term) override;
-    virtual enode* ensure_enode(expr* e);
-    theory_var mk_var(enode * n) override;
-
-    void new_eq_eh(theory_var, theory_var) override;
-    void new_diseq_eh(theory_var, theory_var) override;
-
-    theory* mk_fresh(context* c) override { return alloc(theory_str, *c, c->get_manager(), m_params); }
-    void init_search_eh() override;
-    void add_theory_assumptions(expr_ref_vector & assumptions) override;
-    lbool validate_unsat_core(expr_ref_vector & unsat_core) override;
-    void relevant_eh(app * n) override;
-    void assign_eh(bool_var v, bool is_true) override;
-    void push_scope_eh() override;
-    void pop_scope_eh(unsigned num_scopes) override;
-    void reset_eh() override;
-
-    bool can_propagate() override;
-    void propagate() override;
-
-    final_check_status final_check_eh() override;
-    virtual void attach_new_th_var(enode * n);
-
-    void init_model(model_generator & m) override;
-    model_value_proc * mk_value(enode * n, model_generator & mg) override;
-    void finalize_model(model_generator & mg) override;
-};
-
-};

src/smt/theory_user_propagator.cpp

@@ -110,6 +110,15 @@ void theory_user_propagator::register_cb(expr* e) {
         add_expr(e, true);
 }
 
+void theory_user_propagator::register_on_binding(user_propagator::binding_eh_t& binding_eh) {
+    std::function<bool(quantifier* q, expr* inst)> on_binding = 
+        [this, binding_eh](quantifier* q, expr* inst) {
+            return binding_eh(m_user_context, this, q, inst);
+        };    
+    ctx.register_on_binding(on_binding);
+
+}
+
 bool theory_user_propagator::next_split_cb(expr* e, unsigned idx, lbool phase) {
     if (e == nullptr) { // clear
         m_next_split_var = nullptr;

src/smt/theory_user_propagator.h

@@ -132,6 +132,7 @@ namespace smt {
         void register_diseq(user_propagator::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; }
         void register_created(user_propagator::created_eh_t& created_eh) { m_created_eh = created_eh; }
         void register_decide(user_propagator::decide_eh_t& decide_eh) { m_decide_eh = decide_eh; }
+        void register_on_binding(user_propagator::binding_eh_t& binding_eh);
 
         bool has_fixed() const { return (bool)m_fixed_eh; }
         

src/solver/combined_solver.cpp

@@ -380,6 +380,10 @@ public:
         m_solver2->user_propagate_register_diseq(diseq_eh);
     }
 
+    void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh) override {
+        m_solver2->user_propagate_register_on_binding(binding_eh);
+    }
+    
     void user_propagate_register_expr(expr* e) override {
         m_solver2->user_propagate_register_expr(e);
     }

src/solver/simplifier_solver.cpp

@@ -388,6 +388,9 @@ public:
     void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { s->user_propagate_register_final(final_eh); }
     void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { s->user_propagate_register_eq(eq_eh); }    
     void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { s->user_propagate_register_diseq(diseq_eh); } 
+    void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh) override { 
+        s->user_propagate_register_on_binding(binding_eh); 
+    }
     void user_propagate_register_expr(expr* e) override { m_preprocess_state.freeze(e);  s->user_propagate_register_expr(e); }
     void user_propagate_register_created(user_propagator::created_eh_t& r) override { s->user_propagate_register_created(r); }
     void user_propagate_register_decide(user_propagator::decide_eh_t& r) override { s->user_propagate_register_decide(r); }

src/solver/slice_solver.cpp

@@ -416,6 +416,7 @@ public:
     void user_propagate_register_final(user_propagator::final_eh_t& final_eh) override { s->user_propagate_register_final(final_eh); }
     void user_propagate_register_eq(user_propagator::eq_eh_t& eq_eh) override { s->user_propagate_register_eq(eq_eh); }    
     void user_propagate_register_diseq(user_propagator::eq_eh_t& diseq_eh) override { s->user_propagate_register_diseq(diseq_eh); } 
+    void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh) override { s->user_propagate_register_on_binding(binding_eh); }
     void user_propagate_register_expr(expr* e) override { s->user_propagate_register_expr(e); }
     void user_propagate_register_created(user_propagator::created_eh_t& r) override { s->user_propagate_register_created(r); }
     void user_propagate_register_decide(user_propagator::decide_eh_t& r) override { s->user_propagate_register_decide(r); }

src/solver/tactic2solver.cpp

@@ -115,6 +115,10 @@ public:
         m_tactic->user_propagate_register_diseq(diseq_eh);
     }
 
+    void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh) override {
+        m_tactic->user_propagate_register_on_binding(binding_eh);
+    }
+
     void user_propagate_register_expr(expr* e) override {
         m_tactic->user_propagate_register_expr(e);
     }

src/tactic/dependent_expr_state_tactic.h

@@ -168,6 +168,7 @@ public:
         m_frozen.push_back(e);
     }
 
+
     void user_propagate_clear() override {
         if (m_simp) {
             pop(1);

src/tactic/tactical.cpp

@@ -200,6 +200,10 @@ public:
         m_t2->user_propagate_register_diseq(diseq_eh);
     }
 
+    void user_propagate_register_on_binding(user_propagator::binding_eh_t& binding_eh) override {
+        m_t2->user_propagate_register_on_binding(binding_eh);
+    }
+
     void user_propagate_register_expr(expr* e) override {
         m_t1->user_propagate_register_expr(e);
         m_t2->user_propagate_register_expr(e);

src/tactic/user_propagator_base.h

@@ -28,6 +28,7 @@ namespace user_propagator {
     typedef std::function<void(void*, callback*, expr*)>                     created_eh_t;
     typedef std::function<void(void*, callback*, expr*, unsigned, bool)>     decide_eh_t;
     typedef std::function<void(void*, expr*, unsigned, unsigned const*, unsigned, expr* const*)>        on_clause_eh_t;
+    typedef std::function<bool(void*, callback*, expr*, expr*)>              binding_eh_t;
 
     class plugin : public decl_plugin {
     public:
@@ -92,6 +93,10 @@ namespace user_propagator {
             throw default_exception("user-propagators are only supported on the SMT solver");
         }
 
+        virtual void user_propagate_register_on_binding(binding_eh_t& r) {
+            throw default_exception("user-propagators are only supported on the SMT solver");
+        }
+
         virtual void user_propagate_clear() {
         }
 

src/test/sat_local_search.cpp

@@ -122,7 +122,7 @@ void tst_sat_local_search(char ** argv, int argc, int& i) {
     // set up cancellation/timeout environment.
 
     cancel_eh<reslimit> eh(local_search.rlimit());
-    scoped_ctrl_c ctrlc(eh, false, true);
+    scoped_ctrl_c ctrlc(eh);
     scoped_timer timer(cutoff_time*1000, &eh);        
     local_search.check(0, nullptr, nullptr);    
 

src/util/cancel_eh.h

@@ -18,6 +18,8 @@ Revision History:
 --*/
 #pragma once
 
+#include <atomic>
+#include <mutex>
 #include "util/event_handler.h"
 
 /**
@@ -25,22 +27,29 @@ Revision History:
 */
 template<typename T>
 class cancel_eh : public event_handler {
-    bool m_canceled = false;
+    std::mutex m_mutex;
+    std::atomic<bool> m_canceled = false;
     bool m_auto_cancel = false;
     T & m_obj;
 public:
     cancel_eh(T & o): m_obj(o) {}
     ~cancel_eh() override { if (m_canceled) m_obj.dec_cancel(); if (m_auto_cancel) m_obj.auto_cancel(); }
+
+    // Note that this method doesn't race with the destructor since
+    // potential callers like scoped_ctrl_c/scoped_timer are destroyed
+    // before the cancel_eh destructor is invoked.
+    // Thus, the only races are with itself and with the getters.
     void operator()(event_handler_caller_t caller_id) override {
+        std::lock_guard lock(m_mutex);
         if (!m_canceled) {
             m_caller_id = caller_id;
-            m_canceled = true;
             m_obj.inc_cancel();
+            m_canceled = true;
         }
     }
+
     bool canceled() const { return m_canceled; }
     void reset() { m_canceled = false; }
     T& t() { return m_obj; }
     void set_auto_cancel() { m_auto_cancel = true; }
 };
-

src/util/scoped_ctrl_c.cpp

@@ -16,45 +16,49 @@ Author:
 Revision History:
 
 --*/
-#include<signal.h>
+#include <mutex>
+#include <vector>
+#include <signal.h>
 #include "util/scoped_ctrl_c.h"
 #include "util/gparams.h"
 
-static scoped_ctrl_c * g_obj = nullptr;
+static std::vector<scoped_ctrl_c*> g_list;
+static std::mutex g_list_mutex;
+static void (*g_old_handler)(int);
 
 static void on_ctrl_c(int) {
-    if (g_obj->m_first) {
+    std::lock_guard lock(g_list_mutex);
-        g_obj->m_cancel_eh(CTRL_C_EH_CALLER);
+    for (auto handler : g_list) {
-        if (g_obj->m_once) {
+        if (handler->m_enabled) {
-            g_obj->m_first = false;
+            handler->m_cancel_eh(CTRL_C_EH_CALLER);
-            signal(SIGINT, on_ctrl_c); // re-install the handler
         }
     }
-    else {
+    signal(SIGINT, g_old_handler);
-        signal(SIGINT, g_obj->m_old_handler); 
-        raise(SIGINT);
-    }
 }
 
-scoped_ctrl_c::scoped_ctrl_c(event_handler & eh, bool once, bool enabled):
+scoped_ctrl_c::scoped_ctrl_c(event_handler & eh, bool enabled):
     m_cancel_eh(eh),
-    m_first(true),
+    m_enabled(enabled) {
-    m_once(once),
+    if (enabled && gparams::get_value("ctrl_c") == "false")
-    m_enabled(enabled),
-    m_old_scoped_ctrl_c(g_obj) {
-    if (gparams::get_value("ctrl_c") == "false")
         m_enabled = false;
+
     if (m_enabled) {
-        g_obj = this;
+        std::lock_guard lock(g_list_mutex);
-        m_old_handler = signal(SIGINT, on_ctrl_c); 
+        if (g_list.empty()) {
+            g_old_handler = signal(SIGINT, on_ctrl_c);
+        }
+        g_list.push_back(this);
     }
 }
 
 scoped_ctrl_c::~scoped_ctrl_c() { 
     if (m_enabled) {
-        g_obj = m_old_scoped_ctrl_c;
+        std::lock_guard lock(g_list_mutex);
-        if (m_old_handler != SIG_ERR) {
+        auto it = std::find(g_list.begin(), g_list.end(), this);
-            signal(SIGINT, m_old_handler);
+        SASSERT(it != g_list.end());
+        g_list.erase(it);
+        if (g_list.empty()) {
+            signal(SIGINT, g_old_handler);
         }
     }
 }

src/util/scoped_ctrl_c.h

@@ -23,17 +23,9 @@ Revision History:
 
 struct scoped_ctrl_c {
     event_handler & m_cancel_eh;
-    bool m_first;
-    bool m_once;
     bool m_enabled;
-    void  (STD_CALL *m_old_handler)(int);
-    scoped_ctrl_c * m_old_scoped_ctrl_c;
 public:
-    // If once == true, then the cancel_eh is invoked only at the first Ctrl-C.
-    // The next time, the old signal handler will take over.
     // if enabled == false, then scoped_ctrl_c is a noop
-    scoped_ctrl_c(event_handler & eh, bool once=true, bool enabled=true);
+    scoped_ctrl_c(event_handler & eh, bool enabled = true);
     ~scoped_ctrl_c();
-    void reset() { m_first = true; }
 };
-