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

.github/workflows/android-build.yml

@@ -21,7 +21,7 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
 
     - name: Configure CMake and build
       run:  |

.github/workflows/coverage.yml

@@ -21,7 +21,7 @@ jobs:
       COV_DETAILS_PATH: ${{github.workspace}}/cov-details
 
     steps:
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
 
     - name: Setup
       run: |

.github/workflows/cross-build.yml

@@ -19,7 +19,7 @@ jobs:
 
     steps:
     - name: Checkout code
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
 
     - name: Install cross build tools
       run:  apt update && apt install -y ninja-build cmake python3 g++-11-${{ matrix.arch }}-linux-gnu

.github/workflows/docker-image.yml

@@ -15,10 +15,10 @@ jobs:
 
     steps:
       - name: Check out the repo        
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Log in to GitHub Docker registry
-        uses: docker/login-action@v2
+        uses: docker/login-action@v3
         with:
           registry: ghcr.io
           username: ${{ secrets.DOCKER_USERNAME }}
@@ -29,7 +29,7 @@ jobs:
       # -------
       - name: Extract metadata (tags, labels) for Bare Z3 Docker Image
         id: meta
-        uses: docker/metadata-action@v4
+        uses: docker/metadata-action@v5
         with:
           images: ghcr.io/z3prover/z3
           flavor: |
@@ -41,7 +41,7 @@ jobs:
             type=edge
             type=sha,prefix=ubuntu-20.04-bare-z3-sha-
       - name: Build and push Bare Z3 Docker Image
-        uses: docker/build-push-action@v4.1.1
+        uses: docker/build-push-action@v5.0.0
         with:  
           context: .
           push: true

.github/workflows/msvc-static-build.yml

@@ -14,7 +14,7 @@ jobs:
       BUILD_TYPE: Release
     steps:
     - name: Checkout Repo
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
   
     - name: Build
       run: |

.github/workflows/wasm-release.yml

@@ -21,7 +21,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup node
         uses: actions/setup-node@v3

.github/workflows/wasm.yml

@@ -21,7 +21,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Setup node
         uses: actions/setup-node@v3

.github/workflows/wip.yml

@@ -15,7 +15,7 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-    - uses: actions/checkout@v3
+    - uses: actions/checkout@v4
 
     - name: Configure CMake
       run: cmake -B ${{github.workspace}}/build -DCMAKE_BUILD_TYPE=${{env.BUILD_TYPE}}

scripts/mk_util.py

