From a863a91b130bd0e2a7af2f4ce9f7943df71555a8 Mon Sep 17 00:00:00 2001 From: fleisherdev <55119509+fleisherdev@users.noreply.github.com> Date: Thu, 7 Apr 2022 02:19:21 -0400 Subject: [PATCH 01/37] Allow nightly builds to complete even if package signing fails - NOT published to nuget.org (#5951) Co-authored-by: jofleish --- scripts/nightly.yaml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 374249432..e81135ab5 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -194,6 +194,7 @@ stages: patchVersion: $(Patch) arguments: 'pack $(Agent.TempDirectory)\package\out\Microsoft.Z3.sym.nuspec -Version $(NightlyVersion) -OutputDirectory $(Build.ArtifactStagingDirectory) -Verbosity detailed -Symbols -SymbolPackageFormat snupkg -BasePath $(Agent.TempDirectory)\package\out' - task: EsrpCodeSigning@1 + continueOnError: true displayName: 'Sign Package' inputs: ConnectedServiceName: 'z3-esrp-signing-2' @@ -221,6 +222,7 @@ stages: MaxConcurrency: '50' MaxRetryAttempts: '5' - task: EsrpCodeSigning@1 + continueOnError: true displayName: 'Sign Symbol Package' inputs: ConnectedServiceName: 'z3-esrp-signing-2' @@ -297,6 +299,7 @@ stages: patchVersion: $(Patch) arguments: 'pack $(Agent.TempDirectory)\package\out\Microsoft.Z3.x86.sym.nuspec -Version $(NightlyVersion) -OutputDirectory $(Build.ArtifactStagingDirectory) -Verbosity detailed -Symbols -SymbolPackageFormat snupkg -BasePath $(Agent.TempDirectory)\package\out' - task: EsrpCodeSigning@1 + continueOnError: true displayName: 'Sign Package' inputs: ConnectedServiceName: 'z3-esrp-signing-2' @@ -324,6 +327,7 @@ stages: MaxConcurrency: '50' MaxRetryAttempts: '5' - task: EsrpCodeSigning@1 + continueOnError: true displayName: 'Sign Symbol Package' inputs: ConnectedServiceName: 'z3-esrp-signing-2' From 19531654227522416cd37d48e7407d1ae055ec4b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Apr 2022 08:35:45 +0200 Subject: [PATCH 02/37] set ARM64 if detected under OSX --- CMakeLists.txt | 4 +++- cmake/target_arch_detect.cpp | 2 ++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a9e121d02..5fef02be9 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -198,7 +198,9 @@ elseif (CMAKE_SYSTEM_NAME MATCHES "GNU") message(STATUS "Platform: GNU/Hurd") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_HURD_") elseif (CMAKE_SYSTEM_NAME STREQUAL "Darwin") - # Does macOS really not need any special flags? + if (TARGET_ARCHITECTURE STREQUAL "arm64") + set(CMAKE_OSX_ARCHITECTURES "arm64") + endif() message(STATUS "Platform: Darwin") elseif (CMAKE_SYSTEM_NAME MATCHES "FreeBSD") message(STATUS "Platform: FreeBSD") diff --git a/cmake/target_arch_detect.cpp b/cmake/target_arch_detect.cpp index 0a2d0f3e6..379b5817e 100644 --- a/cmake/target_arch_detect.cpp +++ b/cmake/target_arch_detect.cpp @@ -5,6 +5,8 @@ #error CMAKE_TARGET_ARCH_i686 #elif defined(__x86_64__) || defined(_M_X64) #error CMAKE_TARGET_ARCH_x86_64 +#elif defined(__ARM_ARCH_ISA_A64) +#error CMAKE_TARGET_ARCH_arm64 #elif defined(__ARM_ARCH) #error CMAKE_TARGET_ARCH_arm #else From 8c2909f52bda61ce2422f6fb6484fa69a651e59d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Apr 2022 13:36:23 +0200 Subject: [PATCH 03/37] working on python make for arm Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 4 ++++ src/ast/pb_decl_plugin.cpp | 10 +++++----- src/ast/special_relations_decl_plugin.cpp | 10 +++++----- src/util/params.cpp | 17 +++++++++-------- 4 files changed, 23 insertions(+), 18 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 1fca64f29..78c983ec4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -69,6 +69,7 @@ IS_WINDOWS=False IS_LINUX=False IS_HURD=False IS_OSX=False +IS_OS_ARM64=False IS_FREEBSD=False IS_NETBSD=False IS_OPENBSD=False @@ -598,6 +599,9 @@ if os.name == 'nt': elif os.name == 'posix': if os.uname()[0] == 'Darwin': IS_OSX=True + print("setting Darwin", os.uname()[4]) + if os.uname()[4] == 'arm64': + IS_OS_ARM64 = True elif os.uname()[0] == 'Linux': IS_LINUX=True elif os.uname()[0] == 'GNU': diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp index d4797b507..10e6c694c 100644 --- a/src/ast/pb_decl_plugin.cpp +++ b/src/ast/pb_decl_plugin.cpp @@ -90,11 +90,11 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p void pb_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { if (logic == symbol::null || logic == "QF_FD" || logic == "ALL" || logic == "HORN") { - op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K)); - op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K)); - op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE)); - op_names.push_back(builtin_name(m_pbge_sym.bare_str(), OP_PB_GE)); - op_names.push_back(builtin_name(m_pbeq_sym.bare_str(), OP_PB_EQ)); + op_names.push_back(builtin_name(m_at_most_sym.str(), OP_AT_MOST_K)); + op_names.push_back(builtin_name(m_at_least_sym.str(), OP_AT_LEAST_K)); + op_names.push_back(builtin_name(m_pble_sym.str(), OP_PB_LE)); + op_names.push_back(builtin_name(m_pbge_sym.str(), OP_PB_GE)); + op_names.push_back(builtin_name(m_pbeq_sym.str(), OP_PB_EQ)); } } diff --git a/src/ast/special_relations_decl_plugin.cpp b/src/ast/special_relations_decl_plugin.cpp index 5dc5f32fe..7ed5e8346 100644 --- a/src/ast/special_relations_decl_plugin.cpp +++ b/src/ast/special_relations_decl_plugin.cpp @@ -61,11 +61,11 @@ func_decl * special_relations_decl_plugin::mk_func_decl( void special_relations_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { if (logic == symbol::null) { - op_names.push_back(builtin_name(m_po.bare_str(), OP_SPECIAL_RELATION_PO)); - op_names.push_back(builtin_name(m_lo.bare_str(), OP_SPECIAL_RELATION_LO)); - op_names.push_back(builtin_name(m_plo.bare_str(), OP_SPECIAL_RELATION_PLO)); - op_names.push_back(builtin_name(m_to.bare_str(), OP_SPECIAL_RELATION_TO)); - op_names.push_back(builtin_name(m_tc.bare_str(), OP_SPECIAL_RELATION_TC)); + op_names.push_back(builtin_name(m_po.str(), OP_SPECIAL_RELATION_PO)); + op_names.push_back(builtin_name(m_lo.str(), OP_SPECIAL_RELATION_LO)); + op_names.push_back(builtin_name(m_plo.str(), OP_SPECIAL_RELATION_PLO)); + op_names.push_back(builtin_name(m_to.str(), OP_SPECIAL_RELATION_TO)); + op_names.push_back(builtin_name(m_tc.str(), OP_SPECIAL_RELATION_TC)); } } diff --git a/src/util/params.cpp b/src/util/params.cpp index aefe4e074..1745e56fd 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -24,15 +24,14 @@ Notes: params_ref params_ref::g_empty_params_ref; -std::string norm_param_name(char const * n) { - if (n == nullptr) - return "_"; +std::string norm_param_name(char const* n) { if (*n == ':') n++; std::string r = n; unsigned sz = static_cast(r.size()); if (sz == 0) return "_"; + for (unsigned i = 0; i < sz; i++) { char curr = r[i]; if ('A' <= curr && curr <= 'Z') @@ -44,6 +43,8 @@ std::string norm_param_name(char const * n) { } std::string norm_param_name(symbol const & n) { + if (n.is_null()) + return "_"; return norm_param_name(n.bare_str()); } @@ -156,8 +157,8 @@ struct param_descrs::imp { return m_names[idx]; } - struct lt { - bool operator()(symbol const & s1, symbol const & s2) const { return strcmp(s1.bare_str(), s2.bare_str()) < 0; } + struct symlt { + bool operator()(symbol const & s1, symbol const & s2) const { return ::lt(s1, s2); } }; void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const { @@ -165,13 +166,13 @@ struct param_descrs::imp { for (auto const& kv : m_info) { names.push_back(kv.m_key); } - std::sort(names.begin(), names.end(), lt()); + std::sort(names.begin(), names.end(), symlt()); for (symbol const& name : names) { for (unsigned i = 0; i < indent; i++) out << " "; if (smt2_style) out << ':'; - char const * s = name.bare_str(); - unsigned n = static_cast(strlen(s)); + std::string s = name.str(); + unsigned n = static_cast(s.length()); for (unsigned i = 0; i < n; i++) { if (smt2_style && s[i] == '_') out << '-'; From c47bd1d01f8abdd4937f761e0d32e46c61d46d7f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Apr 2022 13:43:35 +0200 Subject: [PATCH 04/37] add arm64 auto-detect Signed-off-by: Nikolaj Bjorner --- scripts/mk_util.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 78c983ec4..e25d90433 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -599,7 +599,6 @@ if os.name == 'nt': elif os.name == 'posix': if os.uname()[0] == 'Darwin': IS_OSX=True - print("setting Darwin", os.uname()[4]) if os.uname()[4] == 'arm64': IS_OS_ARM64 = True elif os.uname()[0] == 'Linux': @@ -2640,6 +2639,10 @@ def mk_config(): LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS if sysname == 'Linux' and machine.startswith('armv7') or machine.startswith('armv8'): CXXFLAGS = '%s -fpic' % CXXFLAGS + if IS_OSX and IS_OS_ARM64: + CXXFLAGS = '%s -arch arm64' % CXXFLAGS + LDFLAGS = '%s -arch arm64' % LDFLAGS + SLIBEXTRAFLAGS = '%s -arch arm64' % SLIBEXTRAFLAGS config.write('PREFIX=%s\n' % PREFIX) config.write('CC=%s\n' % CC) From 2e91d6688883552f635c53f0d30469ec65b8f00c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 06:28:36 +0200 Subject: [PATCH 05/37] Update mk_util.py use more meaningful name --- scripts/mk_util.py | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index e25d90433..6575f0dbf 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -69,7 +69,7 @@ IS_WINDOWS=False IS_LINUX=False IS_HURD=False IS_OSX=False -IS_OS_ARM64=False +IS_ARCH_ARM64=False IS_FREEBSD=False IS_NETBSD=False IS_OPENBSD=False @@ -599,8 +599,6 @@ if os.name == 'nt': elif os.name == 'posix': if os.uname()[0] == 'Darwin': IS_OSX=True - if os.uname()[4] == 'arm64': - IS_OS_ARM64 = True elif os.uname()[0] == 'Linux': IS_LINUX=True elif os.uname()[0] == 'GNU': @@ -624,7 +622,10 @@ elif os.name == 'posix': else: LINUX_X64=False +if os.uname()[4] == 'arm64': + IS_ARCH_ARM64 = True + def display_help(exit_code): print("mk_make.py: Z3 Makefile generator\n") print("This script generates the Makefile for the Z3 theorem prover.") @@ -2639,7 +2640,7 @@ def mk_config(): LDFLAGS = '%s -static-libgcc -static-libstdc++' % LDFLAGS if sysname == 'Linux' and machine.startswith('armv7') or machine.startswith('armv8'): CXXFLAGS = '%s -fpic' % CXXFLAGS - if IS_OSX and IS_OS_ARM64: + if IS_OSX and IS_ARCH_ARM64: CXXFLAGS = '%s -arch arm64' % CXXFLAGS LDFLAGS = '%s -arch arm64' % LDFLAGS SLIBEXTRAFLAGS = '%s -arch arm64' % SLIBEXTRAFLAGS From 83d2aa85ec7276a53b8978756bc94e7214b5097d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 06:35:25 +0200 Subject: [PATCH 06/37] add arm64 build path --- scripts/mk_unix_dist.py | 6 ++++++ scripts/nightly.yaml | 18 ++++++++++++++++-- 2 files changed, 22 insertions(+), 2 deletions(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 28d68a01b..f5cbf6504 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -72,6 +72,7 @@ def parse_options(): 'nojava', 'nodotnet', 'dotnet-key=', + 'arch=', 'githash', 'nopython' ]) @@ -96,6 +97,11 @@ def parse_options(): JAVA_ENABLED = False elif opt == '--githash': GIT_HASH = True + elif opt == '--arch': + if arg == "arm64": + mk_util.IS_ARCH_ARM64 = True + else: + raise MKException(f"Invalid architecture directive '{arg}'. Legal directives: arm64") else: raise MKException("Invalid command line option '%s'" % opt) set_build_dir(path) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index e81135ab5..4296cab08 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -4,7 +4,6 @@ variables: Minor: '8' Patch: '16' NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName) - MacFlags: 'CXXFLAGS="-arch x86_64" LINK_EXTRA_FLAGS="-arch x86_64" SLINK_EXTRA_FLAGS="-arch x86_64"' stages: - stage: Build @@ -15,7 +14,7 @@ stages: pool: vmImage: "macOS-latest" steps: - - script: $(MacFlags) python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk + - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk - 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)/. @@ -25,6 +24,21 @@ stages: targetPath: $(Build.ArtifactStagingDirectory) + - job: MacArm64 + displayName: "Mac ARM64 Build" + pool: + vmImage: "macOS-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)/. + - task: PublishPipelineArtifact@1 + inputs: + artifactName: 'MacArm64' + targetPath: $(Build.ArtifactStagingDirectory) + + - job: Ubuntu displayName: "Ubuntu build" pool: From babac78c999437ce7fe5c5c9e9e3eab45ded95b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 06:59:07 +0200 Subject: [PATCH 07/37] syntax error? --- scripts/mk_unix_dist.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index f5cbf6504..39f48f448 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -101,7 +101,7 @@ def parse_options(): if arg == "arm64": mk_util.IS_ARCH_ARM64 = True else: - raise MKException(f"Invalid architecture directive '{arg}'. Legal directives: arm64") + raise MKException("Invalid architecture directive '%s'. Legal directives: arm64" % arg) else: raise MKException("Invalid command line option '%s'" % opt) set_build_dir(path) From 1346a168a1346405a313c2a9eceb2560576f8e02 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 07:00:53 +0200 Subject: [PATCH 08/37] #5952 --- src/cmd_context/cmd_context.cpp | 1 + src/cmd_context/cmd_context.h | 1 + src/cmd_context/pdecl.cpp | 59 +++++++++++++++++++++++---------- src/cmd_context/pdecl.h | 17 ++++++---- 4 files changed, 54 insertions(+), 24 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 89efc439f..580cc2de4 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1636,6 +1636,7 @@ void cmd_context::pop(unsigned n) { restore_aux_pdecls(s.m_aux_pdecls_lim); restore_assertions(s.m_assertions_lim); restore_psort_inst(s.m_psort_inst_stack_lim); + m_dt_eh.get()->reset(); m_mcs.shrink(m_mcs.size() - n); m_scopes.shrink(new_lvl); if (!m_global_decls) diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 4f9d80a8d..60a6e930b 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -267,6 +267,7 @@ protected: cmd_context & m_owner; datatype_util m_dt_util; public: + void reset() { m_dt_util.reset(); } dt_eh(cmd_context & owner); ~dt_eh() override; void operator()(sort * dt, pdecl* pd) override; diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 7a93382e9..2bf21de3a 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -156,8 +156,8 @@ public: return false; return m_sort == static_cast(other)->m_sort; } - void display(std::ostream & out) const override { - out << m_sort->get_name(); + std::ostream& display(std::ostream & out) const override { + return out << m_sort->get_name(); } }; @@ -180,8 +180,8 @@ public: get_num_params() == other->get_num_params() && m_idx == static_cast(other)->m_idx; } - void display(std::ostream & out) const override { - out << "s_" << m_idx; + std::ostream& display(std::ostream & out) const override { + return out << "s_" << m_idx; } unsigned idx() const { return m_idx; } }; @@ -254,7 +254,7 @@ public: } return true; } - void display(std::ostream & out) const override { + std::ostream& display(std::ostream & out) const override { if (m_args.empty()) { out << m_decl->get_name(); } @@ -267,6 +267,7 @@ public: } out << ")"; } + return out; } }; @@ -342,12 +343,12 @@ void display_sort_args(std::ostream & out, unsigned num_params) { out << ") "; } -void psort_user_decl::display(std::ostream & out) const { +std::ostream& psort_user_decl::display(std::ostream & out) const { out << "(declare-sort " << m_name; display_sort_args(out, m_num_params); if (m_def) m_def->display(out); - out << ")"; + return out << ")"; } // ------------------- @@ -364,8 +365,8 @@ sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * return m.instantiate_datatype(this, m_name, n, s); } -void psort_dt_decl::display(std::ostream & out) const { - out << "(datatype-sort " << m_name << ")"; +std::ostream& psort_dt_decl::display(std::ostream & out) const { + return out << "(datatype-sort " << m_name << ")"; } // ------------------- @@ -410,8 +411,8 @@ sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, unsigned c } } -void psort_builtin_decl::display(std::ostream & out) const { - out << "(declare-builtin-sort " << m_name << ")"; +std::ostream& psort_builtin_decl::display(std::ostream & out) const { + return out << "(declare-builtin-sort " << m_name << ")"; } void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) const { @@ -615,7 +616,7 @@ sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * } -void pdatatype_decl::display(std::ostream & out) const { +std::ostream& pdatatype_decl::display(std::ostream & out) const { out << "(declare-datatype " << m_name; display_sort_args(out, m_num_params); bool first = true; @@ -631,7 +632,7 @@ void pdatatype_decl::display(std::ostream & out) const { } first = false; } - out << ")"; + return out << ")"; } bool pdatatype_decl::commit(pdecl_manager& m) { @@ -645,9 +646,11 @@ bool pdatatype_decl::commit(pdecl_manager& m) { datatype_decl * d_ptr = dts.m_buffer[0]; sort_ref_vector sorts(m.m()); bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, ps.data(), sorts); + m.notify_mk_datatype(m_name); if (is_ok && m_num_params == 0) { m.notify_new_dt(sorts.get(0), this); } + return is_ok; } @@ -722,6 +725,7 @@ void pdecl_manager::notify_datatype(sort *r, psort_decl* p, unsigned n, sort* co void pdecl_manager::push() { m_notified_lim.push_back(m_notified_trail.size()); + m_datatypes_lim.push_back(m_datatypes_trail.size()); } void pdecl_manager::pop(unsigned n) { @@ -732,6 +736,16 @@ void pdecl_manager::pop(unsigned n) { } m_notified_trail.shrink(new_sz); m_notified_lim.shrink(m_notified_lim.size() - n); + + new_sz = m_datatypes_lim[m_datatypes_lim.size() - n]; + if (new_sz != m_datatypes_trail.size()) { + datatype_util util(m()); + for (unsigned i = m_datatypes_trail.size(); i-- > new_sz; ) + util.plugin().remove(m_datatypes_trail[i]); + } + m_datatypes_trail.shrink(new_sz); + m_datatypes_lim.shrink(m_datatypes_lim.size() - n); + } bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) { @@ -751,16 +765,24 @@ bool pdatatypes_decl::commit(pdecl_manager& m) { sort_ref_vector sorts(m.m()); bool is_ok = m.get_dt_plugin()->mk_datatypes(m_datatypes.size(), dts.m_buffer.data(), 0, nullptr, sorts); if (is_ok) { + for (pdatatype_decl* d : m_datatypes) { + m.notify_mk_datatype(d->get_name()); + } for (unsigned i = 0; i < m_datatypes.size(); ++i) { pdatatype_decl* d = m_datatypes[i]; - if (d->get_num_params() == 0) { + if (d->get_num_params() == 0) m.notify_new_dt(sorts.get(i), this); - } } } + return is_ok; } +void pdecl_manager::notify_mk_datatype(symbol const& name) { + m_datatypes_trail.push_back(name); +} + + struct pdecl_manager::sort_info { psort_decl * m_decl; @@ -985,16 +1007,19 @@ void pdecl_manager::del_decl_core(pdecl * p) { } void pdecl_manager::del_decl(pdecl * p) { - TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";); + TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";); if (p->is_psort()) { psort * _p = static_cast(p); if (_p->is_sort_wrapper()) { - m_sort2psort.erase(static_cast(_p)->get_sort()); + sort* s = static_cast(_p)->get_sort(); + m_sort2psort.erase(s); } else { m_table.erase(_p); } + } + del_decl_core(p); } diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index 3a1db06c1..4f9c56825 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -45,7 +45,7 @@ public: unsigned get_id() const { return m_id; } unsigned get_ref_count() const { return m_ref_count; } unsigned hash() const { return m_id; } - virtual void display(std::ostream & out) const {} + virtual std::ostream& display(std::ostream & out) const { return out;} virtual void reset_cache(pdecl_manager& m) {} }; @@ -123,7 +123,7 @@ protected: ~psort_user_decl() override {} public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; - void display(std::ostream & out) const override; + std::ostream& display(std::ostream & out) const override; }; class psort_builtin_decl : public psort_decl { @@ -137,7 +137,7 @@ protected: public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) override; - void display(std::ostream & out) const override; + std::ostream& display(std::ostream & out) const override; }; class psort_dt_decl : public psort_decl { @@ -148,7 +148,7 @@ protected: ~psort_dt_decl() override {} public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; - void display(std::ostream & out) const override; + std::ostream& display(std::ostream & out) const override; }; @@ -198,7 +198,7 @@ class paccessor_decl : public pdecl { ptype const & get_type() const { return m_type; } ~paccessor_decl() override {} public: - void display(std::ostream & out) const override { pdecl::display(out); } + std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; } void display(std::ostream & out, pdatatype_decl const * const * dts) const; }; @@ -219,7 +219,7 @@ class pconstructor_decl : public pdecl { constructor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s); ~pconstructor_decl() override {} public: - void display(std::ostream & out) const override { pdecl::display(out); } + std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; } void display(std::ostream & out, pdatatype_decl const * const * dts) const; }; @@ -237,7 +237,7 @@ class pdatatype_decl : public psort_decl { ~pdatatype_decl() override {} public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; - void display(std::ostream & out) const override; + std::ostream& display(std::ostream & out) const override; bool has_missing_refs(symbol & missing) const; bool has_duplicate_accessors(symbol & repeated) const; bool commit(pdecl_manager& m); @@ -289,6 +289,8 @@ class pdecl_manager { obj_hashtable m_notified; ptr_vector m_notified_trail; unsigned_vector m_notified_lim; + svector m_datatypes_trail; + unsigned_vector m_datatypes_lim; void init_list(); void del_decl_core(pdecl * p); @@ -319,6 +321,7 @@ public: sort * instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s); sort * instantiate(psort * s, unsigned num, sort * const * args); void notify_datatype(sort *r, psort_decl* p, unsigned n, sort* const* s); + void notify_mk_datatype(symbol const& name); void push(); void pop(unsigned n); From 79553261d189b0583f68bbbc48fb9fc81f45128f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 07:02:32 +0200 Subject: [PATCH 09/37] no uname on nt --- scripts/mk_util.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 6575f0dbf..534910a69 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -621,8 +621,9 @@ elif os.name == 'posix': LINUX_X64=True else: LINUX_X64=False + -if os.uname()[4] == 'arm64': +if os.name == 'posix' and os.uname()[4] == 'arm64': IS_ARCH_ARM64 = True From cb6aba2315e71c0be80451456a75962512fbda92 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 14:07:56 +0200 Subject: [PATCH 10/37] more arm --- scripts/mk_unix_dist.py | 1 + scripts/mk_util.py | 3 ++- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 39f48f448..e89ca410f 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -56,6 +56,7 @@ def display_help(): print(" -f, --force force script to regenerate Makefiles.") print(" --nodotnet do not include .NET bindings in the binary distribution files.") print(" --dotnet-key= sign the .NET assembly with the private key in .") + print(" --arch= set architecture (to arm64) to force arm64 build") print(" --nojava do not include Java bindings in the binary distribution files.") print(" --nopython do not include Python bindings in the binary distribution files.") print(" --githash include git hash in the Zip file.") diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 534910a69..4d7cedba8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2436,7 +2436,7 @@ def mk_config(): if ONLY_MAKEFILES: return config = open(os.path.join(BUILD_DIR, 'config.mk'), 'w') - global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED + global CXX, CC, GMP, GUARD_CF, STATIC_BIN, GIT_HASH, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG, FPMATH_FLAGS, LOG_SYNC, SINGLE_THREADED, IS_ARCH_ARM64 if IS_WINDOWS: CXXFLAGS = '/nologo /Zi /D WIN32 /D _WINDOWS /EHsc /GS /Gd /std:c++17' config.write( @@ -2642,6 +2642,7 @@ def mk_config(): if sysname == 'Linux' and machine.startswith('armv7') or machine.startswith('armv8'): CXXFLAGS = '%s -fpic' % CXXFLAGS if IS_OSX and IS_ARCH_ARM64: + print("Setting arm64") CXXFLAGS = '%s -arch arm64' % CXXFLAGS LDFLAGS = '%s -arch arm64' % LDFLAGS SLIBEXTRAFLAGS = '%s -arch arm64' % SLIBEXTRAFLAGS From 746a4161af454a89bc6d4308d73e47c1021815cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 14:24:21 +0200 Subject: [PATCH 11/37] more passing of parameters --- scripts/mk_unix_dist.py | 2 ++ scripts/mk_util.py | 7 +++++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index e89ca410f..9c2a15c67 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -126,6 +126,8 @@ def mk_build_dir(path): opts.append('--git-describe') if PYTHON_ENABLED: opts.append('--python') + if mk_util.IS_ARCH_ARM64: + opts.append('--arm64=true') if subprocess.call(opts) != 0: raise MKException("Failed to generate build directory at '%s'" % path) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 4d7cedba8..74e761877 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -649,6 +649,7 @@ def display_help(exit_code): print(" -x, --x64 create 64 binary when using Visual Studio.") else: print(" --x86 force 32-bit x86 build on x64 systems.") + print(" --arm64= forcearm64 bit build on/off (supported for Darwin).") print(" -m, --makefiles generate only makefiles.") if IS_WINDOWS: print(" -v, --vsproj generate Visual Studio Project Files.") @@ -691,11 +692,11 @@ def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED - global GUARD_CF, ALWAYS_DYNAMIC_BASE + global GUARD_CF, ALWAYS_DYNAMIC_BASE, IS_ARCH_ARM64 try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', - ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', + ['build=', 'debug', 'silent', 'x64', 'arm64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js', 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded']) except: @@ -718,6 +719,8 @@ def parse_options(): VS_X64 = True elif opt in ('--x86'): LINUX_X64=False + elif opt in ('--arm64'): + IS_ARCH_ARM64 = arg in ('true','on','True','TRUE') elif opt in ('-h', '--help'): display_help(0) elif opt in ('-m', '--makefiles'): From 9533dbaf5c956aee76211b9da5db6b2f49d2259c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 14:34:52 +0200 Subject: [PATCH 12/37] missing arg specifier --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 74e761877..338dd822f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -696,7 +696,7 @@ def parse_options(): try: options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:df:sxhmcvtnp:gj', - ['build=', 'debug', 'silent', 'x64', 'arm64', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', + ['build=', 'debug', 'silent', 'x64', 'arm64=', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js', 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded']) except: From 67434a309670297b435d230fb054e49f3c8e446d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 14:40:55 +0200 Subject: [PATCH 13/37] again --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 338dd822f..34ca9a38a 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -695,7 +695,7 @@ def parse_options(): global GUARD_CF, ALWAYS_DYNAMIC_BASE, IS_ARCH_ARM64 try: options, remainder = getopt.gnu_getopt(sys.argv[1:], - 'b:df:sxhmcvtnp:gj', + 'b:df:sxa:hmcvtnp:gj', ['build=', 'debug', 'silent', 'x64', 'arm64=', 'help', 'makefiles', 'showcpp', 'vsproj', 'guardcf', 'trace', 'dotnet', 'dotnet-key=', 'staticlib', 'prefix=', 'gmp', 'java', 'parallel=', 'gprof', 'js', 'githash=', 'git-describe', 'x86', 'ml', 'optimize', 'pypkgdir=', 'python', 'staticbin', 'log-sync', 'single-threaded']) From f3789e21a349626ae351abd4c1d38a24e57387a5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 14:42:18 +0200 Subject: [PATCH 14/37] id doesn't use mk_util --- src/api/python/CMakeLists.txt | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index e791a2f11..067a25e8c 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -42,8 +42,6 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3/z3core.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "${PROJECT_SOURCE_DIR}/scripts/update_api.py" ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} - # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency - "${PROJECT_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating z3core.py" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} ) From 3821eb4134c977a4a35f57d5384de843d4c2991e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 14:47:38 +0200 Subject: [PATCH 15/37] fpflags --- scripts/mk_util.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 34ca9a38a..761de8b26 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -279,10 +279,13 @@ def test_gmp(cc): def test_fpmath(cc): - global FPMATH_FLAGS + global FPMATH_FLAGS, IS_ARCH_ARM64, IS_OSX if FPMATH_ENABLED == "False": FPMATH_FLAGS="" return "Disabled" + if IS_ARCH_ARM64 and IS_OSX: + FPMATH_FLAGS = "" + return "Disabled-ARM64" if is_verbose(): print("Testing floating point support...") t = TempFile('tstsse.cpp') From 91ca02864cb8552c837a848e8e681373720f6e48 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 14:59:22 +0200 Subject: [PATCH 16/37] arm64 Signed-off-by: Nikolaj Bjorner --- scripts/mk_unix_dist.py | 4 +++- scripts/nightly.yaml | 10 ++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 9c2a15c67..97de725e9 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -181,7 +181,9 @@ def get_os_name(): def get_z3_name(): major, minor, build, revision = get_version() - if sys.maxsize >= 2**32: + if mk_util.IS_ARCH_ARM64: + platform = "arm64" + elif sys.maxsize >= 2**32: platform = "x64" else: platform = "x86" diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 4296cab08..1ba0ea5af 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -180,6 +180,11 @@ stages: inputs: artifact: 'Mac' path: $(Agent.TempDirectory)\package + - task: DownloadPipelineArtifact@2 + displayName: 'Download macOS Arm64 Build' + inputs: + artifact: 'MacArm64' + path: $(Agent.TempDirectory)\package - task: NuGetToolInstaller@0 inputs: versionSpec: 5.x @@ -435,6 +440,11 @@ stages: inputs: artifactName: 'Mac' targetPath: tmp + - task: DownloadPipelineArtifact@2 + displayName: "Download MacArm64" + inputs: + artifactName: 'MacArm64' + targetPath: tmp - task: DownloadPipelineArtifact@2 displayName: "Download Ubuntu" inputs: From fbd35fb58d333b28208eb9da696aa10824e99370 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 16:55:39 +0200 Subject: [PATCH 17/37] skip unit tests for arm --- scripts/nightly.yaml | 1 - 1 file changed, 1 deletion(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 1ba0ea5af..488e5aedf 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -31,7 +31,6 @@ stages: 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)/. - task: PublishPipelineArtifact@1 inputs: From d6d9b25c6854989afcb2b7a72f92759ec2cecde9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 8 Apr 2022 17:12:20 +0200 Subject: [PATCH 18/37] Allow adding constraints in the model_eh callback --- src/opt/opt_context.cpp | 23 +++++++++++++++++------ src/opt/opt_context.h | 1 + 2 files changed, 18 insertions(+), 6 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 3551686f7..02cd90113 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -185,17 +185,27 @@ namespace opt { } void context::set_hard_constraints(expr_ref_vector const& fmls) { - if (m_scoped_state.set(fmls)) { + if (m_calling_on_model) { + for (expr* f : fmls) + add_hard_constraint(f); + return; + } + if (m_scoped_state.set(fmls)) + clear_state(); + } + + void context::add_hard_constraint(expr* f) { + if (m_calling_on_model) + get_solver().assert_expr(f); + else { + m_scoped_state.add(f); clear_state(); } } - void context::add_hard_constraint(expr* f) { - m_scoped_state.add(f); - clear_state(); - } - void context::add_hard_constraint(expr* f, expr* t) { + if (m_calling_on_model) + throw default_exception("adding soft constraints is not supported during callbacks"); m_scoped_state.m_asms.push_back(t); m_scoped_state.add(m.mk_implies(t, f)); clear_state(); @@ -389,6 +399,7 @@ namespace opt { model_ref md = m->copy(); if (!m_model_fixed.contains(md.get())) fix_model(md); + flet _calling(m_calling_on_model, true); m_on_model_eh(m_on_model_ctx, md); m_model_fixed.pop_back(); } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index dd717c392..1e950174a 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -165,6 +165,7 @@ namespace opt { ast_manager& m; on_model_t m_on_model_ctx; std::function m_on_model_eh; + bool m_calling_on_model = false; arith_util m_arith; bv_util m_bv; expr_ref_vector m_hard_constraints; From c98eda03f7c834f771f7e5f1ddfc5517c1029dbd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Apr 2022 06:55:31 +0200 Subject: [PATCH 19/37] nightly osx arm64 wheel --- scripts/nightly.yaml | 10 ++++++++-- src/api/python/setup.py | 4 +++- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 488e5aedf..ad64d05b7 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -399,7 +399,12 @@ stages: inputs: artifactName: 'Mac' targetPath: $(Agent.TempDirectory) - - script: cd $(Agent.TempDirectory); mkdir osx-bin; cd osx-bin; unzip ../*osx*.zip + - task: DownloadPipelineArtifact@2 + inputs: + artifactName: 'MacArm64' + targetPath: $(Agent.TempDirectory) + - script: cd $(Agent.TempDirectory); mkdir osx-x64-bin; cd osx-x64-bin; unzip ../*osx*x64.zip + - script: cd $(Agent.TempDirectory); mkdir osx-arm64-bin; cd osx-arm64-bin; unzip ../*osx*arm64.zip - script: cd $(Agent.TempDirectory); mkdir linux-bin; cd linux-bin; unzip ../*glibc*.zip - script: cd $(Agent.TempDirectory); mkdir win32-bin; cd win32-bin; unzip ../*x86-win*.zip - script: cd $(Agent.TempDirectory); mkdir win64-bin; cd win64-bin; unzip ../*x64-win*.zip @@ -409,7 +414,8 @@ stages: - script: cd src/api/python; echo $(Agent.TempDirectory)/linux-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel - script: cd src/api/python; echo $(Agent.TempDirectory)/win32-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel - script: cd src/api/python; echo $(Agent.TempDirectory)/win64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel - - script: cd src/api/python; echo $(Agent.TempDirectory)/osx-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel + - script: cd src/api/python; echo $(Agent.TempDirectory)/osx-x64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel + - script: cd src/api/python; echo $(Agent.TempDirectory)/osx-arm64-bin/* | xargs printf 'PACKAGE_FROM_RELEASE=%s\n' | xargs -I '{}' env '{}' python3 setup.py bdist_wheel - task: PublishPipelineArtifact@0 inputs: artifactName: 'Python packages' diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 8c73c29e6..796f30e6b 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -279,8 +279,10 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv: osver = RELEASE_METADATA[3] if osver.count('.') > 1: osver = '.'.join(osver.split('.')[:2]) - if arch == 'x64': + if arch == 'x64': plat_name ='macosx_%s_x86_64' % osver.replace('.', '_') + elif arc == 'arm64': + plat_name ='macosx_%s_arm64' % osver.replace('.', '_') else: raise Exception(f"idk how os {distos} {osver} works. what goes here?") else: From fe834b9e4e5519891da0d053ea9caea4640aaaa5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Apr 2022 07:40:48 +0200 Subject: [PATCH 20/37] update regex --- scripts/nightly.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index ad64d05b7..0add769b9 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -403,8 +403,8 @@ stages: inputs: artifactName: 'MacArm64' targetPath: $(Agent.TempDirectory) - - script: cd $(Agent.TempDirectory); mkdir osx-x64-bin; cd osx-x64-bin; unzip ../*osx*x64.zip - - script: cd $(Agent.TempDirectory); mkdir osx-arm64-bin; cd osx-arm64-bin; unzip ../*osx*arm64.zip + - script: cd $(Agent.TempDirectory); mkdir osx-x64-bin; cd osx-x64-bin; unzip ../*x64-osx*.zip + - script: cd $(Agent.TempDirectory); mkdir osx-arm64-bin; cd osx-arm64-bin; unzip ../*arm64-osx*.zip - script: cd $(Agent.TempDirectory); mkdir linux-bin; cd linux-bin; unzip ../*glibc*.zip - script: cd $(Agent.TempDirectory); mkdir win32-bin; cd win32-bin; unzip ../*x86-win*.zip - script: cd $(Agent.TempDirectory); mkdir win64-bin; cd win64-bin; unzip ../*x64-win*.zip From 005b8e3cf85d00dd7360d901580aba9925725c56 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Apr 2022 08:28:22 +0200 Subject: [PATCH 21/37] arc -> arch --- src/api/python/setup.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 796f30e6b..1b455bb56 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -281,7 +281,7 @@ if 'bdist_wheel' in sys.argv and '--plat-name' not in sys.argv: osver = '.'.join(osver.split('.')[:2]) if arch == 'x64': plat_name ='macosx_%s_x86_64' % osver.replace('.', '_') - elif arc == 'arm64': + elif arch == 'arm64': plat_name ='macosx_%s_arm64' % osver.replace('.', '_') else: raise Exception(f"idk how os {distos} {osver} works. what goes here?") From 405a26c5856ba726c31582eaf51103d01f1b51a7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Apr 2022 09:55:02 +0200 Subject: [PATCH 22/37] allow adding constraints during on_model --- src/opt/maxres.cpp | 17 ++++++++--------- src/opt/maxsmt.cpp | 14 +++++++++++++- src/opt/maxsmt.h | 3 +++ src/opt/opt_context.cpp | 11 ++++++++++- src/sat/sat_solver.cpp | 2 ++ 5 files changed, 36 insertions(+), 11 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 27b3b7260..1b4348105 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -791,11 +791,10 @@ public: improve_model(mdl); mdl->set_model_completion(true); unsigned correction_set_size = 0; - for (expr* a : m_asms) { - if (mdl->is_false(a)) { + for (expr* a : m_asms) + if (mdl->is_false(a)) ++correction_set_size; - } - } + if (!m_csmodel.get() || correction_set_size < m_correction_set_size) { m_csmodel = mdl; m_correction_set_size = correction_set_size; @@ -810,22 +809,22 @@ public: return; } - if (!m_c.verify_model(m_index, mdl.get(), upper)) { + if (!m_c.verify_model(m_index, mdl.get(), upper)) return; - } + unsigned num_assertions = s().get_num_assertions(); m_model = mdl; m_c.model_updated(mdl.get()); TRACE("opt", tout << "updated upper: " << upper << "\n";); - for (soft& s : m_soft) { + for (soft& s : m_soft) s.set_value(m_model->is_true(s.s)); - } verify_assignment(); - m_upper = upper; + if (num_assertions == s().get_num_assertions()) + m_upper = upper; trace(); diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 6a8a2ee35..bf25f3f95 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -50,7 +50,13 @@ namespace opt { void maxsmt_solver_base::updt_params(params_ref& p) { m_params.copy(p); - } + } + + void maxsmt_solver_base::reset_upper() { + m_upper = m_lower; + for (soft& s : m_soft) + m_upper += s.weight; + } solver& maxsmt_solver_base::s() { return m_c.get_solver(); @@ -289,6 +295,12 @@ namespace opt { } } + void maxsmt::reset_upper() { + if (m_msolver) { + m_msolver->reset_upper(); + m_upper = m_msolver->get_upper(); + } + } void maxsmt::verify_assignment() { // TBD: have to use a different solver diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index ad355cc9e..5bf637dde 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -103,6 +103,8 @@ namespace opt { }; lbool find_mutexes(obj_map& new_soft); + + void reset_upper(); protected: @@ -153,6 +155,7 @@ namespace opt { void display_answer(std::ostream& out) const; void collect_statistics(statistics& st) const; void model_updated(model* mdl); + void reset_upper(); private: bool is_maxsat_problem(weights_t& ws) const; void verify_assignment(); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 02cd90113..8848b61c9 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -195,13 +195,22 @@ namespace opt { } void context::add_hard_constraint(expr* f) { - if (m_calling_on_model) + if (m_calling_on_model) { get_solver().assert_expr(f); + for (auto const& [k, v] : m_maxsmts) + v->reset_upper(); + for (unsigned i = 0; i < num_objectives(); ++i) { + auto const& o = m_scoped_state.m_objectives[i]; + if (o.m_type != O_MAXSMT) + m_optsmt.update_upper(o.m_index, inf_eps::infinity()); + } + } else { m_scoped_state.add(f); clear_state(); } } + void context::add_hard_constraint(expr* f, expr* t) { if (m_calling_on_model) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 5505cfa70..4a254ac06 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3818,6 +3818,8 @@ namespace sat { void solver::move_to_front(bool_var b) { if (b >= num_vars()) return; + if (m_case_split_queue.empty()) + return; bool_var next = m_case_split_queue.min_var(); auto next_act = m_activity[next]; set_activity(b, next_act + 1); From 011c1b2dd2bd394ac043668e289bfdabbe2b1f27 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Apr 2022 12:06:27 +0200 Subject: [PATCH 23/37] remove refs to bare_str --- src/api/api_ast.cpp | 2 +- src/api/api_log.cpp | 2 +- src/api/api_tactic.cpp | 6 +-- src/ast/ast_smt2_pp.cpp | 12 ++---- src/cmd_context/basic_cmds.cpp | 2 +- src/muz/fp/datalog_parser.cpp | 40 ++++++++++--------- src/muz/rel/dl_finite_product_relation.cpp | 2 +- src/muz/rel/dl_instruction.cpp | 20 +++++----- src/muz/rel/dl_table_relation.cpp | 2 +- src/muz/rel/rel_context.cpp | 2 +- src/tactic/portfolio/smt_strategic_solver.cpp | 5 +-- 11 files changed, 46 insertions(+), 49 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index d5de6b5fb..8144c2baf 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -355,7 +355,7 @@ extern "C" { return mk_c(c)->mk_external_string(buffer.str()); } else { - return mk_c(c)->mk_external_string(_s.bare_str()); + return mk_c(c)->mk_external_string(_s.str()); } Z3_CATCH_RETURN(""); } diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index c1864ae8c..ed5f68e8a 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -88,7 +88,7 @@ void Sy(Z3_symbol sym) { *g_z3_log << "# " << s.get_num(); } else { - *g_z3_log << "$ |" << ll_escaped{s.bare_str()} << '|'; + *g_z3_log << "$ |" << ll_escaped{s.str().c_str()} << '|'; } *g_z3_log << std::endl; } diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 45073cdb1..f67a373dd 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -331,8 +331,8 @@ extern "C" { if (idx >= mk_c(c)->num_tactics()) { SET_ERROR_CODE(Z3_IOB, nullptr); return ""; - } - return mk_c(c)->get_tactic(idx)->get_name().bare_str(); + } + return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str().c_str()); Z3_CATCH_RETURN(""); } @@ -352,7 +352,7 @@ extern "C" { SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } - return mk_c(c)->get_probe(idx)->get_name().bare_str(); + return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str().c_str()); Z3_CATCH_RETURN(""); } diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 9854195a4..59f9ecda6 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -47,18 +47,14 @@ format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len, bo len = static_cast(str.length()); return mk_string(m, str); } - else if (s.is_numerical()) { - std::string str = s.str(); - len = static_cast(str.length()); - return mk_string(m, str); - } - else if (!s.bare_str()) { + else if (s.is_null()) { len = 4; return mk_string(m, "null"); } else { - len = static_cast(strlen(s.bare_str())); - return mk_string(m, s.bare_str()); + std::string str = s.str(); + len = static_cast(str.length()); + return mk_string(m, str); } } diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index afe800af6..f3bd0ed57 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -58,7 +58,7 @@ public: cmd * c = ctx.find_cmd(s); if (c == nullptr) { std::string err_msg("unknown command '"); - err_msg = err_msg + s.bare_str() + "'"; + err_msg = err_msg + s.str() + "'"; throw cmd_exception(std::move(err_msg)); } m_cmds.push_back(s); diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index 899ec497c..030d88d71 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -777,6 +777,7 @@ protected: // Sym ::= String | NUM | Var // dtoken parse_infix(dtoken tok1, char const* td, app_ref& pred) { + std::string td1_(td); symbol td1(td); expr_ref v1(m), v2(m); sort* s = nullptr; @@ -793,12 +794,12 @@ protected: if (tok1 == TK_ID) { expr* _v1 = nullptr; - m_vars.find(td1.bare_str(), _v1); + m_vars.find(td1_, _v1); v1 = _v1; } if (tok3 == TK_ID) { expr* _v2 = nullptr; - m_vars.find(td2.bare_str(), _v2); + m_vars.find(td, _v2); v2 = _v2; } if (!v1 && !v2) { @@ -950,18 +951,19 @@ protected: break; } case TK_ID: { - symbol data (m_lexer->get_token_data()); - if (is_var(data.bare_str())) { + char const* d = m_lexer->get_token_data(); + symbol data (d); + if (is_var(d)) { unsigned idx = 0; expr* v = nullptr; - if (!m_vars.find(data.bare_str(), v)) { + if (!m_vars.find(d, v)) { idx = m_num_vars++; v = m.mk_var(idx, s); - m_vars.insert(data.bare_str(), v); + m_vars.insert(d, v); } else if (s != v->get_sort()) { throw default_exception(default_exception::fmt(), "sort: %s expected, but got: %s\n", - s->get_name().bare_str(), v->get_sort()->get_name().bare_str()); + s->get_name().str().c_str(), v->get_sort()->get_name().str().c_str()); } args.push_back(v); } @@ -1075,21 +1077,21 @@ protected: } sort * register_finite_sort(symbol name, uint64_t domain_size, context::sort_kind k) { - if(m_sort_dict.contains(name.bare_str())) { - throw default_exception(default_exception::fmt(), "sort %s already declared", name.bare_str()); + if(m_sort_dict.contains(name.str().c_str())) { + throw default_exception(default_exception::fmt(), "sort %s already declared", name.str().c_str()); } sort * s = m_decl_util.mk_sort(name, domain_size); m_context.register_finite_sort(s, k); - m_sort_dict.insert(name.bare_str(), s); + m_sort_dict.insert(name.str(), s); return s; } sort * register_int_sort(symbol name) { - if(m_sort_dict.contains(name.bare_str())) { - throw default_exception(default_exception::fmt(), "sort %s already declared", name.bare_str()); + if(m_sort_dict.contains(name.str().c_str())) { + throw default_exception(default_exception::fmt(), "sort %s already declared", name.str().c_str()); } sort * s = m_arith.mk_int(); - m_sort_dict.insert(name.bare_str(), s); + m_sort_dict.insert(name.str(), s); return s; } @@ -1105,8 +1107,8 @@ protected: app * res; if(m_arith.is_int(s)) { uint64_t val; - if (!string_to_uint64(name.bare_str(), val)) { - throw default_exception(default_exception::fmt(), "Invalid integer: \"%s\"", name.bare_str()); + if (!string_to_uint64(name.str().c_str(), val)) { + throw default_exception(default_exception::fmt(), "Invalid integer: \"%s\"", name.str().c_str()); } res = m_arith.mk_numeral(rational(val, rational::ui64()), s); } @@ -1288,7 +1290,7 @@ private: uint64_set & sort_content = *e->get_data().m_value; if(!sort_content.contains(num)) { warning_msg("symbol number %I64u on line %d in file %s does not belong to sort %s", - num, m_current_line, m_current_file.c_str(), s->get_name().bare_str()); + num, m_current_line, m_current_file.c_str(), s->get_name().str().c_str()); return false; } if(!m_use_map_names) { @@ -1366,7 +1368,7 @@ private: func_decl * pred = m_context.try_get_predicate_decl(predicate_name); if(!pred) { throw default_exception(default_exception::fmt(), "tuple file %s for undeclared predicate %s", - m_current_file.c_str(), predicate_name.bare_str()); + m_current_file.c_str(), predicate_name.str().c_str()); } unsigned pred_arity = pred->get_arity(); sort * const * arg_sorts = pred->get_domain(); @@ -1531,9 +1533,9 @@ private: if(m_use_map_names) { auto const & value = m_number_names.insert_if_not_there(num, el_name); - if (value!=el_name) { + if (value != el_name) { warning_msg("mismatch of number names on line %d in file %s. old: \"%s\" new: \"%s\"", - m_current_line, fname.c_str(), value.bare_str(), el_name.bare_str()); + m_current_line, fname.c_str(), value.str().c_str(), el_name.str().c_str()); } } } diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index 8a4b86e6d..07921a3be 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -64,7 +64,7 @@ namespace datalog { } symbol finite_product_relation_plugin::get_name(relation_plugin & inner_plugin) { - std::string str = std::string("fpr_")+inner_plugin.get_name().bare_str(); + std::string str = std::string("fpr_")+inner_plugin.get_name().str(); return symbol(str.c_str()); } diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index 0df03172f..63846e7d5 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -213,10 +213,10 @@ namespace datalog { return true; } void make_annotations(execution_context & ctx) override { - ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str()); + ctx.set_register_annotation(m_reg, m_pred->get_name().str().c_str()); } std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { - const char * rel_name = m_pred->get_name().bare_str(); + auto rel_name = m_pred->get_name(); if (m_store) { return out << "store " << m_reg << " into " << rel_name; } @@ -378,7 +378,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported join operation on relations of kinds %s and %s", - r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str()); + r1.get_plugin().get_name().str().c_str(), r2.get_plugin().get_name().str().c_str()); } store_fn(r1, r2, fn); } @@ -441,7 +441,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported filter_equal operation on a relation of kind %s", - r.get_plugin().get_name().bare_str()); + r.get_plugin().get_name().str().c_str()); } store_fn(r, fn); } @@ -490,7 +490,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported filter_identical operation on a relation of kind %s", - r.get_plugin().get_name().bare_str()); + r.get_plugin().get_name().str().c_str()); } store_fn(r, fn); } @@ -537,7 +537,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported filter_interpreted operation on a relation of kind %s", - r.get_plugin().get_name().bare_str()); + r.get_plugin().get_name().str().c_str()); } store_fn(r, fn); } @@ -594,7 +594,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported filter_interpreted_and_project operation on a relation of kind %s", - reg.get_plugin().get_name().bare_str()); + reg.get_plugin().get_name().str().c_str()); } store_fn(reg, fn); } @@ -837,7 +837,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported join-project operation on relations of kinds %s and %s", - r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str()); + r1.get_plugin().get_name().str().c_str(), r2.get_plugin().get_name().str().c_str()); } store_fn(r1, r2, fn); } @@ -910,7 +910,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported select_equal_and_project operation on a relation of kind %s", - r.get_plugin().get_name().bare_str()); + r.get_plugin().get_name().str().c_str()); } store_fn(r, fn); } @@ -1076,7 +1076,7 @@ namespace datalog { return true; } std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { - return out << "mark_saturated " << m_pred->get_name().bare_str(); + return out << "mark_saturated " << m_pred->get_name(); } void make_annotations(execution_context & ctx) override { } diff --git a/src/muz/rel/dl_table_relation.cpp b/src/muz/rel/dl_table_relation.cpp index de55998f8..8a69f8f85 100644 --- a/src/muz/rel/dl_table_relation.cpp +++ b/src/muz/rel/dl_table_relation.cpp @@ -33,7 +33,7 @@ namespace datalog { // ----------------------------------- symbol table_relation_plugin::create_plugin_name(const table_plugin &p) { - std::string name = std::string("tr_") + p.get_name().bare_str(); + std::string name = std::string("tr_") + p.get_name().str(); return symbol(name.c_str()); } diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 957c85adb..76411a290 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -157,7 +157,7 @@ namespace datalog { //IF_VERBOSE(3, m_context.display_smt2(0,0,verbose_stream());); if (m_context.print_aig().is_non_empty_string()) { - const char *filename = m_context.print_aig().bare_str(); + std::string filename = m_context.print_aig().str(); aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts); std::ofstream strm(filename, std::ios_base::binary); aig(strm); diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 52df38247..0c304aa3f 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -143,10 +143,9 @@ public: tactic_ref t; if (tp.default_tactic() != symbol::null && !tp.default_tactic().is_numerical() && - tp.default_tactic().bare_str() && - tp.default_tactic().bare_str()[0]) { + tp.default_tactic().str()[0]) { cmd_context ctx(false, &m, l); - std::istringstream is(tp.default_tactic().bare_str()); + std::istringstream is(tp.default_tactic().str()); char const* file_name = ""; sexpr_ref se = parse_sexpr(ctx, is, p, file_name); if (se) { From f55b23322860a8e186ae919daa4796ac4850a82e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Apr 2022 12:06:39 +0200 Subject: [PATCH 24/37] #5778 --- src/sat/smt/arith_solver.cpp | 9 +++++---- src/sat/smt/q_model_fixer.cpp | 6 ++++++ 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 5a102fa14..e02a42979 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -549,13 +549,14 @@ namespace arith { found_compatible = false; for (; it != end; ++it) { api_bound* a2 = *it; - if (a1 == a2) continue; - if (a2->get_bound_kind() != kind) continue; + if (a1 == a2) + continue; + if (a2->get_bound_kind() != kind) + continue; rational const& k2(a2->get_value()); found_compatible = true; - if (k1 < k2) { + if (k1 < k2) return it; - } } return end; } diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp index 456525c42..cdea60d23 100644 --- a/src/sat/smt/q_model_fixer.cpp +++ b/src/sat/smt/q_model_fixer.cpp @@ -184,6 +184,8 @@ namespace q { for (euf::enode* n : ctx.get_egraph().enodes_of(f)) { expr* t = n->get_arg(idx)->get_expr(); values.push_back(mdl(t)); + if (!m.is_value(values.back())) + return expr_ref(m.mk_var(idx, srt), m); md->v2t.insert(values.back(), t); md->t2v.insert(t, values.back()); } @@ -299,6 +301,10 @@ namespace q { auto term = [&](unsigned j) { return md->v2t[md->values[j]]; }; + + for (unsigned j = 0; j < sz; ++j) + std::cout << mk_pp(md->values[j], m) << "\n"; + expr* arg = t->get_arg(i); From 0b20a4ebf4b8e3e0188ccbb5dad9b51a88966f04 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com> Date: Sat, 9 Apr 2022 21:46:21 +0200 Subject: [PATCH 25/37] Added rewriting distinct with bitvectors to false if bit-size is too low (#5956) * Fixed problem with registering bitvector functions * Added rewriting distinct with bitvectors to false if bit-size is too low * Removed debug output * Incorporated Nikolaj's comments * Simplifications --- src/ast/rewriter/bv_rewriter.cpp | 15 +++++++++++++++ src/ast/rewriter/bv_rewriter.h | 3 ++- src/ast/rewriter/th_rewriter.cpp | 20 +++++++++++--------- 3 files changed, 28 insertions(+), 10 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 073885c21..1fdd7bd14 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2803,6 +2803,21 @@ br_status bv_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resu return BR_FAILED; } +br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) { + if (num_args <= 1) { + result = m().mk_true(); + return BR_DONE; + } + unsigned sz = get_bv_size(args[0]); + // check if num_args > 2^sz + if (sz >= 32) + return BR_FAILED; + if (num_args <= 1u << sz) + return BR_FAILED; + result = m().mk_false(); + return BR_DONE; +} + br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args, bool is_overflow, expr_ref & result) { SASSERT(num == 2); unsigned bv_sz; diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h index 7f0c67540..88d952c06 100644 --- a/src/ast/rewriter/bv_rewriter.h +++ b/src/ast/rewriter/bv_rewriter.h @@ -180,7 +180,8 @@ public: bool is_urem_any(expr * e, expr * & dividend, expr * & divisor); br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); - br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & resul); + br_status mk_ite_core(expr * c, expr * t, expr * e, expr_ref & result); + br_status mk_distinct(unsigned num_args, expr * const * args, expr_ref & result); bool hi_div0() const { return m_hi_div0; } diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 22d6a83b7..9cf9fc810 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -60,7 +60,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { expr_substitution * m_subst = nullptr; unsigned long long m_max_memory; // in bytes bool m_new_subst = false; - unsigned m_max_steps = UINT_MAX; + unsigned m_max_steps = UINT_MAX; bool m_pull_cheap_ite = true; bool m_flat = true; bool m_cache_all = false; @@ -180,7 +180,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { // theory dispatch for = SASSERT(num == 2); family_id s_fid = args[0]->get_sort()->get_family_id(); - if (s_fid == m_a_rw.get_fid()) + if (s_fid == m_a_rw.get_fid()) st = m_a_rw.mk_eq_core(args[0], args[1], result); else if (s_fid == m_bv_rw.get_fid()) st = m_bv_rw.mk_eq_core(args[0], args[1], result); @@ -193,10 +193,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { else if (s_fid == m_seq_rw.get_fid()) st = m_seq_rw.mk_eq_core(args[0], args[1], result); if (st != BR_FAILED) - return st; - } - if (k == OP_EQ) { - SASSERT(num == 2); + return st; st = apply_tamagotchi(args[0], args[1], result); if (st != BR_FAILED) return st; @@ -210,16 +207,21 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return st; } if ((k == OP_AND || k == OP_OR) && m_seq_rw.u().has_re()) { - st = m_seq_rw.mk_bool_app(f, num, args, result); + st = m_seq_rw.mk_bool_app(f, num, args, result); if (st != BR_FAILED) return st; } - if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) && + if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) && to_app(args[0])->get_family_id() == m_seq_rw.get_fid()) { st = m_seq_rw.mk_eq_core(args[0], args[1], result); if (st != BR_FAILED) return st; } + if (k == OP_DISTINCT && num > 0 && m_bv_rw.is_bv(args[0])) { + st = m_bv_rw.mk_distinct(num, args, result); + if (st != BR_FAILED) + return st; + } return m_b_rw.mk_app_core(f, num, args, result); } @@ -250,7 +252,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { if (fid == m_seq_rw.get_fid()) return m_seq_rw.mk_app_core(f, num, args, result); if (fid == m_char_rw.get_fid()) - return m_char_rw.mk_app_core(f, num, args, result); + return m_char_rw.mk_app_core(f, num, args, result); if (fid == m_rec_rw.get_fid()) return m_rec_rw.mk_app_core(f, num, args, result); return BR_FAILED; From 4f4e9a9963309518c7cdd92a01ae5429533d6369 Mon Sep 17 00:00:00 2001 From: Andreas Date: Mon, 11 Apr 2022 02:40:03 -0400 Subject: [PATCH 26/37] fix a tiny typo (#5960) A dot. --- doc/website.dox.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/website.dox.in b/doc/website.dox.in index 69395492e..f4caa1277 100644 --- a/doc/website.dox.in +++ b/doc/website.dox.in @@ -4,7 +4,7 @@ Z3 is a high-performance theorem prover being developed at Microsoft Research. - The Z3 website is at http://github.com/z3prover.. + The Z3 website is at http://github.com/z3prover. This website hosts the automatically generated documentation for the Z3 APIs. From f43d9d00d4ba7ee040d7e3736a848926a842c082 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Bour?= Date: Mon, 11 Apr 2022 13:38:20 +0200 Subject: [PATCH 27/37] Z3_add_rec_def body is not a macro (#5963) --- src/api/api_ast.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 8144c2baf..7ee95afc8 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -164,7 +164,7 @@ extern "C" { return; } recfun_replace replace(m); - p.set_definition(replace, pd, true, n, _vars.data(), abs_body); + p.set_definition(replace, pd, false, n, _vars.data(), abs_body); Z3_CATCH; } From b0d8b27f37cf184fe632ec84f19785dc20a9ff80 Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com> Date: Mon, 11 Apr 2022 16:50:13 +0200 Subject: [PATCH 28/37] Fixed registering expressions in push/pop (#5964) * Fixed registering expressions in push/pop * Reused existing function --- src/api/api_solver.cpp | 4 ++-- src/api/c++/z3++.h | 17 +++++++++++------ src/api/z3_api.h | 4 ++-- src/sat/smt/user_solver.cpp | 4 ++-- src/smt/theory_user_propagator.cpp | 13 ++++++++----- src/tactic/user_propagator_base.h | 12 ++++++------ 6 files changed, 31 insertions(+), 23 deletions(-) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 99d332724..948064af6 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -883,8 +883,8 @@ extern "C" { Z3_TRY; RESET_ERROR_CODE(); init_solver(c, s); - user_propagator::push_eh_t _push = push_eh; - user_propagator::pop_eh_t _pop = pop_eh; + user_propagator::push_eh_t _push = (void(*)(void*,user_propagator::callback*)) push_eh; + user_propagator::pop_eh_t _pop = (void(*)(void*,user_propagator::callback*,unsigned)) pop_eh; user_propagator::fresh_eh_t _fresh = [=](void * user_ctx, ast_manager& m, user_propagator::context_obj*& _ctx) { ast_context_params params; params.set_foreign_manager(&m); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 4d60de433..101fa04a3 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -3964,18 +3964,23 @@ namespace z3 { } }; - static void push_eh(void* p) { + static void push_eh(void* _p, Z3_solver_callback cb) { + user_propagator_base* p = static_cast(_p); + scoped_cb _cb(p, cb); static_cast(p)->push(); } - static void pop_eh(void* p, unsigned num_scopes) { - static_cast(p)->pop(num_scopes); + static void pop_eh(void* _p, Z3_solver_callback cb, unsigned num_scopes) { + user_propagator_base* p = static_cast(_p); + scoped_cb _cb(p, cb); + static_cast(_p)->pop(num_scopes); } - static void* fresh_eh(void* p, Z3_context ctx) { + static void* fresh_eh(void* _p, Z3_context ctx) { + user_propagator_base* p = static_cast(_p); context* c = new context(ctx); - static_cast(p)->subcontexts.push_back(c); - return static_cast(p)->fresh(*c); + p->subcontexts.push_back(c); + return p->fresh(*c); } static void fixed_eh(void* _p, Z3_solver_callback cb, Z3_ast _var, Z3_ast _value) { diff --git a/src/api/z3_api.h b/src/api/z3_api.h index d7dd0a332..8a610bc6d 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -1434,8 +1434,8 @@ Z3_DECLARE_CLOSURE(Z3_error_handler, void, (Z3_context c, Z3_error_code e)); /** \brief callback functions for user propagator. */ -Z3_DECLARE_CLOSURE(Z3_push_eh, void, (void* ctx)); -Z3_DECLARE_CLOSURE(Z3_pop_eh, void, (void* ctx, unsigned num_scopes)); +Z3_DECLARE_CLOSURE(Z3_push_eh, void, (void* ctx, Z3_solver_callback cb)); +Z3_DECLARE_CLOSURE(Z3_pop_eh, void, (void* ctx, Z3_solver_callback cb, unsigned num_scopes)); Z3_DECLARE_CLOSURE(Z3_fresh_eh, void*, (void* ctx, Z3_context new_context)); Z3_DECLARE_CLOSURE(Z3_fixed_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t, Z3_ast value)); Z3_DECLARE_CLOSURE(Z3_eq_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast s, Z3_ast t)); diff --git a/src/sat/smt/user_solver.cpp b/src/sat/smt/user_solver.cpp index 6b3eb6718..d24af253e 100644 --- a/src/sat/smt/user_solver.cpp +++ b/src/sat/smt/user_solver.cpp @@ -88,7 +88,7 @@ namespace user_solver { void solver::push_core() { th_euf_solver::push_core(); m_prop_lim.push_back(m_prop.size()); - m_push_eh(m_user_context); + m_push_eh(m_user_context, this); } void solver::pop_core(unsigned num_scopes) { @@ -96,7 +96,7 @@ namespace user_solver { unsigned old_sz = m_prop_lim.size() - num_scopes; m_prop.shrink(m_prop_lim[old_sz]); m_prop_lim.shrink(old_sz); - m_pop_eh(m_user_context, num_scopes); + m_pop_eh(m_user_context, this, num_scopes); } void solver::propagate_consequence(prop_info const& prop) { diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 7c53aa8eb..daded32c7 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -25,6 +25,7 @@ using namespace smt; theory_user_propagator::theory_user_propagator(context& ctx): theory(ctx, ctx.get_manager().mk_family_id(user_propagator::plugin::name())), m_var2expr(ctx.get_manager()), + m_push_popping(false), m_to_add(ctx.get_manager()) {} @@ -38,7 +39,7 @@ void theory_user_propagator::force_push() { theory::push_scope_eh(); m_prop_lim.push_back(m_prop.size()); m_to_add_lim.push_back(m_to_add.size()); - m_push_eh(m_user_context); + m_push_eh(m_user_context, this); } } @@ -122,7 +123,8 @@ final_check_status theory_user_propagator::final_check_eh() { if (!(bool)m_final_eh) return FC_DONE; force_push(); - unsigned sz = m_prop.size(); + unsigned sz1 = m_prop.size(); + unsigned sz2 = m_expr2var.size(); try { m_final_eh(m_user_context, this); } @@ -130,7 +132,8 @@ final_check_status theory_user_propagator::final_check_eh() { throw default_exception("Exception thrown in \"final\"-callback"); } propagate(); - bool done = (sz == m_prop.size()) && !ctx.inconsistent(); + // check if it became inconsistent or something new was propagated/registered + bool done = !can_propagate() && !ctx.inconsistent(); return done ? FC_DONE : FC_CONTINUE; } @@ -169,11 +172,11 @@ void theory_user_propagator::pop_scope_eh(unsigned num_scopes) { old_sz = m_to_add_lim.size() - num_scopes; m_to_add.shrink(m_to_add_lim[old_sz]); m_to_add_lim.shrink(old_sz); - m_pop_eh(m_user_context, num_scopes); + m_pop_eh(m_user_context, this, num_scopes); } bool theory_user_propagator::can_propagate() { - return m_qhead < m_prop.size() || !m_to_add.empty(); + return m_qhead < m_prop.size() || m_to_add_qhead < m_to_add.size(); } void theory_user_propagator::propagate_consequence(prop_info const& prop) { diff --git a/src/tactic/user_propagator_base.h b/src/tactic/user_propagator_base.h index 07270ffe6..02a027762 100644 --- a/src/tactic/user_propagator_base.h +++ b/src/tactic/user_propagator_base.h @@ -17,13 +17,13 @@ namespace user_propagator { virtual ~context_obj() = default; }; - typedef std::function final_eh_t; - typedef std::function fixed_eh_t; - typedef std::function eq_eh_t; + typedef std::function final_eh_t; + typedef std::function fixed_eh_t; + typedef std::function eq_eh_t; typedef std::function fresh_eh_t; - typedef std::function push_eh_t; - typedef std::function pop_eh_t; - typedef std::function created_eh_t; + typedef std::function push_eh_t; + typedef std::function pop_eh_t; + typedef std::function created_eh_t; class plugin : public decl_plugin { From c996a66da04c882bc47dccacbf3507f1ab56f8e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Apr 2022 17:05:49 +0200 Subject: [PATCH 29/37] separate pre-processing, add callback parameter to push/pop in python API --- scripts/update_api.py | 4 +- src/api/python/z3/z3.py | 12 ++- src/opt/CMakeLists.txt | 1 + src/opt/maxlex.cpp | 18 ++--- src/opt/maxlex.h | 4 +- src/opt/maxres.cpp | 25 +++--- src/opt/maxres.h | 4 +- src/opt/maxsmt.cpp | 131 ++++++++------------------------ src/opt/maxsmt.h | 42 +++++----- src/opt/opt_mux.h | 32 ++++++++ src/opt/opt_preprocess.cpp | 102 +++++++++++++++++++++++++ src/opt/opt_preprocess.h | 38 +++++++++ src/opt/sortmax.cpp | 41 ++++------ src/opt/wmax.cpp | 28 +++---- src/opt/wmax.h | 4 +- src/sat/smt/euf_internalize.cpp | 1 + 16 files changed, 287 insertions(+), 200 deletions(-) create mode 100644 src/opt/opt_mux.h create mode 100644 src/opt/opt_preprocess.cpp create mode 100644 src/opt/opt_preprocess.h diff --git a/scripts/update_api.py b/scripts/update_api.py index ab1b4d6fd..d4d1ab0e0 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1820,8 +1820,8 @@ _error_handler_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint) _lib.Z3_set_error_handler.restype = None _lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type] -push_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p) -pop_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint) +push_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p) +pop_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint) fresh_eh_type = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) fixed_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 6f4dcf430..d3d6067c3 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -11237,12 +11237,16 @@ def ensure_prop_closures(): _prop_closures = PropClosures() -def user_prop_push(ctx): - _prop_closures.get(ctx).push() +def user_prop_push(ctx, cb): + prop = _prop_closures.get(ctx) + prop.cb = cb + prop.push() -def user_prop_pop(ctx, num_scopes): - _prop_closures.get(ctx).pop(num_scopes) +def user_prop_pop(ctx, cb, num_scopes): + prop = _prop_closures.get(ctx) + prop.cb = cb + pop(num_scopes) def user_prop_fresh(id, ctx): diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt index d88d11c0f..c652bcaea 100644 --- a/src/opt/CMakeLists.txt +++ b/src/opt/CMakeLists.txt @@ -8,6 +8,7 @@ z3_add_component(opt opt_lns.cpp opt_pareto.cpp opt_parse.cpp + opt_preprocess.cpp optsmt.cpp opt_solver.cpp pb_sls.cpp diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp index 46c7104d5..82eee6f5e 100644 --- a/src/opt/maxlex.cpp +++ b/src/opt/maxlex.cpp @@ -26,15 +26,15 @@ Author: namespace opt { - bool is_maxlex(weights_t & _ws) { - vector ws(_ws); - std::sort(ws.begin(), ws.end()); + bool is_maxlex(vector const & _ws) { + vector ws(_ws); + std::sort(ws.begin(), ws.end(), [&](soft const& s1, soft const& s2) { return s1.weight < s2.weight; }); ws.reverse(); rational sum(0); - for (rational const& w : ws) { + for (auto const& [e, w, t] : ws) { sum += w; } - for (rational const& w : ws) { + for (auto const& [e, w, t] : ws) { if (sum > w + w) return false; sum -= w; } @@ -185,8 +185,8 @@ namespace opt { public: - maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& s): - maxsmt_solver_base(c, ws, s), + maxlex(maxsat_context& c, unsigned id, vector& s): + maxsmt_solver_base(c, s), m(c.get_manager()), m_c(c) { // ensure that soft constraints are sorted with largest soft constraints first. @@ -210,8 +210,8 @@ namespace opt { } }; - maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft) { - return alloc(maxlex, c, id, ws, soft); + maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, vector& soft) { + return alloc(maxlex, c, id, soft); } } diff --git a/src/opt/maxlex.h b/src/opt/maxlex.h index b5c1a6e20..fc30b1fd8 100644 --- a/src/opt/maxlex.h +++ b/src/opt/maxlex.h @@ -21,9 +21,9 @@ Notes: namespace opt { - bool is_maxlex(weights_t & ws); + bool is_maxlex(vector const & ws); - maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft); + maxsmt_solver_base* mk_maxlex(maxsat_context& c, unsigned id, vector& soft); }; diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 1b4348105..0d1bf2394 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -129,10 +129,10 @@ private: typedef ptr_vector exprs; public: - maxres(maxsat_context& c, unsigned index, - weights_t& ws, expr_ref_vector const& soft, + maxres(maxsat_context& c, unsigned index, + vector& soft, strategy_t st): - maxsmt_solver_base(c, ws, soft), + maxsmt_solver_base(c, soft), m_index(index), m_B(m), m_asms(m), m_defs(m), m_new_core(m), @@ -875,17 +875,10 @@ public: } lbool init_local() { - m_lower.reset(); m_trail.reset(); lbool is_sat = l_true; - obj_map new_soft; - is_sat = find_mutexes(new_soft); - if (is_sat != l_true) { - return is_sat; - } - for (auto const& kv : new_soft) { - add_soft(kv.m_key, kv.m_value); - } + for (auto const& [e, w, t] : m_soft) + add_soft(e, w); m_max_upper = m_upper; m_found_feasible_optimum = false; m_last_index = 0; @@ -953,12 +946,12 @@ public: }; opt::maxsmt_solver_base* opt::mk_maxres( - maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) { - return alloc(maxres, c, id, ws, soft, maxres::s_primal); + maxsat_context& c, unsigned id, vector& soft) { + return alloc(maxres, c, id, soft, maxres::s_primal); } opt::maxsmt_solver_base* opt::mk_primal_dual_maxres( - maxsat_context& c, unsigned id, weights_t& ws, expr_ref_vector const& soft) { - return alloc(maxres, c, id, ws, soft, maxres::s_primal_dual); + maxsat_context& c, unsigned id, vector& soft) { + return alloc(maxres, c, id, soft, maxres::s_primal_dual); } diff --git a/src/opt/maxres.h b/src/opt/maxres.h index 85c83efba..25ef9bf05 100644 --- a/src/opt/maxres.h +++ b/src/opt/maxres.h @@ -21,9 +21,9 @@ Notes: namespace opt { - maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft); + maxsmt_solver_base* mk_maxres(maxsat_context& c, unsigned id, vector& soft); - maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, weights_t & ws, expr_ref_vector const& soft); + maxsmt_solver_base* mk_primal_dual_maxres(maxsat_context& c, unsigned id, vector& soft); }; diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index bf25f3f95..538ecf59b 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -28,6 +28,7 @@ Notes: #include "opt/wmax.h" #include "opt/opt_params.hpp" #include "opt/opt_context.h" +#include "opt/opt_preprocess.h" #include "smt/theory_wmaxsat.h" #include "smt/theory_pb.h" @@ -35,17 +36,15 @@ Notes: namespace opt { maxsmt_solver_base::maxsmt_solver_base( - maxsat_context& c, vector const& ws, expr_ref_vector const& softs): + maxsat_context& c, vector& s): m(c.get_manager()), m_c(c), + m_soft(s), m_assertions(m), m_trail(m) { c.get_base_model(m_model); SASSERT(m_model); updt_params(c.params()); - for (unsigned i = 0; i < ws.size(); ++i) { - m_soft.push_back(soft(expr_ref(softs.get(i), m), ws[i], false)); - } } void maxsmt_solver_base::updt_params(params_ref& p) { @@ -88,14 +87,22 @@ namespace opt { m_upper.reset(); for (soft& s : m_soft) { s.set_value(m.is_true(s.s)); - if (!s.is_true()) m_upper += s.weight; + if (!s.is_true()) + m_upper += s.weight; } + + preprocess pp(s()); + rational lower(0); + bool r = pp(m_soft, lower); + + if (lower != 0) + m_adjust_value.set_offset(lower + m_adjust_value.get_offset()); TRACE("opt", tout << "upper: " << m_upper << " assignments: "; for (soft& s : m_soft) tout << (s.is_true()?"T":"F"); tout << "\n";); - return true; + return r; } void maxsmt_solver_base::set_mus(bool f) { @@ -165,74 +172,9 @@ namespace opt { verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";); } - lbool maxsmt_solver_base::find_mutexes(obj_map& new_soft) { - m_lower.reset(); - expr_ref_vector fmls(m); - for (soft& s : m_soft) { - new_soft.insert(s.s, s.weight); - fmls.push_back(s.s); - } - vector mutexes; - lbool is_sat = s().find_mutexes(fmls, mutexes); - if (is_sat != l_true) { - return is_sat; - } - for (auto& mux : mutexes) { - process_mutex(mux, new_soft); - } - return l_true; - } - - struct maxsmt_compare_soft { - obj_map const& m_soft; - maxsmt_compare_soft(obj_map const& soft): m_soft(soft) {} - bool operator()(expr* a, expr* b) const { - return m_soft.find(a) > m_soft.find(b); - } - }; - - void maxsmt_solver_base::process_mutex(expr_ref_vector& mutex, obj_map& new_soft) { - TRACE("opt", - for (expr* e : mutex) { - tout << mk_pp(e, m) << " |-> " << new_soft.find(e) << "\n"; - }); - if (mutex.size() <= 1) { - return; - } - maxsmt_compare_soft cmp(new_soft); - ptr_vector _mutex(mutex.size(), mutex.data()); - std::sort(_mutex.begin(), _mutex.end(), cmp); - mutex.reset(); - mutex.append(_mutex.size(), _mutex.data()); - - rational weight(0), sum1(0), sum2(0); - vector weights; - for (expr* e : mutex) { - rational w = new_soft.find(e); - weights.push_back(w); - sum1 += w; - new_soft.remove(e); - } - for (unsigned i = mutex.size(); i-- > 0; ) { - expr_ref soft(m.mk_or(i+1, mutex.data()), m); - m_trail.push_back(soft); - rational w = weights[i]; - weight = w - weight; - m_lower += weight*rational(i); - IF_VERBOSE(1, verbose_stream() << "(opt.maxsat mutex size: " << i + 1 << " weight: " << weight << ")\n";); - sum2 += weight*rational(i+1); - new_soft.insert(soft, weight); - for (; i > 0 && weights[i-1] == w; --i) {} - weight = w; - } - SASSERT(sum1 == sum2); - } - - maxsmt::maxsmt(maxsat_context& c, unsigned index): - m(c.get_manager()), m_c(c), m_index(index), - m_soft_constraints(m), m_answer(m) {} + m(c.get_manager()), m_c(c), m_index(index), m_answer(m) {} lbool maxsmt::operator()() { lbool is_sat = l_undef; @@ -241,25 +183,25 @@ namespace opt { symbol const& maxsat_engine = m_c.maxsat_engine(); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";); - if (optp.maxlex_enable() && is_maxlex(m_weights)) { - m_msolver = mk_maxlex(m_c, m_index, m_weights, m_soft_constraints); + if (optp.maxlex_enable() && is_maxlex(m_soft)) { + m_msolver = mk_maxlex(m_c, m_index, m_soft); } - else if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) { - m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints); + else if (m_soft.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) { + m_msolver = mk_maxres(m_c, m_index, m_soft); } else if (maxsat_engine == symbol("pd-maxres")) { - m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints); + m_msolver = mk_primal_dual_maxres(m_c, m_index, m_soft); } else if (maxsat_engine == symbol("wmax")) { - m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints); + m_msolver = mk_wmax(m_c, m_soft); } else if (maxsat_engine == symbol("sortmax")) { - m_msolver = mk_sortmax(m_c, m_weights, m_soft_constraints); + m_msolver = mk_sortmax(m_c, m_soft); } else { auto str = maxsat_engine.str(); warning_msg("solver %s is not recognized, using default 'maxres'", str.c_str()); - m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints); + m_msolver = mk_maxres(m_c, m_index, m_soft); } if (m_msolver) { @@ -360,39 +302,32 @@ namespace opt { SASSERT(w.is_pos()); unsigned index = 0; if (m_soft_constraint_index.find(f, index)) { - m_weights[index] += w; + m_soft[index].weight += w; } else { - m_soft_constraint_index.insert(f, m_weights.size()); - m_soft_constraints.push_back(f); - m_weights.push_back(w); + m_soft_constraint_index.insert(f, m_soft.size()); + m_soft.push_back(soft(expr_ref(f, m), w, false)); } m_upper += w; } struct cmp_first { bool operator()(std::pair const& x, std::pair const& y) const { - return x.first < y.first; + return x.second < y.second; } }; void maxsmt::display_answer(std::ostream& out) const { - vector> sorted_weights; - unsigned n = m_weights.size(); - for (unsigned i = 0; i < n; ++i) { - sorted_weights.push_back(std::make_pair(i, m_weights[i])); - } - std::sort(sorted_weights.begin(), sorted_weights.end(), cmp_first()); - sorted_weights.reverse(); - for (unsigned i = 0; i < n; ++i) { - unsigned idx = sorted_weights[i].first; - expr* e = m_soft_constraints[idx]; + + unsigned idx = 0; + for (auto const & [_e, w, t] : m_soft) { + expr* e = _e.get(); bool is_not = m.is_not(e, e); - out << m_weights[idx] << ": " << mk_pp(e, m) + out << w << ": " << mk_pp(e, m) << ((is_not != get_assignment(idx))?" |-> true ":" |-> false ") << "\n"; - - } + ++idx; + } } diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 5bf637dde..4029bb911 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -52,21 +52,23 @@ namespace opt { // --------------------------------------------- // base class with common utilities used // by maxsmt solvers - // + // + + struct soft { + expr_ref s; + rational weight; + lbool value; + void set_value(bool t) { value = t?l_true:l_undef; } + void set_value(lbool t) { value = t; } + bool is_true() const { return value == l_true; } + soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {} + }; + class maxsmt_solver_base : public maxsmt_solver { protected: - struct soft { - expr_ref s; - rational weight; - lbool value; - void set_value(bool t) { value = t?l_true:l_undef; } - void set_value(lbool t) { value = t; } - bool is_true() const { return value == l_true; } - soft(expr_ref const& s, rational const& w, bool t): s(s), weight(w), value(t?l_true:l_undef) {} - }; ast_manager& m; maxsat_context& m_c; - vector m_soft; + vector& m_soft; expr_ref_vector m_assertions; expr_ref_vector m_trail; rational m_lower; @@ -76,8 +78,8 @@ namespace opt { params_ref m_params; // config public: - maxsmt_solver_base(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft); - + maxsmt_solver_base(maxsat_context& c, vector& soft); + ~maxsmt_solver_base() override {} rational get_lower() const override { return m_lower; } rational get_upper() const override { return m_upper; } @@ -102,8 +104,6 @@ namespace opt { smt::theory_wmaxsat& operator()(); }; - lbool find_mutexes(obj_map& new_soft); - void reset_upper(); @@ -111,9 +111,6 @@ namespace opt { void enable_sls(bool force); void trace_bounds(char const* solver); - void process_mutex(expr_ref_vector& mutex, obj_map& new_soft); - - }; /** @@ -126,10 +123,9 @@ namespace opt { maxsat_context& m_c; unsigned m_index; scoped_ptr m_msolver; - expr_ref_vector m_soft_constraints; + vector m_soft; obj_map m_soft_constraint_index; expr_ref_vector m_answer; - vector m_weights; rational m_lower; rational m_upper; adjust_value m_adjust_value; @@ -142,9 +138,9 @@ namespace opt { void updt_params(params_ref& p); void add(expr* f, rational const& w); void set_adjust_value(adjust_value& adj); - unsigned size() const { return m_soft_constraints.size(); } - expr* operator[](unsigned idx) const { return m_soft_constraints[idx]; } - rational weight(unsigned idx) const { return m_weights[idx]; } + unsigned size() const { return m_soft.size(); } + expr* operator[](unsigned idx) const { return m_soft[idx].s; } + rational weight(unsigned idx) const { return m_soft[idx].weight; } void commit_assignment(); rational get_lower() const; rational get_upper() const; diff --git a/src/opt/opt_mux.h b/src/opt/opt_mux.h new file mode 100644 index 000000000..b093026f0 --- /dev/null +++ b/src/opt/opt_mux.h @@ -0,0 +1,32 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + opt_mux.h + +Abstract: + + Find mutexes - at most 1 constraints and modify soft constraints and bounds. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-04-11 + +--*/ + +#pragma once + +#include "opt/maxsmt.h" + +namespace opt { + + class mux { + ast_manager& m; + solver& s; + + public: + mux(solver& s); + lbool operator()(vector& soft, rational& bound); + }; +}; diff --git a/src/opt/opt_preprocess.cpp b/src/opt/opt_preprocess.cpp new file mode 100644 index 000000000..f65d5d09b --- /dev/null +++ b/src/opt/opt_preprocess.cpp @@ -0,0 +1,102 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + opt_preprocess.cpp + +Abstract: + + Pre-processing for MaxSMT + + Find mutexes - at most 1 constraints and modify soft constraints and bounds. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-04-11 + +--*/ + +#pragma once + +#include "opt/opt_preprocess.h" + +namespace opt { + + bool preprocess::find_mutexes(vector& softs, rational& lower) { + expr_ref_vector fmls(m); + obj_map new_soft; + for (soft& sf : softs) { + m_trail.push_back(sf.s); + if (new_soft.contains(sf.s)) + new_soft[sf.s] += sf.weight; + else + new_soft.insert(sf.s, sf.weight); + fmls.push_back(sf.s); + } + vector mutexes; + lbool is_sat = s.find_mutexes(fmls, mutexes); + if (is_sat == l_false) + return true; + if (is_sat == l_undef) + return false; + for (auto& mux : mutexes) + process_mutex(mux, new_soft, lower); + softs.reset(); + for (auto const& [k, v] : new_soft) + softs.push_back(soft(expr_ref(k, m), v, false)); + m_trail.reset(); + return true; + } + + struct maxsmt_compare_soft { + obj_map const& m_soft; + maxsmt_compare_soft(obj_map const& soft): m_soft(soft) {} + bool operator()(expr* a, expr* b) const { + return m_soft.find(a) > m_soft.find(b); + } + }; + + void preprocess::process_mutex(expr_ref_vector& mutex, obj_map& new_soft, rational& lower) { + TRACE("opt", + for (expr* e : mutex) { + tout << mk_pp(e, m) << " |-> " << new_soft.find(e) << "\n"; + }); + if (mutex.size() <= 1) + return; + + maxsmt_compare_soft cmp(new_soft); + ptr_vector _mutex(mutex.size(), mutex.data()); + std::sort(_mutex.begin(), _mutex.end(), cmp); + mutex.reset(); + mutex.append(_mutex.size(), _mutex.data()); + + rational weight(0), sum1(0), sum2(0); + vector weights; + for (expr* e : mutex) { + rational w = new_soft.find(e); + weights.push_back(w); + sum1 += w; + new_soft.remove(e); + } + for (unsigned i = mutex.size(); i-- > 0; ) { + expr_ref soft(m.mk_or(i+1, mutex.data()), m); + m_trail.push_back(soft); + rational w = weights[i]; + weight = w - weight; + lower += weight*rational(i); + IF_VERBOSE(1, verbose_stream() << "(opt.maxsat mutex size: " << i + 1 << " weight: " << weight << ")\n";); + sum2 += weight*rational(i+1); + new_soft.insert(soft, weight); + for (; i > 0 && weights[i-1] == w; --i) {} + weight = w; + } + SASSERT(sum1 == sum2); + } + + preprocess::preprocess(solver& s): m(s.get_manager()), s(s), m_trail(m) {} + + bool preprocess::operator()(vector& soft, rational& lower) { + return find_mutexes(soft, lower); + } +}; diff --git a/src/opt/opt_preprocess.h b/src/opt/opt_preprocess.h new file mode 100644 index 000000000..8918e5e89 --- /dev/null +++ b/src/opt/opt_preprocess.h @@ -0,0 +1,38 @@ +/*++ +Copyright (c) 2021 Microsoft Corporation + +Module Name: + + opt_preprocess.h + +Abstract: + + Pre-processing for MaxSMT + + Find mutexes - at most 1 constraints and modify soft constraints and bounds. + +Author: + + Nikolaj Bjorner (nbjorner) 2022-04-11 + +--*/ + +#pragma once + +#include "opt/maxsmt.h" + +namespace opt { + + class preprocess { + ast_manager& m; + solver& s; + expr_ref_vector m_trail; + + bool find_mutexes(vector& softs, rational& lower); + void process_mutex(expr_ref_vector& mutex, obj_map& new_soft, rational& lower); + + public: + preprocess(solver& s); + bool operator()(vector& soft, rational& lower); + }; +}; diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp index c6a2f04a9..a6539e129 100644 --- a/src/opt/sortmax.cpp +++ b/src/opt/sortmax.cpp @@ -36,34 +36,27 @@ namespace opt { expr_ref_vector m_trail; func_decl_ref_vector m_fresh; ref m_filter; - sortmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): - maxsmt_solver_base(c, ws, soft), m_sort(*this), m_trail(m), m_fresh(m) {} + sortmax(maxsat_context& c, vector& s): + maxsmt_solver_base(c, s), m_sort(*this), m_trail(m), m_fresh(m) {} ~sortmax() override {} lbool operator()() override { - obj_map soft; - if (!init()) { - return l_false; - } - lbool is_sat = find_mutexes(soft); - if (is_sat != l_true) { - return is_sat; - } + if (!init()) + return l_undef; + + lbool is_sat = l_true; m_filter = alloc(generic_model_converter, m, "sortmax"); - rational offset = m_lower; - m_upper = offset; expr_ref_vector in(m); expr_ref tmp(m); ptr_vector out; - obj_map::iterator it = soft.begin(), end = soft.end(); - for (; it != end; ++it) { - if (!it->m_value.is_unsigned()) { + for (auto const & [e, w, t] : m_soft) { + if (!w.is_unsigned()) { throw default_exception("sortmax can only handle unsigned weights. Use a different heuristic."); } - unsigned n = it->m_value.get_unsigned(); + unsigned n = w.get_unsigned(); while (n > 0) { - in.push_back(it->m_key); + in.push_back(e); --n; } } @@ -71,19 +64,15 @@ namespace opt { // initialize sorting network outputs using the initial assignment. unsigned first = 0; - it = soft.begin(); - for (; it != end; ++it) { - if (m_model->is_true(it->m_key)) { - unsigned n = it->m_value.get_unsigned(); + for (auto const & [e, w, t] : m_soft) { + if (t == l_true) { + unsigned n = w.get_unsigned(); while (n > 0) { s().assert_expr(out[first]); ++first; --n; } } - else { - m_upper += it->m_value; - } } while (l_true == is_sat && first < out.size() && m_lower < m_upper) { trace_bounds("sortmax"); @@ -149,8 +138,8 @@ namespace opt { }; - maxsmt_solver_base* mk_sortmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) { - return alloc(sortmax, c, ws, soft); + maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector& s) { + return alloc(sortmax, c, s); } } diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 22a660799..812c8f954 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -44,8 +44,8 @@ namespace opt { } public: - wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): - maxsmt_solver_base(c, ws, soft), + wmax(maxsat_context& c, vector& s): + maxsmt_solver_base(c, s), m_trail(m), m_defs(m) {} @@ -54,22 +54,18 @@ namespace opt { lbool operator()() override { TRACE("opt", tout << "weighted maxsat\n";); scoped_ensure_theory wth(*this); - obj_map soft; reset(); - lbool is_sat = find_mutexes(soft); - if (is_sat != l_true) { - return is_sat; - } - m_upper = m_lower; + if (init()) + return l_undef; + + lbool is_sat = l_true; + expr_ref_vector asms(m); vector cores; - for (auto const& kv : soft) { - assert_weighted(wth(), kv.m_key, kv.m_value); - if (!is_true(kv.m_key)) { - m_upper += kv.m_value; - } - } + for (auto const& [k, w, t] : m_soft) + assert_weighted(wth(), k, w); + wth().init_min_cost(m_upper - m_lower); trace_bounds("wmax"); @@ -308,8 +304,8 @@ namespace opt { }; - maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft) { - return alloc(wmax, c, ws, soft); + maxsmt_solver_base* mk_wmax(maxsat_context& c, vector & s) { + return alloc(wmax, c, s); } } diff --git a/src/opt/wmax.h b/src/opt/wmax.h index 6cc3ed46b..0a5167269 100644 --- a/src/opt/wmax.h +++ b/src/opt/wmax.h @@ -22,8 +22,8 @@ Notes: #include "opt/maxsmt.h" namespace opt { - maxsmt_solver_base* mk_wmax(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft); + maxsmt_solver_base* mk_wmax(maxsat_context& c, vector& s); - maxsmt_solver_base* mk_sortmax(maxsat_context& c, weights_t & ws, expr_ref_vector const& soft); + maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector& s); } diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index 116621dcc..045b92c99 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -312,6 +312,7 @@ namespace euf { } } else if (m.is_distinct(e)) { + // TODO - add lazy case for large values of sz. expr_ref_vector eqs(m); unsigned sz = n->num_args(); for (unsigned i = 0; i < sz; ++i) { From ac55e29a56d78bc0bbba26c7346ba0f45431f99b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 11 Apr 2022 22:23:42 +0200 Subject: [PATCH 30/37] disable propagation Signed-off-by: Nikolaj Bjorner --- src/opt/maxsmt.cpp | 19 +++++++++++-------- src/opt/maxsmt.h | 6 +++--- 2 files changed, 14 insertions(+), 11 deletions(-) diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 538ecf59b..dab9ae445 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -91,12 +91,15 @@ namespace opt { m_upper += s.weight; } + return true; + preprocess pp(s()); rational lower(0); bool r = pp(m_soft, lower); + if (lower != 0) - m_adjust_value.set_offset(lower + m_adjust_value.get_offset()); + m_adjust_value->set_offset(lower + m_adjust_value->get_offset()); TRACE("opt", tout << "upper: " << m_upper << " assignments: "; @@ -166,8 +169,8 @@ namespace opt { void maxsmt_solver_base::trace_bounds(char const * solver) { IF_VERBOSE(1, - rational l = m_adjust_value(m_lower); - rational u = m_adjust_value(m_upper); + rational l = (*m_adjust_value)(m_lower); + rational u = (*m_adjust_value)(m_upper); if (l > u) std::swap(l, u); verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";); } @@ -206,7 +209,7 @@ namespace opt { if (m_msolver) { m_msolver->updt_params(m_params); - m_msolver->set_adjust_value(m_adjust_value); + m_msolver->set_adjust_value(*m_adjust_value); is_sat = l_undef; try { is_sat = (*m_msolver)(); @@ -231,9 +234,9 @@ namespace opt { } void maxsmt::set_adjust_value(adjust_value& adj) { - m_adjust_value = adj; + m_adjust_value = &adj; if (m_msolver) { - m_msolver->set_adjust_value(m_adjust_value); + m_msolver->set_adjust_value(adj); } } @@ -265,7 +268,7 @@ namespace opt { rational q = m_msolver->get_lower(); if (q > r) r = q; } - return m_adjust_value(r); + return (*m_adjust_value)(r); } rational maxsmt::get_upper() const { @@ -274,7 +277,7 @@ namespace opt { rational q = m_msolver->get_upper(); if (q < r) r = q; } - return m_adjust_value(r); + return (*m_adjust_value)(r); } void maxsmt::update_lower(rational const& r) { diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 4029bb911..5a3dc4ca8 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -35,7 +35,7 @@ namespace opt { class maxsmt_solver { protected: - adjust_value m_adjust_value; + adjust_value* m_adjust_value = nullptr; public: virtual ~maxsmt_solver() {} virtual lbool operator()() = 0; @@ -45,7 +45,7 @@ namespace opt { virtual void collect_statistics(statistics& st) const = 0; virtual void get_model(model_ref& mdl, svector& labels) = 0; virtual void updt_params(params_ref& p) = 0; - void set_adjust_value(adjust_value& adj) { m_adjust_value = adj; } + void set_adjust_value(adjust_value& adj) { m_adjust_value = &adj; } }; @@ -128,7 +128,7 @@ namespace opt { expr_ref_vector m_answer; rational m_lower; rational m_upper; - adjust_value m_adjust_value; + adjust_value* m_adjust_value = nullptr; model_ref m_model; svector m_labels; params_ref m_params; From b264e6c2904456beae27ce19ec4997251034e42c Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com> Date: Tue, 12 Apr 2022 12:29:53 +0200 Subject: [PATCH 31/37] Reverted reusing can_propagate (#5966) * Fixed registering expressions in push/pop * Reused existing function * Reverted reusing can_propagate --- src/smt/theory_user_propagator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index daded32c7..f783f22fb 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -133,7 +133,7 @@ final_check_status theory_user_propagator::final_check_eh() { } propagate(); // check if it became inconsistent or something new was propagated/registered - bool done = !can_propagate() && !ctx.inconsistent(); + bool done = (sz1 == m_prop.size()) && (sz2 == m_expr2var.size()) && !ctx.inconsistent(); return done ? FC_DONE : FC_CONTINUE; } From 032768b0fc2a6350950ac3065f50ca29eb5495f0 Mon Sep 17 00:00:00 2001 From: Audrey Dutcher Date: Tue, 12 Apr 2022 23:29:36 -0700 Subject: [PATCH 32/37] setup.py: copy generated python files correctly (#5975) --- src/api/python/setup.py | 14 ++++---------- 1 file changed, 4 insertions(+), 10 deletions(-) diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 1b455bb56..5309142f2 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -154,16 +154,10 @@ def _copy_bins(): _clean_bins() - python_dir = None - if RELEASE_DIR is not None: - python_dir = os.path.join(RELEASE_DIR, 'bin', 'python') - elif SRC_DIR == SRC_DIR_LOCAL: - python_dir = os.path.join(SRC_DIR, 'src', 'api', 'python') - if python_dir is not None: - py_z3_build_dir = os.path.join(BUILD_DIR, 'python', 'z3') - root_z3_dir = os.path.join(ROOT_DIR, 'z3') - shutil.copy(os.path.join(py_z3_build_dir, 'z3core.py'), root_z3_dir) - shutil.copy(os.path.join(py_z3_build_dir, 'z3consts.py'), root_z3_dir) + py_z3_build_dir = os.path.join(BUILD_DIR, 'python', 'z3') + root_z3_dir = os.path.join(ROOT_DIR, 'z3') + shutil.copy(os.path.join(py_z3_build_dir, 'z3core.py'), root_z3_dir) + shutil.copy(os.path.join(py_z3_build_dir, 'z3consts.py'), root_z3_dir) # STEP 2: Copy the shared library, the executable and the headers From 9834d7aae0faf2b1cc9b96c7c20b087f96374c51 Mon Sep 17 00:00:00 2001 From: Zachary Wimer Date: Tue, 12 Apr 2022 23:31:24 -0700 Subject: [PATCH 33/37] Setup.py fix dependencies (#5971) * Add wheel as build dependency * pyproject toml update --- src/api/python/pyproject.toml | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 src/api/python/pyproject.toml diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml new file mode 100644 index 000000000..ead8162b7 --- /dev/null +++ b/src/api/python/pyproject.toml @@ -0,0 +1,3 @@ +[build-system] +requires = ["setuptools>=46.4.0", "wheel"] +build-backend = "setuptools.build_meta" From c0b455e01089fdafd2dadd5124d2080dff777823 Mon Sep 17 00:00:00 2001 From: Zachary Wimer Date: Tue, 12 Apr 2022 23:48:08 -0700 Subject: [PATCH 34/37] Add cmake setup.py build dep (#5972) * Add wheel as build dependency * Add cmake as a python build dependency * pyproject toml update Co-authored-by: Nikolaj Bjorner --- src/api/python/pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/pyproject.toml b/src/api/python/pyproject.toml index ead8162b7..a9f2676a7 100644 --- a/src/api/python/pyproject.toml +++ b/src/api/python/pyproject.toml @@ -1,3 +1,3 @@ [build-system] -requires = ["setuptools>=46.4.0", "wheel"] +requires = ["setuptools>=46.4.0", "wheel", "cmake"] build-backend = "setuptools.build_meta" From c9fa00aec1442464c9cc2ab6f3d2e5c749232b6e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Apr 2022 11:22:43 +0200 Subject: [PATCH 35/37] expose recursive functions with own op-code over API --- src/api/api_ast.cpp | 3 +++ src/api/z3_api.h | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 7ee95afc8..9f9039378 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1329,6 +1329,9 @@ extern "C" { } } + if (mk_c(c)->recfun().get_family_id() == _d->get_family_id()) + return Z3_OP_RECURSIVE; + return Z3_OP_UNINTERPRETED; Z3_CATCH_RETURN(Z3_OP_UNINTERPRETED); } diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 8a610bc6d..1388d0ab1 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -996,6 +996,8 @@ typedef enum information is exposed. Tools may use the string representation of the function declaration to obtain more information. + - Z3_OP_RECURSIVE: function declared as recursive + - Z3_OP_UNINTERPRETED: kind used for uninterpreted symbols. */ typedef enum { @@ -1320,6 +1322,7 @@ typedef enum { Z3_OP_FPA_BV2RM, Z3_OP_INTERNAL, + Z3_OP_RECURSIVE, Z3_OP_UNINTERPRETED } Z3_decl_kind; From 3f5eb7fcf29dad76498e560826f9474016358027 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Apr 2022 11:24:16 +0200 Subject: [PATCH 36/37] re-enable pre-process --- src/opt/maxlex.cpp | 2 +- src/opt/maxres.cpp | 4 +--- src/opt/maxsmt.cpp | 42 ++++++++++++++++++++--------------------- src/opt/maxsmt.h | 10 +++------- src/opt/opt_context.cpp | 40 +++++++++++++++++++++------------------ src/opt/opt_context.h | 9 +++++++-- src/opt/opt_solver.h | 1 + src/opt/sortmax.cpp | 8 ++++---- src/opt/wmax.cpp | 8 ++++---- src/opt/wmax.h | 4 ++-- 10 files changed, 66 insertions(+), 62 deletions(-) diff --git a/src/opt/maxlex.cpp b/src/opt/maxlex.cpp index 82eee6f5e..fa97359d0 100644 --- a/src/opt/maxlex.cpp +++ b/src/opt/maxlex.cpp @@ -186,7 +186,7 @@ namespace opt { public: maxlex(maxsat_context& c, unsigned id, vector& s): - maxsmt_solver_base(c, s), + maxsmt_solver_base(c, s, id), m(c.get_manager()), m_c(c) { // ensure that soft constraints are sorted with largest soft constraints first. diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 0d1bf2394..135e0f80e 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -95,7 +95,6 @@ private: expr_ref_vector const& soft() override { return i.m_asms; } }; - unsigned m_index; stats m_stats; expr_ref_vector m_B; expr_ref_vector m_asms; @@ -132,8 +131,7 @@ public: maxres(maxsat_context& c, unsigned index, vector& soft, strategy_t st): - maxsmt_solver_base(c, soft), - m_index(index), + maxsmt_solver_base(c, soft, index), m_B(m), m_asms(m), m_defs(m), m_new_core(m), m_mus(c.get_solver()), diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index dab9ae445..a3d5f2f45 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -35,10 +35,10 @@ Notes: namespace opt { - maxsmt_solver_base::maxsmt_solver_base( - maxsat_context& c, vector& s): + maxsmt_solver_base::maxsmt_solver_base(maxsat_context& c, vector& s, unsigned index): m(c.get_manager()), m_c(c), + m_index(index), m_soft(s), m_assertions(m), m_trail(m) { @@ -91,18 +91,17 @@ namespace opt { m_upper += s.weight; } - return true; + // return true; preprocess pp(s()); rational lower(0); bool r = pp(m_soft, lower); - - if (lower != 0) - m_adjust_value->set_offset(lower + m_adjust_value->get_offset()); + m_c.add_offset(m_index, lower); + m_upper -= lower; TRACE("opt", - tout << "upper: " << m_upper << " assignments: "; + tout << "lower " << lower << " upper: " << m_upper << " assignments: "; for (soft& s : m_soft) tout << (s.is_true()?"T":"F"); tout << "\n";); return r; @@ -169,8 +168,8 @@ namespace opt { void maxsmt_solver_base::trace_bounds(char const * solver) { IF_VERBOSE(1, - rational l = (*m_adjust_value)(m_lower); - rational u = (*m_adjust_value)(m_upper); + rational l = m_c.adjust(m_index, m_lower); + rational u = m_c.adjust(m_index, m_upper); if (l > u) std::swap(l, u); verbose_stream() << "(opt." << solver << " [" << l << ":" << u << "])\n";); } @@ -196,10 +195,10 @@ namespace opt { m_msolver = mk_primal_dual_maxres(m_c, m_index, m_soft); } else if (maxsat_engine == symbol("wmax")) { - m_msolver = mk_wmax(m_c, m_soft); + m_msolver = mk_wmax(m_c, m_soft, m_index); } else if (maxsat_engine == symbol("sortmax")) { - m_msolver = mk_sortmax(m_c, m_soft); + m_msolver = mk_sortmax(m_c, m_soft, m_index); } else { auto str = maxsat_engine.str(); @@ -209,7 +208,6 @@ namespace opt { if (m_msolver) { m_msolver->updt_params(m_params); - m_msolver->set_adjust_value(*m_adjust_value); is_sat = l_undef; try { is_sat = (*m_msolver)(); @@ -233,13 +231,6 @@ namespace opt { return is_sat; } - void maxsmt::set_adjust_value(adjust_value& adj) { - m_adjust_value = &adj; - if (m_msolver) { - m_msolver->set_adjust_value(adj); - } - } - void maxsmt::reset_upper() { if (m_msolver) { m_msolver->reset_upper(); @@ -268,7 +259,7 @@ namespace opt { rational q = m_msolver->get_lower(); if (q > r) r = q; } - return (*m_adjust_value)(r); + return m_c.adjust(m_index, r); } rational maxsmt::get_upper() const { @@ -277,7 +268,7 @@ namespace opt { rational q = m_msolver->get_upper(); if (q < r) r = q; } - return (*m_adjust_value)(r); + return m_c.adjust(m_index, r); } void maxsmt::update_lower(rational const& r) { @@ -370,6 +361,7 @@ namespace opt { model_ref m_model; ref m_fm; symbol m_maxsat_engine; + vector m_offsets; public: solver_maxsat_context(params_ref& p, solver* s, model * m): m_params(p), @@ -394,6 +386,14 @@ namespace opt { bool verify_model(unsigned id, model* mdl, rational const& v) override { return true; }; void set_model(model_ref& _m) override { m_model = _m; } void model_updated(model* mdl) override { } // no-op + rational adjust(unsigned id, rational const& r) override { + m_offsets.reserve(id+1); + return r + m_offsets[id]; + } + void add_offset(unsigned id, rational const& r) override { + m_offsets.reserve(id+1); + m_offsets[id] += r; + } }; lbool maxsmt_wrapper::operator()(vector>& soft) { diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 5a3dc4ca8..b0ae5eeb1 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -34,8 +34,6 @@ namespace opt { class maxsat_context; class maxsmt_solver { - protected: - adjust_value* m_adjust_value = nullptr; public: virtual ~maxsmt_solver() {} virtual lbool operator()() = 0; @@ -45,7 +43,6 @@ namespace opt { virtual void collect_statistics(statistics& st) const = 0; virtual void get_model(model_ref& mdl, svector& labels) = 0; virtual void updt_params(params_ref& p) = 0; - void set_adjust_value(adjust_value& adj) { m_adjust_value = &adj; } }; @@ -67,7 +64,8 @@ namespace opt { class maxsmt_solver_base : public maxsmt_solver { protected: ast_manager& m; - maxsat_context& m_c; + maxsat_context& m_c; + unsigned m_index; vector& m_soft; expr_ref_vector m_assertions; expr_ref_vector m_trail; @@ -78,7 +76,7 @@ namespace opt { params_ref m_params; // config public: - maxsmt_solver_base(maxsat_context& c, vector& soft); + maxsmt_solver_base(maxsat_context& c, vector& soft, unsigned index); ~maxsmt_solver_base() override {} rational get_lower() const override { return m_lower; } @@ -128,7 +126,6 @@ namespace opt { expr_ref_vector m_answer; rational m_lower; rational m_upper; - adjust_value* m_adjust_value = nullptr; model_ref m_model; svector m_labels; params_ref m_params; @@ -137,7 +134,6 @@ namespace opt { lbool operator()(); void updt_params(params_ref& p); void add(expr* f, rational const& w); - void set_adjust_value(adjust_value& adj); unsigned size() const { return m_soft.size(); } expr* operator[](unsigned idx) const { return m_soft[idx].s; } rational weight(unsigned idx) const { return m_soft[idx].weight; } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 8848b61c9..25982e89e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -398,7 +398,7 @@ namespace opt { } void context::set_model(model_ref& m) { - m_model = m; + m_model = m; opt_params optp(m_params); if (optp.dump_models() && m) { model_ref md = m->copy(); @@ -930,7 +930,8 @@ namespace opt { bool context::is_maxsat(expr* fml, expr_ref_vector& terms, vector& weights, rational& offset, bool& neg, symbol& id, expr_ref& orig_term, unsigned& index) { - if (!is_app(fml)) return false; + if (!is_app(fml)) + return false; neg = false; orig_term = nullptr; index = 0; @@ -1105,8 +1106,7 @@ namespace opt { obj.m_weights.append(weights); obj.m_adjust_value.set_offset(offset); obj.m_adjust_value.set_negate(neg); - m_maxsmts.find(id)->set_adjust_value(obj.m_adjust_value); - TRACE("opt", tout << "maxsat: " << id << " offset:" << offset << "\n"; + TRACE("opt", tout << "maxsat: " << neg << " " << id << " offset: " << offset << "\n"; tout << terms << "\n";); } else if (is_maximize(fml, tr, orig_term, index)) { @@ -1158,7 +1158,14 @@ namespace opt { #endif } + rational context::adjust(unsigned id, rational const& v) { + return m_objectives[id].m_adjust_value(v); + } + void context::add_offset(unsigned id, rational const& o) { + m_objectives[id].m_adjust_value.add_offset(o); + } + bool context::verify_model(unsigned index, model* md, rational const& _v) { rational r; app_ref term = m_objectives[index].m_term; @@ -1341,24 +1348,21 @@ namespace opt { break; } case O_MAXSMT: { - bool ok = true; - for (unsigned j = 0; ok && j < obj.m_terms.size(); ++j) { + for (unsigned j = 0; j < obj.m_terms.size(); ++j) { val = (*m_model)(obj.m_terms[j]); TRACE("opt", tout << mk_pp(obj.m_terms[j], m) << " " << val << "\n";); - if (!m.is_true(val)) { + if (!m.is_true(val)) r += obj.m_weights[j]; - } } - if (ok) { - maxsmt& ms = *m_maxsmts.find(obj.m_id); - if (is_lower) { - ms.update_upper(r); - TRACE("opt", tout << "update upper from " << r << " to " << ms.get_upper() << "\n";); - } - else { - ms.update_lower(r); - TRACE("opt", tout << "update lower from " << r << " to " << ms.get_lower() << "\n";); - } + + maxsmt& ms = *m_maxsmts.find(obj.m_id); + if (is_lower) { + ms.update_upper(r); + TRACE("opt", tout << "update upper from " << r << " to " << ms.get_upper() << "\n";); + } + else { + ms.update_lower(r); + TRACE("opt", tout << "update lower from " << r << " to " << ms.get_lower() << "\n";); } break; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 1e950174a..c02689a38 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -57,6 +57,8 @@ namespace opt { virtual smt::context& smt_context() = 0; // access SMT context for SMT based MaxSMT solver (wmax requires SMT core) virtual unsigned num_objectives() = 0; virtual bool verify_model(unsigned id, model* mdl, rational const& v) = 0; + virtual rational adjust(unsigned id, rational const& v) = 0; + virtual void add_offset(unsigned id, rational const& o) = 0; virtual void set_model(model_ref& _m) = 0; virtual void model_updated(model* mdl) = 0; }; @@ -93,7 +95,7 @@ namespace opt { app_ref m_term; // for maximize, minimize term expr_ref_vector m_terms; // for maxsmt vector m_weights; // for maxsmt - adjust_value m_adjust_value; + adjust_value m_adjust_value; symbol m_id; // for maxsmt unsigned m_index; // for maximize/minimize index @@ -269,11 +271,14 @@ namespace opt { void model_updated(model* mdl) override; + rational adjust(unsigned id, rational const& v) override; + + void add_offset(unsigned id, rational const& o) override; + void register_on_model(on_model_t& ctx, std::function& on_model) { m_on_model_ctx = ctx; m_on_model_eh = on_model; } - void collect_timer_stats(statistics& st) const { if (m_time != 0) diff --git a/src/opt/opt_solver.h b/src/opt/opt_solver.h index caac008fd..47fe86f94 100644 --- a/src/opt/opt_solver.h +++ b/src/opt/opt_solver.h @@ -48,6 +48,7 @@ namespace opt { void set_offset(rational const& o) { m_offset = o; } void set_negate(bool neg) { m_negate = neg; } rational const& get_offset() const { return m_offset; } + void add_offset(rational const& o) { if (m_negate) m_offset -= o; else m_offset += o; } bool get_negate() { return m_negate; } inf_eps operator()(inf_eps const& r) const { inf_eps result = r; diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp index a6539e129..962369bf2 100644 --- a/src/opt/sortmax.cpp +++ b/src/opt/sortmax.cpp @@ -36,8 +36,8 @@ namespace opt { expr_ref_vector m_trail; func_decl_ref_vector m_fresh; ref m_filter; - sortmax(maxsat_context& c, vector& s): - maxsmt_solver_base(c, s), m_sort(*this), m_trail(m), m_fresh(m) {} + sortmax(maxsat_context& c, vector& s, unsigned index): + maxsmt_solver_base(c, s, index), m_sort(*this), m_trail(m), m_fresh(m) {} ~sortmax() override {} @@ -138,8 +138,8 @@ namespace opt { }; - maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector& s) { - return alloc(sortmax, c, s); + maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector& s, unsigned index) { + return alloc(sortmax, c, s, index); } } diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 812c8f954..1fbd26cb8 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -44,8 +44,8 @@ namespace opt { } public: - wmax(maxsat_context& c, vector& s): - maxsmt_solver_base(c, s), + wmax(maxsat_context& c, vector& s, unsigned index): + maxsmt_solver_base(c, s, index), m_trail(m), m_defs(m) {} @@ -304,8 +304,8 @@ namespace opt { }; - maxsmt_solver_base* mk_wmax(maxsat_context& c, vector & s) { - return alloc(wmax, c, s); + maxsmt_solver_base* mk_wmax(maxsat_context& c, vector & s, unsigned index) { + return alloc(wmax, c, s, index); } } diff --git a/src/opt/wmax.h b/src/opt/wmax.h index 0a5167269..7f5b26ac6 100644 --- a/src/opt/wmax.h +++ b/src/opt/wmax.h @@ -22,8 +22,8 @@ Notes: #include "opt/maxsmt.h" namespace opt { - maxsmt_solver_base* mk_wmax(maxsat_context& c, vector& s); + maxsmt_solver_base* mk_wmax(maxsat_context& c, vector& s, unsigned index); - maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector& s); + maxsmt_solver_base* mk_sortmax(maxsat_context& c, vector& s, unsigned index); } From ddbe17d581d9835f9bc57079383eefce2b841162 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Apr 2022 16:08:54 +0200 Subject: [PATCH 37/37] #5965 define the is_bool on ArithSortRef --- src/api/python/z3/z3.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index d3d6067c3..223b3e038 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -2279,6 +2279,9 @@ class ArithSortRef(SortRef): """ return self.kind() == Z3_INT_SORT + def is_bool(self): + return False + def subsort(self, other): """Return `True` if `self` is a subsort of `other`.""" return self.is_int() and is_arith_sort(other) and other.is_real()