From a9054bc73b7632047f93190b7a6609c82fae42de Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E5=90=91=E9=98=B3?= <91933474+XiangYyang@users.noreply.github.com> Date: Wed, 20 Mar 2024 17:31:23 +0800 Subject: [PATCH 01/49] fix warning C4244 in util.h (#7171) Add a static cast to avoid warning C4244 on MSVC --- src/util/util.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/util.h b/src/util/util.h index f05e4f9f4..cf0146b12 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -142,7 +142,7 @@ static inline unsigned get_num_1bits(uint64_t v) { v = (v + (v >> 4)) & 0x0F0F0F0F0F0F0F0F; uint64_t r = (v * 0x0101010101010101) >> 56; SASSERT(c == r); - return r; + return static_cast(r); #endif } From 730f9ad9b7186137f9f6280c686399bb572ae5c5 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 19 Mar 2024 09:42:36 -1000 Subject: [PATCH 02/49] Nikolaj's fix in add_zero_assumption Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_explain.cpp | 75 ++++++++++++++++++++++++++++++++++++- 1 file changed, 73 insertions(+), 2 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 87fda76ef..4a60b895f 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -277,11 +277,13 @@ namespace nlsat { } }; - void add_zero_assumption(polynomial_ref & p) { + void add_zero_assumption(polynomial_ref& p) { // If p is of the form p1^n1 * ... * pk^nk, // then only the factors that are zero in the current interpretation needed to be considered. // I don't want to create a nested conjunction in the clause. // Then, I assert p_i1 * ... * p_im != 0 + bool is_linear = true; + unsigned x = max_var(p); { restore_factors _restore(m_factors, m_factors_save); factor(p, m_factors); @@ -294,14 +296,37 @@ namespace nlsat { if (is_zero(sign(f))) { m_zero_fs.push_back(m_factors.get(i)); m_is_even.push_back(false); - } + is_linear &= m_pm.degree(f, x) <= 1; + } + } + } + + if (!is_linear) { + scoped_anum_vector& roots = m_roots_tmp; + roots.reset(); + m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots); + unsigned num_roots = roots.size(); + if (num_roots > 0) { + anum const& x_val = m_assignment.value(x); + for (unsigned i = 0; i < num_roots; i++) { + int s = m_am.compare(x_val, roots[i]); + if (s != 0) + continue; + add_root_literal(atom::ROOT_EQ, x, i + 1, p); + return; + } + display(verbose_stream() << "polynomial ", p); + m_solver.display(verbose_stream()); + UNREACHABLE(); } } SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it. + literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data()); l.neg(); TRACE("nlsat_explain", tout << "adding (zero assumption) literal:\n"; display(tout, l); tout << "\n";); add_literal(l); + } void add_simple_assumption(atom::kind k, poly * p, bool sign = false) { @@ -649,6 +674,52 @@ namespace nlsat { } } + void add_zero_assumption_on_factor(polynomial_ref& f) { + display(std::cout << "zero factors \n", f); + } + // this function also explains the value 0, if met + bool coeffs_are_zeroes(polynomial_ref &s) { + restore_factors _restore(m_factors, m_factors_save); + factor(s, m_factors); + unsigned num_factors = m_factors.size(); + m_zero_fs.reset(); + m_is_even.reset(); + polynomial_ref f(m_pm); + bool have_zero = false; + for (unsigned i = 0; i < num_factors; i++) { + f = m_factors.get(i); + // std::cout << "f=";display(std::cout, f) << "\n"; + if (coeffs_are_zeroes_in_factor(f)) { + have_zero = true; + break; + } + } + if (!have_zero) + return false; + var x = max_var(f); + unsigned n = degree(f, x); + auto c = polynomial_ref(this->m_pm); + for (unsigned j = 0; j <= n; j++) { + c = m_pm.coeff(s, x, j); + SASSERT(sign(c) == 0); + ensure_sign(c); + } + return true; + } + + + bool coeffs_are_zeroes_in_factor(polynomial_ref & s) { + var x = max_var(s); + unsigned n = degree(s, x); + auto c = polynomial_ref(this->m_pm); + for (unsigned j = 0; j <= n; j++) { + c = m_pm.coeff(s, x, j); + if (sign(c) != 0) + return false; + } + return true; + } + /** \brief Add v-psc(p, q, x) into m_todo */ From 70d2263a85f9fb0bd289125a5b9b404017bb40fb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Mar 2024 12:29:55 -0700 Subject: [PATCH 03/49] cast, updated nlexplain --- src/nlsat/nlsat_explain.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 4a60b895f..4bbc5cb03 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -277,6 +277,7 @@ namespace nlsat { } }; + void add_zero_assumption(polynomial_ref& p) { // If p is of the form p1^n1 * ... * pk^nk, // then only the factors that are zero in the current interpretation needed to be considered. @@ -300,7 +301,7 @@ namespace nlsat { } } } - + if (!is_linear) { scoped_anum_vector& roots = m_roots_tmp; roots.reset(); @@ -312,6 +313,7 @@ namespace nlsat { int s = m_am.compare(x_val, roots[i]); if (s != 0) continue; + TRACE("nlsat_explain", tout << "adding (zero assumption) root " << "\n"); add_root_literal(atom::ROOT_EQ, x, i + 1, p); return; } @@ -321,12 +323,11 @@ namespace nlsat { } } SASSERT(!m_zero_fs.empty()); // one of the factors must be zero in the current interpretation, since p is zero in it. - + literal l = m_solver.mk_ineq_literal(atom::EQ, m_zero_fs.size(), m_zero_fs.data(), m_is_even.data()); l.neg(); TRACE("nlsat_explain", tout << "adding (zero assumption) literal:\n"; display(tout, l); tout << "\n";); add_literal(l); - } void add_simple_assumption(atom::kind k, poly * p, bool sign = false) { From f840d5d9650d20e0f6cd650bef92c21e6d15da15 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Mar 2024 21:27:00 -0700 Subject: [PATCH 04/49] na Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_explain.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 4bbc5cb03..27d0531af 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1094,12 +1094,12 @@ namespace nlsat { if (x < max_x) add_cell_lits(ps, x); while (true) { + TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; + display(tout, ps); tout << "\n";); if (all_univ(ps, x) && m_todo.empty()) { m_todo.reset(); break; } - TRACE("nlsat_explain", tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; - display(tout, ps); tout << "\n";); add_lc(ps, x); psc_discriminant(ps, x); psc_resultant(ps, x); From 27a9b8bd03dc7d6daa43d510e7ca14d97ceb7f58 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Mar 2024 21:32:18 -0700 Subject: [PATCH 05/49] fix project minor version Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index d76e03ba6..ce2e7cb7e 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 13, 0, 1) # express a default build version or pick up ci build version + set_version(4, 13, 1, 0) # express a default build version or pick up ci build version # Z3 Project definition def init_project_def(): From 530c6fc625d85ed8b22d27e0b066896f1b669f28 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 20 Mar 2024 22:05:30 -0700 Subject: [PATCH 06/49] fix ##7175 - don't add user macros/functions when smtlib2_compliant=true Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 019b7fd4f..e883d0e9d 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1894,6 +1894,8 @@ void cmd_context::add_declared_functions(model& mdl) { model_params p; if (!p.user_functions()) return; + if (m_params.m_smtlib2_compliant) + return; for (auto const& kv : m_func_decls) { func_decl* f = kv.m_value.first(); if (f->get_family_id() == null_family_id && !mdl.has_interpretation(f)) { @@ -2066,7 +2068,10 @@ void cmd_context::complete_model(model_ref& md) const { if (m_macros.find(k, decls)) body = decls.find(f->get_arity(), f->get_domain()); + if (body && m_params.m_smtlib2_compliant) + continue; sort * range = f->get_range(); + if (!body) body = m().get_some_value(range); if (f->get_arity() > 0) { From 6455de9dd32b0bb75e86383cda0d8f172cb6ef7d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Mar 2024 09:39:13 -0700 Subject: [PATCH 07/49] fix #7179 Ensure that flat associative rewriting is disabled if rewriter.flat is set to false. --- src/ast/rewriter/th_rewriter.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index ee8b79be5..844c51940 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -17,6 +17,7 @@ Notes: --*/ #include "params/rewriter_params.hpp" +#include "params/poly_rewriter_params.hpp" #include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/bool_rewriter.h" #include "ast/rewriter/arith_rewriter.h" @@ -83,7 +84,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { void updt_local_params(params_ref const & _p) { rewriter_params p(_p); - m_flat = true; + poly_rewriter_params pp(_p); + m_flat = pp.flat(); m_max_memory = megabytes_to_bytes(p.max_memory()); m_max_steps = p.max_steps(); m_pull_cheap_ite = p.pull_cheap_ite(); From 648e05754c37220f1fbb5943b4e69545d82b7bae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 21 Mar 2024 09:40:50 -0700 Subject: [PATCH 08/49] #7178 copy build tool chains used for manylinux arm64 into ubuntu builds alternatively, just remove ubuntuArm64 and use the many-linux builds for Arm64? --- scripts/nightly.yaml | 17 +++++++++++++---- scripts/release.yml | 17 +++++++++++++---- 2 files changed, 26 insertions(+), 8 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 00e27507e..c448b5dd7 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -114,10 +114,19 @@ stages: pool: vmImage: "ubuntu-latest" steps: - - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 - - script: git clone https://github.com/z3prover/z3test z3test - - script: python z3test/scripts/test_benchmarks.py build-dist/z3 z3test/regressions/smt2 - - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/. + - script: curl -L -o /tmp/arm-toolchain.tar.xz 'https://developer.arm.com/-/media/Files/downloads/gnu/11.2-2022.02/binrel/gcc-arm-11.2-2022.02-x86_64-aarch64-none-linux-gnu.tar.xz?rev=33c6e30e5ac64e6dba8f0431f2c35f1b&hash=9918A05BF47621B632C7A5C8D2BB438FB80A4480' + - script: mkdir -p /tmp/arm-toolchain/ + - script: tar xf /tmp/arm-toolchain.tar.xz -C /tmp/arm-toolchain/ --strip-components=1 + - script: echo '##vso[task.prependpath]/tmp/arm-toolchain/bin' + - script: echo '##vso[task.prependpath]/tmp/arm-toolchain/aarch64-none-linux-gnu/libc/usr/bin' + - script: echo $PATH + - script: stat /tmp/arm-toolchain/bin/aarch64-none-linux-gnu-gcc + - script: python scripts/mk_unix_dist.py --nodotnet --nojava --arch=arm64 + - task: CopyFiles@2 + inputs: + sourceFolder: dist + contents: '*.zip' + targetFolder: $(Build.ArtifactStagingDirectory) - task: PublishPipelineArtifact@0 inputs: artifactName: 'UbuntuArm64' diff --git a/scripts/release.yml b/scripts/release.yml index 8f1242f82..3125595d7 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -119,10 +119,19 @@ stages: pool: vmImage: "ubuntu-latest" steps: - - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 - - script: git clone https://github.com/z3prover/z3test z3test - - script: python z3test/scripts/test_benchmarks.py build-dist/z3 z3test/regressions/smt2 - - script: cp dist/*.zip $(Build.ArtifactStagingDirectory)/. + - script: curl -L -o /tmp/arm-toolchain.tar.xz 'https://developer.arm.com/-/media/Files/downloads/gnu/11.2-2022.02/binrel/gcc-arm-11.2-2022.02-x86_64-aarch64-none-linux-gnu.tar.xz?rev=33c6e30e5ac64e6dba8f0431f2c35f1b&hash=9918A05BF47621B632C7A5C8D2BB438FB80A4480' + - script: mkdir -p /tmp/arm-toolchain/ + - script: tar xf /tmp/arm-toolchain.tar.xz -C /tmp/arm-toolchain/ --strip-components=1 + - script: echo '##vso[task.prependpath]/tmp/arm-toolchain/bin' + - script: echo '##vso[task.prependpath]/tmp/arm-toolchain/aarch64-none-linux-gnu/libc/usr/bin' + - script: echo $PATH + - script: stat /tmp/arm-toolchain/bin/aarch64-none-linux-gnu-gcc + - script: python scripts/mk_unix_dist.py --nodotnet --nojava --arch=arm64 + - task: CopyFiles@2 + inputs: + sourceFolder: dist + contents: '*.zip' + targetFolder: $(Build.ArtifactStagingDirectory) - task: PublishPipelineArtifact@0 inputs: artifactName: 'UbuntuArm64' From 80642e5a7caf858541a163569c3013afbe39ed14 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sat, 23 Mar 2024 18:38:14 +0000 Subject: [PATCH 09/49] Add check for libatomic requirement to Python build system (#7184) * Add check for libatomic requirement to Python build system * More thorough check * Fix typos --- scripts/mk_util.py | 38 +++++++++++++++++++++++++++++++------- 1 file changed, 31 insertions(+), 7 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 014b0e40f..3e6da0b22 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -314,6 +314,26 @@ def test_fpmath(cc): FPMATH_FLAGS="" return "UNKNOWN" +def test_atomic_required(cc): + t = TempFile('tstatomic.cpp') + t.add(""" + #include + std::atomic x; + std::atomic y; + std::atomic z; + std::atomic w; + int main() { + ++z; + ++y; + ++w; + return ++x; + } + """) + t.commit() + fails_without = exec_compiler_cmd([cc, CPPFLAGS, '', 'tstatomic.cpp', LDFLAGS, '']) != 0 + ok_with = exec_compiler_cmd([cc, CPPFLAGS, '', 'tstatomic.cpp', LDFLAGS + ' -latomic', '']) == 0 + return fails_without and ok_with + def find_jni_h(path): for root, dirs, files in os.walk(path): @@ -555,19 +575,19 @@ def set_version(major, minor, build, revision): print("Set Assembly Version (BUILD):", VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK) return - # use parameters to set up version if not provided by script args + # use parameters to set up version if not provided by script args VER_MAJOR = major VER_MINOR = minor VER_BUILD = build VER_TWEAK = revision - # update VER_TWEAK base on github + # update VER_TWEAK base on github if GIT_DESCRIBE: branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD']) VER_TWEAK = int(check_output(['git', 'rev-list', '--count', 'HEAD'])) - + print("Set Assembly Version (DEFAULT):", VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK) - + def get_version(): return (VER_MAJOR, VER_MINOR, VER_BUILD, VER_TWEAK) @@ -1858,7 +1878,7 @@ class JavaDLLComponent(Component): os.path.join('api', 'java', 'Native')) elif IS_OSX and IS_ARCH_ARM64: out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) -arch arm64 %s$(OBJ_EXT) libz3$(SO_EXT)\n' % - os.path.join('api', 'java', 'Native')) + os.path.join('api', 'java', 'Native')) else: out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' % os.path.join('api', 'java', 'Native')) @@ -2600,6 +2620,9 @@ def mk_config(): CXXFLAGS = '%s -fvisibility=hidden -fvisibility-inlines-hidden -c' % CXXFLAGS FPMATH = test_fpmath(CXX) CXXFLAGS = '%s %s' % (CXXFLAGS, FPMATH_FLAGS) + atomic_required = test_atomic_required(CXX) + if atomic_required: + LDFLAGS = '%s -latomic' % LDFLAGS if LOG_SYNC: CXXFLAGS = '%s -DZ3_LOG_SYNC' % CXXFLAGS if SINGLE_THREADED: @@ -2710,6 +2733,7 @@ def mk_config(): print('Prefix: %s' % PREFIX) print('64-bit: %s' % is64()) print('FP math: %s' % FPMATH) + print('libatomic: %s' % ('required' if atomic_required else 'not required')) print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR) if GPROF: print('gprof: enabled') @@ -2854,7 +2878,7 @@ def update_version(): revision = VER_TWEAK print("UpdateVersion:", get_full_version_string(major, minor, build, revision)) - + if major is None or minor is None or build is None or revision is None: raise MKException("set_version(major, minor, build, revision) must be used before invoking update_version()") if not ONLY_MAKEFILES: @@ -3068,7 +3092,7 @@ def mk_bindings(api_files): z3py_output_dir=get_z3py_dir(), dotnet_output_dir=dotnet_output_dir, java_input_dir=java_input_dir, - java_output_dir=java_output_dir, + java_output_dir=java_output_dir, java_package_name=java_package_name, ml_output_dir=ml_output_dir, ml_src_dir=ml_output_dir From c18a42cf5b0db2f45475ff84266237e10a361a72 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 23 Mar 2024 16:14:24 -0400 Subject: [PATCH 10/49] change signed projection to include root object. --- src/nlsat/nlsat_explain.cpp | 11 ++++++++++- src/qe/nlqsat.cpp | 6 ++++-- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp index 27d0531af..618394ac1 100644 --- a/src/nlsat/nlsat_explain.cpp +++ b/src/nlsat/nlsat_explain.cpp @@ -1744,7 +1744,16 @@ namespace nlsat { solve_eq(x, eq_index, ps); } else { - project_pairs(x, eq_index, ps); + add_zero_assumption(p); + + for (unsigned j = 0; j < ps.size(); ++j) { + if (j == eq_index) + continue; + p = ps.get(j); + int s = sign(p); + atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT)); + add_simple_assumption(k, p, false); + } } return; } diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index d81048c3d..8a6f910bc 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -480,8 +480,10 @@ namespace qe { num_scopes = 2*(level()/2); } else { - SASSERT(clevel.max() + 2 <= level()); - num_scopes = level() - clevel.max(); + if (clevel.max() + 2 <= level()) + num_scopes = level() - clevel.max(); + else + num_scopes = 2; // the projection contains auxiliary variables from root objects. SASSERT(num_scopes >= 2); } From 111fcb9366fbcf6a8b946a09481e32c27afab98d Mon Sep 17 00:00:00 2001 From: Steven Moy Date: Wed, 27 Mar 2024 19:06:58 -0700 Subject: [PATCH 11/49] Implement API to set exit action to exception (#7192) * Implement API to set exit action to exception * Turn on exit_action_to_throw_exception upon API context creation --- src/api/api_context.cpp | 2 ++ src/util/debug.cpp | 31 +++++++++++++++++++++++++++++++ src/util/debug.h | 19 ++++++++++++++----- 3 files changed, 47 insertions(+), 5 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 344224dd3..2f1f50712 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include +#include "util/debug.h" #include "util/z3_version.h" #include "api/api_context.h" #include "ast/ast_pp.h" @@ -393,6 +394,7 @@ extern "C" { Z3_TRY; LOG_Z3_mk_context_rc(c); memory::initialize(UINT_MAX); + set_default_exit_action(exit_action::throw_exception); Z3_context r = reinterpret_cast(alloc(api::context, reinterpret_cast(c), true)); RETURN_Z3(r); Z3_CATCH_RETURN_NO_HANDLE(nullptr); diff --git a/src/util/debug.cpp b/src/util/debug.cpp index c9ca9fc31..ee57ac4b3 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -75,6 +75,37 @@ bool is_debug_enabled(const char * tag) { return g_enabled_debug_tags->contains(tag); } +atomic g_default_exit_action(exit_action::exit); + +exit_action get_default_exit_action() { + return g_default_exit_action; +} + +void set_default_exit_action(exit_action a) { + g_default_exit_action = a; +} + +void invoke_exit_action(unsigned int code) { + exit_action a = get_default_exit_action(); + switch (a) { + case exit_action::exit: + exit(code); + case exit_action::throw_exception: + switch (code) { + case ERR_INTERNAL_FATAL: + throw default_exception("internal fatal"); + case ERR_UNREACHABLE: + throw default_exception("unreachable"); + case ERR_NOT_IMPLEMENTED_YET: + throw default_exception("not implemented yet"); + default: + throw default_exception("unknown"); + } + default: + exit(code); + } +} + atomic g_default_debug_action(debug_action::ask); debug_action get_default_debug_action() { diff --git a/src/util/debug.h b/src/util/debug.h index 5f092b181..5e9ea9b2c 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -35,6 +35,14 @@ enum class debug_action { debug_action get_default_debug_action(); void set_default_debug_action(debug_action a); +enum class exit_action { + exit, + throw_exception, +}; +exit_action get_default_exit_action(); +void set_default_exit_action(exit_action a); +void invoke_exit_action(unsigned int code); + #include "util/error_codes.h" #include "util/warning.h" @@ -56,7 +64,7 @@ void set_default_debug_action(debug_action a); #endif #ifdef NO_Z3_DEBUGGER -#define INVOKE_DEBUGGER() exit(ERR_INTERNAL_FATAL) +#define INVOKE_DEBUGGER() invoke_exit_action(ERR_INTERNAL_FATAL) #else #ifdef _WINDOWS #define INVOKE_DEBUGGER() __debugbreak() @@ -71,6 +79,7 @@ void enable_debug(const char * tag); void disable_debug(const char * tag); bool is_debug_enabled(const char * tag); + #define SASSERT(COND) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); }) #define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); }) #define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); }) @@ -85,25 +94,25 @@ bool is_debug_enabled(const char * tag); #ifdef Z3DEBUG # define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); INVOKE_DEBUGGER();) #else -# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); exit(ERR_UNREACHABLE); } ((void) 0) +# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNEXPECTED CODE WAS REACHED."); invoke_exit_action(ERR_UNREACHABLE); } ((void) 0) #endif #ifdef Z3DEBUG # define NOT_IMPLEMENTED_YET() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); INVOKE_DEBUGGER();) #else -# define NOT_IMPLEMENTED_YET() { notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0) +# define NOT_IMPLEMENTED_YET() { notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); invoke_exit_action(ERR_NOT_IMPLEMENTED_YET); } ((void) 0) #endif #define VERIFY(_x_) if (!(_x_)) { \ notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #_x_ "\n"); \ - exit(ERR_UNREACHABLE); \ + invoke_exit_action(ERR_UNREACHABLE); \ } #define VERIFY_EQ(LHS, RHS) \ if (!((LHS) == (RHS))) { \ notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #LHS " == " #RHS "\n"); \ std::cerr << "LHS value: " << (LHS) << "\nRHS value: " << (RHS) << "\n"; \ - exit(ERR_UNREACHABLE); \ + invoke_exit_action(ERR_UNREACHABLE); \ } #define ENSURE(_x_) VERIFY(_x_) From 51f1e2655c5c3acdf226169348eee1e0c2b4c309 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 Mar 2024 12:59:02 -0700 Subject: [PATCH 12/49] updates to sls Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/solve_eqs.cpp | 1 + src/ast/sls/bv_sls.cpp | 138 +++++++++++++++++++++++------- src/ast/sls/bv_sls.h | 19 ++-- src/ast/sls/bv_sls_eval.cpp | 8 +- src/ast/sls/bv_sls_fixed.cpp | 8 +- src/ast/sls/bv_sls_terms.cpp | 65 ++++++++------ src/ast/sls/bv_sls_terms.h | 10 ++- src/ast/sls/sls_engine.cpp | 8 +- src/ast/sls/sls_engine.h | 6 +- src/ast/sls/sls_valuation.cpp | 39 ++++++--- src/params/sls_params.pyg | 1 + src/sat/smt/sls_solver.cpp | 3 +- src/tactic/sls/sls_tactic.cpp | 33 +++---- 13 files changed, 234 insertions(+), 105 deletions(-) diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp index c97cab7c9..d3e4116b7 100644 --- a/src/ast/simplifiers/solve_eqs.cpp +++ b/src/ast/simplifiers/solve_eqs.cpp @@ -329,6 +329,7 @@ namespace euf { m_config.m_context_solve = p.get_bool("context_solve", tp.solve_eqs_context_solve()); for (auto* ex : m_extract_plugins) ex->updt_params(p); + m_rewriter.updt_params(p); } void solve_eqs::collect_param_descrs(param_descrs& r) { diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index f80a362ba..6a176016f 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -25,12 +25,15 @@ Author: namespace bv { - sls::sls(ast_manager& m): + sls::sls(ast_manager& m, params_ref const& p): m(m), bv(m), m_terms(m), - m_eval(m) - {} + m_eval(m), + m_engine(m, p) + { + updt_params(p); + } void sls::init() { m_terms.init(); @@ -67,20 +70,48 @@ namespace bv { } } + void sls::init_repair_candidates() { + m_to_repair.reset(); + ptr_vector todo; + expr_fast_mark1 mark; + for (auto index : m_repair_roots) + todo.push_back(m_terms.term(index)); + for (unsigned i = 0; i < todo.size(); ++i) { + expr* e = todo[i]; + if (mark.is_marked(e)) + continue; + mark.mark(e); + if (!is_app(e)) + continue; + for (expr* arg : *to_app(e)) + todo.push_back(arg); + + if (is_uninterp_const(e)) + m_to_repair.insert(e->get_id()); + + } + } + + void sls::reinit_eval() { + init_repair_candidates(); + + if (m_to_repair.empty()) + return; + std::function eval = [&](expr* e, unsigned i) { - auto should_keep = [&]() { - return m_rand() % 100 <= 92; - }; - if (m.is_bool(e)) { - if (m_eval.is_fixed0(e) || should_keep()) - return m_eval.bval0(e); - } + unsigned id = e->get_id(); + bool keep = (m_rand() % 100 <= 50) || !m_to_repair.contains(id); + if (m.is_bool(e) && (m_eval.is_fixed0(e) || keep)) + return m_eval.bval0(e); else if (bv.is_bv(e)) { auto& w = m_eval.wval(e); - if (w.fixed.get(i) || should_keep()) - return w.get_bit(i); - } + if (w.fixed.get(i) || keep) + return w.get_bit(i); + //auto const& z = m_engine.get_value(e); + //return rational(z).get_bit(i); + } + return m_rand() % 2 == 0; }; m_eval.init_eval(m_terms.assertions(), eval); @@ -119,7 +150,7 @@ namespace bv { return { false, nullptr }; } - lbool sls::search() { + lbool sls::search1() { // init and init_eval were invoked unsigned n = 0; for (; n++ < m_config.m_max_repairs && m.inc(); ) { @@ -127,7 +158,6 @@ namespace bv { if (!e) return l_true; - trace_repair(down, e); ++m_stats.m_moves; @@ -140,16 +170,32 @@ namespace bv { return l_undef; } + lbool sls::search2() { + lbool res = l_undef; + if (m_stats.m_restarts == 0) + res = m_engine(); + else if (m_stats.m_restarts % 1000 == 0) + res = m_engine.search_loop(); + if (res != l_undef) + m_engine_model = true; + return res; + } + lbool sls::operator()() { lbool res = l_undef; m_stats.reset(); m_stats.m_restarts = 0; + m_engine_model = false; + do { - res = search(); + res = search1(); if (res != l_undef) break; trace(); + res = search2(); + if (res != l_undef) + break; reinit_eval(); } while (m.inc() && m_stats.m_restarts++ < m_config.m_max_restarts); @@ -158,34 +204,60 @@ namespace bv { } void sls::try_repair_down(app* e) { - unsigned n = e->get_num_args(); if (n == 0) { - if (m.is_bool(e)) - m_eval.set(e, m_eval.bval1(e)); - else + if (m.is_bool(e)) { + m_eval.set(e, m_eval.bval1(e)); + } + else { VERIFY(m_eval.wval(e).commit_eval()); + } for (auto p : m_terms.parents(e)) m_repair_up.insert(p->get_id()); + return; } - unsigned s = m_rand(n); - for (unsigned i = 0; i < n; ++i) { - auto j = (i + s) % n; - if (m_eval.try_repair(e, j)) { - set_repair_down(e->get_arg(j)); + if (n == 2) { + auto d1 = get_depth(e->get_arg(0)); + auto d2 = get_depth(e->get_arg(1)); + unsigned s = m_rand(d1 + d2 + 2); + if (s <= d1 && m_eval.try_repair(e, 0)) { + set_repair_down(e->get_arg(0)); + return; + } + if (m_eval.try_repair(e, 1)) { + set_repair_down(e->get_arg(1)); + return; + } + if (m_eval.try_repair(e, 0)) { + set_repair_down(e->get_arg(0)); return; } } - // search a new root / random walk to repair + else { + unsigned s = m_rand(n); + for (unsigned i = 0; i < n; ++i) { + auto j = (i + s) % n; + if (m_eval.try_repair(e, j)) { + set_repair_down(e->get_arg(j)); + return; + } + } + } + // repair was not successful, so reset the state to find a different way to repair + init_repair(); } void sls::try_repair_up(app* e) { - if (m_terms.is_assertion(e) || !m_eval.repair_up(e)) - m_repair_roots.insert(e->get_id()); + if (m_terms.is_assertion(e)) + m_repair_roots.insert(e->get_id()); + else if (!m_eval.repair_up(e)) { + //m_repair_roots.insert(e->get_id()); + init_repair(); + } else { if (!eval_is_correct(e)) { verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; @@ -224,7 +296,10 @@ namespace bv { } model_ref sls::get_model() { - model_ref mdl = alloc(model, m); + if (m_engine_model) + return m_engine.get_model(); + + model_ref mdl = alloc(model, m); auto& terms = m_eval.sort_assertions(m_terms.assertions()); for (expr* e : terms) { if (!re_eval_is_correct(to_app(e))) { @@ -273,7 +348,12 @@ namespace bv { void sls::updt_params(params_ref const& _p) { sls_params p(_p); m_config.m_max_restarts = p.max_restarts(); + m_config.m_max_repairs = p.max_repairs(); m_rand.set_seed(p.random_seed()); + m_terms.updt_params(_p); + params_ref q = _p; + q.set_uint("max_restarts", 10); + m_engine.updt_params(q); } void sls::trace_repair(bool down, expr* e) { diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index bbcd59aea..ae7d7cb57 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -26,6 +26,7 @@ Author: #include "ast/sls/sls_valuation.h" #include "ast/sls/bv_sls_terms.h" #include "ast/sls/bv_sls_eval.h" +#include "ast/sls/sls_engine.h" #include "ast/bv_decl_plugin.h" #include "model/model.h" @@ -49,6 +50,8 @@ namespace bv { ptr_vector m_todo; random_gen m_rand; config m_config; + sls_engine m_engine; + bool m_engine_model = false; std::pair next_to_repair(); @@ -59,19 +62,23 @@ namespace bv { void try_repair_up(app* e); void set_repair_down(expr* e) { m_repair_down = e->get_id(); } - lbool search(); + lbool search1(); + lbool search2(); void reinit_eval(); void init_repair(); void trace(); void trace_repair(bool down, expr* e); + indexed_uint_set m_to_repair; + void init_repair_candidates(); + public: - sls(ast_manager& m); + sls(ast_manager& m, params_ref const& p); /** * Add constraints */ - void assert_expr(expr* e) { m_terms.assert_expr(e); } + void assert_expr(expr* e) { m_terms.assert_expr(e); m_engine.assert_expr(e); } /* * Invoke init after all expressions are asserted. @@ -91,10 +98,10 @@ namespace bv { lbool operator()(); void updt_params(params_ref const& p); - void collect_statistics(statistics & st) const { m_stats.collect_statistics(st); } - void reset_statistics() { m_stats.reset(); } + void collect_statistics(statistics& st) const { m_stats.collect_statistics(st); m_engine.collect_statistics(st); } + void reset_statistics() { m_stats.reset(); m_engine.reset_statistics(); } - sls_stats const& get_stats() const { return m_stats; } + unsigned get_num_moves() { return m_stats.m_moves + m_engine.get_stats().m_moves; } std::ostream& display(std::ostream& out); diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 4b7bf9546..579bc7369 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -24,8 +24,8 @@ namespace bv { {} void sls_eval::init_eval(expr_ref_vector const& es, std::function const& eval) { - sort_assertions(es); - for (expr* e : m_todo) { + auto& terms = sort_assertions(es); + for (expr* e : terms) { if (!is_app(e)) continue; app* a = to_app(e); @@ -49,7 +49,7 @@ namespace bv { TRACE("sls", tout << "Unhandled expression " << mk_pp(e, m) << "\n"); } } - m_todo.reset(); + terms.reset(); } /** @@ -1698,7 +1698,7 @@ namespace bv { } if (bv.is_bv(e)) { auto& v = eval(to_app(e)); - // verbose_stream() << "committing: " << v << "\n"; + for (unsigned i = 0; i < v.nw; ++i) if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) { v.bits().copy_to(v.nw, v.eval); diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index 91ce8e0e2..e2b29b1fe 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -108,6 +108,13 @@ namespace bv { else if (bv.is_numeral(t, a)) init_range(s, -a, nullptr, rational(0), false); } + else if (sign && m.is_eq(e, s, t)) { + if (bv.is_numeral(s, a)) + // 1 <= t - a + init_range(nullptr, rational(1), t, -a, false); + else if (bv.is_numeral(t, a)) + init_range(nullptr, rational(1), s, -a, false); + } else if (bv.is_bit2bool(e, s, idx)) { auto& val = wval(s); val.try_set_bit(idx, !sign); @@ -157,7 +164,6 @@ namespace bv { else v.add_range(-b, -a); } - } void sls_fixed::get_offset(expr* e, expr*& x, rational& offset) { diff --git a/src/ast/sls/bv_sls_terms.cpp b/src/ast/sls/bv_sls_terms.cpp index 8702c3c48..4624ab85c 100644 --- a/src/ast/sls/bv_sls_terms.cpp +++ b/src/ast/sls/bv_sls_terms.cpp @@ -20,12 +20,14 @@ Author: #include "ast/ast_ll_pp.h" #include "ast/sls/bv_sls.h" +#include "ast/rewriter/th_rewriter.h" namespace bv { sls_terms::sls_terms(ast_manager& m): m(m), bv(m), + m_rewriter(m), m_assertions(m), m_pinned(m), m_translated(m), @@ -40,18 +42,20 @@ namespace bv { expr* top = e; m_pinned.push_back(e); m_todo.push_back(e); - expr_fast_mark1 mark; - for (unsigned i = 0; i < m_todo.size(); ++i) { - expr* e = m_todo[i]; - if (!is_app(e)) - continue; - if (m_translated.get(e->get_id(), nullptr)) - continue; - if (mark.is_marked(e)) - continue; - mark.mark(e); - for (auto arg : *to_app(e)) - m_todo.push_back(arg); + { + expr_fast_mark1 mark; + for (unsigned i = 0; i < m_todo.size(); ++i) { + expr* e = m_todo[i]; + if (!is_app(e)) + continue; + if (m_translated.get(e->get_id(), nullptr)) + continue; + if (mark.is_marked(e)) + continue; + mark.mark(e); + for (auto arg : *to_app(e)) + m_todo.push_back(arg); + } } std::stable_sort(m_todo.begin(), m_todo.end(), [&](expr* a, expr* b) { return get_depth(a) < get_depth(b); }); for (expr* e : m_todo) @@ -127,7 +131,7 @@ namespace bv { m_translated.setx(e->get_id(), r); } - expr* sls_terms::mk_sdiv(expr* x, expr* y) { + expr_ref sls_terms::mk_sdiv(expr* x, expr* y) { // d = udiv(abs(x), abs(y)) // y = 0, x >= 0 -> -1 // y = 0, x < 0 -> 1 @@ -141,17 +145,18 @@ namespace bv { expr_ref z(bv.mk_zero(sz), m); expr* signx = bv.mk_ule(bv.mk_numeral(N / 2, sz), x); expr* signy = bv.mk_ule(bv.mk_numeral(N / 2, sz), y); - expr* absx = m.mk_ite(signx, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), x), x); - expr* absy = m.mk_ite(signy, bv.mk_bv_sub(bv.mk_numeral(N - 1, sz), y), y); + expr* absx = m.mk_ite(signx, bv.mk_bv_neg(x), x); + expr* absy = m.mk_ite(signy, bv.mk_bv_neg(y), y); expr* d = bv.mk_bv_udiv(absx, absy); - expr* r = m.mk_ite(m.mk_eq(signx, signy), d, bv.mk_bv_neg(d)); + expr_ref r(m.mk_ite(m.mk_eq(signx, signy), d, bv.mk_bv_neg(d)), m); r = m.mk_ite(m.mk_eq(z, y), - m.mk_ite(signx, bv.mk_one(sz), bv.mk_numeral(N - 1, sz)), - m.mk_ite(m.mk_eq(x, z), z, r)); + m.mk_ite(signx, bv.mk_one(sz), bv.mk_numeral(N - 1, sz)), + m.mk_ite(m.mk_eq(x, z), z, r)); + m_rewriter(r); return r; } - expr* sls_terms::mk_smod(expr* x, expr* y) { + expr_ref sls_terms::mk_smod(expr* x, expr* y) { // u := umod(abs(x), abs(y)) // u = 0 -> 0 // y = 0 -> x @@ -164,21 +169,24 @@ namespace bv { expr_ref abs_x(m.mk_ite(bv.mk_sle(z, x), x, bv.mk_bv_neg(x)), m); expr_ref abs_y(m.mk_ite(bv.mk_sle(z, y), y, bv.mk_bv_neg(y)), m); expr_ref u(bv.mk_bv_urem(abs_x, abs_y), m); - return - m.mk_ite(m.mk_eq(u, z), z, + expr_ref r(m); + r = m.mk_ite(m.mk_eq(u, z), z, m.mk_ite(m.mk_eq(y, z), x, m.mk_ite(m.mk_and(bv.mk_sle(z, x), bv.mk_sle(z, x)), u, m.mk_ite(bv.mk_sle(z, x), bv.mk_bv_add(y, u), m.mk_ite(bv.mk_sle(z, y), bv.mk_bv_sub(y, u), bv.mk_bv_neg(u)))))); - + m_rewriter(r); + return r; } - expr* sls_terms::mk_srem(expr* x, expr* y) { + expr_ref sls_terms::mk_srem(expr* x, expr* y) { // y = 0 -> x // else x - sdiv(x, y) * y - return - m.mk_ite(m.mk_eq(y, bv.mk_zero(bv.get_bv_size(x))), + expr_ref r(m); + r = m.mk_ite(m.mk_eq(y, bv.mk_zero(bv.get_bv_size(x))), x, bv.mk_bv_sub(x, bv.mk_bv_mul(y, mk_sdiv(x, y)))); + m_rewriter(r); + return r; } @@ -209,4 +217,11 @@ namespace bv { m_assertion_set.insert(a->get_id()); } + void sls_terms::updt_params(params_ref const& p) { + params_ref q = p; + q.set_bool("flat", false); + m_rewriter.updt_params(q); + } + + } diff --git a/src/ast/sls/bv_sls_terms.h b/src/ast/sls/bv_sls_terms.h index 3baffc78e..a6294aa9c 100644 --- a/src/ast/sls/bv_sls_terms.h +++ b/src/ast/sls/bv_sls_terms.h @@ -21,6 +21,7 @@ Author: #include "util/scoped_ptr_vector.h" #include "util/uint_set.h" #include "ast/ast.h" +#include "ast/rewriter/th_rewriter.h" #include "ast/sls/sls_stats.h" #include "ast/sls/sls_powers.h" #include "ast/sls/sls_valuation.h" @@ -31,6 +32,7 @@ namespace bv { class sls_terms { ast_manager& m; bv_util bv; + th_rewriter m_rewriter; ptr_vector m_todo, m_args; expr_ref_vector m_assertions, m_pinned, m_translated; app_ref_vector m_terms; @@ -40,12 +42,14 @@ namespace bv { expr* ensure_binary(expr* e); void ensure_binary_core(expr* e); - expr* mk_sdiv(expr* x, expr* y); - expr* mk_smod(expr* x, expr* y); - expr* mk_srem(expr* x, expr* y); + expr_ref mk_sdiv(expr* x, expr* y); + expr_ref mk_smod(expr* x, expr* y); + expr_ref mk_srem(expr* x, expr* y); public: sls_terms(ast_manager& m); + + void updt_params(params_ref const& p); /** * Add constraints diff --git a/src/ast/sls/sls_engine.cpp b/src/ast/sls/sls_engine.cpp index 249c771ed..a2ab861c0 100644 --- a/src/ast/sls/sls_engine.cpp +++ b/src/ast/sls/sls_engine.cpp @@ -421,6 +421,7 @@ lbool sls_engine::search() { // get candidate variables ptr_vector & to_evaluate = m_tracker.get_unsat_constants(m_assertions); + if (to_evaluate.empty()) { res = l_true; @@ -514,6 +515,12 @@ lbool sls_engine::operator()() { if (m_restart_init) m_tracker.randomize(m_assertions); + return search_loop(); +} + + +lbool sls_engine::search_loop() { + lbool res = l_undef; do { @@ -533,7 +540,6 @@ lbool sls_engine::operator()() { } while (res != l_true && m_stats.m_restarts++ < m_max_restarts); verbose_stream() << "(restarts: " << m_stats.m_restarts << " flips: " << m_stats.m_moves << " fps: " << (m_stats.m_moves / m_stats.m_stopwatch.get_current_seconds()) << ")" << std::endl; - return res; } diff --git a/src/ast/sls/sls_engine.h b/src/ast/sls/sls_engine.h index 614534f1a..3e67aa49c 100644 --- a/src/ast/sls/sls_engine.h +++ b/src/ast/sls/sls_engine.h @@ -79,7 +79,11 @@ public: void mk_inv(unsigned bv_sz, const mpz & old_value, mpz & inverted); void mk_flip(sort * s, const mpz & old_value, unsigned bit, mpz & flipped); - lbool search(); + + + lbool search(); + + lbool search_loop(); lbool operator()(); diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index 3160e5cf5..3f619df05 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -106,10 +106,12 @@ namespace bv { bool sls_valuation::commit_eval() { for (unsigned i = 0; i < nw; ++i) - if (0 != (fixed[i] & (m_bits[i] ^ eval[i]))) - return false; - if (!in_range(eval)) + if (0 != (fixed[i] & (m_bits[i] ^ eval[i]))) + return false; + + if (!in_range(eval)) return false; + for (unsigned i = 0; i < nw; ++i) m_bits[i] = eval[i]; SASSERT(well_formed()); @@ -491,8 +493,8 @@ namespace bv { SASSERT(well_formed()); } - void sls_valuation::add_range(rational l, rational h) { - + void sls_valuation::add_range(rational l, rational h) { + l = mod(l, rational::power_of_two(bw)); h = mod(h, rational::power_of_two(bw)); if (h == l) @@ -509,21 +511,28 @@ namespace bv { auto old_lo = lo(); auto old_hi = hi(); if (old_lo < old_hi) { - if (old_lo < l && l < old_hi) + if (old_lo < l && l < old_hi && old_hi <= h) set_value(m_lo, l), old_lo = l; - if (old_hi < h && h < old_hi) + if (l <= old_lo && old_lo < h && h < old_hi) set_value(m_hi, h); } else { SASSERT(old_hi < old_lo); - if (old_lo < l || l < old_hi) - set_value(m_lo, l), - old_lo = l; - if (old_lo < h && h < old_hi) + if (h <= old_hi && old_lo <= l) { + set_value(m_lo, l); set_value(m_hi, h); - else if (old_hi < old_lo && (h < old_hi || old_lo < h)) + } + else if (old_lo <= l && l <= h) { + set_value(m_lo, l); set_value(m_hi, h); + } + else if (old_lo + 1 == l) { + set_value(m_lo, l); + } + else if (old_hi == h + 1) { + set_value(m_hi, h); + } } } @@ -552,8 +561,7 @@ namespace bv { // lo < hi, set most significant bits based on hi // void sls_valuation::tighten_range() { - - // verbose_stream() << "tighten " << *this << "\n"; + if (m_lo == m_hi) return; @@ -613,6 +621,9 @@ namespace bv { break; } + if (has_range() && !in_range(m_bits)) + m_bits = m_lo; + SASSERT(well_formed()); } diff --git a/src/params/sls_params.pyg b/src/params/sls_params.pyg index 05405ef24..18b8d3371 100644 --- a/src/params/sls_params.pyg +++ b/src/params/sls_params.pyg @@ -3,6 +3,7 @@ def_module_params('sls', description='Experimental Stochastic Local Search Solver (for QFBV only).', params=(max_memory_param(), ('max_restarts', UINT, UINT_MAX, 'maximum number of restarts'), + ('max_repairs', UINT, 1000, 'maximum number of repairs before restart'), ('walksat', BOOL, 1, 'use walksat assertion selection (instead of gsat)'), ('walksat_ucb', BOOL, 1, 'use bandit heuristic for walksat assertion selection (instead of random)'), ('walksat_ucb_constant', DOUBLE, 20.0, 'the ucb constant c in the term score + c * f(touched)'), diff --git a/src/sat/smt/sls_solver.cpp b/src/sat/smt/sls_solver.cpp index 8feb9f83e..ae8620e28 100644 --- a/src/sat/smt/sls_solver.cpp +++ b/src/sat/smt/sls_solver.cpp @@ -61,9 +61,10 @@ namespace sls { m_m = alloc(ast_manager, m); ast_translation tr(m, *m_m); + params_ref p; m_completed = false; m_result = l_undef; - m_bvsls = alloc(bv::sls, *m_m); + m_bvsls = alloc(bv::sls, *m_m, p); // walk clauses, add them // walk trail stack until search level, add units // encapsulate bvsls within the arguments of run-local-search. diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 198204d90..520682d1b 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -134,7 +134,7 @@ public: bv_sls_tactic(ast_manager& _m, params_ref const& p) : m(_m), m_params(p) { - m_sls = alloc(bv::sls, m); + m_sls = alloc(bv::sls, m, p); } tactic* translate(ast_manager& m) override { @@ -172,12 +172,12 @@ public: m_sls->init_eval(false_eval); lbool res = m_sls->operator()(); - auto const& stats = m_sls->get_stats(); - report_tactic_progress("Number of flips:", stats.m_moves); - IF_VERBOSE(20, verbose_stream() << res << "\n"); - IF_VERBOSE(20, m_sls->display(verbose_stream())); m_st.reset(); m_sls->collect_statistics(m_st); + report_tactic_progress("Number of flips:", m_sls->get_num_moves()); + IF_VERBOSE(20, verbose_stream() << res << "\n"); + IF_VERBOSE(20, m_sls->display(verbose_stream())); + if (res == l_true) { if (g->models_enabled()) { model_ref mdl = m_sls->get_model(); @@ -207,7 +207,7 @@ public: void cleanup() override { - auto* d = alloc(bv::sls, m); + auto* d = alloc(bv::sls, m, m_params); std::swap(d, m_sls); dealloc(d); } @@ -235,12 +235,6 @@ tactic* mk_bv_sls_tactic(ast_manager& m, params_ref const& p) { static tactic * mk_preamble(ast_manager & m, params_ref const & p) { - params_ref main_p; - main_p.set_bool("elim_and", true); - // main_p.set_bool("pull_cheap_ite", true); - main_p.set_bool("push_ite_bv", true); - main_p.set_bool("blast_distinct", true); - main_p.set_bool("hi_div0", true); params_ref simp2_p = p; simp2_p.set_bool("som", true); @@ -249,18 +243,15 @@ static tactic * mk_preamble(ast_manager & m, params_ref const & p) { simp2_p.set_bool("local_ctx", true); simp2_p.set_uint("local_ctx_limit", 10000000); - params_ref hoist_p; + params_ref hoist_p = p; hoist_p.set_bool("hoist_mul", true); hoist_p.set_bool("som", false); - params_ref gaussian_p; + params_ref gaussian_p = p; // conservative gaussian elimination. gaussian_p.set_uint("gaussian_max_occs", 2); - params_ref ctx_p; - ctx_p.set_uint("max_depth", 32); - ctx_p.set_uint("max_steps", 5000000); - return and_then(and_then(mk_simplify_tactic(m), + return and_then(and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m), using_params(mk_solve_eqs_tactic(m), gaussian_p), mk_elim_uncnstr_tactic(m), @@ -278,7 +269,9 @@ tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { } tactic* mk_qfbv_new_sls_tactic(ast_manager& m, params_ref const& p) { - tactic* t = and_then(mk_preamble(m, p), mk_bv_sls_tactic(m, p)); - t->updt_params(p); + params_ref q = p; + q.set_bool("elim_sign_ext", false); + tactic* t = and_then(mk_preamble(m, q), mk_bv_sls_tactic(m, q)); + t->updt_params(q); return t; } From 84092cbd96a1d4c65bea6db2370807b19519704e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 Mar 2024 15:12:32 -0700 Subject: [PATCH 13/49] add engine-init to control model transfer Signed-off-by: Nikolaj Bjorner --- src/ast/sls/bv_sls.cpp | 24 +++++++++++++++++------- src/ast/sls/bv_sls.h | 1 + 2 files changed, 18 insertions(+), 7 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index 6a176016f..12b11adf9 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -101,16 +101,24 @@ namespace bv { std::function eval = [&](expr* e, unsigned i) { unsigned id = e->get_id(); - bool keep = (m_rand() % 100 <= 50) || !m_to_repair.contains(id); - if (m.is_bool(e) && (m_eval.is_fixed0(e) || keep)) - return m_eval.bval0(e); + bool keep = !m_to_repair.contains(id); + if (m.is_bool(e)) { + if (m_eval.is_fixed0(e) || keep) + return m_eval.bval0(e); + if (m_engine_init) { + auto const& z = m_engine.get_value(e); + return rational(z).get_bit(0); + } + } else if (bv.is_bv(e)) { auto& w = m_eval.wval(e); if (w.fixed.get(i) || keep) return w.get_bit(i); - //auto const& z = m_engine.get_value(e); - //return rational(z).get_bit(i); - } + if (m_engine_init) { + auto const& z = m_engine.get_value(e); + return rational(z).get_bit(i); + } + } return m_rand() % 2 == 0; }; @@ -177,7 +185,8 @@ namespace bv { else if (m_stats.m_restarts % 1000 == 0) res = m_engine.search_loop(); if (res != l_undef) - m_engine_model = true; + m_engine_model = true; + m_engine_init = true; return res; } @@ -187,6 +196,7 @@ namespace bv { m_stats.reset(); m_stats.m_restarts = 0; m_engine_model = false; + m_engine_init = false; do { res = search1(); diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index ae7d7cb57..b1a7f51df 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -52,6 +52,7 @@ namespace bv { config m_config; sls_engine m_engine; bool m_engine_model = false; + bool m_engine_init = false; std::pair next_to_repair(); From 918ac2b1760c7fcea3df80208cf554cc47e77a5d Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 1 Apr 2024 17:25:50 +0100 Subject: [PATCH 14/49] =?UTF-8?q?fix=20#7196:=20make=20the=20code=20C++23?= =?UTF-8?q?=20compatible=20Nikolaj=20is=20now=20more=20bleeding=20edge=20t?= =?UTF-8?q?han=20I=20am...=20I=20must=20be=20getting=20old=3F=20(=CB=98?= =?UTF-8?q?=EF=BD=A5=5F=EF=BD=A5=CB=98)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/util/buffer.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/buffer.h b/src/util/buffer.h index f40914638..3ca597af2 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -21,7 +21,7 @@ Revision History: --*/ #pragma once -#include +#include #include "util/memory_manager.h" template @@ -30,7 +30,7 @@ protected: T * m_buffer = reinterpret_cast(m_initial_buffer); unsigned m_pos = 0; unsigned m_capacity = INITIAL_SIZE; - typename std::aligned_storage::type m_initial_buffer[INITIAL_SIZE]; + alignas(T) std::byte m_initial_buffer[INITIAL_SIZE * sizeof(T)]; void free_memory() { if (m_buffer != reinterpret_cast(m_initial_buffer)) { From 2ce202db755d3e955ae036c9e21efaaed1143573 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Apr 2024 21:08:59 -0700 Subject: [PATCH 15/49] add special handling of lshr, ashr --- src/ast/sls/bv_sls.cpp | 2 +- src/ast/sls/bv_sls_eval.cpp | 270 +++++++++++++++++++++++++++++++++- src/ast/sls/bv_sls_eval.h | 4 + src/ast/sls/sls_valuation.cpp | 107 +++++++++++--- src/ast/sls/sls_valuation.h | 20 ++- 5 files changed, 376 insertions(+), 27 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index 12b11adf9..b94d762cf 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -203,7 +203,7 @@ namespace bv { if (res != l_undef) break; trace(); - res = search2(); + // res = search2(); if (res != l_undef) break; reinit_eval(); diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 579bc7369..2e83f1729 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -84,10 +84,13 @@ namespace bv { return false; auto v = alloc_valuation(e); m_values.set(e->get_id(), v); - if (bv.is_sign_ext(e)) { - unsigned p = e->get_parameter(0).get_int(); - v->set_signed(p); - } + expr* x, * y; + rational val; + if (bv.is_sign_ext(e)) + v->set_signed(e->get_parameter(0).get_int()); + else if (bv.is_bv_ashr(e, x, y) && bv.is_numeral(y, val) && + val.is_unsigned() && val.get_unsigned() <= bv.get_bv_size(e)) + v->set_signed(val.get_unsigned()); return true; } @@ -1349,6 +1352,13 @@ namespace bv { } bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) { + if (true) { + if (i == 0) + return try_repair_ashr0(e, a, b); + else + return try_repair_ashr1(e, a, b); + } + if (i == 0) { unsigned sh = b.to_nat(b.bw); if (sh == 0) @@ -1382,7 +1392,259 @@ namespace bv { } bool sls_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) { +#if 0 return try_repair_ashr(e, a, b, i); +#else + if (i == 0) + return try_repair_lshr0(e, a, b); + else + return try_repair_lshr1(e, a, b); +#endif + } + + /** + * strong: + * - e = (e << b) >> b -> a := e << b, upper b bits set random + * weak: + * - e = 0 -> a := random + * - e > 0 -> a := random with msb(a) >= msb(e) + */ + bool sls_eval::try_repair_lshr0(bvect const& e, bvval& a, bvval const& b) { + + auto& t = m_tmp; + // t := e << b + // t := t >> b + t.set_shift_left(e, b.bits()); + t.set_shift_right(t, b.bits()); + bool use_strong = m_rand(10) != 0; + if (t == e && use_strong) { + t.set_shift_left(e, b.bits()); + unsigned n = b.bits().to_nat(e.bw); + for (unsigned i = e.bw; i-- > e.bw - n;) + t.set(i, a.get_bit(i)); + a.clear_overflow_bits(t); + if (a.set_repair(random_bool(), t)) + return true; + } + + unsigned sh = b.to_nat(b.bw); + if (sh == 0 && a.try_set(e)) + return true; + else if (sh >= b.bw) + return true; + else if (sh < b.bw && m_rand(20) != 0) { + // e = a >> sh + // a[bw-1:sh] = e[bw-sh-1:0] + // a[sh-1:0] = a[sh-1:0] + for (unsigned i = sh; i < a.bw; ++i) + t.set(i, e.get(i - sh)); + for (unsigned i = 0; i < sh; ++i) + t.set(i, a.get_bit(i)); + a.clear_overflow_bits(t); + if (a.try_set(t)) + return true; + } + + //bool r = try_repair_ashr(e, a, const_cast(b), 0); + //verbose_stream() << "repair lshr0 " << e << " b: " << b << " a: " << a << "\n"; + //return r; + + a.get_variant(t, m_rand); + + unsigned msb = a.msb(e); + if (msb > a.msb(t)) { + unsigned num_flex = 0; + for (unsigned i = e.bw; i-- >= msb;) + if (!a.fixed.get(i)) + ++num_flex; + if (num_flex == 0) + return false; + unsigned n = m_rand(num_flex); + for (unsigned i = e.bw; i-- >= msb;) { + if (!a.fixed.get(i)) { + if (n == 0) { + t.set(i, true); + break; + } + else + n--; + } + } + } + return a.set_repair(random_bool(), t); + } + + /** + * strong: + * - clz(a) <= clz(e), e = 0 or (a >> (clz(e) - clz(a)) = e + * - e = 0 and a = 0: b := random + * - e = 0 and a != 0: b := random, such that shift <= b + * - e != 0: b := shift + * where shift := clz(e) - clz(a) + * + * weak: + * - e = 0: b := random + * - e > 0: b := random >= clz(e) + */ + bool sls_eval::try_repair_lshr1(bvect const& e, bvval const& a, bvval& b) { + + auto& t = m_tmp; + auto clza = a.clz(a.bits()); + auto clze = a.clz(e); + t.set_bw(a.bw); + + // strong + if (m_rand(10) != 0 && clza <= clze && (a.is_zero(e) || t.set_shift_right(a.bits(), clze - clza) == e)) { + if (a.is_zero(e) && a.is_zero()) + return true; + unsigned shift = clze - clza; + if (a.is_zero(e)) + shift = m_rand(a.bw + 1 - shift) + shift; + + b.set(t, shift); + if (b.try_set(t)) + return true; + } + + // no change + if (m_rand(10) != 0) { + if (a.is_zero(e)) + return true; + if (b.bits() <= clze) + return true; + } + + // weak + b.get_variant(t, m_rand); + if (a.is_zero(e)) + return b.set_repair(random_bool(), t); + else { + for (unsigned i = 0; i < 4; ++i) { + for (unsigned i = a.bw; !(t <= clze) && i-- > 0; ) + if (!b.fixed.get(i)) + t.set(i, false); + if (t <= clze && b.set_repair(random_bool(), t)) + return true; + b.get_variant(t, m_rand); + } + return false; + } + } + + /** + * strong: + * b < |b| => (e << b) >>a b = e) + * b >= |b| => (e = ones || e = 0) + * - if b < |b|: a := e << b + * - if b >= |b|: a[bw-1] := e = ones + * weak: + * + */ + bool sls_eval::try_repair_ashr0(bvect const& e, bvval& a, bvval const& b) { + auto& t = m_tmp; + t.set_bw(b.bw); + auto n = b.msb(b.bits()); + bool use_strong = m_rand(20) != 0; + if (use_strong && n < b.bw) { + t.set_shift_left(e, b.bits()); + bool sign = t.get(b.bw-1); + t.set_shift_right(t, b.bits()); + if (sign) { + for (unsigned i = b.bw; i-- > b.bw - n; ) + t.set(i, true); + } + use_strong &= t == e; + } + else { + use_strong &= a.is_zero(e) || a.is_ones(e); + } + if (use_strong) { + if (n < b.bw) { + t.set_shift_left(e, b.bits()); + for (unsigned i = 0; i < n; ++i) + t.set(i, a.get_bit(i)); + } + else { + for (unsigned i = 0; i < b.nw; ++i) + t[i] = a.bits()[i]; + t.set(b.bw - 1, a.is_ones(e)); + } + a.clear_overflow_bits(t); + if (a.set_repair(random_bool(), t)) + return true; + } + if (m_rand(10) != 0) { + if (n < b.bw) { + t.set_shift_left(e, b.bits()); + for (unsigned i = 0; i < n; ++i) + t.set(i, random_bool()); + } + else { + a.get_variant(t, m_rand); + t.set(b.bw - 1, a.is_ones(e)); + } + a.clear_overflow_bits(t); + if (a.set_repair(random_bool(), t)) + return true; + } + + a.get_variant(t, m_rand); + return a.set_repair(random_bool(), t); + } + + /* + * strong: + * - clz(a) <= clz(e), e = 0 or (a >>a (clz(e) - clz(a)) = e + * - e = 0 and a = 0: b := random + * - e = 0 and a != 0: b := random, such that shift <= b + * - e != 0: b := shift + * where shift := clz(e) - clz(a) + * + * weak: + * - e = 0: b := random + * - e > 0: b := random >= clz(e) + */ + + bool sls_eval::try_repair_ashr1(bvect const& e, bvval const& a, bvval& b) { + + auto& t = m_tmp; + auto clza = a.clz(a.bits()); + auto clze = a.clz(e); + t.set_bw(a.bw); + + // strong unsigned + if (!a.get_bit(a.bw - 1) && m_rand(10) != 0 && clza <= clze && (a.is_zero(e) || t.set_shift_right(a.bits(), clze - clza) == e)) { + if (a.is_zero(e) && a.is_zero()) + return true; + unsigned shift = clze - clza; + if (a.is_zero(e)) + shift = m_rand(a.bw + 1 - shift) + shift; + + b.set(t, shift); + if (b.try_set(t)) + return true; + } + // strong signed + if (a.get_bit(a.bw - 1) && m_rand(10) != 0 && clza >= clze) { + t.set_shift_right(a.bits(), clza - clze); + for (unsigned i = a.bw; i-- > a.bw - clza + clze; ) + t.set(i, true); + if (e == t) { + if (a.is_zero(e) && a.is_zero()) + return true; + unsigned shift = clze - clza; + if (a.is_zero(e)) + shift = m_rand(a.bw + 1 - shift) + shift; + + b.set(t, shift); + if (b.try_set(t)) + return true; + } + } + + // weak + b.get_variant(t, m_rand); + return b.set_repair(random_bool(), t); } bool sls_eval::try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i) { diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index 5422d5b7c..ebd360481 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -93,6 +93,10 @@ namespace bv { bool try_repair_shl(bvect const& e, bvval& a, bvval& b, unsigned i); bool try_repair_ashr(bvect const& e, bvval& a, bvval& b, unsigned i); bool try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i); + bool try_repair_lshr0(bvect const& e, bvval& a, bvval const& b); + bool try_repair_lshr1(bvect const& e, bvval const& a, bvval& b); + bool try_repair_ashr0(bvect const& e, bvval& a, bvval const& b); + bool try_repair_ashr1(bvect const& e, bvval const& a, bvval& b); bool try_repair_bit2bool(bvval& a, unsigned idx); bool try_repair_udiv(bvect const& e, bvval& a, bvval& b, unsigned i); bool try_repair_urem(bvect const& e, bvval& a, bvval& b, unsigned i); diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index 3f619df05..c251d15ec 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -56,6 +56,20 @@ namespace bv { return mpn_manager().compare(a.data(), a.nw, b.data(), a.nw) >= 0; } + bool operator<=(digit_t a, bvect const& b) { + for (unsigned i = 1; i < b.nw; ++i) + if (0 != b[i]) + return true; + return mpn_manager().compare(&a, 1, b.data(), 1) <= 0; + } + + bool operator<=(bvect const& a, digit_t b) { + for (unsigned i = 1; i < a.nw; ++i) + if (0 != a[i]) + return false; + return mpn_manager().compare(a.data(), 1, &b, 1) <= 0; + } + std::ostream& operator<<(std::ostream& out, bvect const& v) { out << std::hex; bool nz = false; @@ -83,6 +97,57 @@ namespace bv { return r; } + + unsigned bvect::to_nat(unsigned max_n) const { + SASSERT(max_n < UINT_MAX / 2); + unsigned p = 1; + unsigned value = 0; + for (unsigned i = 0; i < bw; ++i) { + if (p >= max_n) { + for (unsigned j = i; j < bw; ++j) + if (get(j)) + return max_n; + return value; + } + if (get(i)) + value += p; + p <<= 1; + } + return value; + } + + bvect& bvect::set_shift_right(bvect const& a, bvect const& b) { + SASSERT(a.bw == b.bw); + unsigned shift = b.to_nat(b.bw); + return set_shift_right(a, shift); + } + + bvect& bvect::set_shift_right(bvect const& a, unsigned shift) { + set_bw(a.bw); + if (shift == 0) + a.copy_to(a.nw, *this); + else if (shift >= a.bw) + set_zero(); + else + for (unsigned i = 0; i < bw; ++i) + set(i, i + shift < bw ? a.get(i + shift) : false); + return *this; + } + + bvect& bvect::set_shift_left(bvect const& a, bvect const& b) { + set_bw(a.bw); + SASSERT(a.bw == b.bw); + unsigned shift = b.to_nat(b.bw); + if (shift == 0) + a.copy_to(a.nw, *this); + else if (shift >= a.bw) + set_zero(); + else + for (unsigned i = bw; i-- > 0; ) + set(i, i >= shift ? a.get(i - shift) : false); + return *this; + } + sls_valuation::sls_valuation(unsigned bw) { set_bw(bw); m_lo.set_bw(bw); @@ -411,6 +476,16 @@ namespace bv { return bw; } + unsigned sls_valuation::clz(bvect const& src) const { + SASSERT(!has_overflow(src)); + unsigned i = bw; + for (; i-- > 0; ) + if (!src.get(i)) + return bw - 1 - i; + return bw; + } + + void sls_valuation::set_value(bvect& bits, rational const& n) { for (unsigned i = 0; i < bw; ++i) bits.set(i, n.get_bit(i)); @@ -438,11 +513,14 @@ namespace bv { void sls_valuation::repair_sign_bits(bvect& dst) const { if (m_signed_prefix == 0) return; - bool sign = dst.get(bw - 1); - for (unsigned i = bw; i-- >= bw - m_signed_prefix; ) { + bool sign = m_signed_prefix == bw ? dst.get(bw - 1) : dst.get(bw - m_signed_prefix - 1); + for (unsigned i = bw; i-- > bw - m_signed_prefix; ) { if (dst.get(i) != sign) { if (fixed.get(i)) { - for (unsigned i = bw; i-- >= bw - m_signed_prefix; ) + unsigned j = bw - m_signed_prefix; + if (j > 0 && !fixed.get(j - 1)) + dst.set(j - 1, !sign); + for (unsigned i = bw; i-- > bw - m_signed_prefix; ) if (!fixed.get(i)) dst.set(i, !sign); return; @@ -466,24 +544,11 @@ namespace bv { return in_range(new_bits); } - unsigned sls_valuation::to_nat(unsigned max_n) { + unsigned sls_valuation::to_nat(unsigned max_n) const { + bvect const& d = m_bits; SASSERT(!has_overflow(d)); - SASSERT(max_n < UINT_MAX / 2); - unsigned p = 1; - unsigned value = 0; - for (unsigned i = 0; i < bw; ++i) { - if (p >= max_n) { - for (unsigned j = i; j < bw; ++j) - if (d.get(j)) - return max_n; - return value; - } - if (d.get(i)) - value += p; - p <<= 1; - } - return value; + return d.to_nat(max_n); } void sls_valuation::shift_right(bvect& out, unsigned shift) const { @@ -493,7 +558,9 @@ namespace bv { SASSERT(well_formed()); } - void sls_valuation::add_range(rational l, rational h) { + void sls_valuation::add_range(rational l, rational h) { + + //return; l = mod(l, rational::power_of_two(bw)); h = mod(h, rational::power_of_two(bw)); diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index dcabf04c0..1beba65a4 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -60,13 +60,27 @@ namespace bv { return bw; } + void set_zero() { + for (unsigned i = 0; i < nw; ++i) + (*this)[i] = 0; + } + + bvect& set_shift_right(bvect const& a, bvect const& b); + bvect& set_shift_right(bvect const& a, unsigned shift); + bvect& set_shift_left(bvect const& a, bvect const& b); + rational get_value(unsigned nw) const; + unsigned to_nat(unsigned max_n) const; + + friend bool operator==(bvect const& a, bvect const& b); friend bool operator<(bvect const& a, bvect const& b); friend bool operator>(bvect const& a, bvect const& b); friend bool operator<=(bvect const& a, bvect const& b); friend bool operator>=(bvect const& a, bvect const& b); + friend bool operator<=(digit_t a, bvect const& b); + friend bool operator<=(bvect const& a, digit_t b); friend std::ostream& operator<<(std::ostream& out, bvect const& v); private: @@ -198,6 +212,8 @@ namespace bv { // most significant bit or bw if src = 0 unsigned msb(bvect const& src) const; + unsigned clz(bvect const& src) const; + bool is_power_of2(bvect const& src) const; // retrieve largest number at or below (above) src which is feasible @@ -232,7 +248,7 @@ namespace bv { clear_overflow_bits(eval); } - void set_zero(bvect& out) const { + void set_zero(bvect& out) const { for (unsigned i = 0; i < nw; ++i) out[i] = 0; } @@ -288,7 +304,7 @@ namespace bv { dst[i] = src[i]; } - unsigned to_nat(unsigned max_n); + unsigned to_nat(unsigned max_n) const; std::ostream& display(std::ostream& out) const { out << m_bits; From d7c0e17f9617d641262bf3a5883d87556773cc5f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Apr 2024 21:11:00 -0700 Subject: [PATCH 16/49] fixes to tighten-range --- src/ast/sls/sls_valuation.cpp | 101 +++++++++++++++------------------- src/ast/sls/sls_valuation.h | 11 ++++ 2 files changed, 55 insertions(+), 57 deletions(-) diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index c251d15ec..6ce1c1df2 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -567,9 +567,6 @@ namespace bv { if (h == l) return; - //verbose_stream() << "[" << l << ", " << h << "[\n"; - //verbose_stream() << *this << "\n"; - if (m_lo == m_hi) { set_value(m_lo, l); set_value(m_hi, h); @@ -603,14 +600,11 @@ namespace bv { } } - - SASSERT(!has_overflow(m_lo)); SASSERT(!has_overflow(m_hi)); tighten_range(); SASSERT(well_formed()); - // verbose_stream() << *this << "\n"; } // @@ -632,60 +626,53 @@ namespace bv { if (m_lo == m_hi) return; - if (!in_range(m_bits)) { - // verbose_stream() << "not in range\n"; - bool compatible = true; - for (unsigned i = 0; i < nw && compatible; ++i) - compatible = 0 == (fixed[i] & (m_bits[i] ^ m_lo[i])); - //verbose_stream() << (fixed[0] & (m_bits[0] ^ m_lo[0])) << "\n"; - //verbose_stream() << bw << " " << m_lo[0] << " " << m_bits[0] << "\n"; - if (compatible) { - //verbose_stream() << "compatible\n"; - set(m_bits, m_lo); - } - else { - bvect tmp(m_bits.nw); - tmp.set_bw(bw); - set(tmp, m_lo); - unsigned max_diff = bw; - for (unsigned i = 0; i < bw; ++i) { - if (fixed.get(i) && (m_bits.get(i) ^ m_lo.get(i))) - max_diff = i; - } - SASSERT(max_diff != bw); - - for (unsigned i = 0; i <= max_diff; ++i) - tmp.set(i, fixed.get(i) && m_bits.get(i)); - - bool found0 = false; - for (unsigned i = max_diff + 1; i < bw; ++i) { - if (found0 || m_lo.get(i) || fixed.get(i)) - tmp.set(i, m_lo.get(i) && fixed.get(i)); - else { - tmp.set(i, true); - found0 = true; - } - } - set(m_bits, tmp); - } + bvect hi1(nw); + hi1.set_bw(bw); + m_hi.copy_to(nw, hi1); + sub1(hi1); + unsigned lo_index = 0, hi_index = 0; + for (unsigned i = nw; i-- > 0; ) { + auto lo_diff = (fixed[i] & (m_bits[i] ^ m_lo[i])); + if (lo_diff != 0 && lo_index == 0) + lo_index = 1 + i * 8 * sizeof(digit_t) + log2(lo_diff); + auto hi_diff = (fixed[i] & (m_bits[i] ^ hi1[i])); + if (hi_diff != 0 && hi_index == 0) + hi_index = 1 + i * 8 * sizeof(digit_t) + log2(hi_diff); } - // update lo, hi to be feasible. - - for (unsigned i = bw; i-- > 0; ) { - if (!fixed.get(i)) - continue; - if (m_bits.get(i) == m_lo.get(i)) - continue; - if (m_bits.get(i)) { - m_lo.set(i, true); - for (unsigned j = i; j-- > 0; ) - m_lo.set(j, fixed.get(j) && m_bits.get(j)); + + if (lo_index != 0) { + lo_index--; + SASSERT(m_lo.get(lo_index) != m_bits.get(lo_index)); + SASSERT(fixed.get(lo_index)); + for (unsigned i = 0; i <= lo_index; ++i) { + if (!fixed.get(i)) + m_lo.set(i, false); + else if (fixed.get(i)) + m_lo.set(i, m_bits.get(i)); } - else { - for (unsigned j = bw; j-- > 0; ) - m_lo.set(j, fixed.get(j) && m_bits.get(j)); + for (unsigned i = lo_index + 1; i < bw; ++i) + if (!fixed.get(i) && !m_lo.get(i)) { + m_lo.set(i, true); + break; + } + } + if (hi_index != 0) { + hi_index--; + SASSERT(hi1.get(hi_index) != m_bits.get(hi_index)); + SASSERT(fixed.get(hi_index)); + for (unsigned i = 0; i <= hi_index; ++i) { + if (!fixed.get(i)) + hi1.set(i, true); + else if (fixed.get(i)) + hi1.set(i, m_bits.get(i)); } - break; + for (unsigned i = hi_index + 1; i < bw; ++i) + if (!fixed.get(i) && hi1.get(i)) { + hi1.set(i, false); + break; + } + add1(hi1); + hi1.copy_to(nw, m_hi); } if (has_range() && !in_range(m_bits)) diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 1beba65a4..90794bfe2 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -274,6 +274,17 @@ namespace bv { } } + void add1(bvect& out) const { + for (unsigned i = 0; i < bw; ++i) { + if (!out.get(i)) { + out.set(i, true); + return; + } + else + out.set(i, false); + } + } + void set_sub(bvect& out, bvect const& a, bvect const& b) const; bool set_add(bvect& out, bvect const& a, bvect const& b) const; bool set_mul(bvect& out, bvect const& a, bvect const& b, bool check_overflow = true) const; From bab7ca2b70398e8ea95211691bb678b7bcc9a0c4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 7 Apr 2024 14:24:13 -0700 Subject: [PATCH 17/49] fixes to bv-sls --- src/ast/sls/bv_sls.cpp | 31 ++-- src/ast/sls/bv_sls.h | 2 +- src/ast/sls/bv_sls_eval.cpp | 70 +++------ src/ast/sls/bv_sls_fixed.cpp | 180 +++++++++++++++-------- src/ast/sls/bv_sls_fixed.h | 6 +- src/ast/sls/sls_valuation.cpp | 265 ++++++++++++++-------------------- src/ast/sls/sls_valuation.h | 7 +- src/tactic/sls/sls_tactic.cpp | 4 +- 8 files changed, 279 insertions(+), 286 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index b94d762cf..f799d3cfe 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -124,6 +124,7 @@ namespace bv { }; m_eval.init_eval(m_terms.assertions(), eval); init_repair(); + // m_engine_init = false; } std::pair sls::next_to_repair() { @@ -161,17 +162,18 @@ namespace bv { lbool sls::search1() { // init and init_eval were invoked unsigned n = 0; - for (; n++ < m_config.m_max_repairs && m.inc(); ) { + for (; n < m_config.m_max_repairs && m.inc(); ) { auto [down, e] = next_to_repair(); if (!e) return l_true; - trace_repair(down, e); - + IF_VERBOSE(20, trace_repair(down, e)); + ++m_stats.m_moves; - - if (down) + if (down) { try_repair_down(e); + ++n; + } else try_repair_up(e); } @@ -181,12 +183,13 @@ namespace bv { lbool sls::search2() { lbool res = l_undef; if (m_stats.m_restarts == 0) - res = m_engine(); + res = m_engine(), + m_engine_init = true; else if (m_stats.m_restarts % 1000 == 0) - res = m_engine.search_loop(); + res = m_engine.search_loop(), + m_engine_init = true; if (res != l_undef) m_engine_model = true; - m_engine_init = true; return res; } @@ -203,7 +206,7 @@ namespace bv { if (res != l_undef) break; trace(); - // res = search2(); + //res = search2(); if (res != l_undef) break; reinit_eval(); @@ -223,6 +226,7 @@ namespace bv { VERIFY(m_eval.wval(e).commit_eval()); } + IF_VERBOSE(3, verbose_stream() << "done\n"); for (auto p : m_terms.parents(e)) m_repair_up.insert(p->get_id()); @@ -256,6 +260,7 @@ namespace bv { } } } + IF_VERBOSE(3, verbose_stream() << "init-repair " << mk_bounded_pp(e, m) << "\n"); // repair was not successful, so reset the state to find a different way to repair init_repair(); } @@ -265,7 +270,7 @@ namespace bv { if (m_terms.is_assertion(e)) m_repair_roots.insert(e->get_id()); else if (!m_eval.repair_up(e)) { - //m_repair_roots.insert(e->get_id()); + IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e)); init_repair(); } else { @@ -366,14 +371,14 @@ namespace bv { m_engine.updt_params(q); } - void sls::trace_repair(bool down, expr* e) { - IF_VERBOSE(20, + std::ostream& sls::trace_repair(bool down, expr* e) { verbose_stream() << (down ? "d #" : "u #") << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " "; if (bv.is_bv(e)) verbose_stream() << m_eval.wval(e) << " " << (m_eval.is_fixed0(e) ? "fixed " : " "); if (m.is_bool(e)) verbose_stream() << m_eval.bval0(e) << " "; - verbose_stream() << "\n"); + verbose_stream() << "\n"; + return verbose_stream(); } void sls::trace() { diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index b1a7f51df..01ccbc41f 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -68,7 +68,7 @@ namespace bv { void reinit_eval(); void init_repair(); void trace(); - void trace_repair(bool down, expr* e); + std::ostream& trace_repair(bool down, expr* e); indexed_uint_set m_to_repair; void init_repair_candidates(); diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 2e83f1729..b69cec867 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -1351,55 +1351,18 @@ namespace bv { return false; } - bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) { - if (true) { + bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) { if (i == 0) return try_repair_ashr0(e, a, b); else return try_repair_ashr1(e, a, b); - } - - if (i == 0) { - unsigned sh = b.to_nat(b.bw); - if (sh == 0) - return a.try_set(e); - else if (sh >= b.bw) { - if (e.get(a.bw - 1)) - return a.try_set_bit(a.bw - 1, true); - else - return a.try_set_bit(a.bw - 1, false); - } - else { - // e = a >> sh - // a[bw-1:sh] = e[bw-sh-1:0] - // a[sh-1:0] = a[sh-1:0] - // ignore sign - for (unsigned i = sh; i < a.bw; ++i) - m_tmp.set(i, e.get(i - sh)); - for (unsigned i = 0; i < sh; ++i) - m_tmp.set(i, a.get_bit(i)); - a.clear_overflow_bits(m_tmp); - return a.try_set(m_tmp); - } - } - else { - // NB. blind sub-range of possible values for b - SASSERT(i == 1); - unsigned sh = m_rand(a.bw + 1); - b.set(m_tmp, sh); - return b.try_set(m_tmp); - } } bool sls_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) { -#if 0 - return try_repair_ashr(e, a, b, i); -#else if (i == 0) return try_repair_lshr0(e, a, b); else return try_repair_lshr1(e, a, b); -#endif } /** @@ -1427,22 +1390,25 @@ namespace bv { return true; } + unsigned sh = b.to_nat(b.bw); - if (sh == 0 && a.try_set(e)) - return true; - else if (sh >= b.bw) - return true; - else if (sh < b.bw && m_rand(20) != 0) { - // e = a >> sh - // a[bw-1:sh] = e[bw-sh-1:0] - // a[sh-1:0] = a[sh-1:0] - for (unsigned i = sh; i < a.bw; ++i) - t.set(i, e.get(i - sh)); - for (unsigned i = 0; i < sh; ++i) - t.set(i, a.get_bit(i)); - a.clear_overflow_bits(t); - if (a.try_set(t)) + if (m_rand(20) != 0) { + if (sh == 0 && a.try_set(e)) return true; + else if (sh >= b.bw) + return true; + else if (sh < b.bw && m_rand(20) != 0) { + // e = a >> sh + // a[bw-1:sh] = e[bw-sh-1:0] + // a[sh-1:0] = a[sh-1:0] + for (unsigned i = sh; i < a.bw; ++i) + t.set(i, e.get(i - sh)); + for (unsigned i = 0; i < sh; ++i) + t.set(i, a.get_bit(i)); + a.clear_overflow_bits(t); + if (a.try_set(t)) + return true; + } } //bool r = try_repair_ashr(e, a, const_cast(b), 0); diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index e2b29b1fe..18518ed09 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -53,7 +53,7 @@ namespace bv { // s <=s t <=> s + K <= t + K, K = 2^{bw-1} - void sls_fixed::init_range(app* e, bool sign) { + bool sls_fixed::init_range(app* e, bool sign) { expr* s, * t, * x, * y; rational a, b; unsigned idx; @@ -64,63 +64,116 @@ namespace bv { if (bv.is_ule(e, s, t)) { get_offset(s, x, a); get_offset(t, y, b); - init_range(x, a, y, b, sign); + return init_range(x, a, y, b, sign); } else if (bv.is_ult(e, s, t)) { get_offset(s, x, a); get_offset(t, y, b); - init_range(y, b, x, a, !sign); + return init_range(y, b, x, a, !sign); } else if (bv.is_uge(e, s, t)) { get_offset(s, x, a); get_offset(t, y, b); - init_range(y, b, x, a, sign); + return init_range(y, b, x, a, sign); } else if (bv.is_ugt(e, s, t)) { get_offset(s, x, a); get_offset(t, y, b); - init_range(x, a, y, b, !sign); + return init_range(x, a, y, b, !sign); } else if (bv.is_sle(e, s, t)) { get_offset(s, x, a); get_offset(t, y, b); - init_range(x, a + N(s), y, b + N(s), sign); + return init_range(x, a + N(s), y, b + N(s), sign); } else if (bv.is_slt(e, s, t)) { get_offset(s, x, a); get_offset(t, y, b); - init_range(y, b + N(s), x, a + N(s), !sign); + return init_range(y, b + N(s), x, a + N(s), !sign); } else if (bv.is_sge(e, s, t)) { get_offset(s, x, a); get_offset(t, y, b); - init_range(y, b + N(s), x, a + N(s), sign); + return init_range(y, b + N(s), x, a + N(s), sign); } else if (bv.is_sgt(e, s, t)) { get_offset(s, x, a); get_offset(t, y, b); - init_range(x, a + N(s), y, b + N(s), !sign); + return init_range(x, a + N(s), y, b + N(s), !sign); } - else if (!sign && m.is_eq(e, s, t)) { + else if (m.is_eq(e, s, t)) { if (bv.is_numeral(s, a)) - // t - a <= 0 - init_range(t, -a, nullptr, rational(0), false); + init_eq(t, a, sign); else if (bv.is_numeral(t, a)) - init_range(s, -a, nullptr, rational(0), false); - } - else if (sign && m.is_eq(e, s, t)) { - if (bv.is_numeral(s, a)) - // 1 <= t - a - init_range(nullptr, rational(1), t, -a, false); - else if (bv.is_numeral(t, a)) - init_range(nullptr, rational(1), s, -a, false); + init_eq(s, a, sign); + else + return false; + return true; } else if (bv.is_bit2bool(e, s, idx)) { auto& val = wval(s); val.try_set_bit(idx, !sign); val.fixed.set(idx, true); val.tighten_range(); + return true; } + return false; + } + + bool sls_fixed::init_eq(expr* t, rational const& a, bool sign) { + unsigned lo, hi; + rational b(0); + // verbose_stream() << mk_bounded_pp(t, m) << " == " << a << "\n"; + expr* s = nullptr; + if (sign) + // 1 <= t - a + init_range(nullptr, rational(1), t, -a, false); + else + // t - a <= 0 + init_range(t, -a, nullptr, rational::zero(), false); + if (!sign && bv.is_bv_not(t, s)) { + for (unsigned i = 0; i < bv.get_bv_size(s); ++i) + if (!a.get_bit(i)) + b += rational::power_of_two(i); + init_eq(s, b, false); + return true; + } + if (!sign && bv.is_concat(t) && to_app(t)->get_num_args() == 2) { + auto x = to_app(t)->get_arg(0); + auto y = to_app(t)->get_arg(1); + auto sz = bv.get_bv_size(y); + auto k = rational::power_of_two(sz); + init_eq(y, mod(a, k), false); + init_eq(x, div(a + k - 1, k), false); + return true; + } + if (bv.is_extract(t, lo, hi, s)) { + if (hi == lo) { + sign = sign ? a == 1 : a == 0; + auto& val = wval(s); + if (val.try_set_bit(lo, !sign)) + val.fixed.set(lo, true); + val.tighten_range(); + } + else if (!sign) { + auto& val = wval(s); + for (unsigned i = lo; i <= hi; ++i) + if (val.try_set_bit(i, a.get_bit(i - lo))) + val.fixed.set(i, true); + val.tighten_range(); + // verbose_stream() << lo << " " << hi << " " << val << " := " << a << "\n"; + } + + if (!sign && hi + 1 == bv.get_bv_size(s)) { + // s < 2^lo * (a + 1) + rational b = rational::power_of_two(lo) * (a + 1) - 1; + rational offset; + get_offset(s, t, offset); + // t + offset <= b + init_range(t, offset, nullptr, b, false); + } + } + return true; } // @@ -132,51 +185,66 @@ namespace bv { // a < x + b <=> ! (x + b <= a) <=> x not in [-a, b - a [ <=> x in [b - a, -a [ a != -1 // x + a < x + b <=> ! (x + b <= x + a) <=> x in [-a, -b [ a != b // - void sls_fixed::init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign) { + bool sls_fixed::init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign) { if (!x && !y) - return; - if (!x) { - // a <= y + b - if (a == 0) - return; - auto& v = wval(y); - if (!sign) - v.add_range(a - b, -b); - else - v.add_range(-b, a - b); - } - else if (!y) { + return false; + if (!x) + return add_range(y, a - b, -b, sign); + else if (!y) + return add_range(x, -a, b - a + 1, sign); + else if (x == y) + return add_range(x, -a, -b, sign); + return false; + } - if (mod(b + 1, rational::power_of_two(bv.get_bv_size(x))) == 0) - return; - auto& v = wval(x); - if (!sign) - v.add_range(-a, b - a + 1); - else - v.add_range(b - a + 1, -a); - } - else if (x == y) { - if (a == b) - return; - auto& v = wval(x); - if (!sign) - v.add_range(-a, -b); - else - v.add_range(-b, -a); + bool sls_fixed::add_range(expr* e, rational lo, rational hi, bool sign) { + auto& v = wval(e); + lo = mod(lo, rational::power_of_two(bv.get_bv_size(e))); + hi = mod(hi, rational::power_of_two(bv.get_bv_size(e))); + if (lo == hi) + return false; + if (sign) + std::swap(lo, hi); + v.add_range(lo, hi); + if (v.lo() == 0 && bv.is_concat(e) && to_app(e)->get_num_args() == 2) { + auto x = to_app(e)->get_arg(0); + auto y = to_app(e)->get_arg(1); + auto sz = bv.get_bv_size(y); + auto k = rational::power_of_two(sz); + lo = v.lo(); + hi = v.hi(); + if (hi <= k) { + add_range(y, lo, hi, false); + init_eq(x, lo, false); + } + else { + hi = div(hi + k - 1, k); + add_range(x, lo, hi, false); + } } + return true; } void sls_fixed::get_offset(expr* e, expr*& x, rational& offset) { expr* s, * t; x = e; offset = 0; - if (bv.is_bv_add(e, s, t)) { - if (bv.is_numeral(s, offset)) + rational n; + while (true) { + if (bv.is_bv_add(x, s, t) && bv.is_numeral(s, n)) { x = t; - else if (bv.is_numeral(t, offset)) + offset += n; + continue; + } + if (bv.is_bv_add(x, s, t) && bv.is_numeral(t, n)) { x = s; + offset += n; + continue; + } + break; } - else if (bv.is_numeral(e, offset)) + if (bv.is_numeral(e, n)) + offset += n, x = nullptr; } @@ -264,11 +332,6 @@ namespace bv { case OP_BADD: { auto& a = wval(e->get_arg(0)); auto& b = wval(e->get_arg(1)); - rational r; - if (bv.is_numeral(e->get_arg(0), r) && b.has_range()) - v.add_range(r + b.lo(), r + b.hi()); - else if (bv.is_numeral(e->get_arg(1), r) && a.has_range()) - v.add_range(r + a.lo(), r + a.hi()); bool pfixed = true; for (unsigned i = 0; i < v.bw; ++i) { if (pfixed && a.fixed.get(i) && b.fixed.get(i)) @@ -283,7 +346,6 @@ namespace bv { v.fixed.set(i, false); } } - break; } case OP_BMUL: { diff --git a/src/ast/sls/bv_sls_fixed.h b/src/ast/sls/bv_sls_fixed.h index 14970c20c..73dd5a52c 100644 --- a/src/ast/sls/bv_sls_fixed.h +++ b/src/ast/sls/bv_sls_fixed.h @@ -30,9 +30,11 @@ namespace bv { bv_util& bv; void init_ranges(expr_ref_vector const& es); - void init_range(app* e, bool sign); - void init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign); + bool init_range(app* e, bool sign); + bool init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign); void get_offset(expr* e, expr*& x, rational& offset); + bool init_eq(expr* e, rational const& v, bool sign); + bool add_range(expr* e, rational lo, rational hi, bool sign); void init_fixed_basic(app* e); void init_fixed_bv(app* e); diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index 6ce1c1df2..1f3674e93 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -204,139 +204,69 @@ namespace bv { // // largest dst <= src and dst is feasible - // set dst := src & (~fixed | bits) - // - // increment dst if dst < src by setting bits below msb(src & ~dst) to 1 - // - // if dst < lo < hi: - // return false - // if lo < hi <= dst: - // set dst := hi - 1 - // if hi <= dst < lo - // set dst := hi - 1 - // + // bool sls_valuation::get_at_most(bvect const& src, bvect& dst) const { SASSERT(!has_overflow(src)); - for (unsigned i = 0; i < nw; ++i) - dst[i] = src[i] & (~fixed[i] | m_bits[i]); - - // - // If dst < src, then find the most significant - // bit where src[idx] = 1, dst[idx] = 0 - // set dst[j] = bits_j | ~fixed_j for j < idx - // - for (unsigned i = nw; i-- > 0; ) { - if (0 != (~dst[i] & src[i])) { - auto idx = log2(~dst[i] & src[i]); - auto mask = (1 << idx) - 1; - dst[i] = (~fixed[i] & mask) | dst[i]; - for (unsigned j = i; j-- > 0; ) - dst[j] = (~fixed[j] | m_bits[j]); - break; - } - } - SASSERT(!has_overflow(dst)); - return round_down(dst); + src.copy_to(nw, dst); + sup_feasible(dst); + if (in_range(dst)) { + SASSERT(can_set(dst)); + return true; + } + if (dst < m_lo && m_lo < m_hi) // dst < lo < hi + return false; + if (is_zero(m_hi)) + return false; + m_hi.copy_to(nw, dst); // hi <= dst < lo or lo < hi <= dst + sub1(dst); + SASSERT(can_set(dst)); + return true; } // // smallest dst >= src and dst is feasible with respect to this. - // set dst := (src & ~fixed) | (fixed & bits) - // - // decrement dst if dst > src by setting bits below msb to 0 unless fixed - // - // if lo < hi <= dst - // return false - // if dst < lo < hi: - // set dst := lo - // if hi <= dst < lo - // set dst := lo - // bool sls_valuation::get_at_least(bvect const& src, bvect& dst) const { SASSERT(!has_overflow(src)); - for (unsigned i = 0; i < nw; ++i) - dst[i] = (~fixed[i] & src[i]) | (fixed[i] & m_bits[i]); + src.copy_to(nw, dst); + dst.set_bw(bw); + inf_feasible(dst); + if (in_range(dst)) { + SASSERT(can_set(dst)); + return true; + } - // - // If dst > src, then find the most significant - // bit where src[idx] = 0, dst[idx] = 1 - // set dst[j] = dst[j] & fixed_j for j < idx - // - for (unsigned i = nw; i-- > 0; ) { - if (0 != (dst[i] & ~src[i])) { - auto idx = log2(dst[i] & ~src[i]); - auto mask = (1 << idx); - dst[i] = dst[i] & (fixed[i] | mask); - for (unsigned j = i; j-- > 0; ) - dst[j] = dst[j] & fixed[j]; - break; - } - } - SASSERT(!has_overflow(dst)); - return round_up(dst); - } - - bool sls_valuation::round_up(bvect& dst) const { - if (m_lo < m_hi) { - if (m_hi <= dst) - return false; - if (m_lo > dst) - set(dst, m_lo); - } - else if (m_hi <= dst && m_lo > dst) - set(dst, m_lo); - SASSERT(!has_overflow(dst)); - return true; - } - - bool sls_valuation::round_down(bvect& dst) const { - if (m_lo < m_hi) { - if (m_lo > dst) - return false; - if (m_hi <= dst) { - set(dst, m_hi); - sub1(dst); - } - } - else if (m_hi <= dst && m_lo > dst) { - set(dst, m_hi); - sub1(dst); - } - SASSERT(well_formed()); + if (dst > m_lo) + return false; + m_lo.copy_to(nw, dst); + SASSERT(can_set(dst)); return true; } bool sls_valuation::set_random_at_most(bvect const& src, bvect& tmp, random_gen& r) { if (!get_at_most(src, tmp)) return false; - if (is_zero(tmp) || (0 == r() % 2)) + + if (is_zero(tmp) || (0 != r(10))) return try_set(tmp); - set_random_below(tmp, r); // random value below tmp - - if (m_lo == m_hi || is_zero(m_lo) || m_lo <= tmp) - return try_set(tmp); - - // for simplicity, bail out if we were not lucky - return get_at_most(src, tmp) && try_set(tmp); + set_random_below(tmp, r); + + return (can_set(tmp) || get_at_most(src, tmp)) && try_set(tmp); } bool sls_valuation::set_random_at_least(bvect const& src, bvect& tmp, random_gen& r) { if (!get_at_least(src, tmp)) return false; - if (is_ones(tmp) || (0 == r() % 2)) + + if (is_ones(tmp) || (0 != r(10))) return try_set(tmp); // random value at least tmp set_random_above(tmp, r); - - if (m_lo == m_hi || is_zero(m_hi) || m_hi > tmp) - return try_set(tmp); - // for simplicity, bail out if we were not lucky - return get_at_least(src, tmp) && try_set(tmp); + return (can_set(tmp) || get_at_least(src, tmp)) && try_set(tmp); } bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, bvect& tmp, random_gen& r) { @@ -533,7 +463,7 @@ namespace bv { // // new_bits != bits => ~fixed - // 0 = (new_bits ^ bits) & fixed + // 0 = (new_bits ^ bits) & fixedf // also check that new_bits are in range // bool sls_valuation::can_set(bvect const& new_bits) const { @@ -559,14 +489,16 @@ namespace bv { } void sls_valuation::add_range(rational l, rational h) { - - //return; + return; + //verbose_stream() << *this << " " << l << " " << h << " --> \n"; l = mod(l, rational::power_of_two(bw)); h = mod(h, rational::power_of_two(bw)); if (h == l) return; +// verbose_stream() << *this << " " << l << " " << h << " --> "; + if (m_lo == m_hi) { set_value(m_lo, l); set_value(m_hi, h); @@ -591,19 +523,25 @@ namespace bv { set_value(m_lo, l); set_value(m_hi, h); } - else if (old_lo + 1 == l) { + else if (old_lo + 1 == l) + set_value(m_lo, l); + else if (old_hi == h + 1) + set_value(m_hi, h); + else if (old_hi == h && old_lo < l) set_value(m_lo, l); - } - else if (old_hi == h + 1) { + else if (old_lo == l && h < old_hi) set_value(m_hi, h); - } } } SASSERT(!has_overflow(m_lo)); SASSERT(!has_overflow(m_hi)); + //verbose_stream() << *this << " --> "; + tighten_range(); + + //verbose_stream() << *this << "\n"; SASSERT(well_formed()); } @@ -621,59 +559,76 @@ namespace bv { // lo + 1 = hi -> set bits = lo // lo < hi, set most significant bits based on hi // + + unsigned sls_valuation::diff_index(bvect const& a) const { + unsigned index = 0; + for (unsigned i = nw; i-- > 0; ) { + auto diff = fixed[i] & (m_bits[i] ^ a[i]); + if (diff != 0 && index == 0) + index = 1 + i * 8 * sizeof(digit_t) + log2(diff); + } + return index; + } + + void sls_valuation::inf_feasible(bvect& a) const { + unsigned lo_index = diff_index(a); + + if (lo_index != 0) { + lo_index--; + SASSERT(a.get(lo_index) != m_bits.get(lo_index)); + SASSERT(fixed.get(lo_index)); + for (unsigned i = 0; i <= lo_index; ++i) { + if (!fixed.get(i)) + a.set(i, false); + else if (fixed.get(i)) + a.set(i, m_bits.get(i)); + } + if (!a.get(lo_index)) { + for (unsigned i = lo_index + 1; i < bw; ++i) + if (!fixed.get(i) && !a.get(i)) { + a.set(i, true); + break; + } + } + } + } + + void sls_valuation::sup_feasible(bvect& a) const { + unsigned hi_index = diff_index(a); + if (hi_index != 0) { + hi_index--; + SASSERT(a.get(hi_index) != m_bits.get(hi_index)); + SASSERT(fixed.get(hi_index)); + for (unsigned i = 0; i <= hi_index; ++i) { + if (!fixed.get(i)) + a.set(i, true); + else if (fixed.get(i)) + a.set(i, m_bits.get(i)); + } + if (a.get(hi_index)) { + for (unsigned i = hi_index + 1; i < bw; ++i) + if (!fixed.get(i) && a.get(i)) { + a.set(i, false); + break; + } + } + } + } + void sls_valuation::tighten_range() { if (m_lo == m_hi) return; + inf_feasible(m_lo); + bvect hi1(nw); hi1.set_bw(bw); m_hi.copy_to(nw, hi1); sub1(hi1); - unsigned lo_index = 0, hi_index = 0; - for (unsigned i = nw; i-- > 0; ) { - auto lo_diff = (fixed[i] & (m_bits[i] ^ m_lo[i])); - if (lo_diff != 0 && lo_index == 0) - lo_index = 1 + i * 8 * sizeof(digit_t) + log2(lo_diff); - auto hi_diff = (fixed[i] & (m_bits[i] ^ hi1[i])); - if (hi_diff != 0 && hi_index == 0) - hi_index = 1 + i * 8 * sizeof(digit_t) + log2(hi_diff); - } - - if (lo_index != 0) { - lo_index--; - SASSERT(m_lo.get(lo_index) != m_bits.get(lo_index)); - SASSERT(fixed.get(lo_index)); - for (unsigned i = 0; i <= lo_index; ++i) { - if (!fixed.get(i)) - m_lo.set(i, false); - else if (fixed.get(i)) - m_lo.set(i, m_bits.get(i)); - } - for (unsigned i = lo_index + 1; i < bw; ++i) - if (!fixed.get(i) && !m_lo.get(i)) { - m_lo.set(i, true); - break; - } - } - if (hi_index != 0) { - hi_index--; - SASSERT(hi1.get(hi_index) != m_bits.get(hi_index)); - SASSERT(fixed.get(hi_index)); - for (unsigned i = 0; i <= hi_index; ++i) { - if (!fixed.get(i)) - hi1.set(i, true); - else if (fixed.get(i)) - hi1.set(i, m_bits.get(i)); - } - for (unsigned i = hi_index + 1; i < bw; ++i) - if (!fixed.get(i) && hi1.get(i)) { - hi1.set(i, false); - break; - } - add1(hi1); - hi1.copy_to(nw, m_hi); - } + sup_feasible(hi1); + add1(hi1); + hi1.copy_to(nw, m_hi); if (has_range() && !in_range(m_bits)) m_bits = m_lo; diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 90794bfe2..04efec24a 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -113,8 +113,6 @@ namespace bv { unsigned m_signed_prefix = 0; unsigned mask; - bool round_up(bvect& dst) const; - bool round_down(bvect& dst) const; void repair_sign_bits(bvect& dst) const; @@ -141,9 +139,11 @@ namespace bv { SASSERT(in_range(m_bits)); if (fixed.get(i) && get_bit(i) != b) return false; + m_bits.set(i, b); eval.set(i, b); if (in_range(m_bits)) return true; + m_bits.set(i, !b); eval.set(i, !b); return false; } @@ -155,6 +155,9 @@ namespace bv { rational lo() const { return m_lo.get_value(nw); } rational hi() const { return m_hi.get_value(nw); } + unsigned diff_index(bvect const& a) const; + void inf_feasible(bvect& a) const; + void sup_feasible(bvect& a) const; void get(bvect& dst) const; void add_range(rational lo, rational hi); diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 520682d1b..f484372c8 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -175,8 +175,8 @@ public: m_st.reset(); m_sls->collect_statistics(m_st); report_tactic_progress("Number of flips:", m_sls->get_num_moves()); - IF_VERBOSE(20, verbose_stream() << res << "\n"); - IF_VERBOSE(20, m_sls->display(verbose_stream())); + IF_VERBOSE(10, verbose_stream() << res << "\n"); + IF_VERBOSE(10, m_sls->display(verbose_stream())); if (res == l_true) { if (g->models_enabled()) { From 9a681b1a37afaaceb4e3b70e94ec3c40f85a07d1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Apr 2024 10:44:53 -0700 Subject: [PATCH 18/49] reorg sls Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.h | 1 + src/ast/sls/bv_sls.cpp | 92 ++++++----------------- src/ast/sls/bv_sls.h | 2 - src/ast/sls/bv_sls_eval.cpp | 135 +++++++++++++++++++++++----------- src/ast/sls/bv_sls_eval.h | 14 ++++ src/ast/sls/bv_sls_fixed.cpp | 51 +++++++++++-- src/ast/sls/bv_sls_fixed.h | 1 + src/ast/sls/sls_valuation.cpp | 10 ++- src/ast/sls/sls_valuation.h | 4 + src/math/lp/nla_core.cpp | 22 ++++-- 10 files changed, 207 insertions(+), 125 deletions(-) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 137dc754f..58445afda 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -438,6 +438,7 @@ public: MATCH_BINARY(is_bv_xor); MATCH_BINARY(is_bv_nand); MATCH_BINARY(is_bv_nor); + MATCH_BINARY(is_concat); MATCH_BINARY(is_bv_uremi); diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index f799d3cfe..df741dac3 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -56,18 +56,13 @@ namespace bv { } } for (auto* t : m_terms.terms()) { - if (t && !re_eval_is_correct(t)) + if (t && !m_eval.re_eval_is_correct(t)) m_repair_roots.insert(t->get_id()); } } void sls::init_repair_goal(app* t) { - if (m.is_bool(t)) - m_eval.set(t, m_eval.bval1(t)); - else if (bv.is_bv(t)) { - auto& v = m_eval.wval(t); - v.bits().copy_to(v.nw, v.eval); - } + m_eval.init_eval(t); } void sls::init_repair_candidates() { @@ -149,7 +144,7 @@ namespace bv { SASSERT(m_eval.bval0(e)); return { true, e }; } - if (!re_eval_is_correct(e)) { + if (!m_eval.re_eval_is_correct(e)) { init_repair_goal(e); return { true, e }; } @@ -162,7 +157,7 @@ namespace bv { lbool sls::search1() { // init and init_eval were invoked unsigned n = 0; - for (; n < m_config.m_max_repairs && m.inc(); ) { + for (; n < m_config.m_max_repairs && m.inc(); ++n) { auto [down, e] = next_to_repair(); if (!e) return l_true; @@ -170,10 +165,8 @@ namespace bv { IF_VERBOSE(20, trace_repair(down, e)); ++m_stats.m_moves; - if (down) { - try_repair_down(e); - ++n; - } + if (down) + try_repair_down(e); else try_repair_up(e); } @@ -219,12 +212,7 @@ namespace bv { void sls::try_repair_down(app* e) { unsigned n = e->get_num_args(); if (n == 0) { - if (m.is_bool(e)) { - m_eval.set(e, m_eval.bval1(e)); - } - else { - VERIFY(m_eval.wval(e).commit_eval()); - } + m_eval.commit_eval(e); IF_VERBOSE(3, verbose_stream() << "done\n"); for (auto p : m_terms.parents(e)) @@ -271,44 +259,24 @@ namespace bv { m_repair_roots.insert(e->get_id()); else if (!m_eval.repair_up(e)) { IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e)); - init_repair(); + if (m_rand(10) != 0) { + m_eval.set_random(e); + + m_repair_roots.insert(e->get_id()); + } + else + init_repair(); } else { - if (!eval_is_correct(e)) { + if (!m_eval.eval_is_correct(e)) { verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; } - SASSERT(eval_is_correct(e)); + SASSERT(m_eval.eval_is_correct(e)); for (auto p : m_terms.parents(e)) m_repair_up.insert(p->get_id()); } } - bool sls::eval_is_correct(app* e) { - if (!m_eval.can_eval1(e)) - return false; - if (m.is_bool(e)) - return m_eval.bval0(e) == m_eval.bval1(e); - if (bv.is_bv(e)) { - auto const& v = m_eval.wval(e); - return v.eval == v.bits(); - } - UNREACHABLE(); - return false; - } - - - bool sls::re_eval_is_correct(app* e) { - if (!m_eval.can_eval1(e)) - return false; - if (m.is_bool(e)) - return m_eval.bval0(e) == m_eval.bval1(e); - if (bv.is_bv(e)) { - auto const& v = m_eval.eval(e); - return v.eval == v.bits(); - } - UNREACHABLE(); - return false; - } model_ref sls::get_model() { if (m_engine_model) @@ -317,24 +285,17 @@ namespace bv { model_ref mdl = alloc(model, m); auto& terms = m_eval.sort_assertions(m_terms.assertions()); for (expr* e : terms) { - if (!re_eval_is_correct(to_app(e))) { + if (!m_eval.re_eval_is_correct(to_app(e))) { verbose_stream() << "missed evaluation #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; - if (bv.is_bv(e)) { - auto const& v = m_eval.wval(e); - verbose_stream() << v << "\n" << v.eval << "\n"; - } + m_eval.display_value(verbose_stream(), e) << "\n"; } if (!is_uninterp_const(e)) continue; auto f = to_app(e)->get_decl(); - if (m.is_bool(e)) - mdl->register_decl(f, m.mk_bool_val(m_eval.bval0(e))); - else if (bv.is_bv(e)) { - auto const& v = m_eval.wval(e); - rational n = v.get_value(); - mdl->register_decl(f, bv.mk_numeral(n, v.bw)); - } + auto v = m_eval.get_value(to_app(e)); + if (v) + mdl->register_decl(f, v); } terms.reset(); return mdl; @@ -350,10 +311,7 @@ namespace bv { out << "u "; if (m_repair_roots.contains(e->get_id())) out << "r "; - if (bv.is_bv(e)) - out << m_eval.wval(e); - else if (m.is_bool(e)) - out << (m_eval.bval0(e)?"T":"F"); + m_eval.display_value(out, e); out << "\n"; } terms.reset(); @@ -372,12 +330,10 @@ namespace bv { } std::ostream& sls::trace_repair(bool down, expr* e) { - verbose_stream() << (down ? "d #" : "u #") + verbose_stream() << (down ? "d #" : "u #") << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " "; - if (bv.is_bv(e)) verbose_stream() << m_eval.wval(e) << " " << (m_eval.is_fixed0(e) ? "fixed " : " "); - if (m.is_bool(e)) verbose_stream() << m_eval.bval0(e) << " "; - verbose_stream() << "\n"; + m_eval.display_value(verbose_stream(), e) << "\n"; return verbose_stream(); } diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index 01ccbc41f..fe31125a7 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -56,8 +56,6 @@ namespace bv { std::pair next_to_repair(); - bool eval_is_correct(app* e); - bool re_eval_is_correct(app* e); void init_repair_goal(app* e); void try_repair_down(app* e); void try_repair_up(app* e); diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index b69cec867..486b33445 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -914,15 +914,14 @@ namespace bv { bool sls_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) { if (is_true) { - if (m_rand() % 20 != 0) + if (m_rand(20) != 0) if (a.try_set(b.bits())) return true; - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); + return a.set_random(m_rand); } else { - bool try_above = m_rand() % 2 == 0; + bool try_above = m_rand(2) == 0; if (try_above) { a.set_add(m_tmp, b.bits(), m_one); if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand)) @@ -1018,17 +1017,16 @@ namespace bv { // If this fails, set a to a random value // bool sls_eval::try_repair_add(bvect const& e, bvval& a, bvval const& b) { - if (m_rand() % 20 != 0) { + if (m_rand(20) != 0) { a.set_sub(m_tmp, e, b.bits()); if (a.try_set(m_tmp)) return true; } - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); + return a.set_random(m_rand); } bool sls_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) { - if (m_rand() % 20 != 0) { + if (m_rand(20) != 0) { if (i == 0) // e = a - b -> a := e + b a.set_add(m_tmp, e, b.bits()); @@ -1039,8 +1037,7 @@ namespace bv { return true; } // fall back to a random value - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); + return a.set_random(m_rand); } /** @@ -1058,15 +1055,11 @@ namespace bv { return a.set_repair(random_bool(), m_tmp); } - if (b.is_zero()) { - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); - } - - if (m_rand() % 20 == 0) { - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); - } + if (b.is_zero()) + return a.set_random(m_rand); + + if (m_rand(20) == 0) + return a.set_random(m_rand); #if 0 verbose_stream() << "solve for " << e << "\n"; @@ -1096,7 +1089,7 @@ namespace bv { b.shift_right(y, parity_b); #if 0 for (unsigned i = parity_b; i < b.bw; ++i) - y.set(i, m_rand() % 2 == 0); + y.set(i, m_rand(2) == 0); #endif } @@ -1151,8 +1144,7 @@ namespace bv { if (a.set_repair(random_bool(), m_tmp)) return true; - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); + return a.set_random(m_rand); } bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) { @@ -1236,7 +1228,7 @@ namespace bv { bool sls_eval::try_repair_sle(bvval& a, bvect const& b, bvect const& p2) { bool r = false; if (b < p2) { - bool coin = m_rand() % 2 == 0; + bool coin = m_rand(2) == 0; if (coin) r = a.set_random_at_least(p2, m_tmp3, m_rand); if (!r) @@ -1268,7 +1260,7 @@ namespace bv { r = a.set_random_in_range(b, p2_1, m_tmp3, m_rand); else { // random b <= x or x < p2 - bool coin = m_rand() % 2 == 0; + bool coin = m_rand(2) == 0; if (coin) r = a.set_random_at_most(p2_1, m_tmp3, m_rand); if (!r) @@ -1657,12 +1649,9 @@ namespace bv { return a.set_repair(true, m_tmp3); } else { - if (a.is_one(e) && a.is_zero()) { - for (unsigned i = 0; i < a.nw; ++i) - m_tmp[i] = random_bits(); - a.clear_overflow_bits(m_tmp); - return b.set_repair(true, m_tmp); - } + if (a.is_one(e) && a.is_zero()) + return b.set_random(m_rand); + if (a.is_one(e)) { a.set(m_tmp, a.bits()); return b.set_repair(true, m_tmp); @@ -1858,8 +1847,7 @@ namespace bv { m_tmp.set(i, e.get(i)); b.clear_overflow_bits(m_tmp); r = b.try_set(m_tmp); - } - //verbose_stream() << e << " := " << a << " " << b << "\n"; + } return r; } @@ -1869,15 +1857,15 @@ namespace bv { // set a outside of [hi:lo] to random values with preference to 0 or 1 bits // bool sls_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) { - if (m_rand() % m_config.m_prob_randomize_extract <= 100) { + if (m_rand(m_config.m_prob_randomize_extract) <= 100) { a.get_variant(m_tmp, m_rand); - if (0 == (m_rand() % 2)) { - auto bit = 0 == (m_rand() % 2); + if (0 == (m_rand(2))) { + auto bit = 0 == (m_rand(2)); if (!a.try_set_range(m_tmp, 0, lo, bit)) a.try_set_range(m_tmp, 0, lo, !bit); } - if (0 == (m_rand() % 2)) { - auto bit = 0 == (m_rand() % 2); + if (0 == (m_rand(2))) { + auto bit = 0 == (m_rand(2)); if (!a.try_set_range(m_tmp, lo + e.bw, a.bw, bit)) a.try_set_range(m_tmp, lo + e.bw, a.bw, !bit); } @@ -1888,10 +1876,7 @@ namespace bv { m_tmp.set(i + lo, e.get(i)); if (a.try_set(m_tmp)) return true; - a.get_variant(m_tmp, m_rand); - bool res = a.set_repair(random_bool(), m_tmp); - // verbose_stream() << "try set " << res << " " << m_tmp[0] << " " << a << "\n"; - return res; + return a.set_random(m_rand); } void sls_eval::set_div(bvect const& a, bvect const& b, unsigned bw, @@ -1945,6 +1930,66 @@ namespace bv { return *m_values[e->get_id()]; } + void sls_eval::init_eval(app* t) { + if (m.is_bool(t)) + set(t, bval1(t)); + else if (bv.is_bv(t)) { + auto& v = wval(t); + v.bits().copy_to(v.nw, v.eval); + } + } + + void sls_eval::commit_eval(app* e) { + if (m.is_bool(e)) { + set(e, bval1(e)); + } + else { + VERIFY(wval(e).commit_eval()); + } + } + + void sls_eval::set_random(app* e) { + if (bv.is_bv(e)) + eval(e).set_random(m_rand); + } + + bool sls_eval::eval_is_correct(app* e) { + if (!can_eval1(e)) + return false; + if (m.is_bool(e)) + return bval0(e) == bval1(e); + if (bv.is_bv(e)) { + auto const& v = wval(e); + return v.eval == v.bits(); + } + UNREACHABLE(); + return false; + } + + bool sls_eval::re_eval_is_correct(app* e) { + if (!can_eval1(e)) + return false; + if (m.is_bool(e)) + return bval0(e) ==bval1(e); + if (bv.is_bv(e)) { + auto const& v = eval(e); + return v.eval == v.bits(); + } + UNREACHABLE(); + return false; + } + + expr_ref sls_eval::get_value(app* e) { + if (m.is_bool(e)) + return expr_ref(m.mk_bool_val(bval0(e)), m); + else if (bv.is_bv(e)) { + auto const& v = wval(e); + rational n = v.get_value(); + return expr_ref(bv.mk_numeral(n, v.bw), m); + } + return expr_ref(m); + } + std::ostream& sls_eval::display(std::ostream& out, expr_ref_vector const& es) { auto& terms = sort_assertions(es); for (expr* e : terms) { @@ -1960,4 +2005,12 @@ namespace bv { terms.reset(); return out; } + + std::ostream& sls_eval::display_value(std::ostream& out, expr* e) { + if (bv.is_bv(e)) + return out << wval(e); + if (m.is_bool(e)) + return out << (bval0(e)?"T":"F"); + return out << "?"; + } } diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index ebd360481..89cd3f4cf 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -157,6 +157,18 @@ namespace bv { sls_valuation& eval(app* e) const; + void commit_eval(app* e); + + void init_eval(app* e); + + void set_random(app* e); + + bool eval_is_correct(app* e); + + bool re_eval_is_correct(app* e); + + expr_ref get_value(app* e); + /** * Override evaluaton. */ @@ -178,5 +190,7 @@ namespace bv { std::ostream& display(std::ostream& out, expr_ref_vector const& es); + + std::ostream& display_value(std::ostream& out, expr* e); }; } diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index 18518ed09..be587a8bd 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -38,8 +38,8 @@ namespace bv { else ; } - ev.m_todo.reset(); init_ranges(es); + ev.m_todo.reset(); } @@ -49,6 +49,44 @@ namespace bv { if (is_app(e)) init_range(to_app(e), sign); } + + for (expr* e : ev.m_todo) + propagate_range_up(e); + } + + void sls_fixed::propagate_range_up(expr* e) { + expr* t, * s; + rational v; + if (bv.is_concat(e, t, s)) { + auto& val = wval(s); + if (val.lo() != val.hi() && (val.lo() < val.hi() || val.hi() == 0)) + // lo <= e + add_range(e, val.lo(), rational::zero(), false); + auto valt = wval(t); +#if 0 + if (val.lo() < val.hi()) + // e < (2^|s|) * hi + add_range(e, rational::zero(), val.hi() * rational::power_of_two(bv.get_bv_size(s)), false); +#endif + } + else if (bv.is_bv_add(e, s, t) && bv.is_numeral(s, v)) { + auto& val = wval(t); + if (val.lo() != val.hi()) + add_range(e, v + val.lo(), v + val.hi(), false); + } + else if (bv.is_bv_add(e, t, s) && bv.is_numeral(s, v)) { + auto& val = wval(t); + if (val.lo() != val.hi()) + add_range(e, v + val.lo(), v + val.hi(), false); + } + // x in [1, 4[ => -x in [-3, 0[ + // x in [lo, hi[ => -x in [-hi + 1, -lo + 1[ + else if (bv.is_bv_mul(e, s, t) && bv.is_numeral(s, v) && + v + 1 == rational::power_of_two(bv.get_bv_size(e))) { + auto& val = wval(t); + if (val.lo() != val.hi()) + add_range(e, -val.hi() + 1, - val.lo() + 1, false); + } } // s <=s t <=> s + K <= t + K, K = 2^{bw-1} @@ -117,6 +155,7 @@ namespace bv { val.tighten_range(); return true; } + return false; } @@ -138,9 +177,8 @@ namespace bv { init_eq(s, b, false); return true; } - if (!sign && bv.is_concat(t) && to_app(t)->get_num_args() == 2) { - auto x = to_app(t)->get_arg(0); - auto y = to_app(t)->get_arg(1); + expr* x, * y; + if (!sign && bv.is_concat(t, x, y)) { auto sz = bv.get_bv_size(y); auto k = rational::power_of_two(sz); init_eq(y, mod(a, k), false); @@ -206,9 +244,8 @@ namespace bv { if (sign) std::swap(lo, hi); v.add_range(lo, hi); - if (v.lo() == 0 && bv.is_concat(e) && to_app(e)->get_num_args() == 2) { - auto x = to_app(e)->get_arg(0); - auto y = to_app(e)->get_arg(1); + expr* x, * y; + if (v.lo() == 0 && bv.is_concat(e, x, y)) { auto sz = bv.get_bv_size(y); auto k = rational::power_of_two(sz); lo = v.lo(); diff --git a/src/ast/sls/bv_sls_fixed.h b/src/ast/sls/bv_sls_fixed.h index 73dd5a52c..2e88484c5 100644 --- a/src/ast/sls/bv_sls_fixed.h +++ b/src/ast/sls/bv_sls_fixed.h @@ -31,6 +31,7 @@ namespace bv { void init_ranges(expr_ref_vector const& es); bool init_range(app* e, bool sign); + void propagate_range_up(expr* e); bool init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign); void get_offset(expr* e, expr*& x, rational& offset); bool init_eq(expr* e, rational const& v, bool sign); diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index 1f3674e93..68143e7b7 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -153,6 +153,7 @@ namespace bv { m_lo.set_bw(bw); m_hi.set_bw(bw); m_bits.set_bw(bw); + m_tmp.set_bw(bw); fixed.set_bw(bw); eval.set_bw(bw); // have lo, hi bits, fixed point to memory allocated within this of size num_bytes each allocated @@ -440,6 +441,11 @@ namespace bv { clear_overflow_bits(dst); } + bool sls_valuation::set_random(random_gen& r) { + get_variant(m_tmp, r); + return set_repair(r(2) == 0, m_tmp); + } + void sls_valuation::repair_sign_bits(bvect& dst) const { if (m_signed_prefix == 0) return; @@ -489,7 +495,7 @@ namespace bv { } void sls_valuation::add_range(rational l, rational h) { - return; + //return; //verbose_stream() << *this << " " << l << " " << h << " --> \n"; l = mod(l, rational::power_of_two(bw)); @@ -622,7 +628,7 @@ namespace bv { inf_feasible(m_lo); - bvect hi1(nw); + bvect& hi1 = m_tmp; hi1.set_bw(bw); m_hi.copy_to(nw, hi1); sub1(hi1); diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 04efec24a..e4828302e 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -110,6 +110,7 @@ namespace bv { protected: bvect m_bits; bvect m_lo, m_hi; // range assignment to bit-vector, as wrap-around interval + bvect m_tmp; unsigned m_signed_prefix = 0; unsigned mask; @@ -123,6 +124,7 @@ namespace bv { bvect fixed; // bit assignment and don't care bit bvect eval; // current evaluation + sls_valuation(unsigned bw); void set_bw(unsigned bw); @@ -231,12 +233,14 @@ namespace bv { bool set_repair(bool try_down, bvect& dst); void set_random_above(bvect& dst, random_gen& r); void set_random_below(bvect& dst, random_gen& r); + bool set_random(random_gen& r); void round_down(bvect& dst, std::function const& is_feasible); void round_up(bvect& dst, std::function const& is_feasible); static digit_t random_bits(random_gen& r); void get_variant(bvect& dst, random_gen& r) const; + bool try_set(bvect const& src) { if (!can_set(src)) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 675bf5022..44f56efcd 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1062,6 +1062,8 @@ new_lemma::~new_lemma() { if (current().is_conflict()) { c.m_conflicts++; } + IF_VERBOSE(4, verbose_stream() << name << "\n"); + IF_VERBOSE(4, verbose_stream() << *this << "\n"); TRACE("nla_solver", tout << name << " " << (++i) << "\n" << *this; ); } @@ -1519,6 +1521,12 @@ lbool core::check() { if (!m_lemmas.empty() || !m_literals.empty() || m_check_feasible) return l_false; } + + if (no_effect() && params().arith_nl_nra()) { + ret = m_nra.check(); + lp_settings().stats().m_nra_calls++; + } + if (no_effect() && should_run_bounded_nlsat()) ret = bounded_nlsat(); @@ -1530,12 +1538,16 @@ lbool core::check() { m_basics.basic_lemma(false); if (no_effect()) - m_divisions.check(); + m_divisions.check(); - if (no_effect()) { - std::function check1 = [&]() { m_order.order_lemma(); }; - std::function check2 = [&]() { m_monotone.monotonicity_lemma(); }; - std::function check3 = [&]() { m_tangents.tangent_lemma(); }; + + if (false && no_effect()) { + std::function check1 = [&]() { m_order.order_lemma(); + }; + std::function check2 = [&]() { m_monotone.monotonicity_lemma(); + }; + std::function check3 = [&]() { m_tangents.tangent_lemma(); + }; std::pair> checks[] = { { 6, check1 }, From 8d0e66b3e371b2e0d54070e98813033c54bacb24 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Apr 2024 11:16:34 -0700 Subject: [PATCH 19/49] fix regression introduced when testing Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 44f56efcd..216e03583 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1522,11 +1522,6 @@ lbool core::check() { return l_false; } - if (no_effect() && params().arith_nl_nra()) { - ret = m_nra.check(); - lp_settings().stats().m_nra_calls++; - } - if (no_effect() && should_run_bounded_nlsat()) ret = bounded_nlsat(); From 7b8980f82d95471bddd6d5fe4a0ba8520956964e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Apr 2024 11:17:03 -0700 Subject: [PATCH 20/49] fix regression introduced when testing Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 216e03583..449ecad4c 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1536,7 +1536,7 @@ lbool core::check() { m_divisions.check(); - if (false && no_effect()) { + if (no_effect()) { std::function check1 = [&]() { m_order.order_lemma(); }; std::function check2 = [&]() { m_monotone.monotonicity_lemma(); From 974ea7b68d925e5404e16402c71bc4ca6832b720 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Apr 2024 17:57:14 -0700 Subject: [PATCH 21/49] maintain ownership of dependency --- src/ast/simplifiers/extract_eqs.h | 5 +++-- src/ast/sls/bv_sls_eval.cpp | 6 +----- src/math/lp/lar_solver.h | 1 + src/tactic/portfolio/smt_strategic_solver.cpp | 10 ++++++++++ 4 files changed, 15 insertions(+), 7 deletions(-) diff --git a/src/ast/simplifiers/extract_eqs.h b/src/ast/simplifiers/extract_eqs.h index 724425d6a..b88a3e8a5 100644 --- a/src/ast/simplifiers/extract_eqs.h +++ b/src/ast/simplifiers/extract_eqs.h @@ -31,8 +31,9 @@ namespace euf { expr* orig; // original expression that encoded equation app* var; // isolated variable expr_ref term; // defined term - expr_dependency* dep; - dependent_eq(expr* orig, app* var, expr_ref const& term, expr_dependency* d) : orig(orig), var(var), term(term), dep(d) {} + expr_dependency_ref dep; + dependent_eq(expr* orig, app* var, expr_ref const& term, expr_dependency* d) : + orig(orig), var(var), term(term), dep(d, term.get_manager()) {} }; typedef vector dep_eq_vector; diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index 486b33445..d7ce8e703 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -1996,11 +1996,7 @@ namespace bv { out << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " "; if (is_fixed0(e)) out << "f "; - if (bv.is_bv(e)) - out << wval(e); - else if (m.is_bool(e)) - out << (bval0(e) ? "T" : "F"); - out << "\n"; + display_value(out, e) << "\n"; } terms.reset(); return out; diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h index ec40fcb24..f223b5cc5 100644 --- a/src/math/lp/lar_solver.h +++ b/src/math/lp/lar_solver.h @@ -393,6 +393,7 @@ public: bool external_is_used(unsigned) const; void pop(unsigned k); unsigned num_scopes() const { return m_trail.get_num_scopes(); } + trail_stack& trail() { return m_trail; } bool compare_values(lpvar j, lconstraint_kind kind, const mpq& right_side); lpvar add_term(const vector>& coeffs, unsigned ext_i); void register_existing_terms(); diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 138c6e646..09e7aa047 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -49,8 +49,18 @@ Notes: #include "parsers/smt2/smt2parser.h" #include "sat/sat_params.hpp" +tactic* mk_tactic_for_logic(ast_manager& m, params_ref const& p, symbol const& logic); +class smt_nested_solver_factory : public solver_factory { +public: + solver* operator()(ast_manager& m, params_ref const& p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const& logic) override { + auto t = mk_tactic_for_logic(m, p, logic); + auto s = mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic); + return s; + } +}; + tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) { if (logic=="QF_UF") return mk_qfuf_tactic(m, p); From 510534dbd40bf0bbb6c2f37eaf85ebc9b49bf499 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 10 Apr 2024 19:09:30 -0700 Subject: [PATCH 22/49] cleanup --- src/ast/sls/bv_sls_eval.cpp | 42 ++++++++++++++--------------------- src/ast/sls/sls_valuation.cpp | 33 +++++++++++++-------------- src/ast/sls/sls_valuation.h | 6 ++--- 3 files changed, 36 insertions(+), 45 deletions(-) diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index d7ce8e703..d61a831d3 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -924,15 +924,15 @@ namespace bv { bool try_above = m_rand(2) == 0; if (try_above) { a.set_add(m_tmp, b.bits(), m_one); - if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand)) + if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_rand)) return true; } a.set_sub(m_tmp, b.bits(), m_one); - if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_tmp2, m_rand)) + if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_rand)) return true; if (!try_above) { a.set_add(m_tmp, b.bits(), m_one); - if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand)) + if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_rand)) return true; } return false; @@ -1007,7 +1007,6 @@ namespace bv { bool sls_eval::try_repair_bxor(bvect const& e, bvval& a, bvval const& b) { for (unsigned i = 0; i < a.nw; ++i) m_tmp[i] = e[i] ^ b.bits()[i]; - a.clear_overflow_bits(m_tmp); return a.set_repair(random_bool(), m_tmp); } @@ -1149,7 +1148,7 @@ namespace bv { bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) { for (unsigned i = 0; i < a.nw; ++i) - m_tmp[i] = ~e[i]; + m_tmp[i] = ~e[i]; a.clear_overflow_bits(m_tmp); return a.try_set(m_tmp); } @@ -1230,14 +1229,14 @@ namespace bv { if (b < p2) { bool coin = m_rand(2) == 0; if (coin) - r = a.set_random_at_least(p2, m_tmp3, m_rand); + r = a.set_random_at_least(p2, m_rand); if (!r) - r = a.set_random_at_most(b, m_tmp3, m_rand); + r = a.set_random_at_most(b, m_rand); if (!coin && !r) - r = a.set_random_at_least(p2, m_tmp3, m_rand); + r = a.set_random_at_least(p2, m_rand); } else - r = a.set_random_in_range(p2, b, m_tmp3, m_rand); + r = a.set_random_in_range(p2, b, m_rand); return r; } @@ -1257,16 +1256,16 @@ namespace bv { bool r = false; if (p2 < b) // random b <= x < p2 - r = a.set_random_in_range(b, p2_1, m_tmp3, m_rand); + r = a.set_random_in_range(b, p2_1, m_rand); else { // random b <= x or x < p2 bool coin = m_rand(2) == 0; if (coin) - r = a.set_random_at_most(p2_1, m_tmp3, m_rand); + r = a.set_random_at_most(p2_1,m_rand); if (!r) - r = a.set_random_at_least(b, m_tmp3, m_rand); + r = a.set_random_at_least(b, m_rand); if (!r && !coin) - r = a.set_random_at_most(p2_1, m_tmp3, m_rand); + r = a.set_random_at_most(p2_1, m_rand); } p2_1.set_bw(0); return r; @@ -1282,28 +1281,28 @@ namespace bv { bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) { if (e) { // a <= t - return a.set_random_at_most(b.bits(), m_tmp, m_rand); + return a.set_random_at_most(b.bits(), m_rand); } else { // a > t a.set_add(m_tmp, b.bits(), m_one); if (a.is_zero(m_tmp)) return false; - return a.set_random_at_least(m_tmp, m_tmp2, m_rand); + return a.set_random_at_least(m_tmp, m_rand); } } bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) { if (e) { // a >= t - return a.set_random_at_least(b.bits(), m_tmp, m_rand); + return a.set_random_at_least(b.bits(), m_rand); } else { // a < t if (b.is_zero()) return false; a.set_sub(m_tmp, b.bits(), m_one); - return a.set_random_at_most(m_tmp, m_tmp2, m_rand); + return a.set_random_at_most(m_tmp, m_rand); } } @@ -1377,7 +1376,6 @@ namespace bv { unsigned n = b.bits().to_nat(e.bw); for (unsigned i = e.bw; i-- > e.bw - n;) t.set(i, a.get_bit(i)); - a.clear_overflow_bits(t); if (a.set_repair(random_bool(), t)) return true; } @@ -1527,7 +1525,6 @@ namespace bv { t[i] = a.bits()[i]; t.set(b.bw - 1, a.is_ones(e)); } - a.clear_overflow_bits(t); if (a.set_repair(random_bool(), t)) return true; } @@ -1541,13 +1538,10 @@ namespace bv { a.get_variant(t, m_rand); t.set(b.bw - 1, a.is_ones(e)); } - a.clear_overflow_bits(t); if (a.set_repair(random_bool(), t)) return true; } - - a.get_variant(t, m_rand); - return a.set_repair(random_bool(), t); + return a.set_random(m_rand); } /* @@ -1645,7 +1639,6 @@ namespace bv { m_tmp2.set(b.msb(m_tmp2), false); while (a.set_add(m_tmp3, m_tmp, m_tmp2)) m_tmp2.set(b.msb(m_tmp2), false); - a.clear_overflow_bits(m_tmp3); return a.set_repair(true, m_tmp3); } else { @@ -1723,7 +1716,6 @@ namespace bv { m_tmp[i] = random_bits(); a.set_sub(m_tmp2, a.bits(), e); set_div(m_tmp2, m_tmp, a.bw, m_tmp3, m_tmp4); - a.clear_overflow_bits(m_tmp3); return b.set_repair(random_bool(), m_tmp3); } } diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index 68143e7b7..c46b2ef77 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -244,34 +244,35 @@ namespace bv { return true; } - bool sls_valuation::set_random_at_most(bvect const& src, bvect& tmp, random_gen& r) { - if (!get_at_most(src, tmp)) + bool sls_valuation::set_random_at_most(bvect const& src, random_gen& r) { + if (!get_at_most(src, m_tmp)) return false; - if (is_zero(tmp) || (0 != r(10))) - return try_set(tmp); + if (is_zero(m_tmp) || (0 != r(10))) + return try_set(m_tmp); // random value below tmp - set_random_below(tmp, r); + set_random_below(m_tmp, r); - return (can_set(tmp) || get_at_most(src, tmp)) && try_set(tmp); + return (can_set(m_tmp) || get_at_most(src, m_tmp)) && try_set(m_tmp); } - bool sls_valuation::set_random_at_least(bvect const& src, bvect& tmp, random_gen& r) { - if (!get_at_least(src, tmp)) + bool sls_valuation::set_random_at_least(bvect const& src, random_gen& r) { + if (!get_at_least(src, m_tmp)) return false; - if (is_ones(tmp) || (0 != r(10))) - return try_set(tmp); + if (is_ones(m_tmp) || (0 != r(10))) + return try_set(m_tmp); // random value at least tmp - set_random_above(tmp, r); + set_random_above(m_tmp, r); - return (can_set(tmp) || get_at_least(src, tmp)) && try_set(tmp); + return (can_set(m_tmp) || get_at_least(src, m_tmp)) && try_set(m_tmp); } - bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, bvect& tmp, random_gen& r) { - if (0 == r() % 2) { + bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r) { + bvect& tmp = m_tmp; + if (0 == r(2)) { if (!get_at_least(lo, tmp)) return false; SASSERT(in_range(tmp)); @@ -342,7 +343,7 @@ namespace bv { bool sls_valuation::set_repair(bool try_down, bvect& dst) { for (unsigned i = 0; i < nw; ++i) dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]); - + clear_overflow_bits(dst); repair_sign_bits(dst); if (in_range(dst)) { set(eval, dst); @@ -674,6 +675,4 @@ namespace bv { c += get_num_1bits(src[i]); return c == 1; } - - } diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index e4828302e..66d7e0281 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -226,9 +226,9 @@ namespace bv { bool get_at_most(bvect const& src, bvect& dst) const; bool get_at_least(bvect const& src, bvect& dst) const; - bool set_random_at_most(bvect const& src, bvect& tmp, random_gen& r); - bool set_random_at_least(bvect const& src, bvect& tmp, random_gen& r); - bool set_random_in_range(bvect const& lo, bvect const& hi, bvect& tmp, random_gen& r); + bool set_random_at_most(bvect const& src, random_gen& r); + bool set_random_at_least(bvect const& src, random_gen& r); + bool set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r); bool set_repair(bool try_down, bvect& dst); void set_random_above(bvect& dst, random_gen& r); From c0bdc7cdd6bd22ea7b15bd37882f42555cc0b77d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Apr 2024 10:49:30 +0200 Subject: [PATCH 23/49] enable concurrent sls with new solver core allow using sls engine (for bit-vectors) with the new core. Examples z3 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=0 /st C:\QF_BV_SAT\bench_10.smt2 z3 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=2 /st C:\QF_BV_SAT\bench_10.smt2 z3 C:\QF_BV_SAT\bench_11100.smt2 sat.smt=true tactic.default_tactic=smt /v:1 smt.sls.enable=true smt.bv.solver=2 /st --- src/ast/sls/bv_sls.cpp | 16 ++- src/ast/sls/bv_sls.h | 7 +- src/ast/sls/bv_sls_fixed.cpp | 16 +-- src/ast/sls/bv_sls_terms.cpp | 2 + src/ast/sls/sls_valuation.cpp | 9 ++ src/sat/sat_solver.cpp | 3 +- src/sat/sat_solver.h | 2 + src/sat/sat_solver/sat_smt_solver.cpp | 14 ++- src/sat/smt/euf_internalize.cpp | 4 + src/sat/smt/euf_model.cpp | 9 ++ src/sat/smt/euf_solver.cpp | 13 ++- src/sat/smt/euf_solver.h | 6 + src/sat/smt/sat_th.h | 3 + src/sat/smt/sls_solver.cpp | 151 +++++++++++++++----------- src/sat/smt/sls_solver.h | 23 +++- src/sat/tactic/goal2sat.cpp | 7 ++ src/smt/params/smt_params.cpp | 2 + src/smt/params/smt_params.h | 1 + src/smt/params/smt_params_helper.pyg | 1 + 19 files changed, 206 insertions(+), 83 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index df741dac3..9af87d3c5 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -93,6 +93,18 @@ namespace bv { if (m_to_repair.empty()) return; + + // add fresh units, if any + bool new_assertion = false; + while (m_get_unit) { + auto e = m_get_unit(); + if (!e) + break; + new_assertion = true; + assert_expr(e); + } + if (new_assertion) + init(); std::function eval = [&](expr* e, unsigned i) { unsigned id = e->get_id(); @@ -212,9 +224,7 @@ namespace bv { void sls::try_repair_down(app* e) { unsigned n = e->get_num_args(); if (n == 0) { - m_eval.commit_eval(e); - - IF_VERBOSE(3, verbose_stream() << "done\n"); + m_eval.commit_eval(e); for (auto p : m_terms.parents(e)) m_repair_up.insert(p->get_id()); diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index fe31125a7..690b618bf 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -53,6 +53,7 @@ namespace bv { sls_engine m_engine; bool m_engine_model = false; bool m_engine_init = false; + std::function m_get_unit; std::pair next_to_repair(); @@ -81,7 +82,6 @@ namespace bv { /* * Invoke init after all expressions are asserted. - * No other expressions can be asserted after init. */ void init(); @@ -91,6 +91,11 @@ namespace bv { */ void init_eval(std::function& eval); + /** + * add callback to retrieve new units + */ + void init_unit(std::function get_unit) { m_get_unit = get_unit; } + /** * Run (bounded) local search to find feasible assignments. */ diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index be587a8bd..9f897a7bd 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -58,16 +58,16 @@ namespace bv { expr* t, * s; rational v; if (bv.is_concat(e, t, s)) { - auto& val = wval(s); - if (val.lo() != val.hi() && (val.lo() < val.hi() || val.hi() == 0)) + auto& vals = wval(s); + if (vals.lo() != vals.hi() && (vals.lo() < vals.hi() || vals.hi() == 0)) // lo <= e - add_range(e, val.lo(), rational::zero(), false); + add_range(e, vals.lo(), rational::zero(), false); auto valt = wval(t); -#if 0 - if (val.lo() < val.hi()) - // e < (2^|s|) * hi - add_range(e, rational::zero(), val.hi() * rational::power_of_two(bv.get_bv_size(s)), false); -#endif + if (valt.lo() != valt.hi() && (valt.lo() < valt.hi() || valt.hi() == 0)) { + // (2^|s|) * lo <= e < (2^|s|) * hi + auto p = rational::power_of_two(bv.get_bv_size(s)); + add_range(e, valt.lo() * p, valt.hi() * p, false); + } } else if (bv.is_bv_add(e, s, t) && bv.is_numeral(s, v)) { auto& val = wval(t); diff --git a/src/ast/sls/bv_sls_terms.cpp b/src/ast/sls/bv_sls_terms.cpp index 4624ab85c..ed1bf2396 100644 --- a/src/ast/sls/bv_sls_terms.cpp +++ b/src/ast/sls/bv_sls_terms.cpp @@ -206,6 +206,7 @@ namespace bv { m_todo.push_back(arg); } // populate parents + m_parents.reset(); m_parents.reserve(m_terms.size()); for (expr* e : m_terms) { if (!e || !is_app(e)) @@ -213,6 +214,7 @@ namespace bv { for (expr* arg : *to_app(e)) m_parents[arg->get_id()].push_back(e); } + m_assertion_set.reset(); for (auto a : m_assertions) m_assertion_set.insert(a->get_id()); } diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index c46b2ef77..99b3921f3 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -245,6 +245,7 @@ namespace bv { } bool sls_valuation::set_random_at_most(bvect const& src, random_gen& r) { + m_tmp.set_bw(bw); if (!get_at_most(src, m_tmp)) return false; @@ -639,6 +640,14 @@ namespace bv { if (has_range() && !in_range(m_bits)) m_bits = m_lo; + + if (mod(lo() + 1, rational::power_of_two(bw)) == hi()) + for (unsigned i = 0; i < nw; ++i) + fixed[i] = ~0; + if (lo() < hi() && hi() < rational::power_of_two(bw - 1)) + for (unsigned i = 0; i < bw; ++i) + if (hi() < rational::power_of_two(i)) + fixed.set(i, true); SASSERT(well_formed()); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 2d2962940..5829b18d1 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1314,7 +1314,7 @@ namespace sat { } bool solver::should_cancel() { - if (limit_reached() || memory_exceeded()) { + if (limit_reached() || memory_exceeded() || m_solver_canceled) { return true; } if (m_config.m_restart_max <= m_restarts) { @@ -1959,6 +1959,7 @@ namespace sat { void solver::init_search() { m_model_is_current = false; + m_solver_canceled = false; m_phase_counter = 0; m_search_state = s_unsat; m_search_unsat_conflicts = m_config.m_search_unsat_conflicts; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 0361fc157..57477f686 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -177,6 +177,7 @@ namespace sat { clause_wrapper_vector m_clauses_to_reinit; std::string m_reason_unknown; bool m_trim = false; + bool m_solver_canceled = false; visit_helper m_visited; @@ -287,6 +288,7 @@ namespace sat { random_gen& rand() { return m_rand; } void set_trim() { m_trim = true; } + void set_canceled() { m_solver_canceled = true; } protected: void reset_var(bool_var v, bool ext, bool dvar); diff --git a/src/sat/sat_solver/sat_smt_solver.cpp b/src/sat/sat_solver/sat_smt_solver.cpp index ab0e71cc3..19b10eb3e 100644 --- a/src/sat/sat_solver/sat_smt_solver.cpp +++ b/src/sat/sat_solver/sat_smt_solver.cpp @@ -197,10 +197,16 @@ public: case l_false: extract_core(); break; - default: + default: { + auto* ext = get_euf(); + if (ext && ext->get_sls_model()) { + r = l_true; + break; + } set_reason_unknown(m_solver.get_reason_unknown()); break; } + } return r; } @@ -576,6 +582,7 @@ private: void add_assumption(expr* a) { init_goal2sat(); m_dep.insert(a, m_goal2sat.internalize(a)); + get_euf()->add_assertion(a); } void internalize_assumptions(expr_ref_vector const& asms) { @@ -632,6 +639,11 @@ private: void get_model_core(model_ref & mdl) override { TRACE("sat", tout << "retrieve model " << (m_solver.model_is_current()?"present":"absent") << "\n";); mdl = nullptr; + auto ext = get_euf(); + if (ext) + mdl = ext->get_sls_model(); + if (mdl) + return; if (!m_solver.model_is_current()) return; if (m_fmls.size() > m_qhead) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index f750f186d..ebb6e4b85 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -525,4 +525,8 @@ namespace euf { return n; } + void solver::add_assertion(expr* f) { + m_assertions.push_back(f); + m_trail.push(push_back_vector(m_assertions)); + } } diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 2035e16b6..ac7ef1522 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -18,6 +18,7 @@ Author: #include "ast/ast_pp.h" #include "ast/ast_ll_pp.h" #include "sat/smt/euf_solver.h" +#include "sat/smt/sls_solver.h" #include "model/value_factory.h" namespace euf { @@ -67,6 +68,14 @@ namespace euf { m_qmodel = mdl; } + model_ref solver::get_sls_model() { + model_ref mdl; + auto s = get_solver(m.mk_family_id("sls"), nullptr); + if (s) + mdl = dynamic_cast(s)->get_model(); + return mdl; + } + void solver::update_model(model_ref& mdl, bool validate) { TRACE("model", tout << "create model\n";); if (m_qmodel) { diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index b108430d8..efd091f66 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -28,6 +28,7 @@ Author: #include "sat/smt/q_solver.h" #include "sat/smt/fpa_solver.h" #include "sat/smt/dt_solver.h" +#include "sat/smt/sls_solver.h" #include "sat/smt/recfun_solver.h" #include "sat/smt/specrel_solver.h" @@ -54,6 +55,7 @@ namespace euf { m_smt_proof_checker(m, p), m_clause(m), m_expr_args(m), + m_assertions(m), m_values(m) { updt_params(p); @@ -77,6 +79,7 @@ namespace euf { }; m_egraph.set_on_merge(on_merge); } + } void solver::updt_params(params_ref const& p) { @@ -185,7 +188,9 @@ namespace euf { IF_VERBOSE(0, verbose_stream() << mk_pp(f, m) << " not handled\n"); } - void solver::init_search() { + void solver::init_search() { + if (get_config().m_sls_enable) + add_solver(alloc(sls::solver, *this)); TRACE("before_search", s().display(tout);); m_reason_unknown.clear(); for (auto* s : m_solvers) @@ -217,7 +222,7 @@ namespace euf { mark_relevant(lit); s().assign(lit, sat::justification::mk_ext_justification(s().scope_lvl(), idx)); } - + lbool solver::resolve_conflict() { for (auto* s : m_solvers) { lbool r = s->resolve_conflict(); @@ -664,7 +669,9 @@ namespace euf { if (give_up) return sat::check_result::CR_GIVEUP; if (m_qsolver && m_config.m_arith_ignore_int) - return sat::check_result::CR_GIVEUP; + return sat::check_result::CR_GIVEUP; + for (auto s : m_solvers) + s->finalize(); return sat::check_result::CR_DONE; } diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 7d2d01473..ec89667d5 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -154,6 +154,7 @@ namespace euf { svector m_scopes; scoped_ptr_vector m_solvers; ptr_vector m_id2solver; + constraint* m_conflict = nullptr; constraint* m_eq = nullptr; @@ -173,6 +174,7 @@ namespace euf { symbol m_smt = symbol("smt"); expr_ref_vector m_clause; expr_ref_vector m_expr_args; + expr_ref_vector m_assertions; // internalization @@ -482,6 +484,10 @@ namespace euf { bool enable_ackerman_axioms(expr* n) const; bool is_fixed(euf::enode* n, expr_ref& val, sat::literal_vector& explain); + void add_assertion(expr* f); + expr_ref_vector const& get_assertions() { return m_assertions; } + model_ref get_sls_model(); + // relevancy bool relevancy_enabled() const { return m_relevancy.enabled(); } diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index e226566b8..cdd1292a3 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -148,6 +148,8 @@ namespace euf { virtual void set_bounds(enode* n) {} + virtual void finalize() {} + }; class th_proof_hint : public sat::proof_hint { @@ -225,6 +227,7 @@ namespace euf { void push() override { m_num_scopes++; } void pop(unsigned n) override; + unsigned random(); }; diff --git a/src/sat/smt/sls_solver.cpp b/src/sat/smt/sls_solver.cpp index ae8620e28..e12ff5ba7 100644 --- a/src/sat/smt/sls_solver.cpp +++ b/src/sat/smt/sls_solver.cpp @@ -23,38 +23,79 @@ Author: namespace sls { solver::solver(euf::solver& ctx): - th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls")) {} + th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls")), + m_units(m) {} solver::~solver() { - if (m_bvsls) { - m_bvsls->cancel(); + finalize(); + } + + void solver::finalize() { + if (!m_completed && m_bvsls) { + m_bvsls->cancel(); m_thread.join(); + m_bvsls->collect_statistics(m_st); + m_bvsls = nullptr; } } - void solver::push_core() { - if (s().scope_lvl() == s().search_lvl() + 1) - init_local_search(); - } - - void solver::pop_core(unsigned n) { - if (s().scope_lvl() - n <= s().search_lvl()) - sample_local_search(); + sat::check_result solver::check() { + + return sat::check_result::CR_DONE; } - void solver::simplify() { - + void solver::simplify() { + } + + bool solver::unit_propagate() { + force_push(); + sample_local_search(); + return false; + } + + bool solver::is_unit(expr* e) { + if (!e) + return false; + m.is_not(e, e); + if (is_uninterp_const(e)) + return true; + bv_util bu(m); + expr* s; + if (bu.is_bit2bool(e, s)) + return is_uninterp_const(s); + return false; + } + + void solver::push_core() { + + } + + void solver::pop_core(unsigned n) { + for (; m_trail_lim < s().init_trail_size(); ++m_trail_lim) { + auto lit = s().trail_literal(m_trail_lim); + auto e = ctx.literal2expr(lit); + if (is_unit(e)) { + // IF_VERBOSE(1, verbose_stream() << "add unit " << mk_pp(e, m) << "\n"); + std::lock_guard lock(m_mutex); + m_units.push_back(e); + m_has_units = true; + } + } } + void solver::init_search() { + init_local_search(); + } void solver::init_local_search() { if (m_bvsls) { m_bvsls->cancel(); m_thread.join(); - if (m_result == l_true) { - verbose_stream() << "Found model using local search - INIT\n"; - exit(1); - } + m_result = l_undef; + m_completed = false; + m_has_units = false; + m_model = nullptr; + m_units.reset(); } // set up state for local search solver here @@ -64,43 +105,12 @@ namespace sls { params_ref p; m_completed = false; m_result = l_undef; + m_model = nullptr; m_bvsls = alloc(bv::sls, *m_m, p); - // walk clauses, add them - // walk trail stack until search level, add units - // encapsulate bvsls within the arguments of run-local-search. - // ensure bvsls does not touch ast-manager. + + for (expr* a : ctx.get_assertions()) + m_bvsls->assert_expr(tr(a)); - unsigned trail_sz = s().trail_size(); - for (unsigned i = 0; i < trail_sz; ++i) { - auto lit = s().trail_literal(i); - if (s().lvl(lit) > s().search_lvl()) - break; - expr_ref fml = literal2expr(lit); - m_bvsls->assert_expr(tr(fml.get())); - } - unsigned num_vars = s().num_vars(); - for (unsigned i = 0; i < 2*num_vars; ++i) { - auto l1 = ~sat::to_literal(i); - auto const& wlist = s().get_wlist(l1); - for (sat::watched const& w : wlist) { - if (!w.is_binary_non_learned_clause()) - continue; - sat::literal l2 = w.get_literal(); - if (l1.index() > l2.index()) - continue; - expr_ref fml(m.mk_or(literal2expr(l1), literal2expr(l2)), m); - m_bvsls->assert_expr(tr(fml.get())); - } - } - for (auto clause : s().clauses()) { - expr_ref_vector cls(m); - for (auto lit : *clause) - cls.push_back(literal2expr(lit)); - expr_ref fml(m.mk_or(cls), m); - m_bvsls->assert_expr(tr(fml.get())); - } - - // use phase assignment from literals? std::function eval = [&](expr* e, unsigned r) { return false; }; @@ -108,23 +118,42 @@ namespace sls { m_bvsls->init(); m_bvsls->init_eval(eval); m_bvsls->updt_params(s().params()); - + m_bvsls->init_unit([&]() { + if (!m_has_units) + return expr_ref(*m_m); + expr_ref e(m); + { + std::lock_guard lock(m_mutex); + if (m_units.empty()) + return expr_ref(*m_m); + e = m_units.back(); + m_units.pop_back(); + } + ast_translation tr(m, *m_m); + return expr_ref(tr(e.get()), *m_m); + }); + m_thread = std::thread([this]() { run_local_search(); }); } void solver::sample_local_search() { - if (m_completed) { - m_thread.join(); - if (m_result == l_true) { - verbose_stream() << "Found model using local search\n"; - exit(1); - } + if (!m_completed) + return; + m_thread.join(); + m_completed = false; + m_bvsls->collect_statistics(m_st); + if (m_result == l_true) { + IF_VERBOSE(2, verbose_stream() << "(sat.sls :model-completed)\n";); + auto mdl = m_bvsls->get_model(); + ast_translation tr(*m_m, m); + m_model = mdl->translate(tr); + s().set_canceled(); } + m_bvsls = nullptr; } void solver::run_local_search() { - lbool r = (*m_bvsls)(); - m_result = r; + m_result = (*m_bvsls)(); m_completed = true; } diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h index c473264ac..55e98fac7 100644 --- a/src/sat/smt/sls_solver.h +++ b/src/sat/smt/sls_solver.h @@ -30,30 +30,43 @@ namespace sls { class solver : public euf::th_euf_solver { std::atomic m_result; - std::atomic m_completed; + std::atomic m_completed, m_has_units; std::thread m_thread; + std::mutex m_mutex; scoped_ptr m_m; scoped_ptr m_bvsls; + model_ref m_model; + unsigned m_trail_lim = 0; + expr_ref_vector m_units; + statistics m_st; void run_local_search(); void init_local_search(); void sample_local_search(); + + bool is_unit(expr*); public: solver(euf::solver& ctx); ~solver(); + void simplify() override; + void init_search() override; + void push_core() override; void pop_core(unsigned n) override; - void simplify() override; sat::literal internalize(expr* e, bool sign, bool root) override { UNREACHABLE(); return sat::null_literal; } void internalize(expr* e) override { UNREACHABLE(); } th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } - + void collect_statistics(statistics& st) const override { st.copy(m_st); } - bool unit_propagate() override { return false; } + model_ref get_model() { return m_model; } + + void finalize() override; + + bool unit_propagate() override; void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override { UNREACHABLE(); } - sat::check_result check() override { return sat::check_result::CR_DONE; } + sat::check_result check() override; std::ostream & display(std::ostream & out) const override { return out; } std::ostream & display_justification(std::ostream & out, sat::ext_justification_idx idx) const override { UNREACHABLE(); return out; } std::ostream & display_constraint(std::ostream & out, sat::ext_constraint_idx idx) const override { UNREACHABLE(); return out; } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 267888804..57e3a89b5 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -895,6 +895,7 @@ struct goal2sat::imp : public sat::sat_internalizer { process(n, true); CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";); SASSERT(m_result_stack.empty()); + add_assertion(n); } void insert_dep(expr* dep0, expr* dep, bool sign) { @@ -989,6 +990,12 @@ struct goal2sat::imp : public sat::sat_internalizer { } } + void add_assertion(expr* f) { + auto* ext = dynamic_cast(m_solver.get_extension()); + if (ext) + ext->add_assertion(f); + } + void update_model(model_ref& mdl) { auto* ext = dynamic_cast(m_solver.get_extension()); if (ext) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index ef617f724..02919b287 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -49,6 +49,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_threads_max_conflicts = p.threads_max_conflicts(); m_threads_cube_frequency = p.threads_cube_frequency(); m_core_validate = p.core_validate(); + m_sls_enable = p.sls_enable(); m_logic = _p.get_sym("logic", m_logic); m_string_solver = p.string_solver(); m_up_persist_clauses = p.up_persist_clauses(); @@ -66,6 +67,7 @@ void smt_params::updt_local_params(params_ref const & _p) { m_lemmas2console = sp.lemmas2console(); m_instantiations2console = sp.instantiations2console(); m_proof_log = sp.proof_log(); + } void smt_params::updt_params(params_ref const & p) { diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index c678b7536..0ef063e4a 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -114,6 +114,7 @@ struct smt_params : public preprocessor_params, bool m_induction = false; bool m_clause_proof = false; symbol m_proof_log; + bool m_sls_enable = false; // ----------------------------------- // diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 708fa87d8..4e498b2c4 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -135,6 +135,7 @@ def_module_params(module_name='smt', ('str.regex_automata_length_attempt_threshold', UINT, 10, 'number of length/path constraint attempts before checking unsatisfiability of regex terms'), ('str.fixed_length_refinement', BOOL, False, 'use abstraction refinement in fixed-length equation solver (Z3str3 only)'), ('str.fixed_length_naive_cex', BOOL, True, 'construct naive counterexamples when fixed-length model construction fails for a given length assignment (Z3str3 only)'), + ('sls.enable', BOOL, False, 'enable sls co-processor with SMT engine'), ('core.minimize', BOOL, False, 'minimize unsat core produced by SMT context'), ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'), ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'), From 43dd6a543640ff7fe9b64954912643e9ff53639f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 11 Apr 2024 18:19:58 +0200 Subject: [PATCH 24/49] include mutex Signed-off-by: Nikolaj Bjorner --- src/sat/smt/sls_solver.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h index 55e98fac7..5a6c9950b 100644 --- a/src/sat/smt/sls_solver.h +++ b/src/sat/smt/sls_solver.h @@ -17,6 +17,7 @@ Author: #pragma once #include +#include #include "util/rlimit.h" #include "ast/sls/bv_sls.h" #include "sat/smt/sat_th.h" From 2682c2ef2b3f31f065cc54b83e91f6d42c60db2f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Apr 2024 16:42:26 +0200 Subject: [PATCH 25/49] sls updates - add SINGLE_THREAD mode - add interface to retrieve "best" model so far --- src/ast/sls/bv_sls.cpp | 18 +++++- src/ast/sls/bv_sls.h | 8 +++ src/sat/smt/intblast_solver.cpp | 2 +- src/sat/smt/sls_solver.cpp | 98 +++++++++++++++++---------------- src/sat/smt/sls_solver.h | 68 +++++++++++++++++------ 5 files changed, 128 insertions(+), 66 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index 9af87d3c5..c0972349b 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -61,6 +61,17 @@ namespace bv { } } + + void sls::set_model() { + if (!m_set_model) + return; + if (m_repair_roots.size() >= m_min_repair_size) + return; + m_min_repair_size = m_repair_roots.size(); + IF_VERBOSE(2, verbose_stream() << "(sls-update-model :num-unsat " << m_min_repair_size << ")\n"); + m_set_model(*get_model()); + } + void sls::init_repair_goal(app* t) { m_eval.init_eval(t); } @@ -94,6 +105,9 @@ namespace bv { if (m_to_repair.empty()) return; + // refresh the best model so far to a callback + set_model(); + // add fresh units, if any bool new_assertion = false; while (m_get_unit) { @@ -130,7 +144,7 @@ namespace bv { return m_rand() % 2 == 0; }; m_eval.init_eval(m_terms.assertions(), eval); - init_repair(); + init_repair(); // m_engine_init = false; } @@ -295,10 +309,12 @@ namespace bv { model_ref mdl = alloc(model, m); auto& terms = m_eval.sort_assertions(m_terms.assertions()); for (expr* e : terms) { +#if 0 if (!m_eval.re_eval_is_correct(to_app(e))) { verbose_stream() << "missed evaluation #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; m_eval.display_value(verbose_stream(), e) << "\n"; } +#endif if (!is_uninterp_const(e)) continue; diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index 690b618bf..987cebcdb 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -54,10 +54,13 @@ namespace bv { bool m_engine_model = false; bool m_engine_init = false; std::function m_get_unit; + std::function m_set_model; + unsigned m_min_repair_size = UINT_MAX; std::pair next_to_repair(); void init_repair_goal(app* e); + void set_model(); void try_repair_down(app* e); void try_repair_up(app* e); void set_repair_down(expr* e) { m_repair_down = e->get_id(); } @@ -96,6 +99,11 @@ namespace bv { */ void init_unit(std::function get_unit) { m_get_unit = get_unit; } + /** + * Add callback to set model + */ + void set_model(std::function f) { m_set_model = f; } + /** * Run (bounded) local search to find feasible assignments. */ diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index f4491896b..459b26339 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -1069,7 +1069,7 @@ namespace intblast { if (e->get_family_id() != bv.get_family_id()) return false; for (euf::enode* arg : euf::enode_args(n)) - dep.add(n, arg->get_root()); + dep.add(n, arg); return true; } diff --git a/src/sat/smt/sls_solver.cpp b/src/sat/smt/sls_solver.cpp index e12ff5ba7..a507619ee 100644 --- a/src/sat/smt/sls_solver.cpp +++ b/src/sat/smt/sls_solver.cpp @@ -22,31 +22,37 @@ Author: namespace sls { +#ifdef SINGLE_THREAD + + solver::solver(euf::solver& ctx) : + th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls")) + {} + +#else solver::solver(euf::solver& ctx): - th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls")), - m_units(m) {} + th_euf_solver(ctx, symbol("sls"), ctx.get_manager().mk_family_id("sls")) + {} solver::~solver() { finalize(); } void solver::finalize() { - if (!m_completed && m_bvsls) { - m_bvsls->cancel(); + if (!m_completed && m_sls) { + m_sls->cancel(); m_thread.join(); - m_bvsls->collect_statistics(m_st); - m_bvsls = nullptr; + m_sls->collect_statistics(m_st); + m_sls = nullptr; + m_shared = nullptr; + m_slsm = nullptr; + m_units = nullptr; } } sat::check_result solver::check() { - return sat::check_result::CR_DONE; } - void solver::simplify() { - } - bool solver::unit_propagate() { force_push(); sample_local_search(); @@ -66,10 +72,6 @@ namespace sls { return false; } - void solver::push_core() { - - } - void solver::pop_core(unsigned n) { for (; m_trail_lim < s().init_trail_size(); ++m_trail_lim) { auto lit = s().trail_literal(m_trail_lim); @@ -77,60 +79,63 @@ namespace sls { if (is_unit(e)) { // IF_VERBOSE(1, verbose_stream() << "add unit " << mk_pp(e, m) << "\n"); std::lock_guard lock(m_mutex); - m_units.push_back(e); + ast_translation tr(m, *m_shared); + m_units->push_back(tr(e.get())); m_has_units = true; } } - } - - void solver::init_search() { - init_local_search(); - } + } - void solver::init_local_search() { - if (m_bvsls) { - m_bvsls->cancel(); + void solver::init_search() { + if (m_sls) { + m_sls->cancel(); m_thread.join(); m_result = l_undef; m_completed = false; m_has_units = false; m_model = nullptr; - m_units.reset(); + m_units = nullptr; } // set up state for local search solver here - m_m = alloc(ast_manager, m); - ast_translation tr(m, *m_m); + m_shared = alloc(ast_manager); + m_slsm = alloc(ast_manager); + m_units = alloc(expr_ref_vector, *m_shared); + ast_translation tr(m, *m_slsm); - params_ref p; m_completed = false; m_result = l_undef; m_model = nullptr; - m_bvsls = alloc(bv::sls, *m_m, p); + m_sls = alloc(bv::sls, *m_slsm, s().params()); for (expr* a : ctx.get_assertions()) - m_bvsls->assert_expr(tr(a)); + m_sls->assert_expr(tr(a)); std::function eval = [&](expr* e, unsigned r) { return false; }; - m_bvsls->init(); - m_bvsls->init_eval(eval); - m_bvsls->updt_params(s().params()); - m_bvsls->init_unit([&]() { + m_sls->init(); + m_sls->init_eval(eval); + m_sls->updt_params(s().params()); + m_sls->init_unit([&]() { if (!m_has_units) - return expr_ref(*m_m); - expr_ref e(m); + return expr_ref(*m_slsm); + expr_ref e(*m_slsm); { std::lock_guard lock(m_mutex); - if (m_units.empty()) - return expr_ref(*m_m); - e = m_units.back(); - m_units.pop_back(); + if (m_units->empty()) + return expr_ref(*m_slsm); + ast_translation tr(*m_shared, *m_slsm); + e = tr(m_units->back()); + m_units->pop_back(); } - ast_translation tr(m, *m_m); - return expr_ref(tr(e.get()), *m_m); + return e; + }); + m_sls->set_model([&](model& mdl) { + std::lock_guard lock(m_mutex); + ast_translation tr(*m_shared, m); + m_model = mdl.translate(tr); }); m_thread = std::thread([this]() { run_local_search(); }); @@ -141,20 +146,21 @@ namespace sls { return; m_thread.join(); m_completed = false; - m_bvsls->collect_statistics(m_st); + m_sls->collect_statistics(m_st); if (m_result == l_true) { IF_VERBOSE(2, verbose_stream() << "(sat.sls :model-completed)\n";); - auto mdl = m_bvsls->get_model(); - ast_translation tr(*m_m, m); + auto mdl = m_sls->get_model(); + ast_translation tr(*m_slsm, m); m_model = mdl->translate(tr); s().set_canceled(); } - m_bvsls = nullptr; + m_sls = nullptr; } void solver::run_local_search() { - m_result = (*m_bvsls)(); + m_result = (*m_sls)(); m_completed = true; } +#endif } diff --git a/src/sat/smt/sls_solver.h b/src/sat/smt/sls_solver.h index 5a6c9950b..e1d8a95b5 100644 --- a/src/sat/smt/sls_solver.h +++ b/src/sat/smt/sls_solver.h @@ -16,13 +16,45 @@ Author: --*/ #pragma once -#include -#include + #include "util/rlimit.h" #include "ast/sls/bv_sls.h" #include "sat/smt/sat_th.h" +#ifdef SINGLE_THREAD + + +namespace euf { + class solver; +} + +namespace sls { + + class solver : public euf::th_euf_solver { + public: + solver(euf::solver& ctx); + + sat::literal internalize(expr* e, bool sign, bool root) override { UNREACHABLE(); return sat::null_literal; } + void internalize(expr* e) override { UNREACHABLE(); } + th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } + + model_ref get_model() { return model_ref(nullptr); } + bool unit_propagate() override { return false; } + void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); } + sat::check_result check() override { return sat::check_result::CR_DONE;} + std::ostream& display(std::ostream& out) const override { return out; } + std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { UNREACHABLE(); return out; } + std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { UNREACHABLE(); return out; } + + }; +} + +#else + +#include +#include + namespace euf { class solver; } @@ -34,38 +66,36 @@ namespace sls { std::atomic m_completed, m_has_units; std::thread m_thread; std::mutex m_mutex; - scoped_ptr m_m; - scoped_ptr m_bvsls; + // m is accessed by the main thread + // m_slsm is accessed by the sls thread + // m_shared is only accessed at synchronization points + scoped_ptr m_shared, m_slsm; + scoped_ptr m_sls; + scoped_ptr m_units; model_ref m_model; unsigned m_trail_lim = 0; - expr_ref_vector m_units; statistics m_st; void run_local_search(); - void init_local_search(); void sample_local_search(); - bool is_unit(expr*); + public: solver(euf::solver& ctx); ~solver(); - void simplify() override; - void init_search() override; + model_ref get_model() { return m_model; } - void push_core() override; + void init_search() override; + void push_core() override {} void pop_core(unsigned n) override; + th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } + void collect_statistics(statistics& st) const override { st.copy(m_st); } + void finalize() override; + bool unit_propagate() override; sat::literal internalize(expr* e, bool sign, bool root) override { UNREACHABLE(); return sat::null_literal; } void internalize(expr* e) override { UNREACHABLE(); } - th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } - void collect_statistics(statistics& st) const override { st.copy(m_st); } - - model_ref get_model() { return m_model; } - - void finalize() override; - - bool unit_propagate() override; void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector & r, bool probing) override { UNREACHABLE(); } sat::check_result check() override; std::ostream & display(std::ostream & out) const override { return out; } @@ -75,3 +105,5 @@ namespace sls { }; } + +#endif \ No newline at end of file From 0368b5271657f9b10ecb7a3ac4d24a5a5a977c5f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 17 Apr 2024 15:16:11 +0200 Subject: [PATCH 26/49] add missing expr Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_model.cpp | 2 +- src/sat/smt/intblast_solver.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index ac7ef1522..9739249db 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -327,7 +327,7 @@ namespace euf { out << mdl << "\n"; } - void solver::validate_model(model& mdl) { + void solver::validate_model(model& mdl) { if (!m_unhandled_functions.empty()) return; if (get_config().m_arith_ignore_int) diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 459b26339..472fa4b2b 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -726,6 +726,7 @@ namespace intblast { r = a.mk_le(smod(bv_expr, 0), smod(bv_expr, 1)); break; case OP_SGEQ: + bv_expr = e->get_arg(0); r = a.mk_ge(smod(bv_expr, 0), smod(bv_expr, 1)); break; case OP_SLT: From e184a9a7111b5e2d20cb7923571ddeb760c97e56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Apr 2024 07:32:52 -0400 Subject: [PATCH 27/49] fix translation of bvudiv --- src/sat/smt/intblast_solver.cpp | 77 +++++++++++++++++++++++---------- src/sat/smt/intblast_solver.h | 2 + 2 files changed, 57 insertions(+), 22 deletions(-) diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 472fa4b2b..33c998041 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -49,6 +49,7 @@ namespace intblast { sat::literal lit = expr2literal(e); if (sign) lit.neg(); + TRACE("bv", tout << mk_pp(e, m) << " -> " << literal2expr(lit) << "\n"); return lit; } @@ -101,6 +102,7 @@ namespace intblast { set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0))); } m_preds.push_back(e); + TRACE("bv", tout << mk_pp(e, m) << " " << mk_pp(translated(e), m) << "\n"); ctx.push(push_back_vector(m_preds)); } @@ -456,10 +458,10 @@ namespace intblast { auto nBv2int = ctx.get_enode(bv2int); auto nxModN = ctx.get_enode(xModN); if (nBv2int->get_root() != nxModN->get_root()) { - auto a = eq_internalize(nBv2int, nxModN); - ctx.mark_relevant(a); - add_unit(a); - return sat::check_result::CR_CONTINUE; + auto a = eq_internalize(nBv2int, nxModN); + ctx.mark_relevant(a); + add_unit(a); + return sat::check_result::CR_CONTINUE; } } return sat::check_result::CR_DONE; @@ -585,12 +587,12 @@ namespace intblast { } void solver::translate_quantifier(quantifier* q) { - if (is_lambda(q)) - throw default_exception("lambdas are not supported in intblaster"); if (m_is_plugin) { set_translated(q, q); return; } + if (is_lambda(q)) + throw default_exception("lambdas are not supported in intblaster"); expr* b = q->get_expr(); unsigned nd = q->get_num_decls(); ptr_vector sorts; @@ -601,7 +603,6 @@ namespace intblast { sorts.push_back(a.mk_int()); } else - sorts.push_back(s); } b = translated(b); @@ -775,13 +776,13 @@ namespace intblast { case OP_BUREM: case OP_BUREM_I: { expr* x = umod(e, 0), * y = umod(e, 1); - r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, a.mk_mod(x, y)); + r = if_eq(y, 0, x, a.mk_mod(x, y)); break; } case OP_BUDIV: case OP_BUDIV_I: { - expr* x = arg(0), * y = umod(e, 1); - r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), a.mk_int(-1), a.mk_idiv(x, y)); + expr* x = umod(e, 0), * y = umod(e, 1); + r = if_eq(y, 0, a.mk_int(-1), a.mk_idiv(x, y)); break; } case OP_BUMUL_NO_OVFL: { @@ -797,7 +798,7 @@ namespace intblast { r = a.mk_int(0); IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); for (unsigned i = 0; i < bv.get_bv_size(e); ++i) - r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), mul(x, a.mk_int(rational::power_of_two(i))), r); + r = if_eq(y, i, mul(x, a.mk_int(rational::power_of_two(i))), r); } break; } @@ -812,7 +813,7 @@ namespace intblast { r = a.mk_int(0); IF_VERBOSE(2, verbose_stream() << "lshr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); for (unsigned i = 0; i < bv.get_bv_size(e); ++i) - r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r); + r = if_eq(y, i, a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r); } break; case OP_BASHR: @@ -833,20 +834,19 @@ namespace intblast { IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); for (unsigned i = 0; i < sz; ++i) { expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i))); - r = m.mk_ite(m.mk_eq(y, a.mk_int(i)), + r = if_eq(y, i, m.mk_ite(signx, add(d, a.mk_int(- rational::power_of_two(sz-i))), d), r); } } break; - case OP_BOR: { + case OP_BOR: // p | q := (p + q) - band(p, q) IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); r = arg(0); for (unsigned i = 1; i < args.size(); ++i) r = a.mk_sub(add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i))); - break; - } + break; case OP_BNAND: r = bnot(band(args)); break; @@ -916,8 +916,8 @@ namespace intblast { r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), add(u, y), r); r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r); r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r); - r = m.mk_ite(m.mk_eq(u, a.mk_int(0)), a.mk_int(0), r); - r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); + r = if_eq(u, 0, a.mk_int(0), r); + r = if_eq(y, 0, x, r); break; } case OP_BSDIV_I: @@ -938,7 +938,7 @@ namespace intblast { y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y); expr* d = a.mk_idiv(x, y); r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d)); - r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r); + r = if_eq(y, 0, m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r); break; } case OP_BSREM_I: @@ -954,7 +954,7 @@ namespace intblast { expr* d = a.mk_idiv(absx, absy); d = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d)); r = a.mk_sub(x, mul(d, y)); - r = m.mk_ite(m.mk_eq(y, a.mk_int(0)), x, r); + r = if_eq(y, 0, x, r); break; } case OP_ROTATE_LEFT: { @@ -973,7 +973,7 @@ namespace intblast { expr* y = umod(e, 1); r = a.mk_int(0); for (unsigned i = 0; i < sz; ++i) - r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(i), r); + r = if_eq(y, i, rotate_left(i), r); break; } case OP_EXT_ROTATE_RIGHT: { @@ -981,7 +981,7 @@ namespace intblast { expr* y = umod(e, 1); r = a.mk_int(0); for (unsigned i = 0; i < sz; ++i) - r = m.mk_ite(m.mk_eq(a.mk_int(i), y), rotate_left(sz - i), r); + r = if_eq(y, i, rotate_left(sz - i), r); break; } case OP_REPEAT: { @@ -1012,6 +1012,18 @@ namespace intblast { set_translated(e, r); } + expr_ref solver::if_eq(expr* n, unsigned k, expr* th, expr* el) { + rational r; + expr_ref _th(th, m), _el(el, m); + if (bv.is_numeral(n, r)) { + if (r == k) + return expr_ref(th, m); + else + return expr_ref(el, m); + } + return expr_ref(m.mk_ite(m.mk_eq(n, a.mk_int(k)), th, el), m); + } + void solver::translate_basic(app* e) { if (m.is_eq(e)) { bool has_bv_arg = any_of(*e, [&](expr* arg) { return bv.is_bv(arg); }); @@ -1125,6 +1137,27 @@ namespace intblast { TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n"); } + void solver::finalize_model(model& mdl) { + return; + for (auto n : ctx.get_egraph().nodes()) { + auto e = n->get_expr(); + if (!is_translated(e)) + continue; + if (!bv.is_bv(e)) + continue; + auto t = translated(e); + + expr_ref ei(bv.mk_bv2int(e), m); + expr_ref ti(a.mk_mod(t, a.mk_int(rational::power_of_two(bv.get_bv_size(e)))), m); + auto ev = mdl(ei); + auto tv = mdl(ti); + if (ev != tv) { + IF_VERBOSE(0, verbose_stream() << mk_pp(e, m) << " <- " << ev << "\n"); + IF_VERBOSE(0, verbose_stream() << mk_pp(t, m) << " <- " << tv << "\n"); + } + } + } + sat::literal_vector const& solver::unsat_core() { return m_core; } diff --git a/src/sat/smt/intblast_solver.h b/src/sat/smt/intblast_solver.h index 0aceb8b2b..34f876be6 100644 --- a/src/sat/smt/intblast_solver.h +++ b/src/sat/smt/intblast_solver.h @@ -77,6 +77,7 @@ namespace intblast { bool is_non_negative(expr* bv_expr, expr* e); expr_ref mul(expr* x, expr* y); expr_ref add(expr* x, expr* y); + expr_ref if_eq(expr* n, unsigned k, expr* th, expr* el); expr* amod(expr* bv_expr, expr* x, rational const& N); rational bv_size(expr* bv_expr); @@ -147,6 +148,7 @@ namespace intblast { rational get_value(expr* e) const; + void finalize_model(model& mdl) override; }; } From cbef183ae50181ce8f3b962cab9d97f51669d089 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Apr 2024 14:57:04 -0400 Subject: [PATCH 28/49] type check equality injectivity axiom Signed-off-by: Nikolaj Bjorner --- src/sat/smt/intblast_solver.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 33c998041..421966377 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -437,10 +437,12 @@ namespace intblast { continue; if (sib->get_arg(0)->get_root() == r1) continue; - auto a = eq_internalize(n, sib); - auto b = eq_internalize(sib->get_arg(0), n->get_arg(0)); - ctx.mark_relevant(a); - ctx.mark_relevant(b); + if (bv.get_bv_size(r1->get_expr()) != bv.get_bv_size(sib->get_arg(0)->get_expr())) + continue; + auto a = eq_internalize(n, sib); + auto b = eq_internalize(sib->get_arg(0), n->get_arg(0)); + ctx.mark_relevant(a); + ctx.mark_relevant(b); add_clause(~a, b, nullptr); return sat::check_result::CR_CONTINUE; } From 2a4f0e785b2b48d611ba4ae8d4c515c1b81890ae Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Apr 2024 18:04:10 -0400 Subject: [PATCH 29/49] tidy --- src/ast/sls/bv_sls.cpp | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index c0972349b..f1b2a9f4f 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -144,7 +144,7 @@ namespace bv { return m_rand() % 2 == 0; }; m_eval.init_eval(m_terms.assertions(), eval); - init_repair(); + init_repair(); // m_engine_init = false; } @@ -284,8 +284,7 @@ namespace bv { else if (!m_eval.repair_up(e)) { IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e)); if (m_rand(10) != 0) { - m_eval.set_random(e); - + m_eval.set_random(e); m_repair_roots.insert(e->get_id()); } else @@ -309,15 +308,8 @@ namespace bv { model_ref mdl = alloc(model, m); auto& terms = m_eval.sort_assertions(m_terms.assertions()); for (expr* e : terms) { -#if 0 - if (!m_eval.re_eval_is_correct(to_app(e))) { - verbose_stream() << "missed evaluation #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; - m_eval.display_value(verbose_stream(), e) << "\n"; - } -#endif if (!is_uninterp_const(e)) continue; - auto f = to_app(e)->get_decl(); auto v = m_eval.get_value(to_app(e)); if (v) From bebcd9470327759739cd598d0be85c73d7a22e42 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 25 Apr 2024 10:29:34 -0400 Subject: [PATCH 30/49] enable logging nla lemmas Signed-off-by: Nikolaj Bjorner --- src/ast/sls/bv_sls_eval.h | 8 ++++++++ src/math/lp/nra_solver.cpp | 22 ++++++++++++++++++++++ src/nlsat/nlsat_solver.cpp | 4 ++++ src/nlsat/nlsat_solver.h | 2 ++ src/smt/params/smt_params_helper.pyg | 1 + 5 files changed, 37 insertions(+) diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index 89cd3f4cf..4384660e7 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -25,6 +25,12 @@ namespace bv { class sls_fixed; + class sls_eval_plugin { + public: + virtual ~sls_eval_plugin() {} + + }; + class sls_eval { struct config { unsigned m_prob_randomize_extract = 50; @@ -40,6 +46,8 @@ namespace bv { random_gen m_rand; config m_config; + scoped_ptr_vector m_plugins; + scoped_ptr_vector m_values; // expr-id -> bv valuation diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index 9c9db4e41..4c1b2b3ee 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -3,6 +3,10 @@ Author: Nikolaj Bjorner, Lev Nachmanson */ +#ifndef SINGLE_THREAD +#include +#endif +#include #include "math/lp/lar_solver.h" #include "math/lp/nra_solver.h" #include "nlsat/nlsat_solver.h" @@ -11,6 +15,7 @@ #include "util/map.h" #include "util/uint_set.h" #include "math/lp/nla_core.h" +#include "smt/params/smt_params_helper.hpp" namespace nra { @@ -157,6 +162,23 @@ struct solver::imp { TRACE("nra", m_nlsat->display(tout)); + smt_params_helper p(m_params); + if (p.arith_nl_log()) { + static unsigned id = 0; + std::stringstream strm; + +#ifndef SINGLE_THREAD + std::thread::id this_id = std::this_thread::get_id(); + strm << "nla_" << this_id << "." << (++id) << ".smt2"; +#else + strm << "nla_" << (++id) << ".smt2"; +#endif + std::ofstream out(strm.str()); + m_nlsat->display_smt2(out); + out << "(check-sat)\n"; + out.close(); + } + lbool r = l_undef; try { r = m_nlsat->check(); diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index d99603dcd..7a63f4e63 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -3863,6 +3863,10 @@ namespace nlsat { return out; } + std::ostream& solver::display_smt2(std::ostream & out) const { + return m_imp->display_smt2(out); + } + std::ostream& solver::display_smt2(std::ostream & out, literal_vector const& ls) const { return display_smt2(out, ls.size(), ls.data()); } diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h index c65a2b4ff..15764150d 100644 --- a/src/nlsat/nlsat_solver.h +++ b/src/nlsat/nlsat_solver.h @@ -254,6 +254,8 @@ namespace nlsat { std::ostream& display_smt2(std::ostream & out, literal_vector const& ls) const; + std::ostream& display_smt2(std::ostream & out) const; + /** \brief Display variable diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 4e498b2c4..1ef795e4b 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -83,6 +83,7 @@ def_module_params(module_name='smt', ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'), ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'), ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'), + ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'), From 2ad9f220f281b82b601b3e2371fd02bfc9b2dc73 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2024 16:57:59 -0700 Subject: [PATCH 31/49] add logging --- src/ast/simplifiers/bound_simplifier.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/ast/simplifiers/bound_simplifier.cpp b/src/ast/simplifiers/bound_simplifier.cpp index 1a5d4c101..2d5094c4f 100644 --- a/src/ast/simplifiers/bound_simplifier.cpp +++ b/src/ast/simplifiers/bound_simplifier.cpp @@ -288,7 +288,8 @@ void bound_simplifier::tighten_bound(dependent_expr const& de) { void bound_simplifier::assert_upper(expr* x, rational const& n, bool strict) { scoped_mpq c(nm); - nm.set(c, n.to_mpq()); + nm.set(c, n.to_mpq()); + TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " < " : " <= ") << n << "\n"); bp.assert_upper(to_var(x), c, strict); } @@ -296,6 +297,7 @@ void bound_simplifier::assert_upper(expr* x, rational const& n, bool strict) { void bound_simplifier::assert_lower(expr* x, rational const& n, bool strict) { scoped_mpq c(nm); nm.set(c, n.to_mpq()); + TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " > " : " >= ") << n << "\n"); bp.assert_lower(to_var(x), c, strict); } @@ -306,6 +308,7 @@ bool bound_simplifier::has_lower(expr* x, rational& n, bool& strict) { return false; strict = m_interval.lower_is_open(i); n = m_interval.lower(i); + TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " > " : " >= ") << n << "\n"); return true; } @@ -316,6 +319,7 @@ bool bound_simplifier::has_upper(expr* x, rational& n, bool& strict) { return false; strict = m_interval.upper_is_open(i); n = m_interval.upper(i); + TRACE("propagate-ineqs", tout << to_var(x) << ": " << mk_pp(x, m) << (strict ? " < " : " <= ") << n << "\n"); return true; } From bc577b93ae3e88e2e34443b68aca66491f5efe03 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2024 16:58:22 -0700 Subject: [PATCH 32/49] refine precision before taking closest integral value. --- src/math/polynomial/algebraic_numbers.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp index 06b4465d7..a10e0dc98 100644 --- a/src/math/polynomial/algebraic_numbers.cpp +++ b/src/math/polynomial/algebraic_numbers.cpp @@ -2599,6 +2599,7 @@ namespace algebraic_numbers { qm().dec(v); } else { + refine_until_prec(const_cast(a), 1); bqm().floor(qm(), lower(a.to_algebraic()), v); } m_wrapper.set(b, v); @@ -2611,6 +2612,7 @@ namespace algebraic_numbers { qm().inc(v); } else { + refine_until_prec(const_cast(a), 1); bqm().ceil(qm(), upper(a.to_algebraic()), v); } m_wrapper.set(b, v); From 39dc8861eec43f91250bc0ad40943a8d457a2dc0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2024 16:59:50 -0700 Subject: [PATCH 33/49] expose comparisons with polynomials, incremental way to extract variables --- src/math/polynomial/polynomial.cpp | 89 +++++++++++++++++++++++++++--- src/math/polynomial/polynomial.h | 19 +++++-- 2 files changed, 94 insertions(+), 14 deletions(-) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index da6bc7b39..44a5c8864 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -190,6 +190,10 @@ namespace polynomial { } }; + bool operator==(monomial const& other) const { + return eq_proc()(this, &other); + } + static unsigned get_obj_size(unsigned sz) { return sizeof(monomial) + sz * sizeof(power); } monomial(unsigned id, unsigned sz, power const * pws, unsigned h): @@ -3221,9 +3225,16 @@ namespace polynomial { }; bool_vector m_found_vars; - void vars(polynomial const * p, var_vector & xs) { - xs.reset(); + void begin_vars_incremental() { m_found_vars.reserve(num_vars(), false); + } + void end_vars_incremental(var_vector& xs) { + // reset m_found_vars + unsigned sz = xs.size(); + for (unsigned i = 0; i < sz; i++) + m_found_vars[xs[i]] = false; + } + void vars(polynomial const * p, var_vector & xs) { unsigned sz = p->size(); for (unsigned i = 0; i < sz; i++) { monomial * m = p->m(i); @@ -3236,10 +3247,6 @@ namespace polynomial { } } } - // reset m_found_vars - sz = xs.size(); - for (unsigned i = 0; i < sz; i++) - m_found_vars[xs[i]] = false; } typedef sbuffer power_buffer; @@ -6045,6 +6052,47 @@ namespace polynomial { } return true; } + + bool ge(polynomial const* p, polynomial const* q) { + unsigned sz1 = p->size(); + unsigned sz2 = q->size(); + unsigned i = 0, j = 0; + while (i < sz1 || j < sz2) { + auto * m1 = i < sz1 ? p->m(i) : q->m(j); + auto & a1 = i < sz1 ? p->a(i) : q->a(j); + auto * m2 = j < sz2 ? q->m(j) : p->m(i); + auto & a2 = j < sz2 ? q->a(j) : p->a(i); + + if (i < sz1 && j == sz2 && m1->is_unit()) { + if (!m_manager.is_pos(a1)) + return false; + ++i; + continue; + } + + if (i == sz1 && j < sz2 && m2->is_unit()) { + if (!m_manager.is_neg(a2)) + return false; + ++j; + continue; + } + + if (i == sz1 || j == sz2) + break; + + if (!(*m1 == *m2)) { + if (m_manager.is_pos(a1) && m1->is_square()) { + ++i; + continue; + } + return false; + } + if (!m_manager.ge(a1, a2)) + return false; + ++i, ++j; + } + return i == sz1 && j == sz2; + } // Functor used to compute the maximal degree of each variable in a polynomial p. class var_max_degree { @@ -7228,13 +7276,33 @@ namespace polynomial { return m_imp->is_nonneg(p); } + bool manager::ge(polynomial const* p, polynomial const* q) { + return m_imp->ge(p, q); + } + + void manager::rename(unsigned sz, var const * xs) { return m_imp->rename(sz, xs); } void manager::vars(polynomial const * p, var_vector & xs) { + xs.reset(); + m_imp->begin_vars_incremental(); + m_imp->vars(p, xs); + m_imp->end_vars_incremental(xs); + } + + void manager::vars_incremental(polynomial const * p, var_vector & xs) { m_imp->vars(p, xs); } + void manager::begin_vars_incremental() { + m_imp->begin_vars_incremental(); + } + + void manager::end_vars_incremental(var_vector & xs) { + m_imp->end_vars_incremental(xs); + } + polynomial * manager::substitute(polynomial const * p, var2mpq const & x2v) { return m_imp->substitute(p, x2v); @@ -7293,17 +7361,20 @@ namespace polynomial { return m_imp->eval(p, x2v, r); } - void manager::display(std::ostream & out, monomial const * m, display_var_proc const & proc, bool user_star) const { + std::ostream& manager::display(std::ostream & out, monomial const * m, display_var_proc const & proc, bool user_star) const { m->display(out, proc, user_star); + return out; } - void manager::display(std::ostream & out, polynomial const * p, display_var_proc const & proc, bool use_star) const { + std::ostream& manager::display(std::ostream & out, polynomial const * p, display_var_proc const & proc, bool use_star) const { SASSERT(m_imp->consistent_coeffs(p)); p->display(out, m_imp->m_manager, proc, use_star); + return out; } - void manager::display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc) const { + std::ostream& manager::display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc) const { p->display_smt2(out, m_imp->m_manager, proc); + return out; } }; diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h index 416422f64..48fe5ffeb 100644 --- a/src/math/polynomial/polynomial.h +++ b/src/math/polynomial/polynomial.h @@ -921,6 +921,13 @@ namespace polynomial { */ bool is_nonneg(polynomial const * p); + + /** + \brief Return true if p is always greater or equal to q. + This is an incomplete check + */ + bool ge(polynomial const* p, polynomial const* q); + /** \brief Make sure the monomials in p are sorted using lexicographical order. Remark: the maximal monomial is at position 0. @@ -931,6 +938,9 @@ namespace polynomial { \brief Collect variables that occur in p into xs */ void vars(polynomial const * p, var_vector & xs); + void vars_incremental(polynomial const * p, var_vector & xs); + void begin_vars_incremental(); + void end_vars_incremental(var_vector & xs); /** \brief Evaluate polynomial p using the assignment [x_1 -> v_1, ..., x_n -> v_n]. @@ -1019,15 +1029,14 @@ namespace polynomial { */ void exact_pseudo_division_mod_d(polynomial const * p, polynomial const * q, var x, var2degree const & x2d, polynomial_ref & Q, polynomial_ref & R); - void display(std::ostream & out, monomial const * m, display_var_proc const & proc = display_var_proc(), bool use_star = true) const; + std::ostream& display(std::ostream & out, monomial const * m, display_var_proc const & proc = display_var_proc(), bool use_star = true) const; - void display(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc(), bool use_star = false) const; + std::ostream& display(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc(), bool use_star = false) const; - void display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc()) const; + std::ostream& display_smt2(std::ostream & out, polynomial const * p, display_var_proc const & proc = display_var_proc()) const; friend std::ostream & operator<<(std::ostream & out, polynomial_ref const & p) { - p.m().display(out, p); - return out; + return p.m().display(out, p); } }; From 4c070f9e76fc11893c705e67ef675aa58f7bff45 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2024 17:00:05 -0700 Subject: [PATCH 34/49] add extra fields to nlsat-clause --- src/nlsat/nlsat_clause.cpp | 5 ++++- src/nlsat/nlsat_clause.h | 17 +++++++++++++---- 2 files changed, 17 insertions(+), 5 deletions(-) diff --git a/src/nlsat/nlsat_clause.cpp b/src/nlsat/nlsat_clause.cpp index a64ec2856..268086c24 100644 --- a/src/nlsat/nlsat_clause.cpp +++ b/src/nlsat/nlsat_clause.cpp @@ -25,7 +25,10 @@ namespace nlsat { m_size(sz), m_capacity(sz), m_learned(learned), - m_activity(0), + m_active(false), + m_removed(false), + m_marked(false), + m_var_hash(0), m_assumptions(as) { for (unsigned i = 0; i < sz; i++) { m_lits[i] = lits[i]; diff --git a/src/nlsat/nlsat_clause.h b/src/nlsat/nlsat_clause.h index 7c3416feb..91467303c 100644 --- a/src/nlsat/nlsat_clause.h +++ b/src/nlsat/nlsat_clause.h @@ -29,7 +29,10 @@ namespace nlsat { unsigned m_size; unsigned m_capacity:31; unsigned m_learned:1; - unsigned m_activity; + unsigned m_active:1; + unsigned m_removed:1; + unsigned m_marked:1; + unsigned m_var_hash; assumption_set m_assumptions; literal m_lits[0]; static size_t get_obj_size(unsigned num_lits) { return sizeof(clause) + num_lits * sizeof(literal); } @@ -46,9 +49,15 @@ namespace nlsat { literal const * begin() const { return m_lits; } literal const * end() const { return m_lits + m_size; } literal const * data() const { return m_lits; } - void inc_activity() { m_activity++; } - void set_activity(unsigned v) { m_activity = v; } - unsigned get_activity() const { return m_activity; } + void set_active(bool b) { m_active = b; } + bool is_active() const { return m_active; } + void set_removed() { m_removed = true; } + bool is_removed() const { return m_removed; } + unsigned var_hash() const { return m_var_hash; } + void set_var_hash(unsigned h) { m_var_hash = h; } + bool is_marked() const { return m_marked; } + void mark() { m_marked = true; } + void unmark() { m_marked = false; } bool contains(literal l) const; bool contains(bool_var v) const; void shrink(unsigned num_lits) { SASSERT(num_lits <= m_size); if (num_lits < m_size) { m_size = num_lits; } } From b0222cbdaa1ad345ac39b3b904ba55f127448be0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2024 17:00:49 -0700 Subject: [PATCH 35/49] temper warning messages from uninitalized pointers --- src/util/hashtable.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/hashtable.h b/src/util/hashtable.h index b2830326b..b59a2e7d8 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -472,7 +472,7 @@ public: that was already in the table. */ data const & insert_if_not_there(data const & e) { - entry * et; + entry * et = nullptr; insert_if_not_there_core(e, et); return et->get_data(); } @@ -482,7 +482,7 @@ public: Return the entry that contains e. */ entry * insert_if_not_there2(data const & e) { - entry * et; + entry * et = nullptr; insert_if_not_there_core(e, et); return et; } From 29e724f78737949d4da73bfaa46fac77a4a43b8e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2024 17:05:21 -0700 Subject: [PATCH 36/49] add gc to lemmas, convert bounds constraints to lemmas, add simplification pre-processing beyond equality extraction --- src/nlsat/nlsat_solver.cpp | 833 +++++++++++++++++++++++++++++++++---- 1 file changed, 747 insertions(+), 86 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 7a63f4e63..8d9e563f8 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -85,6 +85,16 @@ namespace nlsat { typedef polynomial::cache cache; typedef ptr_vector interval_set_vector; + struct bound_constraint { + var x; + polynomial_ref A, B; + bool is_strict; + clause* c; + bound_constraint(var x, polynomial_ref& A, polynomial_ref& B, bool is_strict, clause* c): + x(x), A(A), B(B), is_strict(is_strict), c(c) {} + }; + + ctx& m_ctx; solver& m_solver; reslimit& m_rlimit; @@ -95,13 +105,13 @@ namespace nlsat { cache m_cache; anum_manager& m_am; mutable assumption_manager m_asm; - assignment m_assignment; // partial interpretation + assignment m_assignment, m_lo, m_hi; // partial interpretation evaluator m_evaluator; interval_set_manager & m_ism; ineq_atom_table m_ineq_atoms; root_atom_table m_root_atoms; - svector m_patch_var; - polynomial_ref_vector m_patch_num, m_patch_denom; + + vector m_bounds; id_gen m_cid_gen; clause_vector m_clauses; // set of clauses @@ -228,11 +238,9 @@ namespace nlsat { m_cache(m_pm), m_am(c.m_am), m_asm(*this, m_allocator), - m_assignment(m_am), + m_assignment(m_am), m_lo(m_am), m_hi(m_am), m_evaluator(s, m_assignment, m_pm, m_allocator), m_ism(m_evaluator.ism()), - m_patch_num(m_pm), - m_patch_denom(m_pm), m_num_bool_vars(0), m_display_var(m_perm), m_display_assumption(nullptr), @@ -288,6 +296,8 @@ namespace nlsat { del_unref_atoms(); m_cache.reset(); m_assignment.reset(); + m_lo.reset(); + m_hi.reset(); } void clear() { @@ -1512,8 +1522,6 @@ namespace nlsat { TRACE("nlsat", display_smt2(tout);); m_bk = 0; m_xk = null_var; - m_conflicts = 0; - m_next_conflict = 100; while (true) { CASSERT("nlsat", check_satisfied()); @@ -1565,6 +1573,26 @@ namespace nlsat { } } + void gc() { + if (m_learned.size() <= 2*m_clauses.size()) + return; + reset_watches(); + reinit_cache(); + unsigned j = 0; + for (unsigned i = 0; i < m_learned.size(); ++i) { + auto cls = m_learned[i]; + if (i - j < m_clauses.size() && cls->size() > 1 && !cls->is_active()) + del_clause(cls); + else { + m_learned[j++] = cls; + cls->set_active(false); + } + } + m_learned.shrink(j); + reattach_arith_clauses(m_clauses); + reattach_arith_clauses(m_learned); + } + unsigned m_next_conflict = 100; void log() { if (m_conflicts < m_next_conflict) @@ -1576,6 +1604,8 @@ namespace nlsat { lbool search_check() { lbool r = l_undef; + m_conflicts = 0; + m_next_conflict = 100; while (true) { r = search(); if (r != l_true) break; @@ -1593,14 +1623,19 @@ namespace nlsat { // derive tight bounds. while (true) { lo++; - if (!m_am.gt(v, lo.to_mpq())) { lo--; break; } + if (!m_am.gt(v, lo.to_mpq())) { + lo--; + break; + } } bounds.push_back(std::make_pair(x, lo)); } } if (bounds.empty()) break; - init_search(); + gc(); + init_search(); + IF_VERBOSE(2, verbose_stream() << "(nlsat-b&b :conflicts " << m_conflicts << " :decisions " << m_decisions << " :propagations " << m_propagations << " :clauses " << m_clauses.size() << " :learned " << m_learned.size() << ")\n"); for (auto const& b : bounds) { var x = b.first; rational lo = b.second; @@ -1617,7 +1652,7 @@ namespace nlsat { m_lemma.push_back(~mk_ineq_literal(atom::LT, 1, &p2, &is_even)); // perform branch and bound - clause * cls = mk_clause(m_lemma.size(), m_lemma.data(), false, nullptr); + clause * cls = mk_clause(m_lemma.size(), m_lemma.data(), true, nullptr); if (cls) { TRACE("nlsat", display(tout << "conflict " << lo << " " << hi, *cls); tout << "\n";); } @@ -1826,8 +1861,9 @@ namespace nlsat { } } - void resolve_clause(bool_var b, clause const & c) { + void resolve_clause(bool_var b, clause & c) { TRACE("nlsat_resolve", tout << "resolving clause "; if (b != null_bool_var) tout << "for b: " << b << "\n"; display(tout, c) << "\n";); + c.set_active(true); resolve_clause(b, c.size(), c.data()); m_lemma_assumptions = m_asm.mk_join(static_cast<_assumption_set>(c.assumptions()), m_lemma_assumptions); } @@ -2009,8 +2045,8 @@ namespace nlsat { /** \brief Return true if the conflict was solved. */ - bool resolve(clause const & conflict) { - clause const * conflict_clause = &conflict; + bool resolve(clause & conflict) { + clause * conflict_clause = &conflict; m_lemma_assumptions = nullptr; start: SASSERT(check_marks()); @@ -2405,7 +2441,7 @@ namespace nlsat { } bool can_reorder() const { - return m_patch_var.empty() + return m_bounds.empty() && all_of(m_learned, [&](clause* c) { return !has_root_atom(*c); }) && all_of(m_clauses, [&](clause* c) { return !has_root_atom(*c); }); } @@ -2679,6 +2715,10 @@ namespace nlsat { // solve simple equalities // TBD WU-Reit decomposition? + // - elim_unconstrained + // - solve_eqs + // - fm + /** \brief isolate variables in unit equalities. Assume a clause is c == v*p + q @@ -2694,7 +2734,503 @@ namespace nlsat { The method ignores lemmas and assumes constraints don't use roots. */ + vector> m_var_occurs; + bool simplify() { + unsigned sz = m_clauses.size(); + while (true) { + + while (elim_uncnstr()) + ; + + while (fm()) + ; + + if (!solve_eqs()) + return false; + + subsumption_simplify(); + if (m_clauses.size() >= sz) + break; + sz = m_clauses.size(); + } + + IF_VERBOSE(3, display(verbose_stream())); + + return true; + } + + // + // + bool elim_uncnstr() { + // compute variable occurrences + if (any_of(m_clauses, [&](clause* c) { return has_root_atom(*c); })) + return false; + compute_occurs(); + // for each variable occurrence, figure out if it is unconstrained. + ptr_vector to_delete; + for (unsigned v = m_var_occurs.size(); v-- > 0; ) { + auto& clauses = m_var_occurs[v]; + if (clauses.size() != 1) + continue; + auto& c = *clauses[0]; + if (c.is_removed()) + continue; + if (!is_unconstrained(v, c)) + continue; + c.set_removed(); + to_delete.push_back(&c); + } + for (auto* c : to_delete) + del_clause(c, m_clauses); + + return !to_delete.empty(); + } + + void compute_occurs(clause& c) { + var_vector vars; + m_pm.begin_vars_incremental(); + for (auto lit : c) { + bool_var b = lit.var(); + atom* a = m_atoms[b]; + if (!a) + continue; + if (a->is_ineq_atom()) { + auto sz = to_ineq_atom(a)->size(); + for (unsigned i = 0; i < sz; ++i) { + auto* p = to_ineq_atom(a)->p(i); + m_pm.vars_incremental(p, vars); + } + } + } + m_pm.end_vars_incremental(vars); + unsigned h = 0; + for (auto v : vars) { + m_var_occurs.reserve(v + 1); + m_var_occurs[v].push_back(&c); + h |= (1ul << (v % 32ul)); + } + c.set_var_hash(h); + } + + void compute_occurs() { + m_var_occurs.reset(); + for (auto c : m_clauses) + compute_occurs(*c); + } + + bool is_unconstrained(var x, clause& c) { + poly* p; + polynomial_ref A(m_pm), B(m_pm); + for (auto lit : c) { + bool_var b = lit.var(); + if (!m_atoms[b]) + continue; + auto& a = *to_ineq_atom(m_atoms[b]); + if (!is_single_poly(a, p)) + continue; + + if (1 != m_pm.degree(p, x)) + continue; + + A = m_pm.coeff(p, x, 1, B); + + if (a.is_eq() && !lit.sign()) { + // A*x + B = 0 + if (is_int(x) && is_unit(A)) { + m_bounds.push_back(bound_constraint(x, A, B, false, nullptr)); + return true; + } + + if (!is_int(x) && m_pm.is_const(A)) { + m_bounds.push_back(bound_constraint(x, A, B, false, nullptr)); + return true; + } + } + // TODO: add other cases for LT and GT atoms + } + return false; + } + + bool cleanup_removed() { + unsigned j = 0, sz = m_clauses.size(); + for (unsigned i = 0; i < sz; ++i) { + auto c = m_clauses[i]; + if (c->is_removed()) + del_clause(c); + else + m_clauses[j++] = c; + } + m_clauses.shrink(j); + return j < sz; + } + + // + // Fourier Motzkin elimination + // + + bool fm() { + if (any_of(m_clauses, [&](clause* c) { return has_root_atom(*c); })) + return false; + compute_occurs(); + + for (unsigned v = m_var_occurs.size(); v-- > 0; ) + apply_fm(v, m_var_occurs[v]); + + return cleanup_removed(); + } + + // progression of features + // unit literals + // single occurrence of x in C + // (x <= t or x <= s or C) == (x <= max(s, t) or C) + + + bool is_invertible(var x, polynomial_ref & A) { + if (!m_pm.is_const(A)) + return false; + if (is_int(x) && !is_unit(A)) + return false; + return true; + } + + bool apply_fm(var x, ptr_vector& clauses) { + polynomial_ref A(m_pm), B(m_pm); + vector lo, hi; + poly* p = nullptr; + bool all_solved = true; + for (auto c : clauses) { + if (c->is_removed()) + continue; + if (c->size() != 1) { + all_solved = false; + continue; + } + literal lit = (*c)[0]; + bool sign = lit.sign(); + ineq_atom const& a = *to_ineq_atom(m_atoms[lit.var()]); + if (sign && a.is_eq()) { + all_solved = false; + continue; + } + if (!is_single_poly(a, p)) { + all_solved = false; + continue; + } + if (1 != m_pm.degree(p, x)) { + all_solved = false; + continue; + } + A = m_pm.coeff(p, x, 1, B); + if (!is_invertible(x, A)) { + all_solved = false; + continue; + } + auto const& A_value = m_pm.coeff(A, 0); + bool is_pos = m_pm.m().is_pos(A_value); + bool is_strict = false; + switch (a.get_kind()) { + case atom::LT: + // !(Ax + B < 0) == Ax + B >= 0 + if (sign) + is_strict = false; + else { + // Ax + B < 0 == -Ax - B > 0 + A = -A; + B = -B; + is_pos = !is_pos; + if (is_int(x)) { + // Ax + B > 0 == Ax + B - |A| >= 0 + if (is_pos) + B = m_pm.add(B, A); + else + B = m_pm.sub(B, A); + is_strict = false; + } + else + is_strict = true; + } + break; + case atom::GT: + // !(Ax + B > 0) == -Ax + -B >= 0 + if (sign) { + A = -A; + B = -B; + is_pos = !is_pos; + is_strict = false; + } + else { + // Ax + B > 0 + if (is_int(x)) { + // Ax + B - |A| >= 0 + if (is_pos) + B = m_pm.sub(B, A); + else + B = m_pm.add(B, A); + is_strict = false; + } + else + is_strict = true; + } + break; + case atom::EQ: { + all_solved = false; + continue; + // unsound: + m_display_var(verbose_stream(), x); + display(verbose_stream() << " ", *c) << "\n"; + bound_constraint l(x, A, B, false, c); + bound_constraint h(x, -A, -B, false, c); + apply_fm_equality(x, clauses, l, h); + return true; + } + default: + UNREACHABLE(); + break; + } + auto& set = is_pos ? hi : lo; + bool found = false; + for (auto const& bound : set) { + if (is_strict == bound.is_strict && m_pm.eq(A, bound.A) && m_pm.eq(B, bound.B)) + found = true; + } + if (found) + continue; + + set.push_back(bound_constraint(x, A, B, is_strict, c)); + + } + + if (lo.empty() && hi.empty()) + return false; + + IF_VERBOSE(3, + verbose_stream() << "x" << x << " lo " << lo.size() << " hi " << hi.size() << "\n"; + for (auto c : clauses) + if (!c->is_removed()) + display(verbose_stream(), *c) << "\n"; + ); + + if (apply_fm_equality(x, clauses, lo, hi)) + return true; + + if (!all_solved) + return false; + + auto num_lo = lo.size(), num_hi = hi.size(); + if (num_lo >= 2 && num_hi >= 2 && (num_lo > 2 || num_hi > 2)) + return false; + + apply_fm_inequality(x, clauses, lo, hi); + + return true; + } + + void apply_fm_inequality( + var x, ptr_vector& clauses, + vector& lo, vector& hi) { + + polynomial_ref C(m_pm); + for (auto c : clauses) + c->set_removed(); + + for (auto const& l : lo) { + // l.A * x + l.B, l.is_strict;, l.A < 0 + for (auto const& h : hi) { + // h.A * x + h.B, h.is_strict; h.A > 0 + // (l.A x + l.B)*h.A + (h.A x + h.B)*|l.A| >= 0 + C = m_pm.mul(l.B, h.A); + C = m_pm.sub(C, m_pm.mul(h.B, l.A)); + poly* p = C.get(); + bool is_even = false; + m_lemma.reset(); + if (l.is_strict || h.is_strict) + m_lemma.push_back(mk_ineq_literal(atom::GT, 1, &p, &is_even)); + else + m_lemma.push_back(~mk_ineq_literal(atom::LT, 1, &p, &is_even)); + if (m_lemma[0] == true_literal) + continue; + auto a1 = static_cast<_assumption_set>(l.c->assumptions()); + auto a2 = static_cast<_assumption_set>(h.c->assumptions()); + auto cls = mk_clause(m_lemma.size(), m_lemma.data(), false, m_asm.mk_join(a1, a2)); + if (cls) + compute_occurs(*cls); + IF_VERBOSE(3, display(verbose_stream() << "add resolvent ", *cls) << "\n"); + } + } + + // track updates for model reconstruction + for (auto const& l : lo) + m_bounds.push_back(l); + for (auto const& h : hi) + m_bounds.push_back(h); + } + + bool apply_fm_equality( + var x, ptr_vector& clauses, + vector& lo, vector& hi) { + for (auto& l : lo) { + if (l.is_strict) + continue; + l.A = -l.A; + l.B = -l.B; + for (auto& h : hi) { + if (h.is_strict) + continue; + if (!m_pm.eq(l.B, h.B)) + continue; + if (!m_pm.eq(l.A, h.A)) + continue; + l.A = -l.A; + l.B = -l.B; + apply_fm_equality(x, clauses, l, h); + return true; + } + l.A = -l.A; + l.B = -l.B; + } + return false; + } + + void apply_fm_equality( + var x, ptr_vector& clauses, + bound_constraint& l, bound_constraint& h) { + auto a1 = static_cast<_assumption_set>(l.c->assumptions()); + auto a2 = static_cast<_assumption_set>(h.c->assumptions()); + a1 = m_asm.mk_join(a1, a2); + + // TODO: this can also replace solve_eqs + for (auto c : clauses) { + if (c->is_removed()) + continue; + c->set_removed(); + if (c == l.c || c == h.c) + continue; + m_lemma.reset(); + bool is_tautology = false; + for (literal lit : *c) { + lit = substitute_var(x, l.A, l.B, lit); + m_lemma.push_back(lit); + if (lit == true_literal) + is_tautology = true; + } + if (is_tautology) + continue; + a2 = static_cast<_assumption_set>(c->assumptions()); + auto cls = mk_clause(m_lemma.size(), m_lemma.data(), false, m_asm.mk_join(a1, a2)); + + IF_VERBOSE(3, + if (cls) { + verbose_stream() << "x" << x << " * " << l.A << " = " << l.B << "\n"; + display(verbose_stream(), *c) << " -> "; + display(verbose_stream(), *cls) << "\n"; + }); + if (cls) + compute_occurs(*cls); + } + // track updates for model reconstruction + m_bounds.push_back(l); + m_bounds.push_back(h); + } + + // + // Subsumption simplification + // + void subsumption_simplify() { + compute_occurs(); + for (unsigned v = m_var_occurs.size(); v-- > 0; ) { + auto& clauses = m_var_occurs[v]; + for (auto c : clauses) { + if (c->is_marked() || c->is_removed()) + continue; + c->mark(); + for (auto c2 : clauses) { + if (c == c2 || c2->is_removed()) + continue; + if (subsumes(*c, *c2)) { + IF_VERBOSE(3, display(verbose_stream() << "subsumes ", *c); + display(verbose_stream() << " ", *c2) << "\n"); + c2->set_removed(); + } + } + } + } + for (auto c : m_clauses) + c->unmark(); + + cleanup_removed(); + } + + // does c1 subsume c2? + bool subsumes(clause const& c1, clause const& c2) { + if (c1.size() > c2.size()) + return false; + if ((c1.var_hash() & c2.var_hash()) != c1.var_hash()) + return false; + for (auto lit1 : c1) { + if (!any_of(c2, [&](auto lit2) { return subsumes(lit1, lit2); })) + return false; + } + return true; + } + + bool subsumes(literal lit1, literal lit2) { + if (lit1 == lit2) + return true; + + atom* a1 = m_atoms[lit1.var()]; + atom* a2 = m_atoms[lit2.var()]; + if (!a1 || !a2) + return false; + + // use m_pm.ge(p1, p2) + // whenever lit1 = p1 < 0, lit2 = p2 < 0 + // or lit1 = p1 < 0, lit2 = !(p2 > 0) + // or lit1 = !(p1 > 0), lit2 = !(p2 > 0) + // use m_pm.ge(p2, p1) + // whenever lit1 = p1 > 0, lit2 = p2 > 0 + // or lit1 = !(p1 < 0), lit2 = !(p2 < 0) + // or lit1 = p1 > 0, lit2 = !(p2 < 0) + // or lit1 = !(p1 > 0), lit2 = p2 < 0 + // + if (a1->is_ineq_atom() && a2->is_ineq_atom()) { + auto& i1 = *to_ineq_atom(a1); + auto& i2 = *to_ineq_atom(a2); + auto is_lt1 = !lit1.sign() && a1->get_kind() == atom::kind::LT; + auto is_le1 = lit1.sign() && a1->get_kind() == atom::kind::GT; + auto is_gt1 = !lit1.sign() && a1->get_kind() == atom::kind::GT; + auto is_ge1 = lit1.sign() && a1->get_kind() == atom::kind::LT; + + auto is_lt2 = !lit2.sign() && a2->get_kind() == atom::kind::LT; + auto is_le2 = lit2.sign() && a2->get_kind() == atom::kind::GT; + auto is_gt2 = !lit2.sign() && a2->get_kind() == atom::kind::GT; + auto is_ge2 = lit2.sign() && a2->get_kind() == atom::kind::LT; + + auto check_ge = (is_lt1 && (is_lt2 || is_le2)) || (is_le1 && is_le2); + auto check_le = (is_gt1 && (is_gt2 || is_ge2)) || (is_ge1 && is_ge2); + + if (i1.size() != i2.size()) + ; + else if (check_ge) { + for (unsigned i = 0; i < i1.size(); ++i) + if (!m_pm.ge(i1.p(i), i2.p(i))) + return false; + return true; + } + else if (check_le) { + for (unsigned i = 0; i < i1.size(); ++i) + if (!m_pm.ge(i2.p(i), i1.p(i))) + return false; + return true; + } + } + return false; + } + + // + // Equality simplificadtion (TODO, this should is deprecated by fm) + // + bool solve_eqs() { polynomial_ref p(m_pm), q(m_pm); var v; init_var_signs(); @@ -2704,14 +3240,26 @@ namespace nlsat { change = false; for (clause* c : m_clauses) { if (solve_var(*c, v, p, q)) { - q = -q; + if (!m_pm.is_const(p)) + continue; + // optional throttles to restrict where solved variables are used + if (false && !m_pm.is_linear(q)) + continue; + if (false && !m_pm.is_univariate(q)) + continue; + bool is_small = true; + for (unsigned i = 0; i < m_pm.size(q) && is_small ; ++i) { + auto const& c = m_pm.coeff(q, i); + is_small &= m_pm.m().is_small(c); + } + if (!is_small && false) + continue; TRACE("nlsat", tout << "p: " << p << "\nq: " << q << "\n x" << v << "\n";); - m_patch_var.push_back(v); - m_patch_num.push_back(q); - m_patch_denom.push_back(p); - del_clause(c, m_clauses); - if (!substitute_var(v, p, q)) + m_bounds.push_back(bound_constraint(v, p, q, false, nullptr)); + + if (!substitute_var(v, p, q, *c)) return false; + del_clause(c, m_clauses); TRACE("nlsat", display(tout << "simplified\n");); change = true; break; @@ -2721,84 +3269,185 @@ namespace nlsat { return true; } + // Eliminated variables are tracked in m_bounds. + // Each element in m_bounds tracks the eliminated variable and an upper or lower bound + // that has to be satisfied. Variables that are eliminated through equalities are tracked + // by non-strict bounds. A satisfiable solution is required to provide an evaluation that + // is consistent with the bounds. For equalities, the non-strict lower or upper bound can + // always be assigned as a value to the variable. + void fix_patch() { - for (unsigned i = m_patch_var.size(); i-- > 0; ) { - var v = m_patch_var[i]; - poly* q = m_patch_num.get(i); - poly* p = m_patch_denom.get(i); - scoped_anum pv(m_am), qv(m_am), val(m_am); - m_pm.eval(p, m_assignment, pv); - m_pm.eval(q, m_assignment, qv); - SASSERT(!m_am.is_zero(pv)); - val = qv / pv; - TRACE("nlsat", - m_display_var(tout << "patch v" << v << " ", v) << "\n"; - if (m_assignment.is_assigned(v)) m_am.display(tout << "previous value: ", m_assignment.value(v)); tout << "\n"; - m_am.display(tout << "updated value: ", val); tout << "\n"; - ); - m_assignment.set_core(v, val); - } + m_lo.reset(); m_hi.reset(); + for (auto& b : m_bounds) + m_assignment.reset(b.x); + for (unsigned i = m_bounds.size(); i-- > 0; ) + fix_patch(m_bounds[i]); } - bool substitute_var(var x, poly* p, poly* q) { - bool is_sat = true; - polynomial_ref pr(m_pm); - polynomial_ref_vector ps(m_pm); + // x is unassigned, lo < x -> x <- lo + 1 + // x is unassigned, x < hi -> x <- hi - 1 + // x is unassigned, lo <= x -> x <- lo + // x is unassigned, x <= hi -> x <- hi + // x is assigned above hi, lo is strict lo < x < hi -> set x <- (lo + hi)/2 + // x is assigned below hi, above lo -> no-op + // x is assigned below lo, hi is strict lo < x < hi -> set x <-> (lo + hi)/2 + // x is assigned above hi, x <= hi -> x <- hi + // x is assigned blow lo, lo <= x -> x <- lo + void fix_patch(bound_constraint& b) { + var x = b.x; + scoped_anum Av(m_am), Bv(m_am), val(m_am); + m_pm.eval(b.A, m_assignment, Av); + m_pm.eval(b.B, m_assignment, Bv); + m_am.neg(Bv); + val = Bv / Av; + // Ax >= B + // is-lower : A > 0 + // is-upper: A < 0 + // x <- B / A + bool is_lower = m_am.is_pos(Av); + TRACE("nlsat", + m_display_var(tout << "patch v" << x << " ", x) << "\n"; + if (m_assignment.is_assigned(x)) m_am.display(tout << "previous value: ", m_assignment.value(x)); tout << "\n"; + m_am.display(tout << "updated value: ", val); tout << "\n"; + ); + if (!m_assignment.is_assigned(x)) { + if (!b.is_strict) + m_assignment.set_core(x, val); + else if (is_lower) + m_assignment.set_core(x, val + 1); + else + m_assignment.set_core(x, val - 1); + } + else { + auto& aval = m_assignment.value(x); + if (is_lower) { + // lo < value(x), lo < x -> x is unchanged + if (b.is_strict && m_am.lt(val, aval)) + ; + else if (!b.is_strict && m_am.le(val, aval)) + ; + else if (!b.is_strict) + m_assignment.set_core(x, val); + // aval < lo < x, hi is unassigned: x <- lo + 1 + else if (!m_hi.is_assigned(x)) + m_assignment.set_core(x, val + 1); + // aval < lo < x, hi is assigned: x <- (lo + hi) / 2 + else { + scoped_anum mid(m_am); + m_am.add(m_hi.value(x), val, mid); + mid = mid / 2; + m_assignment.set_core(x, mid); + } + } + else { + // dual to lower bounds + if (b.is_strict && m_am.lt(aval, val)) + ; + else if (!b.is_strict && m_am.le(aval, val)) + ; + else if (!b.is_strict) + m_assignment.set_core(x, val); + else if (!m_lo.is_assigned(x)) + m_assignment.set_core(x, val - 1); + else { + scoped_anum mid(m_am); + m_am.add(m_lo.value(x), val, mid); + mid = mid / 2; + m_assignment.set_core(x, mid); + } + } + } + + if (is_lower) { + if (!m_lo.is_assigned(x) || m_am.lt(m_lo.value(x), val)) + m_lo.set_core(x, val); + } + else { + if (!m_hi.is_assigned(x) || m_am.gt(m_hi.value(x), val)) + m_hi.set_core(x, val); + } + } + + literal substitute_var(var x, poly* p, poly* q, literal lit) { + auto b = lit.var(); + auto a = m_atoms[b]; + if (!a) + return lit; + SASSERT(a->is_ineq_atom()); + auto& a1 = *to_ineq_atom(a); + auto r = substitute_var(x, p, q, a1); + if (r == null_literal) + r = lit; + else if (lit.sign()) + r.neg(); + return r; + } + + literal substitute_var(var x, poly* p, poly* q, ineq_atom const& a) { + unsigned sz = a.size(); + bool_vector even; + polynomial_ref pr(m_pm), qq(q, m_pm); + qq = -qq; + polynomial_ref_vector ps(m_pm); + bool change = false; + auto k = a.get_kind(); + for (unsigned i = 0; i < sz; ++i) { + poly* po = a.p(i); + m_pm.substitute(po, x, qq, p, pr); + change |= pr != po; + TRACE("nlsat", tout << pr << "\n";); + if (m_pm.is_zero(pr)) { + ps.reset(); + even.reset(); + ps.push_back(pr); + even.push_back(false); + break; + } + if (m_pm.is_const(pr)) { + if (!a.is_even(i) && m_pm.m().is_neg(m_pm.coeff(pr, 0))) + k = atom::flip(k); + continue; + } + ps.push_back(pr); + even.push_back(a.is_even(i)); + } + if (!change) + return null_literal; + return mk_ineq_literal(k, ps.size(), ps.data(), even.data()); + } + + bool substitute_var(var x, poly* p, poly* q, clause& src) { u_map b2l; scoped_literal_vector lits(m_solver); - bool_vector even; unsigned num_atoms = m_atoms.size(); for (unsigned j = 0; j < num_atoms; ++j) { atom* a = m_atoms[j]; if (a && a->is_ineq_atom()) { ineq_atom const& a1 = *to_ineq_atom(a); - unsigned sz = a1.size(); - ps.reset(); - even.reset(); - bool change = false; - auto k = a1.get_kind(); - for (unsigned i = 0; i < sz; ++i) { - poly * po = a1.p(i); - m_pm.substitute(po, x, q, p, pr); - change |= pr != po; - TRACE("nlsat", tout << pr << "\n";); - if (m_pm.is_zero(pr)) { - ps.reset(); - even.reset(); - ps.push_back(pr); - even.push_back(false); - break; - } - if (m_pm.is_const(pr)) { - if (!a1.is_even(i) && m_pm.m().is_neg(m_pm.coeff(pr, 0))) { - k = atom::flip(k); - } - continue; - } - ps.push_back(pr); - even.push_back(a1.is_even(i)); - } - if (!change) continue; - literal l = mk_ineq_literal(k, ps.size(), ps.data(), even.data()); + literal l = substitute_var(x, p, q, a1); + if (l == null_literal) + continue; lits.push_back(l); if (a1.m_bool_var != l.var()) { b2l.insert(a1.m_bool_var, l); } } } - is_sat = update_clauses(b2l); - return is_sat; + return update_clauses(b2l, src); } - bool update_clauses(u_map const& b2l) { + bool update_clauses(u_map const& b2l, clause& src) { bool is_sat = true; literal_vector lits; clause_vector to_delete; unsigned n = m_clauses.size(); + auto a1 = static_cast<_assumption_set>(src.assumptions()); for (unsigned i = 0; i < n; ++i) { clause* c = m_clauses[i]; + if (c == &src) + continue; lits.reset(); bool changed = false; bool is_tautology = false; @@ -2827,7 +3476,9 @@ namespace nlsat { is_sat = false; } else { - mk_clause(lits.size(), lits.data(), c->is_learned(), static_cast<_assumption_set>(c->assumptions())); + auto a2 = static_cast<_assumption_set>(c->assumptions()); + auto a = m_asm.mk_join(a1, a2); + mk_clause(lits.size(), lits.data(), c->is_learned(), a); } } } @@ -2855,12 +3506,14 @@ namespace nlsat { \brief determine whether the clause is a comparison v > k or v < k', where k >= 0 or k' <= 0. */ lbool is_cmp0(clause const& c, var& v) { - if (!is_unit_ineq(c)) return l_undef; + if (!is_unit_ineq(c)) + return l_undef; literal lit = c[0]; ineq_atom const& a = *to_ineq_atom(m_atoms[lit.var()]); bool sign = lit.sign(); poly * p0; - if (!is_single_poly(a, p0)) return l_undef; + if (!is_single_poly(a, p0)) + return l_undef; if (m_pm.is_var(p0, v)) { if (!sign && a.get_kind() == atom::GT) { return l_true; @@ -2924,18 +3577,19 @@ namespace nlsat { */ bool solve_var(clause& c, var& v, polynomial_ref& p, polynomial_ref& q) { poly* p0; - if (!is_unit_eq(c)) return false; + if (!is_unit_eq(c)) + return false; ineq_atom & a = *to_ineq_atom(m_atoms[c[0].var()]); - if (!is_single_poly(a, p0)) return false; + if (!is_single_poly(a, p0)) + return false; var mx = max_var(p0); - if (mx >= m_is_int.size()) return false; + if (mx >= m_is_int.size()) + return false; for (var x = 0; x <= mx; ++x) { - if (is_int(x)) - continue; if (1 == m_pm.degree(p0, x)) { p = m_pm.coeff(p0, x, 1, q); - if (!m_pm.is_const(p)) - break; + if (!is_invertible(x, p)) + continue; switch (m_pm.sign(p, m_var_signs)) { case l_true: v = x; @@ -2951,7 +3605,15 @@ namespace nlsat { } } return false; - } + } + + + bool is_unit(polynomial_ref const& p) { + if (!m_pm.is_const(p)) + return false; + auto const& c = m_pm.coeff(p, 0); + return m_pm.m().is_one(c) || m_pm.m().is_minus_one(c); + } // ----------------------- // @@ -3090,8 +3752,7 @@ namespace nlsat { } std::ostream& display_polynomial_smt2(std::ostream & out, poly const* p, display_var_proc const & proc) const { - m_pm.display_smt2(out, p, proc); - return out; + return m_pm.display_smt2(out, p, proc); } std::ostream& display_ineq_smt2(std::ostream & out, ineq_atom const & a, display_var_proc const & proc) const { From aa1a59639445739539003d5b7a0f0ef5502cae08 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2024 17:05:40 -0700 Subject: [PATCH 37/49] add doc-string --- src/nlsat/nlsat_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 8d9e563f8..a1b653a89 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2761,6 +2761,7 @@ namespace nlsat { } // + // Remove unconstrained assertions. // bool elim_uncnstr() { // compute variable occurrences From 1ef43540807559decd41329b8993341ed55fe124 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 Apr 2024 17:52:00 -0700 Subject: [PATCH 38/49] fix build Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index a1b653a89..b155a0f37 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2981,7 +2981,9 @@ namespace nlsat { m_display_var(verbose_stream(), x); display(verbose_stream() << " ", *c) << "\n"; bound_constraint l(x, A, B, false, c); - bound_constraint h(x, -A, -B, false, c); + A = -A; + B = -B; + bound_constraint h(x, A, B, false, c); apply_fm_equality(x, clauses, l, h); return true; } From 869643a551d8edcd707c9d789d8f76f314f0c3e6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 May 2024 10:07:37 -0700 Subject: [PATCH 39/49] fix memory leak --- src/nlsat/nlsat_solver.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index b155a0f37..98ee5233e 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -3033,7 +3033,7 @@ namespace nlsat { var x, ptr_vector& clauses, vector& lo, vector& hi) { - polynomial_ref C(m_pm); + polynomial_ref C(m_pm), D(m_pm); for (auto c : clauses) c->set_removed(); @@ -3043,7 +3043,8 @@ namespace nlsat { // h.A * x + h.B, h.is_strict; h.A > 0 // (l.A x + l.B)*h.A + (h.A x + h.B)*|l.A| >= 0 C = m_pm.mul(l.B, h.A); - C = m_pm.sub(C, m_pm.mul(h.B, l.A)); + D = m_pm.mul(h.B, l.A); + C = m_pm.sub(C, D); poly* p = C.get(); bool is_even = false; m_lemma.reset(); @@ -3101,6 +3102,7 @@ namespace nlsat { auto a1 = static_cast<_assumption_set>(l.c->assumptions()); auto a2 = static_cast<_assumption_set>(h.c->assumptions()); a1 = m_asm.mk_join(a1, a2); + m_lemma_assumptions = a1; // TODO: this can also replace solve_eqs for (auto c : clauses) { From 04c55c34e523c83ba4fd3b21ab927b46b77403ce Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 May 2024 14:45:15 -0700 Subject: [PATCH 40/49] fix unsoundness bug Signed-off-by: Nikolaj Bjorner --- src/math/polynomial/polynomial.cpp | 21 +++++++++++++++++++++ src/nlsat/nlsat_solver.cpp | 15 +++++++++++---- 2 files changed, 32 insertions(+), 4 deletions(-) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 44a5c8864..97f0e25e5 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -6317,6 +6317,27 @@ namespace polynomial { return R.mk(); } + // x*q = p + // + // md = degree of x in p + // P = m0 + ... + // m0 = x^dm*m1 + // m1 * p^dm * q^{md - dm} + // P' = m1 + ... + // property would be that x*q = p => P > 0 <=> P' > 0 + // requires that q > 0 + // Reasoning: + // P > 0 + // <=> { since q > 0 } + // q^md * P > 0 + // <=> + // q^md*x^dm*m0 + .. > 0 + // <=> + // q^{md-dm}*(xq)^dm*m0 + ... > 0 + // <=> + // q^{md-dm}*p^dm + .. > 0 + // <=> + // P' > 0 void substitute(polynomial const* r, var x, polynomial const* p, polynomial const* q, polynomial_ref& result) { unsigned md = degree(r, x); if (md == 0) { diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 98ee5233e..d986f967a 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -2742,10 +2742,8 @@ namespace nlsat { while (elim_uncnstr()) ; - while (fm()) ; - if (!solve_eqs()) return false; @@ -3017,6 +3015,8 @@ namespace nlsat { if (apply_fm_equality(x, clauses, lo, hi)) return true; + return false; + if (!all_solved) return false; @@ -3104,6 +3104,13 @@ namespace nlsat { a1 = m_asm.mk_join(a1, a2); m_lemma_assumptions = a1; + polynomial_ref A(l.A), B(l.B); + + if (m_pm.is_neg(l.A)) { + A = -A; + B = -B; + } + // TODO: this can also replace solve_eqs for (auto c : clauses) { if (c->is_removed()) @@ -3114,7 +3121,7 @@ namespace nlsat { m_lemma.reset(); bool is_tautology = false; for (literal lit : *c) { - lit = substitute_var(x, l.A, l.B, lit); + lit = substitute_var(x, A, B, lit); m_lemma.push_back(lit); if (lit == true_literal) is_tautology = true; @@ -3126,7 +3133,7 @@ namespace nlsat { IF_VERBOSE(3, if (cls) { - verbose_stream() << "x" << x << " * " << l.A << " = " << l.B << "\n"; + m_display_var(verbose_stream(), x) << " * " << l.A << " = " << l.B << "\n"; display(verbose_stream(), *c) << " -> "; display(verbose_stream(), *cls) << "\n"; }); From 231a985bf9beb6aab9719324bd1f2e74f90c3d14 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 May 2024 16:17:06 -0700 Subject: [PATCH 41/49] add virtual destructor to z3::object class Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index cb1446a08..5d0d9425e 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -470,6 +470,7 @@ namespace z3 { context * m_ctx; public: object(context & c):m_ctx(&c) {} + virtual ~object() = default; context & ctx() const { return *m_ctx; } Z3_error_code check_error() const { return m_ctx->check_error(); } friend void check_context(object const & a, object const & b); From 19eb7225ea6bc4fab1bc9aa742e203e5344b38f0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 May 2024 16:20:05 -0700 Subject: [PATCH 42/49] add virtual destructor to z3::object class Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 5d0d9425e..4025be4fd 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -509,7 +509,7 @@ namespace z3 { object::operator=(o); return *this; } - ~param_descrs() { Z3_param_descrs_dec_ref(ctx(), m_descrs); } + ~param_descrs() override { Z3_param_descrs_dec_ref(ctx(), m_descrs); } static param_descrs simplify_param_descrs(context& c) { return param_descrs(c, Z3_simplify_get_param_descrs(c)); } static param_descrs global_param_descrs(context& c) { return param_descrs(c, Z3_get_global_param_descrs(c)); } @@ -527,7 +527,7 @@ namespace z3 { public: params(context & c):object(c) { m_params = Z3_mk_params(c); Z3_params_inc_ref(ctx(), m_params); } params(params const & s):object(s), m_params(s.m_params) { Z3_params_inc_ref(ctx(), m_params); } - ~params() { Z3_params_dec_ref(ctx(), m_params); } + ~params() override { Z3_params_dec_ref(ctx(), m_params); } operator Z3_params() const { return m_params; } params & operator=(params const & s) { Z3_params_inc_ref(s.ctx(), s.m_params); @@ -555,7 +555,7 @@ namespace z3 { ast(context & c):object(c), m_ast(0) {} ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); } ast(ast const & s) :object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); } - ~ast() { if (m_ast) { Z3_dec_ref(*m_ctx, m_ast); } } + ~ast() override { if (m_ast) { Z3_dec_ref(*m_ctx, m_ast); } } operator Z3_ast() const { return m_ast; } operator bool() const { return m_ast != 0; } ast & operator=(ast const & s) { @@ -593,7 +593,7 @@ namespace z3 { ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); } ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); } - ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); } + ~ast_vector_tpl() override { Z3_ast_vector_dec_ref(ctx(), m_vector); } operator Z3_ast_vector() const { return m_vector; } unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); } T operator[](unsigned i) const { Z3_ast r = Z3_ast_vector_get(ctx(), m_vector, i); check_error(); return cast_ast()(ctx(), r); } @@ -2528,7 +2528,7 @@ namespace z3 { public: func_entry(context & c, Z3_func_entry e):object(c) { init(e); } func_entry(func_entry const & s):object(s) { init(s.m_entry); } - ~func_entry() { Z3_func_entry_dec_ref(ctx(), m_entry); } + ~func_entry() override { Z3_func_entry_dec_ref(ctx(), m_entry); } operator Z3_func_entry() const { return m_entry; } func_entry & operator=(func_entry const & s) { Z3_func_entry_inc_ref(s.ctx(), s.m_entry); @@ -2551,7 +2551,7 @@ namespace z3 { public: func_interp(context & c, Z3_func_interp e):object(c) { init(e); } func_interp(func_interp const & s):object(s) { init(s.m_interp); } - ~func_interp() { Z3_func_interp_dec_ref(ctx(), m_interp); } + ~func_interp() override { Z3_func_interp_dec_ref(ctx(), m_interp); } operator Z3_func_interp() const { return m_interp; } func_interp & operator=(func_interp const & s) { Z3_func_interp_inc_ref(s.ctx(), s.m_interp); @@ -2585,7 +2585,7 @@ namespace z3 { model(context & c, Z3_model m):object(c) { init(m); } model(model const & s):object(s) { init(s.m_model); } model(model& src, context& dst, translate) : object(dst) { init(Z3_model_translate(src.ctx(), src, dst)); } - ~model() { Z3_model_dec_ref(ctx(), m_model); } + ~model() override { Z3_model_dec_ref(ctx(), m_model); } operator Z3_model() const { return m_model; } model & operator=(model const & s) { Z3_model_inc_ref(s.ctx(), s.m_model); @@ -2665,7 +2665,7 @@ namespace z3 { stats(context & c):object(c), m_stats(0) {} stats(context & c, Z3_stats e):object(c) { init(e); } stats(stats const & s):object(s) { init(s.m_stats); } - ~stats() { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); } + ~stats() override { if (m_stats) Z3_stats_dec_ref(ctx(), m_stats); } operator Z3_stats() const { return m_stats; } stats & operator=(stats const & s) { Z3_stats_inc_ref(s.ctx(), s.m_stats); @@ -2747,7 +2747,7 @@ namespace z3 { solver(context & c, solver const& src, translate): object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); } solver(solver const & s):object(s) { init(s.m_solver); } solver(solver const& s, simplifier const& simp); - ~solver() { Z3_solver_dec_ref(ctx(), m_solver); } + ~solver() override { Z3_solver_dec_ref(ctx(), m_solver); } operator Z3_solver() const { return m_solver; } solver & operator=(solver const & s) { Z3_solver_inc_ref(s.ctx(), s.m_solver); @@ -2968,7 +2968,7 @@ namespace z3 { goal(context & c, bool models=true, bool unsat_cores=false, bool proofs=false):object(c) { init(Z3_mk_goal(c, models, unsat_cores, proofs)); } goal(context & c, Z3_goal s):object(c) { init(s); } goal(goal const & s):object(s) { init(s.m_goal); } - ~goal() { Z3_goal_dec_ref(ctx(), m_goal); } + ~goal() override { Z3_goal_dec_ref(ctx(), m_goal); } operator Z3_goal() const { return m_goal; } goal & operator=(goal const & s) { Z3_goal_inc_ref(s.ctx(), s.m_goal); @@ -3026,7 +3026,7 @@ namespace z3 { public: apply_result(context & c, Z3_apply_result s):object(c) { init(s); } apply_result(apply_result const & s):object(s) { init(s.m_apply_result); } - ~apply_result() { Z3_apply_result_dec_ref(ctx(), m_apply_result); } + ~apply_result() override { Z3_apply_result_dec_ref(ctx(), m_apply_result); } operator Z3_apply_result() const { return m_apply_result; } apply_result & operator=(apply_result const & s) { Z3_apply_result_inc_ref(s.ctx(), s.m_apply_result); @@ -3051,7 +3051,7 @@ namespace z3 { tactic(context & c, char const * name):object(c) { Z3_tactic r = Z3_mk_tactic(c, name); check_error(); init(r); } tactic(context & c, Z3_tactic s):object(c) { init(s); } tactic(tactic const & s):object(s) { init(s.m_tactic); } - ~tactic() { Z3_tactic_dec_ref(ctx(), m_tactic); } + ~tactic() override { Z3_tactic_dec_ref(ctx(), m_tactic); } operator Z3_tactic() const { return m_tactic; } tactic & operator=(tactic const & s) { Z3_tactic_inc_ref(s.ctx(), s.m_tactic); @@ -3137,7 +3137,7 @@ namespace z3 { simplifier(context & c, char const * name):object(c) { Z3_simplifier r = Z3_mk_simplifier(c, name); check_error(); init(r); } simplifier(context & c, Z3_simplifier s):object(c) { init(s); } simplifier(simplifier const & s):object(s) { init(s.m_simplifier); } - ~simplifier() { Z3_simplifier_dec_ref(ctx(), m_simplifier); } + ~simplifier() override { Z3_simplifier_dec_ref(ctx(), m_simplifier); } operator Z3_simplifier() const { return m_simplifier; } simplifier & operator=(simplifier const & s) { Z3_simplifier_inc_ref(s.ctx(), s.m_simplifier); @@ -3179,7 +3179,7 @@ namespace z3 { probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); } probe(context & c, Z3_probe s):object(c) { init(s); } probe(probe const & s):object(s) { init(s.m_probe); } - ~probe() { Z3_probe_dec_ref(ctx(), m_probe); } + ~probe() public override { Z3_probe_dec_ref(ctx(), m_probe); } operator Z3_probe() const { return m_probe; } probe & operator=(probe const & s) { Z3_probe_inc_ref(s.ctx(), s.m_probe); @@ -3273,7 +3273,7 @@ namespace z3 { object::operator=(o); return *this; } - ~optimize() { Z3_optimize_dec_ref(ctx(), m_opt); } + ~optimize() override { Z3_optimize_dec_ref(ctx(), m_opt); } operator Z3_optimize() const { return m_opt; } void add(expr const& e) { assert(e.is_bool()); @@ -3354,7 +3354,7 @@ namespace z3 { public: fixedpoint(context& c):object(c) { m_fp = Z3_mk_fixedpoint(c); Z3_fixedpoint_inc_ref(c, m_fp); } fixedpoint(fixedpoint const & o):object(o), m_fp(o.m_fp) { Z3_fixedpoint_inc_ref(ctx(), m_fp); } - ~fixedpoint() { Z3_fixedpoint_dec_ref(ctx(), m_fp); } + ~fixedpoint() override { Z3_fixedpoint_dec_ref(ctx(), m_fp); } fixedpoint & operator=(fixedpoint const & o) { Z3_fixedpoint_inc_ref(o.ctx(), o.m_fp); Z3_fixedpoint_dec_ref(ctx(), m_fp); From 2f022782270bf4426ddd1fe2f11dbfefd47df107 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 May 2024 16:35:25 -0700 Subject: [PATCH 43/49] add virtual destructor to z3::object class Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4025be4fd..81a67066e 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3179,7 +3179,7 @@ namespace z3 { probe(context & c, double val):object(c) { Z3_probe r = Z3_probe_const(c, val); check_error(); init(r); } probe(context & c, Z3_probe s):object(c) { init(s); } probe(probe const & s):object(s) { init(s.m_probe); } - ~probe() public override { Z3_probe_dec_ref(ctx(), m_probe); } + ~probe() override { Z3_probe_dec_ref(ctx(), m_probe); } operator Z3_probe() const { return m_probe; } probe & operator=(probe const & s) { Z3_probe_inc_ref(s.ctx(), s.m_probe); From 8f4ffc7caf19ba9c7b4c63935ef19cef215e847f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 May 2024 20:50:52 -0700 Subject: [PATCH 44/49] add logging for first conflict Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index d986f967a..eed908617 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1574,7 +1574,7 @@ namespace nlsat { } void gc() { - if (m_learned.size() <= 2*m_clauses.size()) + if (m_learned.size() <= 4*m_clauses.size()) return; reset_watches(); reinit_cache(); @@ -1595,7 +1595,7 @@ namespace nlsat { unsigned m_next_conflict = 100; void log() { - if (m_conflicts < m_next_conflict) + if (m_conflicts != 1 && m_conflicts < m_next_conflict) return; m_next_conflict += 100; IF_VERBOSE(2, verbose_stream() << "(nlsat :conflicts " << m_conflicts << " :decisions " << m_decisions << " :propagations " << m_propagations << " :clauses " << m_clauses.size() << " :learned " << m_learned.size() << ")\n"); @@ -1605,7 +1605,7 @@ namespace nlsat { lbool search_check() { lbool r = l_undef; m_conflicts = 0; - m_next_conflict = 100; + m_next_conflict = 0; while (true) { r = search(); if (r != l_true) break; @@ -3015,7 +3015,7 @@ namespace nlsat { if (apply_fm_equality(x, clauses, lo, hi)) return true; - return false; + // return false; if (!all_solved) return false; From f9176fb4b72156bb8ceca7ebe1b817d9e87baf85 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 May 2024 11:39:52 -0700 Subject: [PATCH 45/49] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index dfbaea599..e6db550c0 100644 --- a/README.md +++ b/README.md @@ -226,7 +226,7 @@ to Z3's C API. For more information, see [MachineArithmetic/README.md](https://g * Default input format is [SMTLIB2](http://smtlib.cs.uiowa.edu) * Other native foreign function interfaces: -* [C++ API](https://z3prover.github.io/api/html/group__cppapi.html) +* [C++ API](https://z3prover.github.io/api/html/namespacez3.html) * [.NET API](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html) * [Java API](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html) * [Python API](https://z3prover.github.io/api/html/namespacez3py.html) (also available in [pydoc format](https://z3prover.github.io/api/html/z3.html)) From fc6c4c98e26fc0bc1c5c50e1376ff9201f94b880 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 May 2024 14:52:49 -0700 Subject: [PATCH 46/49] initial warppers for seq-map/seq-fold Signed-off-by: Nikolaj Bjorner --- src/api/api_ast.cpp | 4 ++++ src/api/api_seq.cpp | 5 +++++ src/api/api_util.h | 17 +++++++++++++++++ src/api/python/z3/z3.py | 13 +++++++++++++ src/api/z3_api.h | 28 ++++++++++++++++++++++++++++ 5 files changed, 67 insertions(+) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 424b361f3..931167110 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1310,6 +1310,10 @@ extern "C" { case OP_SEQ_INDEX: return Z3_OP_SEQ_INDEX; case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE; case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE; + case OP_SEQ_MAP: return Z3_OP_SEQ_MAP; + case OP_SEQ_MAPI: return Z3_OP_SEQ_MAPI; + case OP_SEQ_FOLDL: return Z3_OP_SEQ_FOLDL; + case OP_SEQ_FOLDLI: return Z3_OP_SEQ_FOLDLI; case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE; case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT; diff --git a/src/api/api_seq.cpp b/src/api/api_seq.cpp index 6a9d0f81c..2b87ef290 100644 --- a/src/api/api_seq.cpp +++ b/src/api/api_seq.cpp @@ -348,5 +348,10 @@ extern "C" { MK_UNARY(Z3_mk_char_from_bv, mk_c(c)->get_char_fid(), OP_CHAR_FROM_BV, SKIP); MK_UNARY(Z3_mk_char_is_digit, mk_c(c)->get_char_fid(), OP_CHAR_IS_DIGIT, SKIP); + MK_BINARY(Z3_mk_seq_map, mk_c(c)->get_seq_fid(), OP_SEQ_MAP, SKIP); + MK_TERNARY(Z3_mk_seq_mapi, mk_c(c)->get_seq_fid(), OP_SEQ_MAPI, SKIP); + MK_TERNARY(Z3_mk_seq_foldl, mk_c(c)->get_seq_fid(), OP_SEQ_FOLDL, SKIP); + MK_FOURARY(Z3_mk_seq_foldli, mk_c(c)->get_seq_fid(), OP_SEQ_FOLDLI, SKIP); + }; diff --git a/src/api/api_util.h b/src/api/api_util.h index 174d75144..7b16229f4 100644 --- a/src/api/api_util.h +++ b/src/api/api_util.h @@ -160,6 +160,23 @@ Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2) { \ MK_TERNARY_BODY(NAME, FID, OP, EXTRA_CODE); \ } +#define MK_FOURARY_BODY(NAME, FID, OP, EXTRA_CODE) \ + Z3_TRY; \ + RESET_ERROR_CODE(); \ + EXTRA_CODE; \ + expr * args[4] = { to_expr(n1), to_expr(n2), to_expr(n3), to_expr(n4) }; \ + ast* a = mk_c(c)->m().mk_app(FID, OP, 0, 0, 4, args); \ + mk_c(c)->save_ast_trail(a); \ + check_sorts(c, a); \ + RETURN_Z3(of_ast(a)); \ + Z3_CATCH_RETURN(0); + +#define MK_FOURARY(NAME, FID, OP, EXTRA_CODE) \ + Z3_ast Z3_API NAME(Z3_context c, Z3_ast n1, Z3_ast n2, Z3_ast n3, Z3_ast n4) { \ + LOG_ ## NAME(c, n1, n2, n3, n4); \ + MK_FOURARY_BODY(NAME, FID, OP, EXTRA_CODE); \ +} + #define MK_NARY(NAME, FID, OP, EXTRA_CODE) \ Z3_ast Z3_API NAME(Z3_context c, unsigned num_args, Z3_ast const* args) { \ Z3_TRY; \ diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 9a3dadda2..44a4aba84 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -11210,6 +11210,19 @@ def Length(s): s = _coerce_seq(s) return ArithRef(Z3_mk_seq_length(s.ctx_ref(), s.as_ast()), s.ctx) +def SeqMap(f, s): + """Map function 'f' over sequence 's'""" + ctx = _get_ctx2(f, s) + s = _coerce_seq(s, ctx) + return _to_expr_ref(Z3_mk_seq_map(s.ctx_ref(), f.as_ast(), s.as_ast()), ctx) + +def SeqMapI(f, i, s): + """Map function 'f' over sequence 's' at index 'i'""" + ctx = _get_ctx(f, s) + s = _coerce_seq(s, ctx) + if not is_expr(i): + i = _py2expr(i) + return _to_expr_ref(Z3_mk_seq_mapi(s.ctx_ref(), f.as_ast(), i.as_ast(), s.as_ast()), ctx) def StrToInt(s): """Convert string expression to integer diff --git a/src/api/z3_api.h b/src/api/z3_api.h index cbf9803db..312acc268 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1193,6 +1193,10 @@ typedef enum { Z3_OP_SEQ_LAST_INDEX, Z3_OP_SEQ_TO_RE, Z3_OP_SEQ_IN_RE, + Z3_OP_SEQ_MAP, + Z3_OP_SEQ_MAPI, + Z3_OP_SEQ_FOLDL, + Z3_OP_SEQ_FOLDLI, // strings Z3_OP_STR_TO_INT, @@ -3798,6 +3802,30 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_seq_last_index(Z3_context c, Z3_ast s, Z3_ast substr); + /** + \brief Create a map of the function \c f over the sequence \c s. + def_API('Z3_mk_seq_map', AST ,(_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_map(Z3_context c, Z3_ast f, Z3_ast s); + + /** + \brief Create a map of the function \c f over the sequence \c s starting at index \c i. + def_API('Z3_mk_seq_mapi', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_mapi(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast s); + + /** + \brief Create a fold of the function \c f over the sequence \c s with accumulator a. + def_API('Z3_mk_seq_foldl', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_foldl(Z3_context c, Z3_ast f, Z3_ast a, Z3_ast s); + + /** + \brief Create a fold with index tracking of the function \c f over the sequence \c s with accumulator \c a starting at index \c i. + def_API('Z3_mk_seq_foldli', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_seq_foldli(Z3_context c, Z3_ast f, Z3_ast i, Z3_ast a, Z3_ast s); + /** \brief Convert string to integer. From c7529d0b25c7195d6786b1c36aef3d0611bd65fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 May 2024 14:56:18 -0700 Subject: [PATCH 47/49] expose fold as well Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 44a4aba84..c3f40a52b 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -11224,6 +11224,19 @@ def SeqMapI(f, i, s): i = _py2expr(i) return _to_expr_ref(Z3_mk_seq_mapi(s.ctx_ref(), f.as_ast(), i.as_ast(), s.as_ast()), ctx) +def SeqFoldLeft(f, a, s): + ctx = _get_ctx2(f, s) + s = _coerce_seq(s, ctx) + a = _py2expr(a) + return _to_expr_ref(Z3_mk_seq_foldl(s.ctx_ref(), f.as_ast(), a.as_ast(), s.as_ast()), ctx) + +def SeqFoldLeftI(f, i, a, s): + ctx = _get_ctx2(f, s) + s = _coerce_seq(s, ctx) + a = _py2expr(a) + i = _py2epxr(i) + return _to_expr_ref(Z3_mk_seq_foldli(s.ctx_ref(), f.as_ast(), i.as_ast(), a.as_ast(), s.as_ast()), ctx) + def StrToInt(s): """Convert string expression to integer >>> a = StrToInt("1") From b12074507859db333772d57671f3fb84a05460d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 May 2024 20:20:05 -0700 Subject: [PATCH 48/49] add C++ bindings for sequence operations Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 81a67066e..81d5bcaa9 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2497,6 +2497,34 @@ namespace z3 { return expr(ctx, r); } + inline expr map(expr const& f, expr const& list) { + context& ctx = f.ctx(); + Z3_ast r = Z3_mk_seq_map(ctx, f, list); + ctx.check_error(); + return expr(ctx, r); + } + + inline expr mapi(expr const& f, expr const& i, expr const& list) { + context& ctx = f.ctx(); + Z3_ast r = Z3_mk_seq_mapi(ctx, f, i, list); + ctx.check_error(); + return expr(ctx, r); + } + + inline expr foldl(expr const& f, expr const& a, expr const& list) { + context& ctx = f.ctx(); + Z3_ast r = Z3_mk_seq_foldl(ctx, f, a, list); + ctx.check_error(); + return expr(ctx, r); + } + + inline expr foldli(expr const& f, expr const& i, expr const& a, expr const& list) { + context& ctx = f.ctx(); + Z3_ast r = Z3_mk_seq_foldli(ctx, f, i, a, list); + ctx.check_error(); + return expr(ctx, r); + } + inline expr mk_or(expr_vector const& args) { array _args(args); Z3_ast r = Z3_mk_or(args.ctx(), _args.size(), _args.ptr()); From efc893263a4fe107b3c62cea02aaa355b2f34ec8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 May 2024 20:54:39 -0700 Subject: [PATCH 49/49] add abs function to API Signed-off-by: Nikolaj Bjorner --- src/api/api_arith.cpp | 1 + src/api/api_ast.cpp | 1 + src/api/z3_api.h | 8 ++++++++ 3 files changed, 10 insertions(+) diff --git a/src/api/api_arith.cpp b/src/api/api_arith.cpp index 7cfd5a345..bba2cf0c3 100644 --- a/src/api/api_arith.cpp +++ b/src/api/api_arith.cpp @@ -123,6 +123,7 @@ extern "C" { Z3_CATCH_RETURN(nullptr); } + MK_UNARY(Z3_mk_abs, mk_c(c)->get_arith_fid(), OP_ABS, SKIP); MK_UNARY(Z3_mk_int2real, mk_c(c)->get_arith_fid(), OP_TO_REAL, SKIP); MK_UNARY(Z3_mk_real2int, mk_c(c)->get_arith_fid(), OP_TO_INT, SKIP); MK_UNARY(Z3_mk_is_int, mk_c(c)->get_arith_fid(), OP_IS_INT, SKIP); diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 931167110..ecbf86b37 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1152,6 +1152,7 @@ extern "C" { case OP_REM: return Z3_OP_REM; case OP_MOD: return Z3_OP_MOD; case OP_POWER: return Z3_OP_POWER; + case OP_ABS: return Z3_OP_ABS; case OP_TO_REAL: return Z3_OP_TO_REAL; case OP_TO_INT: return Z3_OP_TO_INT; case OP_IS_INT: return Z3_OP_IS_INT; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 312acc268..fce5f15d1 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1023,6 +1023,7 @@ typedef enum { Z3_OP_TO_INT, Z3_OP_IS_INT, Z3_OP_POWER, + Z3_OP_ABS, // Arrays & Sets Z3_OP_STORE = 0x300, @@ -2548,6 +2549,13 @@ extern "C" { */ Z3_ast Z3_API Z3_mk_power(Z3_context c, Z3_ast arg1, Z3_ast arg2); + /** + \brief Take the absolute value of an integer + + def_API('Z3_mk_abs', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_abs(Z3_context c, Z3_ast arg); + /** \brief Create less than.