@@ -2519,19 +2519,19 @@ def mk_config():
                 'SLINK_FLAGS=/nologo /LDd\n' % static_opt)
             if VS_X64:
                 config.write(
-                    'CXXFLAGS=/c %s /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
-                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
+                    'LINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
+                    'SLINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
             elif VS_ARM:
                 print("ARM on VS is unsupported")
                 exit(1)
             else:
                 config.write(
-                    'CXXFLAGS=/c %s /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 /arch:SSE2 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=/c %s /Zi /W3 /WX- /Od /Oy- /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /Gm- /RTC1 /arch:SSE2 %s %s\n' % (CXXFLAGS, extra_opt, static_opt))
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
-                    'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
+                    'LINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
+                    'SLINK_EXTRA_FLAGS=/link /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
         else:
             # Windows Release mode
             LTCG=' /LTCG' if SLOW_OPTIMIZE else ''
@@ -2544,19 +2544,19 @@ def mk_config():
                 extra_opt = '%s /D _TRACE ' % extra_opt
             if VS_X64:
                 config.write(
-                    'CXXFLAGS=/c%s %s /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D NDEBUG /D _LIB /D UNICODE /Gm- /GF /Gy /TP %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=/c%s %s /Zi /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D NDEBUG /D _LIB /D UNICODE /Gm- /GF /Gy /TP %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /STACK:8388608 %s\n'
-                    'SLINK_EXTRA_FLAGS=/link%s /profile /MACHINE:X64 /SUBSYSTEM:WINDOWS /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt))
+                    'LINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /STACK:8388608 %s\n'
+                    'SLINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /profile /MACHINE:X64 /SUBSYSTEM:WINDOWS /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt))
             elif VS_ARM:
                 print("ARM on VS is unsupported")
                 exit(1)
             else:
                 config.write(
-                    'CXXFLAGS=/c%s %s /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D NDEBUG /D _CONSOLE /D ASYNC_COMMANDS /Gm- /arch:SSE2 %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
+                    'CXXFLAGS=/c%s %s /Zi /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D NDEBUG /D _CONSOLE /D ASYNC_COMMANDS /Gm- /arch:SSE2 %s %s\n' % (GL, CXXFLAGS, extra_opt, static_opt))
                 config.write(
-                    'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
-                    'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt))
+                    'LINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
+                    'SLINK_EXTRA_FLAGS=/link%s /PROFILE /DEBUG:full /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt))
 
         config.write('CFLAGS=$(CXXFLAGS)\n')
 

scripts/update_api.py

@@ -1887,10 +1887,10 @@ if _lib is None:
   print("  - to the custom Z3_LIB_DIRS Python-builtin before importing the z3 module, e.g. via")
   if sys.version < '3':
     print("    import __builtin__")
-    print("    __builtin__.Z3_LIB_DIRS = [ '/path/to/libz3.%s' ] " % _ext)
+    print("    __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] \# directory containing libz3.%s" % _ext)
   else:
     print("    import builtins")
-    print("    builtins.Z3_LIB_DIRS = [ '/path/to/libz3.%s' ] " % _ext)
+    print("    builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] \# directory containing libz3.%s" % _ext)
   print(_failures)
   raise Z3Exception("libz3.%s not found." % _ext)
 

src/api/api_context.cpp

@@ -157,6 +157,9 @@ namespace api {
         flush_objects();
         for (auto& kv : m_allocated_objects) {
             api::object* val = kv.m_value;
+#ifdef SINGLE_THREAD
+# define m_concurrent_dec_ref false
+#endif
             DEBUG_CODE(if (!m_concurrent_dec_ref) warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name()););
             dealloc(val);
         }

src/ast/converters/model_converter.cpp

@@ -24,7 +24,8 @@ Notes:
  * Add or overwrite value in model.
  */
 void model_converter::display_add(std::ostream& out, smt2_pp_environment& env, ast_manager& m, func_decl* f, expr* e) {
-    VERIFY(e);
+    if (!e)
+        return;
     VERIFY(f->get_range() == e->get_sort());
     ast_smt2_pp_rev(out, f, e, env, params_ref(), 0, "model-add") << "\n";
 }

src/ast/normal_forms/elim_term_ite.cpp

@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include "ast/normal_forms/elim_term_ite.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/rewriter/rewriter_def.h"
 
 br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const* args, expr_ref& result, proof_ref& result_pr) {
     if (!m.is_term_ite(f)) {
@@ -38,3 +39,4 @@ br_status elim_term_ite_cfg::reduce_app(func_decl* f, unsigned n, expr * const*
     return BR_DONE;
 }
 
+template class rewriter_tpl<elim_term_ite_cfg>;

src/ast/pattern/pattern_inference.cpp

@@ -624,9 +624,11 @@ bool pattern_inference_cfg::reduce_quantifier(
     proof_ref & result_pr) {
 
     TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";);
-    if (!is_forall(q)) {
+    if (!m_params.m_pi_enabled)
+        return false;
+
+    if (!is_forall(q)) 
         return false;
-    }
 
     int weight = q->get_weight();
 
@@ -653,9 +655,8 @@ bool pattern_inference_cfg::reduce_quantifier(
         }
     }
 
-    if (q->get_num_patterns() > 0) {
+    if (q->get_num_patterns() > 0) 
         return false;
-    }
 
     if (m_params.m_pi_nopat_weight >= 0)
         weight = m_params.m_pi_nopat_weight;

src/ast/rewriter/rewriter.cpp

@@ -17,6 +17,8 @@ Notes:
 
 --*/
 #include "ast/rewriter/rewriter_def.h"
+#include "ast/rewriter/push_app_ite.h"
+#include "ast/rewriter/elim_bounds.h"
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_smt2_pp.h"
@@ -417,3 +419,6 @@ void inv_var_shifter::process_var(var * v) {
 }
     
 template class rewriter_tpl<beta_reducer_cfg>;
+template class rewriter_tpl<ng_push_app_ite_cfg>;
+template class rewriter_tpl<push_app_ite_cfg>;
+template class rewriter_tpl<elim_bounds_cfg>;

src/ast/rewriter/seq_rewriter.cpp

@@ -1716,6 +1716,10 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
         result = m_autil.mk_numeral(rational(idx), true);
         return BR_DONE;
     }
+    if (a == b) {
+        result = m_autil.mk_int(0);
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
 

src/ast/simplifiers/solve_context_eqs.cpp

@@ -243,8 +243,8 @@ namespace euf {
 
     void solve_context_eqs::collect_nested_equalities(dependent_expr const& df, expr_mark& visited, dep_eq_vector& eqs) {
 
-        svector<std::tuple<bool,unsigned,expr*>> todo;
-        todo.push_back({ false, 0, df.fml()});
+        svector<std::tuple<bool,unsigned,expr*, unsigned>> todo;
+        todo.push_back({ false, 0, df.fml(), 0});
 
         // even depth is conjunctive context, odd is disjunctive
         // when alternating between conjunctive and disjunctive context, increment depth.
@@ -255,37 +255,85 @@ namespace euf {
             return (0 == depth % 2) ? depth : depth + 1;
         };
 
-        while (!todo.empty()) {
-            auto [s, depth, f] = todo.back();
-            todo.pop_back();
+        for (unsigned i = 0; i < todo.size(); ++i) {
+            auto [s, depth, f, p] = todo[i];
             if (visited.is_marked(f))
                 continue;
             visited.mark(f, true);
             if (s && m.is_and(f)) {
                 for (auto* arg : *to_app(f))
-                    todo.push_back({ s, inc_or(depth), arg });
+                    todo.push_back({ s, inc_or(depth), arg, i });
             }
             else if (!s && m.is_or(f)) {
                 for (auto* arg : *to_app(f))
-                    todo.push_back({ s, inc_or(depth), arg });
+                    todo.push_back({ s, inc_or(depth), arg, i });
             }
             if (!s && m.is_and(f)) {
                 for (auto* arg : *to_app(f))
-                    todo.push_back({ s, inc_and(depth), arg });
+                    todo.push_back({ s, inc_and(depth), arg, i });
             }
             else if (s && m.is_or(f)) {
                 for (auto* arg : *to_app(f))
-                    todo.push_back({ s, inc_and(depth), arg });
+                    todo.push_back({ s, inc_and(depth), arg, i });
             }
             else if (m.is_not(f, f))
-                todo.push_back({ !s, depth, f });
+                todo.push_back({ !s, depth, f, i });
             else if (!s && 1 <= depth) {
+                unsigned sz = eqs.size();
                 for (extract_eq* ex : m_solve_eqs.m_extract_plugins) {
                     ex->set_allow_booleans(false);
                     ex->get_eqs(dependent_expr(m, f, nullptr, df.dep()), eqs);
                     ex->set_allow_booleans(true);
                 }
+                // prune eqs for solutions that are not safe in df.fml()
+                for (; sz < eqs.size(); ++sz) {
+                    if (!is_safe_var(eqs[sz].var, i, df.fml(), todo)) {
+                        eqs[sz] = eqs.back();
+                        --sz;
+                        eqs.pop_back();
+                    }
+                }
             }
         }
     }
+    
+    bool solve_context_eqs::is_safe_var(expr* x, unsigned i, expr* f, svector<std::tuple<bool,unsigned,expr*,unsigned>> const& todo) {
+        m_contains_v.reset();
+        m_todo.push_back(f);
+        mark_occurs(m_todo, x, m_contains_v);
+        SASSERT(m_todo.empty());
+
+        auto is_parent = [&](unsigned p, unsigned i) {
+            while (p != i && i != 0) {
+                auto [_s,_depth, _f, _p] = todo[i];
+                i = _p;
+            }
+            return p == i;
+        };
+
+        // retrieve oldest parent of i within the same alternation of and
+        unsigned pi = i;
+        auto [_s, _depth, _f, _p] = todo[i];
+        while (pi != 0) {
+            auto [s, depth, f, p] = todo[pi];
+            if (depth != _depth)
+                break;
+            pi = p;
+        }
+        
+        // determine if j and j have common conjunctive parent
+        // for every j in todo.
+        for (unsigned j = 0; j < todo.size(); ++j) {
+            auto [s, depth, f, p] = todo[j];
+            if (i == j || !m_contains_v.is_marked(f))
+                continue;
+            if (is_parent(j, i)) // j is a parent if i
+                continue;
+            if (is_parent(pi, j)) // pi is a parent of j
+                continue;
+            return false;
+        }
+        return true;
+    }
+
 }

src/ast/simplifiers/solve_context_eqs.h

@@ -45,7 +45,9 @@ namespace euf {
         bool contains_conjunctively(expr* f, bool sign, expr* e, signed_expressions& conjuncts);
         bool is_conjunction(bool sign, expr* f) const;
         
-        void collect_nested_equalities(dependent_expr const& f, expr_mark& visited, dep_eq_vector& eqs);        
+        void collect_nested_equalities(dependent_expr const& f, expr_mark& visited, dep_eq_vector& eqs);
+
+        bool is_safe_var(expr* x, unsigned i, expr* f, svector<std::tuple<bool,unsigned,expr*,unsigned>> const& todo);
 
     public:
         

src/math/lp/lp_bound_propagator.h

@@ -9,29 +9,18 @@
 #include "math/lp/lp_settings.h"
 #include "util/uint_set.h"
 #include "math/lp/implied_bound.h"
-#include <vector>
+#include "util/vector.h"
 namespace lp {
-template <typename T>
-struct my_allocator {
-    using value_type = T;
-
-    T* allocate(std::size_t n) {
-        return static_cast<T*>(memory::allocate(n * sizeof(T)));
-    }
-
-    void deallocate(T* p, std::size_t n) {
-        memory::deallocate(p);
-    }
-};    
+    
 template <typename T>
 class lp_bound_propagator {
-	uint_set m_visited_rows;
+    uint_set m_visited_rows;
     // these maps map a column index to the corresponding index in ibounds
     u_map<unsigned> m_improved_lower_bounds;
     u_map<unsigned> m_improved_upper_bounds;
 
     T& m_imp;
-    std::vector<implied_bound, my_allocator<implied_bound>> m_ibounds;
+    std_vector<implied_bound> m_ibounds;
 
     map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_val2fixed_row;
     // works for rows of the form x + y + sum of fixed = 0
@@ -119,10 +108,10 @@ private:
         ~reset_cheap_eq() { p.reset_cheap_eq_eh(); }
     };
 
-   public:
+public:
     lp_bound_propagator(T& imp) : m_imp(imp) {}
 
-    const std::vector<implied_bound, my_allocator<implied_bound>>& ibounds() const { return m_ibounds; }
+    const std_vector<implied_bound>& ibounds() const { return m_ibounds; }
 
     void init() {
         m_improved_upper_bounds.reset();
@@ -192,13 +181,12 @@ private:
 
     void propagate_monic(lpvar monic_var, const svector<lpvar>& vars) {
        lpvar non_fixed, zero_var;
-       if (!is_linear(vars, zero_var, non_fixed)) {
-            return;
-       }
+       if (!is_linear(vars, zero_var, non_fixed)) 
+           return;
 
-       if (zero_var != null_lpvar) {
+       if (zero_var != null_lpvar) 
             add_bounds_for_zero_var(monic_var, zero_var);
-       } else {
+       else {
             rational k = rational(1);
             for (auto v : vars)
                 if (v != non_fixed) {
@@ -206,19 +194,18 @@ private:
                     if (k.is_big()) return;
                 }
 
-            if (non_fixed != null_lpvar) {
+            if (non_fixed != null_lpvar) 
                 propagate_monic_with_non_fixed(monic_var, vars, non_fixed, k);
-            } else {  // all variables are fixed
+            else   // all variables are fixed
                 propagate_monic_with_all_fixed(monic_var, vars, k);
-            }
        }
     }
 
     void propagate_monic_with_non_fixed(lpvar monic_var, const svector<lpvar>& vars, lpvar non_fixed, const rational& k) {
-       lp::impq bound_value;
-       bool is_strict;
+        lp::impq bound_value;
+        bool is_strict;
 
-       if (lower_bound_is_available(non_fixed)) {
+        if (lower_bound_is_available(non_fixed)) {
             bound_value = lp().column_lower_bound(non_fixed);
             is_strict = !bound_value.y.is_zero();
             auto lambda = [vars, non_fixed](int* s) {

src/math/lp/nla_monotone_lemmas.h

@@ -7,16 +7,14 @@
   --*/
 #pragma once
 namespace nla {
-class core;
-class monotone : common {    
-public:
-    monotone(core *core);
-    void monotonicity_lemma();
-private:
-    void monotonicity_lemma(monic const& m);
-    void monotonicity_lemma_gt(const monic& m);    
-    void monotonicity_lemma_lt(const monic& m);
-    std::vector<rational> get_sorted_key(const monic& rm) const;
-    vector<std::pair<rational, lpvar>> get_sorted_key_with_rvars(const monic& a) const;
-};
+    class core;
+    class monotone : common {    
+    public:
+        monotone(core *core);
+        void monotonicity_lemma();
+    private:
+        void monotonicity_lemma(monic const& m);
+        void monotonicity_lemma_gt(const monic& m);    
+        void monotonicity_lemma_lt(const monic& m);
+    };
 }

src/params/pattern_inference_params.cpp

@@ -21,6 +21,7 @@ Revision History:
 
 void pattern_inference_params::updt_params(params_ref const & _p) {
     pattern_inference_params_helper p(_p);
+    m_pi_enabled                 = p.enabled();
     m_pi_max_multi_patterns      = p.max_multi_patterns();
     m_pi_block_loop_patterns     = p.block_loop_patterns();
     m_pi_decompose_patterns      = p.decompose_patterns();
@@ -35,6 +36,7 @@ void pattern_inference_params::updt_params(params_ref const & _p) {
 #define DISPLAY_PARAM(X) out << #X"=" << X << '\n';
 
 void pattern_inference_params::display(std::ostream & out) const {
+    DISPLAY_PARAM(m_pi_enabled);
     DISPLAY_PARAM(m_pi_max_multi_patterns);
     DISPLAY_PARAM(m_pi_block_loop_patterns);
     DISPLAY_PARAM(m_pi_decompose_patterns);

src/params/pattern_inference_params.h

@@ -27,7 +27,8 @@ enum arith_pattern_inference_kind {
 };
 
 struct pattern_inference_params {
-    unsigned                      m_pi_max_multi_patterns; 
+    bool                          m_pi_enabled = true;
+    unsigned                      m_pi_max_multi_patterns = 1; 
     bool                          m_pi_block_loop_patterns; 
     bool                          m_pi_decompose_patterns;
     arith_pattern_inference_kind  m_pi_arith;
@@ -35,13 +36,11 @@ struct pattern_inference_params {
     unsigned                      m_pi_arith_weight;
     unsigned                      m_pi_non_nested_arith_weight;
     bool                          m_pi_pull_quantifiers;
-    int                           m_pi_nopat_weight;
-    bool                          m_pi_avoid_skolems;
+    int                           m_pi_nopat_weight = -1;
+    bool                          m_pi_avoid_skolems = true;
     bool                          m_pi_warnings;
     
-    pattern_inference_params(params_ref const & p = params_ref()):
-        m_pi_nopat_weight(-1),
-        m_pi_avoid_skolems(true) {
+    pattern_inference_params(params_ref const & p = params_ref()) {
         updt_params(p);
     }
 

src/params/pattern_inference_params_helper.pyg

@@ -7,6 +7,7 @@ def_module_params(class_name='pattern_inference_params_helper',
                           ('decompose_patterns', BOOL, True, 'allow decomposition of patterns into multipatterns'),
                           ('arith', UINT, 1, '0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms'),
                           ('use_database', BOOL, False, 'use pattern database'),
+                          ('enabled', BOOL, True, 'enable a heuristic to infer patterns, when they are not provided'),	
                           ('arith_weight', UINT, 5, 'default weight for quantifiers where the only available pattern has nested arithmetic terms'),
                           ('non_nested_arith_weight', UINT, 10, 'default weight for quantifiers where the only available pattern has non nested arithmetic terms'),
                           ('pull_quantifiers', BOOL, True, 'pull nested quantifiers, if no pattern was found'),

src/parsers/smt2/smt2parser.cpp

@@ -963,6 +963,7 @@ namespace smt2 {
             unsigned line = m_scanner.get_line();
             unsigned pos  = m_scanner.get_pos();
             symbol dt_name = curr_id();
+            check_identifier("unexpected token used as datatype name");
             next();
 
             m_dt_name2idx.reset();

src/smt/theory_lra.cpp

@@ -2176,7 +2176,8 @@ public:
         if (is_infeasible()) {
             get_infeasibility_explanation_and_set_conflict();
             // verbose_stream() << "unsat\n";
-        } else {
+        }
+        else {
             for (auto &ib : m_bp.ibounds()) {
                 m.inc();
                 if (ctx().inconsistent())

src/solver/simplifier_solver.cpp

@@ -110,12 +110,13 @@ class simplifier_solver : public solver {
         expr_ref_vector orig_assumptions(assumptions);
         m_core_replace.reset();
         if (qhead < m_fmls.size() || !assumptions.empty()) {
-            TRACE("solver", tout << "qhead " << qhead << "\n");
             m_preprocess_state.replay(qhead, assumptions);   
             m_preprocess_state.freeze(assumptions);
             m_preprocess.reduce();
             if (!m.inc())
                 return;
+            TRACE("solver", tout << "qhead " << qhead << "\n";
+                  m_preprocess_state.display(tout));
             m_preprocess_state.advance_qhead();
             for (unsigned i = 0; i < assumptions.size(); ++i) 
                 m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i));            

src/util/memory_manager.h

@@ -128,6 +128,19 @@ void dealloc_svect(T * ptr) {
     memory::deallocate(ptr);
 }
 
+template <typename T>
+struct std_allocator {
+    using value_type = T;
+
+    T* allocate(std::size_t n) {
+        return static_cast<T*>(memory::allocate(n * sizeof(T)));
+    }
+
+    void deallocate(T* p, std::size_t n) {
+        memory::deallocate(p);
+    }
+};
+
 struct mem_stat {
 };
 

src/util/vector.h

@@ -33,6 +33,7 @@ Revision History:
 #include "util/memory_manager.h"
 #include "util/hash.h"
 #include "util/z3_exception.h"
+#include <vector>
 
 // disable warning for constant 'if' expressions.
 // these are used heavily in templates.
@@ -40,6 +41,8 @@ Revision History:
 #pragma warning(disable:4127)
 #endif
 
+template <typename T>
+class std_vector : public std::vector<T, std_allocator<T>> {};
 
 #if 0