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

.github/workflows/android-build.yml

@@ -27,7 +27,7 @@ jobs:
       run:  |
         mkdir build
         cd build
-        cmake -DCMAKE_BUILD_TYPE=${{ env.BUILD_TYPE }} -DCMAKE_SYSTEM_NAME=Android -DCMAKE_SYSTEM_VERSION=21 -DCMAKE_ANDROID_ARCH_ABI=${{ matrix.android-abi }} "-DCMAKE_ANDROID_NDK=$ANDROID_NDK_LATEST_HOME" -DZ3_BUILD_JAVA_BINDINGS=TRUE -G "Unix Makefiles" -DJAVA_AWT_LIBRARY=NotNeeded -DJAVA_JVM_LIBRARY=NotNeeded -DJAVA_INCLUDE_PATH2=NotNeeded -DJAVA_AWT_INCLUDE_PATH=NotNeeded ../
+        cmake -DCMAKE_BUILD_TYPE=${{ env.BUILD_TYPE }} -DCMAKE_SYSTEM_NAME=Android -DCMAKE_ANDROID_API=21 -DCMAKE_ANDROID_ARCH_ABI=${{ matrix.android-abi }} "-DCMAKE_ANDROID_NDK=$ANDROID_NDK_LATEST_HOME" -DZ3_BUILD_JAVA_BINDINGS=TRUE -G "Unix Makefiles" ../
         make -j $(nproc)
         tar -cvf z3-build-${{ matrix.android-abi }}.tar *.jar *.so
 

scripts/mk_genfile_common.py

