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

examples/python/mus/mss.py

@@ -73,6 +73,10 @@ class MSSSolver:
              self.varcache[i] = Not(v)
        return self.varcache[i]
 
+   # Retrieve the latest model
+   # Add formulas that are true in the model to 
+   # the current mss
+
    def update_unknown(self):
        self.model = self.s.model()
        new_unknown = set([])
@@ -83,23 +87,29 @@ class MSSSolver:
               new_unknown.add(x)
        self.unknown = new_unknown
       
-   def relax_core(self, core):
+   # Create a name, propositional atom,
-       assert(core <= self.soft_vars)
+   #  for formula 'fml' and return the name.
-       prev = BoolVal(True)
+
-       core_list = [x for x in core]
+   def add_def(self, fml):
-       self.soft_vars -= core
+       name = Bool("%s" % fml)
-       # replace x0, x1, x2, .. by
+       self.s.add(name == fml)
-       # Or(x1, x0), Or(x2, And(x1, x0)), Or(x3, And(x2, And(x1, x0))), ...
+       return name
-       for i in range(len(core_list)-1):
+
-           x = core_list[i]
+   # replace Fs := f0, f1, f2, .. by
-           y = core_list[i+1]
+   # Or(f1, f0), Or(f2, And(f1, f0)), Or(f3, And(f2, And(f1, f0))), ...
-           prevf = And(x, prev)
+
-           prev = Bool("%s" % prevf)
+   def relax_core(self, Fs):
-           self.s.add(prev == prevf)
+       assert(Fs <= self.soft_vars)
-           zf = Or(prev, y)
+       prefix = BoolVal(True)
-           z = Bool("%s" % zf)
+       self.soft_vars -= Fs
-           self.s.add(z == zf)
+       Fs = [ f for f in Fs ]
-           self.soft_vars.add(z)
+       for i in range(len(Fs)-1):
+           prefix = self.add_def(And(Fs[i], prefix))
+           self.soft_vars.add(self.add_def(Or(prefix, Fs[i+1])))
+
+   # Resolve literals from the core that 
+   # are 'explained', e.g., implied by 
+   # other literals.
 
    def resolve_core(self, core):
        new_core = set([])
@@ -111,6 +121,14 @@ class MSSSolver:
        return new_core
 
 
+   # Given a current satisfiable state
+   # Extract an MSS, and ensure that currently 
+   # encoutered cores are avoided in next iterations
+   # by weakening the set of literals that are
+   # examined in next iterations.
+   # Strengthen the solver state by enforcing that
+   # an element from the MCS is encoutered.
+
    def grow(self):
        self.mss = []
        self.mcs = []

src/api/api_context.cpp

@@ -415,6 +415,7 @@ extern "C" {
             return;
         }
         mk_c(c)->m().dec_ref(to_ast(a));
+
         Z3_CATCH;
     }
 

src/api/dotnet/Context.cs

@@ -286,8 +286,8 @@ namespace Microsoft.Z3
             Contract.Ensures(Contract.Result<TupleSort>() != null);
 
             CheckContextMatch(name);
-            CheckContextMatch(fieldNames);
+            CheckContextMatch<Symbol>(fieldNames);
-            CheckContextMatch(fieldSorts);
+            CheckContextMatch<Sort>(fieldSorts);
             return new TupleSort(this, name, (uint)fieldNames.Length, fieldNames, fieldSorts);
         }
 
@@ -303,7 +303,7 @@ namespace Microsoft.Z3
             Contract.Ensures(Contract.Result<EnumSort>() != null);
 
             CheckContextMatch(name);
-            CheckContextMatch(enumNames);
+            CheckContextMatch<Symbol>(enumNames);
             return new EnumSort(this, name, enumNames);
         }
 
@@ -423,7 +423,7 @@ namespace Microsoft.Z3
             Contract.Ensures(Contract.Result<DatatypeSort>() != null);
 
             CheckContextMatch(name);
-            CheckContextMatch(constructors);
+            CheckContextMatch<Constructor>(constructors);
             return new DatatypeSort(this, name, constructors);
         }
 
@@ -436,7 +436,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(constructors, c => c != null));
             Contract.Ensures(Contract.Result<DatatypeSort>() != null);
 
-            CheckContextMatch(constructors);
+            CheckContextMatch<Constructor>(constructors);
             return new DatatypeSort(this, MkSymbol(name), constructors);
         }
 
@@ -454,7 +454,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(names, name => name != null));
             Contract.Ensures(Contract.Result<DatatypeSort[]>() != null);
 
-            CheckContextMatch(names);
+            CheckContextMatch<Symbol>(names);
             uint n = (uint)names.Length;
             ConstructorList[] cla = new ConstructorList[n];
             IntPtr[] n_constr = new IntPtr[n];
@@ -462,7 +462,7 @@ namespace Microsoft.Z3
             {
                 Constructor[] constructor = c[i];
                 Contract.Assume(Contract.ForAll(constructor, arr => arr != null), "Clousot does not support yet quantified formula on multidimensional arrays");
-                CheckContextMatch(constructor);
+                CheckContextMatch<Constructor>(constructor);
                 cla[i] = new ConstructorList(this, constructor);
                 n_constr[i] = cla[i].NativeObject;
             }
@@ -520,7 +520,7 @@ namespace Microsoft.Z3
             Contract.Ensures(Contract.Result<FuncDecl>() != null);
 
             CheckContextMatch(name);
-            CheckContextMatch(domain);
+            CheckContextMatch<Sort>(domain);
             CheckContextMatch(range);
             return new FuncDecl(this, name, domain, range);
         }
@@ -551,7 +551,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(domain, d => d != null));
             Contract.Ensures(Contract.Result<FuncDecl>() != null);
 
-            CheckContextMatch(domain);
+            CheckContextMatch<Sort>(domain);
             CheckContextMatch(range);
             return new FuncDecl(this, MkSymbol(name), domain, range);
         }
@@ -582,7 +582,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(domain, d => d != null));
             Contract.Ensures(Contract.Result<FuncDecl>() != null);
 
-            CheckContextMatch(domain);
+            CheckContextMatch<Sort>(domain);
             CheckContextMatch(range);
             return new FuncDecl(this, prefix, domain, range);
         }
@@ -811,7 +811,7 @@ namespace Microsoft.Z3
             Contract.Ensures(Contract.Result<Expr>() != null);
 
             CheckContextMatch(f);
-            CheckContextMatch(args);
+            CheckContextMatch<Expr>(args);
             return Expr.Create(this, f, args);
         }
 
@@ -884,7 +884,7 @@ namespace Microsoft.Z3
 
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
 
-            CheckContextMatch(args);
+            CheckContextMatch<Expr>(args);
             return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
         }
 
@@ -970,7 +970,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(t, a => a != null));
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
 
-            CheckContextMatch(t);
+            CheckContextMatch<BoolExpr>(t);
             return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
@@ -982,7 +982,7 @@ namespace Microsoft.Z3
             Contract.Requires(t != null);
             Contract.Requires(Contract.ForAll(t, a => a != null));
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
-            CheckContextMatch(t);
+            CheckContextMatch<BoolExpr>(t);
             return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
         }
 
@@ -995,7 +995,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(t, a => a != null));
             Contract.Ensures(Contract.Result<BoolExpr>() != null);
 
-            CheckContextMatch(t);
+            CheckContextMatch<BoolExpr>(t);
             return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
@@ -1025,7 +1025,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(t, a => a != null));
             Contract.Ensures(Contract.Result<ArithExpr>() != null);
 
-            CheckContextMatch(t);
+            CheckContextMatch<ArithExpr>(t);
             return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
@@ -1051,7 +1051,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(t, a => a != null));
             Contract.Ensures(Contract.Result<ArithExpr>() != null);
 
-            CheckContextMatch(t);
+            CheckContextMatch<ArithExpr>(t);
             return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
@@ -1064,7 +1064,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(t, a => a != null));
             Contract.Ensures(Contract.Result<ArithExpr>() != null);
 
-            CheckContextMatch(t);
+            CheckContextMatch<ArithExpr>(t);
             return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)t.Count(), AST.EnumToNative(t)));
         }
 
@@ -1077,7 +1077,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(t, a => a != null));
             Contract.Ensures(Contract.Result<ArithExpr>() != null);
 
-            CheckContextMatch(t);
+            CheckContextMatch<ArithExpr>(t);
             return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
