diff --git a/.clang-format b/.clang-format index c4bbbf1e1..1d7d35dc5 100644 --- a/.clang-format +++ b/.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 diff --git a/.github/workflows/codeql-analysis.yml b/.github/workflows/codeql-analysis.yml new file mode 100644 index 000000000..279bd2b99 --- /dev/null +++ b/.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 \ No newline at end of file diff --git a/a-tst.gcno b/a-tst.gcno deleted file mode 100644 index 3b9127650..000000000 Binary files a/a-tst.gcno and /dev/null differ diff --git a/codeql/custom_queries/FindUnderspecified.ql b/codeql/custom_queries/FindUnderspecified.ql new file mode 100644 index 000000000..0d33dc4f8 --- /dev/null +++ b/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() \ No newline at end of file diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index 06f3ffe3e..c3902dfff 100644 --- a/examples/c++/example.cpp +++ b/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"; diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index 2509434f8..886165455 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -306,12 +306,24 @@ extern "C" { Z3_CATCH; } - static datatype_decl* mk_datatype_decl(Z3_context c, - Z3_symbol name, - unsigned num_constructors, - Z3_constructor constructors[]) { + 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 constrs; for (unsigned i = 0; i < num_constructors; ++i) { constructor* cn = reinterpret_cast(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 const& cnstrs = *data_util.get_datatype_constructors(s); + + for (unsigned i = 0; i < num_constructors; ++i) { + constructor* cn = reinterpret_cast(constructors[i]); + cn->m_constructor = cnstrs[i]; + } + RETURN_Z3_mk_polymorphic_datatype(of_sort(s)); + Z3_CATCH_RETURN(nullptr); + } + typedef ptr_vector 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)); - sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, 1, &p); + vector ps; + 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 datas; for (unsigned i = 0; i < num_sorts; ++i) { constructor_list* cl = reinterpret_cast(constructor_lists[i]); - datas.push_back(mk_datatype_decl(c, sort_names[i], cl->size(), reinterpret_cast(cl->data()))); + datas.push_back(api_datatype_decl(c, sort_names[i], 0, nullptr, cl->size(), reinterpret_cast(cl->data()))); } sort_ref_vector _sorts(m); bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.data(), 0, nullptr, _sorts); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 0a1e359da..71f3ff79b 100644 --- a/src/api/c++/z3++.h +++ b/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 _params(params); + Z3_sort s = Z3_mk_datatype_sort(*this, name, _params.size(), _params.ptr()); check_error(); return sort(*this, s); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 9293b1a31..49f183428 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -474,6 +474,36 @@ namespace Microsoft.Z3 return new DatatypeSort(this, symbol, constructors); } + /// + /// Create a forward reference to a datatype sort. + /// This is useful for creating recursive datatypes or parametric datatypes. + /// + /// name of the datatype sort + /// optional array of sort parameters for parametric datatypes + public DatatypeSort MkDatatypeSortRef(Symbol name, Sort[] parameters = null) + { + Debug.Assert(name != null); + CheckContextMatch(name); + if (parameters != null) + CheckContextMatch(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)); + } + + /// + /// Create a forward reference to a datatype sort. + /// This is useful for creating recursive datatypes or parametric datatypes. + /// + /// name of the datatype sort + /// optional array of sort parameters for parametric datatypes + public DatatypeSort MkDatatypeSortRef(string name, Sort[] parameters = null) + { + using var symbol = MkSymbol(name); + return MkDatatypeSortRef(symbol, parameters); + } + /// /// Create mutually recursive datatypes. /// diff --git a/src/api/java/AST.java b/src/api/java/AST.java index 99cdde948..0257f5294 100644 --- a/src/api/java/AST.java +++ b/src/api/java/AST.java @@ -208,7 +208,13 @@ public class AST extends Z3Object implements Comparable case Z3_FUNC_DECL_AST: return new FuncDecl<>(ctx, obj); case Z3_QUANTIFIER_AST: - return new Quantifier(ctx, obj); + // 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: diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 2350b52ae..691ecd737 100644 --- a/src/api/java/Context.java +++ b/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 DatatypeSort 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 DatatypeSort 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 DatatypeSort 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 DatatypeSort mkDatatypeSortRef(String name) + { + return mkDatatypeSortRef(name, null); + } + /** * Create mutually recursive datatypes. * @param names names of datatype sorts diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 60826665d..910869bcd 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -2148,8 +2148,15 @@ public class Expr 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) - return new Quantifier(ctx, obj); + 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)); diff --git a/src/api/java/Lambda.java b/src/api/java/Lambda.java index 780e543c8..a42dfbf45 100644 --- a/src/api/java/Lambda.java +++ b/src/api/java/Lambda.java @@ -126,7 +126,7 @@ public class Lambda extends ArrayExpr } - private Lambda(Context ctx, long obj) + Lambda(Context ctx, long obj) { super(ctx, obj); } diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml index 4d5238957..cc7294aba 100644 --- a/src/api/ml/z3.ml +++ b/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 diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli index 7afc01918..6764b0e2d 100644 --- a/src/api/ml/z3.mli +++ b/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 diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 051265a78..128726dae 100644 --- a/src/api/python/z3/z3.py +++ b/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): - """Create a reference to a sort that was declared, or will be declared, as a recursive datatype""" +def DatatypeSort(name, params=None, ctx=None): + """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 diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9de58e057..baa2fa34c 100644 --- a/src/api/z3_api.h +++ b/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. diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index f91afc9ac..5bb918c5f 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/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(), diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp index 4de3d7ba7..746d48fa2 100644 --- a/src/ast/normal_forms/nnf.cpp +++ b/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 - r = m.mk_and(m.mk_or(lhs, rhs), m.mk_or(not_lhs, not_rhs)); + else { + 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)), - m.mk_iff_oeq(m.mk_rewrite(aux, r))); + auto a = mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)); + pr = m.mk_transitivity(a, m.mk_iff_oeq(m.mk_rewrite(aux, r))); } } else { diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 8851bc7fd..d5ad70a1f 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/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 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 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 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(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(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 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 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 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(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(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 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; + case LE: + { + 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)) { diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index c5ef8d9ed..d708af9e0 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/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) - result = str().mk_substr(s, m_autil.mk_int(jv + 1), mk_sub(k, 1)); - else - result = str().mk_substr(t, one(), mk_sub(str().mk_length(t), 1)); + if (str().is_extract(t, s, j, k) && m_autil.is_numeral(j, jv) && jv >= 0) { + auto a = m_autil.mk_int(jv + 1); + result = str().mk_substr(s, a, mk_sub(k, 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), - str().mk_nth_u(a, b)); + { + // deterministic evaluation order for guard components + 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), - m_autil.mk_le(c, str().mk_length(a))), - c, - minus_one()); + // enforce deterministic evaluation order for bounds checks + auto a1 = m_autil.mk_le(zero(), c); + auto b1 = m_autil.mk_le(c, str().mk_length(a)); + 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), - str().mk_concat(bs.size()-1, bs.data()+1, sort_a)); + auto a = str().mk_concat(as.size(), as.data(), 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)), - re().mk_reverse(re().mk_to_re(s1))); + auto a_rev = re().mk_reverse(re().mk_to_re(s2)); + 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)) - result = re().mk_union(mk_regex_reverse(r1), mk_regex_reverse(r2)); - else if (re().is_intersection(r, r1, r2)) - result = re().mk_inter(mk_regex_reverse(r1), mk_regex_reverse(r2)); - else if (re().is_diff(r, r1, r2)) - result = re().mk_diff(mk_regex_reverse(r1), mk_regex_reverse(r2)); + else if (re().is_union(r, r1, r2)) { + // enforce deterministic evaluation order + auto a1 = mk_regex_reverse(r1); + auto b1 = mk_regex_reverse(r2); + result = re().mk_union(a1, b1); + } + 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')), - m().mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele)), result); + // isolate nested conjunction for deterministic evaluation + 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()), - m().mk_true(), - re().mk_in_re(a, b1)); + // deterministic evaluation order: build sub-expressions first + auto len_a = str().mk_length(a); + 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), - 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 ge_len = m_autil.mk_ge(len_a, len_hd); + auto prefix = re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd); + 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), - 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)) : - re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl))); + auto ge_len = m_autil.mk_ge(len_a, len_tl); + auto prefix = re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd); + auto tail_seq = str().mk_substr(a, len_hd, len_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; diff --git a/src/ast/sls/sls_bv_tracker.h b/src/ast/sls/sls_bv_tracker.h index 7c9b02a46..37ef91480 100644 --- a/src/ast/sls/sls_bv_tracker.h +++ b/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; diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index ff74e4614..ed7e14b20 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/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 ""; + } + 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", "", "assert term.")); ctx.insert(alloc(builtin_cmd, "check-sat", "*", "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.")); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 4f093e749..5513a86ef 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/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) { @@ -2261,8 +2287,13 @@ void cmd_context::mk_solver() { m_params.get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled); m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic); m_solver = mk_slice_solver(m_solver.get()); - if (m_simplifier_factory) + 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); + } } diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 83d0f06ee..b08944616 100644 --- a/src/cmd_context/cmd_context.h +++ b/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 m_object_refs; // anything that can be named. dictionary m_user_tactic_decls; vector> m_var2values; + scoped_ptr m_preferred; dictionary m_func_decls; obj_map 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; } diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 9e154f9dc..f90768c0a 100644 --- a/src/muz/base/dl_context.cpp +++ b/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()) { diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 83c5f31b6..ff1ae6a07 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/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";); - add_lcs(ps, x); - psc_discriminant(ps, x); - psc_resultant(ps, x); + 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; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 6244533f0..388befe93 100644 --- a/src/opt/opt_context.cpp +++ b/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(); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 123d3a44b..ed2377bab 100644 --- a/src/opt/opt_context.h +++ b/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" @@ -231,7 +232,7 @@ namespace opt { void get_labels(svector & r) override; void get_unsat_core(expr_ref_vector & r) override; std::string reason_unknown() const override; - void set_reason_unknown(char const* msg) override { m_unknown = msg; } + void set_reason_unknown(char const* msg) override { m_unknown = msg; } void display_assignment(std::ostream& out) override; bool is_pareto() override { return m_pareto.get() != nullptr; } diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index e60bbfae6..a409e573a 100644 --- a/src/opt/opt_solver.h +++ b/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); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 0841f73ee..3ce1ece4a 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1621,7 +1621,7 @@ namespace smt2 { if (curr_id_is_underscore()) { has_as = false; return parse_indexed_identifier_core(); - } + } else { SASSERT(curr_id_is_as()); has_as = true; @@ -1638,8 +1638,10 @@ namespace smt2 { // '(' 'as' ')' // '(' '_' + ')' // '(' 'as' (|)+ ')' ')' - symbol parse_qualified_identifier(bool & has_as) { + // '(' lambda (...) ')' + 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; - symbol f = parse_qualified_identifier(has_as); - void * mem = m_stack.allocate(sizeof(quant_frame)); + bool has_as, is_lambda; + auto f = parse_qualified_identifier(has_as, is_lambda); + + 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) { diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 93f09f639..7b0afd7e1 100644 --- a/src/smt/theory_bv.cpp +++ b/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 vec; if (!a->is_bit()) return var_enode_pos(nullptr, UINT32_MAX); diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index f8c2a35b8..d8adbdb70 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -209,61 +209,36 @@ 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()) - return; - - enode* original_enode = nullptr; - unsigned original_bit = 0; - bv_util bv(m); - theory* th = nullptr; - theory_var v = null_theory_var; - - // get the associated theory - if (!d.is_enode()) { - // it might be a value that does not have an enode - th = ctx.get_theory(d.get_theory()); - } - 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()); + unsigned bit = 0; + // determine if case split is a bit-position in a bit-vector + { + bv_util bv(m); + auto th = ctx.get_theory(bv.get_fid()); + if (th) { + // it is then n'th bit of a bit-vector n. + auto [n, nbit] = static_cast(th)->get_bv_with_theory(var, get_family_id()); + if (n) { + e = n->get_expr(); + bit = nbit; + } } } - 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, new_bit, is_pos); + m_decide_eh(m_user_context, this, e, 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 if (ctx.get_assignment(var) != l_undef) throw default_exception("expression in \"decide\" is already assigned"); diff --git a/src/solver/preferred_value_propagator.h b/src/solver/preferred_value_propagator.h new file mode 100644 index 000000000..da83c1fa3 --- /dev/null +++ b/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(ctx); + p.m_trail.push_scope(); + }; + pop_eh = [](void * ctx, user_propagator::callback* cb, unsigned n) -> void { + auto &p = *static_cast(ctx); + p.m_trail.pop_scope(n); + }; + fresh_eh = [](void* ctx, ast_manager& dst, user_propagator::context_obj*& co) -> void* { + auto &p = *static_cast(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(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; +}; \ No newline at end of file diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 206dc0530..77cf2f6fd 100644 --- a/src/test/CMakeLists.txt +++ b/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 diff --git a/src/test/main.cpp b/src/test/main.cpp index c6bb23378..005b7ab59 100644 --- a/src/test/main.cpp +++ b/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); diff --git a/src/test/parametric_datatype.cpp b/src/test/parametric_datatype.cpp new file mode 100644 index 000000000..2a31803aa --- /dev/null +++ b/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 + + +/** + * 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(); +} diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 0d4df44a2..94d95d85c 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -2332,7 +2332,6 @@ bool mpz_manager::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 diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h index 36715facf..cf7cdff05 100644 --- a/src/util/obj_hashtable.h +++ b/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(); } diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index 28656bc63..3a3cdbc87 100644 --- a/src/util/rlimit.cpp +++ b/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); } diff --git a/src/util/warning.cpp b/src/util/warning.cpp index 033c93780..c7becf49f 100644 --- a/src/util/warning.cpp +++ b/src/util/warning.cpp @@ -24,6 +24,10 @@ Revision History: #include "util/buffer.h" #include "util/vector.h" +#ifndef SINGLE_THREAD +#include +#endif + #ifdef _WINDOWS #if defined( __MINGW32__ ) && ( defined( __GNUG__ ) || defined( __clang__ ) ) #include @@ -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 lock(g_warning_mutex); +#endif va_list args; va_start(args, msg); print_msg(g_warning_stream, "WARNING: ", msg, args); diff --git a/z3test b/z3test deleted file mode 160000 index 4186a4bf4..000000000 --- a/z3test +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 4186a4bf47b920d50671c396f904fe69e3e5c41d