mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

Merge branch 'master' into sls

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-11-02 10:41:15 -07:00
parent c7ec2afedb ecdfab81a6
commit 7875c95866
23 changed files with 246 additions and 62 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/docker-image.yml vendored
View file

@ -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:

4
CMakeLists.txt
View file

@ -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

2
README.md
View file

@ -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

6
RELEASE_NOTES.md
View file

@ -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

2
scripts/mk_project.py
View file

@ -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():

2
scripts/mk_util.py
View file

@ -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'

8
scripts/nightly.yaml
View file

@ -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

10
scripts/release.yml
View file

@ -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

22
src/api/dotnet/Optimize.cs
View file

@ -148,6 +148,28 @@ namespace Microsoft.Z3
Native.Z3_optimize_assert(Context.nCtx, NativeObject, a.NativeObject);
}
}
/// <summary>
/// Assert a constraint into the optimize solver, and track it (in the unsat) core
/// using the Boolean constant p.
/// </summary>
/// <remarks>
/// This API is an alternative to <see cref="Check(Expr[])"/> 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 <see cref="AssertAndTrack(BoolExpr[],BoolExpr[])"/>
/// and the Boolean literals
/// provided using <see cref="Check(Expr[])"/> with assumptions.
/// </remarks>
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);
}
/// <summary>
/// Handle to objectives returned by objective functions.
/// </summary>

74
src/api/js/src/high-level/high-level.ts
View file

@ -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<T extends Number>(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<Name> {
declare readonly __typename: Solver['__typename'];
readonly ptr: Z3_solver;
readonly ctx: Context<Name>;
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<Name> {
declare readonly __typename: Optimize['__typename'];
readonly ptr: Z3_optimize;
readonly ctx: Context<Name>;
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<Name>, weight: number | bigint | string | CoercibleRational, id: number | string = "") {
addSoft(expr: Bool<Name>, 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<Name>, constant: Bool<Name> | 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<Name> {
declare readonly __typename: Model['__typename'];
readonly ctx: Context<Name>;
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<Name> {
@ -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<Name> {
@ -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]> {

22
src/api/js/src/high-level/types.ts
View file

@ -663,6 +663,13 @@ export interface Solver<Name extends string = 'main'> {
check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>;
model(): Model<Name>;
/**
* 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<Name extends string = 'main'> {
@ -695,8 +702,14 @@ export interface Optimize<Name extends string = 'main'> {
check(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): Promise<CheckSatResult>;
model(): Model<Name>;
}
/**
* 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<Name extends string> {
@ -746,6 +759,13 @@ export interface Model<Name extends string = 'main'> extends Iterable<FuncDecl<N
decl: FuncDecl<Name, DomainSort, RangeSort>,
defaultValue: CoercibleToMap<SortToExprMap<RangeSort, Name>, Name>,
): FuncInterp<Name>;
/**
* 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;
}
/**

15
src/api/python/setup.py
View file

@ -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",

11
src/api/python/z3/z3.py
View file

@ -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

11
src/ast/rewriter/bv_rewriter.cpp
View file

@ -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;
}

9
src/ast/rewriter/seq_rewriter.cpp
View file

@ -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) ||

42
src/ast/simplifiers/model_reconstruction_trail.cpp
View file

@ -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));
}
/**

11
src/ast/simplifiers/model_reconstruction_trail.h
View file

@ -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);

32
src/ast/sls/sat_ddfw.cpp
View file

@ -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);

5
src/cmd_context/pdecl.cpp
View file

@ -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());

2
src/params/context_params.cpp
View file

@ -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;

4
src/smt/smt_parallel.cpp
View file

@ -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;

10
src/solver/simplifier_solver.cpp
View file

@ -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)

2
src/solver/slice_solver.cpp
View file

@ -373,7 +373,7 @@ public:
lbool check_sat_cc(expr_ref_vector const& cube, vector<expr_ref_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<expr_ref_vector>& mutexes) override {