@@ -2205,7 +2205,7 @@ namespace Microsoft.Z3
             Contract.Ensures(Contract.Result<ArrayExpr>() != null);
 
             CheckContextMatch(f);
-            CheckContextMatch(args);
+            CheckContextMatch<ArrayExpr>(args);
             return (ArrayExpr)Expr.Create(this, Native.Z3_mk_map(nCtx, f.NativeObject, AST.ArrayLength(args), AST.ArrayToNative(args)));
         }
 
@@ -2315,7 +2315,7 @@ namespace Microsoft.Z3
             Contract.Requires(args != null);
             Contract.Requires(Contract.ForAll(args, a => a != null));
 
-            CheckContextMatch(args);
+            CheckContextMatch<ArrayExpr>(args);
             return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
         }
 
@@ -2328,7 +2328,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(args, a => a != null));
             Contract.Ensures(Contract.Result<Expr>() != null);
 
-            CheckContextMatch(args);
+            CheckContextMatch<ArrayExpr>(args);
             return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
         }
 
@@ -2429,7 +2429,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(t, a => a != null));
             Contract.Ensures(Contract.Result<SeqExpr>() != null);
 
-            CheckContextMatch(t);
+            CheckContextMatch<SeqExpr>(t);
             return new SeqExpr(this, Native.Z3_mk_seq_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
@@ -2593,7 +2593,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(t, a => a != null));
             Contract.Ensures(Contract.Result<ReExpr>() != null);
 
-            CheckContextMatch(t);
+            CheckContextMatch<ReExpr>(t);
             return new ReExpr(this, Native.Z3_mk_re_concat(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
 
@@ -2606,7 +2606,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(t, a => a != null));
             Contract.Ensures(Contract.Result<ReExpr>() != null);
 
-            CheckContextMatch(t);
+            CheckContextMatch<ReExpr>(t);
             return new ReExpr(this, Native.Z3_mk_re_union(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
         }
     
@@ -2621,7 +2621,7 @@ namespace Microsoft.Z3
         {
            Contract.Requires(args != null);
            Contract.Requires(Contract.Result<BoolExpr[]>() != null);
-           CheckContextMatch(args);
+           CheckContextMatch<BoolExpr>(args);
            return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint) args.Length,
                                                           AST.ArrayToNative(args), k));
         }
@@ -2635,7 +2635,7 @@ namespace Microsoft.Z3
            Contract.Requires(coeffs != null);
            Contract.Requires(args.Length == coeffs.Length);
            Contract.Requires(Contract.Result<BoolExpr[]>() != null);
-           CheckContextMatch(args);
+           CheckContextMatch<BoolExpr>(args);
            return new BoolExpr(this, Native.Z3_mk_pble(nCtx, (uint) args.Length,
                                                           AST.ArrayToNative(args),
                                                           coeffs, k));
@@ -3386,7 +3386,7 @@ namespace Microsoft.Z3
 
             CheckContextMatch(t1);
             CheckContextMatch(t2);
-            CheckContextMatch(ts);
+            CheckContextMatch<Tactic>(ts);
 
             IntPtr last = IntPtr.Zero;
             if (ts != null && ts.Length > 0)
@@ -3577,7 +3577,7 @@ namespace Microsoft.Z3
             Contract.Requires(t == null || Contract.ForAll(t, tactic => tactic != null));
             Contract.Ensures(Contract.Result<Tactic>() != null);
 
-            CheckContextMatch(t);
+            CheckContextMatch<Tactic>(t);
             return new Tactic(this, Native.Z3_tactic_par_or(nCtx, Tactic.ArrayLength(t), Tactic.ArrayToNative(t)));
         }
 
@@ -4810,7 +4810,7 @@ namespace Microsoft.Z3
         }
 
         [Pure]
-        internal void CheckContextMatch(IEnumerable<Z3Object> arr)
+        internal void CheckContextMatch<T>(IEnumerable<T> arr) where T : Z3Object
         {
             Contract.Requires(arr == null || Contract.ForAll(arr, a => a != null));
 

src/api/dotnet/Expr.cs

@@ -98,7 +98,7 @@ namespace Microsoft.Z3
             Contract.Requires(args != null);
             Contract.Requires(Contract.ForAll(args, a => a != null));
 
-            Context.CheckContextMatch(args);
+            Context.CheckContextMatch<Expr>(args);
             if (IsApp && args.Length != NumArgs)
                 throw new Z3Exception("Number of arguments does not match");
             NativeObject = Native.Z3_update_term(Context.nCtx, NativeObject, (uint)args.Length, Expr.ArrayToNative(args));
@@ -120,8 +120,8 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(to, t => t != null));
             Contract.Ensures(Contract.Result<Expr>() != null);
 
-            Context.CheckContextMatch(from);
+            Context.CheckContextMatch<Expr>(from);
-            Context.CheckContextMatch(to);
+            Context.CheckContextMatch<Expr>(to);
             if (from.Length != to.Length)
                 throw new Z3Exception("Argument sizes do not match");
             return Expr.Create(Context, Native.Z3_substitute(Context.nCtx, NativeObject, (uint)from.Length, Expr.ArrayToNative(from), Expr.ArrayToNative(to)));
@@ -152,7 +152,7 @@ namespace Microsoft.Z3
             Contract.Requires(Contract.ForAll(to, t => t != null));
             Contract.Ensures(Contract.Result<Expr>() != null);
 
-            Context.CheckContextMatch(to);
+            Context.CheckContextMatch<Expr>(to);
             return Expr.Create(Context, Native.Z3_substitute_vars(Context.nCtx, NativeObject, (uint)to.Length, Expr.ArrayToNative(to)));
         }
 

src/api/dotnet/Fixedpoint.cs

@@ -71,7 +71,7 @@ namespace Microsoft.Z3
             Contract.Requires(constraints != null);
             Contract.Requires(Contract.ForAll(constraints, c => c != null));
 
-            Context.CheckContextMatch(constraints);
+            Context.CheckContextMatch<BoolExpr>(constraints);
             foreach (BoolExpr a in constraints)
             {
                 Native.Z3_fixedpoint_assert(Context.nCtx, NativeObject, a.NativeObject);
@@ -151,7 +151,7 @@ namespace Microsoft.Z3
             Contract.Requires(relations != null);
             Contract.Requires(Contract.ForAll(0, relations.Length, i => relations[i] != null));
 
-            Context.CheckContextMatch(relations);
+            Context.CheckContextMatch<FuncDecl>(relations);
             Z3_lbool r = (Z3_lbool)Native.Z3_fixedpoint_query_relations(Context.nCtx, NativeObject,
                                    AST.ArrayLength(relations), AST.ArrayToNative(relations));
             switch (r)

src/api/dotnet/FuncDecl.cs

@@ -339,7 +339,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(args == null || Contract.ForAll(args, a => a != null));
 
-            Context.CheckContextMatch(args);
+            Context.CheckContextMatch<Expr>(args);
             return Expr.Create(Context, this, args);
         }
 

src/api/dotnet/Goal.cs

@@ -82,7 +82,7 @@ namespace Microsoft.Z3
             Contract.Requires(constraints != null);
             Contract.Requires(Contract.ForAll(constraints, c => c != null));
 
