mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 02:16:16 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-07-21 23:22:37 -07:00
commit 87dd837b55
6 changed files with 14 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
CMakeLists.txt
View file

@ -2,7 +2,7 @@
cmake_minimum_required(VERSION 3.4) cmake_minimum_required(VERSION 3.4)
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake") set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
project(Z3 VERSION 4.9.2.0 LANGUAGES CXX) project(Z3 VERSION 4.10.0.0 LANGUAGES CXX)
################################################################################ ################################################################################
# Project version # Project version

2
scripts/mk_project.py
View file

@ -8,7 +8,7 @@
from mk_util import * from mk_util import *
def init_version(): def init_version():
set_version(4, 9, 2, 0) set_version(4, 10, 0, 0)
# Z3 Project definition # Z3 Project definition
def init_project_def(): def init_project_def():

4
scripts/nightly.yaml
View file

@ -1,8 +1,8 @@
variables: variables:
Major: '4' Major: '4'
Minor: '9' Minor: '10'
Patch: '2' Patch: '0'
NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName) NightlyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)-$(Build.DefinitionName)
stages: stages:

2
scripts/release.yml
View file

@ -6,7 +6,7 @@
trigger: none trigger: none
variables: variables:
ReleaseVersion: '4.9.2' ReleaseVersion: '4.10.0'
stages: stages:

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

@ -1050,6 +1050,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
return check(Z3.model_to_string(contextPtr, this.ptr)); return check(Z3.model_to_string(contextPtr, this.ptr));
} }
toString() {
return this.sexpr();
}
eval(expr: Bool<Name>, modelCompletion?: boolean): Bool<Name>; eval(expr: Bool<Name>, modelCompletion?: boolean): Bool<Name>;
eval(expr: Arith<Name>, modelCompletion?: boolean): Arith<Name>; eval(expr: Arith<Name>, modelCompletion?: boolean): Arith<Name>;
eval(expr: Expr<Name>, modelCompletion: boolean = false) { eval(expr: Expr<Name>, modelCompletion: boolean = false) {

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

@ -204,12 +204,13 @@ class Context:
Z3_set_param_value(conf, str(prev), _to_param_value(a)) Z3_set_param_value(conf, str(prev), _to_param_value(a))
prev = None prev = None
self.ctx = Z3_mk_context_rc(conf) self.ctx = Z3_mk_context_rc(conf)
self.owner = True
self.eh = Z3_set_error_handler(self.ctx, z3_error_handler) self.eh = Z3_set_error_handler(self.ctx, z3_error_handler)
Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT) Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
Z3_del_config(conf) Z3_del_config(conf)
def __del__(self): def __del__(self):
if Z3_del_context is not None: if Z3_del_context is not None and self.owner:
Z3_del_context(self.ctx) Z3_del_context(self.ctx)
self.ctx = None self.ctx = None
self.eh = None self.eh = None
@ -11367,12 +11368,14 @@ def user_prop_fresh(ctx, new_ctx):
_prop_closures.set_threaded() _prop_closures.set_threaded()
prop = _prop_closures.get(ctx) prop = _prop_closures.get(ctx)
nctx = Context() nctx = Context()
Z3_del_context(nctx.ctx)
new_ctx = to_ContextObj(new_ctx) new_ctx = to_ContextObj(new_ctx)
nctx.ctx = new_ctx nctx.ctx = new_ctx
nctx.eh = Z3_set_error_handler(new_ctx, z3_error_handler) nctx.eh = Z3_set_error_handler(new_ctx, z3_error_handler)
nctx.owner = False
new_prop = prop.fresh(nctx) new_prop = prop.fresh(nctx)
_prop_closures.set(new_prop.id, new_prop) _prop_closures.set(new_prop.id, new_prop)
return ctypes.c_void_p(new_prop.id) return new_prop.id
def to_Ast(ptr,): def to_Ast(ptr,):
ast = Ast(ptr) ast = Ast(ptr)