Merge branch 'Z3Prover:master' into param-tuning

.clang-format

@@ -9,6 +9,7 @@ IndentWidth: 4
 TabWidth: 4
 UseTab: Never
 
+
 # Column width
 ColumnLimit: 120
 
@@ -34,6 +35,8 @@ BraceWrapping:
    AfterControlStatement: false
    AfterNamespace: false
    AfterStruct: false
+   BeforeElse : true
+   AfterCaseLabel: false
 # Spacing
 SpaceAfterCStyleCast: false
 SpaceAfterLogicalNot: false
@@ -42,7 +45,6 @@ SpaceInEmptyParentheses: false
 SpacesInCStyleCastParentheses: false
 SpacesInParentheses: false
 SpacesInSquareBrackets: false
-IndentCaseLabels: false
 
 # Alignment
 AlignConsecutiveAssignments: false
@@ -56,6 +58,7 @@ BinPackArguments: true
 BinPackParameters: true
 BreakBeforeBinaryOperators: None
 BreakBeforeTernaryOperators: true
+# BreakBeforeElse: true
 
 # Includes
 SortIncludes: false  # Z3 has specific include ordering conventions
@@ -63,6 +66,11 @@ SortIncludes: false  # Z3 has specific include ordering conventions
 # Namespaces
 NamespaceIndentation: All
 
+# Switch statements
+IndentCaseLabels: false
+AllowShortCaseLabelsOnASingleLine: true
+IndentCaseBlocks: false
+
 # Comments and documentation
 ReflowComments: true
 SpacesBeforeTrailingComments: 2

.github/workflows/codeql-analysis.yml

@@ -0,0 +1,37 @@
+name: "CodeQL"
+
+on:
+  workflow_dispatch:
+
+
+jobs:
+  analyze:
+    name: Analyze
+    runs-on: ubuntu-latest
+    permissions:
+      actions: read
+      contents: read
+      security-events: write
+
+    strategy:
+      fail-fast: false
+      matrix:
+        language: [cpp]
+
+    steps:
+    - name: Checkout repository
+      uses: actions/checkout@v5
+
+    - name: Initialize CodeQL
+      uses: github/codeql-action/init@v4
+      with:
+        languages: ${{ matrix.language }}
+
+    - name: Autobuild
+      uses: github/codeql-action/autobuild@v4
+
+    - name: Run CodeQL Query
+      uses: github/codeql-action/analyze@v4
+      with:
+        category: 'custom'
+        queries: ./codeql/custom-queries

codeql/custom_queries/FindUnderspecified.ql

@@ -0,0 +1,87 @@
+ /**
+
+  * Finds function calls with arguments that have unspecified evaluation order.
+
+  *
+
+  * @name Unspecified argument evaluation order
+
+  * @kind problem
+
+  * @problem.severity warning
+
+  * @id cpp/z3/unspecevalorder
+
+  */
+
+
+
+  import cpp
+
+
+
+  predicate isPureFunc(Function f) {
+
+    f.getName() = "m" or
+
+    not exists(Assignment a | a.getEnclosingFunction() = f) and
+
+    forall(FunctionCall g | g.getEnclosingFunction() = f | isPureFunc(g.getTarget()))
+
+  }
+
+
+
+  predicate sideEffectfulArgument(Expr a) {
+
+    exists(Function f | f = a.(FunctionCall).getTarget() |
+
+      not f instanceof ConstMemberFunction and
+
+      not isPureFunc(f)
+
+    )
+
+    or
+
+    exists(ArrayExpr b | b = a.(ArrayExpr) |
+
+      sideEffectfulArgument(b.getArrayBase()) or sideEffectfulArgument(b.getArrayOffset())
+
+    )
+
+    or
+
+    exists(Assignment b | b = a)
+
+    or
+
+    exists(BinaryOperation b | b = a | sideEffectfulArgument(b.getAnOperand()))
+
+    or
+
+    exists(UnaryOperation b | b = a | sideEffectfulArgument(b.getOperand()))
+
+  }
+
+
+
+  from FunctionCall f, Expr a, int i, Expr b, int j where
+
+    i < j and
+
+    f.getTarget().getName() != "operator&&" and
+
+    f.getTarget().getName() != "operator||" and
+
+    a = f.getArgument(i) and
+
+    b = f.getArgument(j) and
+
+    sideEffectfulArgument(a) and
+
+    sideEffectfulArgument(b)
+
+  select f, "potentially unspecified evaluation order of function arguments: $@ and $@", a,
+
+    i.toString(), b, j.toString()

examples/c++/example.cpp

@@ -1006,6 +1006,95 @@ void datatype_example() {
 
 }
 
+void polymorphic_datatype_example() {
+    std::cout << "polymorphic datatype example\n";
+    context ctx;
+
+    // Create type variables alpha and beta for polymorphic datatype using C API
+    Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha");
+    Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta");
+    sort alpha(ctx, Z3_mk_type_variable(ctx, alpha_sym));
+    sort beta(ctx, Z3_mk_type_variable(ctx, beta_sym));
+    
+    std::cout << "Type variables: " << alpha << ", " << beta << "\n";
+
+    // Define parametric Pair datatype with constructor mk-pair(first: alpha, second: beta)
+    symbol pair_name = ctx.str_symbol("Pair");
+    symbol mk_pair_name = ctx.str_symbol("mk-pair");
+    symbol is_pair_name = ctx.str_symbol("is-pair");
+    symbol first_name = ctx.str_symbol("first");
+    symbol second_name = ctx.str_symbol("second");
+    
+    symbol field_names[2] = {first_name, second_name};
+    sort field_sorts[2] = {alpha, beta};  // Use type variables
+    
+    constructors cs(ctx);
+    cs.add(mk_pair_name, is_pair_name, 2, field_names, field_sorts);
+    sort pair = ctx.datatype(pair_name, cs);
+    
+    std::cout << "Created parametric datatype: " << pair << "\n";
+    
+    // Instantiate Pair with concrete types: (Pair Int Real)
+    sort_vector params_int_real(ctx);
+    params_int_real.push_back(ctx.int_sort());
+    params_int_real.push_back(ctx.real_sort());
+    sort pair_int_real = ctx.datatype_sort(pair_name, params_int_real);
+    
+    std::cout << "Instantiated with Int and Real: " << pair_int_real << "\n";
+    
+    // Instantiate Pair with concrete types: (Pair Real Int)
+    sort_vector params_real_int(ctx);
+    params_real_int.push_back(ctx.real_sort());
+    params_real_int.push_back(ctx.int_sort());
+    sort pair_real_int = ctx.datatype_sort(pair_name, params_real_int);
+    
+    std::cout << "Instantiated with Real and Int: " << pair_real_int << "\n";
+    
+    // Get constructors and accessors for (Pair Int Real) using C API
+    func_decl mk_pair_ir(ctx, Z3_get_datatype_sort_constructor(ctx, pair_int_real, 0));
+    func_decl first_ir(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 0));
+    func_decl second_ir(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_int_real, 0, 1));
+    
+    std::cout << "Constructors and accessors for (Pair Int Real):\n";
+    std::cout << "  Constructor: " << mk_pair_ir << "\n";
+    std::cout << "  first accessor: " << first_ir << "\n";
+    std::cout << "  second accessor: " << second_ir << "\n";
+    
+    // Get constructors and accessors for (Pair Real Int) using C API
+    func_decl mk_pair_ri(ctx, Z3_get_datatype_sort_constructor(ctx, pair_real_int, 0));
+    func_decl first_ri(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 0));
+    func_decl second_ri(ctx, Z3_get_datatype_sort_constructor_accessor(ctx, pair_real_int, 0, 1));
+    
+    std::cout << "Constructors and accessors for (Pair Real Int):\n";
+    std::cout << "  Constructor: " << mk_pair_ri << "\n";
+    std::cout << "  first accessor: " << first_ri << "\n";
+    std::cout << "  second accessor: " << second_ri << "\n";
+    
+    // Create constants of these types
+    expr p1 = ctx.constant("p1", pair_int_real);
+    expr p2 = ctx.constant("p2", pair_real_int);
+    
+    std::cout << "Created constants: " << p1 << " : " << p1.get_sort() << "\n";
+    std::cout << "                   " << p2 << " : " << p2.get_sort() << "\n";
+    
+    // Create expressions using accessors
+    expr first_p1 = first_ir(p1);   // first(p1) has type Int
+    expr second_p2 = second_ri(p2); // second(p2) has type Int
+    
+    std::cout << "first(p1) = " << first_p1 << " : " << first_p1.get_sort() << "\n";
+    std::cout << "second(p2) = " << second_p2 << " : " << second_p2.get_sort() << "\n";
+    
+    // Create equality term: (= (first p1) (second p2))
+    expr eq = first_p1 == second_p2;
+    std::cout << "Equality term: " << eq << "\n";
+    
+    // Verify both sides have the same type (Int)
+    assert(first_p1.get_sort().id() == ctx.int_sort().id());
+    assert(second_p2.get_sort().id() == ctx.int_sort().id());
+    
+    std::cout << "Successfully created and verified polymorphic datatypes!\n";
+}
+
 void expr_vector_example() {
     std::cout << "expr_vector example\n";
     context c;
@@ -1394,6 +1483,7 @@ int main() {
         enum_sort_example(); std::cout << "\n";
         tuple_example(); std::cout << "\n";
         datatype_example(); std::cout << "\n";
+        polymorphic_datatype_example(); std::cout << "\n";
         expr_vector_example(); std::cout << "\n";
         exists_expr_vector_example(); std::cout << "\n";
         substitute_example(); std::cout << "\n";

src/api/api_datatype.cpp

@@ -306,12 +306,24 @@ extern "C" {
         Z3_CATCH;
     }
 
-    static datatype_decl* mk_datatype_decl(Z3_context c,
+    static datatype_decl* api_datatype_decl(Z3_context c,
                                             Z3_symbol name,
+                                            unsigned num_parameters,
+                                            Z3_sort const parameters[],
                                             unsigned num_constructors,
                                             Z3_constructor constructors[]) {
         datatype_util& dt_util = mk_c(c)->dtutil();
         ast_manager& m = mk_c(c)->m();
+        
+        sort_ref_vector params(m);
+        
+        // A correct use of the API is to always provide parameters explicitly.
+        // implicit parameters through polymorphic type variables does not work
+        // because the order of polymorphic variables in the parameters is ambiguous.
+        if (num_parameters > 0 && parameters) 
+            for (unsigned i = 0; i < num_parameters; ++i) 
+                params.push_back(to_sort(parameters[i]));
+        
         ptr_vector<constructor_decl> constrs;
         for (unsigned i = 0; i < num_constructors; ++i) {
             constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
@@ -326,7 +338,7 @@ extern "C" {
             }
             constrs.push_back(mk_constructor_decl(cn->m_name, cn->m_tester, acc.size(), acc.data()));
         }
-        return mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, num_constructors, constrs.data());
+        return mk_datatype_decl(dt_util, to_symbol(name), params.size(), params.data(), num_constructors, constrs.data());
     }
 
     Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
@@ -341,7 +353,7 @@ extern "C" {
 
         sort_ref_vector sorts(m);
         {
-            datatype_decl * data = mk_datatype_decl(c, name, num_constructors, constructors);
+            datatype_decl * data = api_datatype_decl(c, name, 0, nullptr, num_constructors, constructors);
             bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, nullptr, sorts);
             del_datatype_decl(data);
 
@@ -363,6 +375,42 @@ extern "C" {
         Z3_CATCH_RETURN(nullptr);
     }
 
+    Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c,
+                                              Z3_symbol name,
+                                              unsigned num_parameters,
+                                              Z3_sort parameters[],
+                                              unsigned num_constructors,
+                                              Z3_constructor constructors[]) {
+        Z3_TRY;
+        LOG_Z3_mk_polymorphic_datatype(c, name, num_parameters, parameters, num_constructors, constructors);
+        RESET_ERROR_CODE();
+        ast_manager& m = mk_c(c)->m();
+        datatype_util data_util(m);
+
+        sort_ref_vector sorts(m);
+        {
+            datatype_decl * data = api_datatype_decl(c, name, num_parameters, parameters, num_constructors, constructors);
+            bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, nullptr, sorts);
+            del_datatype_decl(data);
+
+            if (!is_ok) {
+                SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
+                RETURN_Z3(nullptr);
+            }
+        }
+        sort * s = sorts.get(0);
+
+        mk_c(c)->save_ast_trail(s);
+        ptr_vector<func_decl> const& cnstrs = *data_util.get_datatype_constructors(s);
+
+        for (unsigned i = 0; i < num_constructors; ++i) {
+            constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
+            cn->m_constructor = cnstrs[i];
+        }
+        RETURN_Z3_mk_polymorphic_datatype(of_sort(s));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
     typedef ptr_vector<constructor> constructor_list;
 
     Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c,
@@ -387,14 +435,18 @@ extern "C" {
         Z3_CATCH;
     }
 
-    Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name) {
+    Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[]) {
         Z3_TRY;
-        LOG_Z3_mk_datatype_sort(c, name);
+        LOG_Z3_mk_datatype_sort(c, name, num_params, params);
         RESET_ERROR_CODE();
         ast_manager& m = mk_c(c)->m();
         datatype_util adt_util(m);
-        parameter p(to_symbol(name));
+        vector<parameter> ps;
-        sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, 1, &p);
+        ps.push_back(parameter(to_symbol(name)));
+        for (unsigned i = 0; i < num_params; ++i) {
+            ps.push_back(parameter(to_sort(params[i])));
+        }
+        sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, ps.size(), ps.data());
         mk_c(c)->save_ast_trail(s);
         RETURN_Z3(of_sort(s));
         Z3_CATCH_RETURN(nullptr);