@@ -886,8 +886,7 @@ def def_module_params(module_name, export, params, class_name=None, description=
         hpp = os.path.join(dirname, '%s.hpp' % class_name)
         out = open(hpp, 'w')
         out.write('// Automatically generated file\n')
-        out.write('#ifndef __%s_HPP_\n' % class_name.upper())
-        out.write('#define __%s_HPP_\n' % class_name.upper())
+        out.write('#pragma once\n')
         out.write('#include "util/params.h"\n')
         if export:
             out.write('#include "util/gparams.h"\n')
@@ -919,7 +918,6 @@ def def_module_params(module_name, export, params, class_name=None, description=
                 out.write('  %s %s() const { return p.%s("%s", %s); }\n' %
                           (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param)))
         out.write('};\n')
-        out.write('#endif\n')
         out.close()
         OUTPUT_HPP_FILE.append(hpp)
 

src/api/dotnet/Context.cs

@@ -124,7 +124,7 @@ public StringSymbol MkSymbol(string name)
         /// </summary>
         internal Symbol[] MkSymbols(string[] names)
         {
-            if (names == null) return null;
+            if (names == null) return new Symbol[0];
             Symbol[] result = new Symbol[names.Length];
             for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
             return result;

src/api/java/Context.java

@@ -110,7 +110,7 @@ public StringSymbol mkSymbol(String name)
     Symbol[] mkSymbols(String[] names)
     {
         if (names == null)
-            return null;
+            return new Symbol[0];
         Symbol[] result = new Symbol[names.length];
         for (int i = 0; i < names.length; ++i)
             result[i] = mkSymbol(names[i]);

src/api/js/src/high-level/high-level.test.ts

@@ -8,7 +8,7 @@ import { Arith, Bool, Model, Z3AssertionError, Z3HighLevel } from './types';
  *
  * **NOTE**: The set of solutions might be infinite.
  * Always ensure to limit amount generated, either by knowing that the
- * solution space is constrainted, or by taking only a specified
+ * solution space is constrained, or by taking only a specified
  * amount of solutions
  * ```typescript
  * import { sliceAsync } from 'iter-tools';
@@ -46,7 +46,7 @@ async function* allSolutions<Name extends string>(...assertions: Bool<Name>[]):
           .filter(decl => decl.arity() === 0)
           .map(decl => {
             const term = decl.call();
-            // TODO(ritave): Assert not an array / uinterpeted sort
+            // TODO(ritave): Assert not an array / uninterpreted sort
             const value = model.eval(term, true);
             return term.neq(value);
           }),

src/api/js/src/high-level/high-level.ts

@@ -224,6 +224,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
     function _toExpr(ast: Z3_ast): Bool<Name> | IntNum<Name> | RatNum<Name> | Arith<Name> | Expr<Name> {
       const kind = check(Z3.get_ast_kind(contextPtr, ast));
       if (kind === Z3_ast_kind.Z3_QUANTIFIER_AST) {
+        if (Z3.is_quantifier_forall(contextPtr, ast))
+           return new BoolImpl(ast);
+        if (Z3.is_quantifier_exists(contextPtr, ast))
+           return new BoolImpl(ast);
+        if (Z3.is_lambda(contextPtr, ast))
+           return new ExprImpl(ast);
         assert(false);
       }
       const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast)));

src/api/js/src/high-level/types.ts

@@ -617,7 +617,7 @@ export interface Arith<Name extends string = 'main'> extends Expr<Name, ArithSor
    */
   mul(other: Arith<Name> | number | bigint | string): Arith<Name>;
   /**
-   * Substract second number from the first one
+   * Subtract second number from the first one
    */
   sub(other: Arith<Name> | number | bigint | string): Arith<Name>;
   /**
@@ -709,7 +709,7 @@ export interface RatNum<Name extends string = 'main'> extends Arith<Name> {
 }
 
 /**
- * A Sort represting Bit Vector numbers of specified {@link BitVecSort.size size}
+ * A Sort representing Bit Vector numbers of specified {@link BitVecSort.size size}
  *
  * @typeParam Bits - A number representing amount of bits for this sort
  * @category Bit Vectors
@@ -878,42 +878,42 @@ export interface BitVec<Bits extends number = number, Name extends string = 'mai
 
   /**
    * Creates a signed less-or-equal operation (`<=`)
-   * @category Comparision
+   * @category Comparison
    */
   sle(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
   /**
    * Creates an unsigned less-or-equal operation (`<=`)
-   * @category Comparision
+   * @category Comparison
    */
   ule(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
   /**
    * Creates a signed less-than operation (`<`)
-   * @category Comparision
+   * @category Comparison
    */
   slt(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
   /**
    * Creates an unsigned less-than operation (`<`)
-   * @category Comparision
+   * @category Comparison
    */
   ult(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
   /**
    * Creates a signed greater-or-equal operation (`>=`)
-   * @category Comparision
+   * @category Comparison
    */
   sge(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
   /**
    * Creates an unsigned greater-or-equal operation (`>=`)
-   * @category Comparision
+   * @category Comparison
    */
   uge(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
   /**
    * Creates a signed greater-than operation (`>`)
-   * @category Comparision
+   * @category Comparison
    */
   sgt(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
   /**
    * Creates an unsigned greater-than operation (`>`)
-   * @category Comparision
+   * @category Comparison
    */
   ugt(other: CoercibleToBitVec<Bits, Name>): Bool<Name>;
 

src/api/ml/README.md

@@ -39,7 +39,7 @@ $ ldd ./run
         /lib64/ld-linux-x86-64.so.2 (0x00007fb570de9000)
 ```
 
-The bytecode version will have a depedency on z3 and other external
+The bytecode version will have a dependency on z3 and other external
 libraries (packed as dlls and usually installed in opam switch):
 ```
 $ ocamlobjinfo run | grep 'Used DLL' -A5
@@ -126,7 +126,7 @@ Using Dynlink
 -------------
 
 The built z3ml.cmxs file is a self-contained shared library that
-doesn't have any depndencies on z3 (the z3 code is included in it) and
+doesn't have any dependencies on z3 (the z3 code is included in it) and
 could be loaded with `Dynlink.loadfile` in runtime.
 
 Installation

src/ast/array_decl_plugin.h

@@ -178,6 +178,7 @@ class array_recognizers {
     bool is_default(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_DEFAULT); }
     bool is_subset(expr const* n) const { return is_app_of(n, m_fid, OP_SET_SUBSET); }
     bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); }
+    bool is_map(func_decl* f, func_decl*& g) const { return is_map(f) && (g = get_map_func_decl(f), true); }
     func_decl * get_as_array_func_decl(expr * n) const;
     func_decl * get_as_array_func_decl(func_decl* f) const;
     func_decl * get_map_func_decl(func_decl* f) const;

src/ast/macros/macro_finder.cpp

@@ -376,7 +376,17 @@ bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vect
     return found_new_macro;
 }
 
+void macro_finder::revert_unsafe_macros(vector<justified_expr>& new_fmls) {
+    auto& unsafe_macros = m_macro_manager.unsafe_macros();
+    for (auto* f : unsafe_macros) {
+        quantifier* q = m_macro_manager.get_macro_quantifier(f);
+        new_fmls.push_back(justified_expr(m, q, nullptr));
+    }
+    unsafe_macros.reset();
+}
+
 void macro_finder::operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls) {
+    m_macro_manager.unsafe_macros().reset();
     TRACE("macro_finder", tout << "processing macros...\n";);
     vector<justified_expr> _new_fmls;
     if (expand_macros(n, fmls, _new_fmls)) {
@@ -388,6 +398,7 @@ void macro_finder::operator()(unsigned n, justified_expr const* fmls, vector<jus
                 break;
         }
     }
+    revert_unsafe_macros(_new_fmls);
     new_fmls.append(_new_fmls);
 }
 

src/ast/macros/macro_finder.h

@@ -39,6 +39,8 @@ class macro_finder {
 
     bool is_macro(expr * n, app_ref & head, expr_ref & def);
 
+    void revert_unsafe_macros(vector<justified_expr>& new_fmls);
+
 public:
     macro_finder(ast_manager & m, macro_manager & mm);
     ~macro_finder();

src/ast/macros/macro_manager.cpp

@@ -241,12 +241,14 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
 struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
     ast_manager& m; 
     macro_manager& mm;
+    array_util a;
     expr_dependency_ref m_used_macro_dependencies; 
     expr_ref_vector m_trail;
 
     macro_expander_cfg(ast_manager& m, macro_manager& mm):
         m(m),
         mm(mm),
+        a(m),
         m_used_macro_dependencies(m),
         m_trail(m)
     {}
@@ -296,7 +298,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
             return false;
         app * n = to_app(_n);
         quantifier * q = nullptr;
-        func_decl * d  = n->get_decl();
+        func_decl * d  = n->get_decl(), *d2 = nullptr;
         TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
         if (mm.m_decl2macro.find(d, q)) {            
             app * head = nullptr;
@@ -343,6 +345,12 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
             m_used_macro_dependencies = m.mk_join(m_used_macro_dependencies, ed); 
             return true;
         }
+        else if (a.is_as_array(d, d2) && mm.m_decl2macro.find(d2, q)) {
+            mm.unsafe_macros().insert(d2);
+        }
+        else if (a.is_map(d, d2) && mm.m_decl2macro.find(d2, q)) {
+            mm.unsafe_macros().insert(d2);
+        }
         return false;
     }
 };

src/ast/macros/macro_manager.h

@@ -47,6 +47,7 @@ class macro_manager {
     expr_dependency_ref_vector       m_macro_deps;
     obj_hashtable<func_decl>         m_forbidden_set;
     func_decl_ref_vector             m_forbidden;
+    obj_hashtable<func_decl>         m_unsafe_macros;
     struct scope {
         unsigned m_decls_lim;
         unsigned m_forbidden_lim;
@@ -86,7 +87,7 @@ class macro_manager {
     quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = nullptr; m_decl2macro.find(f, q); return q; }
     void get_head_def(quantifier * q, func_decl * d, app * & head, expr_ref & def, bool& revert) const;
     void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep);
-
+    obj_hashtable<func_decl>& unsafe_macros() { return m_unsafe_macros; }
 
 };
 

src/math/interval/dep_intervals.cpp

@@ -7,7 +7,7 @@
 
   Abstract:
 
-    intervals with depedency tracking.
+    intervals with dependency tracking.
 
   Author:
   Nikolaj Bjorner (nbjorner)

src/math/interval/dep_intervals.h

@@ -7,7 +7,7 @@
 
   Abstract:
 
-    intervals with depedency tracking.
+    intervals with dependency tracking.
 
   Author:
   Nikolaj Bjorner (nbjorner)

src/math/lp/lar_solver.h

@@ -93,7 +93,7 @@ class lar_solver : public column_namer {
     unsigned_vector                                     m_row_bounds_to_replay;
 
     u_set                                               m_basic_columns_with_changed_cost;
-    // these are basic columns with the value changed, so the the corresponding row in the tableau
+    // these are basic columns with the value changed, so the corresponding row in the tableau
     // does not sum to zero anymore
     u_set                                               m_incorrect_columns;
     // copy of m_r_solver.inf_set()

src/muz/fp/dl_cmds.cpp

@@ -226,7 +226,7 @@ class dl_query_cmd : public parametric_cmd {
     void set_next_arg(cmd_context & ctx, func_decl* t) override {
         m_target = t;
         if (t->get_family_id() != null_family_id) {
-            throw cmd_exception("Invalid query argument, expected uinterpreted function name, but argument is interpreted");
+            throw cmd_exception("Invalid query argument, expected uninterpreted function name, but argument is interpreted");
         }
         datalog::context& dlctx = m_dl_ctx->dlctx();
         if (!dlctx.get_predicates().contains(t)) {

src/muz/transforms/dl_mk_slice.cpp

@@ -25,7 +25,7 @@ Revision History:
     Let x_i, y_i, z_i be indices into the vectors x, y, z.
 
     Suppose that positions in P and R are annotated with what is
-    slicable.
+    sliceable.
 
     Sufficient conditions for sliceability:
 
@@ -43,9 +43,9 @@ Revision History:
       and the positions where z_i is used in P and R are sliceable
 
 
-    A more refined approach may be using Gaussean elimination based
+    A more refined approach may be using Gaussian elimination based
     on x,z and eliminating variables from x,y (expressing them in terms
-    of a disjoint subeset of x,z).
+    of a disjoint subset of x,z).
 
 
 --*/
@@ -441,7 +441,7 @@ namespace datalog {
 
     void mk_slice::filter_unique_vars(rule& r) {
         // 
-        // Variables that occur in multiple uinterpreted predicates are not sliceable.
+        // Variables that occur in multiple uninterpreted predicates are not sliceable.
         // 
         uint_set used_vars;
         for (unsigned j = 0; j < r.get_uninterpreted_tail_size(); ++j) {

src/sat/sat_solver.h

@@ -527,20 +527,21 @@ namespace sat {
 
         unsigned m_conflicts_since_init { 0 };
         unsigned m_restarts { 0 };
-        unsigned m_restart_next_out { 0 };
-        unsigned m_conflicts_since_restart { 0 };
-        bool     m_force_conflict_analysis { false };
-        unsigned m_simplifications { 0 };
-        unsigned m_restart_threshold { 0 };
-        unsigned m_luby_idx { 0 };
-        unsigned m_conflicts_since_gc { 0 };
-        unsigned m_gc_threshold { 0 };
-        unsigned m_defrag_threshold { 0 };
-        unsigned m_num_checkpoints { 0 };
-        double   m_min_d_tk { 0 } ;
-        unsigned m_next_simplify { 0 };
-        bool     m_simplify_enabled { true };
-        bool     m_restart_enabled { true };
+        unsigned m_restart_next_out = 0;
+        unsigned m_conflicts_since_restart = 0;
+        bool     m_force_conflict_analysis = false;
+        unsigned m_simplifications = 0;
+        unsigned m_restart_threshold = 0;
+        unsigned m_luby_idx = 0;
+        unsigned m_conflicts_since_gc = 0;
+        unsigned m_gc_threshold = 0;
+        unsigned m_defrag_threshold = 0;
+        unsigned m_num_checkpoints = 0;
+        double   m_min_d_tk = 0.0 ;
+        unsigned m_next_simplify = 0;
+        double   m_simplify_mult = 1.5;
+        bool     m_simplify_enabled = true;
+        bool     m_restart_enabled = true;
         bool guess(bool_var next);
         bool decide();
         bool_var next_var();
@@ -713,7 +714,6 @@ namespace sat {
         //
         // -----------------------
     public:
-        void set_should_simplify() { m_next_simplify = m_conflicts_since_init; }
         bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit;  }
         bool is_probing() const { return m_is_probing; }
         bool is_free(bool_var v) const { return m_free_vars.contains(v); }