-            Context.CheckContextMatch(constraints);
+            Context.CheckContextMatch<BoolExpr>(constraints);
             foreach (BoolExpr c in constraints)
             {
                 Contract.Assert(c != null); // It was an assume, now made an assert just to be sure we do not regress

src/api/dotnet/Quantifier.cs

@@ -172,10 +172,10 @@ namespace Microsoft.Z3
             Contract.Requires(patterns == null || Contract.ForAll(patterns, p => p != null));
             Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
 
-            Context.CheckContextMatch(patterns);
+            Context.CheckContextMatch<Pattern>(patterns);
-            Context.CheckContextMatch(noPatterns);
+            Context.CheckContextMatch<Expr>(noPatterns);
-            Context.CheckContextMatch(sorts);
+            Context.CheckContextMatch<Sort>(sorts);
-            Context.CheckContextMatch(names);
+            Context.CheckContextMatch<Symbol>(names);
             Context.CheckContextMatch(body);
 
             if (sorts.Length != names.Length)
@@ -212,8 +212,8 @@ namespace Microsoft.Z3
             Contract.Requires(noPatterns == null || Contract.ForAll(noPatterns, np => np != null));
             Contract.Requires(bound == null || Contract.ForAll(bound, n => n != null));
 
-            Context.CheckContextMatch(noPatterns);
+            Context.CheckContextMatch<Expr>(noPatterns);
-            Context.CheckContextMatch(patterns);
+            Context.CheckContextMatch<Pattern>(patterns);
             //Context.CheckContextMatch(bound);
             Context.CheckContextMatch(body);
 

src/api/dotnet/Solver.cs

@@ -111,7 +111,7 @@ namespace Microsoft.Z3
             Contract.Requires(constraints != null);
             Contract.Requires(Contract.ForAll(constraints, c => c != null));
 
-            Context.CheckContextMatch(constraints);
+            Context.CheckContextMatch<BoolExpr>(constraints);
             foreach (BoolExpr a in constraints)
             {
                 Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject);
@@ -142,8 +142,8 @@ namespace Microsoft.Z3
             Contract.Requires(constraints != null);
             Contract.Requires(Contract.ForAll(constraints, c => c != null));
             Contract.Requires(Contract.ForAll(ps, c => c != null));
-            Context.CheckContextMatch(constraints);
+            Context.CheckContextMatch<BoolExpr>(constraints);
-            Context.CheckContextMatch(ps);
+            Context.CheckContextMatch<BoolExpr>(ps);
             if (constraints.Length != ps.Length)
                 throw new Z3Exception("Argument size mismatch");
             

src/api/dotnet/Z3Object.cs

@@ -138,7 +138,7 @@ namespace Microsoft.Z3
         }
 
         [Pure]
-        internal static IntPtr[] EnumToNative(IEnumerable<Z3Object> a)
+        internal static IntPtr[] EnumToNative<T>(IEnumerable<T> a) where T : Z3Object
         {
             Contract.Ensures(a == null || Contract.Result<IntPtr[]>() != null);
             Contract.Ensures(a == null || Contract.Result<IntPtr[]>().Length == a.Count());

src/api/python/z3.py

@@ -118,6 +118,8 @@ def _get_args(args):
     try:
         if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
             return args[0]
+        elif len(args) == 1 and isinstance(args[0], set):
+            return [arg for arg in args[0]]
         else:
             return args
     except:  # len is not necessarily defined when args is not a sequence (use reflection?)

src/ast/ast.cpp

@@ -78,7 +78,10 @@ void parameter::del_eh(ast_manager & m, family_id fid) {
     }
     else if (is_external()) {
         SASSERT(fid != null_family_id);
-        m.get_plugin(fid)->del(*this);
+        decl_plugin * plugin = m.get_plugin(fid);
+        if (plugin) {
+            plugin->del(*this);
+        }
     }
 }
 
@@ -1418,9 +1421,10 @@ ast_manager::~ast_manager() {
     }
     it = m_plugins.begin();
     for (; it != end; ++it) {
-        if (*it)
+        if (*it) 
             dealloc(*it);
     }