@@ -416,7 +468,7 @@ extern "C" {
         ptr_vector<datatype_decl> datas;
         for (unsigned i = 0; i < num_sorts; ++i) {
             constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]);
-            datas.push_back(mk_datatype_decl(c, sort_names[i], cl->size(), reinterpret_cast<Z3_constructor*>(cl->data())));
+            datas.push_back(api_datatype_decl(c, sort_names[i], 0, nullptr, cl->size(), reinterpret_cast<Z3_constructor*>(cl->data())));
         }
         sort_ref_vector _sorts(m);
         bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.data(), 0, nullptr, _sorts);

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

@@ -343,6 +343,14 @@ namespace z3 {
         */
         sort datatype_sort(symbol const& name);
 
+        /**
+           \brief a reference to a recursively defined parametric datatype.
+           Expect that it gets defined as a \ref datatype.
+           \param name name of the datatype
+           \param params sort parameters
+        */
+        sort datatype_sort(symbol const& name, sort_vector const& params);
+
             
         /**
            \brief create an uninterpreted sort with the name given by the string or symbol.
@@ -2173,7 +2181,15 @@ namespace z3 {
     inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
     inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
     inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
+
     /**
+       \brief signed division operator for bitvectors.
+    */
+    inline expr sdiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsdiv(a.ctx(), a, b)); }
+    inline expr sdiv(expr const & a, int b) { return sdiv(a, a.ctx().num_val(b, a.get_sort())); }
+    inline expr sdiv(int a, expr const & b) { return sdiv(b.ctx().num_val(a, b.get_sort()), b); }
+
+/**
        \brief unsigned division operator for bitvectors.
     */
     inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
@@ -3617,7 +3633,14 @@ namespace z3 {
 
 
     inline sort context::datatype_sort(symbol const& name) {
-        Z3_sort s = Z3_mk_datatype_sort(*this, name);
+        Z3_sort s = Z3_mk_datatype_sort(*this, name, 0, nullptr);
+        check_error();
+        return sort(*this, s);            
+    }
+
+    inline sort context::datatype_sort(symbol const& name, sort_vector const& params) {
+        array<Z3_sort> _params(params);
+        Z3_sort s = Z3_mk_datatype_sort(*this, name, _params.size(), _params.ptr());
         check_error();
         return sort(*this, s);            
     }

src/api/dotnet/Context.cs

@@ -474,6 +474,36 @@ namespace Microsoft.Z3
             return new DatatypeSort(this, symbol, constructors);
         }
 
+        /// <summary>
+        /// Create a forward reference to a datatype sort.
+        /// This is useful for creating recursive datatypes or parametric datatypes.
+        /// </summary>
+        /// <param name="name">name of the datatype sort</param>
+        /// <param name="parameters">optional array of sort parameters for parametric datatypes</param>
+        public DatatypeSort MkDatatypeSortRef(Symbol name, Sort[] parameters = null)
+        {
+            Debug.Assert(name != null);
+            CheckContextMatch(name);
+            if (parameters != null)
+                CheckContextMatch<Sort>(parameters);
+            
+            var numParams = (parameters == null) ? 0 : (uint)parameters.Length;
+            var paramsNative = (parameters == null) ? null : AST.ArrayToNative(parameters);
+            return new DatatypeSort(this, Native.Z3_mk_datatype_sort(nCtx, name.NativeObject, numParams, paramsNative));
+        }
+
+        /// <summary>
+        /// Create a forward reference to a datatype sort.
+        /// This is useful for creating recursive datatypes or parametric datatypes.
+        /// </summary>
+        /// <param name="name">name of the datatype sort</param>
+        /// <param name="parameters">optional array of sort parameters for parametric datatypes</param>
+        public DatatypeSort MkDatatypeSortRef(string name, Sort[] parameters = null)
+        {
+            using var symbol = MkSymbol(name);
+            return MkDatatypeSortRef(symbol, parameters);
+        }
+
         /// <summary>
         /// Create mutually recursive datatypes.
         /// </summary>

src/api/java/AST.java

@@ -208,7 +208,13 @@ public class AST extends Z3Object implements Comparable<AST>
         case Z3_FUNC_DECL_AST:
             return new FuncDecl<>(ctx, obj);
         case Z3_QUANTIFIER_AST:
+            // a quantifier AST is a lambda iff it is neither a forall nor an exists. 
+            boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj);
+            if (isLambda) {
+               return new Lambda(ctx, obj);
+            } else {
                return new Quantifier(ctx, obj);
+            }
         case Z3_SORT_AST:
             return Sort.create(ctx, obj);
         case Z3_APP_AST:

src/api/java/Context.java

@@ -388,6 +388,54 @@ public class Context implements AutoCloseable {
         return new DatatypeSort<>(this, mkSymbol(name), constructors);
     }
 
