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<elim_term_ite_cfg>;
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<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>;
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<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;
+ }
+
}
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<std::tuple<bool,unsigned,expr*,unsigned>> const& todo);
public:
diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 6a01d4ace..8af04c793 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/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) {
diff --git a/src/math/lp/nla_monotone_lemmas.h b/src/math/lp/nla_monotone_lemmas.h
index d13f588e8..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<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);
+ };
}
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/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index fa73788e6..9357b7a65 100644
--- a/src/smt/theory_lra.cpp
+++ b/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())
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));
diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h
index 7dab520df..053816449 100644
--- a/src/util/memory_manager.h
+++ b/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 {
};
diff --git a/src/util/vector.h b/src/util/vector.h
index 1cb25a8c4..9ca9a1103 100644
--- a/src/util/vector.h
+++ b/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