diff --git a/.github/workflows/docker-image.yml b/.github/workflows/docker-image.yml index c3949d6c5..cf930c86e 100644 --- a/.github/workflows/docker-image.yml +++ b/.github/workflows/docker-image.yml @@ -1,8 +1,6 @@ name: Publish Docker image on: - schedule: - - cron: "0 1 * * 0" # every Sunday at 1 am workflow_dispatch: # on button click permissions: diff --git a/CMakeLists.txt b/CMakeLists.txt index 797087641..cfd435714 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,7 +2,7 @@ cmake_minimum_required(VERSION 3.16) set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") -project(Z3 VERSION 4.13.3.0 LANGUAGES CXX) +project(Z3 VERSION 4.13.4.0 LANGUAGES CXX) ################################################################################ # Project version @@ -191,6 +191,8 @@ if (CMAKE_SYSTEM_NAME STREQUAL "Darwin") elseif (WIN32) message(STATUS "Platform: Windows") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS") + # workaround for #7420 + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_DISABLE_CONSTEXPR_MUTEX_CONSTRUCTOR") elseif (EMSCRIPTEN) message(STATUS "Platform: Emscripten") list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS diff --git a/README.md b/README.md index 5350bc38b..00e5acf71 100644 --- a/README.md +++ b/README.md @@ -46,7 +46,7 @@ cd build nmake ``` -Z3 uses C++17. The recommended version of Visual Studio is therefore VS2019. +Z3 uses C++20. The recommended version of Visual Studio is therefore VS2019. ## Building Z3 using make and GCC/Clang diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index c35875fed..020e34a9d 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -10,6 +10,12 @@ Version 4.next - native word level bit-vector solving. - introduction of simple induction lemmas to handle a limited repertoire of induction proofs. +Version 4.13.3 +============== +- Fixes, including #7363 +- Fix paths to Java binaries in release +- Remove internal build names from pypi wheels + Version 4.13.2 ============== - Performance regression fix. #7404 diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 545eaebe2..6399552e8 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -8,7 +8,7 @@ from mk_util import * def init_version(): - set_version(4, 13, 3, 0) # express a default build version or pick up ci build version + set_version(4, 13, 4, 0) # express a default build version or pick up ci build version # Z3 Project definition def init_project_def(): diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 0177dc564..5296e12d8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2500,7 +2500,7 @@ def mk_config(): 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, IS_ARCH_ARM64 if IS_WINDOWS: - CXXFLAGS = '/nologo /Zi /D WIN32 /D _WINDOWS /EHsc /GS /Gd /std:c++20' + CXXFLAGS = '/nologo /Zi /D WIN32 /D _WINDOWS /EHsc /GS /Gd /std:c++20 -D_DISABLE_CONSTEXPR_MUTEX_CONSTRUCTOR' config.write( 'CC=cl\n' 'CXX=cl\n' diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 74768fbea..c8dc16d62 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -1,7 +1,7 @@ variables: Major: '4' Minor: '13' - Patch: '3' + Patch: '4' ReleaseVersion: $(Major).$(Minor).$(Patch) AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId) NightlyVersion: $(AssemblyVersion)-$(Build.buildId) @@ -12,7 +12,7 @@ stages: - job: MacBuild displayName: "Mac Build" pool: - vmImage: "macOS-latest" + vmImage: "macOS-13" steps: - task: PythonScript@0 displayName: Build @@ -41,9 +41,9 @@ stages: - job: MacBuildArm64 displayName: "Mac ARM64 Build" pool: - vmImage: "macOS-latest" + vmImage: "macOS-13" steps: - - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 --os=osx-11.0 + - 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: cp dist/*.zip $(Build.ArtifactStagingDirectory)/. - task: PublishPipelineArtifact@1 diff --git a/scripts/release.yml b/scripts/release.yml index 148adc26b..435c92935 100644 --- a/scripts/release.yml +++ b/scripts/release.yml @@ -6,7 +6,7 @@ trigger: none variables: - ReleaseVersion: '4.13.3' + ReleaseVersion: '4.13.4' stages: @@ -17,7 +17,7 @@ stages: - job: MacBuild displayName: "Mac Build" pool: - vmImage: "macOS-latest" + vmImage: "macOS-13" steps: - task: PythonScript@0 displayName: Build @@ -46,9 +46,9 @@ stages: - job: MacBuildArm64 displayName: "Mac ARM64 Build" pool: - vmImage: "macOS-latest" + vmImage: "macOS-13" steps: - - script: python scripts/mk_unix_dist.py --dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64 --os=osx-11.0 + - 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: cp dist/*.zip $(Build.ArtifactStagingDirectory)/. - task: PublishPipelineArtifact@1 @@ -98,7 +98,7 @@ stages: - script: echo '##vso[task.prependpath]/tmp/arm-toolchain/aarch64-none-linux-gnu/libc/usr/bin' - script: echo $PATH - script: stat /tmp/arm-toolchain/bin/aarch64-none-linux-gnu-gcc - - script: python scripts/mk_unix_dist.py --nodotnet --nojava --arch=arm64 + - script: python scripts/mk_unix_dist.py --nodotnet --arch=arm64 - task: CopyFiles@2 inputs: sourceFolder: dist diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index 891ed4105..3bc06de16 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -148,6 +148,28 @@ namespace Microsoft.Z3 Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject); } } + + /// + /// Assert a constraint into the optimize solver, and track it (in the unsat) core + /// using the Boolean constant p. + /// + /// + /// This API is an alternative to with assumptions for extracting unsat cores. + /// Both APIs can be used in the same solver. The unsat core will contain a combination + /// of the Boolean variables provided using + /// and the Boolean literals + /// provided using with assumptions. + /// + public void AssertAndTrack(BoolExpr constraint, BoolExpr p) + { + Debug.Assert(constraint != null); + Debug.Assert(p != null); + Context.CheckContextMatch(constraint); + Context.CheckContextMatch(p); + + Native.Z3_optimize_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject); + } + /// /// Handle to objectives returned by objective functions. /// diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 0869dbd7b..2c69848c3 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -178,6 +178,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel { ctxs.forEach(other => assert('ctx' in other ? ctx === other.ctx : ctx === other, 'Context mismatch')); } + function _assertPtr(ptr: T | null): asserts ptr is T { + if (ptr == null) throw new TypeError('Expected non-null pointer'); + } + // call this after every nontrivial call to the underlying API function throwIfError() { if (Z3.get_error_code(contextPtr) !== Z3_error_code.Z3_OK) { @@ -1203,7 +1207,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { const myAst = this.ast; Z3.inc_ref(contextPtr, myAst); - cleanup.register(this, () => Z3.dec_ref(contextPtr, myAst)); + cleanup.register(this, () => Z3.dec_ref(contextPtr, myAst), this); } get ast(): Z3_ast { @@ -1240,8 +1244,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { class SolverImpl implements Solver { declare readonly __typename: Solver['__typename']; - readonly ptr: Z3_solver; readonly ctx: Context; + private _ptr: Z3_solver | null; + get ptr(): Z3_solver { + _assertPtr(this._ptr); + return this._ptr; + } constructor(ptr: Z3_solver | string = Z3.mk_solver(contextPtr)) { this.ctx = ctx; @@ -1251,9 +1259,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } else { myPtr = ptr; } - this.ptr = myPtr; + this._ptr = myPtr; Z3.solver_inc_ref(contextPtr, myPtr); - cleanup.register(this, () => Z3.solver_dec_ref(contextPtr, myPtr)); + cleanup.register(this, () => Z3.solver_dec_ref(contextPtr, myPtr), this); } set(key: string, value: any): void { @@ -1327,21 +1335,32 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.solver_from_string(contextPtr, this.ptr, s); throwIfError(); } + + release() { + Z3.solver_dec_ref(contextPtr, this.ptr); + // Mark the ptr as null to prevent double free + this._ptr = null; + cleanup.unregister(this); + } } class OptimizeImpl implements Optimize { declare readonly __typename: Optimize['__typename']; - readonly ptr: Z3_optimize; readonly ctx: Context; + private _ptr: Z3_optimize | null; + get ptr(): Z3_optimize { + _assertPtr(this._ptr); + return this._ptr; + } constructor(ptr: Z3_optimize = Z3.mk_optimize(contextPtr)) { this.ctx = ctx; let myPtr: Z3_optimize; myPtr = ptr; - this.ptr = myPtr; + this._ptr = myPtr; Z3.optimize_inc_ref(contextPtr, myPtr); - cleanup.register(this, () => Z3.optimize_dec_ref(contextPtr, myPtr)); + cleanup.register(this, () => Z3.optimize_dec_ref(contextPtr, myPtr), this); } set(key: string, value: any): void { @@ -1363,11 +1382,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel { }); } - addSoft(expr: Bool, weight: number | bigint | string | CoercibleRational, id: number | string = "") { + addSoft(expr: Bool, weight: number | bigint | string | CoercibleRational, id: number | string = '') { if (isCoercibleRational(weight)) { weight = `${weight.numerator}/${weight.denominator}`; } - check(Z3.optimize_assert_soft(contextPtr, this.ptr, expr.ast, weight.toString(), _toSymbol(id))) + check(Z3.optimize_assert_soft(contextPtr, this.ptr, expr.ast, weight.toString(), _toSymbol(id))); } addAndTrack(expr: Bool, constant: Bool | string) { @@ -1395,9 +1414,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { _assertContext(expr); return expr.ast; }); - const result = await asyncMutex.runExclusive(() => - check(Z3.optimize_check(contextPtr, this.ptr, assumptions)), - ); + const result = await asyncMutex.runExclusive(() => check(Z3.optimize_check(contextPtr, this.ptr, assumptions))); switch (result) { case Z3_lbool.Z3_L_FALSE: return 'unsat'; @@ -1422,17 +1439,28 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Z3.optimize_from_string(contextPtr, this.ptr, s); throwIfError(); } - } + release() { + Z3.optimize_dec_ref(contextPtr, this.ptr); + this._ptr = null; + cleanup.unregister(this); + } + } class ModelImpl implements Model { declare readonly __typename: Model['__typename']; readonly ctx: Context; + private _ptr: Z3_model | null; + get ptr(): Z3_model { + _assertPtr(this._ptr); + return this._ptr; + } - constructor(readonly ptr: Z3_model = Z3.mk_model(contextPtr)) { + constructor(ptr: Z3_model = Z3.mk_model(contextPtr)) { this.ctx = ctx; + this._ptr = ptr; Z3.model_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.model_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.model_dec_ref(contextPtr, ptr), this); } length() { @@ -1594,6 +1622,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { _assertContext(sort); return new AstVectorImpl(check(Z3.model_get_sort_universe(contextPtr, this.ptr, sort.ptr))); } + + release() { + Z3.model_dec_ref(contextPtr, this.ptr); + this._ptr = null; + cleanup.unregister(this); + } } class FuncEntryImpl implements FuncEntry { @@ -1604,7 +1638,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_func_entry) { this.ctx = ctx; Z3.func_entry_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.func_entry_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.func_entry_dec_ref(contextPtr, ptr), this); } numArgs() { @@ -1627,7 +1661,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_func_interp) { this.ctx = ctx; Z3.func_interp_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.func_interp_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.func_interp_dec_ref(contextPtr, ptr), this); } elseValue(): Expr { @@ -1922,7 +1956,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { this.ptr = myPtr; Z3.tactic_inc_ref(contextPtr, myPtr); - cleanup.register(this, () => Z3.tactic_dec_ref(contextPtr, myPtr)); + cleanup.register(this, () => Z3.tactic_dec_ref(contextPtr, myPtr), this); } } @@ -2586,7 +2620,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_ast_vector = Z3.mk_ast_vector(contextPtr)) { this.ctx = ctx; Z3.ast_vector_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.ast_vector_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.ast_vector_dec_ref(contextPtr, ptr), this); } length(): number { @@ -2684,7 +2718,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(readonly ptr: Z3_ast_map = Z3.mk_ast_map(contextPtr)) { this.ctx = ctx; Z3.ast_map_inc_ref(contextPtr, ptr); - cleanup.register(this, () => Z3.ast_map_dec_ref(contextPtr, ptr)); + cleanup.register(this, () => Z3.ast_map_dec_ref(contextPtr, ptr), this); } [Symbol.iterator](): Iterator<[Key, Value]> { diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 6f3630a6d..45a06bda6 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -663,6 +663,13 @@ export interface Solver { check(...exprs: (Bool | AstVector>)[]): Promise; model(): Model; + + /** + * Manually decrease the reference count of the solver + * This is automatically done when the solver is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } export interface Optimize { @@ -695,8 +702,14 @@ export interface Optimize { check(...exprs: (Bool | AstVector>)[]): Promise; model(): Model; -} + /** + * Manually decrease the reference count of the optimize + * This is automatically done when the optimize is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; +} /** @hidden */ export interface ModelCtor { @@ -746,6 +759,13 @@ export interface Model extends Iterable, defaultValue: CoercibleToMap, Name>, ): FuncInterp; + + /** + * Manually decrease the reference count of the model + * This is automatically done when the model is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; } /** diff --git a/src/api/python/setup.py b/src/api/python/setup.py index 11ba42cf8..c39cdd6b0 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -250,10 +250,25 @@ class sdist(_sdist): self.execute(_copy_sources, (), msg="Copying source files") _sdist.run(self) +# The Azure Dev Ops pipelines use internal OS version tagging that don't correspond +# to releases. + +internal_build_re = re.compile("(.+)\_7") + class bdist_wheel(_bdist_wheel): + + def remove_build_machine_os_version(self, platform, os_version_tag): + if platform in ["osx", "darwin", "sequoia"]: + m = internal_build_re.search(os_version_tag) + if m: + return m.group(1) + "_0" + return os_version_tag + + def finalize_options(self): if BUILD_ARCH is not None and BUILD_PLATFORM is not None: os_version_tag = '_'.join(BUILD_OS_VERSION[:2]) if BUILD_OS_VERSION is not None else 'xxxxxx' + os_version_tag = self.remove_build_machine_os_version(BUILD_PLATFORM, os_version_tag) TAGS = { # linux tags cannot be deployed - they must be auditwheel'd to pick the right compatibility tag based on imported libc symbol versions ("linux", "x86_64"): "linux_x86_64", diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 5c2a35995..38538509c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1073,6 +1073,13 @@ class ExprRef(AstRef): _z3_assert(is_app(self), "Z3 application expected") return FuncDeclRef(Z3_get_app_decl(self.ctx_ref(), self.as_ast()), self.ctx) + def kind(self): + """Return the Z3 internal kind of a function application.""" + if z3_debug(): + _z3_assert(is_app(self), "Z3 application expected") + return Z3_get_decl_kind(self.ctx_ref(), Z3_get_app_decl(self.ctx_ref(), self.ast)) + + def num_args(self): """Return the number of arguments of a Z3 application. @@ -1393,7 +1400,7 @@ def is_app_of(a, k): >>> is_app_of(n, Z3_OP_MUL) False """ - return is_app(a) and a.decl().kind() == k + return is_app(a) and a.kind() == k def If(a, b, c, ctx=None): @@ -9447,7 +9454,7 @@ _ROUNDING_MODES = frozenset({ def set_default_rounding_mode(rm, ctx=None): global _dflt_rounding_mode if is_fprm_value(rm): - _dflt_rounding_mode = rm.decl().kind() + _dflt_rounding_mode = rm.kind() else: _z3_assert(_dflt_rounding_mode in _ROUNDING_MODES, "illegal rounding mode") _dflt_rounding_mode = rm diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 7b54f76a1..20241536f 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -2785,9 +2785,16 @@ br_status bv_rewriter::mk_eq_bv2int(expr* lhs, expr* rhs, expr_ref& result) { result = m.mk_false(); return BR_REWRITE1; } - if (m_util.is_bv2int(lhs, x) && m_util.is_bv2int(rhs, y)) { + if (m_util.is_bv2int(lhs, x) && + m_util.is_bv2int(rhs, y)) { + auto szx = m_util.get_bv_size(x); + auto szy = m_util.get_bv_size(y); + if (szx < szy) + x = m_util.mk_zero_extend(szy - szx, x); + else if (szx > szy) + y = m_util.mk_zero_extend(szx - szy, y); result = m.mk_eq(x, y); - return BR_REWRITE1; + return BR_REWRITE2; } return BR_FAILED; } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 7e39931f4..216f23e93 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -4541,6 +4541,15 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { result = m_br.mk_eq_rw(a, b_s); return BR_REWRITE_FULL; } + expr* c = nullptr, *d = nullptr, *e = nullptr; + if (re().is_concat(b, c, d) && re().is_to_re(c, e) && re().is_full_seq(d)) { + result = str().mk_prefix(e, a); + return BR_REWRITE1; + } + if (re().is_concat(b, c, d) && re().is_to_re(d, e) && re().is_full_seq(c)) { + result = str().mk_suffix(e, a); + return BR_REWRITE1; + } expr* b1 = nullptr; expr* eps = nullptr; if (re().is_opt(b, b1) || diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp index 47ebea525..6905e0967 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.cpp +++ b/src/ast/simplifiers/model_reconstruction_trail.cpp @@ -20,6 +20,19 @@ Author: #include "ast/converters/generic_model_converter.h" +void model_reconstruction_trail::add_vars(expr* e, ast_mark& free_vars) { + for (expr* t : subterms::all(expr_ref(e, m))) { + if (is_app(t) && is_uninterp(t)) { + func_decl* f = to_app(t)->get_decl(); + TRACE("simplifier", tout << "add var " << f->get_name() << "\n"); + free_vars.mark(f, true); + if (m_model_vars.is_marked(f)) + m_intersects_with_model = true; + } + } +} + + // accumulate a set of dependent exprs, updating m_trail to exclude loose // substitutions that use variables from the dependent expressions. @@ -27,6 +40,8 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt if (m_trail.empty()) return; + if (qhead == st.qtail()) + return; ast_mark free_vars; m_intersects_with_model = false; @@ -46,7 +61,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt return; for (auto& t : m_trail) { - TRACE("simplifier", tout << " active " << t->m_active << " hide " << t->is_hide() << " intersects " << t->intersects(free_vars) << "\n"); + TRACE("simplifier", tout << " active " << t->m_active << " hide " << t->is_hide() << " intersects " << t->intersects(free_vars) << " loose " << t->is_loose() << "\n"); if (!t->m_active) continue; @@ -59,9 +74,24 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt // loose entries that intersect with free vars are deleted from the trail // and their removed formulas are added to the resulting constraints. - if (t->is_loose()) { + + if (t->is_loose() && !t->is_def() && t->is_subst()) { + for (auto const& [k, v] : t->m_subst->sub()) { + add_vars(v, free_vars); + st.add(dependent_expr(m, m.mk_eq(k, v), nullptr, nullptr)); + } + t->m_active = false; + continue; + } + + bool all_const = true; + for (auto const& [d, def, dep] : t->m_defs) + all_const &= d->get_arity() == 0; + + if (t->is_loose() && (!t->is_def() || !all_const || t->is_subst())) { for (auto r : t->m_removed) { add_vars(r, free_vars); + TRACE("simplifier", tout << "replay removed " << r << "\n"); st.add(r); } m_trail_stack.push(value_trail(t->m_active)); @@ -101,6 +131,12 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt assumptions[i] = g; // ignore dep. } + if (t->is_loose()) { + SASSERT(all_const); + SASSERT(!t->is_subst()); + for (auto const& [d, def, dep] : t->m_defs) + st.add(dependent_expr(m, m.mk_eq(m.mk_const(d), def), nullptr, nullptr)); + } continue; } @@ -141,6 +177,8 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt // ignore dep. } } + + TRACE("simplifier", st.display(tout)); } /** diff --git a/src/ast/simplifiers/model_reconstruction_trail.h b/src/ast/simplifiers/model_reconstruction_trail.h index c2d8b0001..02271c6b4 100644 --- a/src/ast/simplifiers/model_reconstruction_trail.h +++ b/src/ast/simplifiers/model_reconstruction_trail.h @@ -112,16 +112,7 @@ class model_reconstruction_trail { * record if there is an intersection with the model_vars that are * registered when updates are added to the trail. */ - void add_vars(expr* e, ast_mark& free_vars) { - for (expr* t : subterms::all(expr_ref(e, m))) - if (is_app(t) && is_uninterp(t)) { - func_decl* f = to_app(t)->get_decl(); - TRACE("simplifier", tout << "add var " << f->get_name() << "\n"); - free_vars.mark(f, true); - if (m_model_vars.is_marked(f)) - m_intersects_with_model = true; - } - } + void add_vars(expr* e, ast_mark& free_vars); void add_vars(dependent_expr const& d, ast_mark& free_vars) { add_vars(d.fml(), free_vars); diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp index 5473271ff..ecd8a1716 100644 --- a/src/ast/sls/sat_ddfw.cpp +++ b/src/ast/sls/sat_ddfw.cpp @@ -186,6 +186,38 @@ namespace sat { m_unsat.remove(m_clauses.size()); } + void ddfw::add(solver const& s) { + set_seed(s.get_config().m_random_seed); + for (auto& ci : m_clauses) + m_alloc.del_clause(ci.m_clause); + m_clauses.reset(); + m_use_list.reset(); + m_num_non_binary_clauses = 0; + + unsigned trail_sz = s.init_trail_size(); + for (unsigned i = 0; i < trail_sz; ++i) { + add(1, s.m_trail.data() + i); + } + unsigned sz = s.m_watches.size(); + for (unsigned l_idx = 0; l_idx < sz; ++l_idx) { + literal l1 = ~to_literal(l_idx); + watch_list const & wlist = s.m_watches[l_idx]; + for (watched const& w : wlist) { + if (!w.is_binary_non_learned_clause()) + continue; + literal l2 = w.get_literal(); + if (l1.index() > l2.index()) + continue; + literal ls[2] = { l1, l2 }; + add(2, ls); + } + } + for (clause* c : s.m_clauses) { + add(c->size(), c->begin()); + } + m_num_non_binary_clauses = s.m_clauses.size(); + } + void ddfw::add_assumptions() { for (unsigned i = 0; i < m_assumptions.size(); ++i) add(1, m_assumptions.data() + i); diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index f343be94d..4dfb0f8bb 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -225,7 +225,9 @@ class psort_app : public psort { sort * a = m_args[i]->instantiate(m, n, s); args_i.push_back(a); } - r = m_decl->instantiate(m, args_i.size(), args_i.data()); + r = m_decl->instantiate(m, args_i.size(), args_i.data()); + if (m_num_params != n) + throw default_exception("mismatch between number of declared and supplied sort parameters"); cache(m, s, r); return r; } @@ -771,6 +773,7 @@ bool pdatatypes_decl::commit(pdecl_manager& m) { for (unsigned i = 0; i < d->get_num_params(); ++i) { ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, nullptr)); } + dts.m_buffer.push_back(d->instantiate_decl(m, ps.size(), ps.data())); } sort_ref_vector sorts(m.m()); diff --git a/src/params/context_params.cpp b/src/params/context_params.cpp index 1d5d10b39..a5c907208 100644 --- a/src/params/context_params.cpp +++ b/src/params/context_params.cpp @@ -202,7 +202,7 @@ bool context_params::is_shell_only_parameter(char const* _p) const { std::string p(_p); lower_case(p); if (p == "dump_models" || p == "well_sorted_check" || - p == "model_validate" || p == "smtlib2_compliant" || + p == "model_validate" || p == "stats") return true; diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 82bda1d39..ccbefa69e 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -134,7 +134,7 @@ namespace smt { dst = tr(unit_trail.get(j)); pctx.assert_expr(dst); } - unit_lim[i] = sz; + unit_lim[i] = pctx.assigned_literals().size(); } IF_VERBOSE(1, verbose_stream() << "(smt.thread :units " << sz << ")\n"); }; @@ -149,7 +149,7 @@ namespace smt { expr_ref c(pm); pctx.get_fparams().m_max_conflicts = std::min(thread_max_conflicts, max_conflicts); - if (num_rounds > 0 && (pctx.get_fparams().m_threads_cube_frequency % num_rounds) == 0) + if (num_rounds > 0 && (num_rounds % pctx.get_fparams().m_threads_cube_frequency) == 0) cube(pctx, lasms, c); IF_VERBOSE(1, verbose_stream() << "(smt.thread " << i; if (num_rounds > 0) verbose_stream() << " :round " << num_rounds; diff --git a/src/solver/simplifier_solver.cpp b/src/solver/simplifier_solver.cpp index ae1d6b8a2..b114f364f 100644 --- a/src/solver/simplifier_solver.cpp +++ b/src/solver/simplifier_solver.cpp @@ -130,6 +130,10 @@ class simplifier_solver : public solver { unsigned qhead = m_preprocess_state.qhead(); expr_ref_vector orig_assumptions(assumptions); m_core_replace.reset(); + m_preprocess_state.replay(qhead, assumptions); + for (unsigned i = 0; i < assumptions.size(); ++i) + m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i)); + if (qhead < m_fmls.size()) { m_preprocess.reduce(); if (!m.inc()) @@ -138,11 +142,7 @@ class simplifier_solver : public solver { m_preprocess_state.display(tout)); m_preprocess_state.advance_qhead(); } - if (!assumptions.empty()) { - m_preprocess_state.replay(m_preprocess_state.qhead(), assumptions); - for (unsigned i = 0; i < assumptions.size(); ++i) - m_core_replace.insert(assumptions.get(i), orig_assumptions.get(i)); - } + m_mc = m_preprocess_state.model_trail().get_model_converter(); m_cached_mc = nullptr; for (; qhead < m_fmls.size(); ++qhead) diff --git a/src/solver/slice_solver.cpp b/src/solver/slice_solver.cpp index 7c4e1fb82..28815b4d6 100644 --- a/src/solver/slice_solver.cpp +++ b/src/solver/slice_solver.cpp @@ -373,7 +373,7 @@ public: lbool check_sat_cc(expr_ref_vector const& cube, vector const& clauses) override { flush(); - return check_sat_cc(cube, clauses); + return s->check_sat_cc(cube, clauses); } lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override {