+    /**
+     * Create a forward reference to a datatype sort.
+     * This is useful for creating recursive datatypes or parametric datatypes.
+     * @param name name of the datatype sort
+     * @param params optional array of sort parameters for parametric datatypes
+     **/
+    public <R> DatatypeSort<R> mkDatatypeSortRef(Symbol name, Sort[] params)
+    {
+        checkContextMatch(name);
+        if (params != null)
+            checkContextMatch(params);
+        
+        int numParams = (params == null) ? 0 : params.length;
+        long[] paramsNative = (params == null) ? new long[0] : AST.arrayToNative(params);
+        return new DatatypeSort<>(this, Native.mkDatatypeSort(nCtx(), name.getNativeObject(), numParams, paramsNative));
+    }
+
+    /**
+     * Create a forward reference to a datatype sort (non-parametric).
+     * This is useful for creating recursive datatypes.
+     * @param name name of the datatype sort
+     **/
+    public <R> DatatypeSort<R> mkDatatypeSortRef(Symbol name)
+    {
+        return mkDatatypeSortRef(name, null);
+    }
+
+    /**
+     * Create a forward reference to a datatype sort.
+     * This is useful for creating recursive datatypes or parametric datatypes.
+     * @param name name of the datatype sort
+     * @param params optional array of sort parameters for parametric datatypes
+     **/
+    public <R> DatatypeSort<R> mkDatatypeSortRef(String name, Sort[] params)
+    {
+        return mkDatatypeSortRef(mkSymbol(name), params);
+    }
+
+    /**
+     * Create a forward reference to a datatype sort (non-parametric).
+     * This is useful for creating recursive datatypes.
+     * @param name name of the datatype sort
+     **/
+    public <R> DatatypeSort<R> mkDatatypeSortRef(String name)
+    {
+        return mkDatatypeSortRef(name, null);
+    }
+
     /**
      * Create mutually recursive datatypes. 
      * @param names names of datatype sorts 

src/api/java/Expr.java

@@ -2148,8 +2148,15 @@ public class Expr<R extends Sort> extends AST
     static Expr<?> create(Context ctx, long obj)
     {
         Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
-        if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
+        if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) {
+			// a quantifier AST is a lambda iff it is neither a forall nor an exists. 
+            boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj);
+            if (isLambda) {
+               return new Lambda(ctx, obj);
+            } else {
                return new Quantifier(ctx, obj);
+            }
+		}
         long s = Native.getSort(ctx.nCtx(), obj);
         Z3_sort_kind sk = Z3_sort_kind
                 .fromInt(Native.getSortKind(ctx.nCtx(), s));

src/api/java/Lambda.java

@@ -126,7 +126,7 @@ public class Lambda<R extends Sort> extends ArrayExpr<Sort, R>
    }
 
 
-    private Lambda(Context ctx, long obj)
+    Lambda(Context ctx, long obj)
     {
         super(ctx, obj);
     }

src/api/ml/z3.ml

@@ -909,11 +909,17 @@ struct
     mk_sort ctx (Symbol.mk_string ctx name) constructors
 
   let mk_sort_ref (ctx: context) (name:Symbol.symbol) =
-    Z3native.mk_datatype_sort ctx name
+    Z3native.mk_datatype_sort ctx name 0 []
 
   let mk_sort_ref_s (ctx: context) (name: string) =
     mk_sort_ref ctx (Symbol.mk_string ctx name)
 
+  let mk_sort_ref_p (ctx: context) (name:Symbol.symbol) (params:Sort.sort list) =
+    Z3native.mk_datatype_sort ctx name (List.length params) params
+
+  let mk_sort_ref_ps (ctx: context) (name: string) (params:Sort.sort list) =
+    mk_sort_ref_p ctx (Symbol.mk_string ctx name) params
+
   let mk_sorts (ctx:context) (names:Symbol.symbol list) (c:Constructor.constructor list list) =
     let n = List.length names in
     let f e = ConstructorList.create ctx e in

src/api/ml/z3.mli

@@ -1087,6 +1087,12 @@ sig
   (* [mk_sort_ref_s ctx s] is [mk_sort_ref ctx (Symbol.mk_string ctx s)] *)
   val mk_sort_ref_s : context -> string -> Sort.sort
 
+  (** Create a forward reference to a parametric datatype sort. *)
+  val mk_sort_ref_p : context -> Symbol.symbol -> Sort.sort list -> Sort.sort
+
+  (** Create a forward reference to a parametric datatype sort. *)
+  val mk_sort_ref_ps : context -> string -> Sort.sort list -> Sort.sort
+
   (** Create a new datatype sort. *)
   val mk_sort : context -> Symbol.symbol -> Constructor.constructor list -> Sort.sort
 

src/api/python/z3/z3.py

@@ -5474,10 +5474,30 @@ class DatatypeRef(ExprRef):
         """Return the datatype sort of the datatype expression `self`."""
         return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
 
-def DatatypeSort(name, ctx = None):
+def DatatypeSort(name, params=None, ctx=None):
-    """Create a reference to a sort that was declared, or will be declared, as a recursive datatype"""
+    """Create a reference to a sort that was declared, or will be declared, as a recursive datatype.
+    
+    Args:
+        name: name of the datatype sort
+        params: optional list/tuple of sort parameters for parametric datatypes
+        ctx: Z3 context (optional)
+    
+    Example:
+        >>> # Non-parametric datatype
+        >>> TreeRef = DatatypeSort('Tree')
+        >>> # Parametric datatype with one parameter
+        >>> ListIntRef = DatatypeSort('List', [IntSort()])
+        >>> # Parametric datatype with multiple parameters
+        >>> PairRef = DatatypeSort('Pair', [IntSort(), BoolSort()])
+    """
     ctx = _get_ctx(ctx)
-    return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
+    if params is None or len(params) == 0:
+        return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx), 0, (Sort * 0)()), ctx)
+    else:
+        _params = (Sort * len(params))()
+        for i in range(len(params)):
+            _params[i] = params[i].ast
+        return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx), len(params), _params), ctx)
 
 def TupleSort(name, sorts, ctx=None):
     """Create a named tuple sort base on a set of underlying sorts

src/api/z3_api.h

@@ -2127,6 +2127,33 @@ extern "C" {
                                   unsigned num_constructors,
                                   Z3_constructor constructors[]);
 
+    /**
+       \brief Create a parametric datatype with explicit type parameters.
+       
+       This function is similar to #Z3_mk_datatype, except it takes an explicit set of type parameters.
+       The parameters can be type variables created with #Z3_mk_type_variable, allowing the definition
+       of polymorphic datatypes that can be instantiated with different concrete types.
+
+       \param c logical context
+       \param name name of the datatype
+       \param num_parameters number of type parameters (can be 0)
+       \param parameters array of type parameters (type variables or concrete sorts)
+       \param num_constructors number of constructors
+       \param constructors array of constructor specifications
+
+       \sa Z3_mk_datatype
+       \sa Z3_mk_type_variable
+       \sa Z3_mk_datatype_sort
+
+       def_API('Z3_mk_polymorphic_datatype', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(UINT), _inout_array(4, CONSTRUCTOR)))
+     */
+    Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c,
+                                              Z3_symbol name,
+                                              unsigned num_parameters,
+                                              Z3_sort parameters[],
+                                              unsigned num_constructors,
+                                              Z3_constructor constructors[]);
+
     /**
        \brief create a forward reference to a recursive datatype being declared.
        The forward reference can be used in a nested occurrence: the range of an array
@@ -2136,9 +2163,14 @@ extern "C" {
        Forward references can replace the use sort references, that are unsigned integers
        in the \c Z3_mk_constructor call
 
-       def_API('Z3_mk_datatype_sort', SORT, (_in(CONTEXT), _in(SYMBOL)))
+       \param c logical context
+       \param name name of the datatype
+       \param num_params number of sort parameters  
+       \param params array of sort parameters
+
+       def_API('Z3_mk_datatype_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT)))
      */
