Merge branch 'master' into regex-develop

CMakeLists.txt

@@ -409,6 +409,20 @@ list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT})
 ################################################################################
 include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake)
 
+################################################################################
+# If using Ninja, force color output for Clang (and gcc, disabled to check build).
+################################################################################
+if (UNIX AND CMAKE_GENERATOR STREQUAL "Ninja")
+  if (CMAKE_CXX_COMPILER_ID STREQUAL "Clang")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics")
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fcolor-diagnostics")
+  endif()
+#  if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU")
+#    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color")
+#    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fdiagnostics-color")
+#  endif()
+endif()
+
 ################################################################################
 # Option to control what type of library we build
 ################################################################################
@@ -434,7 +448,7 @@ else()
 endif()
 
 ################################################################################
-# Postion independent code
+# Position independent code
 ################################################################################
 # This is required because code built in the components will end up in a shared
 # library. If not building a shared library ``-fPIC`` isn't needed and would add

configure

@@ -14,4 +14,4 @@ if ! $PYTHON -c "print('testing')" > /dev/null ; then
    exit 1
 fi
 
-$PYTHON scripts/mk_make.py $*
+$PYTHON scripts/mk_make.py "$@"

examples/tptp/tptp5.cpp

@@ -1609,7 +1609,6 @@ public:
                 display_inference(out, "rewrite", "thm", p);
                 break;
             case Z3_OP_PR_PULL_QUANT: 
-            case Z3_OP_PR_PULL_QUANT_STAR: 
                 display_inference(out, "pull_quant", "thm", p);
                 break;
             case Z3_OP_PR_PUSH_QUANT: 
@@ -1669,12 +1668,6 @@ public:
             case Z3_OP_PR_NNF_NEG: 
                 display_inference(out, "nnf_neg", "sab", p); 
                 break;
-            case Z3_OP_PR_NNF_STAR: 
-                display_inference(out, "nnf", "sab", p); 
-                break;
-            case Z3_OP_PR_CNF_STAR: 
-                display_inference(out, "cnf", "sab", p); 
-                break;
             case Z3_OP_PR_SKOLEMIZE:
                 display_inference(out, "skolemize", "sab", p); 
                 break;                
@@ -1706,10 +1699,6 @@ public:
             return display_hyp_inference(out, "modus_ponens", "thm", conclusion, hyp, hyp2);
         }
         case Z3_OP_PR_NNF_POS:
-        case Z3_OP_PR_NNF_STAR: 
-            return display_hyp_inference(out, "nnf", "sab", conclusion, hyp);
-        case Z3_OP_PR_CNF_STAR: 
-            return display_hyp_inference(out, "cnf", "sab", conclusion, hyp);
         case Z3_OP_PR_SKOLEMIZE:
             return display_hyp_inference(out, "skolemize", "sab", conclusion, hyp);
         case Z3_OP_PR_TRANSITIVITY:

scripts/mk_consts_files.py

@@ -72,7 +72,7 @@ def main(args):
 
     if count == 0:
         logging.info('No files generated. You need to specific an output directory'
-                     ' for the relevant langauge bindings')
+                     ' for the relevant language bindings')
     # TODO: Add support for other bindings
     return 0
 

scripts/mk_util.py

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

src/api/api_ast.cpp

@@ -919,7 +919,6 @@ extern "C" {
             case PR_REWRITE: return Z3_OP_PR_REWRITE;
             case PR_REWRITE_STAR: return Z3_OP_PR_REWRITE_STAR;
             case PR_PULL_QUANT: return Z3_OP_PR_PULL_QUANT;
-            case PR_PULL_QUANT_STAR: return Z3_OP_PR_PULL_QUANT_STAR;
             case PR_PUSH_QUANT: return Z3_OP_PR_PUSH_QUANT;
             case PR_ELIM_UNUSED_VARS: return Z3_OP_PR_ELIM_UNUSED_VARS;
             case PR_DER: return Z3_OP_PR_DER;
@@ -936,9 +935,7 @@ extern "C" {
             case PR_IFF_OEQ: return Z3_OP_PR_IFF_OEQ;
             case PR_NNF_POS: return Z3_OP_PR_NNF_POS;
             case PR_NNF_NEG: return Z3_OP_PR_NNF_NEG;
-            case PR_NNF_STAR: return Z3_OP_PR_NNF_STAR;
             case PR_SKOLEMIZE:  return Z3_OP_PR_SKOLEMIZE;
-            case PR_CNF_STAR: return Z3_OP_PR_CNF_STAR;
             case PR_MODUS_PONENS_OEQ: return Z3_OP_PR_MODUS_PONENS_OEQ;
             case PR_TH_LEMMA: return Z3_OP_PR_TH_LEMMA;
             case PR_HYPER_RESOLVE: return Z3_OP_PR_HYPER_RESOLVE;
@@ -1059,6 +1056,7 @@ extern "C" {
             switch(_d->get_decl_kind()) {
             case OP_DT_CONSTRUCTOR:  return Z3_OP_DT_CONSTRUCTOR;
             case OP_DT_RECOGNISER:   return Z3_OP_DT_RECOGNISER;
+            case OP_DT_IS:           return Z3_OP_DT_IS;
             case OP_DT_ACCESSOR:     return Z3_OP_DT_ACCESSOR;
             case OP_DT_UPDATE_FIELD: return Z3_OP_DT_UPDATE_FIELD;
             default:

src/api/api_datatype.cpp

@@ -137,7 +137,7 @@ extern "C" {
             func_decl* decl = (decls)[i];
             mk_c(c)->save_multiple_ast_trail(decl);
             enum_consts[i] = of_func_decl(decl);
-            decl = dt_util.get_constructor_recognizer(decl);
+            decl = dt_util.get_constructor_is(decl);
             mk_c(c)->save_multiple_ast_trail(decl);
             enum_testers[i] = of_func_decl(decl);
         }
@@ -196,7 +196,7 @@ extern "C" {
             *nil_decl = of_func_decl(f);
         }
         if (is_nil_decl) {
-            f = data_util.get_constructor_recognizer(cnstrs[0]);
+            f = data_util.get_constructor_is(cnstrs[0]);
             mk_c(c)->save_multiple_ast_trail(f);
             *is_nil_decl = of_func_decl(f);
         }
@@ -206,7 +206,7 @@ extern "C" {
             *cons_decl = of_func_decl(f);
         }
         if (is_cons_decl) {
-            f = data_util.get_constructor_recognizer(cnstrs[1]);
+            f = data_util.get_constructor_is(cnstrs[1]);
             mk_c(c)->save_multiple_ast_trail(f);
             *is_cons_decl = of_func_decl(f);
         }
@@ -290,7 +290,7 @@ extern "C" {
             *constructor_decl = of_func_decl(f);
         }
         if (tester) {
-            func_decl* f2 = data_util.get_constructor_recognizer(f);
+            func_decl* f2 = data_util.get_constructor_is(f);
             mk_c(c)->save_multiple_ast_trail(f2);
             *tester = of_func_decl(f2);
         }
@@ -497,7 +497,7 @@ extern "C" {
             RETURN_Z3(nullptr);
         }
         func_decl* decl = (decls)[idx];
-        decl = dt_util.get_constructor_recognizer(decl);
+        decl = dt_util.get_constructor_is(decl);
         mk_c(c)->save_ast_trail(decl);
         RETURN_Z3(of_func_decl(decl));
         Z3_CATCH_RETURN(nullptr);

src/api/api_solver.cpp

@@ -17,6 +17,11 @@ Revision History:
 
 --*/
 #include<iostream>
+#include "util/scoped_ctrl_c.h"
+#include "util/cancel_eh.h"
+#include "util/file_path.h"
+#include "util/scoped_timer.h"
+#include "ast/ast_pp.h"
 #include "api/z3.h"
 #include "api/api_log_macros.h"
 #include "api/api_context.h"
@@ -26,14 +31,10 @@ Revision History:
 #include "api/api_stats.h"
 #include "api/api_ast_vector.h"
 #include "solver/tactic2solver.h"
-#include "util/scoped_ctrl_c.h"
+#include "solver/smt_logics.h"
-#include "util/cancel_eh.h"
-#include "util/file_path.h"
-#include "util/scoped_timer.h"
 #include "tactic/portfolio/smt_strategic_solver.h"
 #include "smt/smt_solver.h"
 #include "smt/smt_implied_equalities.h"
-#include "solver/smt_logics.h"
 #include "cmd_context/cmd_context.h"
 #include "parsers/smt2/smt2parser.h"
 #include "sat/dimacs.h"

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

@@ -989,7 +989,7 @@ namespace z3 {
 
         /**
            \brief sequence and regular expression operations.
-           + is overloaeded as sequence concatenation and regular expression union.
+           + is overloaded as sequence concatenation and regular expression union.
            concat is overloaded to handle sequences and regular expressions
         */
         expr extract(expr const& offset, expr const& length) const { 

src/api/dotnet/Context.cs

@@ -2515,7 +2515,7 @@ namespace Microsoft.Z3
 
 
         /// <summary>
-        /// Concatentate sequences.
+        /// Concatenate sequences.
         /// </summary>
         public SeqExpr MkConcat(params SeqExpr[] t)
         {
@@ -3597,7 +3597,7 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty)
+        /// Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty)
         /// or trivially unsatisfiable (i.e., contains `false').
         /// </summary>
         public Tactic FailIfNotDecided()
@@ -4656,7 +4656,7 @@ namespace Microsoft.Z3
         /// Conversion of a floating-point term into a bit-vector.
         /// </summary>
         /// <remarks>
-        /// Produces a term that represents the conversion of the floating-poiunt term t into a
+        /// Produces a term that represents the conversion of the floating-point term t into a
         /// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary,
         /// the result will be rounded according to rounding mode rm.
         /// </remarks>
@@ -4677,7 +4677,7 @@ namespace Microsoft.Z3
         /// Conversion of a floating-point term into a real-numbered term.
         /// </summary>
         /// <remarks>
-        /// Produces a term that represents the conversion of the floating-poiunt term t into a
+        /// Produces a term that represents the conversion of the floating-point term t into a
         /// real number. Note that this type of conversion will often result in non-linear
         /// constraints over real terms.
         /// </remarks>
@@ -4696,7 +4696,7 @@ namespace Microsoft.Z3
         /// <remarks>
         /// The size of the resulting bit-vector is automatically determined. Note that
         /// IEEE 754-2008 allows multiple different representations of NaN. This conversion
-        /// knows only one NaN and it will always produce the same bit-vector represenatation of
+        /// knows only one NaN and it will always produce the same bit-vector representation of
         /// that NaN.
         /// </remarks>
         /// <param name="t">FloatingPoint term.</param>

src/api/dotnet/Expr.cs

@@ -932,7 +932,7 @@ namespace Microsoft.Z3
         /// Indicates whether the term is a proof by condensed transitivity of a relation
         /// </summary>
         /// <remarks>
-        /// Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
+        /// Condensed transitivity proof. 
         /// It combines several symmetry and transitivity proofs.
         /// Example:
         /// T1: (R a b)
@@ -1035,14 +1035,11 @@ namespace Microsoft.Z3
         /// </summary>
         /// <remarks>
         /// A proof for rewriting an expression t into an expression s.
-        /// This proof object is used if the parameter PROOF_MODE is 1.
         /// This proof object can have n antecedents.
         /// The antecedents are proofs for equalities used as substitution rules.
-        /// The object is also used in a few cases if the parameter PROOF_MODE is 2.
+        /// The object is used in a few cases:
-        /// The cases are:
         /// - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
         /// - When converting bit-vectors to Booleans (BIT2BOOL=true)
-        /// - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
         /// </remarks>
         public bool IsProofRewriteStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_REWRITE_STAR; } }
 
@@ -1054,15 +1051,6 @@ namespace Microsoft.Z3
         /// </remarks>
         public bool IsProofPullQuant { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT; } }
 
-        /// <summary>
-        /// Indicates whether the term is a proof for pulling quantifiers out.
-        /// </summary>
-        /// <remarks>
-        /// A proof for (iff P Q) where Q is in prenex normal form.
-        /// This proof object is only used if the parameter PROOF_MODE is 1.
-        /// This proof object has no antecedents
-        /// </remarks>
-        public bool IsProofPullQuantStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR; } }
 
         /// <summary>
         /// Indicates whether the term is a proof for pushing quantifiers in.
@@ -1304,28 +1292,6 @@ namespace Microsoft.Z3
         /// </remarks>
         public bool IsProofNNFNeg { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_NEG; } }
 
-        /// <summary>
-        /// Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
-        /// </summary>
-        /// <remarks>
-        /// A proof for (~ P Q) where Q is in negation normal form.
-        ///
-        /// This proof object is only used if the parameter PROOF_MODE is 1.
-        ///
-        /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
-        /// </remarks>
-        public bool IsProofNNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_NNF_STAR; } }
-
-        /// <summary>
-        /// Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
-        /// </summary>
-        /// <remarks>
-        /// A proof for (~ P Q) where Q is in conjunctive normal form.
-        /// This proof object is only used if the parameter PROOF_MODE is 1.
-        /// This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
-        /// </remarks>
-        public bool IsProofCNFStar { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_PR_CNF_STAR; } }
-
         /// <summary>
         /// Indicates whether the term is a proof for a Skolemization step
         /// </summary>

src/api/java/Context.java