+    m_plugins.reset();
     while (!m_ast_table.empty()) {
         DEBUG_CODE(std::cout << "ast_manager LEAKED: " << m_ast_table.size() << std::endl;);
         ptr_vector<ast> roots;
@@ -1430,14 +1434,22 @@ ast_manager::~ast_manager() {
         for (; it_a != end_a; ++it_a) {
             ast* n = (*it_a);
             switch (n->get_kind()) {
-            case AST_SORT:
+            case AST_SORT: {
-                mark_array_ref(mark, to_sort(n)->get_info()->get_num_parameters(), to_sort(n)->get_info()->get_parameters());
+                sort_info* info = to_sort(n)->get_info();
+                if (info != 0) {
+                    mark_array_ref(mark, info->get_num_parameters(), info->get_parameters());
+                }
                 break;
-            case AST_FUNC_DECL:
+            }
-                mark_array_ref(mark, to_func_decl(n)->get_info()->get_num_parameters(), to_func_decl(n)->get_info()->get_parameters());
+            case AST_FUNC_DECL: {
+                func_decl_info* info = to_func_decl(n)->get_info();
+                if (info != 0) {
+                    mark_array_ref(mark, info->get_num_parameters(), info->get_parameters());
+                }
                 mark_array_ref(mark, to_func_decl(n)->get_arity(), to_func_decl(n)->get_domain());
                 mark.mark(to_func_decl(n)->get_range(), true);
                 break;
+            }
             case AST_APP:
                 mark.mark(to_app(n)->get_decl(), true);
                 mark_array_ref(mark, to_app(n)->get_num_args(), to_app(n)->get_args());
@@ -1857,8 +1869,8 @@ void ast_manager::delete_node(ast * n) {
             dec_array_ref(worklist, to_quantifier(n)->get_num_patterns(), to_quantifier(n)->get_patterns());
             dec_array_ref(worklist, to_quantifier(n)->get_num_no_patterns(), to_quantifier(n)->get_no_patterns());
             break;
-    default:
+        default:
-        break;
+            break;
         }
         if (m_debug_ref_count) {
             m_debug_free_indices.insert(n->m_id,0);

src/ast/datatype_decl_plugin.cpp

@@ -732,7 +732,8 @@ void datatype_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol
 datatype_util::datatype_util(ast_manager & m):
     m_manager(m),
     m_family_id(m.mk_family_id("datatype")),
-    m_asts(m) {
+    m_asts(m),
+    m_start(0) {
 }
 
 datatype_util::~datatype_util() {
@@ -807,11 +808,11 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
     // If there is no such constructor, then we select one that 
     //   2) each type T_i is not recursive or contains a constructor that does not depend on T
     ptr_vector<func_decl> const * constructors = get_datatype_constructors(ty);
-    ptr_vector<func_decl>::const_iterator it  = constructors->begin();
-    ptr_vector<func_decl>::const_iterator end = constructors->end();
     // step 1)
-    for (; it != end; ++it) {
+    unsigned sz = constructors->size();
-        func_decl * c = *it;
+    ++m_start;
+    for (unsigned j = 0; j < sz; ++j) {        
+        func_decl * c = (*constructors)[(j + m_start) % sz];
         unsigned num_args = c->get_arity();
         unsigned i = 0;
         for (; i < num_args; i++) {
@@ -823,9 +824,8 @@ func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector<so
             return c;
     }
     // step 2)
-    it  = constructors->begin();
+    for (unsigned j = 0; j < sz; ++j) {        
-    for (; it != end; ++it) {
+        func_decl * c = (*constructors)[(j + m_start) % sz];
-        func_decl * c = *it;
         TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";);
         unsigned num_args = c->get_arity();
         unsigned i = 0;
@@ -964,6 +964,7 @@ void datatype_util::reset() {
     std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
     m_vectors.reset();
     m_asts.reset();
+    ++m_start;
 }
 
 /**

src/ast/datatype_decl_plugin.h

@@ -176,7 +176,8 @@ class datatype_util {
     obj_map<sort, bool>                         m_is_enum;
     ast_ref_vector                              m_asts;
     ptr_vector<ptr_vector<func_decl> >          m_vectors;
-    
+    unsigned                                    m_start;
+
     func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
     func_decl * get_constructor(sort * ty, unsigned c_id);
 

src/ast/macros/macro_util.cpp

@@ -458,28 +458,32 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
     expr_ref_buffer  var_mapping(m_manager);
     bool changed = false;
     unsigned num_args = head->get_num_args();
-    unsigned max      = num_args;
+    unsigned max_var_idx = 0;
     for (unsigned i = 0; i < num_args; i++) {
-        var * v     = to_var(head->get_arg(i));
+        var const * v = to_var(head->get_arg(i));
-        if (v->get_idx() >= max)
+        if (v->get_idx() > max_var_idx)
-            max = v->get_idx() + 1;
+            max_var_idx = v->get_idx();
     }
     TRACE("normalize_expr_bug",
           tout << "head: " << mk_pp(head, m_manager) << "\n";
           tout << "applying substitution to:\n" << mk_bounded_pp(t, m_manager) << "\n";);
     for (unsigned i = 0; i < num_args; i++) {
-        var * v     = to_var(head->get_arg(i));
+        var * v = to_var(head->get_arg(i));
         if (v->get_idx() != i) {
             changed = true;
-            var * new_var = m_manager.mk_var(i, v->get_sort());
+            var_ref new_var(m_manager.mk_var(i, v->get_sort()), m_manager);
-            CTRACE("normalize_expr_bug", v->get_idx() >= num_args, tout << mk_pp(v, m_manager) << ", num_args: " << num_args << "\n";);
+            var_mapping.setx(max_var_idx - v->get_idx(), new_var);
-            SASSERT(v->get_idx() < max);
-            var_mapping.setx(max - v->get_idx() - 1, new_var);
-        }
-        else {
-            var_mapping.setx(max - i - 1, v);
         }
+        else
+            var_mapping.setx(max_var_idx - i, v);
     }
+    
+    for (unsigned i = num_args; i <= max_var_idx; i++)
+        // CMW: Won't be used, but dictates a larger binding size, 
+        // so that the indexes between here and in the rewriter match.
+        // It's possible that we don't see the true max idx of all vars here.
+        var_mapping.setx(max_var_idx - i, 0); 
+
     if (changed) {
         // REMARK: t may have nested quantifiers... So, I must use the std order for variable substitution.
         var_subst subst(m_manager, true); 
@@ -488,7 +492,7 @@ void macro_util::normalize_expr(app * head, expr * t, expr_ref & norm_t) const {
               tout << "applying substitution to:\n" << mk_ll_pp(t, m_manager) << "\nsubstitution:\n";
               for (unsigned i = 0; i < var_mapping.size(); i++) {
                   if (var_mapping[i] != 0)
-                    tout << "#" << i << " -> " << mk_pp(var_mapping[i], m_manager) << "\n";
+                    tout << "#" << i << " -> " << mk_ll_pp(var_mapping[i], m_manager);
               });
         subst(t, var_mapping.size(), var_mapping.c_ptr(), norm_t);
     }

src/ast/pp_params.pyg

@@ -16,4 +16,5 @@ def_module_params('pp',
                           ('fixed_indent', BOOL, False, 'use a fixed indentation for applications'),
                           ('single_line', BOOL, False, 'ignore line breaks when true'),
                           ('bounded', BOOL, False, 'ignore characters exceeding max width'),
+                          ('pretty_proof', BOOL, False, 'use slower, but prettier, printer for proofs'),
                           ('simplify_implies', BOOL, True, 'simplify nested implications for pretty printing')))

src/ast/seq_decl_plugin.cpp

@@ -144,6 +144,9 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const {
     if (length() < src.length()) {
         return zstring(*this);
     }
+    if (src.length() == 0) {
+        return zstring(*this);
+    }
     bool found = false;
     for (unsigned i = 0; i < length(); ++i) {
         bool eq = !found && i + src.length() <= length();

src/cmd_context/basic_cmds.cpp

@@ -29,6 +29,7 @@ Notes:
 #include"gparams.h"
 #include"env_params.h"
 #include"well_sorted.h"
+#include"pp_params.hpp"
 
 class help_cmd : public cmd {
     svector<symbol> m_cmds;
@@ -161,14 +162,19 @@ ATOMIC_CMD(get_proof_cmd, "get-proof", "retrieve proof", {
         throw cmd_exception("proof is not well sorted");
     }
     
-    // TODO: reimplement a new SMT2 pretty printer 
+    pp_params params;
-    ast_smt_pp pp(ctx.m());
+    if (params.pretty_proof()) {
-    cmd_is_declared isd(ctx);
+        ctx.regular_stream() << mk_pp(pr, ctx.m()) << std::endl;
-    pp.set_is_declared(&isd);
+    }
-    pp.set_logic(ctx.get_logic());
+    else {
-    // ctx.regular_stream() << mk_pp(pr, ctx.m()) << "\n";
+        // TODO: reimplement a new SMT2 pretty printer 
-    pp.display_smt2(ctx.regular_stream(), pr);
+        ast_smt_pp pp(ctx.m());
-    ctx.regular_stream() << std::endl;
+        cmd_is_declared isd(ctx);
+        pp.set_is_declared(&isd);
+        pp.set_logic(ctx.get_logic());
+        pp.display_smt2(ctx.regular_stream(), pr);
+        ctx.regular_stream() << std::endl;
+    }
 });
 
 #define PRINT_CORE()                                            \

src/cmd_context/interpolant_cmds.cpp

@@ -28,7 +28,6 @@
 #include"mpq.h"
 #include"expr2var.h"
 #include"pp.h"
-#include"pp_params.hpp"
 #include"iz3interp.h"
 #include"iz3checker.h"
 #include"iz3profiling.h"

src/muz/dataflow/dataflow.h

@@ -72,7 +72,7 @@ namespace datalog {
                     }
                     e->get_data().m_value->push_back(cur);
                 }
-                if (cur->get_uninterpreted_tail_size() == 0) {
+                if (cur->get_positive_tail_size() == 0) {
                     func_decl *sym = cur->get_head()->get_decl();
                     bool new_info = m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_up(m_context, cur);
                     if (new_info) {
@@ -97,7 +97,7 @@ namespace datalog {
         }
 
         void step_bottom_up() {
-            for(todo_set::iterator I = m_todo[m_todo_idx].begin(),
+            for(todo_set::iterator I = m_todo[m_todo_idx].begin(),                    
                 E = m_todo[m_todo_idx].end(); I!=E; ++I) {
                 ptr_vector<rule> * rules; 
                 if (!m_body2rules.find(*I, rules))
@@ -236,7 +236,7 @@ namespace datalog {
             return m_facts.get(m_rule->get_decl(idx), Fact::null_fact);
         }
         unsigned size() const {
-            return m_rule->get_uninterpreted_tail_size();
+            return m_rule->get_positive_tail_size();
         }
     };
 

src/muz/transforms/dl_mk_coi_filter.cpp

@@ -44,6 +44,7 @@ namespace datalog {
                 if (m_context.has_facts(r->get_decl(i))) {
                     return 0;
                 }
+
                 if (r->is_neg_tail(i)) {
                     if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
                         if (!new_tail) {
@@ -53,11 +54,14 @@ namespace datalog {
                             }
                             new_tail = true;
                         }
-                    } else if (new_tail) {
+                    } 
+                    else if (new_tail) {
                         m_new_tail.push_back(r->get_tail(i));
                         m_new_tail_neg.push_back(true);
                     }
-                } else {
+                } 
+
+                else {
                     SASSERT(!new_tail);
                     if (!engine.get_fact(r->get_decl(i)).is_reachable()) {
                         contained = false;

src/parsers/smt/smtparser.cpp

@@ -1573,7 +1573,8 @@ private:
                         return false;
                     }
                 }
-                expr * p = m_manager.mk_pattern(ts.size(), (app*const*)(ts.c_ptr()));
+                expr_ref p(m_manager);
+                p = m_manager.mk_pattern(ts.size(), (app*const*)(ts.c_ptr()));
                 if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) {
                     set_error("invalid pattern", children[0]);
                     return false;
@@ -1581,8 +1582,11 @@ private:
                 patterns.push_back(p);
             }
             else if (children[0]->string() == symbol("ex_act") && ts.size() == 1) {
-                app * sk_hack = m_manager.mk_app(m_sk_hack, 1, ts.c_ptr());
+                app_ref sk_hack(m_manager);
-                expr * p = m_manager.mk_pattern(1, &sk_hack);
+                sk_hack = m_manager.mk_app(m_sk_hack, 1, ts.c_ptr());
+                app * sk_hackp = sk_hack.get();
+                expr_ref p(m_manager);
+                p = m_manager.mk_pattern(1, &sk_hackp);
                 if (!p || (!ignore_user_patterns() && !m_pattern_validator(num_bindings, p, children[0]->line(), children[0]->pos()))) {
                     set_error("invalid pattern", children[0]);
                     return false;

src/sat/sat_bceq.cpp

@@ -493,14 +493,14 @@ namespace sat {
     void bceq::operator()() {
         if (!m_solver.m_config.m_bcd) return;
         flet<bool> _disable_bcd(m_solver.m_config.m_bcd, false);
-        flet<bool> _disable_min(m_solver.m_config.m_minimize_core, false);
+        flet<bool> _disable_min(m_solver.m_config.m_core_minimize, false);
         flet<bool> _disable_opt(m_solver.m_config.m_optimize_model, false);
         flet<unsigned> _bound_maxc(m_solver.m_config.m_max_conflicts, 1500);
 
         use_list     ul;        
         solver       s(m_solver.m_params, m_solver.rlimit(), 0);
         s.m_config.m_bcd            = false;
-        s.m_config.m_minimize_core  = false;
+        s.m_config.m_core_minimize  = false;
         s.m_config.m_optimize_model = false;
         s.m_config.m_max_conflicts  = 1500;
         m_use_list = &ul;

src/sat/sat_config.cpp

@@ -107,8 +107,8 @@ namespace sat {
             m_gc_increment    = p.gc_increment();
         }
         m_minimize_lemmas = p.minimize_lemmas();
-        m_minimize_core   = p.minimize_core();
+        m_core_minimize   = p.core_minimize();
-        m_minimize_core_partial   = p.minimize_core_partial();
+        m_core_minimize_partial   = p.core_minimize_partial();
         m_optimize_model  = p.optimize_model();
         m_bcd             = p.bcd();
         m_dyn_sub_res     = p.dyn_sub_res();

src/sat/sat_config.h

@@ -69,8 +69,8 @@ namespace sat {
 
         bool               m_minimize_lemmas;
         bool               m_dyn_sub_res;
-        bool               m_minimize_core;
+        bool               m_core_minimize;
-        bool               m_minimize_core_partial;
+        bool               m_core_minimize_partial;
         bool               m_optimize_model;
         bool               m_bcd;
 

src/sat/sat_mus.cpp

@@ -58,7 +58,7 @@ namespace sat {
     }
 
     lbool mus::operator()() {
-        flet<bool> _disable_min(s.m_config.m_minimize_core, false);
+        flet<bool> _disable_min(s.m_config.m_core_minimize, false);
         flet<bool> _disable_opt(s.m_config.m_optimize_model, false);
         flet<bool> _is_active(m_is_active, true);
         IF_VERBOSE(3, verbose_stream() << "(sat.mus " << s.get_core() << ")\n";);
@@ -69,7 +69,7 @@ namespace sat {
     }
 
     lbool mus::mus1() {
-        bool minimize_partial = s.m_config.m_minimize_core_partial;
+        bool minimize_partial = s.m_config.m_core_minimize_partial;
         TRACE("sat", tout << "old core: " << s.get_core() << "\n";);
         literal_vector& core = get_core();
         literal_vector& mus = m_mus;
@@ -96,7 +96,7 @@ namespace sat {
                 // IF_VERBOSE(0, verbose_stream() << "num literals: " << core << " " << mus << "\n";);
                 break;
             }
-            if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
+            if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
                 IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
                 set_core();
                 return l_true;
@@ -172,7 +172,7 @@ namespace sat {
 
     lbool mus::qx(literal_set& assignment, literal_set& support, bool has_support) {
         lbool is_sat = l_true;
-        if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
+        if (s.m_config.m_core_minimize_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
             IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
             return l_true;
         }

src/sat/sat_params.pyg

@@ -19,8 +19,8 @@ def_module_params('sat',
                           ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
                           ('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
                           ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
-                          ('minimize_core', BOOL, False, 'minimize computed core'),
+                          ('core.minimize', BOOL, False, 'minimize computed core'),
-                          ('minimize_core_partial', BOOL, False, 'apply partial (cheap) core minimization'),
+                          ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
                           ('optimize_model', BOOL, False, 'enable optimization of soft constraints'),
                           ('bcd', BOOL, False, 'enable blocked clause decomposition for equality extraction'),
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))

src/sat/sat_solver.cpp

@@ -937,7 +937,7 @@ namespace sat {
 
 
     bool solver::init_weighted_assumptions(unsigned num_lits, literal const* lits, double const* weights, double max_weight) {
-        flet<bool> _min1(m_config.m_minimize_core, false);
+        flet<bool> _min1(m_config.m_core_minimize, false);
         m_weight = 0;
         m_blocker.reset();
         svector<lbool> values;
@@ -2015,7 +2015,7 @@ namespace sat {
             idx--;
         }        
         reset_unmark(old_size);
-        if (m_config.m_minimize_core) {
+        if (m_config.m_core_minimize) {
             if (m_min_core_valid && m_min_core.size() < m_core.size()) {
                 IF_VERBOSE(1, verbose_stream() << "(sat.updating core " << m_min_core.size() << " " << m_core.size() << ")\n";);
                 m_core.reset();

src/smt/smt_conflict_resolution.cpp

@@ -403,7 +403,6 @@ namespace smt {
         // the previous levels were already inconsistent, or the inconsistency was
         // triggered by an axiom or justification proof wrapper, this two kinds
         // of justification are considered level zero.
-
         if (m_conflict_lvl <= m_ctx.get_search_level()) {
             TRACE("conflict", tout << "problem is unsat\n";);
             if (m_manager.proofs_enabled())

src/smt/smt_consequences.cpp

@@ -18,6 +18,8 @@ Revision History:
 --*/
 #include "smt_context.h"
 #include "ast_util.h"
+#include "datatype_decl_plugin.h"
+#include "model_pp.h"
 
 namespace smt {
 
@@ -31,77 +33,112 @@ namespace smt {
         return mk_and(premises);
     }
 
-    void context::extract_fixed_consequences(unsigned start, obj_map<expr, expr*>& vars, uint_set const& assumptions, expr_ref_vector& conseq) {
+    //
+    // The literal lit is assigned at the search level, so it follows from the assumptions.
+    // We retrieve the set of assumptions it depends on in the set 's'.
+    // The map m_antecedents contains the association from these literals to the assumptions they depend on.
+    // We then examine the contents of the literal lit and augment the set of consequences in one of the following cases:
+    // - e is a propositional atom and it is one of the variables that is to be fixed.
+    // - e is an equality between a variable and value that is to be fixed.
+    // - e is a data-type recognizer of a variable that is to be fixed.
+    // 
+    void context::extract_fixed_consequences(literal lit, obj_map<expr, expr*>& vars, uint_set const& assumptions, expr_ref_vector& conseq) {
         ast_manager& m = m_manager;
-        pop_to_search_lvl();
+        datatype_util dt(m);
-        literal_vector const& lits = assigned_literals();
-        unsigned sz = lits.size();
         expr* e1, *e2;       
-        expr_ref fml(m);
+        expr_ref fml(m);        
-        for (unsigned i = start; i < sz; ++i) {            
+        if (lit == true_literal) return;
-            literal lit = lits[i];
+        expr* e = bool_var2expr(lit.var());
-            if (lit == true_literal) continue;
+        uint_set s;
-            expr* e = bool_var2expr(lit.var());
+        if (assumptions.contains(lit.var())) {
-            uint_set s;
+            s.insert(lit.var());
-            if (assumptions.contains(lit.var())) {
+        }
-                s.insert(lit.var());
+        else {
-            }
+            b_justification js = get_justification(lit.var());
-            else {
+            switch (js.get_kind()) {
-                b_justification js = get_justification(lit.var());
+            case b_justification::CLAUSE: {
-                switch (js.get_kind()) {
+                clause * cls = js.get_clause();
-                case b_justification::CLAUSE: {
+                if (!cls) break;
-                    clause * cls      = js.get_clause();
+                unsigned num_lits = cls->get_num_literals();
-                    unsigned num_lits = cls->get_num_literals();
+                for (unsigned j = 0; j < num_lits; ++j) {
-                    for (unsigned j = 0; j < num_lits; ++j) {
+                    literal lit2 = cls->get_literal(j);
-                        literal lit2 = cls->get_literal(j);
+                    if (lit2.var() != lit.var()) {
-                        if (lit2.var() != lit.var()) {
+                        s |= m_antecedents.find(lit2.var());
-                            s |= m_antecedents.find(lit2.var());
-                        }
                     }
-                    break;
                 }
-                case b_justification::BIN_CLAUSE: {
+                break;
-                    s |= m_antecedents.find(js.get_literal().var());
-                    break;
-                }
-                case b_justification::AXIOM: {
-                    break;
-                }
-                case b_justification::JUSTIFICATION: {
-                    literal_vector literals;
-                    m_conflict_resolution->justification2literals(js.get_justification(), literals);
-                    for (unsigned j = 0; j < literals.size(); ++j) {
-                        s |= m_antecedents.find(literals[j].var());
-                    }
-                    break;
-                }
-                }                
-            }       
-            m_antecedents.insert(lit.var(), s);
-            TRACE("context", display_literal_verbose(tout, lit); tout << " " << s << "\n";);
-            bool found = false;
-            if (vars.contains(e)) {
-                found = true;
-                fml = lit.sign()?m.mk_not(e):e;
-                vars.erase(e);
             }
-            else if (!lit.sign() && m.is_eq(e, e1, e2)) {
+            case b_justification::BIN_CLAUSE: {
-                if (vars.contains(e2)) {
+                s |= m_antecedents.find(js.get_literal().var());
-                    std::swap(e1, e2);
+                break;
-                }
+            }
-                if (vars.contains(e1) && m.is_value(e2)) {
+            case b_justification::AXIOM: {
-                    found = true;
+                break;
-                    fml = e;
+            }
-                    vars.erase(e1);                    
+            case b_justification::JUSTIFICATION: {
-                }
+                literal_vector literals;
+                m_conflict_resolution->justification2literals(js.get_justification(), literals);
+                for (unsigned j = 0; j < literals.size(); ++j) {
+                    s |= m_antecedents.find(literals[j].var());
+                }
+                break;
             }
-            if (found) {
-                fml = m.mk_implies(antecedent2fml(s), fml);
-                conseq.push_back(fml);
             }
         }
+        m_antecedents.insert(lit.var(), s);
+        TRACE("context", display_literal_verbose(tout, lit); tout << " " << s << "\n";);
+        bool found = false;
+        if (vars.contains(e)) {
+            found = true;
+            fml = lit.sign() ? m.mk_not(e) : e;
+            vars.erase(e);
+        }
+        else if (!lit.sign() && m.is_eq(e, e1, e2)) {
+            if (vars.contains(e2)) {
+                std::swap(e1, e2);
+            }
+            if (vars.contains(e1) && m.is_value(e2)) {
+                found = true;
+                fml = e;
+                vars.erase(e1);
+            }
+        }
+        else if (!lit.sign() && is_app(e) && dt.is_recognizer(to_app(e)->get_decl())) {
+            if (vars.contains(to_app(e)->get_arg(0))) {
+                found = true;
+                fml = m.mk_eq(to_app(e)->get_arg(0), m.mk_const(dt.get_recognizer_constructor(to_app(e)->get_decl())));
+                vars.erase(to_app(e)->get_arg(0));
+            }
+        }
+        if (found) {
+            fml = m.mk_implies(antecedent2fml(s), fml);
+            conseq.push_back(fml);
+        }
     }
 
+    void context::extract_fixed_consequences(unsigned start, obj_map<expr, expr*>& vars, uint_set const& assumptions, expr_ref_vector& conseq) {
+        pop_to_search_lvl();
+        SASSERT(!inconsistent());
+        literal_vector const& lits = assigned_literals();
+        unsigned sz = lits.size();
+        for (unsigned i = start; i < sz; ++i) {            
+            extract_fixed_consequences(lits[i], vars, assumptions, conseq);
+        }
+        SASSERT(!inconsistent());
+    }
+    
+
+    //
+    // The assignment stack is assumed consistent.
+    // For each Boolean variable, we check if there is a literal assigned to the 
+    // opposite value of the reference model, and for non-Boolean variables we
+    // check if the current state forces the variable to be distinct from the reference value.
+    // 
+    // For yet to be determined Boolean variables we furthermore force the phase to be opposite
+    // to the reference value in the attempt to let the sat engine emerge with a model that
+    // rules out as many non-fixed variables as possible.
+    // 
+
     unsigned context::delete_unfixed(obj_map<expr, expr*>& var2val, expr_ref_vector& unfixed) {
         ast_manager& m = m_manager;
         ptr_vector<expr> to_delete;
@@ -144,10 +181,15 @@ namespace smt {
         return to_delete.size();
     }
 
+#define are_equal(v, k) (e_internalized(k) && e_internalized(v) && get_enode(k)->get_root() == get_enode(v)->get_root())
+
     //
     // Extract equalities that are congruent at the search level.
+    // Add a clause to short-circuit the congruence justifications for
+    // next rounds.
     // 
     unsigned context::extract_fixed_eqs(obj_map<expr, expr*>& var2val, expr_ref_vector& conseq) {
+        TRACE("context", tout << "extract fixed consequences\n";);
         ast_manager& m = m_manager;
         ptr_vector<expr> to_delete;
         expr_ref fml(m), eq(m);
@@ -155,8 +197,7 @@ namespace smt {
         for (; it != end; ++it) {
             expr* k = it->m_key;
             expr* v = it->m_value;
-            if (!m.is_bool(k) && e_internalized(k) && e_internalized(v) && 
+            if (!m.is_bool(k) && are_equal(k, v)) {
-                get_enode(k)->get_root() == get_enode(v)->get_root()) {
                 literal_vector literals;
                 m_conflict_resolution->eq2literals(get_enode(v), get_enode(k), literals);
                 uint_set s;
@@ -175,9 +216,10 @@ namespace smt {
                 }
                 eq = mk_eq_atom(k, v);
                 internalize_formula(eq, false);
-                literal lit(get_bool_var(eq), true);
+                literal lit(get_bool_var(eq), false);
                 literals.push_back(lit);
                 mk_clause(literals.size(), literals.c_ptr(), 0);
+                TRACE("context", display_literals_verbose(tout, literals.size(), literals.c_ptr()););
             }
         }    
         for (unsigned i = 0; i < to_delete.size(); ++i) {
@@ -192,6 +234,7 @@ namespace smt {
                                     expr_ref_vector& unfixed) {
 
         m_antecedents.reset();
+        pop_to_base_lvl();
         lbool is_sat = check(assumptions.size(), assumptions.c_ptr());
         if (is_sat != l_true) {
             return is_sat;
@@ -207,6 +250,7 @@ namespace smt {
         expr_ref_vector trail(m);
         model_evaluator eval(*mdl.get());
         expr_ref val(m);
+        TRACE("context", model_pp(tout, *mdl););
         for (unsigned i = 0; i < vars.size(); ++i) {
             eval(vars[i], val);
             if (m.is_value(val)) {
@@ -233,9 +277,17 @@ namespace smt {
             obj_map<expr,expr*>::iterator it = var2val.begin();
             expr* e = it->m_key;
             expr* val = it->m_value;
-            push_scope();
-            unsigned current_level = m_scope_lvl;
 
+            TRACE("context", tout << "scope level: " << get_scope_level() << "\n";);
+            SASSERT(!inconsistent());
+
+            //
+            // The current variable is checked to be a backbone
+            // We add the negation of the reference assignment to the variable.
+            // If the variable is a Boolean, it means adding literal that has
+            // the opposite value of the current reference model.
+            // If the variable is a non-Boolean, it means adding a disequality.
+            //
             literal lit;
             if (m.is_bool(e)) {
                 lit = literal(get_bool_var(e), m.is_true(val));
@@ -244,9 +296,20 @@ namespace smt {
                 eq = mk_eq_atom(e, val);
                 internalize_formula(eq, false);
                 lit = literal(get_bool_var(eq), true);
+                TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n";
+                      display_literal_verbose(tout, lit); tout << "\n"; 
+                      tout << "Equal: " << are_equal(e, val) << "\n";);
             }
+            mark_as_relevant(lit);
+            push_scope();
             assign(lit, b_justification::mk_axiom(), true);
             flet<bool> l(m_searching, true);
+
+            // 
+            // We check if the current assignment stack can be extended to a 
+            // satisfying assignment. bounded search may decide to restart, 
+            // in which case it returns l_undef and clears search failure.
+            //
             while (true) {
                 is_sat = bounded_search();
                 TRACE("context", tout << "search result: " << is_sat << "\n";);
@@ -260,33 +323,78 @@ namespace smt {
                 }
                 break;
             }
-            if (get_assignment(lit) == l_true) {
+            //
+            // If the state is satisfiable with the current variable assigned to 
+            // a different value from the reference model, it is unfixed.
+            // 
+            // If it is assigned above the search level we can't conclude anything
+            // about its value. 
+            // extract_fixed_consequences pops the assignment stack to the search level
+            // so this sets up the state to retry finding fixed values.
+            // 
+            // Otherwise, the variable is fixed.
+            // - it is either assigned at the search level to l_false, or
+            // - the state is l_false, which means that the variable is fixed by
+            //   the background constraints (and does not depend on assumptions).
+            // 
+            if (is_sat == l_true && get_assignment(lit) == l_true && is_relevant(lit)) { 
                 var2val.erase(e);
                 unfixed.push_back(e);
+                SASSERT(!are_equal(e, val));
+                TRACE("context", tout << mk_pp(e, m) << " is unfixed\n";
+                      display_literal_verbose(tout, lit); tout << "\n";
+                      tout << "relevant: " << is_relevant(lit) << "\n";
+                      display(tout););
             }
-            else if (get_assign_level(lit) > get_search_level()) {
+            else if (is_sat == l_true && (get_assign_level(lit) > get_search_level() || !is_relevant(lit))) {
                 TRACE("context", tout << "Retry fixing: " << mk_pp(e, m) << "\n";);
-                pop_to_search_lvl();
+                extract_fixed_consequences(num_units, var2val, _assumptions, conseq);
                 ++num_reiterations;
                 continue;
             }
             else {
-                TRACE("context", tout << "Fixed: " << mk_pp(e, m) << "\n";);
+                //
+                // The state can be labeled as inconsistent when the implied consequence does
+                // not depend on assumptions, then the conflict level sits at the search level
+                // which causes the conflict resolver to decide that the state is unsat.
+                //
+                if (l_false == is_sat) {
+                    SASSERT(inconsistent());
+                    m_conflict = null_b_justification;
+                    m_not_l = null_literal;
+                }
+                TRACE("context", tout << "Fixed: " << mk_pp(e, m) << " " << is_sat << "\n";
+                      if (is_sat == l_false) display(tout););
+                
             }
             ++num_iterations;
 
+            //
+            // Check the slow pass: it retrieves an updated model and checks if the
+            // values in the updated model differ from the values in the reference
+            // model. 
+            // 
             bool apply_slow_pass = model_threshold <= num_iterations || num_iterations <= 2;
-            if (apply_slow_pass) {
+            if (apply_slow_pass && is_sat == l_true) {
                 num_unfixed += delete_unfixed(var2val, unfixed);
                 // The next time we check the model is after 1.5 additional iterations.
                 model_threshold *= 3;
                 model_threshold /= 2;                                
             }
-            // repeat until we either have a model with negated literal or 
-            // the literal is implied at base.
 
+            //
+            // Walk the assignment stack at level 1 for learned consequences.
+            // The current literal should be assigned at the search level unless
+            // the state is is_sat == l_true and the assignment to lit is l_true.
+            // This condition is checked above.
+            // 
             extract_fixed_consequences(num_units, var2val, _assumptions, conseq);
             num_units = assigned_literals().size();
+
+            //
+            // Fixed equalities can be extracted by walking all variables and checking
+            // if the congruence roots are equal at the search level.
+            // 
             if (apply_slow_pass) {
                 num_fixed_eqs += extract_fixed_eqs(var2val, conseq);
                 IF_VERBOSE(1, verbose_stream() << "(get-consequences"
@@ -306,18 +414,72 @@ namespace smt {
                       << " unfixed-deleted: " << num_unfixed
                       << ")\n";);        
             }
+            TRACE("context", tout << "finishing " << mk_pp(e, m) << "\n";);
+            SASSERT(!inconsistent());
+            
+            //
+            // This becomes unnecessary when the fixed consequence are 
+            // completely extracted.
+            // 
             if (var2val.contains(e)) {
                 TRACE("context", tout << "Fixed value to " << mk_pp(e, m) << " was not processed\n";);
                 expr_ref fml(m);
                 fml = m.mk_eq(e, var2val.find(e));
+                if (!m_antecedents.contains(lit.var())) {
+                    extract_fixed_consequences(lit, var2val, _assumptions, conseq);
+                }
                 fml = m.mk_implies(antecedent2fml(m_antecedents[lit.var()]), fml);
                 conseq.push_back(fml);
                 var2val.erase(e);
-                SASSERT(get_assignment(lit) == l_false);
             }        
         }
         end_search();
+        DEBUG_CODE(validate_consequences(assumptions, vars, conseq, unfixed););
         return l_true;
     }
 
+    //
+    // Validate, in a slow pass, that the current consequences are correctly 
+    // extracted.
+    // 
+    void context::validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 
+                                        expr_ref_vector const& conseq, expr_ref_vector const& unfixed) {
+        ast_manager& m = m_manager;
+        expr_ref tmp(m);
+        SASSERT(!inconsistent());
+        for (unsigned i = 0; i < conseq.size(); ++i) {
+            push();            
+            for (unsigned j = 0; j < assumptions.size(); ++j) {
+                assert_expr(assumptions[j]);
+            }
+            TRACE("context", tout << "checking: " << mk_pp(conseq[i], m) << "\n";);
+            tmp = m.mk_not(conseq[i]);
+            assert_expr(tmp);
+            lbool is_sat = check();
+            SASSERT(is_sat != l_true);
+            pop(1);
+        }
+        model_ref mdl;
+        for (unsigned i = 0; i < unfixed.size(); ++i) {
+            push();            
+            for (unsigned j = 0; j < assumptions.size(); ++j) {
+                assert_expr(assumptions[j]);
+            }
+            TRACE("context", tout << "checking unfixed: " << mk_pp(unfixed[i], m) << "\n";);
+            lbool is_sat = check();            
+            SASSERT(is_sat != l_false);
+            if (is_sat == l_true) {
+                get_model(mdl);
+                mdl->eval(unfixed[i], tmp);
+                if (m.is_value(tmp)) {
+                    tmp = m.mk_not(m.mk_eq(unfixed[i], tmp));
+                    assert_expr(tmp);
+                    is_sat = check();
+                    SASSERT(is_sat != l_false);
+                }
+            }
+            pop(1);
+        }
+    }
+
 }

src/smt/smt_context.cpp

@@ -1094,7 +1094,7 @@ namespace smt {
        \brief This method is invoked when a new disequality is asserted.
        The disequality is propagated to the theories.
     */
-    void context::add_diseq(enode * n1, enode * n2) {
+    bool context::add_diseq(enode * n1, enode * n2) {
         enode * r1 = n1->get_root();
         enode * r2 = n2->get_root();
         TRACE("add_diseq", tout << "assigning: #" << n1->get_owner_id() << " != #" << n2->get_owner_id() << "\n";
@@ -1111,7 +1111,7 @@ namespace smt {
 
         if (r1 == r2) {
             TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";);
-            return; // context is inconsistent
+            return false; // context is inconsistent
         }
 
         // Propagate disequalities to theories
@@ -1145,6 +1145,7 @@ namespace smt {
                 l1 = l1->get_next();
             }
         }
+        return true;
     }
     
     /**
@@ -1400,7 +1401,9 @@ namespace smt {
                 }
                 else {
                     TRACE("add_diseq", display_eq_detail(tout, bool_var2enode(v)););
-                    add_diseq(get_enode(lhs), get_enode(rhs));
+                    if (!add_diseq(get_enode(lhs), get_enode(rhs)) && !inconsistent()) {
+                        set_conflict(b_justification(mk_justification(eq_propagation_justification(get_enode(lhs), get_enode(rhs)))), ~l);                        
+                    }
                 }
             }
             else if (d.is_theory_atom()) {

src/smt/smt_context.h

@@ -942,7 +942,7 @@ namespace smt {
             push_eq(n1, n2, eq_justification::mk_cg(used_commutativity));
         }
 
-        void add_diseq(enode * n1, enode * n2);
+        bool add_diseq(enode * n1, enode * n2);
 
         void assign_quantifier(quantifier * q);
 
@@ -1345,6 +1345,7 @@ namespace smt {
             vector<bool_var> b2v, ast_translation& tr);
 
         u_map<uint_set> m_antecedents;
+        void extract_fixed_consequences(literal lit, obj_map<expr, expr*>& var2val, uint_set const& assumptions, expr_ref_vector& conseq);
         void extract_fixed_consequences(unsigned idx, obj_map<expr, expr*>& var2val, uint_set const& assumptions, expr_ref_vector& conseq);
         
         unsigned delete_unfixed(obj_map<expr, expr*>& var2val, expr_ref_vector& unfixed);
@@ -1353,6 +1354,9 @@ namespace smt {
 
         expr_ref antecedent2fml(uint_set const& ante);
 
+        void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, 
+                                   expr_ref_vector const& conseq, expr_ref_vector const& unfixed);
+
 
     public:
         context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref());

src/smt/smt_internalizer.cpp

@@ -1284,7 +1284,6 @@ namespace smt {
         TRACE("mk_clause", tout << "creating clause:\n"; display_literals(tout, num_lits, lits); tout << "\n";);
         switch (k) {
         case CLS_AUX: {
-            unsigned old_num_lits = num_lits;
             literal_buffer simp_lits;
             if (!simplify_aux_clause_literals(num_lits, lits, simp_lits))
                 return 0; // clause is equivalent to true;

src/smt/theory_arith_eq.h

@@ -64,7 +64,7 @@ namespace smt {
                     lower(v2)->push_justification(ante, numeral::zero(), proofs_enabled());
                     upper(v)->push_justification(ante, numeral::zero(), proofs_enabled());
 
-                    TRACE("arith_fixed_propagate_eq", tout << "propagate eq: v" << v << " = v" << v2 << "\n";
+                    TRACE("arith_eq", tout << "propagate eq: v" << v << " = v" << v2 << "\n";
                           display_var(tout, v);
                           display_var(tout, v2););
                     m_stats.m_fixed_eqs++;
@@ -175,7 +175,7 @@ namespace smt {
         timer.stop();
         ok++;
         if (ok % 100000 == 0) {
-            TRACE("propagate_cheap_eq", 
+            TRACE("arith_eq", 
                   tout << total << " " << ok << " " 
                   << static_cast<double>(ok)/static_cast<double>(total) 
                   << " " << timer.get_seconds() << "\n";
@@ -216,7 +216,7 @@ namespace smt {
     void theory_arith<Ext>::propagate_cheap_eq(unsigned rid) {
         if (!propagate_eqs())
             return;
-        TRACE("propagate_cheap_eq", tout << "checking if row " << rid << " can propagate equality.\n";
+        TRACE("arith_eq", tout << "checking if row " << rid << " can propagate equality.\n";
               display_row_info(tout, rid););
         row const & r = m_rows[rid];
         theory_var x;
@@ -258,7 +258,7 @@ namespace smt {
                 // found equality x = y
                 antecedents ante(*this);
                 collect_fixed_var_justifications(r, ante);
-                TRACE("propagate_cheap_eq", tout << "propagate eq using x-y=0 row:\n"; display_row_info(tout, r););
+                TRACE("arith_eq", tout << "propagate eq using x-y=0 row:\n"; display_row_info(tout, r););
                 m_stats.m_offset_eqs++;
                 propagate_eq_to_core(x, y, ante);
             }
@@ -299,7 +299,7 @@ namespace smt {
                             antecedents ante(*this);
                             collect_fixed_var_justifications(r, ante);
                             collect_fixed_var_justifications(r2, ante);
-                            TRACE("propagate_cheap_eq", tout << "propagate eq two rows:\n"; 
+                            TRACE("arith_eq", tout << "propagate eq two rows:\n"; 
                                   tout << "swapped: " << swapped << "\n";
                                   tout << "x  : v" << x << "\n";
                                   tout << "x2 : v" << x2 << "\n";
@@ -343,7 +343,7 @@ namespace smt {
                     antecedents.eqs().size(), antecedents.eqs().c_ptr(),
                     _x, _y, 
                     antecedents.num_params(), antecedents.params("eq-propagate")));
-        TRACE("propagate_eq_to_core", tout << "detected equality: #" << _x->get_owner_id() << " = #" << _y->get_owner_id() << "\n";
+        TRACE("arith_eq", tout << "detected equality: #" << _x->get_owner_id() << " = #" << _y->get_owner_id() << "\n";
               display_var(tout, x);
               display_var(tout, y););
         ctx.assign_eq(_x, _y, eq_justification(js));

src/smt/theory_datatype.h

@@ -97,6 +97,7 @@ namespace smt {
         virtual void pop_scope_eh(unsigned num_scopes);
         virtual final_check_status final_check_eh();
         virtual void reset_eh();
+        virtual void restart_eh() { m_util.reset(); }
         virtual bool is_shared(theory_var v) const;
     public:
         theory_datatype(ast_manager & m, theory_datatype_params & p);

src/smt/theory_seq.cpp

@@ -249,6 +249,7 @@ final_check_status theory_seq::final_check_eh() {
     }
     m_new_propagation = false;
     TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
+    TRACE("seq_verbose", get_context().display(tout););
     if (simplify_and_solve_eqs()) {
         ++m_stats.m_solve_eqs;
         TRACE("seq", tout << ">>solve_eqs\n";);
@@ -1009,6 +1010,17 @@ bool theory_seq::is_nth(expr* e) const {
     return is_skolem(m_nth, e);
 }
 
+bool theory_seq::is_nth(expr* e, expr*& e1, expr*& e2) const {
+    if (is_nth(e)) {
+        e1 = to_app(e)->get_arg(0);
+        e2 = to_app(e)->get_arg(1);
+        return true;
+    }
+    else {
+        return false;
+    }
+}
+
 bool theory_seq::is_tail(expr* e, expr*& s, unsigned& idx) const {
     rational r;
     return
@@ -1038,6 +1050,10 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) {
     return mk_skolem(m_nth, s, idx, 0, char_sort);
 }
 
+expr_ref theory_seq::mk_sk_ite(expr* c, expr* t, expr* e) {
+    return mk_skolem(symbol("seq.if"), c, t, e, m.get_sort(t));
+}
+
 expr_ref theory_seq::mk_last(expr* s) {
     zstring str;
     if (m_util.str.is_string(s, str) && str.length() > 0) {
@@ -1133,7 +1149,7 @@ bool theory_seq::check_extensionality() {
                     continue;
                 }
                 TRACE("seq", tout << m_lhs << " = " << m_rhs << "\n";);
-                ctx.assume_eq(n1, n2);                
+                ctx.assume_eq(n1, n2);
                 return false;
             }
         }
@@ -2668,6 +2684,13 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
     }
     else if (m.is_ite(e, e1, e2, e3)) {
         literal lit(mk_literal(e1));
+#if 0
+        expr_ref sk_ite = mk_sk_ite(e1, e2, e3);
+        add_axiom(~lit, mk_eq(e2, sk_ite, false));
+        add_axiom( lit, mk_eq(e3, sk_ite, false));
+        result = sk_ite;
+
+#else
         switch (ctx.get_assignment(lit)) {
         case l_true:
             deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit)));
@@ -2684,6 +2707,7 @@ expr_ref theory_seq::expand(expr* e0, dependency*& eqs) {
                   tout << lit << "@ level: " << ctx.get_scope_level() << "\n";);
             break;
         }
+#endif
     }
     else if (m_util.str.is_itos(e, e1)) {
         rational val;
@@ -2902,9 +2926,13 @@ void theory_seq::add_replace_axiom(expr* r) {
     expr_ref xty = mk_concat(x, t, y);
     expr_ref xsy = mk_concat(x, s, y);
     literal cnt = mk_literal(m_util.str.mk_contains(a ,s));
+    literal a_emp = mk_eq_empty(a);
+    literal s_emp = mk_eq_empty(s);
+    add_axiom(~a_emp, mk_seq_eq(r, a));
     add_axiom(cnt,  mk_seq_eq(r, a));
-    add_axiom(~cnt, mk_seq_eq(a, xsy));
+    add_axiom(~s_emp, mk_seq_eq(r, a));
-    add_axiom(~cnt, mk_seq_eq(r, xty));
+    add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(a, xsy));
+    add_axiom(~cnt, a_emp, s_emp, mk_seq_eq(r, xty));
     tightest_prefix(s, x);
 }
 

src/smt/theory_seq.h

@@ -449,10 +449,12 @@ namespace smt {
         bool is_var(expr* b);
         bool add_solution(expr* l, expr* r, dependency* dep);
         bool is_nth(expr* a) const;
+        bool is_nth(expr* a, expr*& e1, expr*& e2) const;
         bool is_tail(expr* a, expr*& s, unsigned& idx) const;
         bool is_eq(expr* e, expr*& a, expr*& b) const; 
         bool is_pre(expr* e, expr*& s, expr*& i);
         bool is_post(expr* e, expr*& s, expr*& i);
+        expr_ref mk_sk_ite(expr* c, expr* t, expr* f);
         expr_ref mk_nth(expr* s, expr* idx);
         expr_ref mk_last(expr* e);
         expr_ref mk_first(expr* e);

src/tactic/bv/dt2bv_tactic.cpp

@@ -112,7 +112,7 @@ class dt2bv_tactic : public tactic {
                 unsigned idx = m_t.m_dt.get_constructor_idx(f);
                 result = m_t.m_bv.mk_numeral(idx, bv_size);
             }
-            else {
+            else if (is_uninterp_const(a)) {
                 // create a fresh variable, add bounds constraints for it.
                 unsigned nc = m_t.m_dt.get_datatype_num_constructors(s);
                 result = m.mk_fresh_const(f->get_name().str().c_str(), m_t.m_bv.mk_sort(bv_size));
@@ -130,6 +130,9 @@ class dt2bv_tactic : public tactic {
                 m_t.m_ext->insert(f, f_def);
                 m_t.m_filter->insert(to_app(result)->get_decl());
             }
+            else {
+                return false;
+            }
             m_cache.insert(a, result);
             ++m_t.m_num_translated;
             return true;