diff --git a/.github/workflows/android-build.yml b/.github/workflows/android-build.yml index 019eb18b1..8a6a32c6b 100644 --- a/.github/workflows/android-build.yml +++ b/.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: | diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 366a2224e..2ed02aab1 100644 --- a/.github/workflows/coverage.yml +++ b/.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: | diff --git a/.github/workflows/cross-build.yml b/.github/workflows/cross-build.yml index 83fae7a5d..8745215d2 100644 --- a/.github/workflows/cross-build.yml +++ b/.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 diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index 301ee2c87..82e0c4c0b 100644 --- a/.github/workflows/docker-image.yml +++ b/.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 diff --git a/.github/workflows/msvc-static-build.yml b/.github/workflows/msvc-static-build.yml index 2db222161..b329d5abc 100644 --- a/.github/workflows/msvc-static-build.yml +++ b/.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: | diff --git a/.github/workflows/wasm-release.yml b/.github/workflows/wasm-release.yml index de15a242c..defcd8fea 100644 --- a/.github/workflows/wasm-release.yml +++ b/.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 diff --git a/.github/workflows/wasm.yml b/.github/workflows/wasm.yml index e8ac095e5..9e321947e 100644 --- a/.github/workflows/wasm.yml +++ b/.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 diff --git a/.github/workflows/wip.yml b/.github/workflows/wip.yml index ffea6225c..5ed29a457 100644 --- a/.github/workflows/wip.yml +++ b/.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}} diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 74d585dae..3d3996792 100644 --- a/scripts/mk_util.py +++ b/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') diff --git a/scripts/update_api.py b/scripts/update_api.py index 5f8db1932..c68597ea2 100755 --- a/scripts/update_api.py +++ b/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) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 2b7a4ce43..53f53347e 100644 --- a/src/api/api_context.cpp +++ b/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); } diff --git a/src/ast/converters/model_converter.cpp b/src/ast/converters/model_converter.cpp index 716970cba..d053394ca 100644 --- a/src/ast/converters/model_converter.cpp +++ b/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"; } diff --git a/src/ast/normal_forms/elim_term_ite.cpp b/src/ast/normal_forms/elim_term_ite.cpp index 3376e9dda..077f66d1f 100644 --- a/src/ast/normal_forms/elim_term_ite.cpp +++ b/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; diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp index 4391d8bf8..7c7576c84 100644 --- a/src/ast/pattern/pattern_inference.cpp +++ b/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; diff --git a/src/ast/rewriter/rewriter.cpp b/src/ast/rewriter/rewriter.cpp index 3b25b9409..51c4764df 100644 --- a/src/ast/rewriter/rewriter.cpp +++ b/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; +template class rewriter_tpl; +template class rewriter_tpl; +template class rewriter_tpl; diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 24df51845..90ba5bb3a 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/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; } diff --git a/src/ast/simplifiers/solve_context_eqs.cpp b/src/ast/simplifiers/solve_context_eqs.cpp index b56802caf..c58786f0e 100644 --- a/src/ast/simplifiers/solve_context_eqs.cpp +++ b/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> todo; - todo.push_back({ false, 0, df.fml()}); + svector> 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> 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; + } + } diff --git a/src/ast/simplifiers/solve_context_eqs.h b/src/ast/simplifiers/solve_context_eqs.h index 8332d3a73..a11a1043b 100644 --- a/src/ast/simplifiers/solve_context_eqs.h +++ b/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> const& todo); public: diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h index 2cb646777..fb9c469a8 100644 --- a/src/math/lp/nla_monotone_lemmas.h +++ b/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 get_sorted_key(const monic& rm) const; - vector> 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); + }; } diff --git a/src/params/pattern_inference_params.cpp b/src/params/pattern_inference_params.cpp index aac574c6e..0e548c896 100644 --- a/src/params/pattern_inference_params.cpp +++ b/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); diff --git a/src/params/pattern_inference_params.h b/src/params/pattern_inference_params.h index b037411ec..e558a6a7b 100644 --- a/src/params/pattern_inference_params.h +++ b/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); } diff --git a/src/params/pattern_inference_params_helper.pyg b/src/params/pattern_inference_params_helper.pyg index cb1f02877..80d36e3ec 100644 --- a/src/params/pattern_inference_params_helper.pyg +++ b/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'), diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 5e22d9d29..98323816a 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/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(); diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index d70d232e4..0c4c2a7b6 100644 --- a/src/solver/simplifier_solver.cpp +++ b/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));