@@ -1978,7 +1978,7 @@ public class Context implements AutoCloseable {
     }
     
     /**
-     * Concatentate sequences.
+     * Concatenate sequences.
      */
     public SeqExpr mkConcat(SeqExpr... t)
     {
@@ -2781,7 +2781,7 @@ public class Context implements AutoCloseable {
     }
 
     /**
-     * Create a tactic that fails if the goal is not triviall satisfiable (i.e.,
+     * Create a tactic that fails if the goal is not trivially satisfiable (i.e.,
      * empty) or trivially unsatisfiable (i.e., contains `false').
      **/
     public Tactic failIfNotDecided()
@@ -3769,7 +3769,7 @@ public class Context implements AutoCloseable {
      * @param sz Size of the resulting bit-vector.
      * @param signed Indicates whether the result is a signed or unsigned bit-vector.
      * Remarks:
-     * Produces a term that represents the conversion of the floating-poiunt term t into a
+     * Produces a term that represents the conversion of the floating-point term t into a
      * bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, 
      * the result will be rounded according to rounding mode rm.        
      * @throws Z3Exception 
@@ -3786,7 +3786,7 @@ public class Context implements AutoCloseable {
      * Conversion of a floating-point term into a real-numbered term.
      * @param t FloatingPoint term
      * Remarks:
-     * Produces a term that represents the conversion of the floating-poiunt term t into a
+     * Produces a term that represents the conversion of the floating-point term t into a
      * real number. Note that this type of conversion will often result in non-linear 
      * constraints over real terms.
      * @throws Z3Exception 
@@ -3802,7 +3802,7 @@ public class Context implements AutoCloseable {
      * Remarks:
      * The size of the resulting bit-vector is automatically determined. Note that 
      * IEEE 754-2008 allows multiple different representations of NaN. This conversion 
-     * knows only one NaN and it will always produce the same bit-vector represenatation of 
+     * knows only one NaN and it will always produce the same bit-vector representation of
      * that NaN. 
      * @throws Z3Exception 
      **/

src/api/java/Expr.java

@@ -1398,8 +1398,7 @@ public class Expr extends AST
     /**
      * Indicates whether the term is a proof by condensed transitivity of a
      * relation
-     * Remarks:  Condensed transitivity proof. This proof object is
+     * Remarks:  Condensed transitivity proof. It combines several symmetry
-     * only used if the parameter PROOF_MODE is 1. It combines several symmetry
      * and transitivity proofs. Example: T1: (R a b) T2: (R c b) T3: (R c d)
      * [trans* T1 T2 T3]: (R a d) R must be a symmetric and transitive relation.
      * 
@@ -1506,14 +1505,11 @@ public class Expr extends AST
     /**
      * Indicates whether the term is a proof by rewriting
      * Remarks:  A proof for
-     * rewriting an expression t into an expression s. This proof object is used
+     * rewriting an expression t into an expression s. This proof object can have n
-     * if the parameter PROOF_MODE is 1. This proof object can have n
      * antecedents. The antecedents are proofs for equalities used as
-     * substitution rules. The object is also used in a few cases if the
+     * substitution rules. The object is used in a few cases . The cases are: - When applying contextual
-     * parameter PROOF_MODE is 2. The cases are: - When applying contextual
      * simplification (CONTEXT_SIMPLIFIER=true) - When converting bit-vectors to
-     * Booleans (BIT2BOOL=true) - When pulling ite expression up
+     * Booleans (BIT2BOOL=true) 
-     * (PULL_CHEAP_ITE_TREES=true) 
      * @throws Z3Exception on error
      * @return a boolean
      **/
@@ -1534,17 +1530,6 @@ public class Expr extends AST
         return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT;
     }
 
-    /**
-     * Indicates whether the term is a proof for pulling quantifiers out.
-     * 
-     * Remarks:  A proof for (iff P Q) where Q is in prenex normal form. This * proof object is only used if the parameter PROOF_MODE is 1. This proof * object has no antecedents 
-     * @throws Z3Exception on error
-     * @return a boolean
-     **/
-    public boolean isProofPullQuantStar()
-    {
-        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_PULL_QUANT_STAR;
-    }
 
     /**
      * Indicates whether the term is a proof for pushing quantifiers in.
@@ -1804,38 +1789,6 @@ public class Expr extends AST
         return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_NEG;
     }
 
-    /**
-     * Indicates whether the term is a proof for (~ P Q) here Q is in negation
-     * normal form.
-     * Remarks:  A proof for (~ P Q) where Q is in negation normal
-     * form.
-     * 
-     * This proof object is only used if the parameter PROOF_MODE is 1.
-     * 
-     * This proof object may have n antecedents. Each antecedent is a
-     * PR_DEF_INTRO. 
-     * @throws Z3Exception on error
-     * @return a boolean
-     **/
-    public boolean isProofNNFStar()
-    {
-        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_NNF_STAR;
-    }
-
-    /**
-     * Indicates whether the term is a proof for (~ P Q) where Q is in
-     * conjunctive normal form.
-     * Remarks:  A proof for (~ P Q) where Q is in
-     * conjunctive normal form. This proof object is only used if the parameter
-     * PROOF_MODE is 1. This proof object may have n antecedents. Each
-     * antecedent is a PR_DEF_INTRO. 
-     * @throws Z3Exception on error
-     * @return a boolean
-     **/
-    public boolean isProofCNFStar()
-    {
-        return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_PR_CNF_STAR;
-    }
 
     /**
      * Indicates whether the term is a proof for a Skolemization step

src/api/python/z3/z3.py

@@ -2428,7 +2428,7 @@ def is_rational_value(a):
     return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
 
 def is_algebraic_value(a):
-    """Return `True` if `a` is an algerbraic value of sort Real.
+    """Return `True` if `a` is an algebraic value of sort Real.
 
     >>> is_algebraic_value(RealVal("3/5"))
     False
@@ -4437,7 +4437,7 @@ class Datatype:
         """Declare constructor named `name` with the given accessors `args`.
         Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort or a reference to the datatypes being declared.
 
-        In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
+        In the following example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
         declares the constructor named `cons` that builds a new List using an integer and a List.
         It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
         and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create
@@ -4451,13 +4451,13 @@ class Datatype:
         if __debug__:
             _z3_assert(isinstance(name, str), "String expected")
             _z3_assert(name != "", "Constructor name cannot be empty")
-        return self.declare_core(name, "is_" + name, *args)
+        return self.declare_core(name, "is-" + name, *args)
 
     def __repr__(self):
         return "Datatype(%s, %s)" % (self.name, self.constructors)
 
     def create(self):
-        """Create a Z3 datatype based on the constructors declared using the mehtod `declare()`.
+        """Create a Z3 datatype based on the constructors declared using the method `declare()`.
 
         The function `CreateDatatypes()` must be used to define mutually recursive datatypes.
 
@@ -4575,7 +4575,7 @@ def CreateDatatypes(*ds):
                 cref = cref()
             setattr(dref, cref_name, cref)
             rref  = dref.recognizer(j)
-            setattr(dref, rref.name(), rref)
+            setattr(dref, "is_" + cref_name, rref)
             for k in range(cref_arity):
                 aref = dref.accessor(j, k)
                 setattr(dref, aref.name(), aref)
@@ -4629,16 +4629,16 @@ class DatatypeSortRef(SortRef):
         >>> List.num_constructors()
         2
         >>> List.recognizer(0)
-        is_cons
+        is(cons)
         >>> List.recognizer(1)
-        is_nil
+        is(nil)
         >>> simplify(List.is_nil(List.cons(10, List.nil)))
         False
         >>> simplify(List.is_cons(List.cons(10, List.nil)))
         True
         >>> l = Const('l', List)
         >>> simplify(List.is_cons(l))
-        is_cons(l)
+        is(cons, l)
         """
         if __debug__:
             _z3_assert(idx < self.num_constructors(), "Invalid recognizer index")
@@ -6818,8 +6818,8 @@ class FiniteDomainSortRef(SortRef):
 
     def size(self):
         """Return the size of the finite domain sort"""
-        r = (ctype.c_ulonglong * 1)()
+        r = (ctypes.c_ulonglong * 1)()
-        if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast(), r):
+        if Z3_get_finite_domain_sort_size(self.ctx_ref(), self.ast, r):
             return r[0]
         else:
             raise Z3Exception("Failed to retrieve finite domain sort size")
@@ -7447,6 +7447,19 @@ def With(t, *args, **keys):
     p = args2params(args, keys, t.ctx)
     return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
 
+def WithParams(t, p):
+    """Return a tactic that applies tactic `t` using the given configuration options.
+
+    >>> x, y = Ints('x y')
+    >>> p = ParamsRef()
+    >>> p.set("som", True)
+    >>> t = WithParams(Tactic('simplify'), p)
+    >>> t((x + 1)*(y + 2) == 0)
+    [[2*x + y + x*y == -2]]
+    """
+    t = _to_tactic(t, None)
+    return Tactic(Z3_tactic_using_params(t.ctx.ref(), t.tactic, p.params), t.ctx)
+
 def Repeat(t, max=4294967295, ctx=None):
     """Return a tactic that keeps applying `t` until the goal is not modified anymore or the maximum number of iterations `max` is reached.
 
@@ -8253,7 +8266,7 @@ def tree_interpolant(pat,p=None,ctx=None):
     solver that determines satisfiability.
 
     >>> x = Int('x')
-    >>> y = Int('y')
+    >>> y = Int('y')	
     >>> print(tree_interpolant(And(Interpolant(x < 0), Interpolant(y > 2), x == y)))
     [Not(x >= 0), Not(y <= 2)]
 
@@ -8861,7 +8874,7 @@ class FPNumRef(FPRef):
     def isSubnormal(self):
         return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
 
-    """Indicates whether the numeral is postitive."""
+    """Indicates whether the numeral is positive."""
     def isPositive(self):
         return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
 
@@ -9657,7 +9670,7 @@ def fpToIEEEBV(x, ctx=None):
     The size of the resulting bit-vector is automatically determined.
 
     Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
-    knows only one NaN and it will always produce the same bit-vector represenatation of
+    knows only one NaN and it will always produce the same bit-vector representation of
     that NaN.
 
     >>> x = FP('x', FPSort(8, 24))
@@ -9832,7 +9845,7 @@ def Empty(s):
     raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
 
 def Full(s):
-    """Create the regular expression that accepts the universal langauge
+    """Create the regular expression that accepts the universal language
     >>> e = Full(ReSort(SeqSort(IntSort())))
     >>> print(e)
     re.all

src/api/python/z3/z3printer.py

@@ -485,7 +485,9 @@ class PP:
             raise StopPPException()
 
     def pp(self, f, indent):
-        if f.is_string():
+        if isinstance(f, str):
+            sef.pp_string(f, indent)
+        elif f.is_string():
             self.pp_string(f, indent)
         elif f.is_indent():
             self.pp(f.child, min(indent + f.indent, self.max_indent))
@@ -846,10 +848,17 @@ class Formatter:
         else:
             return seq1('MultiPattern', [ self.pp_expr(arg, d+1, xs) for arg in a.children() ])
 
+    def pp_is(self, a, d, xs):
+        f  = a.params()[0]
+        return self.pp_fdecl(f, a, d, xs)
+
     def pp_map(self, a, d, xs):
+        f  = z3.get_map_func(a)
+        return self.pp_fdecl(f, a, d, xs)
+
+    def pp_fdecl(self, f, a, d, xs):
         r  = []
         sz = 0
-        f  = z3.get_map_func(a)
         r.append(to_format(f.name()))
         for child in a.children(): 
             r.append(self.pp_expr(child, d+1, xs))
@@ -909,6 +918,8 @@ class Formatter:
                 return self.pp_unary_param(a, d, xs)
             elif k == Z3_OP_EXTRACT:
                 return self.pp_extract(a, d, xs)
+            elif k == Z3_OP_DT_IS:
+                return self.pp_is(a, d, xs)
             elif k == Z3_OP_ARRAY_MAP:
                 return self.pp_map(a, d, xs)
             elif k == Z3_OP_CONST_ARRAY:
@@ -963,6 +974,14 @@ class Formatter:
         else:
             return to_format(self.pp_unknown())
 
+    def pp_decl(self, f):
+        k = f.kind()
+        if k == Z3_OP_DT_IS or k == Z3_OP_ARRAY_MAP:
+           g  = f.params()[0]
+           r = [ to_format(g.name()) ]
+           return seq1(self.pp_name(f), r)
+        return self.pp_name(f)        
+
     def pp_seq_core(self, f, a, d, xs):
         self.visited = self.visited + 1
         if d > self.max_depth or self.visited > self.max_visited:
@@ -1054,7 +1073,7 @@ class Formatter:
         elif z3.is_sort(a):
             return self.pp_sort(a)
         elif z3.is_func_decl(a):
-            return self.pp_name(a)
+            return self.pp_decl(a)
         elif isinstance(a, z3.Goal) or isinstance(a, z3.AstVector):
             return self.pp_seq(a, 0, [])
         elif isinstance(a, z3.Solver):

src/api/z3.h

@@ -21,7 +21,8 @@ Notes:
 #ifndef Z3_H_
 #define Z3_H_
 
-#include<stdio.h>
+#include <stdio.h>
+#include <stdbool.h>
 #include "z3_macros.h"
 #include "z3_api.h"
 #include "z3_ast_containers.h"

src/api/z3_api.h

@@ -459,7 +459,7 @@ typedef enum
        [trans T1 T2]: (R t u)
        }
 
-   - Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof. This proof object is only used if the parameter PROOF_MODE is 1.
+   - Z3_OP_PR_TRANSITIVITY_STAR: Condensed transitivity proof. 
      It combines several symmetry and transitivity proofs.
 
           Example:
@@ -539,21 +539,14 @@ typedef enum
           }
 
    - Z3_OP_PR_REWRITE_STAR: A proof for rewriting an expression t into an expression s.
-       This proof object is used if the parameter PROOF_MODE is 1.
        This proof object can have n antecedents.
        The antecedents are proofs for equalities used as substitution rules.
-       The object is also used in a few cases if the parameter PROOF_MODE is 2.
+       The proof rule is used in a few cases. The cases are:
-       The cases are:
          - When applying contextual simplification (CONTEXT_SIMPLIFIER=true)
          - When converting bit-vectors to Booleans (BIT2BOOL=true)
-         - When pulling ite expression up (PULL_CHEAP_ITE_TREES=true)
 
    - Z3_OP_PR_PULL_QUANT: A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents.
 
-   - Z3_OP_PR_PULL_QUANT_STAR: A proof for (iff P Q) where Q is in prenex normal form.
-       This proof object is only used if the parameter PROOF_MODE is 1.
-       This proof object has no antecedents.
-
    - Z3_OP_PR_PUSH_QUANT: A proof for:
 
        \nicebox{
@@ -726,15 +719,6 @@ typedef enum
          [nnf-neg T1 T2 T3 T4]: (~ (not (iff s_1 s_2))
                                    (and (or r_1 r_2) (or r_1' r_2')))
        }
-   - Z3_OP_PR_NNF_STAR: A proof for (~ P Q) where Q is in negation normal form.
-
-       This proof object is only used if the parameter PROOF_MODE is 1.
-
-       This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
-
-   - Z3_OP_PR_CNF_STAR: A proof for (~ P Q) where Q is in conjunctive normal form.
-       This proof object is only used if the parameter PROOF_MODE is 1.
-       This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO.
 
    - Z3_OP_PR_SKOLEMIZE: Proof for:
 
@@ -876,6 +860,8 @@ typedef enum
 
       - Z3_OP_DT_RECOGNISER: datatype recognizer.
 
+      - Z3_OP_DT_IS: datatype recognizer.
+
       - Z3_OP_DT_ACCESSOR: datatype accessor.
 
       - Z3_OP_DT_UPDATE_FIELD: datatype field update.
@@ -1140,7 +1126,6 @@ typedef enum {
     Z3_OP_PR_REWRITE,
     Z3_OP_PR_REWRITE_STAR,
     Z3_OP_PR_PULL_QUANT,
-    Z3_OP_PR_PULL_QUANT_STAR,
     Z3_OP_PR_PUSH_QUANT,
     Z3_OP_PR_ELIM_UNUSED_VARS,
     Z3_OP_PR_DER,
@@ -1157,8 +1142,6 @@ typedef enum {
     Z3_OP_PR_IFF_OEQ,
     Z3_OP_PR_NNF_POS,
     Z3_OP_PR_NNF_NEG,
-    Z3_OP_PR_NNF_STAR,
-    Z3_OP_PR_CNF_STAR,
     Z3_OP_PR_SKOLEMIZE,
     Z3_OP_PR_MODUS_PONENS_OEQ,
     Z3_OP_PR_TH_LEMMA,
@@ -1220,6 +1203,7 @@ typedef enum {
     // Datatypes
     Z3_OP_DT_CONSTRUCTOR=0x800,
     Z3_OP_DT_RECOGNISER,
+    Z3_OP_DT_IS,
     Z3_OP_DT_ACCESSOR,
     Z3_OP_DT_UPDATE_FIELD,
 
@@ -1474,7 +1458,6 @@ extern "C" {
     /*@{*/
 
     /**
-        \deprecated
         \brief Create a configuration object for the Z3 context object.
 
         Configurations are created in order to assign parameters prior to creating
@@ -1507,7 +1490,6 @@ extern "C" {
     Z3_config Z3_API Z3_mk_config(void);
 
     /**
-        \deprecated
         \brief Delete the given configuration object.
 
         \sa Z3_mk_config
@@ -1517,7 +1499,6 @@ extern "C" {
     void Z3_API Z3_del_config(Z3_config c);
 
     /**
-        \deprecated
         \brief Set a configuration parameter.
 
         The following parameters can be set for
@@ -1534,7 +1515,6 @@ extern "C" {
     /*@{*/
 
     /**
-       \deprecated
        \brief Create a context using the given configuration.
 
        After a context is created, the configuration cannot be changed,
@@ -1614,7 +1594,6 @@ extern "C" {
     void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a);
 
     /**
-       \deprecated
        \brief Set a value of a context parameter.
 
        \sa Z3_global_param_set

src/api/z3_fpa.h

@@ -756,7 +756,7 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into an unsigned bit-vector.
 
-        Produces a term that represents the conversion of the floating-poiunt term t into a
+        Produces a term that represents the conversion of the floating-point term t into a
         bit-vector term of size sz in unsigned 2's complement format. If necessary, the result
         will be rounded according to rounding mode rm.
 
@@ -772,7 +772,7 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into a signed bit-vector.
 
-        Produces a term that represents the conversion of the floating-poiunt term t into a
+        Produces a term that represents the conversion of the floating-point term t into a
         bit-vector term of size sz in signed 2's complement format. If necessary, the result
         will be rounded according to rounding mode rm.
 
@@ -788,7 +788,7 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into a real-numbered term.
 
-        Produces a term that represents the conversion of the floating-poiunt term t into a
+        Produces a term that represents the conversion of the floating-point term t into a
         real number. Note that this type of conversion will often result in non-linear
         constraints over real terms.
 
@@ -1011,7 +1011,7 @@ extern "C" {
         determined.
 
         Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
-        knows only one NaN and it will always produce the same bit-vector represenatation of
+        knows only one NaN and it will always produce the same bit-vector representation of
         that NaN.
 
         def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))

src/api/z3_interp.h

@@ -98,7 +98,7 @@ extern "C" {
 
         Interpolant may not necessarily be computable from all
         proofs. To be sure an interpolant can be computed, the proof
-        must be generated by an SMT solver for which interpoaltion is
+        must be generated by an SMT solver for which interpolation is
         supported, and the premises must be expressed using only
         theories and operators for which interpolation is supported.
 
@@ -199,7 +199,7 @@ extern "C" {
        (implies (and c1 ... cn f) v)
 
        where c1 .. cn are the children of v (which must precede v in the file)
-       and f is the formula assiciated to node v. The last formula in the
+       and f is the formula associated to node v. The last formula in the
        file is the root vertex, and is represented by the predicate "false".
 
        A solution to a tree interpolation problem can be thought of as a

src/ast/ast.cpp

@@ -663,7 +663,6 @@ basic_decl_plugin::basic_decl_plugin():
     m_not_or_elim_decl(nullptr),
     m_rewrite_decl(nullptr),
     m_pull_quant_decl(nullptr),
-    m_pull_quant_star_decl(nullptr),
     m_push_quant_decl(nullptr),
     m_elim_unused_vars_decl(nullptr),
     m_der_decl(nullptr),
@@ -827,7 +826,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
     case PR_REWRITE:                      return mk_proof_decl("rewrite", k, 0, m_rewrite_decl);
     case PR_REWRITE_STAR:                 return mk_proof_decl("rewrite*", k, num_parents, m_rewrite_star_decls);
     case PR_PULL_QUANT:                   return mk_proof_decl("pull-quant", k, 0, m_pull_quant_decl);
-    case PR_PULL_QUANT_STAR:              return mk_proof_decl("pull-quant*", k, 0, m_pull_quant_star_decl);
     case PR_PUSH_QUANT:                   return mk_proof_decl("push-quant", k, 0, m_push_quant_decl);
     case PR_ELIM_UNUSED_VARS:             return mk_proof_decl("elim-unused", k, 0, m_elim_unused_vars_decl);
     case PR_DER:                          return mk_proof_decl("der", k, 0, m_der_decl);
@@ -844,8 +842,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
     case PR_IFF_OEQ:                      return mk_proof_decl("iff~", k, 1, m_iff_oeq_decl);
     case PR_NNF_POS:                      return mk_proof_decl("nnf-pos", k, num_parents, m_nnf_pos_decls);
     case PR_NNF_NEG:                      return mk_proof_decl("nnf-neg", k, num_parents, m_nnf_neg_decls);
-    case PR_NNF_STAR:                     return mk_proof_decl("nnf*", k, num_parents, m_nnf_star_decls);
-    case PR_CNF_STAR:                     return mk_proof_decl("cnf*", k, num_parents, m_cnf_star_decls);
     case PR_SKOLEMIZE:                    return mk_proof_decl("sk", k, 0, m_skolemize_decl);
     case PR_MODUS_PONENS_OEQ:             return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl);
     case PR_TH_LEMMA:                     return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls);
@@ -949,7 +945,6 @@ void basic_decl_plugin::finalize() {
     DEC_REF(m_not_or_elim_decl);
     DEC_REF(m_rewrite_decl);
     DEC_REF(m_pull_quant_decl);
-    DEC_REF(m_pull_quant_star_decl);
     DEC_REF(m_push_quant_decl);
     DEC_REF(m_elim_unused_vars_decl);
     DEC_REF(m_der_decl);
@@ -975,8 +970,6 @@ void basic_decl_plugin::finalize() {
     DEC_ARRAY_REF(m_apply_def_decls);
     DEC_ARRAY_REF(m_nnf_pos_decls);
     DEC_ARRAY_REF(m_nnf_neg_decls);
-    DEC_ARRAY_REF(m_nnf_star_decls);
-    DEC_ARRAY_REF(m_cnf_star_decls);
 
     DEC_ARRAY_REF(m_th_lemma_decls);
     DEC_REF(m_hyper_res_decl0);
@@ -1532,32 +1525,39 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
               tout << "fid: " << fid << " fidname: " << get_family_name(fid) << "\n";
           });
     ast_translation trans(const_cast<ast_manager&>(from), *this, false);
+    // Inheriting plugins can create new family ids. Since new family ids are
+    // assigned in the order that they are created, this can result in differing
+    // family ids. To avoid this, we first assign all family ids and only then inherit plugins.
     for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
-      SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
+        symbol fid_name   = from.get_family_name(fid);
-      SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
+        if (!m_family_manager.has_family(fid)) {
-      symbol fid_name   = from.get_family_name(fid);
+            family_id new_fid = mk_family_id(fid_name);
-      TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid
+            (void)new_fid;
-            << ", target has_family: " << m_family_manager.has_family(fid) << "\n";
+            TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
-            if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
+        }
-      if (!m_family_manager.has_family(fid)) {
+    }
-          family_id new_fid = mk_family_id(fid_name);
+    for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
-          (void)new_fid;
+        SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
-          TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
+        SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
-      }
+        symbol fid_name   = from.get_family_name(fid);
-      TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
+        (void)fid_name;
-      SASSERT(fid == get_family_id(fid_name));
+        TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid
-      if (from.has_plugin(fid) && !has_plugin(fid)) {
+              << ", target has_family: " << m_family_manager.has_family(fid) << "\n";
-          decl_plugin * new_p = from.get_plugin(fid)->mk_fresh();
+              if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
-          register_plugin(fid, new_p);
+        TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
-          SASSERT(new_p->get_family_id() == fid);
+        SASSERT(fid == get_family_id(fid_name));
-          SASSERT(has_plugin(fid));
+        if (from.has_plugin(fid) && !has_plugin(fid)) {
-      }
+            decl_plugin * new_p = from.get_plugin(fid)->mk_fresh();
-      if (from.has_plugin(fid)) {
+            register_plugin(fid, new_p);
-          get_plugin(fid)->inherit(from.get_plugin(fid), trans);
+            SASSERT(new_p->get_family_id() == fid);
-      }
+            SASSERT(has_plugin(fid));
-      SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
+        }
-      SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
+        if (from.has_plugin(fid)) {
-      SASSERT(!from.has_plugin(fid) || has_plugin(fid));
+            get_plugin(fid)->inherit(from.get_plugin(fid), trans);
+        }
+        SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
+        SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
+        SASSERT(!from.has_plugin(fid) || has_plugin(fid));
     }
 }
 
@@ -2837,12 +2837,6 @@ proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
     return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q));
 }
 
-proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) {
-    if (proofs_disabled())
-        return nullptr;
-    return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q));
-}
-
 proof * ast_manager::mk_push_quant(quantifier * q, expr * e) {
     if (proofs_disabled())
         return nullptr;
@@ -3087,15 +3081,6 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof *
     return mk_app(m_basic_family_id, PR_NNF_NEG, args.size(), args.c_ptr());
 }
 
-proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
-    if (proofs_disabled())
-        return nullptr;
-    ptr_buffer<expr> args;
-    args.append(num_proofs, (expr**) proofs);
-    args.push_back(mk_oeq(s, t));
-    return mk_app(m_basic_family_id, PR_NNF_STAR, args.size(), args.c_ptr());
-}
-
 proof * ast_manager::mk_skolemization(expr * q, expr * e) {
     if (proofs_disabled())
         return nullptr;
@@ -3104,15 +3089,6 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) {
     return mk_app(m_basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e));
 }
 
-proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
-    if (proofs_disabled())
-        return nullptr;
-    ptr_buffer<expr> args;
-    args.append(num_proofs, (expr**) proofs);
-    args.push_back(mk_oeq(s, t));
-    return mk_app(m_basic_family_id, PR_CNF_STAR, args.size(), args.c_ptr());
-}
-
 proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
     if (proofs_disabled())
         return nullptr;

src/ast/ast.h

@@ -1042,11 +1042,11 @@ enum basic_op_kind {
 
     PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO,
     PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT,
-    PR_PULL_QUANT_STAR, PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
+    PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
 
     PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM,
 
-    PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR,
+    PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_SKOLEMIZE, 
     PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR
 };
 
@@ -1080,7 +1080,6 @@ protected:
     func_decl * m_not_or_elim_decl;
     func_decl * m_rewrite_decl;
     func_decl * m_pull_quant_decl;
-    func_decl * m_pull_quant_star_decl;
     func_decl * m_push_quant_decl;
     func_decl * m_elim_unused_vars_decl;
     func_decl * m_der_decl;
@@ -1106,8 +1105,6 @@ protected:
     ptr_vector<func_decl> m_apply_def_decls;
     ptr_vector<func_decl> m_nnf_pos_decls;
     ptr_vector<func_decl> m_nnf_neg_decls;
-    ptr_vector<func_decl> m_nnf_star_decls;
-    ptr_vector<func_decl> m_cnf_star_decls;
 
     ptr_vector<func_decl> m_th_lemma_decls;
     func_decl * m_hyper_res_decl0;
@@ -2182,7 +2179,6 @@ public:
     proof * mk_oeq_rewrite(expr * s, expr * t);
     proof * mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
     proof * mk_pull_quant(expr * e, quantifier * q);
-    proof * mk_pull_quant_star(expr * e, quantifier * q);
     proof * mk_push_quant(quantifier * q, expr * e);
     proof * mk_elim_unused_vars(quantifier * q, expr * r);
     proof * mk_der(quantifier * q, expr * r);
@@ -2201,9 +2197,8 @@ public:
 
     proof * mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
     proof * mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
-    proof * mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
     proof * mk_skolemization(expr * q, expr * e);
-    proof * mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
+
 
     proof * mk_and_elim(proof * p, unsigned i);
     proof * mk_not_or_elim(proof * p, unsigned i);

src/ast/ast_pp_util.cpp

@@ -38,6 +38,7 @@ void ast_pp_util::collect(expr_ref_vector const& es) {
 void ast_pp_util::display_decls(std::ostream& out) {
     smt2_pp_environment_dbg env(m);
     ast_smt_pp pp(m);
+    coll.order_deps();
     unsigned n = coll.get_num_sorts();
     for (unsigned i = 0; i < n; ++i) {
         pp.display_ast_smt2(out, coll.get_sorts()[i], 0, 0, nullptr);
@@ -45,13 +46,18 @@ void ast_pp_util::display_decls(std::ostream& out) {
     n = coll.get_num_decls();
     for (unsigned i = 0; i < n; ++i) {
         func_decl* f = coll.get_func_decls()[i];
-        if (f->get_family_id() == null_family_id) {
+        if (f->get_family_id() == null_family_id && !m_removed.contains(f)) {
             ast_smt2_pp(out, f, env);
             out << "\n";
         }
     }
 }
 
+void ast_pp_util::remove_decl(func_decl* f) {
+    m_removed.insert(f);
+}
+
+
 void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) {
     if (neat) {
         smt2_pp_environment_dbg env(m);

src/ast/ast_pp_util.h

@@ -20,9 +20,11 @@ Revision History:
 #define AST_PP_UTIL_H_
 
 #include "ast/decl_collector.h"
+#include "util/obj_hashtable.h"
 
 class ast_pp_util {
     ast_manager&        m;
+    obj_hashtable<func_decl> m_removed;
  public:        
 
     decl_collector      coll;
@@ -35,6 +37,8 @@ class ast_pp_util {
 
     void collect(expr_ref_vector const& es);
 
+    void remove_decl(func_decl* f);
+
     void display_decls(std::ostream& out);
 
     void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true);

src/ast/ast_smt_pp.cpp

@@ -952,6 +952,10 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
         strm << "; " << m_attributes.c_str();
     }
 
+#if 0
+    decls.display_decls(strm);
+#else
+    decls.order_deps();
     ast_mark sort_mark;
     for (unsigned i = 0; i < decls.get_num_sorts(); ++i) {
         sort* s = decls.get_sorts()[i];
@@ -978,18 +982,19 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
             strm << "\n";
         }
     }
+#endif
 
-    for (unsigned i = 0; i < m_assumptions.size(); ++i) {
+    for (expr* a : m_assumptions) {
         smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
         strm << "(assert\n ";
-        p(m_assumptions[i].get());
+        p(a);
         strm << ")\n";
     }
 
-    for (unsigned i = 0; i < m_assumptions_star.size(); ++i) {
+    for (expr* a : m_assumptions_star) {
         smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
         strm << "(assert\n ";
-        p(m_assumptions_star[i].get());
+        p(a);
         strm << ")\n";
     }
 

src/ast/datatype_decl_plugin.cpp

@@ -791,6 +791,14 @@ namespace datatype {
         return res;
     }
 
+
+    func_decl * util::get_constructor_is(func_decl * con) {
+        SASSERT(is_constructor(con));
+        sort * datatype = con->get_range();
+        parameter ps[1] = { parameter(con)};
+        return m.mk_func_decl(m_family_id, OP_DT_IS, 1, ps, 1, &datatype);
+    }
+
     func_decl * util::get_constructor_recognizer(func_decl * con) {
         SASSERT(is_constructor(con));
         func_decl * d = nullptr;
@@ -1040,15 +1048,11 @@ namespace datatype {
             sort* s = todo.back();
             todo.pop_back();
             out << s->get_name() << " =\n";
-
             ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
-            for (unsigned i = 0; i < cnstrs.size(); ++i) {
+            for (func_decl * cns : cnstrs) {
-                func_decl* cns = cnstrs[i];
+                out << "  " << cns->get_name() << " :: ";
-                func_decl* rec = get_constructor_recognizer(cns);
-                out << "  " << cns->get_name() << " :: " << rec->get_name() << " :: ";
                 ptr_vector<func_decl> const & accs = *get_constructor_accessors(cns);
-                for (unsigned j = 0; j < accs.size(); ++j) {
+                for (func_decl* acc : accs) {
-                    func_decl* acc = accs[j];
                     sort* s1 = acc->get_range();
                     out << "(" << acc->get_name() << ": " << s1->get_name() << ") "; 
                     if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) {

src/ast/datatype_decl_plugin.h

@@ -368,6 +368,7 @@ namespace datatype {
         sort*  get_datatype_parameter_sort(sort * ty, unsigned idx);
         func_decl * get_non_rec_constructor(sort * ty);
         func_decl * get_constructor_recognizer(func_decl * constructor);
+        func_decl * get_constructor_is(func_decl * constructor);
         ptr_vector<func_decl> const * get_constructor_accessors(func_decl * constructor);
         func_decl * get_accessor_constructor(func_decl * accessor);
         func_decl * get_recognizer_constructor(func_decl * recognizer) const;

src/ast/decl_collector.cpp

@@ -18,6 +18,7 @@ Revision History:
 
 --*/
 #include "ast/decl_collector.h"
+#include "ast/ast_pp.h"
 
 void decl_collector::visit_sort(sort * n) {
     family_id fid = n->get_family_id();
@@ -25,19 +26,21 @@ void decl_collector::visit_sort(sort * n) {
         m_sorts.push_back(n);
     if (fid == m_dt_fid) {
         m_sorts.push_back(n);
-
         unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n);
         for (unsigned i = 0; i < num_cnstr; i++) {
             func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i);
-            m_decls.push_back(cnstr);
+            m_todo.push_back(cnstr);
             ptr_vector<func_decl> const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr);
             unsigned num_cas = cnstr_acc.size();
             for (unsigned j = 0; j < num_cas; j++) {
-                func_decl * accsr = cnstr_acc.get(j);
+                m_todo.push_back(cnstr_acc.get(j));
-                m_decls.push_back(accsr);
             }
         }
     }
+    for (unsigned i = n->get_num_parameters(); i-- > 0; ) {
+        parameter const& p = n->get_parameter(i);
+        if (p.is_ast()) m_todo.push_back(p.get_ast());
+    }
 }
 
 bool decl_collector::is_bool(sort * s) {
@@ -63,43 +66,43 @@ decl_collector::decl_collector(ast_manager & m, bool preds):
 }
 
 void decl_collector::visit(ast* n) {
-    ptr_vector<ast> todo;
+    datatype_util util(m());
-    todo.push_back(n);
+    m_todo.push_back(n);
-    while (!todo.empty()) {
+    while (!m_todo.empty()) {
-        n = todo.back();
+        n = m_todo.back();
-        todo.pop_back();
+        m_todo.pop_back();
         if (!m_visited.is_marked(n)) {
             m_visited.mark(n, true);
             switch(n->get_kind()) {
             case AST_APP: {
                 app * a = to_app(n);
-                for (unsigned i = 0; i < a->get_num_args(); ++i) {
+                for (expr* arg : *a) {
-                    todo.push_back(a->get_arg(i));
+                    m_todo.push_back(arg);
                 }
-                todo.push_back(a->get_decl());
+                m_todo.push_back(a->get_decl());
                 break;
             }
             case AST_QUANTIFIER: {
                 quantifier * q = to_quantifier(n);
                 unsigned num_decls = q->get_num_decls();
                 for (unsigned i = 0; i < num_decls; ++i) {
-                    todo.push_back(q->get_decl_sort(i));
+                    m_todo.push_back(q->get_decl_sort(i));
                 }
-                todo.push_back(q->get_expr());
+                m_todo.push_back(q->get_expr());
                 for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
-                    todo.push_back(q->get_pattern(i));
+                    m_todo.push_back(q->get_pattern(i));
                 }
                 break;
             }
-            case AST_SORT:
+            case AST_SORT: 
                 visit_sort(to_sort(n));
                 break;
             case AST_FUNC_DECL: {
                 func_decl * d = to_func_decl(n);
                 for (unsigned i = 0; i < d->get_arity(); ++i) {
-                    todo.push_back(d->get_domain(i));
+                    m_todo.push_back(d->get_domain(i));
                 }
-                todo.push_back(d->get_range());
+                m_todo.push_back(d->get_range());
                 visit_func(d);
                 break;
             }
@@ -112,5 +115,44 @@ void decl_collector::visit(ast* n) {
     }
 }
 
+void decl_collector::order_deps() {
+    top_sort<sort> st;
+    for (sort * s : m_sorts) st.insert(s, collect_deps(s));
+    st.topological_sort();
+    m_sorts.reset();
+    for (sort* s : st.top_sorted()) m_sorts.push_back(s);
+}
+
+decl_collector::sort_set* decl_collector::collect_deps(sort* s) {
+    sort_set* set = alloc(sort_set);
+    collect_deps(s, *set);
+    set->remove(s);
+    return set;
+}
+
+void decl_collector::collect_deps(sort* s, sort_set& set) {
+    if (set.contains(s)) return;
+    set.insert(s);
+    if (s->is_sort_of(m_dt_util.get_family_id(), DATATYPE_SORT)) {
+        unsigned num_sorts = m_dt_util.get_datatype_num_parameter_sorts(s);
+        for (unsigned i = 0; i < num_sorts; ++i) {
+            set.insert(m_dt_util.get_datatype_parameter_sort(s, i));
+        }
+        unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(s);
+        for (unsigned i = 0; i < num_cnstr; i++) {
+            func_decl * cnstr = m_dt_util.get_datatype_constructors(s)->get(i);
+            set.insert(cnstr->get_range());
+            for (unsigned j = 0; j < cnstr->get_arity(); ++j) 
+                set.insert(cnstr->get_domain(j));
+        }
+    }
+
+    for (unsigned i = s->get_num_parameters(); i-- > 0; ) {
+        parameter const& p = s->get_parameter(i);
+        if (p.is_ast() && is_sort(p.get_ast())) {
+            set.insert(to_sort(p.get_ast()));
+        }
+    }
+}
 
 

src/ast/decl_collector.h

@@ -20,6 +20,7 @@ Revision History:
 #ifndef SMT_DECL_COLLECTOR_H_
 #define SMT_DECL_COLLECTOR_H_
 
+#include "util/top_sort.h"
 #include "ast/ast.h"
 #include "ast/datatype_decl_plugin.h"
 
@@ -33,11 +34,17 @@ class decl_collector {
     family_id             m_basic_fid;
     family_id             m_dt_fid;
     datatype_util         m_dt_util;
+    ptr_vector<ast>       m_todo;
 
     void visit_sort(sort* n);
     bool is_bool(sort* s);
     void visit_func(func_decl* n);
 
+    typedef obj_hashtable<sort> sort_set;
+    sort_set* collect_deps(sort* s);
+    void collect_deps(top_sort<sort>& st);
+    void collect_deps(sort* s, sort_set& set);
+
 
 public:
     // if preds == true, then predicates are stored in a separate collection.
@@ -48,9 +55,12 @@ public:
     void visit(unsigned n, expr* const* es);
     void visit(expr_ref_vector const& es);
 
+    void order_deps();
+
     unsigned get_num_sorts() const { return m_sorts.size(); }
     unsigned get_num_decls() const { return m_decls.size(); }
     unsigned get_num_preds() const { return m_preds.size(); }
+    
     sort * const * get_sorts() const { return m_sorts.c_ptr(); }
     func_decl * const * get_func_decls() const { return m_decls.c_ptr(); }
     func_decl * const * get_pred_decls() const { return m_preds.c_ptr(); }

src/ast/fpa/fpa2bv_converter.cpp

@@ -25,7 +25,7 @@ Notes:
 #include "ast/fpa/fpa2bv_converter.h"
 #include "ast/rewriter/fpa_rewriter.h"
 
-#define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); }
+#define BVULT(X,Y,R) { expr_ref t(m); t = m_bv_util.mk_ule(Y,X); m_simp.mk_not(t, R); }
 
 fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
     m(m),
@@ -4085,7 +4085,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
     TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
 }
 
-void fpa2bv_converter::reset(void) {
+void fpa2bv_converter::reset() {
     dec_ref_map_key_values(m, m_const2bv);
     dec_ref_map_key_values(m, m_rm_const2bv);
     dec_ref_map_key_values(m, m_uf2bvuf);

src/ast/fpa/fpa2bv_converter.h

@@ -150,7 +150,7 @@ public:
     void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
     expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y);
 
-    void reset(void);
+    void reset();
 
     void dbg_decouple(const char * prefix, expr_ref & e);
     expr_ref_vector m_extra_assertions;

src/ast/fpa_decl_plugin.cpp

@@ -160,7 +160,7 @@ bool fpa_decl_plugin::is_rm_numeral(expr * n, mpf_rounding_mode & val) {
         return true;
     }
 
-    return 0;
+    return false;
 }
 
 bool fpa_decl_plugin::is_rm_numeral(expr * n) {

src/ast/macros/quasi_macros.cpp

@@ -91,7 +91,7 @@ public:
     void operator()(var * n) { m_bitset.set(n->get_idx(), true); }
     void operator()(quantifier * n) {}
     void operator()(app * n) {}
-    bool all_used(void) {
+    bool all_used() {
         for (unsigned i = 0; i < m_bitset.size() ; i++)
             if (!m_bitset.get(i))
                 return false;

src/ast/proofs/proof_checker.cpp

@@ -440,16 +440,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m);); 
         return false;
     }
-    case PR_PULL_QUANT_STAR: {
-        if (match_proof(p) &&
-            match_fact(p, fact) &&
-            match_iff(fact.get(), t1, t2)) {
-            // TBD: check the enchilada.
-            return true;
-        }
-        IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m);); 
-        return false;
-    }
     case PR_PUSH_QUANT: {
         if (match_proof(p) &&
             match_fact(p, fact) &&
@@ -730,10 +720,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         // TBD:
         return true;
     }
-    case PR_NNF_STAR: {
-        // TBD:
-        return true;
-    }
     case PR_SKOLEMIZE: {
         // (exists ?x (p ?x y)) -> (p (sk y) y)
         // (not (forall ?x (p ?x y))) -> (not (p (sk y) y))
@@ -755,19 +741,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         UNREACHABLE();
         return false;
     }
-    case PR_CNF_STAR: {
-        for (unsigned i = 0; i < proofs.size(); ++i) {
-            if (match_op(proofs[i].get(), PR_DEF_INTRO, terms)) {
-                // ok
-            }
-            else {
-                UNREACHABLE();
-                return false;
-            }
-        }
-        // coarse grain CNF conversion.
-        return true;
-    }
     case PR_MODUS_PONENS_OEQ: {
         if (match_fact(p, fact) &&
             match_proof(p, p0, p1) &&
@@ -922,7 +895,7 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
     }
 }
 
-bool proof_checker::match_fact(proof* p, expr_ref& fact) {
+bool proof_checker::match_fact(proof const* p, expr_ref& fact) const {
     if (m.is_proof(p) &&
         m.has_fact(p)) {
         fact = m.get_fact(p);
@@ -938,13 +911,13 @@ void proof_checker::add_premise(proof* p) {
     }
 }
 
-bool proof_checker::match_proof(proof* p) {
+bool proof_checker::match_proof(proof const* p) const {
     return 
         m.is_proof(p) &&
         m.get_num_parents(p) == 0;
 }
 
-bool proof_checker::match_proof(proof* p, proof_ref& p0) {
+bool proof_checker::match_proof(proof const* p, proof_ref& p0) const {
     if (m.is_proof(p) &&
         m.get_num_parents(p) == 1) {
         p0 = m.get_parent(p, 0);
@@ -953,7 +926,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0) {
     return false;
 }
  
-bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
+bool proof_checker::match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const {
     if (m.is_proof(p) &&
         m.get_num_parents(p) == 2) {
         p0 = m.get_parent(p, 0);
@@ -963,7 +936,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
     return false;
 }
 
-bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
+bool proof_checker::match_proof(proof const* p, proof_ref_vector& parents) const {
     if (m.is_proof(p)) {
         for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
             parents.push_back(m.get_parent(p, i));
@@ -974,7 +947,7 @@ bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
 }
 
 
-bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_num_args() == 2) {
         d = to_app(e)->get_decl();
@@ -986,7 +959,7 @@ bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_r
 }
 
 
-bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms) {
+bool proof_checker::match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const {
     if (e->get_kind() == AST_APP) {
         d = to_app(e)->get_decl();
         for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
@@ -997,9 +970,9 @@ bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms)
     return false;
 }
 
-bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) {
+bool proof_checker::match_quantifier(expr const* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) const {
     if (is_quantifier(e)) {
-        quantifier* q = to_quantifier(e);
+        quantifier const* q = to_quantifier(e);
         is_univ = q->is_forall();
         body = q->get_expr();
         for (unsigned i = 0; i < q->get_num_decls(); ++i) {
@@ -1010,7 +983,7 @@ bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& so
     return false;
 }
 
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k &&
@@ -1022,7 +995,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
     return false;
 }
 
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k) {
@@ -1035,7 +1008,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
 }
 
 
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k &&
@@ -1046,39 +1019,39 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
     return false;
 }
 
-bool proof_checker::match_not(expr* e, expr_ref& t) {
+bool proof_checker::match_not(expr const* e, expr_ref& t) const {
     return match_op(e, OP_NOT, t);
 }
 
-bool proof_checker::match_or(expr* e, expr_ref_vector& terms) {
+bool proof_checker::match_or(expr const* e, expr_ref_vector& terms) const {
     return match_op(e, OP_OR, terms);
 }
 
-bool proof_checker::match_and(expr* e, expr_ref_vector& terms) {
+bool proof_checker::match_and(expr const* e, expr_ref_vector& terms) const {
     return match_op(e, OP_AND, terms);
 }
 
-bool proof_checker::match_iff(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_IFF, t1, t2);
 }
 
-bool proof_checker::match_equiv(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_equiv(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_oeq(e, t1, t2) || match_eq(e, t1, t2);
 }
 
-bool proof_checker::match_implies(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_IMPLIES, t1, t2);
 }
 
-bool proof_checker::match_eq(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_EQ, t1, t2) || match_iff(e, t1, t2);
 }
 
-bool proof_checker::match_oeq(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_OEQ, t1, t2);
 }
 
-bool proof_checker::match_negated(expr* a, expr* b) {
+bool proof_checker::match_negated(expr const* a, expr* b) const {
     expr_ref t(m);
     return 
         (match_not(a, t) && t.get() == b) ||
@@ -1186,14 +1159,14 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
 
 }
 
-bool proof_checker::match_nil(expr* e) const {
+bool proof_checker::match_nil(expr const* e) const {
     return 
         is_app(e) &&
         to_app(e)->get_family_id() == m_hyp_fid &&
         to_app(e)->get_decl_kind() == OP_NIL;
 }
 
-bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const {
+bool proof_checker::match_cons(expr const* e, expr_ref& a, expr_ref& b) const {
     if (is_app(e) &&
         to_app(e)->get_family_id() == m_hyp_fid &&
         to_app(e)->get_decl_kind() == OP_CONS) {
@@ -1205,7 +1178,7 @@ bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const {
 }
 
 
-bool proof_checker::match_atom(expr* e, expr_ref& a) const {
+bool proof_checker::match_atom(expr const* e, expr_ref& a) const {
     if (is_app(e) &&
         to_app(e)->get_family_id() == m_hyp_fid &&
         to_app(e)->get_decl_kind() == OP_ATOM) {
@@ -1227,7 +1200,7 @@ expr* proof_checker::mk_nil() {
     return m_nil.get();
 }
 
-bool proof_checker::is_hypothesis(proof* p) const {
+bool proof_checker::is_hypothesis(proof const* p) const {
     return 
         m.is_proof(p) &&
         p->get_decl_kind() == PR_HYPOTHESIS;
@@ -1253,7 +1226,7 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
     } 
 }
 
-void proof_checker::dump_proof(proof * pr) {
+void proof_checker::dump_proof(proof const* pr) {
     if (!m_dump_lemmas)
         return;
     SASSERT(m.has_fact(pr));

src/ast/proofs/proof_checker.h

@@ -77,39 +77,39 @@ private:
     bool check1_spc(proof* p, expr_ref_vector& side_conditions);
     bool check_arith_proof(proof* p);
     bool check_arith_literal(bool is_pos, app* lit, rational const& coeff, expr_ref& sum, bool& is_strict);
-    bool match_fact(proof* p, expr_ref& fact);
+    bool match_fact(proof const* p, expr_ref& fact) const;
     void add_premise(proof* p);
-    bool match_proof(proof* p);
+    bool match_proof(proof const* p) const;
-    bool match_proof(proof* p, proof_ref& p0);
+    bool match_proof(proof const* p, proof_ref& p0) const;
-    bool match_proof(proof* p, proof_ref& p0, proof_ref& p1);
+    bool match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const;
-    bool match_proof(proof* p, proof_ref_vector& parents);
+    bool match_proof(proof const* p, proof_ref_vector& parents) const;
-    bool match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2);
+    bool match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const;
-    bool match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2);
+    bool match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const;
-    bool match_op(expr* e, decl_kind k, expr_ref& t);
+    bool match_op(expr const* e, decl_kind k, expr_ref& t) const;
-    bool match_op(expr* e, decl_kind k, expr_ref_vector& terms);
+    bool match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const;
-    bool match_iff(expr* e, expr_ref& t1, expr_ref& t2);
+    bool match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_implies(expr* e, expr_ref& t1, expr_ref& t2);
+    bool match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_eq(expr* e, expr_ref& t1, expr_ref& t2);
+    bool match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_oeq(expr* e, expr_ref& t1, expr_ref& t2);
+    bool match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const;
-    bool match_not(expr* e, expr_ref& t);
+    bool match_not(expr const* e, expr_ref& t) const;
-    bool match_or(expr* e, expr_ref_vector& terms);
+    bool match_or(expr const* e, expr_ref_vector& terms) const;
-    bool match_and(expr* e, expr_ref_vector& terms);
+    bool match_and(expr const* e, expr_ref_vector& terms) const;
-    bool match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms);
+    bool match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const;
-    bool match_quantifier(expr*, bool& is_univ, sort_ref_vector&, expr_ref& body);
+    bool match_quantifier(expr const*, bool& is_univ, sort_ref_vector&, expr_ref& body) const;
-    bool match_negated(expr* a, expr* b);
+    bool match_negated(expr const* a, expr* b) const;
-    bool match_equiv(expr* a, expr_ref& t1, expr_ref& t2);
+    bool match_equiv(expr const* a, expr_ref& t1, expr_ref& t2) const;
     void get_ors(expr* e, expr_ref_vector& ors);
     void get_hypotheses(proof* p, expr_ref_vector& ante);
 
-    bool match_nil(expr* e) const;
+    bool match_nil(expr const* e) const;
-    bool match_cons(expr* e, expr_ref& a, expr_ref& b) const;
+    bool match_cons(expr const* e, expr_ref& a, expr_ref& b) const;
-    bool match_atom(expr* e, expr_ref& a) const;
+    bool match_atom(expr const* e, expr_ref& a) const;
     expr* mk_nil();
     expr* mk_cons(expr* a, expr* b);
     expr* mk_atom(expr* e);
-    bool is_hypothesis(proof* p) const;
+    bool is_hypothesis(proof const* p) const;
     expr* mk_hyp(unsigned num_hyps, expr * const * hyps);
-    void dump_proof(proof * pr);
+    void dump_proof(proof const* pr);
     void dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent);
 
     void set_false(expr_ref& e, unsigned idx, expr_ref& lit);

src/ast/rewriter/CMakeLists.txt

@@ -25,7 +25,6 @@ z3_add_component(rewriter
     pb_rewriter.cpp
     pb2bv_rewriter.cpp
     push_app_ite.cpp
-    pull_ite_tree.cpp
     quant_hoist.cpp
     rewriter.cpp
     seq_rewriter.cpp

src/ast/rewriter/pull_ite_tree.cpp

@@ -1,221 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    pull_ite_tree.cpp
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-06-22.
-
-Revision History:
-
---*/
-#include "ast/rewriter/pull_ite_tree.h"
-#include "ast/recurse_expr_def.h"
-#include "ast/for_each_expr.h"
-#include "ast/ast_pp.h"
-
-pull_ite_tree::pull_ite_tree(ast_manager & m):
-    m_manager(m),
-    m_rewriter(m),
-    m_cache(m) {
-}
-
-void pull_ite_tree::cache_result(expr * n, expr * r, proof * pr) { 
-    m_cache.insert(n, r, pr); 
-}
-
-void pull_ite_tree::visit(expr * n, bool & visited) {
-    if (!is_cached(n)) {
-        m_todo.push_back(n);
-        visited = false;
-    }
-}
-
-bool pull_ite_tree::visit_children(expr * n) {
-    if (m_manager.is_ite(n)) {
-        bool visited = true;
-        visit(to_app(n)->get_arg(1), visited);
-        visit(to_app(n)->get_arg(2), visited);
-        return visited;
-    }
-    else {
-        return true;
-    }
-}
-
-void pull_ite_tree::reduce(expr * n) {
-    // Remark: invoking the simplifier to build the new expression saves a lot of memory.
-    if (m_manager.is_ite(n)) {
-        expr * c = to_app(n)->get_arg(0);
-        expr * t_old = to_app(n)->get_arg(1);
-        expr * e_old = to_app(n)->get_arg(2);
-        expr * t     = nullptr;
-        proof * t_pr = nullptr;
-        expr * e     = nullptr;
-        proof * e_pr = nullptr;
-        get_cached(t_old, t, t_pr);
-        get_cached(e_old, e, e_pr);
-        expr_ref r(m_manager);
-        expr * args[3] = {c, t, e};
-        r = m_rewriter.mk_app(to_app(n)->get_decl(), 3, args);
-        if (!m_manager.proofs_enabled()) {
-            // expr * r = m_manager.mk_ite(c, t, e);
-            cache_result(n, r, nullptr);
-        }
-        else {
-            // t_pr is a proof for (m_p ... t_old ...) == t
-            // e_pr is a proof for (m_p ... e_old ...) == e
-            expr_ref old(m_manager);
-            expr_ref p_t_old(m_manager);
-            expr_ref p_e_old(m_manager);
-            old     = mk_p_arg(n); // (m_p ... n ...) where n is (ite c t_old e_old)
-            p_t_old = mk_p_arg(t_old); // (m_p ... t_old ...)
-            p_e_old = mk_p_arg(e_old); // (m_p ... e_old ...)
-            expr_ref tmp1(m_manager);
-            tmp1 = m_manager.mk_ite(c, p_t_old, p_e_old); // (ite c (m_p ... t_old ...) (m_p ... e_old ...))
-            proof * pr1 = m_manager.mk_rewrite(old, tmp1);  // proof for (m_p ... (ite c t_old e_old) ...) = (ite c (m_p ... t_old ...) (m_p ... e_old ...))
-            expr_ref tmp2(m_manager);
-            tmp2 = m_manager.mk_ite(c, t, e); // (ite c t e)
-            proof * pr2 = nullptr; // it will contain a proof for (ite c (m_p ... t_old ...) (m_p ... e_old ...)) = (ite c t e)
-            proof * pr3 = nullptr; // it will contain a proof for (m_p ... (ite c t_old e_old) ...)               = (ite c t e)
-            proof * proofs[2];
-            unsigned num_proofs = 0;
-            if (t_pr != nullptr) {
-                proofs[num_proofs] = t_pr;
-                num_proofs++;
-            }
-            if (e_pr != nullptr) {
-                proofs[num_proofs] = e_pr;
-                num_proofs++;
-            }
-            if (num_proofs > 0) {
-                pr2 = m_manager.mk_congruence(to_app(tmp1), to_app(tmp2), num_proofs, proofs);
-                pr3 = m_manager.mk_transitivity(pr1, pr2);
-            }
-            else {
-                pr3 = pr1;
-            }
-            proof * pr4 = nullptr; // it will contain a proof for (ite c t e) = r
-            proof * pr5 = nullptr; // it will contain a proof for (m_p ... (ite c t_old e_old) ...) = r
-            if (tmp2 != r) {
-                pr4 = m_manager.mk_rewrite(tmp2, r);
-                pr5 = m_manager.mk_transitivity(pr3, pr4);
-            }
-            else {
-                pr5 = pr3;
-            }
-            cache_result(n, r, pr5);
-        }
-    }
-    else {
-        expr_ref r(m_manager);
-        m_args[m_arg_idx] = n;
-        r = m_rewriter.mk_app(m_p, m_args.size(), m_args.c_ptr());
-        if (!m_manager.proofs_enabled()) {
-            // expr * r = m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr());
-            cache_result(n, r, nullptr);
-        }
-        else {
-            expr_ref old(m_manager);
-            proof * p;
-            old = mk_p_arg(n);
-            if (old == r)
-                p = nullptr;
-            else
-                p = m_manager.mk_rewrite(old, r);
-            cache_result(n, r, p);
-        }
-    }
-}
-
-void pull_ite_tree::operator()(app * n, app_ref & r, proof_ref & pr) {
-    unsigned num_args = n->get_num_args();
-    m_args.resize(num_args);
-    m_p = n->get_decl();
-    expr * ite = nullptr;
-    for (unsigned i = 0; i < num_args; i++) {
-        expr * arg = n->get_arg(i);
-        if (ite) {
-            m_args[i] = arg;
-        }
-        else if (m_manager.is_ite(arg)) {
-            m_arg_idx = i;
-            m_args[i] = 0;
-            ite       = arg;
-        }
-        else {
-            m_args[i] = arg;
-        }
-    }
-    if (!ite) {
-        r = n;
-        pr = nullptr;
-        return;
-    }
-    m_todo.push_back(ite);
-    while (!m_todo.empty()) {
-        expr * n = m_todo.back();
-        if (is_cached(n))
-            m_todo.pop_back();
-        else if (visit_children(n)) {
-            m_todo.pop_back();
-            reduce(n);
-        }
-    }
-    SASSERT(is_cached(ite));
-    expr *   _r = nullptr;
-    proof * _pr = nullptr;
-    get_cached(ite, _r, _pr);
-    r  = to_app(_r);
-    pr = _pr;
-    m_cache.reset();
-    m_todo.reset();
-}
-
-
-
-pull_ite_tree_cfg::pull_ite_tree_cfg(ast_manager & m):
-    m(m),
-    m_trail(m),
-    m_proc(m) {
-}
-
-bool pull_ite_tree_cfg::get_subst(expr * n, expr* & r, proof* & p) {
-    if (is_app(n) && is_target(to_app(n))) {
-        app_ref tmp(m);
-        proof_ref pr(m);
-        m_proc(to_app(n), tmp, pr);
-        if (tmp != n) {
-            r = tmp;
-            p = pr;
-            m_trail.push_back(r);
-            m_trail.push_back(p);
-            return true;
-        }
-    }
-    return false;
-}
-
-bool pull_cheap_ite_tree_cfg::is_target(app * n) const {
-    bool r = 
-        n->get_num_args() == 2 &&
-        n->get_family_id() != null_family_id &&
-        m.is_bool(n) &&
-        (m.is_value(n->get_arg(0)) || m.is_value(n->get_arg(1))) &&
-        (m.is_term_ite(n->get_arg(0)) || m.is_term_ite(n->get_arg(1)));
-    TRACE("pull_ite_target", tout << mk_pp(n, m) << "\nresult: " << r << "\n";);
-    return r;
-}
-
-
-
-
-
-

src/ast/rewriter/pull_ite_tree.h

@@ -1,113 +0,0 @@
-/*++
-Copyright (c) 2006 Microsoft Corporation
-
-Module Name:
-
-    pull_ite_tree.h
-
-Abstract:
-
-    <abstract>
-
-Author:
-
-    Leonardo de Moura (leonardo) 2008-06-22.
-
-Revision History:
-
---*/
-#ifndef PULL_ITE_TREE_H_
-#define PULL_ITE_TREE_H_
-
-#include "ast/ast.h"
-#include "ast/rewriter/rewriter.h"
-#include "ast/rewriter/th_rewriter.h"
-#include "ast/expr_map.h"
-#include "ast/recurse_expr.h"
-#include "util/obj_hashtable.h"
-
-/**
-   \brief Functor for applying the following transformation
-   F[(p (ite c t1 t2) args)] = F'[(ite c t1 t2), p, args]
-
-   F'[(ite c t1 t2), p, args] = (ite c F'[t1, p, args] F'[t2, p, args])
-   F'[t, p, args] = (p t args)
-*/
-class pull_ite_tree {
-    ast_manager &         m_manager;
-    th_rewriter           m_rewriter;
-    func_decl *           m_p;
-    ptr_vector<expr>      m_args;
-    unsigned              m_arg_idx; //!< position of the ite argument
-    expr_map              m_cache;
-    ptr_vector<expr>      m_todo;
-
-    bool is_cached(expr * n) const { return m_cache.contains(n); }
-    void get_cached(expr * n, expr * & r, proof * & p) const { m_cache.get(n, r, p); }
-    void cache_result(expr * n, expr * r, proof * pr);
-    void visit(expr * n, bool & visited);
-    bool visit_children(expr * n);
-    void reduce(expr * n);
-    /**
-       \brief Creante an application (m_p ... n ...) where n is the argument m_arg_idx and the other arguments
-       are in m_args.
-    */
-    expr * mk_p_arg(expr * n) {
-        m_args[m_arg_idx] = n;
-        return m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr());
-    }
-public:
-    pull_ite_tree(ast_manager & m);
-    /**
-       \brief Apply the transformation above if n contains an ite-expression.
-       Store the result in r. If n does not contain an ite-expression, then
-       store n in r.
-
-       When proof generation is enabled, pr is a proof for n = r.
-    */
-    void operator()(app * n, app_ref & r, proof_ref & pr);
-};
-
-/**
-   \brief Functor for applying the pull_ite_tree on subexpressions n that
-   satisfy the is_target virtual predicate.
-*/
-class pull_ite_tree_cfg : public default_rewriter_cfg {
-protected:
-    ast_manager& m;
-    expr_ref_vector m_trail;
-    pull_ite_tree m_proc;
-public:
-    pull_ite_tree_cfg(ast_manager & m);
-    virtual ~pull_ite_tree_cfg() {}
-    virtual bool is_target(app * n) const = 0;
-    bool get_subst(expr * n, expr* & r, proof* & p);
-};
-
-/**
-   \brief Apply pull_ite_tree on predicates of the form
-   (p ite v) and (p v ite)
-
-   where:
-   - p is an interpreted predicate
-   - ite is an ite-term expression
-   - v is a value
-*/
-class pull_cheap_ite_tree_cfg : public pull_ite_tree_cfg {
-public:
-    pull_cheap_ite_tree_cfg(ast_manager & m):pull_ite_tree_cfg(m) {}
-    ~pull_cheap_ite_tree_cfg() override {}
-    bool is_target(app * n) const override;
-};
-
-class pull_cheap_ite_tree_rw  : public rewriter_tpl<pull_cheap_ite_tree_cfg> {
-    pull_cheap_ite_tree_cfg m_cfg;
-public:
-    pull_cheap_ite_tree_rw(ast_manager& m):
-        rewriter_tpl<pull_cheap_ite_tree_cfg>(m, m.proofs_enabled(), m_cfg),
-        m_cfg(m)
-    {}
-};
-
-#endif /* PULL_ITE_TREE_H_ */
-

src/ast/rewriter/rewriter_def.h

@@ -358,7 +358,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
                 if (ProofGen) {
                     NOT_IMPLEMENTED_YET();
                     // We do not support the use of bindings in proof generation mode.
-                    // Thus we have to apply the subsitution here, and
+                    // Thus we have to apply the substitution here, and
                     // beta_reducer subst(m());
                     // subst.set_bindings(new_num_args, new_args);
                     // expr_ref r2(m());

src/ast/rewriter/seq_rewriter.cpp

@@ -1478,9 +1478,7 @@ br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
         return BR_DONE;
     }
     if (m_util.re.is_full_char(a)) {
-        sort* seq_sort = nullptr;
+        result = m_util.re.mk_full_seq(m().get_sort(a));
-        VERIFY(m_util.is_re(a, seq_sort));
-        result = m_util.re.mk_full_seq(seq_sort);
         return BR_DONE;
     }
     if (m_util.re.is_empty(a)) {

src/ast/seq_decl_plugin.cpp

@@ -671,9 +671,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
 
     case _OP_REGEXP_FULL_CHAR:
-        if (!range) {
+        if (!range) range = m_re;
-            range = m_re;
-        }
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(symbol("re.allchar"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_FULL_CHAR_SET));
 
@@ -690,9 +688,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, range, func_decl_info(m_family_id, k));        
 
     case _OP_REGEXP_EMPTY:
-        if (!range) {
+        if (!range) range = m_re;
-            range = m_re;
-        }
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_EMPTY_SET));
 

src/cmd_context/cmd_context.cpp

@@ -320,7 +320,7 @@ bool cmd_context::macros_find(symbol const& s, unsigned n, expr*const* args, exp
         if (d.m_domain.size() != n) continue;
         bool eq = true;
         for (unsigned i = 0; eq && i < n; ++i) {
-            eq = d.m_domain[i] == m().get_sort(args[i]);
+            eq = m().compatible_sorts(d.m_domain[i], m().get_sort(args[i]));
         }
         if (eq) {
             t = d.m_body;
@@ -719,6 +719,7 @@ void cmd_context::init_manager_core(bool new_manager) {
     m_dt_eh = alloc(dt_eh, *this);
     m_pmanager->set_new_datatype_eh(m_dt_eh.get());
     if (!has_logic()) {
+        TRACE("cmd_context", tout << "init manager\n";);
         // add list type only if the logic is not specified.
         // it prevents clashes with builtin types.
         insert(pm().mk_plist_decl());
@@ -1408,7 +1409,8 @@ void cmd_context::restore_assertions(unsigned old_sz) {
         SASSERT(m_assertions.empty());
         return;
     }
-    SASSERT(old_sz <= m_assertions.size());
+    if (old_sz == m_assertions.size()) return;
+    SASSERT(old_sz < m_assertions.size());
     SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size());
     restore(m(), m_assertions, old_sz);
     if (produce_unsat_cores())
@@ -2015,7 +2017,7 @@ void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) {
         m_owner.insert(c);
         func_decl * r = m_dt_util.get_constructor_recognizer(c);
         m_owner.insert(r);
-        TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";);
+        // TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";);
         for (func_decl * a : *m_dt_util.get_constructor_accessors(c)) {
             TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";);
             m_owner.insert(a);

src/cmd_context/pdecl.cpp

@@ -852,7 +852,7 @@ pdecl_manager::pdecl_manager(ast_manager & m):
 pdecl_manager::~pdecl_manager() {
     dec_ref(m_list);
     reset_sort_info();
-    SASSERT(m_sort2psort.empty());    
+    SASSERT(m_sort2psort.empty());
     SASSERT(m_table.empty());
 }
 
@@ -946,6 +946,7 @@ void pdecl_manager::del_decl_core(pdecl * p) {
 }
 
 void pdecl_manager::del_decl(pdecl * p) {
+    TRACE("pdecl_manager", p->display(tout); tout << "\n";);
     if (p->is_psort()) {
         psort * _p = static_cast<psort*>(p);
         if (_p->is_sort_wrapper())

src/interp/iz3checker.cpp

@@ -43,7 +43,7 @@ struct iz3checker : iz3base {
     /* HACK: for tree interpolants, we assume that uninterpreted functions
        are global. This is because in the current state of the tree interpolation
        code, symbols that appear in sibling sub-trees have to be global, and
-       we have no way to eliminate such function symbols. When tree interpoaltion is
+       we have no way to eliminate such function symbols. When tree interpolation is
        fixed, we can tree function symbols the same as constant symbols. */
 
     bool is_tree;

src/model/func_interp.cpp

@@ -112,7 +112,8 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
         return false;
     }
 
-    if ((m_arity == 0) ||
+    if (!is_ground(t) ||
+        (m_arity == 0) ||
         (m_arity == 1 && !m().is_eq(c, a0, a1)) ||
         (m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity)))
         return false;

src/muz/base/dl_context.cpp

@@ -1106,6 +1106,16 @@ namespace datalog {
             names.push_back(m_rule_names[i]);            
         }
     }
+
+    static std::ostream& display_symbol(std::ostream& out, symbol const& nm) {
+        if (is_smt2_quoted_symbol(nm)) {
+            out << mk_smt2_quoted_symbol(nm);
+        }
+        else {
+            out << nm;
+        }
+        return out;
+    }
  
     void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) {
         ast_manager& m = get_manager();
@@ -1148,13 +1158,13 @@ namespace datalog {
         if (!use_fixedpoint_extensions) {
             out << "(set-logic HORN)\n";
         }
+        for (func_decl * f : rels) 
+            visitor.remove_decl(f);
 
         visitor.display_decls(out);
-        func_decl_set::iterator it = rels.begin(), end = rels.end();
+
-        for (; it != end; ++it) {
+        for (func_decl * f : rels) 
-            func_decl* f = *it;
             display_rel_decl(out, f);
-        }
 
         if (use_fixedpoint_extensions && do_declare_vars) {
             declare_vars(rules, fresh_names, out);
@@ -1185,13 +1195,7 @@ namespace datalog {
                     nm = symbol(s.str().c_str());                    
                 }
                 fresh_names.add(nm);
-                if (is_smt2_quoted_symbol(nm)) {
+                display_symbol(out, nm) << ")";
-                    out << mk_smt2_quoted_symbol(nm);
-                }
-                else {
-                    out << nm;
-                }
-                out << ")";
             }
             out << ")\n";
         }
@@ -1219,7 +1223,8 @@ namespace datalog {
                     PP(qfn);
                     out << ")\n";
                 }
-                out << "(query " << fn->get_name() << ")\n";
+                out << "(query ";
+                display_symbol(out, fn->get_name()) << ")\n";
             }
         }
         else {
@@ -1238,7 +1243,8 @@ namespace datalog {
 
     void context::display_rel_decl(std::ostream& out, func_decl* f) {
         smt2_pp_environment_dbg env(m);
-        out << "(declare-rel " << f->get_name() << " (";
+        out << "(declare-rel ";
+        display_symbol(out, f->get_name()) << " (";
         for (unsigned i = 0; i < f->get_arity(); ++i) {                
             ast_smt2_pp(out, f->get_domain(i), env);
             if (i + 1 < f->get_arity()) {

src/muz/base/fixedpoint_params.pyg

@@ -33,7 +33,7 @@ def_module_params('fixedpoint',
                            "updated relation was modified or not"),
                           ('datalog.compile_with_widening', BOOL, False, 
                            "widening will be used to compile recursive rules"),
-                          ('datalog.default_table_checked', BOOL, False, "if true, the detault " +
+                          ('datalog.default_table_checked', BOOL, False, "if true, the default " +
                            'table will be default_table inside a wrapper that checks that its results ' +
                            'are the same as of default_table_checker table'),
                           ('datalog.default_table_checker', SYMBOL, 'null', "see default_table_checked"),
@@ -59,7 +59,7 @@ def_module_params('fixedpoint',
                           ('duality.full_expand', BOOL, False, 'Fully expand derivation trees'),
                           ('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'),
                           ('duality.feasible_edges', BOOL, True, 
-                           'Don\'t expand definitley infeasible edges'),
+                           'Don\'t expand definitely infeasible edges'),
                           ('duality.use_underapprox', BOOL, False, 'Use underapproximations'),
                           ('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'),
                           ('duality.recursion_bound', UINT, UINT_MAX, 
@@ -130,7 +130,7 @@ def_module_params('fixedpoint',
                           ('xform.magic', BOOL, False, 
                            "perform symbolic magic set transformation"),
                           ('xform.scale', BOOL, False, 
-                           "add scaling variable to linear real arithemtic clauses"),
+                           "add scaling variable to linear real arithmetic clauses"),
                           ('xform.inline_linear', BOOL, True, "try linear inlining method"),
                           ('xform.inline_eager', BOOL, True, "try eager inlining of rules"),
                           ('xform.inline_linear_branch', BOOL, False, 
@@ -176,7 +176,7 @@ def_module_params('fixedpoint',
                           ('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),
                           ('spacer.reach_as_init', BOOL, True, "Extend initial rules with computed reachability facts"),
                           ('spacer.blast_term_ite', BOOL, True, "Expand non-Boolean ite-terms"),
-                          ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministicly"),
+                          ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministically"),
                           ('spacer.reach_dnf', BOOL, True, "Restrict reachability facts to DNF"),
                           ('bmc.linear_unrolling_depth', UINT, UINT_MAX, "Maximal level to explore"),
                           ('spacer.split_farkas_literals', BOOL, False, "Split Farkas literals"),

src/muz/pdr/pdr_context.cpp

@@ -1736,6 +1736,7 @@ namespace pdr {
     }
 
     void context::validate_model() {
+        IF_VERBOSE(1, verbose_stream() << "(pdr.validate_model)\n";);
         std::stringstream msg;
         expr_ref_vector refs(m);
         expr_ref tmp(m);
@@ -1745,11 +1746,10 @@ namespace pdr {
         get_level_property(m_inductive_lvl, refs, rs);
         inductive_property ex(m, mc, rs);
         ex.to_model(model);
-        decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
         var_subst vs(m, false);
         expr_free_vars fv;
-        for (; it != end; ++it) {
+        for (auto const& kv : m_rels) {
-            ptr_vector<datalog::rule> const& rules = it->m_value->rules();
+            ptr_vector<datalog::rule> const& rules = kv.m_value->rules();
             for (unsigned i = 0; i < rules.size(); ++i) {
                 datalog::rule& r = *rules[i];
                 model->eval(r.get_head(), tmp);
@@ -1916,7 +1916,7 @@ namespace pdr {
                     verbose_stream() << ex.to_string();
                 });
 
-            // upgrade invariants that are known to be inductive.
+            // upgrade invariants that are known to be inductive.            
             decl2rel::iterator it = m_rels.begin (), end = m_rels.end ();
             for (; m_inductive_lvl > 0 && it != end; ++it) {
                 if (it->m_value->head() != m_query_pred) {

src/muz/pdr/pdr_prop_solver.cpp

@@ -133,7 +133,7 @@ namespace pdr {
                 else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) ||
                          (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){
                     func_decl* f = to_app(val)->get_decl();
-                    func_decl* r = dt.get_constructor_recognizer(f);
+                    func_decl* r = dt.get_constructor_is(f);
                     conjs[i] = m.mk_app(r, c);
                     ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f);
                     for (unsigned j = 0; j < acc.size(); ++j) {

src/muz/spacer/spacer_util.cpp

@@ -694,7 +694,7 @@ void expand_literals(ast_manager &m, expr_ref_vector& conjs)
         } else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) ||
                     (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){
                 func_decl* f = to_app(val)->get_decl();
-                func_decl* r = dt.get_constructor_recognizer(f);
+                func_decl* r = dt.get_constructor_is(f);
                 conjs[i] = m.mk_app(r, c);
                 ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f);
                 for (unsigned j = 0; j < acc.size(); ++j) {

src/muz/transforms/dl_mk_array_instantiation.h

@@ -26,7 +26,7 @@ Implementation:
 
     1) Dealing with multiple quantifiers -> The options fixedpoint.xform.instantiate_arrays.nb_quantifier gives the number of quantifiers per array.
 
-    2) Inforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms
+    2) Enforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms
        P(a) into P(i, a[i]). This enforces the solver to limit the space search at the cost of imprecise results. This option
        corresponds to fixedpoint.xform.instantiate_arrays.enforce
 

src/muz/transforms/dl_mk_interp_tail_simplifier.h

@@ -53,7 +53,7 @@ namespace datalog {
             */
             void reset(rule * r);
 
-            /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
+            /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */
             bool unify(expr * e1, expr * e2);
 
             void get_result(rule_ref & res);

src/muz/transforms/dl_mk_rule_inliner.cpp

@@ -209,9 +209,7 @@ namespace datalog {
             rel->collect_non_empty_predicates(m_preds_with_facts);
         }
 
-        rule_set::iterator rend = orig.end();
+        for (rule * r : orig) {
-        for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {
-            rule * r = *rit;
             func_decl * head_pred = r->get_decl();
             m_head_pred_ctr.inc(head_pred);
 
@@ -258,9 +256,7 @@ namespace datalog {
     rule_set * mk_rule_inliner::create_allowed_rule_set(rule_set const & orig) 
     {
         rule_set * res = alloc(rule_set, m_context);
-        unsigned rcnt = orig.get_num_rules();
+        for (rule * r : orig) {
-        for (unsigned i=0; i<rcnt; i++) {
-            rule * r = orig.get_rule(i);
             if (inlining_allowed(orig, r->get_decl())) {
                 res->add_rule(r);
             }
@@ -283,13 +279,11 @@ namespace datalog {
         
         const rule_stratifier::comp_vector& comps = r.get_stratifier().get_strats();
 
-        rule_stratifier::comp_vector::const_iterator cend = comps.end();
+        for (rule_stratifier::item_set * stratum : comps) {
-        for (rule_stratifier::comp_vector::const_iterator it = comps.begin(); it!=cend; ++it) {
+            if (stratum->size() == 1) {
-            rule_stratifier::item_set * stratum = *it;
-            if (stratum->size()==1) {
                 continue;
             }
-            SASSERT(stratum->size()>1);
+            SASSERT(stratum->size() > 1);
             func_decl * first_stratum_pred = *stratum->begin();
 
             //we're trying to break cycles by removing one predicate from each of them
@@ -307,9 +301,7 @@ namespace datalog {
         const rule_stratifier::comp_vector& comps = 
             proposed_inlined_rules.get_stratifier().get_strats();
 
-        rule_stratifier::comp_vector::const_iterator cend = comps.end();
+        for (rule_stratifier::item_set * stratum : comps) {
-        for (rule_stratifier::comp_vector::const_iterator it = comps.begin(); it!=cend; ++it) {
-            rule_stratifier::item_set * stratum = *it;
 
             SASSERT(stratum->size()==1);
             func_decl * head_pred = *stratum->begin();
@@ -318,10 +310,7 @@ namespace datalog {
             bool is_multi_occurrence_pred = m_tail_pred_ctr.get(head_pred)>1;
 
             const rule_vector& pred_rules = proposed_inlined_rules.get_predicate_rules(head_pred);
-            rule_vector::const_iterator iend = pred_rules.end();
+            for (rule * r : pred_rules) {
-            for (rule_vector::const_iterator iit = pred_rules.begin(); iit!=iend; ++iit) {
-                rule * r = *iit;
-
                 unsigned pt_len = r->get_positive_tail_size();
                 for (unsigned ti = 0; ti<pt_len; ++ti) {
                     func_decl * tail_pred = r->get_decl(ti);
@@ -405,28 +394,22 @@ namespace datalog {
         // now we start filling in the set of the inlined rules in a topological order,
         // so that we inline rules into other rules
 
-        SASSERT(m_inlined_rules.get_num_rules()==0);
+        SASSERT(m_inlined_rules.get_num_rules() == 0);
 
         const rule_stratifier::comp_vector& comps = candidate_inlined_set->get_stratifier().get_strats();
 
-        rule_stratifier::comp_vector::const_iterator cend = comps.end();
+        for (rule_stratifier::item_set * stratum : comps) {
-        for (rule_stratifier::comp_vector::const_iterator it = comps.begin(); it!=cend; ++it) {
+            SASSERT(stratum->size() == 1);
-            rule_stratifier::item_set * stratum = *it;
-            SASSERT(stratum->size()==1);
             func_decl * pred = *stratum->begin();
-
+            for (rule * r : candidate_inlined_set->get_predicate_rules(pred)) {
-            const rule_vector& pred_rules = candidate_inlined_set->get_predicate_rules(pred);
+                transform_rule(orig, r, m_inlined_rules);
-            rule_vector::const_iterator iend = pred_rules.end();
-            for (rule_vector::const_iterator iit = pred_rules.begin(); iit!=iend; ++iit) {
-                transform_rule(orig, *iit, m_inlined_rules);
             }
         }
 
         TRACE("dl", tout << "inlined rules after mutual inlining:\n" << m_inlined_rules;  );
 
-        for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) {
+        for (rule * r : m_inlined_rules) {
-            rule* r = m_inlined_rules.get_rule(i);
+            datalog::del_rule(m_mc, *r, false);
-            datalog::del_rule(m_mc, *r, true);
         }
     }
 
@@ -439,9 +422,7 @@ namespace datalog {
             rule_ref r(todo.back(), m_rm);
             todo.pop_back();
             unsigned pt_len = r->get_positive_tail_size();
-
             unsigned i = 0;
-
             for  (; i < pt_len && !inlining_allowed(orig, r->get_decl(i)); ++i) {};
 
             SASSERT(!has_quantifier(*r.get()));
@@ -455,9 +436,7 @@ namespace datalog {
 
             func_decl * pred = r->get_decl(i);
             const rule_vector& pred_rules = m_inlined_rules.get_predicate_rules(pred);
-            rule_vector::const_iterator iend = pred_rules.end();
+            for (rule * inl_rule : pred_rules) {
-            for (rule_vector::const_iterator iit = pred_rules.begin(); iit!=iend; ++iit) {
-                rule * inl_rule = *iit;
                 rule_ref inl_result(m_rm);
                 if (try_to_inline_rule(*r.get(), *inl_rule, i, inl_result)) {
                     todo.push_back(inl_result);
@@ -475,9 +454,8 @@ namespace datalog {
 
         bool something_done = false;
 
-        rule_set::iterator rend = orig.end();
+        for (rule* rl : orig) {
-        for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {
+            rule_ref r(rl, m_rm);
-            rule_ref r(*rit, m_rm);
             func_decl * pred = r->get_decl();
 
             // if inlining is allowed, then we are eliminating 
@@ -508,19 +486,14 @@ namespace datalog {
     bool mk_rule_inliner::is_oriented_rewriter(rule * r, rule_stratifier const& strat) {
         func_decl * head_pred = r->get_decl();
         unsigned head_strat = strat.get_predicate_strat(head_pred);
-
         unsigned head_arity = head_pred->get_arity();
-
-
         unsigned pt_len = r->get_positive_tail_size();
-        for (unsigned ti=0; ti<pt_len; ++ti) {
+        for (unsigned ti=0; ti < pt_len; ++ti) {            
-            
             func_decl * pred = r->get_decl(ti);
-
             unsigned pred_strat = strat.get_predicate_strat(pred);
-            SASSERT(pred_strat<=head_strat);
+            SASSERT(pred_strat <= head_strat);
 
-            if (pred_strat==head_strat) {
+            if (pred_strat == head_strat) {
                 if (pred->get_arity()>head_arity
                     || (pred->get_arity()==head_arity && pred->get_id()>=head_pred->get_id()) ) {
                     return false;
@@ -855,13 +828,9 @@ namespace datalog {
             return nullptr;
         }
 
-        rule_set::iterator end = source.end();
+        for (rule const* r : source) 
-        for (rule_set::iterator it = source.begin(); it != end; ++ it) {
+            if (has_quantifier(*r)) 
-            if (has_quantifier(**it)) {
+                return nullptr;        
-                return nullptr;
-            }
-        }
-        
 
         if (m_context.get_model_converter()) {
             hsmc = alloc(horn_subsume_model_converter, m);

src/muz/transforms/dl_mk_rule_inliner.h

@@ -45,7 +45,7 @@ namespace datalog {
             : m(ctx.get_manager()), m_rm(ctx.get_rule_manager()), m_context(ctx), 
             m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false), m_normalize(true) {}
             
-        /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
+        /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */
         bool unify_rules(rule const& tgt, unsigned tgt_idx, rule const& src);
 
         /**

src/muz/transforms/dl_mk_scale.h

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Add scale factor to linear (Real) arithemetic Horn clauses.
+    Add scale factor to linear (Real) arithmetic Horn clauses.
     The transformation replaces occurrences of isolated constants by
     a scale multiplied to each constant. 
 

src/muz/transforms/dl_transforms.cpp

@@ -59,7 +59,7 @@ namespace datalog {
         transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, ctx, 37000));
 
         if (ctx.get_params().datalog_subsumption()) {
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 35005));
+            transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 35005));
         }
         transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 35000));
         transf.register_plugin(alloc(datalog::mk_coi_filter, ctx, 34990));
@@ -67,20 +67,20 @@ namespace datalog {
 
         //and another round of inlining
         if (ctx.get_params().datalog_subsumption()) {
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34975));
+            transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34975));
         }
         transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34970));
         transf.register_plugin(alloc(datalog::mk_coi_filter, ctx, 34960));
         transf.register_plugin(alloc(datalog::mk_interp_tail_simplifier, ctx, 34950));
-
+        
         if (ctx.get_params().datalog_subsumption()) {
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34940));
+            transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34940));
-        transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34930));
+            transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34930));
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34920));
+            transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34920));
-        transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34910));
+            transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34910));
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34900));
+            transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34900));
-        transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34890));
+            transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34890));
-        transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34880));
+            transf.register_plugin(alloc(datalog::mk_subsumption_checker, ctx, 34880));
         }
         else {
             transf.register_plugin(alloc(datalog::mk_rule_inliner, ctx, 34930));

src/opt/CMakeLists.txt

@@ -2,7 +2,6 @@ z3_add_component(opt
   SOURCES
     maxres.cpp
     maxsmt.cpp
-    mss.cpp
     opt_cmds.cpp
     opt_context.cpp
     opt_pareto.cpp

src/opt/maxres.cpp

@@ -57,7 +57,6 @@ Notes:
 #include "opt/maxres.h"
 #include "ast/ast_pp.h"
 #include "solver/mus.h"
-#include "opt/mss.h"
 #include "sat/sat_solver/inc_sat_solver.h"
 #include "opt/opt_context.h"
 #include "ast/pb_decl_plugin.h"
@@ -90,7 +89,6 @@ private:
     obj_map<expr, rational> m_asm2weight;
     ptr_vector<expr> m_new_core;
     mus              m_mus;
-    mss              m_mss;
     expr_ref_vector  m_trail;
     strategy_t       m_st;
     rational         m_max_upper;    
@@ -121,7 +119,6 @@ public:
         m_index(index), 
         m_B(m), m_asms(m), m_defs(m),
         m_mus(c.get_solver()),
-        m_mss(c.get_solver(), m),
         m_trail(m),
         m_st(st),
         m_correction_set_size(0),

src/opt/mss.cpp

@@ -1,285 +0,0 @@
-/*++
-Copyright (c) 2014 Microsoft Corporation
-
-Module Name:
-
-    mss.cpp
-
-Abstract:
-   
-    MSS/MCS extraction.
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2014-2-8
-
-Notes:
-
-
---*/
-
-#include "solver/solver.h"
-#include "opt/mss.h"
-#include "ast/ast_pp.h"
-#include "model/model_smt2_pp.h"
-
-namespace opt {
-
-
-    mss::mss(solver& s, ast_manager& m): m_s(s), m(m) {
-    }
-    
-    mss::~mss() {
-    }    
-
-    bool mss::check_result() {
-        lbool is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr());
-        if (is_sat == l_undef) return true;
-        SASSERT(m_mss.empty() || is_sat == l_true);
-        if (is_sat == l_false) return false;
-        expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
-        for (; it != end; ++it) {
-            m_mss.push_back(*it);
-            is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr());
-            m_mss.pop_back();
-            if (is_sat == l_undef) return true;
-            SASSERT(is_sat == l_false);
-            if (is_sat == l_true) return false;
-        }
-        return true;
-    }
-
-    void mss::initialize(exprs& literals) {
-        expr* n;
-        expr_set lits, core_lits;
-        for (unsigned i = 0; i < literals.size(); ++i) {
-            n = literals[i];
-            lits.insert(n);
-            m.is_not(n, n);
-            if (!is_uninterp_const(n)) {
-                throw default_exception("arguments have to be uninterpreted literals");
-            }
-        }
-        exprs rest_core;
-        expr_ref tmp(m);
-        //
-        // the last core is a dummy core. It contains literals that
-        // did not occur in previous cores and did not evaluate to true
-        // in the current model.
-        //
-        for (unsigned i = 0; i < m_cores.size(); ++i) {
-            exprs const& core = m_cores[i];
-            for (unsigned j = 0; j < core.size(); ++j) {
-                expr* n = core[j];
-                if (!core_lits.contains(n)) {
-                    core_lits.insert(n);
-                    if (m_model->eval(n, tmp) && m.is_true(tmp)) {
-                        add_mss(n);
-                    }
-                    else {
-                        m_todo.push_back(n);
-                    }
-                }
-            }
-        }
-        for (unsigned i = 0; i < literals.size(); ++i) {
-            expr* n = literals[i];
-            if (!core_lits.contains(n)) {
-                if (m_model->eval(n, tmp) && m.is_true(tmp)) {
-                    m_mss.push_back(n);
-                }
-                else {
-                    rest_core.push_back(n);
-                    core_lits.insert(n);
-                    m_todo.push_back(n);
-                }
-            }
-        }
-        m_cores.push_back(rest_core);
-    }
-
-    void mss::add_mss(expr* n) {
-        if (!m_mss_set.contains(n)) {
-            m_mss_set.insert(n);
-            m_mss.push_back(n);
-        }
-    }
-
-    void mss::update_core(exprs& core) {
-        unsigned j = 0;
-        for (unsigned i = 0; i < core.size(); ++i) {            
-            expr* n = core[i];
-            if (!m_mss_set.contains(n)) {
-                if (i != j) {
-                    core[j] = core[i];
-                }
-                ++j;
-            }
-        }
-        core.resize(j);
-    }
-
-    void mss::update_mss() {
-        expr_ref tmp(m);
-        unsigned j = 0;
-        for (unsigned i = 0; i < m_todo.size(); ++i) {
-            expr* n = m_todo[i];
-            SASSERT(!m_mss_set.contains(n));
-            if (m_mcs.contains(n)) {
-                continue; // remove from cores.
-            }
-            if (m_model->eval(n, tmp) && m.is_true(tmp)) {
-                add_mss(n);
-            }
-            else {
-                if (j != i) {
-                    m_todo[j] = m_todo[i];
-                }
-                ++j;
-            }
-        }
-        m_todo.resize(j);
-    }       
-    
-    lbool mss::operator()(model* initial_model, vector<exprs> const& _cores, exprs& literals, exprs& mcs) {
-        m_mss.reset();
-        m_todo.reset();
-        m_model = initial_model;
-        m_cores.reset();
-        SASSERT(m_model);
-        m_cores.append(_cores);
-        initialize(literals);
-        TRACE("opt", 
-              display_vec(tout << "lits: ", literals.size(), literals.c_ptr());
-              display(tout););
-        lbool is_sat = l_true;
-        for (unsigned i = 0; is_sat == l_true && i < m_cores.size(); ++i) {
-            bool has_mcs = false;
-            bool is_last = i + 1 < m_cores.size();
-            SASSERT(check_invariant());
-            update_core(m_cores[i]); // remove members of mss
-            is_sat = process_core(1, m_cores[i], has_mcs, is_last); 
-        }    
-        if (is_sat == l_true) {
-            SASSERT(check_invariant());
-            TRACE("opt", display(tout););
-            literals.reset();
-            literals.append(m_mss);
-            mcs.reset();
-            expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
-            for (; it != end; ++it) {
-                mcs.push_back(*it);
-            }
-            SASSERT(check_result());
-        }
-        m_mcs.reset();
-        m_mss_set.reset();
-        IF_VERBOSE(2, display_vec(verbose_stream() << "mcs: ", mcs.size(), mcs.c_ptr()););
-        return is_sat;
-    }
-
-    
-    //
-    // at least one literal in core is false in current model.
-    // pick literals in core that are not yet in mss.
-    //    
-    lbool mss::process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last) {
-        SASSERT(sz > 0);
-        if (core.empty()) {
-            return l_true;
-        }
-        if (m.canceled()) {
-            return l_undef;
-        }
-        if (sz == 1 && core.size() == 1 && is_last && !has_mcs) {
-            // there has to be at least one false 
-            // literal in the core.
-            TRACE("opt", tout << "mcs: " << mk_pp(core[0], m) << "\n";);
-            m_mcs.insert(core[0]);
-            return l_true;
-        }
-        sz = std::min(sz, core.size());
-        TRACE("opt", display_vec(tout << "process (total " << core.size() << ") :", sz, core.c_ptr()););
-        unsigned sz_save = m_mss.size();
-        m_mss.append(sz, core.c_ptr());
-        lbool is_sat = m_s.check_sat(m_mss.size(), m_mss.c_ptr());
-        IF_VERBOSE(3, display_vec(verbose_stream() << "mss: ", m_mss.size(), m_mss.c_ptr()););
-        m_mss.resize(sz_save);
-        switch (is_sat) {
-        case l_true:
-            m_s.get_model(m_model);
-            update_mss();           
-            DEBUG_CODE(
-                for (unsigned i = 0; i < sz; ++i) {
-                    SASSERT(m_mss_set.contains(core[i]));
-                });
-            update_core(core);
-            return process_core(2*sz, core, has_mcs, is_last);
-        case l_false:
-            if (sz == 1) {
-                has_mcs = true;
-                m_mcs.insert(core[0]);
-                core[0] = core.back();
-                core.pop_back();
-            }
-            else {
-                exprs core2;            
-                core2.append(core.size()-sz, core.c_ptr()+sz);
-                core.resize(sz);
-                is_sat = process_core(sz, core2, has_mcs, false);
-                if (is_sat != l_true) {
-                    return is_sat;
-                }
-                update_core(core);
-            }
-            return process_core(1, core, has_mcs, is_last);
-        case l_undef:
-            return l_undef;
-        }
-        
-        return l_true;
-    }
-
-    void mss::display_vec(std::ostream& out, unsigned sz, expr* const* args) const {
-        for (unsigned i = 0; i < sz; ++i) {
-            out << mk_pp(args[i], m) << " ";
-        }
-        out << "\n";
-    }
-
-    void mss::display(std::ostream& out) const {
-        for (unsigned i = 0; i < m_cores.size(); ++i) {
-            display_vec(out << "core: ", m_cores[i].size(), m_cores[i].c_ptr());
-        }
-        expr_set::iterator it = m_mcs.begin(), end = m_mcs.end();
-        out << "mcs:\n";
-        for (; it != end; ++it) {
-            out << mk_pp(*it, m) << "\n";
-        }
-        out << "\n";
-        out << "mss:\n";
-        for (unsigned i = 0; i < m_mss.size(); ++i) {
-           out << mk_pp(m_mss[i], m) << "\n";
-        }
-        out << "\n";
-        if (m_model) {
-            model_smt2_pp(out, m, *(m_model.get()), 0);
-        }
-    }
-
-    bool mss::check_invariant() const {
-        if (!m_model) return true;
-        expr_ref tmp(m);
-        for (unsigned i = 0; i < m_mss.size(); ++i) {
-            expr* n = m_mss[i];
-            if (!m_model->eval(n, tmp)) return true;
-            CTRACE("opt", !m.is_true(tmp), tout << mk_pp(n, m) << " |-> " << mk_pp(tmp, m) << "\n";);
-            SASSERT(!m.is_false(tmp));
-        }
-        return true;
-    }
-}
-
-
-
-

src/opt/mss.h

@@ -1,57 +0,0 @@
-/*++
-Copyright (c) 2014 Microsoft Corporation
-
-Module Name:
-
-    mss.h
-
-Abstract:
-   
-    Maximal satisfying subset/minimal correction sets: MSS/MCS
-
-Author:
-
-    Nikolaj Bjorner (nbjorner) 2014-2-8
-
-Notes:
-
---*/
-#ifndef MSS_H_
-#define MSS_H_
-
-namespace opt {
-    class mss {
-        solver&       m_s;
-        ast_manager&  m;
-        typedef ptr_vector<expr> exprs;
-        typedef obj_hashtable<expr>  expr_set;
-        exprs         m_mss;
-        expr_set      m_mcs;
-        expr_set      m_mss_set;
-        vector<exprs> m_cores;
-        exprs         m_todo;
-        model_ref     m_model;
-    public:
-        mss(solver& s, ast_manager& m);
-        ~mss();
-        
-        lbool operator()(model* initial_model, vector<exprs> const& cores, exprs& literals, exprs& mcs);
-                
-
-        void get_model(model_ref& mdl) { mdl = m_model; }
-
-    private:
-        void  initialize(exprs& literals);
-        bool  check_result();
-        void  add_mss(expr* n);
-        void  update_mss();
-        void  update_core(exprs& core);
-        lbool process_core(unsigned sz, exprs& core, bool& has_mcs, bool is_last);
-        void display(std::ostream& out) const;
-        void display_vec(std::ostream& out, unsigned sz, expr* const* args) const;
-        bool check_invariant() const;
-    };
-
-};
-
-#endif

src/opt/opt_context.cpp

@@ -402,8 +402,8 @@ namespace opt {
     */
     bool context::scoped_lex() {
         if (m_maxsat_engine == symbol("maxres")) {
-            for (unsigned i = 0; i < m_objectives.size(); ++i) {
+            for (auto const& o : m_objectives) {
-                if (m_objectives[i].m_type != O_MAXSMT) return true;
+                if (o.m_type != O_MAXSMT) return true;
             }
             return false;
         }
@@ -413,14 +413,16 @@ namespace opt {
     lbool context::execute_lex() {
         lbool r = l_true;
         bool sc = scoped_lex();
-        IF_VERBOSE(1, verbose_stream() << "(optsmt:lex)\n";);
+        IF_VERBOSE(1, verbose_stream() << "(opt :lex)\n";);
-        for (unsigned i = 0; r == l_true && i < m_objectives.size(); ++i) {
+        unsigned sz = m_objectives.size();
-            bool is_last = i + 1 == m_objectives.size();
+        for (unsigned i = 0; r == l_true && i < sz; ++i) {
-            r = execute(m_objectives[i], i + 1 < m_objectives.size(), sc && !is_last);
+            objective const& o = m_objectives[i];
+            bool is_last = i + 1 == sz;            
+            r = execute(o, i + 1 < sz, sc && !is_last && o.m_type != O_MAXSMT);
             if (r == l_true && !get_lower_as_num(i).is_finite()) {
                 return r;
             }
-            if (r == l_true && i + 1 < m_objectives.size()) {
+            if (r == l_true && i + 1 < sz) {
                 update_lower();
             }
         }

src/opt/opt_solver.cpp

@@ -227,9 +227,13 @@ namespace opt {
         smt::theory_var v = m_objective_vars[i];
         bool has_shared = false;
         inf_eps val = get_optimizer().maximize(v, blocker, has_shared);
+        get_model(m_model);
         inf_eps val2;
         m_valid_objectives[i] = true;
         TRACE("opt", tout << (has_shared?"has shared":"non-shared") << "\n";);
+        if (!m_models[i]) {
+            set_model(i);
+        }
         if (m_context.get_context().update_model(has_shared)) {
             if (has_shared && val != current_objective_value(i)) {
                 decrement_value(i, val);
@@ -247,7 +251,7 @@ namespace opt {
                 tout << "objective:     " << mk_pp(m_objective_terms[i].get(), m) << "\n";
                 tout << "maximal value: " << val << "\n"; 
                 tout << "new condition: " << blocker << "\n";
-                model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); });
+                if (m_models[i]) model_smt2_pp(tout << "update model:\n", m, *m_models[i], 0); });
     }
 
     void opt_solver::set_model(unsigned i) {
@@ -299,6 +303,7 @@ namespace opt {
 
     void opt_solver::get_model(model_ref & m) {
         m_context.get_model(m);
+        if (!m) m = m_model; else m_model = m;
     }
     
     proof * opt_solver::get_proof() {

src/opt/opt_solver.h

@@ -73,6 +73,7 @@ namespace opt {
         filter_model_converter& m_fm;
         progress_callback * m_callback;
         symbol              m_logic;
+        model_ref           m_model;
         svector<smt::theory_var>  m_objective_vars;
         vector<inf_eps>     m_objective_values;
         sref_vector<model>  m_models;

src/parsers/smt2/smt2parser.cpp

@@ -970,6 +970,9 @@ namespace smt2 {
                 check_rparen_next("invalid datatype declaration, ')' expected");
             }
             else {
+                if (dt_name) {
+                    m_ctx.insert(pm().mk_psort_dt_decl(0, *dt_name));
+                }
                 parse_constructor_decls(ct_decls);
             }
             check_rparen_next("invalid datatype declaration, ')' expected");
@@ -1411,7 +1414,7 @@ namespace smt2 {
             else {
                 SASSERT(is_app(pattern));
                 func_decl * f = to_app(pattern)->get_decl();
-                func_decl * r = dtutil().get_constructor_recognizer(f);
+                func_decl * r = dtutil().get_constructor_is(f);
                 ptr_vector<func_decl> const * acc = dtutil().get_constructor_accessors(f);
                 shifter()(t, acc->size(), tsh);
                 for (func_decl* a : *acc) {

src/qe/qe_datatype_plugin.cpp

@@ -261,7 +261,7 @@ namespace qe {
                 return false;
             }
             func_decl* c = a->get_decl();
-            func_decl* r = m_util.get_constructor_recognizer(c);
+            func_decl_ref r(m_util.get_constructor_is(c), m);
             ptr_vector<func_decl> const & acc = *m_util.get_constructor_accessors(c);
             SASSERT(acc.size() == a->get_num_args());
             //
@@ -380,7 +380,7 @@ namespace qe {
             }
             func_decl* c = l->get_decl();
             ptr_vector<func_decl> const& acc = *m_util.get_constructor_accessors(c);
-            func_decl* rec = m_util.get_constructor_recognizer(c);
+            func_decl* rec = m_util.get_constructor_is(c);
             expr_ref_vector conj(m);
             conj.push_back(m.mk_app(rec, r));
             for (unsigned i = 0; i < acc.size(); ++i) {
@@ -627,7 +627,7 @@ namespace qe {
             // 
             if (!has_recognizer(x, fml, r, c)) {
                 c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned());
-                r = m_datatype_util.get_constructor_recognizer(c);
+                r = m_datatype_util.get_constructor_is(c);
                 app* is_c = m.mk_app(r, x);                
                 // assert v => r(x)            
                 m_ctx.add_constraint(true, is_c);
@@ -674,7 +674,7 @@ namespace qe {
             // 
             if (!has_recognizer(x, fml, r, c)) {
                 c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned());
-                r = m_datatype_util.get_constructor_recognizer(c);
+                r = m_datatype_util.get_constructor_is(c);
                 app* is_c = m.mk_app(r, x);                
                 fml = m.mk_and(is_c, fml);
                 app_ref fresh_x(m.mk_fresh_const("x", s), m);
@@ -775,7 +775,7 @@ namespace qe {
             }
             
             c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned());
-            r = m_datatype_util.get_constructor_recognizer(c);
+            r = m_datatype_util.get_constructor_is(c);
             app* is_c = m.mk_app(r, x);
             
             // assert v => r(x)

src/qe/qe_datatypes.cpp

@@ -151,7 +151,7 @@ namespace qe {
                 return false;
             }
             func_decl* c = a->get_decl();
-            func_decl* rec = dt.get_constructor_recognizer(c);
+            func_decl_ref rec(dt.get_constructor_is(c), m);
             ptr_vector<func_decl> const & acc = *dt.get_constructor_accessors(c);
             SASSERT(acc.size() == a->get_num_args());
             //
@@ -232,7 +232,7 @@ namespace qe {
             func_decl* c = to_app(l)->get_decl();
             ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(c);
             if (!is_app_of(r, c)) {
-                lits.push_back(m.mk_app(dt.get_constructor_recognizer(c), r));
+                lits.push_back(m.mk_app(dt.get_constructor_is(c), r));
             }
             for (unsigned i = 0; i < acc.size(); ++i) {
                 lits.push_back(m.mk_eq(to_app(l)->get_arg(i), access(c, i, acc, r)));

src/qe/qe_lite.cpp

@@ -692,7 +692,7 @@ namespace eq {
                 }
             }
             else {
-                func_decl* rec = dt.get_constructor_recognizer(d);
+                func_decl* rec = dt.get_constructor_is(d);
                 conjs.push_back(m.mk_app(rec, r));
                 ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(d);
                 for (unsigned i = 0; i < acc.size(); ++i) {

src/sat/sat_solver.cpp

@@ -1139,7 +1139,7 @@ namespace sat {
     }
 
     void solver::reinit_assumptions() {
-        if (tracking_assumptions() && scope_lvl() == 0) {
+        if (tracking_assumptions() && scope_lvl() == 0 && !inconsistent()) {
             TRACE("sat", tout << m_assumptions << "\n";);
             push();
             for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) {

src/smt/asserted_formulas.cpp

@@ -27,8 +27,9 @@ Revision History:
 #include "ast/macros/quasi_macros.h"
 #include "smt/asserted_formulas.h"
 
-asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
+asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_ref const& p):
     m(m),
+    m_smt_params(sp),
     m_params(p),
     m_rewriter(m),
     m_substitution(m),
@@ -46,7 +47,6 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
     m_refine_inj_axiom(*this),
     m_max_bv_sharing_fn(*this),
     m_elim_term_ite(*this),
-    m_pull_cheap_ite_trees(*this),
     m_pull_nested_quantifiers(*this),
     m_elim_bvs_from_quantifiers(*this),
     m_cheap_quant_fourier_motzkin(*this),
@@ -66,20 +66,20 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
 }
 
 void asserted_formulas::setup() {
-    switch (m_params.m_lift_ite) {
+    switch (m_smt_params.m_lift_ite) {
     case LI_FULL:
-        m_params.m_ng_lift_ite = LI_NONE;
+        m_smt_params.m_ng_lift_ite = LI_NONE;
         break;
     case LI_CONSERVATIVE:
-        if (m_params.m_ng_lift_ite == LI_CONSERVATIVE)
+        if (m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE)
-            m_params.m_ng_lift_ite = LI_NONE;
+            m_smt_params.m_ng_lift_ite = LI_NONE;
         break;
     default:
         break;
     }
 
-    if (m_params.m_relevancy_lvl == 0)
+    if (m_smt_params.m_relevancy_lvl == 0)
-        m_params.m_relevancy_lemma = false;
+        m_smt_params.m_relevancy_lemma = false;
 }
 
 
@@ -118,21 +118,24 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
     }
 }
 
+void asserted_formulas::updt_params(params_ref const& p) {
+    m_params.append(p);
+}
+
 void asserted_formulas::set_eliminate_and(bool flag) {
     if (flag == m_elim_and) return;
     m_elim_and = flag;
-    params_ref p;
+    if (m_smt_params.m_pull_cheap_ite) m_params.set_bool("pull_cheap_ite", true);
-    p.set_bool("pull_cheap_ite", false);
+    m_params.set_bool("elim_and", flag);
-    p.set_bool("elim_and", flag);
+    m_params.set_bool("arith_ineq_lhs", true);
-    p.set_bool("arith_ineq_lhs", true);
+    m_params.set_bool("sort_sums", true);
-    p.set_bool("sort_sums", true);
+    m_params.set_bool("rewrite_patterns", true);
-    p.set_bool("rewrite_patterns", true);
+    m_params.set_bool("eq2ineq", m_smt_params.m_arith_eq2ineq);
-    p.set_bool("eq2ineq", m_params.m_arith_eq2ineq);
+    m_params.set_bool("gcd_rounding", true);
-    p.set_bool("gcd_rounding", true);
+    m_params.set_bool("expand_select_store", true);
-    p.set_bool("expand_select_store", true);
+    m_params.set_bool("bv_sort_ac", true);
-    p.set_bool("bv_sort_ac", true);
+    m_params.set_bool("som", true);
-    p.set_bool("som", true);
+    m_rewriter.updt_params(m_params);
-    m_rewriter.updt_params(p);
     flush_cache();
 }
 
@@ -144,7 +147,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
     if (inconsistent())
         return;
 
-    if (m_params.m_preprocess) {
+    if (m_smt_params.m_preprocess) {
         TRACE("assert_expr_bug", tout << r << "\n";);
         set_eliminate_and(false); // do not eliminate and before nnf.
         m_rewriter(e, r, pr);
@@ -227,7 +230,7 @@ void asserted_formulas::reduce() {
         return;
     if (m_qhead == m_formulas.size())
         return;
-    if (!m_params.m_preprocess)
+    if (!m_smt_params.m_preprocess)
         return;
     if (m_macro_manager.has_macros())
         invoke(m_find_macros);
@@ -241,7 +244,6 @@ void asserted_formulas::reduce() {
     if (!invoke(m_nnf_cnf)) return;
     set_eliminate_and(true);
     if (!invoke(m_reduce_asserted_formulas)) return;
-    if (!invoke(m_pull_cheap_ite_trees)) return;
     if (!invoke(m_pull_nested_quantifiers)) return;
     if (!invoke(m_lift_ite)) return;
     if (!invoke(m_ng_lift_ite)) return;

src/smt/asserted_formulas.h

@@ -26,7 +26,6 @@ Revision History:
 #include "ast/rewriter/bit2int.h"
 #include "ast/rewriter/maximize_ac_sharing.h"
 #include "ast/rewriter/distribute_forall.h"
-#include "ast/rewriter/pull_ite_tree.h"
 #include "ast/rewriter/push_app_ite.h"
 #include "ast/rewriter/inj_axiom.h"
 #include "ast/rewriter/bv_elim.h"
@@ -44,7 +43,8 @@ Revision History:
 class asserted_formulas {
     
     ast_manager &               m;
-    smt_params &                m_params;
+    smt_params &                m_smt_params;
+    params_ref                  m_params;
     th_rewriter                 m_rewriter;
     expr_substitution           m_substitution;
     scoped_expr_substitution    m_scoped_substitution;
@@ -89,7 +89,7 @@ class asserted_formulas {
     public:
         find_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-macros") {}
         void operator()() override { af.find_macros_core(); }
-        bool should_apply() const override { return af.m_params.m_macro_finder && af.has_quantifiers(); }
+        bool should_apply() const override { return af.m_smt_params.m_macro_finder && af.has_quantifiers(); }
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
     };
 
@@ -97,7 +97,7 @@ class asserted_formulas {
     public:
         apply_quasi_macros_fn(asserted_formulas& af): simplify_fmls(af, "find-quasi-macros") {}
         void operator()() override { af.apply_quasi_macros(); }
-        bool should_apply() const override { return af.m_params.m_quasi_macros && af.has_quantifiers(); }
+        bool should_apply() const override { return af.m_smt_params.m_quasi_macros && af.has_quantifiers(); }
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
     };
 
@@ -105,7 +105,7 @@ class asserted_formulas {
     public:
         nnf_cnf_fn(asserted_formulas& af): simplify_fmls(af, "nnf-cnf") {}
         void operator()() override { af.nnf_cnf(); }
-        bool should_apply() const override { return af.m_params.m_nnf_cnf || (af.m_params.m_mbqi && af.has_quantifiers()); }
+        bool should_apply() const override { return af.m_smt_params.m_nnf_cnf || (af.m_smt_params.m_mbqi && af.has_quantifiers()); }
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
     };
 
@@ -113,7 +113,7 @@ class asserted_formulas {
     public:
         propagate_values_fn(asserted_formulas& af): simplify_fmls(af, "propagate-values") {}
         void operator()() override { af.propagate_values(); }
-        bool should_apply() const override { return af.m_params.m_propagate_values; }
+        bool should_apply() const override { return af.m_smt_params.m_propagate_values; }
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { UNREACHABLE(); }
     };
 
@@ -122,30 +122,30 @@ class asserted_formulas {
     public:
         distribute_forall_fn(asserted_formulas& af): simplify_fmls(af, "distribute-forall"), m_functor(af.m) {}
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_functor(j.get_fml(), n); }
-        bool should_apply() const override { return af.m_params.m_distribute_forall && af.has_quantifiers(); }
+        bool should_apply() const override { return af.m_smt_params.m_distribute_forall && af.has_quantifiers(); }
         void post_op() override { af.reduce_and_solve();  TRACE("asserted_formulas", af.display(tout);); }
     };
 
     class pattern_inference_fn : public simplify_fmls {
         pattern_inference_rw m_infer;
     public:
-        pattern_inference_fn(asserted_formulas& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_params) {}
+        pattern_inference_fn(asserted_formulas& af): simplify_fmls(af, "pattern-inference"), m_infer(af.m, af.m_smt_params) {}
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_infer(j.get_fml(), n, p); }
-        bool should_apply() const override { return af.m_params.m_ematching && af.has_quantifiers(); }
+        bool should_apply() const override { return af.m_smt_params.m_ematching && af.has_quantifiers(); }
     };
 
     class refine_inj_axiom_fn : public simplify_fmls {
     public:
         refine_inj_axiom_fn(asserted_formulas& af): simplify_fmls(af, "refine-injectivity") {}
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override;
-        bool should_apply() const override { return af.m_params.m_refine_inj_axiom && af.has_quantifiers(); }
+        bool should_apply() const override { return af.m_smt_params.m_refine_inj_axiom && af.has_quantifiers(); }
     };
 
     class max_bv_sharing_fn : public simplify_fmls {
     public:
         max_bv_sharing_fn(asserted_formulas& af): simplify_fmls(af, "maximizing-bv-sharing") {}
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { af.m_bv_sharing(j.get_fml(), n, p); }
-        bool should_apply() const override { return af.m_params.m_max_bv_sharing; }
+        bool should_apply() const override { return af.m_smt_params.m_max_bv_sharing; }
         void post_op() override { af.m_reduce_asserted_formulas(); }
     };
 
@@ -154,7 +154,7 @@ class asserted_formulas {
     public:
         elim_term_ite_fn(asserted_formulas& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {}
         void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.get_fml(), n, p); }
-        bool should_apply() const override { return af.m_params.m_eliminate_term_ite && af.m_params.m_lift_ite != LI_FULL; }
+        bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != LI_FULL; }
         void post_op() override { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); }
     };
 
@@ -172,13 +172,12 @@ class asserted_formulas {
 
 #define MK_SIMPLIFIERF(NAME, FUNCTOR, MSG, APP, REDUCE) MK_SIMPLIFIERA(NAME, FUNCTOR, MSG, APP, (af.m), REDUCE)
 
-    MK_SIMPLIFIERF(pull_cheap_ite_trees, pull_cheap_ite_tree_rw, "pull-cheap-ite-trees", af.m_params.m_pull_cheap_ite_trees, false);
+    MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_smt_params.m_pull_nested_quantifiers && af.has_quantifiers(), false);
-    MK_SIMPLIFIERF(pull_nested_quantifiers, pull_nested_quant, "pull-nested-quantifiers", af.m_params.m_pull_nested_quantifiers && af.has_quantifiers(), false);
+    MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_smt_params.m_eliminate_bounds && af.has_quantifiers(), true);
-    MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_params.m_eliminate_bounds && af.has_quantifiers(), true);
+    MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_smt_params.m_bb_quantifiers, true);
-    MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_params.m_bb_quantifiers, true);
+    MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_smt_params.m_simplify_bit2int, true);
-    MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_params.m_simplify_bit2int, true);
+    MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_lift_ite == LI_CONSERVATIVE), true);
-    MK_SIMPLIFIERA(lift_ite, push_app_ite_rw, "lift-ite", af.m_params.m_lift_ite != LI_NONE, (af.m, af.m_params.m_lift_ite == LI_CONSERVATIVE), true);
+    MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE), true);
-    MK_SIMPLIFIERA(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_params.m_ng_lift_ite != LI_NONE, (af.m, af.m_params.m_ng_lift_ite == LI_CONSERVATIVE), true);
 
 
     reduce_asserted_formulas_fn m_reduce_asserted_formulas;
@@ -187,7 +186,6 @@ class asserted_formulas {
     refine_inj_axiom_fn         m_refine_inj_axiom;
     max_bv_sharing_fn           m_max_bv_sharing_fn;
     elim_term_ite_fn            m_elim_term_ite;
-    pull_cheap_ite_trees        m_pull_cheap_ite_trees;
     pull_nested_quantifiers     m_pull_nested_quantifiers;
     elim_bvs_from_quantifiers   m_elim_bvs_from_quantifiers;
     cheap_quant_fourier_motzkin m_cheap_quant_fourier_motzkin;
@@ -219,14 +217,14 @@ class asserted_formulas {
     bool is_gt(expr* lhs, expr* rhs);
     void compute_depth(expr* e);
     unsigned depth(expr* e) { return m_expr2depth[e]; }
-    bool pull_cheap_ite_trees();
 
     void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
 
 public:
-    asserted_formulas(ast_manager & m, smt_params & p);
+    asserted_formulas(ast_manager & m, smt_params & smtp, params_ref const& p);
     ~asserted_formulas();
 
+    void updt_params(params_ref const& p);
     bool has_quantifiers() const { return m_has_quantifiers; }
     void setup();
     void assert_expr(expr * e, proof * in_pr);

src/smt/mam.cpp

@@ -3924,7 +3924,7 @@ namespace smt {
         }
 
 #ifdef Z3DEBUG
-        virtual bool check_missing_instances() {
+        bool check_missing_instances() override {
             TRACE("missing_instance", tout << "checking for missing instances...\n";);
             flet<bool> l(m_check_missing_instances, true);
             rematch(false);

src/smt/params/preprocessor_params.cpp

@@ -41,7 +41,7 @@ void preprocessor_params::display(std::ostream & out) const {
 
     DISPLAY_PARAM(m_lift_ite);
     DISPLAY_PARAM(m_ng_lift_ite);
-    DISPLAY_PARAM(m_pull_cheap_ite_trees);
+    DISPLAY_PARAM(m_pull_cheap_ite);
     DISPLAY_PARAM(m_pull_nested_quantifiers);
     DISPLAY_PARAM(m_eliminate_term_ite);
     DISPLAY_PARAM(m_macro_finder);

src/smt/params/preprocessor_params.h

@@ -32,7 +32,7 @@ struct preprocessor_params : public pattern_inference_params,
                              public bit_blaster_params {
     lift_ite_kind   m_lift_ite;
     lift_ite_kind   m_ng_lift_ite;  // lift ite for non ground terms
-    bool            m_pull_cheap_ite_trees;
+    bool            m_pull_cheap_ite;
     bool            m_pull_nested_quantifiers;
     bool            m_eliminate_term_ite;
     bool            m_macro_finder;
@@ -54,7 +54,7 @@ public:
     preprocessor_params(params_ref const & p = params_ref()):
         m_lift_ite(LI_NONE),
         m_ng_lift_ite(LI_NONE), 
-        m_pull_cheap_ite_trees(false),
+        m_pull_cheap_ite(false),
         m_pull_nested_quantifiers(false),
         m_eliminate_term_ite(false),
         m_macro_finder(false),

src/smt/smt_context.cpp

@@ -45,7 +45,7 @@ namespace smt {
         m_fparams(p),
         m_params(_p),
         m_setup(*this, p),
-        m_asserted_formulas(m, p),
+        m_asserted_formulas(m, p, _p),
         m_qmanager(alloc(quantifier_manager, *this, p, _p)),
         m_model_generator(alloc(model_generator, m)),
         m_relevancy_propagator(mk_relevancy_propagator(*this)),
@@ -132,6 +132,10 @@ namespace smt {
         return !m_manager.limit().inc();
     }
 
+    void context::updt_params(params_ref const& p) {
+        m_params.append(p);
+        m_asserted_formulas.updt_params(p);
+    }
 
     void context::copy(context& src_ctx, context& dst_ctx) {
         ast_manager& dst_m = dst_ctx.get_manager();
@@ -3143,6 +3147,7 @@ namespace smt {
             push_scope();
             for (unsigned i = 0; i < num_assumptions; i++) {
                 expr * curr_assumption = assumptions[i];
+                if (m_manager.is_true(curr_assumption)) continue;
                 SASSERT(is_valid_assumption(m_manager, curr_assumption));
                 proof * pr = m_manager.mk_asserted(curr_assumption);
                 internalize_assertion(curr_assumption, pr, 0);
@@ -4313,9 +4318,7 @@ namespace smt {
             if (m_fparams.m_model_compact)
                 m_proto_model->compress();
             TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model););
-        }
+            IF_VERBOSE(11, model_pp(verbose_stream(), *m_proto_model););
-        else {
-
         }
     }
 

src/smt/smt_context.h

@@ -262,6 +262,8 @@ namespace smt {
             return m_params;
         }
 
+        void updt_params(params_ref const& p);
+
         bool get_cancel_flag();
 
         region & get_region() {
@@ -1387,7 +1389,7 @@ namespace smt {
         void flush();
         config_mode get_config_mode(bool use_static_features) const;
         virtual void setup_context(bool use_static_features);
-        void setup_components(void);
+        void setup_components();
         void pop_to_base_lvl();
         void pop_to_search_lvl();
 #ifdef Z3DEBUG

src/smt/smt_kernel.cpp

@@ -123,7 +123,6 @@ namespace smt {
             return m_kernel.preferred_sat(asms, cores);
         }
 
-
         lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) {
             return m_kernel.find_mutexes(vars, mutexes);
         }
@@ -196,9 +195,7 @@ namespace smt {
         }
 
         void updt_params(params_ref const & p) {
-            // We don't need params2smt_params anymore. smt_params has support for reading params_ref.
+            m_kernel.updt_params(p);
-            // The update is performed at smt_kernel "users".
-            // params2smt_params(p, fparams());
         }
     };
 
@@ -218,7 +215,6 @@ namespace smt {
         imp::copy(*src.m_imp, *dst.m_imp);
     }
 
-
     bool kernel::set_logic(symbol logic) {
         return m_imp->set_logic(logic);
     }
@@ -263,9 +259,9 @@ namespace smt {
     }
 
     void kernel::reset() {
-        ast_manager & _m       = m();
+        ast_manager & _m = m();
         smt_params & fps = m_imp->fparams();
-        params_ref ps          = m_imp->params();
+        params_ref ps    = m_imp->params();
         #pragma omp critical (smt_kernel)
         {
             m_imp->~imp();

src/smt/smt_model_finder.cpp

@@ -914,6 +914,7 @@ namespace smt {
                         func_interp * fi = m_model->get_func_interp(f);
                         if (fi == nullptr) {
                             fi = alloc(func_interp, m, f->get_arity());
+                            TRACE("model_finder", tout << "register " << f->get_name() << "\n";);
                             m_model->register_decl(f, fi);
                             SASSERT(fi->is_partial());
                         }
@@ -1784,13 +1785,8 @@ namespace smt {
                 return !m_cond_macros.empty();
             }
 
-            macro_iterator begin_macros() const {
+            ptr_vector<cond_macro> const& macros() const { return m_cond_macros; }
-                return m_cond_macros.begin();
-            }
 
-            macro_iterator end_macros() const {
-                return m_cond_macros.end();
-            }
 
             void set_the_one(func_decl * m) {
                 m_the_one = m;
@@ -2445,6 +2441,7 @@ namespace smt {
                     m_model->register_decl(f, fi);
                 }
                 fi->set_else(f_else);
+                TRACE("model_finder", tout << f->get_name() << " " << mk_pp(f_else, m_manager) << "\n";);
             }
 
             virtual bool process(ptr_vector<quantifier> const & qs, ptr_vector<quantifier> & new_qs, ptr_vector<quantifier> & residue) = 0;
@@ -2499,10 +2496,7 @@ namespace smt {
 
             bool process(quantifier * q, ptr_vector<quantifier> const & qs) {
                 quantifier_info * qi = get_qinfo(q);
-                quantifier_info::macro_iterator it  = qi->begin_macros();
+                for (cond_macro* m : qi->macros()) {
-                quantifier_info::macro_iterator end = qi->end_macros();
-                for (; it != end; ++it) {
-                    cond_macro * m = *it;
                     if (!m->satisfy_atom())
                         continue;
                     func_decl * f  = m->get_f();
@@ -2548,10 +2542,10 @@ namespace smt {
               where Q_{f_i} is the set of quantifiers that contain the function f_i.
               Let f_i = def_i be macros (in this solver conditions are ignored).
               Let Q_{f_i = def_i} be the set of quantifiers where f_i = def_i is a macro.
-              Then, the set Q can be satisfied using f_1 = def_1 ... f_n = d_n
+              Then, the set Q can be satisfied using f_1 = def_1 ... f_n = def_n
               when
 
-              Q_{f_1} union ... union Q_{f_n} = Q_{f_1 = def_1} ... Q_{f_n = d_n} (*)
+              Q_{f_1} union ... union Q_{f_n} = Q_{f_1 = def_1} ... Q_{f_n = def_n} (*)
 
               So, given a set of macros f_1 = def_1, ..., f_n = d_n, it is very easy to check
               whether they can be used to satisfy all quantifiers that use f_1, ..., f_n in
@@ -2630,12 +2624,7 @@ namespace smt {
                 s->insert(q);
             }
 
-            quantifier_set * get_q_f(func_decl * f) {
+            quantifier_set * get_q_f(func_decl * f) { return m_q_f[f]; }
-                quantifier_set * s = nullptr;
-                m_q_f.find(f, s);
-                SASSERT(s != 0);
-                return s;
-            }
 
             quantifier_set * get_q_f_def(func_decl * f, expr * def) {
                 quantifier_set * s = nullptr;
@@ -2644,12 +2633,7 @@ namespace smt {
                 return s;
             }
 
-            expr_set * get_f_defs(func_decl * f) {
+            expr_set * get_f_defs(func_decl * f) { return m_f2defs[f]; }
-                expr_set * s = nullptr;
-                m_f2defs.find(f, s);
-                SASSERT(s != 0);
-                return s;
-            }
 
             void reset_q_fs() {
                 std::for_each(m_qsets.begin(), m_qsets.end(), delete_proc<quantifier_set>());
@@ -2666,10 +2650,7 @@ namespace smt {
 
             bool is_candidate(quantifier * q) const {
                 quantifier_info * qi = get_qinfo(q);
-                quantifier_info::macro_iterator it  = qi->begin_macros();
+                for (cond_macro * m : qi->macros()) {
-                quantifier_info::macro_iterator end = qi->end_macros();
-                for (; it != end; ++it) {
-                    cond_macro * m = *it;
                     if (m->satisfy_atom() && !m_forbidden.contains(m->get_f()))
                         return true;
                 }
@@ -2712,10 +2693,7 @@ namespace smt {
                         if (!m_forbidden.contains(f))
                             insert_q_f(q, f);
                     }
-                    quantifier_info::macro_iterator it3  = qi->begin_macros();
+                    for (cond_macro * m : qi->macros()) {
-                    quantifier_info::macro_iterator end3 = qi->end_macros();
-                    for (; it3 != end3; ++it3) {
-                        cond_macro * m = *it3;
                         if (m->satisfy_atom() && !m_forbidden.contains(m->get_f())) {
                             insert_q_f_def(q, m->get_f(), m->get_def());
                             m_candidates.insert(m->get_f());
@@ -2842,11 +2820,7 @@ namespace smt {
             void get_candidates_from_residue(func_decl_set & candidates) {
                 for (quantifier * q : m_residue) {
                     quantifier_info * qi = get_qinfo(q);
-
+                    for (cond_macro * m : qi->macros()) {
-                    quantifier_info::macro_iterator it2  = qi->begin_macros();
-                    quantifier_info::macro_iterator end2 = qi->end_macros();
-                    for (; it2 != end2; ++it2) {
-                        cond_macro * m = *it2;
                         func_decl * f  = m->get_f();
                         if (m->satisfy_atom() && !m_forbidden.contains(f) && !m_fs.contains(f)) {
                             candidates.insert(f);
@@ -2875,6 +2849,7 @@ namespace smt {
 
                     m_satisfied.push_scope();
                     m_residue.push_scope();
+                    TRACE("model_finder", tout << f->get_name() << " " << mk_pp(def, m_manager) << "\n";);
                     m_fs.insert(f, def);
 
                     if (update_satisfied_residue(f, def)) {
@@ -2889,12 +2864,56 @@ namespace smt {
                 }
             }
 
+            /**
+               \brief check if satisfied subset introduces a cyclic dependency.
+
+               f_1 = def_1(f_2), ..., f_n = def_n(f_1)
+             */
+
+            expr_mark               m_visited;
+            obj_hashtable<func_decl> m_acyclic;
+            bool is_cyclic() {
+                m_acyclic.reset();
+                while (true) {
+                    unsigned sz = m_acyclic.size();
+                    if (sz == m_fs.size()) return false; // there are no cyclic dependencies
+                    for (auto const& kv : m_fs) {
+                        func_decl * f = kv.m_key;
+                        if (m_acyclic.contains(f)) continue;
+                        if (is_acyclic(kv.m_value))
+                            m_acyclic.insert(f);
+                    }
+                    if (sz == m_acyclic.size()) return true; // no progress, so dependency cycle found.                    
+                }
+            }
+           
+            struct occurs {};
+            struct occurs_check {
+                hint_solver& m_cls;
+                occurs_check(hint_solver& hs): m_cls(hs) {}
+                void operator()(app* n) { if (m_cls.m_fs.contains(n->get_decl()) && !m_cls.m_acyclic.contains(n->get_decl())) throw occurs(); }
+                void operator()(var* n) {}
+                void operator()(quantifier* n) {}
+            };
+            bool is_acyclic(expr* def) {
+                m_visited.reset();
+                occurs_check oc(*this);
+                try {
+                    for_each_expr(oc, m_visited, def);
+                }
+                catch (occurs) {
+                    return false;
+                }
+                return true;
+            }
+
             /**
                \brief Try to reduce m_residue (if not empty) by selecting a function f
                that is a macro in the residue.
             */
             void greedy(unsigned depth) {
                 if (m_residue.empty()) {
+                    if (is_cyclic()) return;
                     TRACE("model_finder_hint",
                           tout << "found subset that is satisfied by macros\n";
                           display_search_state(tout););
@@ -3007,11 +3026,11 @@ namespace smt {
             qi_params const *                      m_qi_params;
 
             bool add_macro(func_decl * f, expr * f_else) {
-                TRACE("non_auf_macro_solver", tout << "trying to add macro for " << f->get_name() << "\n" << mk_pp(f_else, m_manager) << "\n";);
+                TRACE("model_finder", tout << "trying to add macro for " << f->get_name() << "\n" << mk_pp(f_else, m_manager) << "\n";);
                 func_decl_set * s = m_dependencies.mk_func_decl_set();
                 m_dependencies.collect_ng_func_decls(f_else, s);
                 if (!m_dependencies.insert(f, s)) {
-                    TRACE("non_auf_macro_solver", tout << "failed to add macro\n";);
+                    TRACE("model_finder", tout << "failed to add macro\n";);
                     return false; // cyclic dependency
                 }
                 set_else_interp(f, f_else);
@@ -3033,10 +3052,7 @@ namespace smt {
             cond_macro * get_macro_for(func_decl * f, quantifier * q) {
                 cond_macro * r = nullptr;
                 quantifier_info * qi = get_qinfo(q);
-                quantifier_info::macro_iterator it  = qi->begin_macros();
+                for (cond_macro * m : qi->macros()) {
-                quantifier_info::macro_iterator end = qi->end_macros();
-                for (; it != end; ++it) {
-                    cond_macro * m = *it;
                     if (m->get_f() == f && !m->is_hint() && is_better_macro(m, r))
                         r = m;
                 }
@@ -3048,13 +3064,10 @@ namespace smt {
             void collect_candidates(ptr_vector<quantifier> const & qs, obj_map<func_decl, mq_pair> & full_macros, func_decl_set & cond_macros) {
                 for (quantifier * q : qs) {
                     quantifier_info * qi = get_qinfo(q);
-                    quantifier_info::macro_iterator it2  = qi->begin_macros();
+                    for (cond_macro * m : qi->macros()) {
-                    quantifier_info::macro_iterator end2 = qi->end_macros();
-                    for (; it2 != end2; ++it2) {
-                        cond_macro * m = *it2;
                         if (!m->is_hint()) {
                             func_decl * f = m->get_f();
-                            TRACE("non_auf_macro_solver", tout << "considering macro for: " << f->get_name() << "\n";
+                            TRACE("model_finder", tout << "considering macro for: " << f->get_name() << "\n";
                                   m->display(tout); tout << "\n";);
                             SASSERT(m_qi_params != 0);
                             if (m->is_unconditional() && (!qi->is_auf() || m->get_weight() >= m_qi_params->m_mbqi_force_template)) {

src/smt/smt_relevancy.cpp

@@ -527,7 +527,7 @@ namespace smt {
         }
 
 #ifdef Z3DEBUG
-        bool check_relevancy_app(app * n) const {
+        bool check_relevancy_app(app * n) const  {
             SASSERT(is_relevant(n));
             unsigned num_args = n->get_num_args();
             for (unsigned i = 0; i < num_args; i++) {
@@ -537,7 +537,7 @@ namespace smt {
             return true;
         }
         
-        virtual bool check_relevancy_or(app * n, bool root) const {
+        bool check_relevancy_or(app * n, bool root) const override {
             lbool val    = root ? l_true : m_context.find_assignment(n);
             if (val == l_false)
                 return check_relevancy_app(n);
@@ -600,7 +600,7 @@ namespace smt {
             return true;
         }
         
-        bool check_relevancy(expr_ref_vector const & v) const {
+        bool check_relevancy(expr_ref_vector const & v) const override {
             SASSERT(!can_propagate());
             ast_manager & m = get_manager();
             unsigned sz = v.size();

src/smt/smt_setup.cpp

@@ -507,7 +507,7 @@ namespace smt {
         m_params.m_nnf_cnf             = false;
         if (st.m_max_ite_tree_depth > 50) {
             m_params.m_arith_eq2ineq        = false;
-            m_params.m_pull_cheap_ite_trees = true;
+            m_params.m_pull_cheap_ite       = true;
             m_params.m_arith_propagate_eqs  = true;
             m_params.m_relevancy_lvl        = 2; 
             m_params.m_relevancy_lemma      = false;

src/smt/theory_arith_core.h

@@ -469,7 +469,8 @@ namespace smt {
         if (negated) l_conseq.neg();
 
         TRACE("arith_axiom", tout << mk_pp(ante, m) << "\n" << mk_pp(conseq, m) << "\n";
-              tout << s_ante << "\n" << s_conseq << "\n";);
+              tout << s_ante << "\n" << s_conseq << "\n";
+              tout << l_ante << "\n" << l_conseq << "\n";);
 
         // literal lits[2] = {l_ante, l_conseq};
         mk_clause(l_ante, l_conseq, 0, nullptr);
@@ -589,13 +590,13 @@ namespace smt {
     }
 
     //
-    // create the term: s := to_real(to_int(x)) - x
+    // create the term: s := x - to_real(to_int(x))
     // add the bounds 0 <= s < 1   
     //
     template<typename Ext>
     void theory_arith<Ext>::mk_to_int_axiom(app * n) {
         SASSERT(m_util.is_to_int(n));
-        ast_manager & m    = get_manager();
+        ast_manager & m  = get_manager();
         expr* x = n->get_arg(0);
 
         // to_int (to_real x) = x
@@ -603,11 +604,15 @@ namespace smt {
             mk_axiom(m.mk_false(), m.mk_eq(to_app(x)->get_arg(0), n));
             return;
         }
-        expr* to_r = m_util.mk_to_real(n);
+        expr_ref to_r(m_util.mk_to_real(n), m);
-        expr_ref lo(m_util.mk_le(to_r, x), m);
+        expr_ref diff(m_util.mk_add(x, m_util.mk_mul(m_util.mk_real(-1), to_r)), m);
-        expr_ref hi(m_util.mk_lt(x, m_util.mk_add(to_r, m_util.mk_numeral(rational(1), false))), m);
+        
-        mk_axiom(m.mk_false(), lo);
+        expr_ref lo(m_util.mk_ge(diff, m_util.mk_real(0)), m);
-        mk_axiom(m.mk_false(), hi);
+        expr_ref hi(m_util.mk_ge(diff, m_util.mk_real(1)), m);
+        hi = m.mk_not(hi);
+
+        mk_axiom(m.mk_false(), lo, false);
+        mk_axiom(m.mk_false(), hi, false);
     }
 
     template<typename Ext>
@@ -1202,7 +1207,7 @@ namespace smt {
 
     template<typename Ext>
     bool theory_arith<Ext>::internalize_atom(app * n, bool gate_ctx) {
-        TRACE("arith_internalize", tout << "internalising atom:\n" << mk_pp(n, this->get_manager()) << "\n";);
+        TRACE("arith_internalize", tout << "internalizing atom:\n" << mk_pp(n, this->get_manager()) << "\n";);
         context & ctx = get_context();
         SASSERT(m_util.is_le(n) || m_util.is_ge(n) || m_util.is_is_int(n));
         SASSERT(!ctx.b_internalized(n));

src/smt/theory_datatype.cpp

@@ -167,7 +167,7 @@ namespace smt {
         func_decl * upd  = n->get_decl();
         func_decl * acc  = to_func_decl(upd->get_parameter(0).get_ast());
         func_decl * con  = m_util.get_accessor_constructor(acc);
-        func_decl * rec  = m_util.get_constructor_recognizer(con);
+        func_decl * rec  = m_util.get_constructor_is(con);
         ptr_vector<func_decl> const & accessors = *m_util.get_constructor_accessors(con);
         app_ref rec_app(m.mk_app(rec, arg1), m);
         ctx.internalize(rec_app, false);
@@ -710,7 +710,7 @@ namespace smt {
             literal consequent;
             if (!r) {
                 ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(dt);
-                func_decl * rec = m_util.get_constructor_recognizer(constructors[unassigned_idx]);
+                func_decl * rec = m_util.get_constructor_is(constructors[unassigned_idx]);
                 app * rec_app   = get_manager().mk_app(rec, n->get_owner());
                 ctx.internalize(rec_app, false);
                 consequent = literal(ctx.get_bool_var(rec_app));
@@ -751,12 +751,12 @@ namespace smt {
         m_stats.m_splits++;
 
         if (d->m_recognizers.empty()) {
-            r = m_util.get_constructor_recognizer(non_rec_c);
+            r = m_util.get_constructor_is(non_rec_c);
         }
         else {
             enode * recognizer    = d->m_recognizers[non_rec_idx];
             if (recognizer == nullptr) {
-                r = m_util.get_constructor_recognizer(non_rec_c);
+                r = m_util.get_constructor_is(non_rec_c);
             }
             else if (!ctx.is_relevant(recognizer)) {
                 ctx.mark_as_relevant(recognizer);
@@ -776,7 +776,7 @@ namespace smt {
                     if (curr == nullptr) {
                         ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s);
                         // found empty slot...
-                        r = m_util.get_constructor_recognizer(constructors[idx]);
+                        r = m_util.get_constructor_is(constructors[idx]);
                         break;
                     }
                     else if (!ctx.is_relevant(curr)) { 

src/smt/theory_seq.cpp

@@ -2346,28 +2346,31 @@ bool theory_seq::check_int_string() {
     bool change = false;
     for (unsigned i = 0; i < m_int_string.size(); ++i) {
         expr* e = m_int_string[i].get(), *n;
-        if (m_util.str.is_itos(e) && add_itos_axiom(e)) {
+        if (m_util.str.is_itos(e) && add_itos_val_axiom(e)) {
             change = true;
         }
-        else if (m_util.str.is_stoi(e, n) && add_stoi_axiom(e)) {
+        else if (m_util.str.is_stoi(e, n) && add_stoi_val_axiom(e)) {
             change = true;
         }
     }
     return change;
 }
 
-bool theory_seq::add_stoi_axiom(expr* e) {
+void theory_seq::add_stoi_axiom(expr* e) {
+    TRACE("seq", tout << mk_pp(e, m) << "\n";);
+    SASSERT(m_util.str.is_stoi(e));
+    literal l = mk_simplified_literal(m_autil.mk_ge(e, arith_util(m).mk_int(-1)));
+    add_axiom(l);    
+}
+
+bool theory_seq::add_stoi_val_axiom(expr* e) {
     context& ctx = get_context();
     expr* n = nullptr;
     rational val;
     TRACE("seq", tout << mk_pp(e, m) << "\n";);
     VERIFY(m_util.str.is_stoi(e, n));    
     if (!get_num_value(e, val)) {
-        literal l = mk_simplified_literal(m_autil.mk_ge(e, arith_util(m).mk_int(-1)));
+        return false;
-        add_axiom(l);
-        TRACE("seq", tout << l << " " << ctx.get_assignment(l) << "\n";
-              ctx.display(tout););
-        return true;
     }
     if (!m_stoi_axioms.contains(val)) {
         m_stoi_axioms.insert(val);
@@ -2445,54 +2448,60 @@ expr_ref theory_seq::digit2int(expr* ch) {
     return expr_ref(mk_skolem(symbol("seq.digit2int"), ch, nullptr, nullptr, m_autil.mk_int()), m);
 }
 
-bool theory_seq::add_itos_axiom(expr* e) {
+void theory_seq::add_itos_axiom(expr* e) {
+    rational val;
+    expr* n = nullptr;
+    TRACE("seq", tout << mk_pp(e, m) << "\n";);
+    VERIFY(m_util.str.is_itos(e, n));
+
+    // itos(n) = "" <=> n < 0
+    app_ref e1(m_util.str.mk_empty(m.get_sort(e)), m);
+    expr_ref zero(arith_util(m).mk_int(0), m);
+    literal eq1 = mk_eq(e1, e, false);
+    literal ge0 = mk_literal(m_autil.mk_ge(n, zero));
+    // n >= 0 => itos(n) != ""
+    // itos(n) = "" or n >= 0
+    add_axiom(~eq1, ~ge0);
+    add_axiom(eq1, ge0);
+    
+    // n >= 0 => stoi(itos(n)) = n
+    app_ref stoi(m_util.str.mk_stoi(e), m);
+    add_axiom(~ge0, mk_eq(stoi, n, false));
+
+    // n >= 0 => itos(n) in (0-9)+
+    expr_ref num_re(m);
+    num_re = m_util.re.mk_range(m_util.str.mk_string(symbol("0")), m_util.str.mk_string(symbol("9")));
+    num_re = m_util.re.mk_plus(num_re);
+    app_ref in_re(m_util.re.mk_in_re(e, num_re), m);
+    add_axiom(~ge0, mk_literal(in_re));
+}
+
+bool theory_seq::add_itos_val_axiom(expr* e) {
     context& ctx = get_context();
     rational val;
     expr* n = nullptr;
     TRACE("seq", tout << mk_pp(e, m) << "\n";);
     VERIFY(m_util.str.is_itos(e, n));
-    if (get_num_value(n, val)) {
+    bool change = false;
-        if (!m_itos_axioms.contains(val)) {
-            m_itos_axioms.insert(val);
-            app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);            
-            expr_ref n1(arith_util(m).mk_numeral(val, true), m);
 
-            // itos(n) = "25" <=> n = 25
+    if (get_num_value(n, val) && !val.is_neg() && !m_itos_axioms.contains(val)) {
-            literal eq1 = mk_eq(n1, n , false);
+        m_itos_axioms.insert(val);
-            literal eq2 = mk_eq(e, e1, false);
+        app_ref e1(m_util.str.mk_string(symbol(val.to_string().c_str())), m);            
-            add_axiom(~eq1, eq2);
+        expr_ref n1(arith_util(m).mk_numeral(val, true), m);
-            add_axiom(~eq2, eq1);
+        
-            ctx.force_phase(eq1);
+        // itos(n) = "25" <=> n = 25
-            ctx.force_phase(eq2);
+        literal eq1 = mk_eq(n1, n , false);
-
+        literal eq2 = mk_eq(e, e1, false);
-            m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_itos_axioms, val));
+        add_axiom(~eq1, eq2);
-            m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
+        add_axiom(~eq2, eq1);
-            return true;
+        ctx.force_phase(eq1);
-        }
+        ctx.force_phase(eq2);
+        
+        m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_itos_axioms, val));
+        m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));        
+        change = true;        
     }
-    else {
+    return change;
-        // stoi(itos(n)) = n
-        app_ref e2(m_util.str.mk_stoi(e), m);
-        if (ctx.e_internalized(e2) && ctx.get_enode(e2)->get_root() == ctx.get_enode(n)->get_root()) {
-            return false;
-        }
-        add_axiom(mk_eq(e2, n, false));
-
-#if 1
-        expr_ref num_re(m), opt_re(m);
-        num_re = m_util.re.mk_range(m_util.str.mk_string(symbol("0")), m_util.str.mk_string(symbol("9")));
-        num_re = m_util.re.mk_plus(num_re);
-        opt_re = m_util.re.mk_opt(m_util.re.mk_to_re(m_util.str.mk_string(symbol("-"))));
-        num_re = m_util.re.mk_concat(opt_re, num_re);
-        app_ref in_re(m_util.re.mk_in_re(e, num_re), m);
-        internalize_term(in_re);
-        propagate_in_re(in_re, true);
-#endif
-        m_trail_stack.push(push_replay(alloc(replay_axiom, m, e)));
-        return true;
-    }
-
-    return false;
 }
 
 void theory_seq::apply_sort_cnstr(enode* n, sort* s) {
@@ -2721,13 +2730,12 @@ public:
         bool is_string = th.m_util.is_string(m_sort);
         expr_ref result(th.m);
         if (is_string) {
-            svector<unsigned> sbuffer;
+            unsigned_vector sbuffer;
             bv_util bv(th.m);
             rational val;
             unsigned sz;
-
+            for (source_t src : m_source) {
-            for (unsigned i = 0; i < m_source.size(); ++i) {
+                switch (src) {
-                switch (m_source[i]) {
                 case unit_source: {
                     VERIFY(bv.is_numeral(values[j++], val, sz));
                     sbuffer.push_back(val.get_unsigned());
@@ -2757,12 +2765,13 @@ public:
                     break;
                 }
                 }
+                // TRACE("seq", tout << src << " " << sbuffer << "\n";);
             }
             result = th.m_util.str.mk_string(zstring(sbuffer.size(), sbuffer.c_ptr()));
         }
         else {
-            for (unsigned i = 0; i < m_source.size(); ++i) {
+            for (source_t src : m_source) {
-                switch (m_source[i]) {
+                switch (src) {
                 case unit_source:
                     args.push_back(th.m_util.str.mk_unit(values[j++]));
                     break;
@@ -2804,8 +2813,8 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
         seq_value_proc* sv = alloc(seq_value_proc, *this, srt);
        
         TRACE("seq", tout << mk_pp(e, m) << "\n";);
-        for (unsigned i = 0; i < concats.size(); ++i) {
+        for (expr* c : concats) {
-            expr* c = concats[i], *c1;
+            expr *c1;
             TRACE("seq", tout << mk_pp(c, m) << "\n";);
             if (m_util.str.is_unit(c, c1)) {
                 if (ctx.e_internalized(c1)) {
@@ -3048,8 +3057,11 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
             enode* n2 = ctx.get_enode(e1);
             res = m_util.str.mk_string(symbol(val.to_string().c_str()));
 #if 1
+            if (val.is_neg()) {
+                result = e;
+            }
             // TBD remove this: using roots is unsound for propagation.
-            if (n1->get_root() == n2->get_root()) {
+            else if (n1->get_root() == n2->get_root()) {
                 result = res;
                 deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(n1, n2)));
             }
@@ -3147,6 +3159,9 @@ void theory_seq::deque_axiom(expr* n) {
     else if (m_util.str.is_itos(n)) {
         add_itos_axiom(n);
     }
+    else if (m_util.str.is_stoi(n)) {
+        add_stoi_axiom(n);
+    }
 }
 
 
@@ -3366,9 +3381,9 @@ void theory_seq::add_itos_length_axiom(expr* len) {
     rational len1, len2;
     rational ten(10);
     if (get_num_value(n, len1)) {
-        bool neg = len1.is_neg();
+        if (len1.is_neg()) {
-        if (neg) len1.neg();
+            return;
-        num_char1 = neg?2:1;
+        }
         // 0 <= x < 10
         // 10 <= x < 100
         // 100 <= x < 1000
@@ -3387,13 +3402,12 @@ void theory_seq::add_itos_length_axiom(expr* len) {
 
     literal len_le(mk_literal(m_autil.mk_le(len, m_autil.mk_int(num_char))));
     literal len_ge(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(num_char))));
+    literal n_ge_0(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
+    add_axiom(~n_ge_0, mk_literal(m_autil.mk_ge(len, m_autil.mk_int(1))));   
 
     if (num_char == 1) {
-        add_axiom(len_ge);
-        literal n_ge_0(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(0))));
         literal n_ge_10(mk_literal(m_autil.mk_ge(n, m_autil.mk_int(10))));
         add_axiom(~n_ge_0, n_ge_10, len_le);
-        add_axiom(~len_le, n_ge_0);
         add_axiom(~len_le, ~n_ge_10);
         return;
     }
@@ -3401,22 +3415,13 @@ void theory_seq::add_itos_length_axiom(expr* len) {
     for (unsigned i = 2; i < num_char; ++i) {
         hi *= ten;
     }
-    // n <= -hi or n >= hi*10  <=>  len >= num_chars
+    // n >= hi*10  <=>  len >= num_chars
-    // -10*hi < n < 100*hi    <=>  len <= num_chars
+    //  n < 100*hi    <=>  len <= num_chars
-    literal n_le_hi    = mk_literal(m_autil.mk_le(n, m_autil.mk_numeral(-hi, true)));
     literal n_ge_10hi  = mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(ten*hi, true)));
-    literal n_le_m10hi = mk_literal(m_autil.mk_le(n, m_autil.mk_numeral(-ten*hi, true)));
     literal n_ge_100hi = mk_literal(m_autil.mk_ge(n, m_autil.mk_numeral(ten*ten*hi, true)));
     
-    add_axiom(~n_le_hi,   len_ge);
     add_axiom(~n_ge_10hi, len_ge);
-    add_axiom(n_le_hi, n_ge_10hi, ~len_ge);
-
-    add_axiom(n_le_m10hi, n_ge_100hi, len_le);
-    add_axiom(~n_le_m10hi, ~len_le);
     add_axiom(~n_ge_100hi, ~len_le);
-
-    add_axiom(mk_literal(m_autil.mk_ge(len, m_autil.mk_int(1))));   
 }
 
 
@@ -3729,6 +3734,7 @@ bool theory_seq::is_extract_suffix(expr* s, expr* i, expr* l) {
 
 /*
   0 <= l <= len(s) => s = ey & l = len(e)
+  len(s) < l => s = e
  */
 void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
     TRACE("seq", tout << mk_pp(e, m) << " " << mk_pp(s, m) << " " << mk_pp(l, m) << "\n";);
@@ -3743,6 +3749,7 @@ void theory_seq::add_extract_prefix_axiom(expr* e, expr* s, expr* l) {
     add_axiom(~l_ge_0, ~l_le_s, mk_seq_eq(s, ey));
     add_axiom(~l_ge_0, ~l_le_s, mk_eq(l, le, false));
     add_axiom(~l_ge_0, ~l_le_s, mk_eq(ls_minus_l, m_util.str.mk_length(y), false));
+    add_axiom(l_le_s, mk_eq(e, s, false));
 }
 
 /*
@@ -4214,7 +4221,9 @@ void theory_seq::relevant_eh(app* n) {
         m_util.str.is_extract(n) ||
         m_util.str.is_at(n) ||
         m_util.str.is_empty(n) ||
-        m_util.str.is_string(n)) {
+        m_util.str.is_string(n) ||
+        m_util.str.is_itos(n) || 
+        m_util.str.is_stoi(n)) {
         enque_axiom(n);
     }
 

src/smt/theory_seq.h

@@ -507,8 +507,10 @@ namespace smt {
         void add_elim_string_axiom(expr* n);
         void add_at_axiom(expr* n);
         void add_in_re_axiom(expr* n);
-        bool add_stoi_axiom(expr* n);
+        void add_itos_axiom(expr* n);
-        bool add_itos_axiom(expr* n);
+        void add_stoi_axiom(expr* n);
+        bool add_stoi_val_axiom(expr* n);
+        bool add_itos_val_axiom(expr* n);
         literal is_digit(expr* ch);
         expr_ref digit2int(expr* ch);
         void add_itos_length_axiom(expr* n);

src/smt/theory_str.cpp

@@ -668,7 +668,6 @@ namespace smt {
     }
 
     app * theory_str::mk_indexof(expr * haystack, expr * needle) {
-        // TODO check meaning of the third argument here
         app * indexof = u.str.mk_index(haystack, needle, mk_int(0));
         m_trail.push_back(indexof);
         // immediately force internalization so that axiom setup does not fail
@@ -877,14 +876,7 @@ namespace smt {
                     instantiate_axiom_Contains(e);
                 } else if (u.str.is_index(a)) {
                     instantiate_axiom_Indexof(e);
-                    /* TODO NEXT: Indexof2/Lastindexof rewrite?
-                       } else if (is_Indexof2(e)) {
-                       instantiate_axiom_Indexof2(e);
-                       } else if (is_LastIndexof(e)) {
-                       instantiate_axiom_LastIndexof(e);
-                    */
                 } else if (u.str.is_extract(a)) {
-                    // TODO check semantics of substr vs. extract
                     instantiate_axiom_Substr(e);
                 } else if (u.str.is_replace(a)) {
                     instantiate_axiom_Replace(e);
@@ -1265,27 +1257,37 @@ namespace smt {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
-        app * expr = e->get_owner();
+        app * ex = e->get_owner();
-        if (axiomatized_terms.contains(expr)) {
+        if (axiomatized_terms.contains(ex)) {
-            TRACE("str", tout << "already set up Indexof axiom for " << mk_pp(expr, m) << std::endl;);
+            TRACE("str", tout << "already set up str.indexof axiom for " << mk_pp(ex, m) << std::endl;);
             return;
         }
-        axiomatized_terms.insert(expr);
+        SASSERT(ex->get_num_args() == 3);
+        // if the third argument is exactly the integer 0, we can use this "simple" indexof;
+        // otherwise, we call the "extended" version
+        expr * startingPosition = ex->get_arg(2);
+        rational startingInteger;
+        if (!m_autil.is_numeral(startingPosition, startingInteger) || !startingInteger.is_zero()) {
+            // "extended" indexof term with prefix
+            instantiate_axiom_Indexof_extended(e);
+            return;
+        }
+        axiomatized_terms.insert(ex);
 
-        TRACE("str", tout << "instantiate Indexof axiom for " << mk_pp(expr, m) << std::endl;);
+        TRACE("str", tout << "instantiate str.indexof axiom for " << mk_pp(ex, m) << std::endl;);
 
         expr_ref x1(mk_str_var("x1"), m);
         expr_ref x2(mk_str_var("x2"), m);
         expr_ref indexAst(mk_int_var("index"), m);
 
-        expr_ref condAst(mk_contains(expr->get_arg(0), expr->get_arg(1)), m);
+        expr_ref condAst(mk_contains(ex->get_arg(0), ex->get_arg(1)), m);
         SASSERT(condAst);
 
         // -----------------------
         // true branch
         expr_ref_vector thenItems(m);
         //  args[0] = x1 . args[1] . x2
-        thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x1, mk_concat(expr->get_arg(1), x2))));
+        thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x1, mk_concat(ex->get_arg(1), x2))));
         //  indexAst = |x1|
         thenItems.push_back(ctx.mk_eq_atom(indexAst, mk_strlen(x1)));
         //     args[0]  = x3 . x4
@@ -1293,11 +1295,11 @@ namespace smt {
         //  /\ ! contains(x3, args[1])
         expr_ref x3(mk_str_var("x3"), m);
         expr_ref x4(mk_str_var("x4"), m);
-        expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(expr->get_arg(1)), mk_int(-1)), m);
+        expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(ex->get_arg(1)), mk_int(-1)), m);
         SASSERT(tmpLen);
-        thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
+        thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x3, x4)));
         thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
-        thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1))));
+        thenItems.push_back(mk_not(m, mk_contains(x3, ex->get_arg(1))));
         expr_ref thenBranch(m.mk_and(thenItems.size(), thenItems.c_ptr()), m);
         SASSERT(thenBranch);
 
@@ -1309,26 +1311,42 @@ namespace smt {
         expr_ref breakdownAssert(m.mk_ite(condAst, thenBranch, elseBranch), m);
         SASSERT(breakdownAssert);
 
-        expr_ref reduceToIndex(ctx.mk_eq_atom(expr, indexAst), m);
+        expr_ref reduceToIndex(ctx.mk_eq_atom(ex, indexAst), m);
         SASSERT(reduceToIndex);
 
         expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToIndex), m);
         SASSERT(finalAxiom);
         assert_axiom(finalAxiom);
+
+        {
+            // heuristic: integrate with str.contains information
+            // (but don't introduce it if it isn't already in the instance)
+            expr_ref haystack(ex->get_arg(0), m), needle(ex->get_arg(1), m), startIdx(ex->get_arg(2), m);
+            expr_ref zeroAst(mk_int(0), m);
+            // (H contains N) <==> (H indexof N, i) >= 0
+            expr_ref premise(u.str.mk_contains(haystack, needle), m);
+            ctx.internalize(premise, false);
+            expr_ref conclusion(m_autil.mk_ge(ex, zeroAst), m);
+            expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
+            SASSERT(containsAxiom);
+            // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
+            m_delayed_axiom_setup_terms.push_back(containsAxiom);
+        }
     }
 
-    void theory_str::instantiate_axiom_Indexof2(enode * e) {
+    void theory_str::instantiate_axiom_Indexof_extended(enode * e) {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
         app * expr = e->get_owner();
         if (axiomatized_terms.contains(expr)) {
-            TRACE("str", tout << "already set up Indexof2 axiom for " << mk_pp(expr, m) << std::endl;);
+            TRACE("str", tout << "already set up extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;);
             return;
         }
+        SASSERT(expr->get_num_args() == 3);
         axiomatized_terms.insert(expr);
 
-        TRACE("str", tout << "instantiate Indexof2 axiom for " << mk_pp(expr, m) << std::endl;);
+        TRACE("str", tout << "instantiate extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;);
 
         // -------------------------------------------------------------------------------
         //   if (arg[2] >= length(arg[0]))                          // ite2
@@ -1360,7 +1378,7 @@ namespace smt {
         ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1))));
         ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen));
         ite2ElseItems.push_back(ite3);
-        expr_ref ite2Else(m.mk_and(ite2ElseItems.size(), ite2ElseItems.c_ptr()), m);
+        expr_ref ite2Else(mk_and(ite2ElseItems), m);
         SASSERT(ite2Else);
 
         expr_ref ite2(m.mk_ite(
@@ -1383,6 +1401,20 @@ namespace smt {
         expr_ref reduceTerm(ctx.mk_eq_atom(expr, resAst), m);
         SASSERT(reduceTerm);
         assert_axiom(reduceTerm);
+
+        {
+            // heuristic: integrate with str.contains information
+            // (but don't introduce it if it isn't already in the instance)
+            expr_ref haystack(expr->get_arg(0), m), needle(expr->get_arg(1), m), startIdx(expr->get_arg(2), m);
+            // (H contains N) <==> (H indexof N, i) >= 0
+            expr_ref premise(u.str.mk_contains(haystack, needle), m);
+            ctx.internalize(premise, false);
+            expr_ref conclusion(m_autil.mk_ge(expr, zeroAst), m);
+            expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
+            SASSERT(containsAxiom);
+            // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
+            m_delayed_axiom_setup_terms.push_back(containsAxiom);
+        }
     }
 
     void theory_str::instantiate_axiom_LastIndexof(enode * e) {
@@ -1854,8 +1886,11 @@ namespace smt {
             // trivially true for any string!
             assert_axiom(ex);
         } else if (u.re.is_full_char(regex)) {
-            TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;);
+            // any char = any string of length 1
-            NOT_IMPLEMENTED_YET(); 
+            expr_ref rhs(ctx.mk_eq_atom(mk_strlen(str), mk_int(1)), m);
+            expr_ref finalAxiom(m.mk_iff(ex, rhs), m);
+            SASSERT(finalAxiom);
+            assert_axiom(finalAxiom);
         } else {
             TRACE("str", tout << "ERROR: unknown regex expression " << mk_pp(regex, m) << "!" << std::endl;);
             NOT_IMPLEMENTED_YET();
@@ -5602,6 +5637,8 @@ namespace smt {
                 // merge arg0 and arg1
                 expr * arg0 = to_app(node)->get_arg(0);
                 expr * arg1 = to_app(node)->get_arg(1);
+				SASSERT(arg0 != node);
+				SASSERT(arg1 != node);
                 expr * arg0DeAlias = dealias_node(arg0, varAliasMap, concatAliasMap);
                 expr * arg1DeAlias = dealias_node(arg1, varAliasMap, concatAliasMap);
                 get_grounded_concats(arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
@@ -6369,6 +6406,13 @@ namespace smt {
                 make_transition(tmp, ch, tmp);
             }
             TRACE("str", tout << "re.all NFA: start = " << start << ", end = " << end << std::endl;);
+        } else if (u.re.is_full_char(e)) {
+            // effectively . (match any one character)
+            for (unsigned int i = 0; i < 256; ++i) {
+                char ch = (char)i;
+                make_transition(start, ch, end);
+            }
+            TRACE("str", tout << "re.allchar NFA: start = " << start << ", end = " << end << std::endl;);
         } else {
             TRACE("str", tout << "invalid regular expression" << std::endl;);
             m_valid = false;
@@ -9678,8 +9722,8 @@ namespace smt {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
-        expr_ref_vector assignments(m);
+        //expr_ref_vector assignments(m);
-        ctx.get_assignments(assignments);
+        //ctx.get_assignments(assignments);
 
         if (opt_VerifyFinalCheckProgress) {
             finalCheckProgressIndicator = false;

src/smt/theory_str.h

@@ -538,7 +538,7 @@ protected:
     void instantiate_axiom_suffixof(enode * e);
     void instantiate_axiom_Contains(enode * e);
     void instantiate_axiom_Indexof(enode * e);
-    void instantiate_axiom_Indexof2(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);

src/solver/combined_solver.cpp

@@ -18,10 +18,11 @@ Author:
 Notes:
 
 --*/
-#include "solver/solver.h"
 #include "util/scoped_timer.h"
-#include "solver/combined_solver_params.hpp"
 #include "util/common_msgs.h"
+#include "ast/ast_pp.h"
+#include "solver/solver.h"
+#include "solver/combined_solver_params.hpp"
 #define PS_VB_LVL 15
 
 /**

src/tactic/aig/aig.cpp

@@ -267,7 +267,7 @@ struct aig_manager::imp {
             }
             if  (b == r) {
                 if (sign1) {
-                    // subsitution
+                    // substitution
                     // not (a and b) and r --> (not a) and r   IF b == r
                     l = a;
                     l.invert();

src/tactic/arith/nla2bv_tactic.cpp

@@ -459,7 +459,7 @@ public:
         SASSERT(g->is_well_sorted());
     }
     
-    void cleanup(void) override {
+    void cleanup() override {
     }
 };
 

src/tactic/core/ctx_simplify_tactic.cpp

@@ -582,7 +582,7 @@ struct ctx_simplify_tactic::imp {
             for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
                 expr * t = g.form(i);
                 process(t, r);
-                proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(t, r, 0, nullptr)); // TODO :-)
+                proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(t, r));
                 g.update(i, r, new_pr, g.dep(i));
             }
         }

src/tactic/core/dom_simplify_tactic.cpp

@@ -382,7 +382,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
             change |= r != g.form(i);
             proof* new_pr = nullptr;
             if (g.proofs_enabled()) {
-                new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr));
+                new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
             }
             g.update(i, r, new_pr, g.dep(i));
         }
@@ -402,7 +402,7 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
             CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
             proof* new_pr = nullptr;
             if (g.proofs_enabled()) {
-                new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, nullptr));
+                new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
             }
             g.update(i, r, new_pr, g.dep(i));
         }

src/tactic/sls/bvsls_opt_engine.h

@@ -65,7 +65,7 @@ protected:
                        unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move,
                        mpz const & max_score, expr * objective);
 
-    mpz top_score(void) {
+    mpz top_score() {
         mpz res(0);
         obj_hashtable<expr> const & top_exprs = m_obj_tracker.get_top_exprs();
         for (obj_hashtable<expr>::iterator it = top_exprs.begin();

src/tactic/sls/sls_engine.h

@@ -99,7 +99,7 @@ public:
 
     // stats const & get_stats(void) { return m_stats; }
     void collect_statistics(statistics & st) const;
-    void reset_statistics(void) { m_stats.reset(); }    
+    void reset_statistics() { m_stats.reset(); }
 
     bool full_eval(model & mdl);
 
@@ -109,7 +109,7 @@ public:
     void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted);
     void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped);            
 
-    lbool search(void);    
+    lbool search();
 
     lbool operator()();
     void operator()(goal_ref const & g, model_converter_ref & mc);

src/tactic/tactic_exception.h

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Tactic expection object.
+    Tactic exception object.
 
 Author:
 

src/tactic/tactical.cpp

@@ -907,7 +907,7 @@ public:
         m_t->operator()(in, result, mc, pc, core);
     }
    
-    void cleanup(void) override { m_t->cleanup(); }
+    void cleanup() override { m_t->cleanup(); }
     void collect_statistics(statistics & st) const override { m_t->collect_statistics(st); }
     void reset_statistics() override { m_t->reset_statistics(); }
     void updt_params(params_ref const & p) override { m_t->updt_params(p); }

src/tactic/tactical.h

@@ -47,7 +47,7 @@ tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5
 
 tactic * repeat(tactic * t, unsigned max = UINT_MAX); 
 /**
-   \brief Fails if \c t produeces more than \c threshold subgoals.
+   \brief Fails if \c t produces more than \c threshold subgoals.
    Otherwise, it behaves like \c t.
 */
 tactic * fail_if_branching(tactic * t, unsigned threshold = 1);

src/tactic/ufbv/ufbv_rewriter.cpp

@@ -196,14 +196,14 @@ int ufbv_rewriter::is_smaller(expr * e1, expr * e2) const {
 class max_var_id_proc {
     unsigned    m_max_var_id;
 public:
-    max_var_id_proc(void):m_max_var_id(0) {}
+    max_var_id_proc():m_max_var_id(0) {}
     void operator()(var * n) {
         if(n->get_idx() > m_max_var_id)
             m_max_var_id = n->get_idx();
     }
     void operator()(quantifier * n) {}
     void operator()(app * n) {}
-    unsigned get_max(void) { return m_max_var_id; }
+    unsigned get_max() { return m_max_var_id; }
 };
 
 unsigned ufbv_rewriter::max_var_id(expr * e)
@@ -253,7 +253,7 @@ void ufbv_rewriter::remove_fwd_idx(func_decl * f, quantifier * demodulator) {
     }
 }
 
-bool ufbv_rewriter::check_fwd_idx_consistency(void) {
+bool ufbv_rewriter::check_fwd_idx_consistency() {
     for (fwd_idx_map::iterator it = m_fwd_idx.begin(); it != m_fwd_idx.end() ; it++ ) {
         quantifier_set * set = it->m_value;
         SASSERT(set);

src/tactic/ufbv/ufbv_rewriter.h

@@ -173,7 +173,7 @@ class ufbv_rewriter {
     
     void insert_fwd_idx(expr * large, expr * small, quantifier * demodulator);
     void remove_fwd_idx(func_decl * f, quantifier * demodulator);
-    bool check_fwd_idx_consistency(void);
+    bool check_fwd_idx_consistency();
     void show_fwd_idx(std::ostream & out);
     bool is_demodulator(expr * e, expr_ref & large, expr_ref & small) const;
     bool can_rewrite(expr * n, expr * lhs);

src/test/heap.cpp

@@ -19,20 +19,22 @@ Revision History:
 #include<iostream>
 #include "util/util.h"
 #include "util/heap.h"
-#include "util/hashtable.h"
 #include "util/trace.h"
+#include "util/uint_set.h"
+// include "util/hashtable.h"
 
 struct lt_proc { bool operator()(int v1, int v2) const { return v1 < v2; } };
+//struct int_hash_proc { unsigned operator()(int v) const { std::cout << "hash " << v << "\n"; VERIFY(v >= 0); return v; }};  
+//typedef int_hashtable<int_hash_proc, default_eq<int> > int_set; 
 typedef heap<lt_proc> int_heap;
-struct int_hash_proc { unsigned operator()(int v) const { return v * 17; }};
-typedef int_hashtable<int_hash_proc, default_eq<int> > int_set;
 #define N 10000
 
 static random_gen heap_rand(1);
 
 static void tst1() {
     int_heap h(N);
-    int_set  t;
+//    int_set t;
+    uint_set  t;
     for (int i = 0; i < N * 3; i++) {
         int val = heap_rand() % N;
         if (!h.contains(val)) {
@@ -41,14 +43,15 @@ static void tst1() {
             t.insert(val);
         }
         else {
+            if (!t.contains(val)) {
+                for (int v : t) std::cout << v << "\n";
+            }
             ENSURE(t.contains(val));
         }
     }
     ENSURE(h.check_invariant());
-    int_set::iterator it  = t.begin();
+    for (int v : t) {
-    int_set::iterator end = t.end();
+        ENSURE(h.contains(v));
-    for (; it != end; ++it) {
-        ENSURE(h.contains(*it));
     }
     while (!h.empty()) {
         int m1 = h.min_value();
@@ -84,6 +87,8 @@ static void dump_heap(const int_heap2 & h, std::ostream & out) {
 static void tst2() {
     int_heap2 h(N);
     for (int i = 0; i < N * 10; i++) {
+
+        if (i % 1 == 0) std::cout << "i: " << i << std::endl;
         if (i % 1000 == 0) std::cout << "i: " << i << std::endl;
         int cmd = heap_rand() % 10;
         if (cmd <= 3) {
@@ -134,6 +139,7 @@ void tst_heap() {
     enable_trace("heap");
     unsigned i = 0;
     while (i < 3) {
+        IF_VERBOSE(1, verbose_stream() << "test\n";);
         heap_rand.set_seed(i++);
         tst1();
         init_values();

src/test/quant_elim.cpp

@@ -13,6 +13,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/reg_decl_plugins.h"
 
 
+#if 0
 static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char const* option) {
 
     //    enable_trace("bit2int");
@@ -48,6 +49,7 @@ static void test_qe(ast_manager& m, lbool expected_outcome, expr* fml, char cons
         //exit(-1);
     }
 }
+#endif
 
 static void test_formula(lbool expected_outcome, char const* fml) {
     ast_manager m;

src/util/hashtable.h

@@ -449,7 +449,7 @@ public:
             INSERT_LOOP_CORE_BODY();
         }
         UNREACHABLE();
-        return 0;
+        return false;
     }
 
     bool insert_if_not_there_core(const data & e, entry * & et) {

src/util/lp/dense_matrix.h

@@ -79,13 +79,14 @@ public:
 
     void apply_from_left_to_X(vector<X> & w, lp_settings & );
 
-    virtual void set_number_of_rows(unsigned /*m*/) {}
+    void set_number_of_rows(unsigned /*m*/) override {}
-    virtual void set_number_of_columns(unsigned /*n*/) { }
+    void set_number_of_columns(unsigned /*n*/) override {}
+#ifdef Z3DEBUG
+    T get_elem(unsigned i, unsigned j) const override { return m_values[i * m_n + j]; }
+#endif
 
-    T get_elem(unsigned i, unsigned j) const { return m_values[i * m_n + j]; }
+    unsigned row_count() const override { return m_m; }
-
+    unsigned column_count() const override { return m_n; }
-    unsigned row_count() const { return m_m; }
-    unsigned column_count() const { return m_n; }
 
     void set_elem(unsigned i, unsigned j, const T& val) {  m_values[i * m_n + j] = val;  }