-    Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name);
+    Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[]);
 
     /**
        \brief Create list of constructors.

src/ast/datatype_decl_plugin.cpp

@@ -300,6 +300,12 @@ namespace datatype {
                         TRACE(datatype, tout << "expected sort parameter at position " << i << " got: " << s << "\n";);
                         throw invalid_datatype();
                     }
+                    // Allow type variables as parameters for polymorphic datatypes
+                    sort* param_sort = to_sort(s.get_ast());
+                    if (!m_manager->is_type_var(param_sort) && param_sort->get_family_id() == null_family_id) {
+                        // Type variables and concrete sorts are allowed, but not other uninterpreted sorts
+                        // Actually, all sorts should be allowed including uninterpreted ones
+                    }
                 }
                                 
                 sort* s = m_manager->mk_sort(name.get_symbol(),

src/ast/normal_forms/nnf.cpp

@@ -566,7 +566,8 @@ struct nnf::imp {
         expr * _then      = rs[2];
         expr * _else      = rs[3];
 
-        app * r = m.mk_and(m.mk_or(_not_cond, _then), m.mk_or(_cond, _else));
+        expr* a = m.mk_or(_not_cond, _then);
+        app * r = m.mk_and(a, m.mk_or(_cond, _else));
         m_result_stack.shrink(fr.m_spos);
         m_result_stack.push_back(r);
         if (proofs_enabled()) {
@@ -612,11 +613,13 @@ struct nnf::imp {
 
         app * r;
         if (is_eq(t) == fr.m_pol) {
-            auto a = m.mk_or(not_lhs, rhs);
+            expr* a = m.mk_or(not_lhs, rhs);
             r = m.mk_and(a, m.mk_or(lhs, not_rhs));
         }
-        else
+        else {
-            r = m.mk_and(m.mk_or(lhs, rhs), m.mk_or(not_lhs, not_rhs));
+            expr* a = m.mk_or(lhs, rhs);
+            r = m.mk_and(a, m.mk_or(not_lhs, not_rhs));
+        }
         m_result_stack.shrink(fr.m_spos);
         m_result_stack.push_back(r);
         if (proofs_enabled()) {
@@ -688,8 +691,8 @@ struct nnf::imp {
             if (proofs_enabled()) {
                 expr_ref aux(m);
                 aux = m.mk_label(true, names.size(), names.data(), arg);
-                pr = m.mk_transitivity(mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)),
+                auto a = mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux));
-                                         m.mk_iff_oeq(m.mk_rewrite(aux, r)));
+                pr = m.mk_transitivity(a, m.mk_iff_oeq(m.mk_rewrite(aux, r)));
             }
         }
         else {

src/ast/rewriter/arith_rewriter.cpp

@@ -720,24 +720,36 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
     }
     expr* c = nullptr, *t = nullptr, *e = nullptr;
     if (m.is_ite(arg1, c, t, e) && is_numeral(t, a1) && is_numeral(arg2, a2)) {
+        expr_ref a(m.mk_not(c), m);
         switch (kind) {
-        case LE: result = a1 <= a2 ? m.mk_or(c, m_util.mk_le(e, arg2)) : m.mk_and(m.mk_not(c), m_util.mk_le(e, arg2)); return BR_REWRITE2;
+        case LE: result = a1 <= a2 ? m.mk_or(c, m_util.mk_le(e, arg2)) : m.mk_and(a, m_util.mk_le(e, arg2)); return BR_REWRITE2;
-        case GE: result = a1 >= a2 ? m.mk_or(c, m_util.mk_ge(e, arg2)) : m.mk_and(m.mk_not(c), m_util.mk_ge(e, arg2)); return BR_REWRITE2;
+        case GE: result = a1 >= a2 ? m.mk_or(c, m_util.mk_ge(e, arg2)) : m.mk_and(a, m_util.mk_ge(e, arg2)); return BR_REWRITE2;
-        case EQ: result = a1 == a2 ? m.mk_or(c, m.mk_eq(e, arg2))    : m.mk_and(m.mk_not(c), m_util.mk_eq(e, arg2)); return BR_REWRITE2;
+        case EQ: result = a1 == a2 ? m.mk_or(c, m.mk_eq(e, arg2))    : m.mk_and(a, m_util.mk_eq(e, arg2)); return BR_REWRITE2;
         }
     }
     if (m.is_ite(arg1, c, t, e) && is_numeral(e, a1) && is_numeral(arg2, a2)) {
+        expr_ref a(m.mk_not(c), m);
         switch (kind) {
-        case LE: result = a1 <= a2 ? m.mk_or(m.mk_not(c), m_util.mk_le(t, arg2)) : m.mk_and(c, m_util.mk_le(t, arg2)); return BR_REWRITE2;
+        case LE: result = a1 <= a2 ? m.mk_or(a, m_util.mk_le(t, arg2)) : m.mk_and(c, m_util.mk_le(t, arg2)); return BR_REWRITE2;
-        case GE: result = a1 >= a2 ? m.mk_or(m.mk_not(c), m_util.mk_ge(t, arg2)) : m.mk_and(c, m_util.mk_ge(t, arg2)); return BR_REWRITE2;
+        case GE: result = a1 >= a2 ? m.mk_or(a, m_util.mk_ge(t, arg2)) : m.mk_and(c, m_util.mk_ge(t, arg2)); return BR_REWRITE2;
-        case EQ: result = a1 == a2 ? m.mk_or(m.mk_not(c), m.mk_eq(t, arg2))    : m.mk_and(c, m_util.mk_eq(t, arg2)); return BR_REWRITE2;
+        case EQ: result = a1 == a2 ? m.mk_or(a, m.mk_eq(t, arg2))    : m.mk_and(c, m_util.mk_eq(t, arg2)); return BR_REWRITE2;
         }
     }
     if (m.is_ite(arg1, c, t, e) && arg1->get_ref_count() == 1) {
         switch (kind) {
-        case LE: result = m.mk_ite(c, m_util.mk_le(t, arg2), m_util.mk_le(e, arg2)); return BR_REWRITE2;
+        case LE:
-        case GE: result = m.mk_ite(c, m_util.mk_ge(t, arg2), m_util.mk_ge(e, arg2)); return BR_REWRITE2;
+        {
-        case EQ: result = m.mk_ite(c, m.mk_eq(t, arg2), m.mk_eq(e, arg2)); return BR_REWRITE2;
+            auto a = m_util.mk_le(t, arg2);
+            result = m.mk_ite(c, a, m_util.mk_le(e, arg2)); return BR_REWRITE2;
+        }
+        case GE: {
+            auto a = m_util.mk_ge(t, arg2);
+            result = m.mk_ite(c, a, m_util.mk_ge(e, arg2)); return BR_REWRITE2;
+        }
+        case EQ:{
+            auto a = m.mk_eq(t, arg2);
+            result = m.mk_ite(c, a, m.mk_eq(e, arg2)); return BR_REWRITE2;
+        }
         }
     }
     if (m_util.is_to_int(arg2) && is_numeral(arg1)) {        

src/ast/rewriter/seq_rewriter.cpp

@@ -55,7 +55,8 @@ expr_ref sym_expr::accept(expr* e) {
             result = m.mk_bool_val((r1 <= r2) && (r2 <= r3));            
         }
         else {
-            result = m.mk_and(u.mk_le(m_t, e), u.mk_le(e, m_s));
+            auto a = u.mk_le(m_t, e);
+            result = m.mk_and(a, u.mk_le(e, m_s));
         }
         break;
     }
@@ -190,7 +191,9 @@ br_status seq_rewriter::mk_eq_helper(expr* a, expr* b, expr_ref& result) {
     // sa in (ra n rb) u (C(ra) n C(rb))
     if (is_not)
         rb = re().mk_complement(rb);
-    expr* r = re().mk_union(re().mk_inter(ra, rb), re().mk_inter(re().mk_complement(ra), re().mk_complement(rb)));
+    auto a_ = re().mk_inter(ra, rb);
+    auto b_ = re().mk_complement(ra);
+    expr* r = re().mk_union(a_, re().mk_inter(b_, re().mk_complement(rb)));
     result = re().mk_in_re(sa, r);
     return BR_REWRITE_FULL;
 }
@@ -620,10 +623,14 @@ expr_ref seq_rewriter::mk_seq_rest(expr* t) {
     expr_ref result(m());
     expr* s, * j, * k;
     rational jv;
-    if (str().is_extract(t, s, j, k) &&  m_autil.is_numeral(j, jv) && jv >= 0) 
+    if (str().is_extract(t, s, j, k) &&  m_autil.is_numeral(j, jv) && jv >= 0) {
-        result = str().mk_substr(s, m_autil.mk_int(jv + 1), mk_sub(k, 1));
+        auto a = m_autil.mk_int(jv + 1);
-    else 
+        result = str().mk_substr(s, a, mk_sub(k, 1));
-        result = str().mk_substr(t, one(), mk_sub(str().mk_length(t), 1));
+    }
+    else {
+        auto a = one();
+        result = str().mk_substr(t, a, mk_sub(str().mk_length(t), 1));
+    }
     return result;
 }
 
@@ -654,7 +661,10 @@ expr_ref seq_rewriter::mk_seq_last(expr* t) {
 *  No: if k > |s| then substring(s,0,k) = substring(s,0,k-1)
 */
 expr_ref seq_rewriter::mk_seq_butlast(expr* t) {
-    return expr_ref(str().mk_substr(t, zero(), m_autil.mk_sub(str().mk_length(t), one())), m());
+    auto b = zero();
+    auto c = str().mk_length(t);
+    auto a = str().mk_substr(t, b, m_autil.mk_sub(c, one()));
+    return expr_ref(a, m());
 }
 
 /*
@@ -1374,9 +1384,16 @@ br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
     }    
 
     expr* la = str().mk_length(a);
-    result = m().mk_ite(m().mk_and(m_autil.mk_ge(b, zero()), m().mk_not(m_autil.mk_le(la, b))), 
+    {
-                        str().mk_nth_i(a, b),
+        // deterministic evaluation order for guard components
-                        str().mk_nth_u(a, b));
+        auto ge0 = m_autil.mk_ge(b, zero());
+        auto le_la = m_autil.mk_le(la, b);
+        auto not_le = m().mk_not(le_la);
+        auto guard = m().mk_and(ge0, not_le);
+        auto t1 = str().mk_nth_i(a, b);
+        auto e1 = str().mk_nth_u(a, b);
+        result = m().mk_ite(guard, t1, e1);
+    }
     return BR_REWRITE_FULL;
 }
 
@@ -1547,17 +1564,20 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
     }
 
     if (str().is_empty(b)) {
-        result = m().mk_ite(m().mk_and(m_autil.mk_le(zero(), c),
+        // enforce deterministic evaluation order for bounds checks
-                                       m_autil.mk_le(c, str().mk_length(a))),
+        auto a1 = m_autil.mk_le(zero(), c);
-                            c,
+        auto b1 = m_autil.mk_le(c, str().mk_length(a));
-                            minus_one());
+        auto cond = m().mk_and(a1, b1);
+        result = m().mk_ite(cond, c, minus_one());
         return BR_REWRITE2;
     }
 
     
     if (str().is_empty(a)) {
         expr* emp = str().mk_is_empty(b);
-        result = m().mk_ite(m().mk_and(m().mk_eq(c, zero()), emp), zero(), minus_one());
+        auto a1 = m().mk_eq(c, zero());
+        auto cond = m().mk_and(a1, emp);
+        result = m().mk_ite(cond, zero(), minus_one());
         return BR_REWRITE2;
     }
 
@@ -1870,7 +1890,10 @@ br_status seq_rewriter::mk_seq_map(expr* f, expr* seqA, expr_ref& result) {
         return BR_REWRITE2;
     }
     if (str().is_concat(seqA, s1, s2)) {
-        result = str().mk_concat(str().mk_map(f, s1), str().mk_map(f, s2));
+        // introduce temporaries to ensure deterministic evaluation order of recursive map calls
+        auto m1 = str().mk_map(f, s1);
+        auto m2 = str().mk_map(f, s2);
+        result = str().mk_concat(m1, m2);
         return BR_REWRITE2;
     }
     return BR_FAILED;
@@ -1890,7 +1913,9 @@ br_status seq_rewriter::mk_seq_mapi(expr* f, expr* i, expr* seqA, expr_ref& resu
     }
     if (str().is_concat(seqA, s1, s2)) {
         expr_ref j(m_autil.mk_add(i, str().mk_length(s1)), m());
-        result = str().mk_concat(str().mk_mapi(f, i, s1), str().mk_mapi(f, j, s2));
+        auto left  = str().mk_mapi(f, i, s1);
+        auto right = str().mk_mapi(f, j, s2);
+        result = str().mk_concat(left, right);
         return BR_REWRITE2;
     }
     return BR_FAILED;
@@ -2046,8 +2071,8 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
                 SASSERT(bs.size() > 1);
                 s1 = s1.extract(s2.length(), s1.length() - s2.length());
                 as[0] = str().mk_string(s1);
-                result = str().mk_prefix(str().mk_concat(as.size(), as.data(), sort_a),
+                auto a = str().mk_concat(as.size(), as.data(), sort_a);
-                                              str().mk_concat(bs.size()-1, bs.data()+1, sort_a));
+                result = str().mk_prefix(a, str().mk_concat(bs.size()-1, bs.data()+1, sort_a));
                 TRACE(seq, tout << s1 << " " << s2 << " " << result << "\n";);
                 return BR_REWRITE_FULL;                
             }
@@ -2384,7 +2409,8 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
     }
     expr* b;
     if (str().is_itos(a, b)) {
-        result = m().mk_ite(m_autil.mk_ge(b, zero()), b, minus_one());
+        auto a = m_autil.mk_ge(b, zero());
+        result = m().mk_ite(a, b, minus_one());
         return BR_DONE;
     }
     if (str().is_ubv2s(a, b)) {
@@ -2395,7 +2421,8 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
     
     expr* c = nullptr, *t = nullptr, *e = nullptr;
     if (m().is_ite(a, c, t, e)) {
-        result = m().mk_ite(c, str().mk_stoi(t), str().mk_stoi(e));
+        auto a = str().mk_stoi(t);
+        result = m().mk_ite(c, a, str().mk_stoi(e));
         return BR_REWRITE_FULL;
     }
 
@@ -2703,7 +2730,10 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
     zstring zs;
     unsigned lo = 0, hi = 0;
     if (re().is_concat(r, r1, r2)) {
-        result = re().mk_concat(re().mk_reverse(r2), re().mk_reverse(r1));
+        // deterministic evaluation order for reverse operands
+        auto a_rev = re().mk_reverse(r2);
+        auto b_rev = re().mk_reverse(r1);
+        result = re().mk_concat(a_rev, b_rev);
         return BR_REWRITE2;
     }
     else if (re().is_star(r, r1)) {
@@ -2715,15 +2745,22 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
         return BR_REWRITE2;
     }
     else if (re().is_union(r, r1, r2)) {
-        result = re().mk_union(re().mk_reverse(r1), re().mk_reverse(r2));
+        // ensure deterministic evaluation order of parameters
+        auto a = re().mk_reverse(r1);
+        auto b = re().mk_reverse(r2);
+        result = re().mk_union(a, b);
         return BR_REWRITE2;
     }
     else if (re().is_intersection(r, r1, r2)) {
-        result = re().mk_inter(re().mk_reverse(r1), re().mk_reverse(r2));
+        auto a = re().mk_reverse(r1);
+        auto b = re().mk_reverse(r2);
+        result = re().mk_inter(a, b);
         return BR_REWRITE2;
     }
     else if (re().is_diff(r, r1, r2)) {
-        result = re().mk_diff(re().mk_reverse(r1), re().mk_reverse(r2));
+        auto a = re().mk_reverse(r1);
+        auto b = re().mk_reverse(r2);
+        result = re().mk_diff(a, b);
         return BR_REWRITE2;
     }
     else if (m().is_ite(r, p, r1, r2)) {
@@ -2767,8 +2804,9 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
         return BR_DONE;
     }
     else if (re().is_to_re(r, s) && str().is_concat(s, s1, s2)) {
-        result = re().mk_concat(re().mk_reverse(re().mk_to_re(s2)), 
+        auto a_rev = re().mk_reverse(re().mk_to_re(s2));
-                                re().mk_reverse(re().mk_to_re(s1)));
+        auto b_rev = re().mk_reverse(re().mk_to_re(s1));
+        result = re().mk_concat(a_rev, b_rev);
         return BR_REWRITE3;
     }
     else {
@@ -2957,7 +2995,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
         }
         else {
             // observe that the precondition |r1|>0 is is implied by c1 for use of mk_seq_first
-            m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(mk_seq_first(r1), e), c1);
+            {
+                auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort)));
+                auto eq_first = m().mk_eq(mk_seq_first(r1), e);
+                m_br.mk_and(is_non_empty, eq_first, c1);
+            }
             m_br.mk_and(path, c1, c2);
             if (m().is_false(c2))
                 result = nothing();
@@ -2970,7 +3012,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
         if (re().is_to_re(r2, r1)) {
             // here r1 is a sequence
             // observe that the precondition |r1|>0 of mk_seq_last is implied by c1
-            m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(mk_seq_last(r1), e), c1);
+            {
+                auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort)));
+                auto eq_last = m().mk_eq(mk_seq_last(r1), e);
+                m_br.mk_and(is_non_empty, eq_last, c1);
+            }
             m_br.mk_and(path, c1, c2);
             if (m().is_false(c2))
                 result = nothing();
@@ -3002,8 +3048,15 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
             result = mk_antimirov_deriv_union(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing()));
     }
     else if (m().is_ite(r, c, r1, r2)) {
-        c1 = simplify_path(e, m().mk_and(c, path));
+        {
-        c2 = simplify_path(e, m().mk_and(m().mk_not(c), path));
+            auto cp = m().mk_and(c, path);
+            c1 = simplify_path(e, cp);
+        }
+        {
+            auto notc = m().mk_not(c);
+            auto np = m().mk_and(notc, path);
+            c2 = simplify_path(e, np);
+        }
         if (m().is_false(c1))
             result = mk_antimirov_deriv(e, r2, c2);
         else if (m().is_false(c2))
@@ -3018,7 +3071,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
             // SASSERT(u().is_char(c1));
             // SASSERT(u().is_char(c2));
             // case: c1 <= e <= c2
-            range = simplify_path(e, m().mk_and(u().mk_le(c1, e), u().mk_le(e, c2)));
+            // deterministic evaluation for range bounds
+            auto a_le = u().mk_le(c1, e);
+            auto b_le = u().mk_le(e, c2);
+            auto rng_cond = m().mk_and(a_le, b_le);
+            range = simplify_path(e, rng_cond);
             psi = simplify_path(e, m().mk_and(path, range));
         }
         else if (!str().is_string(r1) && str().is_unit_string(r2, c2)) {
@@ -3399,12 +3456,22 @@ expr_ref seq_rewriter::mk_regex_reverse(expr* r) {
         result = mk_regex_concat(mk_regex_reverse(r2), mk_regex_reverse(r1));
     else if (m().is_ite(r, c, r1, r2))
         result = m().mk_ite(c, mk_regex_reverse(r1), mk_regex_reverse(r2));
-    else if (re().is_union(r, r1, r2))
+    else if (re().is_union(r, r1, r2)) {
-        result = re().mk_union(mk_regex_reverse(r1), mk_regex_reverse(r2));
+        // enforce deterministic evaluation order
-    else if (re().is_intersection(r, r1, r2))
+        auto a1 = mk_regex_reverse(r1);
-        result = re().mk_inter(mk_regex_reverse(r1), mk_regex_reverse(r2));
+        auto b1 = mk_regex_reverse(r2);
-    else if (re().is_diff(r, r1, r2))
+        result = re().mk_union(a1, b1);
-        result = re().mk_diff(mk_regex_reverse(r1), mk_regex_reverse(r2));
+    }
+    else if (re().is_intersection(r, r1, r2)) {
+        auto a1 = mk_regex_reverse(r1);
+        auto b1 = mk_regex_reverse(r2);
+        result = re().mk_inter(a1, b1);
+    }
+    else if (re().is_diff(r, r1, r2)) {
+        auto a1 = mk_regex_reverse(r1);
+        auto b1 = mk_regex_reverse(r2);
+        result = re().mk_diff(a1, b1);
+    }
     else if (re().is_star(r, r1))
         result = re().mk_star(mk_regex_reverse(r1));
     else if (re().is_plus(r, r1))
@@ -3982,8 +4049,13 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
             // if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else []
             //
             hd = mk_seq_first(r1);
-            m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')), 
+            // isolate nested conjunction for deterministic evaluation
-                m().mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele)), result);
+            auto a0 = u().mk_le(m_util.mk_char('0'), ele);
+            auto a1 = u().mk_le(ele, m_util.mk_char('9'));
+            auto a2 = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort)));
+            auto a3 = m().mk_eq(hd, ele);
+            auto inner = m().mk_and(a2, a3);
+            m_br.mk_and(a0, a1, inner, result);
             tl = re().mk_to_re(mk_seq_rest(r1));            
             return re_and(result, tl);
         }
@@ -4017,7 +4089,10 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
                 // tl = rest of reverse(r2) i.e. butlast of r2
                 //hd = str().mk_nth_i(r2, m_autil.mk_sub(str().mk_length(r2), one()));
                 hd = mk_seq_last(r2);
-                m_br.mk_and(m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result);
+                // factor nested constructor calls to enforce deterministic argument evaluation order
+                auto a_non_empty = m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort)));
+                auto a_eq        = m().mk_eq(hd, ele);
+                m_br.mk_and(a_non_empty, a_eq, result);
                 tl = re().mk_to_re(mk_seq_butlast(r2));
                 return re_and(result, re().mk_reverse(tl));
             }
@@ -4302,9 +4377,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         (re().is_union(b, b1, eps) && re().is_epsilon(eps)) ||
         (re().is_union(b, eps, b1) && re().is_epsilon(eps)))
     {
-        result = m().mk_ite(m().mk_eq(str().mk_length(a), zero()),
+        // deterministic evaluation order: build sub-expressions first
-            m().mk_true(),
+        auto len_a = str().mk_length(a);
-            re().mk_in_re(a, b1));
+        auto is_empty = m().mk_eq(len_a, zero());
+        auto in_b1 = re().mk_in_re(a, b1);
+        result = m().mk_ite(is_empty, m().mk_true(), in_b1);
         return BR_REWRITE_FULL;
     }
     if (str().is_empty(a)) {
@@ -4334,9 +4411,10 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         expr_ref len_hd(m_autil.mk_int(re().min_length(hd)), m()); 
         expr_ref len_a(str().mk_length(a), m());
         expr_ref len_tl(m_autil.mk_sub(len_a, len_hd), m());
-        result = m().mk_and(m_autil.mk_ge(len_a, len_hd),
+        auto ge_len = m_autil.mk_ge(len_a, len_hd);
-                            re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd),
+        auto prefix = re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd);
-                            re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl));
+        auto suffix = re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl);
+        result = m().mk_and(ge_len, prefix, suffix);
         return BR_REWRITE_FULL;
     }
     if (get_re_head_tail_reversed(b, hd, tl)) {
@@ -4345,10 +4423,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
         expr_ref len_a(str().mk_length(a), m());
         expr_ref len_hd(m_autil.mk_sub(len_a, len_tl), m());
         expr* s = nullptr;
-        result = m().mk_and(m_autil.mk_ge(len_a, len_tl),
+        auto ge_len = m_autil.mk_ge(len_a, len_tl);
-            re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd),
+        auto prefix = re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd);
-            (re().is_to_re(tl, s) ? m().mk_eq(s, str().mk_substr(a, len_hd, len_tl)) :
+        auto tail_seq = str().mk_substr(a, len_hd, len_tl);
-                re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl)));
+        auto tail = (re().is_to_re(tl, s) ? m().mk_eq(s, tail_seq) : re().mk_in_re(tail_seq, tl));
+        result = m().mk_and(ge_len, prefix, tail);
         return BR_REWRITE_FULL;
     }
 
@@ -4614,11 +4693,17 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
 br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
     expr *e1 = nullptr, *e2 = nullptr;
     if (re().is_intersection(a, e1, e2)) {
-        result = re().mk_union(re().mk_complement(e1), re().mk_complement(e2));
+        // enforce deterministic evaluation order for nested complement arguments
+        auto a1 = re().mk_complement(e1);
+        auto b1 = re().mk_complement(e2);
+        result = re().mk_union(a1, b1);
         return BR_REWRITE2;
     }
     if (re().is_union(a, e1, e2)) {
-        result = re().mk_inter(re().mk_complement(e1), re().mk_complement(e2));
+        // enforce deterministic evaluation order for nested complement arguments
+        auto a1 = re().mk_complement(e1);
+        auto b1 = re().mk_complement(e2);
+        result = re().mk_inter(a1, b1);
         return BR_REWRITE2;
     }
     if (re().is_empty(a)) {
@@ -5011,7 +5096,9 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
         rep.insert(elem, solution);
         rep(cond);
         if (!is_uninterp_const(elem)) { 
-            cond = m().mk_and(m().mk_eq(elem, solution), cond);
+            // ensure deterministic evaluation order when augmenting condition
+            auto eq_sol = m().mk_eq(elem, solution);
+            cond = m().mk_and(eq_sol, cond);
         }
     }    
     else if (all_ranges) {
@@ -5074,11 +5161,16 @@ br_status seq_rewriter::reduce_re_is_empty(expr* r, expr_ref& result) {
     }
     // Partial DNF expansion:
     else if (re().is_intersection(r, r1, r2) && re().is_union(r1, r3, r4)) {
-        result = eq_empty(re().mk_union(re().mk_inter(r3, r2), re().mk_inter(r4, r2)));
+        // enforce deterministic order for nested intersections inside union
+        auto a1 = re().mk_inter(r3, r2);
+        auto b1 = re().mk_inter(r4, r2);
+        result = eq_empty(re().mk_union(a1, b1));
         return BR_REWRITE3;
     }
     else if (re().is_intersection(r, r1, r2) && re().is_union(r2, r3, r4)) {
-        result = eq_empty(re().mk_union(re().mk_inter(r3, r1), re().mk_inter(r4, r1)));
+        auto a1 = re().mk_inter(r3, r1);
+        auto b1 = re().mk_inter(r4, r1);
+        result = eq_empty(re().mk_union(a1, b1));
         return BR_REWRITE3;
     }
     return BR_FAILED;

src/ast/sls/sls_bv_tracker.h

@@ -42,8 +42,37 @@ class sls_tracker {
     struct value_score {
         value_score() : value(unsynch_mpz_manager::mk_z(0)) {};
         value_score(value_score&&) noexcept = default;
+        value_score(const value_score &other) {
+            m = other.m;
+            if (other.m && !unsynch_mpz_manager::is_zero(other.value)) {
+                m->set(value, other.value);
+            }
+            score = other.score;
+            score_prune = other.score_prune;
+            has_pos_occ = other.has_pos_occ;
+            has_neg_occ = other.has_neg_occ;
+            distance = other.distance;
+            touched = other.touched;
+        }
         ~value_score() { if (m) m->del(value); }
         value_score& operator=(value_score&&) = default;
+        value_score &operator=(const value_score &other) {
+            if (this != &other) {
+                if (m)
+                    m->del(value);
+                m = other.m;
+                if (other.m && !unsynch_mpz_manager::is_zero(other.value)) {
+                    m->set(value, other.value);
+                }
+                score = other.score;
+                score_prune = other.score_prune;
+                has_pos_occ = other.has_pos_occ;
+                has_neg_occ = other.has_neg_occ;
+                distance = other.distance;
+                touched = other.touched;
+            }
+            return *this;
+        }
         unsynch_mpz_manager * m = nullptr;
         mpz value;
         double score = 0.0;

src/cmd_context/basic_cmds.cpp

@@ -334,6 +334,52 @@ public:
     }    
 };
 
+class prefer_cmd : public cmd {
+    expr *m_formula = nullptr;
+
+public:
+    prefer_cmd() : cmd("prefer") {}
+    char const *get_usage() const override {
+        return "<formula>";
+    }
+    char const *get_descr(cmd_context &ctx) const override {
+        return "set a preferred formula for the solver";
+    }
+    unsigned get_arity() const override {
+        return 1;
+    }
+    void prepare(cmd_context &ctx) override {
+        m_formula = nullptr;
+    }
+    cmd_arg_kind next_arg_kind(cmd_context &ctx) const override {
+        return CPK_EXPR;
+    }
+    void set_next_arg(cmd_context &ctx, expr *e) override {
+        m_formula = e;
+    }
+    void execute(cmd_context &ctx) override {
+        SASSERT(m_formula);
+        ctx.set_preferred(m_formula);
+    }
+};
+
+class reset_preferences_cmd : public cmd {
+    public:
+    reset_preferences_cmd() : cmd("reset-preferences") {}
+    char const *get_usage() const override {
+        return "";
+    }
+    char const *get_descr(cmd_context &ctx) const override {
+        return "reset all preferred formulas";
+    }
+    unsigned get_arity() const override {
+        return 0;
+    }
+    void execute(cmd_context &ctx) override {
+        ctx.reset_preferred();
+    }
+};
+
 class set_get_option_cmd : public cmd {
 protected:
     symbol      m_true;
@@ -926,6 +972,8 @@ void install_basic_cmds(cmd_context & ctx) {
     ctx.insert(alloc(get_info_cmd));
     ctx.insert(alloc(set_info_cmd));
     ctx.insert(alloc(set_initial_value_cmd));
+    ctx.insert(alloc(prefer_cmd));
+    ctx.insert(alloc(reset_preferences_cmd));
     ctx.insert(alloc(get_consequences_cmd));
     ctx.insert(alloc(builtin_cmd, "assert", "<term>", "assert term."));
     ctx.insert(alloc(builtin_cmd, "check-sat", "<boolean-constants>*", "check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true."));

src/cmd_context/cmd_context.cpp

@@ -628,6 +628,7 @@ cmd_context::~cmd_context() {
     finalize_tactic_manager();
     m_proof_cmds = nullptr;
     m_var2values.reset();
+    m_preferred = nullptr;
     reset(true);
     m_mcs.reset();
     m_solver = nullptr;
@@ -656,6 +657,8 @@ void cmd_context::set_opt(opt_wrapper* opt) {
     for (auto const& [var, value] : m_var2values)
         m_opt->initialize_value(var, value);
     m_opt->set_logic(m_logic);
+    if (m_preferred)
+        m_opt->set_preferred(m_preferred.get());
 }
 
 void cmd_context::global_params_updated() {
@@ -1518,6 +1521,8 @@ void cmd_context::reset(bool finalize) {
     m_dt_eh  = nullptr;
     m_std_subst = nullptr;
     m_rev_subst = nullptr;
+    m_preferred = nullptr;
+    m_var2values.reset();
     if (m_manager) {
         dealloc(m_pmanager);
         m_pmanager = nullptr;
@@ -1884,6 +1889,27 @@ void cmd_context::set_initial_value(expr* var, expr* value) {
     m_var2values.push_back({expr_ref(var, m()), expr_ref(value, m())});    
 }
 
+void cmd_context::set_preferred(expr* fmla) {
+    if (!m_preferred) {
+        auto p = alloc(preferred_value_propagator, m());
+        m_preferred = p;
+        if (get_solver()) {
+            get_solver()->user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh);
+            get_solver()->user_propagate_register_decide(p->decide_eh);
+        }
+    }
+    if (get_opt())
+        get_opt()->set_preferred(m_preferred.get());  
+    m_preferred->set_preferred(fmla);
+}
+
+void cmd_context::reset_preferred() {
+    if (!m_scopes.empty())
+        throw default_exception("reset-preferred can only be invoked at base level");
+    if (m_preferred) 
+        m_preferred->reset_preferred();   
+}
+
 
 void cmd_context::display_model(model_ref& mdl) {
     if (mdl) {
@@ -2263,6 +2289,11 @@ void cmd_context::mk_solver() {
     m_solver = mk_slice_solver(m_solver.get());
     if (m_simplifier_factory)
         m_solver = mk_simplifier_solver(m_solver.get(), &m_simplifier_factory);
+    if (m_preferred) {
+        auto p = m_preferred.get();
+        m_solver->user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh);
+        m_solver->user_propagate_register_decide(p->decide_eh);
+    }
 }
 
 

src/cmd_context/cmd_context.h

@@ -39,6 +39,7 @@ Notes:
 #include "solver/check_logic.h"
 #include "solver/progress_callback.h"
 #include "solver/simplifier_solver.h"
+#include "solver/preferred_value_propagator.h"
 #include "cmd_context/pdecl.h"
 #include "cmd_context/tactic_manager.h"
 #include "params/context_params.h"
@@ -163,6 +164,9 @@ struct builtin_decl {
 };
 
 class opt_wrapper : public check_sat_result {
+protected:
+    preferred_value_propagator *m_preferred = nullptr;
+
 public:
     opt_wrapper(ast_manager& m): check_sat_result(m) {}
     virtual bool empty() = 0;
@@ -176,7 +180,7 @@ public:
     virtual void get_box_model(model_ref& mdl, unsigned index) = 0;
     virtual void updt_params(params_ref const& p) = 0;
     virtual void initialize_value(expr* var, expr* value) = 0;
-
+    void set_preferred(preferred_value_propagator *p) { m_preferred = p; }
 };
 
 class ast_context_params : public context_params { 
@@ -265,6 +269,7 @@ protected:
     dictionary<object_ref*>      m_object_refs; // anything that can be named.
     dictionary<sexpr*>           m_user_tactic_decls;
     vector<std::pair<expr_ref, expr_ref>> m_var2values;
+    scoped_ptr<preferred_value_propagator> m_preferred;
 
     dictionary<func_decls>       m_func_decls;
     obj_map<func_decl, symbol>   m_func_decl2alias;
@@ -429,6 +434,8 @@ public:
     void set_solver(solver* s) { m_solver = s; }
     void set_proof_cmds(proof_cmds* pc) { m_proof_cmds = pc; }
     void set_initial_value(expr* var, expr* value);
+    void set_preferred(expr *fmla);
+    void reset_preferred();
 
     void set_solver_factory(solver_factory * s);
     void set_simplifier_factory(simplifier_factory& sf) { m_simplifier_factory = sf; }

src/muz/base/dl_context.cpp

@@ -776,10 +776,26 @@ namespace datalog {
         array_util    ar;
         DL_ENGINE     m_engine_type;
 
-        bool is_large_bv(sort* s) {
+        bool is_large_bv(expr *e) {
+            sort *s = e->get_sort();
+            if (bv.is_bv_sort(s)) {
+                unsigned sz = bv.get_bv_size(s);
+                if (sz > 24)
+                    return true;
+            }
+            if (is_app(e)) {
+                unsigned sz = 0;
+                for (auto arg : *to_app(e)) {
+                    if (bv.is_bv(arg))
+                        sz += bv.get_bv_size(arg->get_sort());
+                }
+                if (sz > 24)
+                    return true;
+            }
             return false;
         }
 
+
     public:
         engine_type_proc(ast_manager& m): m(m), a(m), dt(m), bv(m), ar(m), m_engine_type(DATALOG_ENGINE) {}
 
@@ -795,7 +811,7 @@ namespace datalog {
             else if (dt.is_datatype(e->get_sort())) {
                 m_engine_type = SPACER_ENGINE;
             }
-            else if (is_large_bv(e->get_sort())) {
+            else if (is_large_bv(e)) {
                 m_engine_type = SPACER_ENGINE;
             }
             else if (!e->get_sort()->get_num_elements().is_finite()) {

src/nlsat/nlsat_explain.cpp

@@ -1226,6 +1226,7 @@ namespace nlsat {
          * https://arxiv.org/abs/2003.00409 
          */
         void project_cdcac(polynomial_ref_vector & ps, var max_x) {
+            bool first = true;
             if (ps.empty())
                 return;
 
@@ -1244,8 +1245,6 @@ namespace nlsat {
             // Remark: after vanishing coefficients are eliminated, ps may not contain max_x anymore
             
             polynomial_ref_vector samples(m_pm);
-
-            
             if (x < max_x)
                 cac_add_cell_lits(ps, x, samples);
 
@@ -1256,9 +1255,18 @@ namespace nlsat {
                 }
                 TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
                       display(tout, ps); tout << "\n";);
+                if (first) { // The first run is special because x is not constrained by the sample, we cannot surround it by the root functions.
+                    // we make the polynomials in ps delinable
                     add_lcs(ps, x);
                     psc_discriminant(ps, x);
                     psc_resultant(ps, x);
+                    first = false;
+                }
+                else {
+                    add_lcs(ps, x);
+                    psc_discriminant(ps, x);
+                    psc_resultant_sample(ps, x, samples);
+                }
                 
                 if (m_todo.empty())
                     break;

src/opt/opt_context.cpp

@@ -316,6 +316,11 @@ namespace opt {
             m_model_converter->convert_initialize_value(m_scoped_state.m_values);
         for (auto & [var, value] : m_scoped_state.m_values) 
             s.user_propagate_initialize_value(var, value);
+        if (m_preferred) {
+            auto p = m_preferred;
+            s.user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh);
+            s.user_propagate_register_decide(p->decide_eh);
+        }
         
         opt_params optp(m_params);
         symbol pri = optp.priority();

src/opt/opt_context.h

@@ -22,6 +22,7 @@ Notes:
 #include "ast/bv_decl_plugin.h"
 #include "ast/converters/model_converter.h"
 #include "tactic/tactic.h"
+#include "solver/preferred_value_propagator.h"
 #include "qe/qsat.h"
 #include "opt/opt_solver.h"
 #include "opt/opt_pareto.h"

src/opt/opt_solver.h

@@ -117,6 +117,49 @@ namespace opt {
         void set_phase(phase* p) override { m_context.set_phase(p); }
         void move_to_front(expr* e) override { m_context.move_to_front(e); }
         void user_propagate_initialize_value(expr* var, expr* value) override { m_context.user_propagate_initialize_value(var, value); }
+        void user_propagate_init(void *ctx, user_propagator::push_eh_t &push_eh, user_propagator::pop_eh_t &pop_eh, user_propagator::fresh_eh_t &fresh_eh) override {
+            m_context.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
+            m_first = false;
+        }
+
+        void user_propagate_register_fixed(user_propagator::fixed_eh_t &fixed_eh) override {
+            m_context.user_propagate_register_fixed(fixed_eh);
+        }
+
+        void user_propagate_register_final(user_propagator::final_eh_t &final_eh) override {
+            m_context.user_propagate_register_final(final_eh);
+        }
+
+        void user_propagate_register_eq(user_propagator::eq_eh_t &eq_eh) override {
+            m_context.user_propagate_register_eq(eq_eh);
+        }
+
+        void user_propagate_register_diseq(user_propagator::eq_eh_t &diseq_eh) override {
+            m_context.user_propagate_register_diseq(diseq_eh);
+        }
+
+        void user_propagate_register_expr(expr *e) override {
+            m_context.user_propagate_register_expr(e);
+        }
+
+        void user_propagate_register_created(user_propagator::created_eh_t &r) override {
+            m_context.user_propagate_register_created(r);   
+        }
+
+        void user_propagate_register_decide(user_propagator::decide_eh_t &r) override {
+            m_context.user_propagate_register_decide(r);
+        }
+
+        void user_propagate_register_on_binding(user_propagator::binding_eh_t &r) override {
+            m_context.user_propagate_register_on_binding(r);
+        }
+
+         void user_propagate_clear() override {
+        }
+
+        void register_on_clause(void *, user_propagator::on_clause_eh_t &r) override {
+            m_context.register_on_clause(nullptr, r);
+        }
 
         void set_logic(symbol const& logic);
 

src/parsers/smt2/smt2parser.cpp

@@ -1638,8 +1638,10 @@ namespace smt2 {
         //    '(' 'as' <identifier> <sort> ')'
         //    '(' '_'  <identifier> <num>+ ')'
         //    '(' 'as' <identifier '(' '_' <identifier> (<num>|<func-decl-ref>)+ ')' <sort> ')'
-        symbol parse_qualified_identifier(bool & has_as) {
+        //    '(' lambda (...) <expr> ')'
+        symbol parse_qualified_identifier(bool & has_as, bool & is_lambda) {
             SASSERT(curr_is_lparen() || curr_is_identifier());
+            is_lambda = false;
             if (curr_is_identifier()) {
                 has_as   = false;
                 symbol r = curr_id();
@@ -1648,6 +1650,12 @@ namespace smt2 {
             }
             SASSERT(curr_is_lparen());
             next();
+            if (curr_id_is_lambda()) {
+                is_lambda = true;
+                has_as = false;
+                return symbol("select");
+            }
+                           
             if (!curr_is_identifier() || (!curr_id_is_underscore() && !curr_id_is_as()))
                 throw parser_exception("invalid qualified/indexed identifier, '_' or 'as' expected");
             return parse_qualified_identifier_core(has_as);
@@ -1860,11 +1868,14 @@ namespace smt2 {
             SASSERT(curr_is_lparen() || curr_is_identifier());
             unsigned param_spos  = m_param_stack.size();
             unsigned expr_spos  = expr_stack().size();
-            bool     has_as;
+            bool has_as, is_lambda;
-            symbol   f = parse_qualified_identifier(has_as);
+            auto f = parse_qualified_identifier(has_as, is_lambda);
-            void * mem      = m_stack.allocate(sizeof(quant_frame));
+
+            void * mem      = m_stack.allocate(sizeof(app_frame));
             new (mem) app_frame(f, expr_spos, param_spos, has_as);
             m_num_expr_frames++;
+            if (is_lambda) 
+                push_quant_frame(lambda_k);            
         }
 
         void push_expr_frame(expr_frame * curr) {

src/smt/theory_bv.cpp

@@ -1890,6 +1890,8 @@ namespace smt {
 
     theory_bv::var_enode_pos theory_bv::get_bv_with_theory(bool_var v, theory_id id) const {
         atom* a      = get_bv2a(v);
+        if (!a)
+            return var_enode_pos(nullptr, UINT32_MAX);
         svector<var_enode_pos> vec;
         if (!a->is_bit())
             return var_enode_pos(nullptr, UINT32_MAX);

src/smt/theory_user_propagator.cpp

@@ -209,59 +209,34 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
     if (!m_decide_eh)
         return;
 
-    const bool_var_data& d = ctx.get_bdata(var);
+    expr *e = ctx.bool_var2expr(var);
+    if (!e)
+        e = m.mk_true(); // use a dummy case split atom.
 
-    if (!d.is_enode() && !d.is_theory_atom())
+    unsigned bit = 0;
-        return;
+    // determine if case split is a bit-position in a bit-vector
-
+    {
-    enode* original_enode = nullptr;
-    unsigned original_bit = 0;
         bv_util bv(m);
-    theory* th = nullptr;
+        auto th = ctx.get_theory(bv.get_fid());
-    theory_var v = null_theory_var;
+        if (th) {
-
+            // it is then n'th bit of a bit-vector n.
-    // get the associated theory
+            auto [n, nbit] = static_cast<theory_bv *>(th)->get_bv_with_theory(var, get_family_id());
-    if (!d.is_enode()) {
+            if (n) {
-        // it might be a value that does not have an enode
+                e = n->get_expr();
-        th = ctx.get_theory(d.get_theory());
+                bit = nbit;
-    }
-    else {
-        original_enode = ctx.bool_var2enode(var);
-        v = original_enode->get_th_var(get_family_id());
-        if (v == null_theory_var) {
-            // it is not a registered boolean expression
-            th = ctx.get_theory(d.get_theory());
             }
         }
-
-    if (v == null_theory_var && !th)
-        return;
-
-    if (v == null_theory_var && th->get_family_id() != bv.get_fid())
-        return;
-
-    if (v == null_theory_var) {
-        // it is not a registered boolean value but it is a bitvector
-        auto registered_bv = ((theory_bv*) th)->get_bv_with_theory(var, get_family_id());
-        if (!registered_bv.first)
-            // there is no registered bv associated with the bit
-            return;
-        original_enode = registered_bv.first;
-        original_bit = registered_bv.second;
-        v = original_enode->get_th_var(get_family_id());
     }
 
-    // call the registered callback
-    unsigned new_bit = original_bit;
-
     force_push();
-    expr *e = var2expr(v);
+    m_decide_eh(m_user_context, this, e, bit, is_pos);
-    m_decide_eh(m_user_context, this, e, new_bit, is_pos);
 
     bool_var new_var;
     if (!get_case_split(new_var, is_pos) || new_var == var)
         // The user did not interfere
         return;
+    TRACE(user_propagate,
+          tout << "decide: " << ctx.bool_var2expr(var) << " -> " << ctx.bool_var2expr(new_var) << "\n");
     var = new_var;
                     
     // check if the new variable is unassigned

src/solver/preferred_value_propagator.h

@@ -0,0 +1,85 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    preferred_value_propagator.h
+
+Abstract:
+
+    Specialized propagator for preferred values
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 10-2-2025
+
+Notes:
+
+--*/
+#pragma once
+
+#include "tactic/user_propagator_base.h"
+#include "util/trail.h"
+
+
+class preferred_value_propagator {
+    ast_manager &m;
+    expr_ref_vector m_preferred;
+    unsigned m_qhead = 0;
+    trail_stack m_trail;
+
+    bool decide(user_propagator::callback& cb) {
+        if (m_qhead >= m_preferred.size())
+            return false;
+        m_trail.push(value_trail(m_qhead));
+        while (m_qhead < m_preferred.size()) {
+            expr *e = m_preferred.get(m_qhead);
+            bool is_not = m.is_not(e, e);
+            m_qhead++;
+            if (cb.next_split_cb(e, 0, is_not ? l_false : l_true))
+                return true;
+        }
+        return false;
+    }
+
+public:
+    preferred_value_propagator(ast_manager &m) : m(m), m_preferred(m) {
+         push_eh = [](void * ctx, user_propagator::callback* cb) {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            p.m_trail.push_scope(); 
+         };
+        pop_eh = [](void * ctx, user_propagator::callback* cb, unsigned n) -> void {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            p.m_trail.pop_scope(n);
+        };
+        fresh_eh = [](void* ctx, ast_manager& dst, user_propagator::context_obj*& co) -> void* {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            ast_translation tr(p.m, dst);
+            auto r = alloc(preferred_value_propagator, dst);
+            for (auto e : p.m_preferred)
+                r->set_preferred(tr(e));
+            return r;
+        };
+
+        decide_eh = [](void * ctx, user_propagator::callback * cb, expr *, unsigned, bool) -> bool {
+            auto &p = *static_cast<preferred_value_propagator *>(ctx);
+            return p.decide(*cb);
+        };
+    }
+    ~preferred_value_propagator() = default;
+    void set_preferred(expr *e) {
+        m_preferred.push_back(e);
+        if (m_trail.get_num_scopes() > 0)
+            m_trail.push(push_back_vector(m_preferred));
+    }
+    void reset_preferred() {
+        if (m_trail.get_num_scopes() != 0)
+            throw default_exception("cannot reset preferred values in scoped context");
+        m_preferred.reset();
+        SASSERT(m_qhead == 0);
+    }
+    user_propagator::push_eh_t push_eh;
+    user_propagator::pop_eh_t pop_eh;
+    user_propagator::fresh_eh_t fresh_eh;
+    user_propagator::decide_eh_t decide_eh;
+};

src/test/CMakeLists.txt

@@ -21,6 +21,7 @@ add_executable(test-z3
   api_polynomial.cpp
   api_pb.cpp
   api_datalog.cpp
+  parametric_datatype.cpp
   arith_rewriter.cpp
   arith_simplifier_plugin.cpp
   ast.cpp

src/test/main.cpp

@@ -179,6 +179,7 @@ int main(int argc, char ** argv) {
     TST(api_polynomial);
     TST(api_pb);
     TST(api_datalog);
+    TST(parametric_datatype);
     TST(cube_clause);
     TST(old_interval);
     TST(get_implied_equalities);

src/test/parametric_datatype.cpp

@@ -0,0 +1,122 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    parametric_datatype.cpp
+
+Abstract:
+
+    Test parametric datatypes with type variables.
+
+Author:
+
+    Copilot 2025-10-12
+
+--*/
+
+#include "api/z3.h"
+#include "util/util.h"
+#include <iostream>
+
+
+/**
+ * Test Z3_mk_polymorphic_datatype API with explicit parameters.
+ * 
+ * This test demonstrates the API that explicitly accepts type parameters.
+ */
+static void test_polymorphic_datatype_api() {
+    std::cout << "test_polymorphic_datatype_api\n";
+    
+    Z3_config cfg = Z3_mk_config();
+    Z3_context ctx = Z3_mk_context(cfg);
+    Z3_del_config(cfg);
+    
+    // Create type variables alpha and beta for polymorphic datatype
+    Z3_symbol alpha_sym = Z3_mk_string_symbol(ctx, "alpha");
+    Z3_symbol beta_sym = Z3_mk_string_symbol(ctx, "beta");
+    Z3_sort alpha = Z3_mk_type_variable(ctx, alpha_sym);
+    Z3_sort beta = Z3_mk_type_variable(ctx, beta_sym);
+    
+    // Define parametric triple datatype with constructor mk-triple(first: alpha, second: beta, third: alpha)
+    Z3_symbol triple_name = Z3_mk_string_symbol(ctx, "triple");
+    Z3_symbol mk_triple_name = Z3_mk_string_symbol(ctx, "mk-triple");
+    Z3_symbol is_triple_name = Z3_mk_string_symbol(ctx, "is-triple");
+    Z3_symbol first_name = Z3_mk_string_symbol(ctx, "first");
+    Z3_symbol second_name = Z3_mk_string_symbol(ctx, "second");
+    Z3_symbol third_name = Z3_mk_string_symbol(ctx, "third");
+    
+    Z3_symbol field_names[3] = {first_name, second_name, third_name};
+    Z3_sort field_sorts[3] = {alpha, beta, alpha};  // Use type variables
+    unsigned sort_refs[3] = {0, 0, 0};  // Not recursive references
+    
+    Z3_constructor mk_triple_con = Z3_mk_constructor(
+        ctx, mk_triple_name, is_triple_name, 3, field_names, field_sorts, sort_refs
+    );
+    
+    // Create the parametric datatype using Z3_mk_polymorphic_datatype
+    Z3_constructor constructors[1] = {mk_triple_con};
+    Z3_sort type_params[2] = {alpha, beta};
+    Z3_sort triple = Z3_mk_polymorphic_datatype(ctx, triple_name, 2, type_params, 1, constructors);
+    
+    Z3_del_constructor(ctx, mk_triple_con);
+    
+    std::cout << "Created parametric triple datatype using Z3_mk_polymorphic_datatype\n";
+    std::cout << "triple sort: " << Z3_sort_to_string(ctx, triple) << "\n";
+    
+    // Now instantiate the datatype with concrete types
+    Z3_sort int_sort = Z3_mk_int_sort(ctx);
+    Z3_sort bool_sort = Z3_mk_bool_sort(ctx);
+    
+    // Create (triple Int Bool)
+    Z3_sort params_int_bool[2] = {int_sort, bool_sort};
+    Z3_sort triple_int_bool = Z3_mk_datatype_sort(ctx, triple_name, 2, params_int_bool);
+    
+    std::cout << "Instantiated triple with Int and Bool\n";
+    std::cout << "triple_int_bool: " << Z3_sort_to_string(ctx, triple_int_bool) << "\n";
+    
+    // Get constructors and accessors from the instantiated datatype
+    Z3_func_decl mk_triple_int_bool = Z3_get_datatype_sort_constructor(ctx, triple_int_bool, 0);
+    Z3_func_decl first_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 0);
+    Z3_func_decl second_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 1);
+    Z3_func_decl third_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 2);
+    
+    std::cout << "Got constructors and accessors from instantiated datatype\n";
+    
+    // Create a constant t : (triple Int Bool)
+    Z3_symbol t_sym = Z3_mk_string_symbol(ctx, "t");
+    Z3_ast t = Z3_mk_const(ctx, t_sym, triple_int_bool);
+    
+    // Create (first t) - should be Int
+    Z3_ast first_t = Z3_mk_app(ctx, first_int_bool, 1, &t);
+    
+    // Create (third t) - should also be Int
+    Z3_ast third_t = Z3_mk_app(ctx, third_int_bool, 1, &t);
+    
+    // Create the equality (= (first t) (third t))
+    Z3_ast eq = Z3_mk_eq(ctx, first_t, third_t);
+    
+    std::cout << "Created term: " << Z3_ast_to_string(ctx, eq) << "\n";
+    
+    // Verify the term was created successfully
+    ENSURE(eq != nullptr);
+    
+    // Check that first_t and third_t have the same sort (Int)
+    Z3_sort first_t_sort = Z3_get_sort(ctx, first_t);
+    Z3_sort third_t_sort = Z3_get_sort(ctx, third_t);
+    
+    std::cout << "Sort of (first t): " << Z3_sort_to_string(ctx, first_t_sort) << "\n";
+    std::cout << "Sort of (third t): " << Z3_sort_to_string(ctx, third_t_sort) << "\n";
+    
+    // Both should be Int
+    ENSURE(Z3_is_eq_sort(ctx, first_t_sort, int_sort));
+    ENSURE(Z3_is_eq_sort(ctx, third_t_sort, int_sort));
+    
+    std::cout << "test_polymorphic_datatype_api passed!\n";
+    
+    Z3_del_context(ctx);
+}
+
+void tst_parametric_datatype() {
+    test_polymorphic_datatype_api();
+}

src/util/mpz.cpp

@@ -2332,7 +2332,6 @@ bool mpz_manager<SYNCH>::is_perfect_square(mpz const & a, mpz & root) {
     set(sq_lo, 1);    
 
     bool result = false;
-    bool first = true;
     // lo*lo <= *this < hi*hi
 
     // first find small interval lo*lo <= a <<= hi*hi

src/util/obj_hashtable.h

@@ -58,6 +58,13 @@ public:
     struct key_data {
         Key *  m_key = nullptr;
         Value  m_value;
+        key_data() {}
+        key_data(Key *key) : m_key(key) {}
+        key_data(Key *k, Value const &v) : m_key(k), m_value(v) {}
+        key_data(key_data &&kd) noexcept = default;
+        key_data(key_data const &kd) noexcept = default;
+        key_data &operator=(key_data const &kd)  = default;
+        key_data &operator=(key_data &&kd) = default;
         Value const & get_value() const { return m_value; }
         Key & get_key () const { return *m_key; }
         unsigned hash() const { return m_key->hash(); }

src/util/rlimit.cpp

@@ -78,6 +78,8 @@ char const* reslimit::get_cancel_msg() const {
 
 void reslimit::push_child(reslimit* r) {
     lock_guard lock(*g_rlimit_mux);
+    r->m_limit = std::min(r->m_limit, m_limit - std::min(m_limit, m_count));
+    r->m_count = 0;
     m_children.push_back(r);    
 }
 

src/util/warning.cpp

@@ -24,6 +24,10 @@ Revision History:
 #include "util/buffer.h"
 #include "util/vector.h"
 
+#ifndef SINGLE_THREAD
+#include <mutex>
+#endif
+
 #ifdef _WINDOWS
 #if defined( __MINGW32__ ) && ( defined( __GNUG__ ) || defined( __clang__ ) )
 #include <crtdbg.h>
@@ -67,6 +71,10 @@ static bool g_use_std_stdout = false;
 static std::ostream* g_error_stream = nullptr;
 static std::ostream* g_warning_stream = nullptr;
 
+#ifndef SINGLE_THREAD
+static std::mutex g_warning_mutex;
+#endif
+
 void send_warnings_to_stdout(bool flag) {
     g_use_std_stdout = flag;
 }
@@ -129,6 +137,9 @@ void print_msg(std::ostream * out, const char* prefix, const char* msg, va_list
 
 void warning_msg(const char * msg, ...) {
     if (g_warning_msgs) {
+#ifndef SINGLE_THREAD
+        std::lock_guard<std::mutex> lock(g_warning_mutex);
+#endif
         va_list args;
         va_start(args, msg);
         print_msg(g_warning_stream, "WARNING: ", msg, args);

z3test

@@ -1 +0,0 @@
-Subproject commit 4186a4bf47b920d50671c396f904fe69e3e5c41d