mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-22 20:39:11 +00:00
Code Activity

Merge branch 'master' into nl2lin

Browse source 
# Conflicts:
#	src/math/lp/nla_coi.cpp
#	src/math/lp/nla_coi.h
#	src/math/lp/nla_core.cpp
#	src/math/lp/nla_grobner.cpp
#	src/math/lp/nla_grobner.h
#	src/math/lp/nla_pp.cpp
#	src/math/lp/nra_solver.cpp
#	src/nlsat/nlsat_explain.h
#	src/smt/theory_lra.cpp
This commit is contained in:
Lev Nachmanson 2025-12-16 11:47:13 -10:00
commit a6f44f8c88
373 changed files with 31824 additions and 22376 deletions
Download patch file Download diff file Expand all files Collapse all files

108
src/CMakeLists.txt
View file

@ -1,29 +1,3 @@
################################################################################
# API header files
################################################################################
# This lists the API header files that are scanned by
# some of the build rules to generate some files needed
# by the build
set(Z3_API_HEADER_FILES_TO_SCAN
z3_api.h
z3_ast_containers.h
z3_algebraic.h
z3_polynomial.h
z3_rcf.h
z3_fixedpoint.h
z3_optimization.h
z3_fpa.h
z3_spacer.h
)
set(Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "")
foreach (header_file ${Z3_API_HEADER_FILES_TO_SCAN})
set(full_path_api_header_file "${CMAKE_CURRENT_SOURCE_DIR}/api/${header_file}")
list(APPEND Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "${full_path_api_header_file}")
if (NOT EXISTS "${full_path_api_header_file}")
message(FATAL_ERROR "API header file \"${full_path_api_header_file}\" does not exist")
endif()
endforeach()
################################################################################
# Traverse directories each adding a Z3 component
################################################################################
@ -39,7 +13,6 @@ add_subdirectory(math/polynomial)
add_subdirectory(math/dd)
add_subdirectory(math/hilbert)
add_subdirectory(math/simplex)
add_subdirectory(math/automata)
add_subdirectory(math/interval)
add_subdirectory(math/realclosure)
add_subdirectory(math/subpaving)
@ -153,6 +126,16 @@ set_target_properties(libz3 PROPERTIES
VERSION ${Z3_VERSION}
SOVERSION ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR})
# Set macOS-specific properties for proper .dylib versioning (fixes issue #6651)
if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
set_target_properties(libz3 PROPERTIES
# Use @rpath for install name to make library relocatable
INSTALL_NAME_DIR "@rpath"
# Enable RPATH support
MACOSX_RPATH TRUE
)
endif()
if (NOT MSVC)
# On UNIX like platforms if we don't change the OUTPUT_NAME
# the library gets a name like ``liblibz3.so`` so we change it
@ -168,6 +151,60 @@ endif()
# so that if those are also shared libraries they are referenced by `libz3.so`.
target_link_libraries(libz3 PRIVATE ${Z3_DEPENDENT_LIBS})
################################################################################
# Create include directory with headers for easier developer integration
################################################################################
set(Z3_BUILD_INCLUDE_DIR "${CMAKE_BINARY_DIR}/include")
file(MAKE_DIRECTORY "${Z3_BUILD_INCLUDE_DIR}")
# Copy Z3 API headers to build include directory
set(Z3_API_HEADERS
api/z3.h
api/z3_api.h
api/z3_algebraic.h
api/z3_ast_containers.h
api/z3_fixedpoint.h
api/z3_fpa.h
api/z3_logger.h
api/z3_macros.h
api/z3_optimization.h
api/z3_polynomial.h
api/z3_private.h
api/z3_rcf.h
api/z3_replayer.h
api/z3_spacer.h
api/z3_v1.h
api/c++/z3++.h
)
# Create custom target to copy headers
#add_custom_target(z3_headers_copy ALL
# COMMENT "Copying Z3 API headers to build include directory"
#)
#
#foreach(header_file ${Z3_API_HEADERS})
# get_filename_component(header_name "${header_file}" NAME)
# set(src_file "${CMAKE_CURRENT_SOURCE_DIR}/${header_file}")
# set(dst_file "${Z3_BUILD_INCLUDE_DIR}/${header_name}")
#
# add_custom_command(
# TARGET z3_headers_copy POST_BUILD
# COMMAND ${CMAKE_COMMAND} -E copy_if_different
# "${src_file}"
# "${dst_file}"
# COMMENT "Copying ${header_name} to include directory"
# VERBATIM
# )
#endforeach()
# Make libz3 depend on header copying
#add_dependencies(libz3 z3_headers_copy)
# Update libz3 to also expose the build include directory
target_include_directories(libz3 INTERFACE
$<BUILD_INTERFACE:${Z3_BUILD_INCLUDE_DIR}>
)
# This is currently only for the OpenMP flags. It needs to be set
# via `target_link_libraries()` rather than `z3_append_linker_flag_list_to_target()`
# because when building the `libz3` as a static library when the target is exported
@ -242,7 +279,7 @@ endif()
################################################################################
cmake_dependent_option(Z3_BUILD_EXECUTABLE
"Build the z3 executable" ON
"CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR" OFF)
"CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR;Z3_BUILD_LIBZ3_CORE" OFF)
if (Z3_BUILD_EXECUTABLE)
add_subdirectory(shell)
@ -254,26 +291,13 @@ endif()
cmake_dependent_option(Z3_BUILD_TEST_EXECUTABLES
"Build test executables" ON
"CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR" OFF)
"CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR;Z3_BUILD_LIBZ3_CORE" OFF)
if (Z3_BUILD_TEST_EXECUTABLES)
add_subdirectory(test)
endif()
################################################################################
# Z3 API bindings
################################################################################
option(Z3_BUILD_PYTHON_BINDINGS "Build Python bindings for Z3" OFF)
if (Z3_BUILD_PYTHON_BINDINGS)
if (NOT Z3_BUILD_LIBZ3_SHARED)
message(FATAL_ERROR "The python bindings will not work with a static libz3. "
"You either need to disable Z3_BUILD_PYTHON_BINDINGS or enable Z3_BUILD_LIBZ3_SHARED")
endif()
add_subdirectory(api/python)
endif()
################################################################################
# .NET bindings
################################################################################

7
src/api/api_arith.cpp
View file

@ -156,8 +156,15 @@ extern "C" {
}
bool Z3_API Z3_is_algebraic_number(Z3_context c, Z3_ast a) {
Z3_TRY;
LOG_Z3_is_algebraic_number(c, a);
RESET_ERROR_CODE();
if (!is_expr(a)) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return false;
}
return mk_c(c)->autil().is_irrational_algebraic_numeral(to_expr(a));
Z3_CATCH_RETURN(false);
}
Z3_ast Z3_API Z3_get_algebraic_number_lower(Z3_context c, Z3_ast a, unsigned precision) {

1
src/api/api_array.cpp
View file

@ -268,7 +268,6 @@ extern "C" {
MK_UNARY(Z3_mk_set_complement, mk_c(c)->get_array_fid(), OP_SET_COMPLEMENT, SKIP);
MK_BINARY(Z3_mk_set_subset, mk_c(c)->get_array_fid(), OP_SET_SUBSET, SKIP);
MK_BINARY(Z3_mk_array_ext, mk_c(c)->get_array_fid(), OP_ARRAY_EXT, SKIP);
MK_BINARY(Z3_mk_set_has_size, mk_c(c)->get_array_fid(), OP_SET_HAS_SIZE, SKIP);
Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f) {
Z3_TRY;

12
src/api/api_ast.cpp
View file

@ -225,13 +225,15 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_fresh_func_decl(c, prefix, domain_size, domain, range);
RESET_ERROR_CODE();
CHECK_IS_SORT(range, nullptr);
CHECK_SORTS(domain_size, domain, nullptr);
if (prefix == nullptr) {
prefix = "";
}
func_decl* d = mk_c(c)->m().mk_fresh_func_decl(prefix,
domain_size,
reinterpret_cast<sort*const*>(domain),
to_sorts(domain),
to_sort(range), false);
mk_c(c)->save_ast_trail(d);
@ -243,9 +245,11 @@ extern "C" {
Z3_TRY;
LOG_Z3_mk_fresh_const(c, prefix, ty);
RESET_ERROR_CODE();
CHECK_IS_SORT(ty, nullptr);
if (prefix == nullptr) {
prefix = "";
}
app* a = mk_c(c)->m().mk_fresh_const(prefix, to_sort(ty), false);
mk_c(c)->save_ast_trail(a);
RETURN_Z3(of_ast(a));
@ -654,6 +658,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_sort_name(c, t);
RESET_ERROR_CODE();
CHECK_IS_SORT(t, of_symbol(symbol::null));
CHECK_VALID_AST(t, of_symbol(symbol::null));
return of_symbol(to_sort(t)->get_name());
Z3_CATCH_RETURN(of_symbol(symbol::null));
@ -795,12 +800,11 @@ extern "C" {
unsigned timeout = p.get_uint("timeout", mk_c(c)->get_timeout());
bool use_ctrl_c = p.get_bool("ctrl_c", false);
th_rewriter m_rw(m, p);
m_rw.set_solver(alloc(api::seq_expr_solver, m, p));
expr_ref result(m);
cancel_eh<reslimit> eh(m.limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_ctrl_c ctrlc(eh, use_ctrl_c);
scoped_timer timer(timeout, &eh);
try {
m_rw(a, result);
@ -1188,8 +1192,6 @@ extern "C" {
case OP_SET_SUBSET: return Z3_OP_SET_SUBSET;
case OP_AS_ARRAY: return Z3_OP_AS_ARRAY;
case OP_ARRAY_EXT: return Z3_OP_ARRAY_EXT;
case OP_SET_CARD: return Z3_OP_SET_CARD;
case OP_SET_HAS_SIZE: return Z3_OP_SET_HAS_SIZE;
default:
return Z3_OP_INTERNAL;
}

28
src/api/api_context.h
View file

@ -57,23 +57,6 @@ namespace smt2 {
namespace api {
class seq_expr_solver : public expr_solver {
ast_manager& m;
params_ref const& p;
solver_ref s;
public:
seq_expr_solver(ast_manager& m, params_ref const& p): m(m), p(p) {}
lbool check_sat(expr* e) override {
if (!s) {
s = mk_smt_solver(m, p, symbol("ALL"));
}
s->push();
s->assert_expr(e);
lbool r = s->check_sat();
s->pop(1);
return r;
}
};
class context : public tactic_manager {
@ -286,10 +269,13 @@ namespace api {
inline api::context * mk_c(Z3_context c) { return reinterpret_cast<api::context*>(c); }
#define RESET_ERROR_CODE() { mk_c(c)->reset_error_code(); }
#define SET_ERROR_CODE(ERR, MSG) { mk_c(c)->set_error_code(ERR, MSG); }
#define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == 0) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } }
#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } }
#define CHECK_NON_NULL(_p_,_ret_) { if (_p_ == nullptr) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is null"); return _ret_; } }
#define CHECK_VALID_AST(_a_, _ret_) { if (_a_ == nullptr || !CHECK_REF_COUNT(_a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "not a valid ast"); return _ret_; } }
inline bool is_expr(Z3_ast a) { return is_expr(to_ast(a)); }
#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == 0 || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } }
#define CHECK_IS_EXPR(_p_, _ret_) { if (_p_ == nullptr || !is_expr(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not an expression"); return _ret_; } }
#define CHECK_IS_SORT(_p_, _ret_) { if (_p_ == nullptr || !is_sort(_p_)) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not a sort"); return _ret_; } }
#define CHECK_SORTS(_n_, _ps_, _ret_) { for (unsigned i = 0; i < _n_; ++i) if (!is_sort(_ps_[i])) { SET_ERROR_CODE(Z3_INVALID_ARG, "ast is not a sort"); return _ret_; } }
inline bool is_bool_expr(Z3_context c, Z3_ast a) { return is_expr(a) && mk_c(c)->m().is_bool(to_expr(a)); }
#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == 0 || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } }
#define CHECK_FORMULA(_a_, _ret_) { if (_a_ == nullptr || !CHECK_REF_COUNT(_a_) || !is_bool_expr(c, _a_)) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return _ret_; } }
inline void check_sorts(Z3_context c, ast * n) { mk_c(c)->check_sorts(n); }

2
src/api/api_datalog.cpp
View file

@ -287,7 +287,7 @@ extern "C" {
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
api::context::set_interruptable si(*(mk_c(c)), eh);
scoped_timer timer(timeout, &eh);
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_ctrl_c ctrlc(eh, use_ctrl_c);
try {
r = to_fixedpoint_ref(d)->ctx().query(to_expr(q));
}

74
src/api/api_datatype.cpp
View file

@ -306,12 +306,24 @@ extern "C" {
Z3_CATCH;
}
static datatype_decl* mk_datatype_decl(Z3_context c,
Z3_symbol name,
unsigned num_constructors,
Z3_constructor constructors[]) {
static datatype_decl* api_datatype_decl(Z3_context c,
Z3_symbol name,
unsigned num_parameters,
Z3_sort const parameters[],
unsigned num_constructors,
Z3_constructor constructors[]) {
datatype_util& dt_util = mk_c(c)->dtutil();
ast_manager& m = mk_c(c)->m();
sort_ref_vector params(m);
// A correct use of the API is to always provide parameters explicitly.
// implicit parameters through polymorphic type variables does not work
// because the order of polymorphic variables in the parameters is ambiguous.
if (num_parameters > 0 && parameters)
for (unsigned i = 0; i < num_parameters; ++i)
params.push_back(to_sort(parameters[i]));
ptr_vector<constructor_decl> constrs;
for (unsigned i = 0; i < num_constructors; ++i) {
constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
@ -326,7 +338,7 @@ extern "C" {
}
constrs.push_back(mk_constructor_decl(cn->m_name, cn->m_tester, acc.size(), acc.data()));
}
return mk_datatype_decl(dt_util, to_symbol(name), 0, nullptr, num_constructors, constrs.data());
return mk_datatype_decl(dt_util, to_symbol(name), params.size(), params.data(), num_constructors, constrs.data());
}
Z3_sort Z3_API Z3_mk_datatype(Z3_context c,
@ -341,7 +353,7 @@ extern "C" {
sort_ref_vector sorts(m);
{
datatype_decl * data = mk_datatype_decl(c, name, num_constructors, constructors);
datatype_decl * data = api_datatype_decl(c, name, 0, nullptr, num_constructors, constructors);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, nullptr, sorts);
del_datatype_decl(data);
@ -363,6 +375,42 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c,
Z3_symbol name,
unsigned num_parameters,
Z3_sort parameters[],
unsigned num_constructors,
Z3_constructor constructors[]) {
Z3_TRY;
LOG_Z3_mk_polymorphic_datatype(c, name, num_parameters, parameters, num_constructors, constructors);
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
datatype_util data_util(m);
sort_ref_vector sorts(m);
{
datatype_decl * data = api_datatype_decl(c, name, num_parameters, parameters, num_constructors, constructors);
bool is_ok = mk_c(c)->get_dt_plugin()->mk_datatypes(1, &data, 0, nullptr, sorts);
del_datatype_decl(data);
if (!is_ok) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
RETURN_Z3(nullptr);
}
}
sort * s = sorts.get(0);
mk_c(c)->save_ast_trail(s);
ptr_vector<func_decl> const& cnstrs = *data_util.get_datatype_constructors(s);
for (unsigned i = 0; i < num_constructors; ++i) {
constructor* cn = reinterpret_cast<constructor*>(constructors[i]);
cn->m_constructor = cnstrs[i];
}
RETURN_Z3_mk_polymorphic_datatype(of_sort(s));
Z3_CATCH_RETURN(nullptr);
}
typedef ptr_vector<constructor> constructor_list;
Z3_constructor_list Z3_API Z3_mk_constructor_list(Z3_context c,
@ -387,14 +435,18 @@ extern "C" {
Z3_CATCH;
}
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name) {
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[]) {
Z3_TRY;
LOG_Z3_mk_datatype_sort(c, name);
LOG_Z3_mk_datatype_sort(c, name, num_params, params);
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
datatype_util adt_util(m);
parameter p(to_symbol(name));
sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, 1, &p);
vector<parameter> ps;
ps.push_back(parameter(to_symbol(name)));
for (unsigned i = 0; i < num_params; ++i) {
ps.push_back(parameter(to_sort(params[i])));
}
sort * s = m.mk_sort(adt_util.get_family_id(), DATATYPE_SORT, ps.size(), ps.data());
mk_c(c)->save_ast_trail(s);
RETURN_Z3(of_sort(s));
Z3_CATCH_RETURN(nullptr);
@ -416,7 +468,7 @@ extern "C" {
ptr_vector<datatype_decl> datas;
for (unsigned i = 0; i < num_sorts; ++i) {
constructor_list* cl = reinterpret_cast<constructor_list*>(constructor_lists[i]);
datas.push_back(mk_datatype_decl(c, sort_names[i], cl->size(), reinterpret_cast<Z3_constructor*>(cl->data())));
datas.push_back(api_datatype_decl(c, sort_names[i], 0, nullptr, cl->size(), reinterpret_cast<Z3_constructor*>(cl->data())));
}
sort_ref_vector _sorts(m);
bool ok = mk_c(c)->get_dt_plugin()->mk_datatypes(datas.size(), datas.data(), 0, nullptr, _sorts);

16
src/api/api_fpa.cpp
View file

@ -896,7 +896,7 @@ extern "C" {
Z3_CATCH_RETURN(0);
}
bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn) {
bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, bool * sgn) {
Z3_TRY;
LOG_Z3_fpa_get_numeral_sign(c, t, sgn);
RESET_ERROR_CODE();
@ -1224,6 +1224,20 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
bool Z3_API Z3_fpa_is_numeral(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_is_numeral(c, t);
RESET_ERROR_CODE();
api::context * ctx = mk_c(c);
fpa_util & fu = ctx->fpautil();
if (!is_expr(t)) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
return false;
}
return fu.is_numeral(to_expr(t));
Z3_CATCH_RETURN(false);
}
bool Z3_API Z3_fpa_is_numeral_nan(Z3_context c, Z3_ast t) {
Z3_TRY;
LOG_Z3_fpa_is_numeral_nan(c, t);

3
src/api/api_model.cpp
View file

@ -160,9 +160,6 @@ extern "C" {
model * _m = to_model_ref(m);
params_ref p;
ast_manager& mgr = mk_c(c)->m();
if (!_m->has_solver()) {
_m->set_solver(alloc(api::seq_expr_solver, mgr, p));
}
expr_ref result(mgr);
model::scoped_model_completion _scm(*_m, model_completion);
result = (*_m)(to_expr(t));

20
src/api/api_opt.cpp
View file

@ -154,7 +154,7 @@ extern "C" {
bool use_ctrl_c = to_optimize_ptr(o)->get_params().get_bool("ctrl_c", true);
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_ctrl_c ctrlc(eh, use_ctrl_c);
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
@ -481,4 +481,22 @@ extern "C" {
Z3_CATCH;
}
Z3_optimize Z3_API Z3_optimize_translate(Z3_context c, Z3_optimize o, Z3_context target) {
Z3_TRY;
LOG_Z3_optimize_translate(c, o, target);
RESET_ERROR_CODE();
// Translate the opt::context to the target manager
opt::context* translated_ctx = to_optimize_ptr(o)->translate(mk_c(target)->m());
// Create a new Z3_optimize_ref in the target context
Z3_optimize_ref* result_ref = alloc(Z3_optimize_ref, *mk_c(target));
result_ref->m_opt = translated_ctx;
mk_c(target)->save_object(result_ref);
Z3_optimize result = of_optimize(result_ref);
RETURN_Z3(result);
Z3_CATCH_RETURN(nullptr);
}
};

2
src/api/api_rcf.cpp
View file

@ -385,7 +385,7 @@ extern "C" {
Z3_CATCH_RETURN(nullptr);
}
int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, int * lower_is_inf, int * lower_is_open, Z3_rcf_num * lower, int * upper_is_inf, int * upper_is_open, Z3_rcf_num * upper) {
int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, bool * lower_is_inf, bool * lower_is_open, Z3_rcf_num * lower, bool * upper_is_inf, bool * upper_is_open, Z3_rcf_num * upper) {
Z3_TRY;
LOG_Z3_rcf_interval(c, a, lower_is_inf, lower_is_open, lower, upper_is_inf, upper_is_open, upper);
RESET_ERROR_CODE();

3
src/api/api_seq.cpp
View file

@ -293,6 +293,9 @@ extern "C" {
MK_TERNARY(Z3_mk_seq_extract, mk_c(c)->get_seq_fid(), OP_SEQ_EXTRACT, SKIP);
MK_TERNARY(Z3_mk_seq_replace, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE, SKIP);
MK_TERNARY(Z3_mk_seq_replace_all, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE_ALL, SKIP);
MK_TERNARY(Z3_mk_seq_replace_re, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE_RE, SKIP);
MK_TERNARY(Z3_mk_seq_replace_re_all, mk_c(c)->get_seq_fid(), OP_SEQ_REPLACE_RE_ALL, SKIP);
MK_BINARY(Z3_mk_seq_at, mk_c(c)->get_seq_fid(), OP_SEQ_AT, SKIP);
MK_BINARY(Z3_mk_seq_nth, mk_c(c)->get_seq_fid(), OP_SEQ_NTH, SKIP);
MK_UNARY(Z3_mk_seq_length, mk_c(c)->get_seq_fid(), OP_SEQ_LENGTH, SKIP);

24
src/api/api_solver.cpp
View file

@ -146,6 +146,8 @@ extern "C" {
bool proofs_enabled = true, models_enabled = true, unsat_core_enabled = false;
params_ref p = s->m_params;
mk_c(c)->params().get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled);
if (!s->m_solver_factory)
s->m_solver_factory = mk_smt_solver_factory();
s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic);
param_descrs r;
@ -274,7 +276,11 @@ extern "C" {
LOG_Z3_solver_translate(c, s, target);
RESET_ERROR_CODE();
params_ref const& p = to_solver(s)->m_params;
Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(target), (solver_factory *)nullptr);
solver_factory* translated_factory = nullptr;
if (to_solver(s)->m_solver_factory.get()) {
translated_factory = to_solver(s)->m_solver_factory->translate(mk_c(target)->m());
}
Z3_solver_ref * sr = alloc(Z3_solver_ref, *mk_c(target), translated_factory);
init_solver(c, s);
sr->m_solver = to_solver(s)->m_solver->translate(mk_c(target)->m(), p);
mk_c(target)->save_object(sr);
@ -650,7 +656,7 @@ extern "C" {
api::context::set_interruptable si(*(mk_c(c)), eh);
lbool result = l_undef;
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_ctrl_c ctrlc(eh, use_ctrl_c);
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
@ -748,7 +754,7 @@ extern "C" {
cancel_eh<reslimit> eh(mk_c(c)->m().limit());
to_solver(s)->set_eh(&eh);
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_ctrl_c ctrlc(eh, use_ctrl_c);
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
@ -871,7 +877,7 @@ extern "C" {
to_solver(s)->set_eh(&eh);
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_ctrl_c ctrlc(eh, use_ctrl_c);
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
@ -919,7 +925,7 @@ extern "C" {
to_solver(s)->set_eh(&eh);
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_ctrl_c ctrlc(eh, use_ctrl_c);
scoped_timer timer(timeout, &eh);
scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
try {
@ -1160,6 +1166,14 @@ extern "C" {
Z3_CATCH;
}
void Z3_API Z3_solver_propagate_on_binding(Z3_context c, Z3_solver s, Z3_on_binding_eh binding_eh) {
Z3_TRY;
RESET_ERROR_CODE();
user_propagator::binding_eh_t c = (bool(*)(void*, user_propagator::callback*, expr*, expr*))binding_eh;
to_solver_ref(s)->user_propagate_register_on_binding(c);
Z3_CATCH;
}
bool Z3_API Z3_solver_next_split(Z3_context c, Z3_solver_callback cb, Z3_ast t, unsigned idx, Z3_lbool phase) {
Z3_TRY;
LOG_Z3_solver_next_split(c, cb, t, idx, phase);

2
src/api/api_tactic.cpp
View file

@ -427,7 +427,7 @@ extern "C" {
api::context::set_interruptable si(*(mk_c(c)), eh);
{
scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
scoped_ctrl_c ctrlc(eh, use_ctrl_c);
scoped_timer timer(timeout, &eh);
try {
exec(*to_tactic_ref(t), new_goal, ref->m_subgoals);

1
src/api/api_util.h
View file

@ -67,6 +67,7 @@ inline ast * const * to_asts(Z3_ast const* a) { return reinterpret_cast<ast* con
inline sort * to_sort(Z3_sort a) { return reinterpret_cast<sort*>(a); }
inline Z3_sort of_sort(sort* s) { return reinterpret_cast<Z3_sort>(s); }
inline bool is_sort(Z3_sort a) { return is_sort(to_sort(a)); }
inline sort * const * to_sorts(Z3_sort const* a) { return reinterpret_cast<sort* const*>(a); }
inline Z3_sort const * of_sorts(sort* const* s) { return reinterpret_cast<Z3_sort const*>(s); }

70
src/api/c++/z3++.h
View file

@ -327,6 +327,15 @@ namespace z3 {
*/
sort datatype(symbol const& name, constructors const& cs);
/**
\brief Create a parametric recursive datatype.
\c name is the name of the recursive datatype
\c params - the sort parameters of the datatype
\c cs - the \c n constructors used to define the datatype
References to the datatype and mutually recursive datatypes can be created using \ref datatype_sort.
*/
sort datatype(symbol const &name, sort_vector const &params, constructors const &cs);
/**
\brief Create a set of mutually recursive datatypes.
\c n - number of recursive datatypes
@ -343,6 +352,14 @@ namespace z3 {
*/
sort datatype_sort(symbol const& name);
/**
\brief a reference to a recursively defined parametric datatype.
Expect that it gets defined as a \ref datatype.
\param name name of the datatype
\param params sort parameters
*/
sort datatype_sort(symbol const& name, sort_vector const& params);
/**
\brief create an uninterpreted sort with the name given by the string or symbol.
@ -2173,7 +2190,15 @@ namespace z3 {
inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
/**
\brief signed division operator for bitvectors.
*/
inline expr sdiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsdiv(a.ctx(), a, b)); }
inline expr sdiv(expr const & a, int b) { return sdiv(a, a.ctx().num_val(b, a.get_sort())); }
inline expr sdiv(int a, expr const & b) { return sdiv(b.ctx().num_val(a, b.get_sort()), b); }
/**
\brief unsigned division operator for bitvectors.
*/
inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }
@ -3288,6 +3313,7 @@ namespace z3 {
Z3_optimize m_opt;
public:
struct translate {};
class handle final {
unsigned m_h;
public:
@ -3295,6 +3321,12 @@ namespace z3 {
unsigned h() const { return m_h; }
};
optimize(context& c):object(c) { m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt); }
optimize(context & c, optimize const& src, translate): object(c) {
Z3_optimize o = Z3_optimize_translate(src.ctx(), src, c);
check_error();
m_opt = o;
Z3_optimize_inc_ref(c, m_opt);
}
optimize(optimize const & o):object(o), m_opt(o.m_opt) {
Z3_optimize_inc_ref(o.ctx(), o.m_opt);
}
@ -3600,6 +3632,16 @@ namespace z3 {
return sort(*this, s);
}
inline sort context::datatype(symbol const &name, sort_vector const& params, constructors const &cs) {
array<Z3_sort> _params(params);
array<Z3_constructor> _cs(cs.size());
for (unsigned i = 0; i < cs.size(); ++i)
_cs[i] = cs[i];
Z3_sort s = Z3_mk_polymorphic_datatype(*this, name, _params.size(), _params.ptr(), cs.size(), _cs.ptr());
check_error();
return sort(*this, s);
}
inline sort_vector context::datatypes(
unsigned n, symbol const* names,
constructor_list *const* cons) {
@ -3617,7 +3659,14 @@ namespace z3 {
inline sort context::datatype_sort(symbol const& name) {
Z3_sort s = Z3_mk_datatype_sort(*this, name);
Z3_sort s = Z3_mk_datatype_sort(*this, name, 0, nullptr);
check_error();
return sort(*this, s);
}
inline sort context::datatype_sort(symbol const& name, sort_vector const& params) {
array<Z3_sort> _params(params);
Z3_sort s = Z3_mk_datatype_sort(*this, name, _params.size(), _params.ptr());
check_error();
return sort(*this, s);
}
@ -4295,12 +4344,14 @@ namespace z3 {
typedef std::function<void(expr const&, expr const&)> eq_eh_t;
typedef std::function<void(expr const&)> created_eh_t;
typedef std::function<void(expr, unsigned, bool)> decide_eh_t;
typedef std::function<bool(expr const&, expr const&)> on_binding_eh_t;
final_eh_t m_final_eh;
eq_eh_t m_eq_eh;
fixed_eh_t m_fixed_eh;
created_eh_t m_created_eh;
decide_eh_t m_decide_eh;
on_binding_eh_t m_on_binding_eh;
solver* s;
context* c;
std::vector<z3::context*> subcontexts;
@ -4372,6 +4423,13 @@ namespace z3 {
expr val(p->ctx(), _val);
p->m_decide_eh(val, bit, is_pos);
}
static bool on_binding_eh(void* _p, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst) {
user_propagator_base* p = static_cast<user_propagator_base*>(_p);
scoped_cb _cb(p, cb);
expr q(p->ctx(), _q), inst(p->ctx(), _inst);
return p->m_on_binding_eh(q, inst);
}
public:
user_propagator_base(context& c) : s(nullptr), c(&c) {}
@ -4498,6 +4556,14 @@ namespace z3 {
}
}
void register_on_binding() {
m_on_binding_eh = [this](expr const& q, expr const& inst) {
return on_binding(q, inst);
};
if (s)
Z3_solver_propagate_on_binding(ctx(), *s, on_binding_eh);
}
virtual void fixed(expr const& /*id*/, expr const& /*e*/) { }
virtual void eq(expr const& /*x*/, expr const& /*y*/) { }
@ -4508,6 +4574,8 @@ namespace z3 {
virtual void decide(expr const& /*val*/, unsigned /*bit*/, bool /*is_pos*/) {}
virtual bool on_binding(expr const& /*q*/, expr const& /*inst*/) { return true; }
bool next_split(expr const& e, unsigned idx, Z3_lbool phase) {
assert(cb);
return Z3_solver_next_split(ctx(), cb, e, idx, phase);

147
src/api/dotnet/Context.cs
View file

@ -474,6 +474,36 @@ namespace Microsoft.Z3
return new DatatypeSort(this, symbol, constructors);
}
/// <summary>
/// Create a forward reference to a datatype sort.
/// This is useful for creating recursive datatypes or parametric datatypes.
/// </summary>
/// <param name="name">name of the datatype sort</param>
/// <param name="parameters">optional array of sort parameters for parametric datatypes</param>
public DatatypeSort MkDatatypeSortRef(Symbol name, Sort[] parameters = null)
{
Debug.Assert(name != null);
CheckContextMatch(name);
if (parameters != null)
CheckContextMatch<Sort>(parameters);
var numParams = (parameters == null) ? 0 : (uint)parameters.Length;
var paramsNative = (parameters == null) ? null : AST.ArrayToNative(parameters);
return new DatatypeSort(this, Native.Z3_mk_datatype_sort(nCtx, name.NativeObject, numParams, paramsNative));
}
/// <summary>
/// Create a forward reference to a datatype sort.
/// This is useful for creating recursive datatypes or parametric datatypes.
/// </summary>
/// <param name="name">name of the datatype sort</param>
/// <param name="parameters">optional array of sort parameters for parametric datatypes</param>
public DatatypeSort MkDatatypeSortRef(string name, Sort[] parameters = null)
{
using var symbol = MkSymbol(name);
return MkDatatypeSortRef(symbol, parameters);
}
/// <summary>
/// Create mutually recursive datatypes.
/// </summary>
@ -867,7 +897,6 @@ namespace Microsoft.Z3
{
Debug.Assert(f != null);
Debug.Assert(args == null || args.All(a => a != null));
CheckContextMatch(f);
CheckContextMatch<Expr>(args);
return Expr.Create(this, f, args);
@ -879,11 +908,7 @@ namespace Microsoft.Z3
public Expr MkApp(FuncDecl f, IEnumerable<Expr> args)
{
Debug.Assert(f != null);
Debug.Assert(args == null || args.All(a => a != null));
CheckContextMatch(f);
CheckContextMatch(args);
return Expr.Create(this, f, args.ToArray());
return MkApp(f, args?.ToArray());
}
#region Propositional
@ -892,7 +917,6 @@ namespace Microsoft.Z3
/// </summary>
public BoolExpr MkTrue()
{
return new BoolExpr(this, Native.Z3_mk_true(nCtx));
}
@ -901,7 +925,6 @@ namespace Microsoft.Z3
/// </summary>
public BoolExpr MkFalse()
{
return new BoolExpr(this, Native.Z3_mk_false(nCtx));
}
@ -910,7 +933,6 @@ namespace Microsoft.Z3
/// </summary>
public BoolExpr MkBool(bool value)
{
return value ? MkTrue() : MkFalse();
}
@ -935,7 +957,6 @@ namespace Microsoft.Z3
Debug.Assert(args != null);
Debug.Assert(args.All(a => a != null));
CheckContextMatch<Expr>(args);
return new BoolExpr(this, Native.Z3_mk_distinct(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
}
@ -955,7 +976,6 @@ namespace Microsoft.Z3
public BoolExpr MkNot(BoolExpr a)
{
Debug.Assert(a != null);
CheckContextMatch(a);
return new BoolExpr(this, Native.Z3_mk_not(nCtx, a.NativeObject));
}
@ -1020,9 +1040,10 @@ namespace Microsoft.Z3
/// <summary>
/// Create an expression representing <c>t1 xor t2 xor t3 ... </c>.
/// </summary>
public BoolExpr MkXor(IEnumerable<BoolExpr> ts)
public BoolExpr MkXor(IEnumerable<BoolExpr> args)
{
Debug.Assert(ts != null);
Debug.Assert(args != null);
var ts = args.ToArray();
Debug.Assert(ts.All(a => a != null));
CheckContextMatch<BoolExpr>(ts);
@ -1036,13 +1057,13 @@ namespace Microsoft.Z3
/// <summary>
/// Create an expression representing <c>t[0] and t[1] and ...</c>.
/// </summary>
public BoolExpr MkAnd(params BoolExpr[] t)
public BoolExpr MkAnd(params BoolExpr[] ts)
{
Debug.Assert(t != null);
Debug.Assert(t.All(a => a != null));
Debug.Assert(ts != null);
Debug.Assert(ts.All(a => a != null));
CheckContextMatch<BoolExpr>(t);
return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
CheckContextMatch<BoolExpr>(ts);
return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
}
/// <summary>
@ -1051,102 +1072,86 @@ namespace Microsoft.Z3
public BoolExpr MkAnd(IEnumerable<BoolExpr> t)
{
Debug.Assert(t != null);
Debug.Assert(t.All(a => a != null));
CheckContextMatch<BoolExpr>(t);
var ands = t.ToArray();
return new BoolExpr(this, Native.Z3_mk_and(nCtx, (uint)t.Count(), AST.ArrayToNative(ands)));
return MkAnd(t.ToArray());
}
/// <summary>
/// Create an expression representing <c>t[0] or t[1] or ...</c>.
/// </summary>
public BoolExpr MkOr(params BoolExpr[] t)
public BoolExpr MkOr(params BoolExpr[] ts)
{
Debug.Assert(t != null);
Debug.Assert(t.All(a => a != null));
Debug.Assert(ts != null);
Debug.Assert(ts.All(a => a != null));
CheckContextMatch<BoolExpr>(t);
return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
}
/// <summary>
/// Create an expression representing <c>t[0] or t[1] or ...</c>.
/// </summary>
public BoolExpr MkOr(IEnumerable<BoolExpr> t)
{
Debug.Assert(t != null);
Debug.Assert(t.All(a => a != null));
CheckContextMatch(t);
var ts = t.ToArray();
CheckContextMatch<BoolExpr>(ts);
return new BoolExpr(this, Native.Z3_mk_or(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
}
/// <summary>
/// Create an expression representing <c>t[0] or t[1] or ...</c>.
/// </summary>
public BoolExpr MkOr(IEnumerable<BoolExpr> ts)
{
Debug.Assert(ts != null);
return MkOr(ts.ToArray());
}
#endregion
#region Arithmetic
/// <summary>
/// Create an expression representing <c>t[0] + t[1] + ...</c>.
/// </summary>
public ArithExpr MkAdd(params ArithExpr[] t)
public ArithExpr MkAdd(params ArithExpr[] ts)
{
Debug.Assert(t != null);
Debug.Assert(t.All(a => a != null));
Debug.Assert(ts != null);
Debug.Assert(ts.All(a => a != null));
CheckContextMatch<ArithExpr>(t);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
CheckContextMatch<ArithExpr>(ts);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
}
/// <summary>
/// Create an expression representing <c>t[0] + t[1] + ...</c>.
/// </summary>
public ArithExpr MkAdd(IEnumerable<ArithExpr> t)
public ArithExpr MkAdd(IEnumerable<ArithExpr> ts)
{
Debug.Assert(t != null);
Debug.Assert(t.All(a => a != null));
CheckContextMatch(t);
var ts = t.ToArray();
return (ArithExpr)Expr.Create(this, Native.Z3_mk_add(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
Debug.Assert(ts != null);
return MkAdd(ts.ToArray());
}
/// <summary>
/// Create an expression representing <c>t[0] * t[1] * ...</c>.
/// </summary>
public ArithExpr MkMul(params ArithExpr[] t)
public ArithExpr MkMul(params ArithExpr[] ts)
{
Debug.Assert(t != null);
Debug.Assert(t.All(a => a != null));
Debug.Assert(ts != null);
Debug.Assert(ts.All(a => a != null));
CheckContextMatch<ArithExpr>(t);
var ts = t.ToArray();
CheckContextMatch<ArithExpr>(ts);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
}
/// <summary>
/// Create an expression representing <c>t[0] * t[1] * ...</c>.
/// </summary>
public ArithExpr MkMul(IEnumerable<ArithExpr> t)
public ArithExpr MkMul(IEnumerable<ArithExpr> ts)
{
Debug.Assert(t != null);
Debug.Assert(t.All(a => a != null));
CheckContextMatch<ArithExpr>(t);
var ts = t.ToArray();
return (ArithExpr)Expr.Create(this, Native.Z3_mk_mul(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
Debug.Assert(ts != null);
return MkMul(ts.ToArray());
}
/// <summary>
/// Create an expression representing <c>t[0] - t[1] - ...</c>.
/// </summary>
public ArithExpr MkSub(params ArithExpr[] t)
public ArithExpr MkSub(params ArithExpr[] ts)
{
Debug.Assert(t != null);
Debug.Assert(t.All(a => a != null));
Debug.Assert(ts != null);
Debug.Assert(ts.All(a => a != null));
CheckContextMatch<ArithExpr>(t);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)t.Length, AST.ArrayToNative(t)));
CheckContextMatch<ArithExpr>(ts);
return (ArithExpr)Expr.Create(this, Native.Z3_mk_sub(nCtx, (uint)ts.Length, AST.ArrayToNative(ts)));
}
/// <summary>
@ -2843,8 +2848,8 @@ namespace Microsoft.Z3
public BoolExpr MkAtMost(IEnumerable<BoolExpr> args, uint k)
{
Debug.Assert(args != null);
CheckContextMatch<BoolExpr>(args);
var ts = args.ToArray();
CheckContextMatch<BoolExpr>(ts);
return new BoolExpr(this, Native.Z3_mk_atmost(nCtx, (uint)ts.Length,
AST.ArrayToNative(ts), k));
}
@ -2855,8 +2860,8 @@ namespace Microsoft.Z3
public BoolExpr MkAtLeast(IEnumerable<BoolExpr> args, uint k)
{
Debug.Assert(args != null);
CheckContextMatch<BoolExpr>(args);
var ts = args.ToArray();
CheckContextMatch<BoolExpr>(ts);
return new BoolExpr(this, Native.Z3_mk_atleast(nCtx, (uint)ts.Length,
AST.ArrayToNative(ts), k));
}

4
src/api/dotnet/FPNum.cs
View file

@ -50,8 +50,8 @@ namespace Microsoft.Z3
{
get
{
int res = 0;
if (Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res) == 0)
byte res = 0;
if (0 == Native.Z3_fpa_get_numeral_sign(Context.nCtx, NativeObject, ref res))
throw new Z3Exception("Sign is not a Boolean value");
return res != 0;
}

2
src/api/dotnet/Log.cs
View file

@ -41,7 +41,7 @@ namespace Microsoft.Z3
public static bool Open(string filename)
{
m_is_open = true;
return Native.Z3_open_log(filename) == 1;
return 0 != Native.Z3_open_log(filename);
}
/// <summary>

41
src/api/dotnet/UserPropagator.cs
View file

@ -64,7 +64,15 @@ namespace Microsoft.Z3
/// <param name="idx">If the term is a bit-vector, then an index into the bit-vector being branched on</param>
/// <param name="phase">The tentative truth-value</param>
public delegate void DecideEh(Expr term, uint idx, bool phase);
/// <summary>
/// Delegate type for callback when a quantifier is bound to an instance.
/// </summary>
/// <param name="q">Quantifier</param>
/// <param name="inst">Instance</param>
/// <returns>true if binding is allowed to take effect in the solver, false if blocked by callback</returns>
public delegate bool OnBindingEh(Expr q, Expr inst);
// access managed objects through a static array.
// thread safety is ignored for now.
GCHandle gch;
@ -78,6 +86,7 @@ namespace Microsoft.Z3
EqEh diseq_eh;
CreatedEh created_eh;
DecideEh decide_eh;
OnBindingEh on_binding_eh;
Native.Z3_push_eh push_eh;
Native.Z3_pop_eh pop_eh;
@ -89,6 +98,7 @@ namespace Microsoft.Z3
Native.Z3_eq_eh diseq_wrapper;
Native.Z3_decide_eh decide_wrapper;
Native.Z3_created_eh created_wrapper;
Native.Z3_on_binding_eh on_binding_wrapper;
void Callback(Action fn, Z3_solver_callback cb)
{
@ -175,6 +185,19 @@ namespace Microsoft.Z3
prop.Callback(() => prop.decide_eh(t, idx, phase), cb);
}
static bool _on_binding(voidp _ctx, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst)
{
var prop = (UserPropagator)GCHandle.FromIntPtr(_ctx).Target;
using var q = Expr.Create(prop.ctx, _q);
using var inst = Expr.Create(prop.ctx, _inst);
bool result = true;
prop.Callback(() => {
if (prop.on_binding_wrapper != null)
result = prop.on_binding_eh(q, inst);
}, cb);
return result;
}
/// <summary>
/// Propagator constructor from a solver class.
/// </summary>
@ -362,6 +385,20 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Set binding callback
/// </summary>
public OnBindingEh OnBinding
{
set
{
this.on_binding_wrapper = _on_binding;
this.on_binding_eh = value;
if (solver != null)
Native.Z3_solver_propagate_on_binding(ctx.nCtx, solver.NativeObject, on_binding_wrapper);
}
}
/// <summary>
/// Set the next decision
@ -378,6 +415,8 @@ namespace Microsoft.Z3
return Native.Z3_solver_next_split(ctx.nCtx, this.callback, e?.NativeObject ?? IntPtr.Zero, idx, phase) != 0;
}
/// <summary>
/// Track assignments to a term
/// </summary>

8
src/api/java/AST.java
View file

@ -208,7 +208,13 @@ public class AST extends Z3Object implements Comparable<AST>
case Z3_FUNC_DECL_AST:
return new FuncDecl<>(ctx, obj);
case Z3_QUANTIFIER_AST:
return new Quantifier(ctx, obj);
// a quantifier AST is a lambda iff it is neither a forall nor an exists.
boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj);
if (isLambda) {
return new Lambda(ctx, obj);
} else {
return new Quantifier(ctx, obj);
}
case Z3_SORT_AST:
return Sort.create(ctx, obj);
case Z3_APP_AST:

86
src/api/java/Context.java
View file

@ -388,6 +388,54 @@ public class Context implements AutoCloseable {
return new DatatypeSort<>(this, mkSymbol(name), constructors);
}
/**
* Create a forward reference to a datatype sort.
* This is useful for creating recursive datatypes or parametric datatypes.
* @param name name of the datatype sort
* @param params optional array of sort parameters for parametric datatypes
**/
public <R> DatatypeSort<R> mkDatatypeSortRef(Symbol name, Sort[] params)
{
checkContextMatch(name);
if (params != null)
checkContextMatch(params);
int numParams = (params == null) ? 0 : params.length;
long[] paramsNative = (params == null) ? new long[0] : AST.arrayToNative(params);
return new DatatypeSort<>(this, Native.mkDatatypeSort(nCtx(), name.getNativeObject(), numParams, paramsNative));
}
/**
* Create a forward reference to a datatype sort (non-parametric).
* This is useful for creating recursive datatypes.
* @param name name of the datatype sort
**/
public <R> DatatypeSort<R> mkDatatypeSortRef(Symbol name)
{
return mkDatatypeSortRef(name, null);
}
/**
* Create a forward reference to a datatype sort.
* This is useful for creating recursive datatypes or parametric datatypes.
* @param name name of the datatype sort
* @param params optional array of sort parameters for parametric datatypes
**/
public <R> DatatypeSort<R> mkDatatypeSortRef(String name, Sort[] params)
{
return mkDatatypeSortRef(mkSymbol(name), params);
}
/**
* Create a forward reference to a datatype sort (non-parametric).
* This is useful for creating recursive datatypes.
* @param name name of the datatype sort
**/
public <R> DatatypeSort<R> mkDatatypeSortRef(String name)
{
return mkDatatypeSortRef(name, null);
}
/**
* Create mutually recursive datatypes.
* @param names names of datatype sorts
@ -2032,7 +2080,7 @@ public class Context implements AutoCloseable {
public SeqExpr<CharSort> mkString(String s)
{
StringBuilder buf = new StringBuilder();
for (int i = 0; i < s.length(); ++i) {
for (int i = 0; i < s.length(); i += Character.charCount(s.codePointAt(i))) {
int code = s.codePointAt(i);
if (code <= 32 || 127 < code)
buf.append(String.format("\\u{%x}", code));
@ -2178,6 +2226,15 @@ public class Context implements AutoCloseable {
return (IntExpr)Expr.create(this, Native.mkSeqIndex(nCtx(), s.getNativeObject(), substr.getNativeObject(), offset.getNativeObject()));
}
/**
* Extract the last index of sub-string.
*/
public final <R extends Sort> IntExpr mkLastIndexOf(Expr<SeqSort<R>> s, Expr<SeqSort<R>> substr)
{
checkContextMatch(s, substr);
return (IntExpr)Expr.create(this, Native.mkSeqLastIndex(nCtx(), s.getNativeObject(), substr.getNativeObject()));
}
/**
* Replace the first occurrence of src by dst in s.
*/
@ -2187,6 +2244,33 @@ public class Context implements AutoCloseable {
return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplace(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
}
/**
* Replace all occurrences of src by dst in s.
*/
public final <R extends Sort> SeqExpr<R> mkReplaceAll(Expr<SeqSort<R>> s, Expr<SeqSort<R>> src, Expr<SeqSort<R>> dst)
{
checkContextMatch(s, src, dst);
return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplaceAll(nCtx(), s.getNativeObject(), src.getNativeObject(), dst.getNativeObject()));
}
/**
* Replace the first occurrence of regular expression re with dst in s.
*/
public final <R extends Sort> SeqExpr<R> mkReplaceRe(Expr<SeqSort<R>> s, ReExpr<SeqSort<R>> re, Expr<SeqSort<R>> dst)
{
checkContextMatch(s, re, dst);
return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplaceRe(nCtx(), s.getNativeObject(), re.getNativeObject(), dst.getNativeObject()));
}
/**
* Replace all occurrences of regular expression re with dst in s.
*/
public final <R extends Sort> SeqExpr<R> mkReplaceReAll(Expr<SeqSort<R>> s, ReExpr<SeqSort<R>> re, Expr<SeqSort<R>> dst)
{
checkContextMatch(s, re, dst);
return (SeqExpr<R>) Expr.create(this, Native.mkSeqReplaceReAll(nCtx(), s.getNativeObject(), re.getNativeObject(), dst.getNativeObject()));
}
/**
* Convert a regular expression that accepts sequence s.
*/

11
src/api/java/Expr.java
View file

@ -2148,8 +2148,15 @@ public class Expr<R extends Sort> extends AST
static Expr<?> create(Context ctx, long obj)
{
Z3_ast_kind k = Z3_ast_kind.fromInt(Native.getAstKind(ctx.nCtx(), obj));
if (k == Z3_ast_kind.Z3_QUANTIFIER_AST)
return new Quantifier(ctx, obj);
if (k == Z3_ast_kind.Z3_QUANTIFIER_AST) {
// a quantifier AST is a lambda iff it is neither a forall nor an exists.
boolean isLambda = !Native.isQuantifierExists(ctx.nCtx(), obj) && !Native.isQuantifierForall(ctx.nCtx(), obj);
if (isLambda) {
return new Lambda(ctx, obj);
} else {
return new Quantifier(ctx, obj);
}
}
long s = Native.getSort(ctx.nCtx(), obj);
Z3_sort_kind sk = Z3_sort_kind
.fromInt(Native.getSortKind(ctx.nCtx(), s));

4
src/api/java/FPNum.java
View file

@ -27,10 +27,10 @@ public class FPNum extends FPExpr
* @throws Z3Exception
*/
public boolean getSign() {
Native.IntPtr res = new Native.IntPtr();
Native.BoolPtr res = new Native.BoolPtr();
if (!Native.fpaGetNumeralSign(getContext().nCtx(), getNativeObject(), res))
throw new Z3Exception("Sign is not a Boolean value");
return res.value != 0;
return res.value;
}
/**

2
src/api/java/Lambda.java
View file

@ -126,7 +126,7 @@ public class Lambda<R extends Sort> extends ArrayExpr<Sort, R>
}
private Lambda(Context ctx, long obj)
Lambda(Context ctx, long obj)
{
super(ctx, obj);
}

2
src/api/java/Log.java
View file

@ -36,7 +36,7 @@ public final class Log
public static boolean open(String filename)
{
m_is_open = true;
return Native.openLog(filename) == 1;
return Native.openLog(filename);
}
/**

8
src/api/java/NativeStatic.txt
View file

@ -92,6 +92,7 @@ struct JavaInfo {
jmethodID eq = nullptr;
jmethodID final = nullptr;
jmethodID decide = nullptr;
jmethodID on_binding = nullptr;
Z3_solver_callback cb = nullptr;
};
@ -153,6 +154,12 @@ static void decide_eh(void* _p, Z3_solver_callback cb, Z3_ast _val, unsigned bit
info->jenv->CallVoidMethod(info->jobj, info->decide, (jlong)_val, bit, is_pos);
}
static jboolean on_binding_eh(void* _p, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst) {
JavaInfo *info = static_cast<JavaInfo*>(_p);
ScopedCB scoped(info, cb);
return info->jenv->CallBooleanMethod(info->jobj, info->on_binding, (jlong)_q, (jlong)_inst);
}
DLL_VIS JNIEXPORT jlong JNICALL Java_com_microsoft_z3_Native_propagateInit(JNIEnv *jenv, jclass cls, jobject jobj, jlong ctx, jlong solver) {
JavaInfo *info = new JavaInfo;
@ -167,6 +174,7 @@ DLL_VIS JNIEXPORT jlong JNICALL Java_com_microsoft_z3_Native_propagateInit(JNIEn
info->eq = jenv->GetMethodID(jcls, "eqWrapper", "(JJ)V");
info->final = jenv->GetMethodID(jcls, "finWrapper", "()V");
info->decide = jenv->GetMethodID(jcls, "decideWrapper", "(JIZ)V");
info->on_binding = jenv->GetMethodID(jcls, "onBindingWrapper", "(JJ)Z");
if (!info->push || !info->pop || !info->fresh || !info->created || !info->fixed || !info->eq || !info->final || !info->decide) {
assert(false);

2
src/api/java/Sort.java
View file

@ -144,6 +144,8 @@ public class Sort extends AST
return new SeqSort<>(ctx, obj);
case Z3_RE_SORT:
return new ReSort<>(ctx, obj);
case Z3_CHAR_SORT:
return new CharSort(ctx, obj);
default:
throw new Z3Exception("Unknown sort kind");
}

9
src/api/java/UserPropagatorBase.java
View file

@ -43,6 +43,13 @@ public abstract class UserPropagatorBase extends Native.UserPropagatorBase {
eq(x, y);
}
@Override
protected final boolean onBindingWrapper(long lq, long linst) {
Expr q = new Expr(ctx, lq);
Expr inst = new Expr(ctx, linst);
return on_binding(q, inst);
}
@Override
protected final UserPropagatorBase freshWrapper(long lctx) {
return fresh(new Context(lctx));
@ -77,6 +84,8 @@ public abstract class UserPropagatorBase extends Native.UserPropagatorBase {
public void fixed(Expr<?> var, Expr<?> value) {}
public void eq(Expr<?> x, Expr<?> y) {}
public boolean on_binding(Expr<?> q, Expr<?> inst) { return true; }
public void decide(Expr<?> var, int bit, boolean is_pos) {}

454
src/api/js/package-lock.json generated
View file

@ -46,12 +46,15 @@
}
},
"node_modules/@babel/code-frame": {
"version": "7.18.6",
"resolved": "https://registry.npmjs.org/@babel/code-frame/-/code-frame-7.18.6.tgz",
"integrity": "sha512-TDCmlK5eOvH+eH7cdAFlNXeVJqWIQ7gW9tY1GJIpUtFb6CmjVyq2VM3u71bOyR8CRihcCgMUYoDNyLXao3+70Q==",
"version": "7.27.1",
"resolved": "https://registry.npmjs.org/@babel/code-frame/-/code-frame-7.27.1.tgz",
"integrity": "sha512-cjQ7ZlQ0Mv3b47hABuTevyTuYN4i+loJKGeV9flcCgIK37cCXRh+L1bd3iBHlynerhQ7BhCkn2BPbQUL+rGqFg==",
"dev": true,
"license": "MIT",
"dependencies": {
"@babel/highlight": "^7.18.6"
"@babel/helper-validator-identifier": "^7.27.1",
"js-tokens": "^4.0.0",
"picocolors": "^1.1.1"
},
"engines": {
"node": ">=6.9.0"
@ -236,19 +239,21 @@
}
},
"node_modules/@babel/helper-string-parser": {
"version": "7.19.4",
"resolved": "https://registry.npmjs.org/@babel/helper-string-parser/-/helper-string-parser-7.19.4.tgz",
"integrity": "sha512-nHtDoQcuqFmwYNYPz3Rah5ph2p8PFeFCsZk9A/48dPc/rGocJ5J3hAAZ7pb76VWX3fZKu+uEr/FhH5jLx7umrw==",
"version": "7.27.1",
"resolved": "https://registry.npmjs.org/@babel/helper-string-parser/-/helper-string-parser-7.27.1.tgz",
"integrity": "sha512-qMlSxKbpRlAridDExk92nSobyDdpPijUq2DW6oDnUqd0iOGxmQjyqhMIihI9+zv4LPyZdRje2cavWPbCbWm3eA==",
"dev": true,
"license": "MIT",
"engines": {
"node": ">=6.9.0"
}
},
"node_modules/@babel/helper-validator-identifier": {
"version": "7.19.1",
"resolved": "https://registry.npmjs.org/@babel/helper-validator-identifier/-/helper-validator-identifier-7.19.1.tgz",
"integrity": "sha512-awrNfaMtnHUr653GgGEs++LlAvW6w+DcPrOliSMXWCKo597CwL5Acf/wWdNkf/tfEQE3mjkeD1YOVZOUV/od1w==",
"version": "7.28.5",
"resolved": "https://registry.npmjs.org/@babel/helper-validator-identifier/-/helper-validator-identifier-7.28.5.tgz",
"integrity": "sha512-qSs4ifwzKJSV39ucNjsvc6WVHs6b7S03sOh2OcHF9UHfVPqWWALUsNUVzhSBiItjRZoLHx7nIarVjqKVusUZ1Q==",
"dev": true,
"license": "MIT",
"engines": {
"node": ">=6.9.0"
}
@ -263,38 +268,28 @@
}
},
"node_modules/@babel/helpers": {
"version": "7.19.4",
"resolved": "https://registry.npmjs.org/@babel/helpers/-/helpers-7.19.4.tgz",
"integrity": "sha512-G+z3aOx2nfDHwX/kyVii5fJq+bgscg89/dJNWpYeKeBv3v9xX8EIabmx1k6u9LS04H7nROFVRVK+e3k0VHp+sw==",
"version": "7.28.4",
"resolved": "https://registry.npmjs.org/@babel/helpers/-/helpers-7.28.4.tgz",
"integrity": "sha512-HFN59MmQXGHVyYadKLVumYsA9dBFun/ldYxipEjzA4196jpLZd8UjEEBLkbEkvfYreDqJhZxYAWFPtrfhNpj4w==",
"dev": true,
"license": "MIT",
"dependencies": {
"@babel/template": "^7.18.10",
"@babel/traverse": "^7.19.4",
"@babel/types": "^7.19.4"
},
"engines": {
"node": ">=6.9.0"
}
},
"node_modules/@babel/highlight": {
"version": "7.18.6",
"resolved": "https://registry.npmjs.org/@babel/highlight/-/highlight-7.18.6.tgz",
"integrity": "sha512-u7stbOuYjaPezCuLj29hNW1v64M2Md2qupEKP1fHc7WdOA3DgLh37suiSrZYY7haUB7iBeQZ9P1uiRF359do3g==",
"dev": true,
"dependencies": {
"@babel/helper-validator-identifier": "^7.18.6",
"chalk": "^2.0.0",
"js-tokens": "^4.0.0"
"@babel/template": "^7.27.2",
"@babel/types": "^7.28.4"
},
"engines": {
"node": ">=6.9.0"
}
},
"node_modules/@babel/parser": {
"version": "7.19.4",
"resolved": "https://registry.npmjs.org/@babel/parser/-/parser-7.19.4.tgz",
"integrity": "sha512-qpVT7gtuOLjWeDTKLkJ6sryqLliBaFpAtGeqw5cs5giLldvh+Ch0plqnUMKoVAUS6ZEueQQiZV+p5pxtPitEsA==",
"version": "7.28.5",
"resolved": "https://registry.npmjs.org/@babel/parser/-/parser-7.28.5.tgz",
"integrity": "sha512-KKBU1VGYR7ORr3At5HAtUQ+TV3SzRCXmA/8OdDZiLDBIZxVyzXuztPjfLd3BV1PRAQGCMWWSHYhL0F8d5uHBDQ==",
"dev": true,
"license": "MIT",
"dependencies": {
"@babel/types": "^7.28.5"
},
"bin": {
"parser": "bin/babel-parser.js"
},
@ -465,26 +460,25 @@
}
},
"node_modules/@babel/runtime": {
"version": "7.19.4",
"resolved": "https://registry.npmjs.org/@babel/runtime/-/runtime-7.19.4.tgz",
"integrity": "sha512-EXpLCrk55f+cYqmHsSR+yD/0gAIMxxA9QK9lnQWzhMCvt+YmoBN7Zx94s++Kv0+unHk39vxNO8t+CMA2WSS3wA==",
"version": "7.28.4",
"resolved": "https://registry.npmjs.org/@babel/runtime/-/runtime-7.28.4.tgz",
"integrity": "sha512-Q/N6JNWvIvPnLDvjlE1OUBLPQHH6l3CltCEsHIujp45zQUSSh8K+gHnaEX45yAT1nyngnINhvWtzN+Nb9D8RAQ==",
"dev": true,
"dependencies": {
"regenerator-runtime": "^0.13.4"
},
"license": "MIT",
"engines": {
"node": ">=6.9.0"
}
},
"node_modules/@babel/template": {
"version": "7.18.10",
"resolved": "https://registry.npmjs.org/@babel/template/-/template-7.18.10.tgz",
"integrity": "sha512-TI+rCtooWHr3QJ27kJxfjutghu44DLnasDMwpDqCXVTal9RLp3RSYNh4NdBrRP2cQAoG9A8juOQl6P6oZG4JxA==",
"version": "7.27.2",
"resolved": "https://registry.npmjs.org/@babel/template/-/template-7.27.2.tgz",
"integrity": "sha512-LPDZ85aEJyYSd18/DkjNh4/y1ntkE5KwUHWTiqgRxruuZL2F1yuHligVHLvcHY2vMHXttKFpJn6LwfI7cw7ODw==",
"dev": true,
"license": "MIT",
"dependencies": {
"@babel/code-frame": "^7.18.6",
"@babel/parser": "^7.18.10",
"@babel/types": "^7.18.10"
"@babel/code-frame": "^7.27.1",
"@babel/parser": "^7.27.2",
"@babel/types": "^7.27.1"
},
"engines": {
"node": ">=6.9.0"
@ -511,19 +505,6 @@
"node": ">=6.9.0"
}
},
"node_modules/@babel/traverse/node_modules/@babel/code-frame": {
"version": "7.22.13",
"resolved": "https://registry.npmjs.org/@babel/code-frame/-/code-frame-7.22.13.tgz",
"integrity": "sha512-XktuhWlJ5g+3TJXc5upd9Ks1HutSArik6jf2eAjYFyIOf4ej3RN+184cZbzDvbPnuTJIUhPKKJE3cIsYTiAT3w==",
"dev": true,
"dependencies": {
"@babel/highlight": "^7.22.13",
"chalk": "^2.4.2"
},
"engines": {
"node": ">=6.9.0"
}
},
"node_modules/@babel/traverse/node_modules/@babel/generator": {
"version": "7.23.0",
"resolved": "https://registry.npmjs.org/@babel/generator/-/generator-7.23.0.tgz",
@ -585,78 +566,6 @@
"node": ">=6.9.0"
}
},
"node_modules/@babel/traverse/node_modules/@babel/helper-string-parser": {
"version": "7.22.5",
"resolved": "https://registry.npmjs.org/@babel/helper-string-parser/-/helper-string-parser-7.22.5.tgz",
"integrity": "sha512-mM4COjgZox8U+JcXQwPijIZLElkgEpO5rsERVDJTc2qfCDfERyob6k5WegS14SX18IIjv+XD+GrqNumY5JRCDw==",
"dev": true,
"engines": {
"node": ">=6.9.0"
}
},
"node_modules/@babel/traverse/node_modules/@babel/helper-validator-identifier": {
"version": "7.22.20",
"resolved": "https://registry.npmjs.org/@babel/helper-validator-identifier/-/helper-validator-identifier-7.22.20.tgz",
"integrity": "sha512-Y4OZ+ytlatR8AI+8KZfKuL5urKp7qey08ha31L8b3BwewJAoJamTzyvxPR/5D+KkdJCGPq/+8TukHBlY10FX9A==",
"dev": true,
"engines": {
"node": ">=6.9.0"
}
},
"node_modules/@babel/traverse/node_modules/@babel/highlight": {
"version": "7.22.20",
"resolved": "https://registry.npmjs.org/@babel/highlight/-/highlight-7.22.20.tgz",
"integrity": "sha512-dkdMCN3py0+ksCgYmGG8jKeGA/8Tk+gJwSYYlFGxG5lmhfKNoAy004YpLxpS1W2J8m/EK2Ew+yOs9pVRwO89mg==",
"dev": true,
"dependencies": {
"@babel/helper-validator-identifier": "^7.22.20",
"chalk": "^2.4.2",
"js-tokens": "^4.0.0"
},
"engines": {
"node": ">=6.9.0"
}
},
"node_modules/@babel/traverse/node_modules/@babel/parser": {
"version": "7.23.0",
"resolved": "https://registry.npmjs.org/@babel/parser/-/parser-7.23.0.tgz",
"integrity": "sha512-vvPKKdMemU85V9WE/l5wZEmImpCtLqbnTvqDS2U1fJ96KrxoW7KrXhNsNCblQlg8Ck4b85yxdTyelsMUgFUXiw==",
"dev": true,
"bin": {
"parser": "bin/babel-parser.js"
},
"engines": {
"node": ">=6.0.0"
}
},
"node_modules/@babel/traverse/node_modules/@babel/template": {
"version": "7.22.15",
"resolved": "https://registry.npmjs.org/@babel/template/-/template-7.22.15.tgz",
"integrity": "sha512-QPErUVm4uyJa60rkI73qneDacvdvzxshT3kksGqlGWYdOTIUOwJ7RDUL8sGqslY1uXWSL6xMFKEXDS3ox2uF0w==",
"dev": true,
"dependencies": {
"@babel/code-frame": "^7.22.13",
"@babel/parser": "^7.22.15",
"@babel/types": "^7.22.15"
},
"engines": {
"node": ">=6.9.0"
}
},
"node_modules/@babel/traverse/node_modules/@babel/types": {
"version": "7.23.0",
"resolved": "https://registry.npmjs.org/@babel/types/-/types-7.23.0.tgz",
"integrity": "sha512-0oIyUfKoI3mSqMvsxBdclDwxXKXAUA8v/apZbc+iSyARYou1o8ZGDxbUYyLFoW2arqS2jDGqJuZvv1d/io1axg==",
"dev": true,
"dependencies": {
"@babel/helper-string-parser": "^7.22.5",
"@babel/helper-validator-identifier": "^7.22.20",
"to-fast-properties": "^2.0.0"
},
"engines": {
"node": ">=6.9.0"
}
},
"node_modules/@babel/traverse/node_modules/@jridgewell/gen-mapping": {
"version": "0.3.3",
"resolved": "https://registry.npmjs.org/@jridgewell/gen-mapping/-/gen-mapping-0.3.3.tgz",
@ -672,14 +581,14 @@
}
},
"node_modules/@babel/types": {
"version": "7.19.4",
"resolved": "https://registry.npmjs.org/@babel/types/-/types-7.19.4.tgz",
"integrity": "sha512-M5LK7nAeS6+9j7hAq+b3fQs+pNfUtTGq+yFFfHnauFA8zQtLRfmuipmsKDKKLuyG+wC8ABW43A153YNawNTEtw==",
"version": "7.28.5",
"resolved": "https://registry.npmjs.org/@babel/types/-/types-7.28.5.tgz",
"integrity": "sha512-qQ5m48eI/MFLQ5PxQj4PFaprjyCTLI37ElWMmNs0K8Lk3dVeOdNpB3ks8jc7yM5CDmVC73eMVk/trk3fgmrUpA==",
"dev": true,
"license": "MIT",
"dependencies": {
"@babel/helper-string-parser": "^7.19.4",
"@babel/helper-validator-identifier": "^7.19.1",
"to-fast-properties": "^2.0.0"
"@babel/helper-string-parser": "^7.27.1",
"@babel/helper-validator-identifier": "^7.28.5"
},
"engines": {
"node": ">=6.9.0"
@ -1968,10 +1877,11 @@
"dev": true
},
"node_modules/brace-expansion": {
"version": "1.1.11",
"resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.11.tgz",
"integrity": "sha512-iCuPHDFgrHX7H2vEI/5xpz07zSHB00TpugqhmYtVmMO6518mCuRMoOYFldEBl0g187ufozdaHgWKcYFb61qGiA==",
"version": "1.1.12",
"resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-1.1.12.tgz",
"integrity": "sha512-9T9UjW3r0UW5c1Q7GTwllptXwhvYmEzFhzMfZ9H7FQWt+uZePjZPjBP/W1ZEyZ1twGWom5/56TF4lPcqjnDHcg==",
"dev": true,
"license": "MIT",
"dependencies": {
"balanced-match": "^1.0.0",
"concat-map": "0.0.1"
@ -2250,10 +2160,11 @@
"dev": true
},
"node_modules/cross-spawn": {
"version": "6.0.5",
"resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-6.0.5.tgz",
"integrity": "sha512-eTVLrBSt7fjbDygz805pMnstIs2VTBNkRm0qxZd+M7A5XDdxVRWO5MxGBXZhjY4cqLYLdtrGqRf8mBPmzwSpWQ==",
"version": "6.0.6",
"resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-6.0.6.tgz",
"integrity": "sha512-VqCUuhcd1iB+dsv8gxPttb5iZh/D0iubSP21g36KXdEuf6I5JiioesUVjpCdHV9MZRUfVFlvwtIUyPfxo5trtw==",
"dev": true,
"license": "MIT",
"dependencies": {
"nice-try": "^1.0.4",
"path-key": "^2.0.1",
@ -2505,10 +2416,11 @@
}
},
"node_modules/execa/node_modules/cross-spawn": {
"version": "7.0.3",
"resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-7.0.3.tgz",
"integrity": "sha512-iRDPJKUPVEND7dHPO8rkbOnPpyDygcDFtWjpeWNCgy8WP2rXcxXL8TskReQl6OrB2G7+UJrags1q15Fudc7G6w==",
"version": "7.0.6",
"resolved": "https://registry.npmjs.org/cross-spawn/-/cross-spawn-7.0.6.tgz",
"integrity": "sha512-uV2QOWP2nWzsy2aMp8aRibhi9dlzF5Hgh5SHaB9OiTGEyDTiJJyx0uy51QXdyWbtAHNua4XJzUKca3OzKUd3vA==",
"dev": true,
"license": "MIT",
"dependencies": {
"path-key": "^3.1.0",
"shebang-command": "^2.0.0",
@ -3645,6 +3557,117 @@
"node": ">=8"
}
},
"node_modules/jest-cli": {
"version": "28.1.3",
"resolved": "https://registry.npmjs.org/jest-cli/-/jest-cli-28.1.3.tgz",
"integrity": "sha512-roY3kvrv57Azn1yPgdTebPAXvdR2xfezaKKYzVxZ6It/5NCxzJym6tUI5P1zkdWhfUYkxEI9uZWcQdaFLo8mJQ==",
"dev": true,
"license": "MIT",
"dependencies": {
"@jest/core": "^28.1.3",
"@jest/test-result": "^28.1.3",
"@jest/types": "^28.1.3",
"chalk": "^4.0.0",
"exit": "^0.1.2",
"graceful-fs": "^4.2.9",
"import-local": "^3.0.2",
"jest-config": "^28.1.3",
"jest-util": "^28.1.3",
"jest-validate": "^28.1.3",
"prompts": "^2.0.1",
"yargs": "^17.3.1"
},
"bin": {
"jest": "bin/jest.js"
},
"engines": {
"node": "^12.13.0 || ^14.15.0 || ^16.10.0 || >=17.0.0"
},
"peerDependencies": {
"node-notifier": "^8.0.1 || ^9.0.0 || ^10.0.0"
},
"peerDependenciesMeta": {
"node-notifier": {
"optional": true
}
}
},
"node_modules/jest-cli/node_modules/ansi-styles": {
"version": "4.3.0",
"resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-4.3.0.tgz",
"integrity": "sha512-zbB9rCJAT1rbjiVDb2hqKFHNYLxgtk8NURxZ3IZwD3F6NtxbXZQCnnSi1Lkx+IDohdPlFp222wVALIheZJQSEg==",
"dev": true,
"license": "MIT",
"dependencies": {
"color-convert": "^2.0.1"
},
"engines": {
"node": ">=8"
},
"funding": {
"url": "https://github.com/chalk/ansi-styles?sponsor=1"
}
},
"node_modules/jest-cli/node_modules/chalk": {
"version": "4.1.2",
"resolved": "https://registry.npmjs.org/chalk/-/chalk-4.1.2.tgz",
"integrity": "sha512-oKnbhFyRIXpUuez8iBMmyEa4nbj4IOQyuhc/wy9kY7/WVPcwIO9VA668Pu8RkO7+0G76SLROeyw9CpQ061i4mA==",
"dev": true,
"license": "MIT",
"dependencies": {
"ansi-styles": "^4.1.0",
"supports-color": "^7.1.0"
},
"engines": {
"node": ">=10"
},
"funding": {
"url": "https://github.com/chalk/chalk?sponsor=1"
}
},
"node_modules/jest-cli/node_modules/color-convert": {
"version": "2.0.1",
"resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz",
"integrity": "sha512-RRECPsj7iu/xb5oKYcsFHSppFNnsj/52OVTRKb4zP5onXwVF3zVmmToNcOfGC+CRDpfK/U584fMg38ZHCaElKQ==",
"dev": true,
"license": "MIT",
"dependencies": {
"color-name": "~1.1.4"
},
"engines": {
"node": ">=7.0.0"
}
},
"node_modules/jest-cli/node_modules/color-name": {
"version": "1.1.4",
"resolved": "https://registry.npmjs.org/color-name/-/color-name-1.1.4.tgz",
"integrity": "sha512-dOy+3AuW3a2wNbZHIuMZpTcgjGuLU/uBL/ubcZF9OXbDo8ff4O8yVp5Bf0efS8uEoYo5q4Fx7dY9OgQGXgAsQA==",
"dev": true,
"license": "MIT"
},
"node_modules/jest-cli/node_modules/has-flag": {
"version": "4.0.0",
"resolved": "https://registry.npmjs.org/has-flag/-/has-flag-4.0.0.tgz",
"integrity": "sha512-EykJT/Q1KjTWctppgIAgfSO0tKVuZUjhgMr17kqTumMl6Afv3EISleU7qZUzoXDFTAHTDC4NOoG/ZxU3EvlMPQ==",
"dev": true,
"license": "MIT",
"engines": {
"node": ">=8"
}
},
"node_modules/jest-cli/node_modules/supports-color": {
"version": "7.2.0",
"resolved": "https://registry.npmjs.org/supports-color/-/supports-color-7.2.0.tgz",
"integrity": "sha512-qpCAvRl9stuOHveKsn7HncJRvv501qIacKzQlO/+Lwxc9+0q2wLyv4Dfvt80/DPn2pqOBsJdDiogXGR9+OvwRw==",
"dev": true,
"license": "MIT",
"dependencies": {
"has-flag": "^4.0.0"
},
"engines": {
"node": ">=8"
}
},
"node_modules/jest-config": {
"version": "28.1.3",
"resolved": "https://registry.npmjs.org/jest-config/-/jest-config-28.1.3.tgz",
@ -5283,110 +5306,6 @@
"url": "https://github.com/chalk/supports-color?sponsor=1"
}
},
"node_modules/jest/node_modules/ansi-styles": {
"version": "4.3.0",
"resolved": "https://registry.npmjs.org/ansi-styles/-/ansi-styles-4.3.0.tgz",
"integrity": "sha512-zbB9rCJAT1rbjiVDb2hqKFHNYLxgtk8NURxZ3IZwD3F6NtxbXZQCnnSi1Lkx+IDohdPlFp222wVALIheZJQSEg==",
"dev": true,
"dependencies": {
"color-convert": "^2.0.1"
},
"engines": {
"node": ">=8"
},
"funding": {
"url": "https://github.com/chalk/ansi-styles?sponsor=1"
}
},
"node_modules/jest/node_modules/chalk": {
"version": "4.1.2",
"resolved": "https://registry.npmjs.org/chalk/-/chalk-4.1.2.tgz",
"integrity": "sha512-oKnbhFyRIXpUuez8iBMmyEa4nbj4IOQyuhc/wy9kY7/WVPcwIO9VA668Pu8RkO7+0G76SLROeyw9CpQ061i4mA==",
"dev": true,
"dependencies": {
"ansi-styles": "^4.1.0",
"supports-color": "^7.1.0"
},
"engines": {
"node": ">=10"
},
"funding": {
"url": "https://github.com/chalk/chalk?sponsor=1"
}
},
"node_modules/jest/node_modules/color-convert": {
"version": "2.0.1",
"resolved": "https://registry.npmjs.org/color-convert/-/color-convert-2.0.1.tgz",
"integrity": "sha512-RRECPsj7iu/xb5oKYcsFHSppFNnsj/52OVTRKb4zP5onXwVF3zVmmToNcOfGC+CRDpfK/U584fMg38ZHCaElKQ==",
"dev": true,
"dependencies": {
"color-name": "~1.1.4"
},
"engines": {
"node": ">=7.0.0"
}
},
"node_modules/jest/node_modules/color-name": {
"version": "1.1.4",
"resolved": "https://registry.npmjs.org/color-name/-/color-name-1.1.4.tgz",
"integrity": "sha512-dOy+3AuW3a2wNbZHIuMZpTcgjGuLU/uBL/ubcZF9OXbDo8ff4O8yVp5Bf0efS8uEoYo5q4Fx7dY9OgQGXgAsQA==",
"dev": true
},
"node_modules/jest/node_modules/has-flag": {
"version": "4.0.0",
"resolved": "https://registry.npmjs.org/has-flag/-/has-flag-4.0.0.tgz",
"integrity": "sha512-EykJT/Q1KjTWctppgIAgfSO0tKVuZUjhgMr17kqTumMl6Afv3EISleU7qZUzoXDFTAHTDC4NOoG/ZxU3EvlMPQ==",
"dev": true,
"engines": {
"node": ">=8"
}
},
"node_modules/jest/node_modules/jest-cli": {
"version": "28.1.3",
"resolved": "https://registry.npmjs.org/jest-cli/-/jest-cli-28.1.3.tgz",
"integrity": "sha512-roY3kvrv57Azn1yPgdTebPAXvdR2xfezaKKYzVxZ6It/5NCxzJym6tUI5P1zkdWhfUYkxEI9uZWcQdaFLo8mJQ==",
"dev": true,
"dependencies": {
"@jest/core": "^28.1.3",
"@jest/test-result": "^28.1.3",
"@jest/types": "^28.1.3",
"chalk": "^4.0.0",
"exit": "^0.1.2",
"graceful-fs": "^4.2.9",
"import-local": "^3.0.2",
"jest-config": "^28.1.3",
"jest-util": "^28.1.3",
"jest-validate": "^28.1.3",
"prompts": "^2.0.1",
"yargs": "^17.3.1"
},
"bin": {
"jest": "bin/jest.js"
},
"engines": {
"node": "^12.13.0 || ^14.15.0 || ^16.10.0 || >=17.0.0"
},
"peerDependencies": {
"node-notifier": "^8.0.1 || ^9.0.0 || ^10.0.0"
},
"peerDependenciesMeta": {
"node-notifier": {
"optional": true
}
}
},
"node_modules/jest/node_modules/supports-color": {
"version": "7.2.0",
"resolved": "https://registry.npmjs.org/supports-color/-/supports-color-7.2.0.tgz",
"integrity": "sha512-qpCAvRl9stuOHveKsn7HncJRvv501qIacKzQlO/+Lwxc9+0q2wLyv4Dfvt80/DPn2pqOBsJdDiogXGR9+OvwRw==",
"dev": true,
"dependencies": {
"has-flag": "^4.0.0"
},
"engines": {
"node": ">=8"
}
},
"node_modules/js-tokens": {
"version": "4.0.0",
"resolved": "https://registry.npmjs.org/js-tokens/-/js-tokens-4.0.0.tgz",
@ -5394,10 +5313,11 @@
"dev": true
},
"node_modules/js-yaml": {
"version": "3.14.1",
"resolved": "https://registry.npmjs.org/js-yaml/-/js-yaml-3.14.1.tgz",
"integrity": "sha512-okMH7OXXJ7YrN9Ok3/SXrnu4iX9yOk+25nqX4imS2npuvTYDmo/QEZoqwZkYaIDk3jVvBOTOIEgEhaLOynBS9g==",
"version": "3.14.2",
"resolved": "https://registry.npmjs.org/js-yaml/-/js-yaml-3.14.2.tgz",
"integrity": "sha512-PMSmkqxr106Xa156c2M265Z+FTrPl+oxd/rgOQy2tijQeK5TxQ43psO1ZCwhVOSdnn+RzkzlRz/eY4BgJBYVpg==",
"dev": true,
"license": "MIT",
"dependencies": {
"argparse": "^1.0.7",
"esprima": "^4.0.0"
@ -5914,10 +5834,11 @@
}
},
"node_modules/picocolors": {
"version": "1.0.0",
"resolved": "https://registry.npmjs.org/picocolors/-/picocolors-1.0.0.tgz",
"integrity": "sha512-1fygroTLlHu66zi26VoTDv8yRgm0Fccecssto+MhsZ0D/DGW2sm8E8AjW7NU5VVTRt5GxbeZ5qBuJr+HyLYkjQ==",
"dev": true
"version": "1.1.1",
"resolved": "https://registry.npmjs.org/picocolors/-/picocolors-1.1.1.tgz",
"integrity": "sha512-xceH2snhtb5M9liqDsmEw56le376mTZkEX/jEb/RxNFyegNul7eNslCXP9FDj/Lcu0X8KEyMceP2ntpaHrDEVA==",
"dev": true,
"license": "ISC"
},
"node_modules/picomatch": {
"version": "2.3.1",
@ -6068,12 +5989,6 @@
"node": ">=6"
}
},
"node_modules/regenerator-runtime": {
"version": "0.13.10",
"resolved": "https://registry.npmjs.org/regenerator-runtime/-/regenerator-runtime-0.13.10.tgz",
"integrity": "sha512-KepLsg4dU12hryUO7bp/axHAKvwGOCV0sGloQtpagJ12ai+ojVDqkeGSiRX1zlq+kjIMZ1t7gpze+26QqtdGqw==",
"dev": true
},
"node_modules/regexp.prototype.flags": {
"version": "1.4.3",
"resolved": "https://registry.npmjs.org/regexp.prototype.flags/-/regexp.prototype.flags-1.4.3.tgz",
@ -6537,15 +6452,6 @@
"integrity": "sha512-3f0uOEAQwIqGuWW2MVzYg8fV/QNnc/IpuJNG837rLuczAaLVHslWHZQj4IGiEl5Hs3kkbhwL9Ab7Hrsmuj+Smw==",
"dev": true
},
"node_modules/to-fast-properties": {
"version": "2.0.0",
"resolved": "https://registry.npmjs.org/to-fast-properties/-/to-fast-properties-2.0.0.tgz",
"integrity": "sha512-/OaKK0xYrs3DmxRYqL/yDc+FxFUVYhDlXMhRmv3z915w2HF1tnN1omB354j8VUGO/hbRzyD6Y3sA7v7GS/ceog==",
"dev": true,
"engines": {
"node": ">=4"
}
},
"node_modules/to-regex-range": {
"version": "5.0.1",
"resolved": "https://registry.npmjs.org/to-regex-range/-/to-regex-range-5.0.1.tgz",
@ -6722,9 +6628,9 @@
}
},
"node_modules/typedoc/node_modules/brace-expansion": {
"version": "2.0.1",
"resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-2.0.1.tgz",
"integrity": "sha512-XnAIvQ8eM+kC6aULx6wuQiwVsnzsi9d3WxzV3FpWTGA19F621kwdbsAcFKXgKUHZWsy+mY6iL1sHTxWEFCytDA==",
"version": "2.0.2",
"resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-2.0.2.tgz",
"integrity": "sha512-Jt0vHyM+jmUBqojB7E1NIYadt0vI0Qxjxd2TErW94wDz+E2LAm5vKMXXwg6ZZBTHPuUlDgQHKXvjGBdfcF1ZDQ==",
"dev": true,
"license": "MIT",
"dependencies": {

1
src/api/js/scripts/parse-api.ts
View file

@ -56,6 +56,7 @@ const types = {
Z3_final_eh: 'Z3_final_eh',
Z3_created_eh: 'Z3_created_eh',
Z3_decide_eh: 'Z3_decide_eh',
Z3_on_binding_eh: 'Z3_on_binding_eh',
Z3_on_clause_eh: 'Z3_on_clause_eh',
} as unknown as Record<string, string>;

70
src/api/js/src/high-level/high-level.test.ts
View file

@ -890,4 +890,74 @@ describe('high-level', () => {
expect(model.eval(z).eqIdentity(Int.val(5))).toBeTruthy();
});
});
describe('datatypes', () => {
it('should create simple enum datatype', async () => {
const { Datatype, Int, Bool, Solver } = api.Context('main');
// Create a simple Color enum datatype
const Color = Datatype('Color');
Color.declare('red');
Color.declare('green');
Color.declare('blue');
const ColorSort = Color.create();
// Test that we can access the constructors
expect(typeof (ColorSort as any).red).not.toBe('undefined');
expect(typeof (ColorSort as any).green).not.toBe('undefined');
expect(typeof (ColorSort as any).blue).not.toBe('undefined');
// Test that we can access the recognizers
expect(typeof (ColorSort as any).is_red).not.toBe('undefined');
expect(typeof (ColorSort as any).is_green).not.toBe('undefined');
expect(typeof (ColorSort as any).is_blue).not.toBe('undefined');
});
it('should create recursive list datatype', async () => {
const { Datatype, Int, Solver } = api.Context('main');
// Create a recursive List datatype like in the Python example
const List = Datatype('List');
List.declare('cons', ['car', Int.sort()], ['cdr', List]);
List.declare('nil');
const ListSort = List.create();
// Test that constructors and accessors exist
expect(typeof (ListSort as any).cons).not.toBe('undefined');
expect(typeof (ListSort as any).nil).not.toBe('undefined');
expect(typeof (ListSort as any).is_cons).not.toBe('undefined');
expect(typeof (ListSort as any).is_nil).not.toBe('undefined');
expect(typeof (ListSort as any).car).not.toBe('undefined');
expect(typeof (ListSort as any).cdr).not.toBe('undefined');
});
it('should create mutually recursive tree datatypes', async () => {
const { Datatype, Int } = api.Context('main');
// Create mutually recursive Tree and TreeList datatypes
const Tree = Datatype('Tree');
const TreeList = Datatype('TreeList');
Tree.declare('leaf', ['value', Int.sort()]);
Tree.declare('node', ['children', TreeList]);
TreeList.declare('nil');
TreeList.declare('cons', ['car', Tree], ['cdr', TreeList]);
const [TreeSort, TreeListSort] = Datatype.createDatatypes(Tree, TreeList);
// Test that both datatypes have their constructors
expect(typeof (TreeSort as any).leaf).not.toBe('undefined');
expect(typeof (TreeSort as any).node).not.toBe('undefined');
expect(typeof (TreeListSort as any).nil).not.toBe('undefined');
expect(typeof (TreeListSort as any).cons).not.toBe('undefined');
// Test accessors exist
expect(typeof (TreeSort as any).value).not.toBe('undefined');
expect(typeof (TreeSort as any).children).not.toBe('undefined');
expect(typeof (TreeListSort as any).car).not.toBe('undefined');
expect(typeof (TreeListSort as any).cdr).not.toBe('undefined');
});
});
});

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

@ -17,6 +17,8 @@ import {
Z3_ast_print_mode,
Z3_ast_vector,
Z3_context,
Z3_constructor,
Z3_constructor_list,
Z3_decl_kind,
Z3_error_code,
Z3_func_decl,
@ -88,6 +90,10 @@ import {
FuncEntry,
SMTSetSort,
SMTSet,
Datatype,
DatatypeSort,
DatatypeExpr,
DatatypeCreation,
} from './types';
import { allSatisfy, assert, assertExhaustive } from './utils';
@ -825,6 +831,17 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
}
}
const Datatype = Object.assign(
(name: string): DatatypeImpl => {
return new DatatypeImpl(ctx, name);
},
{
createDatatypes(...datatypes: DatatypeImpl[]): DatatypeSortImpl[] {
return createDatatypes(...datatypes);
}
}
);
////////////////
// Operations //
////////////////
@ -1290,10 +1307,6 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
return new SetImpl<ElemSort>(check(Z3.mk_set_difference(contextPtr, a.ast, b.ast)));
}
function SetHasSize<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>, size: bigint | number | string | IntNum<Name>): Bool<Name> {
const a = typeof size === 'object'? Int.sort().cast(size) : Int.sort().cast(size);
return new BoolImpl(check(Z3.mk_set_has_size(contextPtr, set.ast, a.ast)));
}
function SetAdd<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>, elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort> {
const arg = set.elemSort().cast(elem as any);
@ -2627,9 +2640,6 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
diff(b: SMTSet<Name, ElemSort>): SMTSet<Name, ElemSort> {
return SetDifference(this, b);
}
hasSize(size: string | number | bigint | IntNum<Name>): Bool<Name> {
return SetHasSize(this, size);
}
add(elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort> {
return SetAdd(this, elem);
}
@ -2647,6 +2657,185 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
}
}
////////////////////////////
// Datatypes
////////////////////////////
class DatatypeImpl implements Datatype<Name> {
readonly ctx: Context<Name>;
readonly name: string;
public constructors: Array<[string, Array<[string, Sort<Name> | Datatype<Name>]>]> = [];
constructor(ctx: Context<Name>, name: string) {
this.ctx = ctx;
this.name = name;
}
declare(name: string, ...fields: Array<[string, Sort<Name> | Datatype<Name>]>): this {
this.constructors.push([name, fields]);
return this;
}
create(): DatatypeSort<Name> {
const datatypes = createDatatypes(this);
return datatypes[0];
}
}
class DatatypeSortImpl extends SortImpl implements DatatypeSort<Name> {
declare readonly __typename: DatatypeSort['__typename'];
numConstructors(): number {
return Z3.get_datatype_sort_num_constructors(contextPtr, this.ptr);
}
constructorDecl(idx: number): FuncDecl<Name> {
const ptr = Z3.get_datatype_sort_constructor(contextPtr, this.ptr, idx);
return new FuncDeclImpl(ptr);
}
recognizer(idx: number): FuncDecl<Name> {
const ptr = Z3.get_datatype_sort_recognizer(contextPtr, this.ptr, idx);
return new FuncDeclImpl(ptr);
}
accessor(constructorIdx: number, accessorIdx: number): FuncDecl<Name> {
const ptr = Z3.get_datatype_sort_constructor_accessor(contextPtr, this.ptr, constructorIdx, accessorIdx);
return new FuncDeclImpl(ptr);
}
cast(other: CoercibleToExpr<Name>): DatatypeExpr<Name>;
cast(other: DatatypeExpr<Name>): DatatypeExpr<Name>;
cast(other: CoercibleToExpr<Name> | DatatypeExpr<Name>): DatatypeExpr<Name> {
if (isExpr(other)) {
assert(this.eqIdentity(other.sort), 'Value cannot be converted to this datatype');
return other as DatatypeExpr<Name>;
}
throw new Error('Cannot coerce value to datatype expression');
}
subsort(other: Sort<Name>) {
_assertContext(other.ctx);
return this.eqIdentity(other);
}
}
class DatatypeExprImpl extends ExprImpl<Z3_ast, DatatypeSortImpl> implements DatatypeExpr<Name> {
declare readonly __typename: DatatypeExpr['__typename'];
}
function createDatatypes(...datatypes: DatatypeImpl[]): DatatypeSortImpl[] {
if (datatypes.length === 0) {
throw new Error('At least one datatype must be provided');
}
// All datatypes must be from the same context
const dtCtx = datatypes[0].ctx;
for (const dt of datatypes) {
if (dt.ctx !== dtCtx) {
throw new Error('All datatypes must be from the same context');
}
}
const sortNames = datatypes.map(dt => dt.name);
const constructorLists: Z3_constructor_list[] = [];
const scopedConstructors: Z3_constructor[] = [];
try {
// Create constructor lists for each datatype
for (const dt of datatypes) {
const constructors: Z3_constructor[] = [];
for (const [constructorName, fields] of dt.constructors) {
const fieldNames: string[] = [];
const fieldSorts: Z3_sort[] = [];
const fieldRefs: number[] = [];
for (const [fieldName, fieldSort] of fields) {
fieldNames.push(fieldName);
if (fieldSort instanceof DatatypeImpl) {
// Reference to another datatype being defined
const refIndex = datatypes.indexOf(fieldSort);
if (refIndex === -1) {
throw new Error(`Referenced datatype "${fieldSort.name}" not found in datatypes being created`);
}
// For recursive references, we pass null and the ref index
fieldSorts.push(null as any); // null will be handled by the Z3 API
fieldRefs.push(refIndex);
} else {
// Regular sort
fieldSorts.push((fieldSort as Sort<Name>).ptr);
fieldRefs.push(0);
}
}
const constructor = Z3.mk_constructor(
contextPtr,
Z3.mk_string_symbol(contextPtr, constructorName),
Z3.mk_string_symbol(contextPtr, `is_${constructorName}`),
fieldNames.map(name => Z3.mk_string_symbol(contextPtr, name)),
fieldSorts,
fieldRefs
);
constructors.push(constructor);
scopedConstructors.push(constructor);
}
const constructorList = Z3.mk_constructor_list(contextPtr, constructors);
constructorLists.push(constructorList);
}
// Create the datatypes
const sortSymbols = sortNames.map(name => Z3.mk_string_symbol(contextPtr, name));
const resultSorts = Z3.mk_datatypes(contextPtr, sortSymbols, constructorLists);
// Create DatatypeSortImpl instances
const results: DatatypeSortImpl[] = [];
for (let i = 0; i < resultSorts.length; i++) {
const sortImpl = new DatatypeSortImpl(resultSorts[i]);
// Attach constructor, recognizer, and accessor functions dynamically
const numConstructors = sortImpl.numConstructors();
for (let j = 0; j < numConstructors; j++) {
const constructor = sortImpl.constructorDecl(j);
const recognizer = sortImpl.recognizer(j);
const constructorName = constructor.name().toString();
// Attach constructor function
if (constructor.arity() === 0) {
// Nullary constructor (constant)
(sortImpl as any)[constructorName] = constructor.call();
} else {
(sortImpl as any)[constructorName] = constructor;
}
// Attach recognizer function
(sortImpl as any)[`is_${constructorName}`] = recognizer;
// Attach accessor functions
for (let k = 0; k < constructor.arity(); k++) {
const accessor = sortImpl.accessor(j, k);
const accessorName = accessor.name().toString();
(sortImpl as any)[accessorName] = accessor;
}
}
results.push(sortImpl);
}
return results;
} finally {
// Clean up resources
for (const constructor of scopedConstructors) {
Z3.del_constructor(contextPtr, constructor);
}
for (const constructorList of constructorLists) {
Z3.del_constructor_list(contextPtr, constructorList);
}
}
}
class QuantifierImpl<
QVarSorts extends NonEmptySortArray<Name>,
QSort extends BoolSort<Name> | SMTArraySort<Name, QVarSorts>,
@ -3029,6 +3218,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
BitVec,
Array,
Set,
Datatype,
////////////////
// Operations //
@ -3095,7 +3285,6 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
SetUnion,
SetIntersect,
SetDifference,
SetHasSize,
SetAdd,
SetDel,
SetComplement,
@ -3120,6 +3309,6 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
setParam,
resetParams,
Context: createContext,
Context: createContext as ContextCtor,
};
}

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

@ -3,6 +3,8 @@ import {
Z3_ast_map,
Z3_ast_vector,
Z3_context,
Z3_constructor,
Z3_constructor_list,
Z3_decl_kind,
Z3_func_decl,
Z3_func_entry,
@ -123,6 +125,7 @@ export type CheckSatResult = 'sat' | 'unsat' | 'unknown';
/** @hidden */
export interface ContextCtor {
<Name extends string>(name: Name, options?: Record<string, any>): Context<Name>;
new <Name extends string>(name: Name, options?: Record<string, any>): Context<Name>;
}
export interface Context<Name extends string = 'main'> {
@ -362,6 +365,8 @@ export interface Context<Name extends string = 'main'> {
readonly Array: SMTArrayCreation<Name>;
/** @category Expressions */
readonly Set: SMTSetCreation<Name>;
/** @category Expressions */
readonly Datatype: DatatypeCreation<Name>;
////////////////
// Operations //
@ -625,9 +630,6 @@ export interface Context<Name extends string = 'main'> {
/** @category Operations */
SetDifference<ElemSort extends AnySort<Name>>(a: SMTSet<Name, ElemSort>, b: SMTSet<Name, ElemSort>): SMTSet<Name, ElemSort>;
/** @category Operations */
SetHasSize<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>, size: bigint | number | string | IntNum<Name>): Bool<Name>;
/** @category Operations */
SetAdd<ElemSort extends AnySort<Name>>(set: SMTSet<Name, ElemSort>, elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort>;
@ -842,7 +844,8 @@ export interface Sort<Name extends string = 'main'> extends Ast<Name, Z3_sort> {
| BoolSort['__typename']
| ArithSort['__typename']
| BitVecSort['__typename']
| SMTArraySort['__typename'];
| SMTArraySort['__typename']
| DatatypeSort['__typename'];
kind(): Z3_sort_kind;
@ -966,7 +969,8 @@ export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySo
| Bool['__typename']
| Arith['__typename']
| BitVec['__typename']
| SMTArray['__typename'];
| SMTArray['__typename']
| DatatypeExpr['__typename'];
get sort(): S;
@ -1643,7 +1647,6 @@ export interface SMTSet<Name extends string = 'main', ElemSort extends AnySort<N
intersect(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort>;
diff(b: SMTSet<Name, ElemSort>): SMTSet<Name, ElemSort>;
hasSize(size: bigint | number | string | IntNum<Name>): Bool<Name>;
add(elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort>;
del(elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): SMTSet<Name, ElemSort>;
@ -1653,6 +1656,111 @@ export interface SMTSet<Name extends string = 'main', ElemSort extends AnySort<N
subsetOf(b: SMTSet<Name, ElemSort>): Bool<Name>;
}
//////////////////////////////////////////
//
// Datatypes
//
//////////////////////////////////////////
/**
* Helper class for declaring Z3 datatypes.
*
* Follows the same pattern as Python Z3 API for declaring constructors
* before creating the actual datatype sort.
*
* @example
* ```typescript
* const List = new ctx.Datatype('List');
* List.declare('cons', ['car', ctx.Int.sort()], ['cdr', List]);
* List.declare('nil');
* const ListSort = List.create();
* ```
*
* @category Datatypes
*/
export interface Datatype<Name extends string = 'main'> {
readonly ctx: Context<Name>;
readonly name: string;
/**
* Declare a constructor for this datatype.
*
* @param name Constructor name
* @param fields Array of [field_name, field_sort] pairs
*/
declare(name: string, ...fields: Array<[string, AnySort<Name> | Datatype<Name>]>): this;
/**
* Create the actual datatype sort from the declared constructors.
* For mutually recursive datatypes, use Context.createDatatypes instead.
*/
create(): DatatypeSort<Name>;
}
/**
* @category Datatypes
*/
export interface DatatypeCreation<Name extends string> {
/**
* Create a new datatype declaration helper.
*/
(name: string): Datatype<Name>;
/**
* Create mutually recursive datatypes.
*
* @param datatypes Array of Datatype declarations
* @returns Array of created DatatypeSort instances
*/
createDatatypes(...datatypes: Datatype<Name>[]): DatatypeSort<Name>[];
}
/**
* A Sort representing an algebraic datatype.
*
* After creation, this sort will have constructor, recognizer, and accessor
* functions dynamically attached based on the declared constructors.
*
* @category Datatypes
*/
export interface DatatypeSort<Name extends string = 'main'> extends Sort<Name> {
/** @hidden */
readonly __typename: 'DatatypeSort';
/**
* Number of constructors in this datatype
*/
numConstructors(): number;
/**
* Get the idx'th constructor function declaration
*/
constructorDecl(idx: number): FuncDecl<Name>;
/**
* Get the idx'th recognizer function declaration
*/
recognizer(idx: number): FuncDecl<Name>;
/**
* Get the accessor function declaration for the idx_a'th field of the idx_c'th constructor
*/
accessor(constructorIdx: number, accessorIdx: number): FuncDecl<Name>;
cast(other: CoercibleToExpr<Name>): DatatypeExpr<Name>;
cast(other: DatatypeExpr<Name>): DatatypeExpr<Name>;
}
/**
* Represents expressions of datatype sorts.
*
* @category Datatypes
*/
export interface DatatypeExpr<Name extends string = 'main'> extends Expr<Name, DatatypeSort<Name>, Z3_ast> {
/** @hidden */
readonly __typename: 'DatatypeExpr';
}
/**
* Defines the expression type of the body of a quantifier expression

4
src/api/js/src/node.ts
View file

@ -11,7 +11,7 @@ export * from './low-level/types.__GENERATED__';
* The main entry point to the Z3 API
*
* ```typescript
* import { init, sat } from 'z3-solver';
* import { init } from 'z3-solver';
*
* const { Context } = await init();
* const { Solver, Int } = new Context('main');
@ -22,7 +22,7 @@ export * from './low-level/types.__GENERATED__';
* const solver = new Solver();
* solver.add(x.add(2).le(y.sub(10))); // x + 2 <= y - 10
*
* if (await solver.check() !== sat) {
* if (await solver.check() !== 'sat') {
* throw new Error("couldn't find a solution")
* }
* const model = solver.model();

27
src/api/julia/CMakeLists.txt
View file

@ -1,5 +1,32 @@
find_package(JlCxx REQUIRED)
# Check for Windows MSVC + MinGW library compatibility issues
if(WIN32 AND CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
# Get the JlCxx library path to check its format
get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_LOCATION)
if(NOT JLCXX_LIB_PATH)
get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_LOCATION_RELEASE)
endif()
if(NOT JLCXX_LIB_PATH)
get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_IMPLIB)
endif()
if(NOT JLCXX_LIB_PATH)
get_target_property(JLCXX_LIB_PATH JlCxx::cxxwrap_julia IMPORTED_IMPLIB_RELEASE)
endif()
if(JLCXX_LIB_PATH AND JLCXX_LIB_PATH MATCHES "\\.dll\\.a$")
message(FATAL_ERROR
"Julia bindings build error: Incompatible CxxWrap library format detected.\n"
"The found libcxxwrap_julia library (${JLCXX_LIB_PATH}) is a MinGW import library (.dll.a), "
"but Z3 is being built with MSVC which requires .lib format.\n\n"
"Solutions:\n"
"1. Use MinGW/GCC instead of MSVC to build Z3\n"
"2. Install a MSVC-compatible version of CxxWrap\n"
"3. Disable Julia bindings with -DZ3_BUILD_JULIA_BINDINGS=OFF\n\n"
"For more information, see: https://github.com/JuliaInterop/CxxWrap.jl#compiling-the-c-code")
endif()
endif()
add_library(z3jl SHARED z3jl.cpp)
target_link_libraries(z3jl PRIVATE JlCxx::cxxwrap_julia libz3)
target_include_directories(z3jl PRIVATE

2
src/api/ml/CMakeLists.txt
View file

@ -255,6 +255,7 @@ set(z3ml_example_src ${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml)
add_custom_command(
TARGET build_z3_ocaml_bindings POST_BUILD
COMMAND "${OCAMLFIND}" ocamlc
-cclib "${libz3_path}/libz3${so_ext}"
-o "${z3ml_bin}/ml_example.byte"
-package zarith
-linkpkg
@ -270,6 +271,7 @@ add_custom_command(
add_custom_command(
TARGET build_z3_ocaml_bindings POST_BUILD
COMMAND "${OCAMLFIND}" ocamlopt
-cclib "${libz3_path}/libz3${so_ext}"
-o "${z3ml_bin}/ml_example"
-package zarith
-linkpkg

10
src/api/ml/z3.ml
View file

@ -15,7 +15,7 @@ type context = Z3native.context
module Log =
struct
let open_ filename =
lbool_of_int (Z3native.open_log filename) = L_TRUE
(Z3native.open_log filename)
let close = Z3native.close_log
let append = Z3native.append_log
end
@ -909,11 +909,17 @@ struct
mk_sort ctx (Symbol.mk_string ctx name) constructors
let mk_sort_ref (ctx: context) (name:Symbol.symbol) =
Z3native.mk_datatype_sort ctx name
Z3native.mk_datatype_sort ctx name 0 []
let mk_sort_ref_s (ctx: context) (name: string) =
mk_sort_ref ctx (Symbol.mk_string ctx name)
let mk_sort_ref_p (ctx: context) (name:Symbol.symbol) (params:Sort.sort list) =
Z3native.mk_datatype_sort ctx name (List.length params) params
let mk_sort_ref_ps (ctx: context) (name: string) (params:Sort.sort list) =
mk_sort_ref_p ctx (Symbol.mk_string ctx name) params
let mk_sorts (ctx:context) (names:Symbol.symbol list) (c:Constructor.constructor list list) =
let n = List.length names in
let f e = ConstructorList.create ctx e in

6
src/api/ml/z3.mli
View file

@ -1087,6 +1087,12 @@ sig
(* [mk_sort_ref_s ctx s] is [mk_sort_ref ctx (Symbol.mk_string ctx s)] *)
val mk_sort_ref_s : context -> string -> Sort.sort
(** Create a forward reference to a parametric datatype sort. *)
val mk_sort_ref_p : context -> Symbol.symbol -> Sort.sort list -> Sort.sort
(** Create a forward reference to a parametric datatype sort. *)
val mk_sort_ref_ps : context -> string -> Sort.sort list -> Sort.sort
(** Create a new datatype sort. *)
val mk_sort : context -> Symbol.symbol -> Constructor.constructor list -> Sort.sort

33
src/api/python/CMakeLists.txt
View file

@ -70,13 +70,32 @@ else()
endif()
# Link libz3 into the python directory so bindings work out of the box
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
"${PROJECT_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
"${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
DEPENDS libz3
COMMENT "Linking libz3 into python directory"
)
# Handle both built libz3 and pre-installed libz3
if (TARGET libz3)
# Get the libz3 location - handle both regular and imported targets
get_target_property(LIBZ3_IS_IMPORTED libz3 IMPORTED)
if (LIBZ3_IS_IMPORTED)
# For imported targets, get the IMPORTED_LOCATION
get_target_property(LIBZ3_SOURCE_PATH libz3 IMPORTED_LOCATION)
# No dependency on libz3 target since it's pre-built
set(LIBZ3_DEPENDS "")
else()
# For regular targets, use the build output location
set(LIBZ3_SOURCE_PATH "${PROJECT_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}")
set(LIBZ3_DEPENDS libz3)
endif()
add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
"${LIBZ3_SOURCE_PATH}"
"${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
DEPENDS ${LIBZ3_DEPENDS}
COMMENT "Linking libz3 into python directory"
)
else()
message(FATAL_ERROR "libz3 target not found. Cannot build Python bindings.")
endif()
# Convenient top-level target
add_custom_target(build_z3_python_bindings

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

@ -113,14 +113,21 @@ def _clean_native_build():
def _z3_version():
post = os.getenv('Z3_VERSION_SUFFIX', '')
print("z3_version", "release dir", RELEASE_DIR)
if RELEASE_DIR is None:
fn = os.path.join(SRC_DIR, 'scripts', 'mk_project.py')
if os.path.exists(fn):
with open(fn) as f:
for line in f:
n = re.match(r".*set_version\((.*), (.*), (.*), (.*)\).*", line)
if not n is None:
return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post
dirs = [SRC_DIR, ROOT_DIR, SRC_DIR_REPO, SRC_DIR_LOCAL, os.path.join(ROOT_DIR, '..', '..')]
for d in dirs:
if os.path.exists(d):
print(d, ": ", os.listdir(d))
fns = [os.path.join(d, 'scripts', 'VERSION.txt') for d in dirs]
for fn in fns:
print("loading version file", fn, "exists", os.path.exists(fn))
if os.path.exists(fn):
with open(fn) as f:
for line in f:
n = re.match(r"(.*)\.(.*)\.(.*)\.(.*)", line)
if not n is None:
return n.group(1) + '.' + n.group(2) + '.' + n.group(3) + '.' + n.group(4) + post
return "?.?.?.?"
else:
version = RELEASE_METADATA[0]
@ -284,7 +291,7 @@ class sdist(_sdist):
# The Azure Dev Ops pipelines use internal OS version tagging that don't correspond
# to releases.
internal_build_re = re.compile("(.+)\_7")
internal_build_re = re.compile("(.+)_7")
class bdist_wheel(_bdist_wheel):

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

@ -653,6 +653,10 @@ class SortRef(AstRef):
"""
return not Z3_is_eq_sort(self.ctx_ref(), self.ast, other.ast)
def __gt__(self, other):
"""Create the function space Array(self, other)"""
return ArraySort(self, other)
def __hash__(self):
""" Hash code. """
return AstRef.__hash__(self)
@ -1241,6 +1245,18 @@ def _coerce_expr_merge(s, a):
else:
return s
def _check_same_sort(a, b, ctx=None):
if not isinstance(a, ExprRef):
return False
if not isinstance(b, ExprRef):
return False
if ctx is None:
ctx = a.ctx
a_sort = Z3_get_sort(ctx.ctx, a.ast)
b_sort = Z3_get_sort(ctx.ctx, b.ast)
return Z3_is_eq_sort(ctx.ctx, a_sort, b_sort)
def _coerce_exprs(a, b, ctx=None):
if not is_expr(a) and not is_expr(b):
@ -1255,6 +1271,9 @@ def _coerce_exprs(a, b, ctx=None):
if isinstance(b, float) and isinstance(a, ArithRef):
b = RealVal(b, a.ctx)
if _check_same_sort(a, b, ctx):
return (a, b)
s = None
s = _coerce_expr_merge(s, a)
s = _coerce_expr_merge(s, b)
@ -1506,6 +1525,8 @@ def Consts(names, sort):
def FreshConst(sort, prefix="c"):
"""Create a fresh constant of a specified sort"""
if z3_debug():
_z3_assert(is_sort(sort), f"Z3 sort expected, got {type(sort)}")
ctx = _get_ctx(sort.ctx)
return _to_expr_ref(Z3_mk_fresh_const(ctx.ref(), prefix, sort.ast), ctx)
@ -4989,13 +5010,6 @@ def Ext(a, b):
_z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays")
return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
def SetHasSize(a, k):
ctx = a.ctx
k = _py2expr(k, ctx)
return _to_expr_ref(Z3_mk_set_has_size(ctx.ref(), a.as_ast(), k.as_ast()), ctx)
def is_select(a):
"""Return `True` if `a` is a Z3 array select application.
@ -5468,10 +5482,30 @@ class DatatypeRef(ExprRef):
"""Return the datatype sort of the datatype expression `self`."""
return DatatypeSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
def DatatypeSort(name, ctx = None):
"""Create a reference to a sort that was declared, or will be declared, as a recursive datatype"""
def DatatypeSort(name, params=None, ctx=None):
"""Create a reference to a sort that was declared, or will be declared, as a recursive datatype.
Args:
name: name of the datatype sort
params: optional list/tuple of sort parameters for parametric datatypes
ctx: Z3 context (optional)
Example:
>>> # Non-parametric datatype
>>> TreeRef = DatatypeSort('Tree')
>>> # Parametric datatype with one parameter
>>> ListIntRef = DatatypeSort('List', [IntSort()])
>>> # Parametric datatype with multiple parameters
>>> PairRef = DatatypeSort('Pair', [IntSort(), BoolSort()])
"""
ctx = _get_ctx(ctx)
return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx)), ctx)
if params is None or len(params) == 0:
return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx), 0, (Sort * 0)()), ctx)
else:
_params = (Sort * len(params))()
for i in range(len(params)):
_params[i] = params[i].ast
return DatatypeSortRef(Z3_mk_datatype_sort(ctx.ref(), to_symbol(name, ctx), len(params), _params), ctx)
def TupleSort(name, sorts, ctx=None):
"""Create a named tuple sort base on a set of underlying sorts
@ -7257,7 +7291,7 @@ class Solver(Z3PPObject):
>>> s.reset()
>>> s.add(2**x == 4)
>>> s.check()
unknown
sat
"""
s = BoolSort(self.ctx)
assumptions = _get_args(assumptions)
@ -7501,7 +7535,7 @@ class Solver(Z3PPObject):
>>> x = Int('x')
>>> s = SimpleSolver()
>>> s.add(2**x == 4)
>>> s.add(x == 2**x)
>>> s.check()
unknown
>>> s.reason_unknown()
@ -9998,7 +10032,7 @@ class FPNumRef(FPRef):
"""
def sign(self):
num = (ctypes.c_int)()
num = ctypes.c_bool()
nsign = Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(num))
if nsign is False:
raise Z3Exception("error retrieving the sign of a numeral.")
@ -11812,6 +11846,16 @@ def user_prop_decide(ctx, cb, t_ref, idx, phase):
t = _to_expr_ref(to_Ast(t_ref), prop.ctx())
prop.decide(t, idx, phase)
prop.cb = old_cb
def user_prop_binding(ctx, cb, q_ref, inst_ref):
prop = _prop_closures.get(ctx)
old_cb = prop.cb
prop.cb = cb
q = _to_expr_ref(to_Ast(q_ref), prop.ctx())
inst = _to_expr_ref(to_Ast(inst_ref), prop.ctx())
r = prop.binding(q, inst)
prop.cb = old_cb
return r
_user_prop_push = Z3_push_eh(user_prop_push)
@ -11823,6 +11867,7 @@ _user_prop_final = Z3_final_eh(user_prop_final)
_user_prop_eq = Z3_eq_eh(user_prop_eq)
_user_prop_diseq = Z3_eq_eh(user_prop_diseq)
_user_prop_decide = Z3_decide_eh(user_prop_decide)
_user_prop_binding = Z3_on_binding_eh(user_prop_binding)
def PropagateFunction(name, *sig):
@ -11871,6 +11916,7 @@ class UserPropagateBase:
self.diseq = None
self.decide = None
self.created = None
self.binding = None
if ctx:
self.fresh_ctx = ctx
if s:
@ -11934,7 +11980,14 @@ class UserPropagateBase:
assert not self._ctx
if self.solver:
Z3_solver_propagate_decide(self.ctx_ref(), self.solver.solver, _user_prop_decide)
self.decide = decide
self.decide = decide
def add_on_binding(self, binding):
assert not self.binding
assert not self._ctx
if self.solver:
Z3_solver_propagate_on_binding(self.ctx_ref(), self.solver.solver, _user_prop_binding)
self.binding = binding
def push(self):
raise Z3Exception("push needs to be overwritten")

4
src/api/python/z3/z3printer.py
View file

@ -831,7 +831,7 @@ class Formatter:
else:
_z3_assert(z3.is_fp_value(a), "expecting FP num ast")
r = []
sgn = c_int(0)
sgn = ctypes.c_bool()
sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False)
sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast)
@ -861,7 +861,7 @@ class Formatter:
else:
_z3_assert(z3.is_fp_value(a), "expecting FP num ast")
r = []
sgn = (ctypes.c_int)(0)
sgn = ctypes.c_bool()
sgnb = Z3_fpa_get_numeral_sign(a.ctx_ref(), a.ast, byref(sgn))
exp = Z3_fpa_get_numeral_exponent_string(a.ctx_ref(), a.ast, False)
sig = Z3_fpa_get_numeral_significand_string(a.ctx_ref(), a.ast)

81
src/api/z3_api.h
View file

@ -1037,8 +1037,6 @@ typedef enum {
Z3_OP_SET_SUBSET,
Z3_OP_AS_ARRAY,
Z3_OP_ARRAY_EXT,
Z3_OP_SET_HAS_SIZE,
Z3_OP_SET_CARD,
// Bit-vectors
Z3_OP_BNUM = 0x400,
@ -1440,6 +1438,7 @@ Z3_DECLARE_CLOSURE(Z3_eq_eh, void, (void* ctx, Z3_solver_callback cb, Z3_as
Z3_DECLARE_CLOSURE(Z3_final_eh, void, (void* ctx, Z3_solver_callback cb));
Z3_DECLARE_CLOSURE(Z3_created_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t));
Z3_DECLARE_CLOSURE(Z3_decide_eh, void, (void* ctx, Z3_solver_callback cb, Z3_ast t, unsigned idx, bool phase));
Z3_DECLARE_CLOSURE(Z3_on_binding_eh, bool, (void* ctx, Z3_solver_callback cb, Z3_ast q, Z3_ast inst));
Z3_DECLARE_CLOSURE(Z3_on_clause_eh, void, (void* ctx, Z3_ast proof_hint, unsigned n, unsigned const* deps, Z3_ast_vector literals));
@ -2126,6 +2125,33 @@ extern "C" {
unsigned num_constructors,
Z3_constructor constructors[]);
/**
\brief Create a parametric datatype with explicit type parameters.
This function is similar to #Z3_mk_datatype, except it takes an explicit set of type parameters.
The parameters can be type variables created with #Z3_mk_type_variable, allowing the definition
of polymorphic datatypes that can be instantiated with different concrete types.
\param c logical context
\param name name of the datatype
\param num_parameters number of type parameters (can be 0)
\param parameters array of type parameters (type variables or concrete sorts)
\param num_constructors number of constructors
\param constructors array of constructor specifications
\sa Z3_mk_datatype
\sa Z3_mk_type_variable
\sa Z3_mk_datatype_sort
def_API('Z3_mk_polymorphic_datatype', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(UINT), _inout_array(4, CONSTRUCTOR)))
*/
Z3_sort Z3_API Z3_mk_polymorphic_datatype(Z3_context c,
Z3_symbol name,
unsigned num_parameters,
Z3_sort parameters[],
unsigned num_constructors,
Z3_constructor constructors[]);
/**
\brief create a forward reference to a recursive datatype being declared.
The forward reference can be used in a nested occurrence: the range of an array
@ -2135,9 +2161,14 @@ extern "C" {
Forward references can replace the use sort references, that are unsigned integers
in the \c Z3_mk_constructor call
def_API('Z3_mk_datatype_sort', SORT, (_in(CONTEXT), _in(SYMBOL)))
\param c logical context
\param name name of the datatype
\param num_params number of sort parameters
\param params array of sort parameters
def_API('Z3_mk_datatype_sort', SORT, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT)))
*/
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name);
Z3_sort Z3_API Z3_mk_datatype_sort(Z3_context c, Z3_symbol name, unsigned num_params, Z3_sort const params[]);
/**
\brief Create list of constructors.
@ -3283,12 +3314,6 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_as_array(Z3_context c, Z3_func_decl f);
/**
\brief Create predicate that holds if Boolean array \c set has \c k elements set to true.
def_API('Z3_mk_set_has_size', AST, (_in(CONTEXT), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_set_has_size(Z3_context c, Z3_ast set, Z3_ast k);
/**@}*/
@ -3767,6 +3792,27 @@ extern "C" {
*/
Z3_ast Z3_API Z3_mk_seq_replace(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
/**
\brief Replace all occurrences of \c src with \c dst in \c s.
def_API('Z3_mk_seq_replace_all', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_replace_all(Z3_context c, Z3_ast s, Z3_ast src, Z3_ast dst);
/**
\brief Replace the first occurrence of regular expression \c re with \c dst in \c s.
def_API('Z3_mk_seq_replace_re', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_replace_re(Z3_context c, Z3_ast s, Z3_ast re, Z3_ast dst);
/**
\brief Replace all occurrences of regular expression \c re with \c dst in \c s.
def_API('Z3_mk_seq_replace_re_all', AST ,(_in(CONTEXT), _in(AST), _in(AST), _in(AST)))
*/
Z3_ast Z3_API Z3_mk_seq_replace_re_all(Z3_context c, Z3_ast s, Z3_ast re, Z3_ast dst);
/**
\brief Retrieve from \c s the unit sequence positioned at position \c index.
The sequence is empty if the index is out of bounds.
@ -5823,7 +5869,7 @@ extern "C" {
\sa Z3_append_log
\sa Z3_close_log
extra_API('Z3_open_log', INT, (_in(STRING),))
extra_API('Z3_open_log', BOOL, (_in(STRING),))
*/
bool Z3_API Z3_open_log(Z3_string filename);
@ -7086,7 +7132,7 @@ extern "C" {
\brief retrieve the decision depth of Boolean literals (variables or their negations).
Assumes a check-sat call and no other calls (to extract models) have been invoked.
def_API('Z3_solver_get_levels', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(UINT), _in_array(3, UINT)))
def_API('Z3_solver_get_levels', VOID, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR), _in(UINT), _out_array(3, UINT)))
*/
void Z3_API Z3_solver_get_levels(Z3_context c, Z3_solver s, Z3_ast_vector literals, unsigned sz, unsigned levels[]);
@ -7225,6 +7271,17 @@ extern "C" {
*/
void Z3_API Z3_solver_propagate_decide(Z3_context c, Z3_solver s, Z3_decide_eh decide_eh);
/**
\brief register a callback when the solver instantiates a quantifier.
If the callback returns false, the actual instantiation of the quantifier is blocked.
This allows the user propagator selectively prioritize instantiations without relying on default
or configured weights.
def_API('Z3_solver_propagate_on_binding', VOID, (_in(CONTEXT), _in(SOLVER), _fnptr(Z3_on_binding_eh)))
*/
void Z3_API Z3_solver_propagate_on_binding(Z3_context c, Z3_solver s, Z3_on_binding_eh on_binding_eh);
/**
Sets the next (registered) expression to split on.
The function returns false and ignores the given expression in case the expression is already assigned internally

22
src/api/z3_fpa.h
View file

@ -1089,6 +1089,22 @@ extern "C" {
*/
unsigned Z3_API Z3_fpa_get_sbits(Z3_context c, Z3_sort s);
/**
\brief Checks whether a given ast is a floating-point numeral.
\param c logical context
\param t an ast
\sa Z3_fpa_is_numeral_nan
\sa Z3_fpa_is_numeral_inf
\sa Z3_fpa_is_numeral_normal
\sa Z3_fpa_is_numeral_subnormal
\sa Z3_fpa_is_numeral_zero
def_API('Z3_fpa_is_numeral', BOOL, (_in(CONTEXT), _in(AST)))
*/
bool Z3_API Z3_fpa_is_numeral(Z3_context c, Z3_ast t);
/**
\brief Checks whether a given floating-point numeral is a NaN.
@ -1220,12 +1236,12 @@ extern "C" {
\param sgn the retrieved sign
\returns true if \c t corresponds to a floating point numeral, otherwise invokes exception handler or returns false
Remarks: sets \c sgn to 0 if `t' is positive and to 1 otherwise, except for
Remarks: sets \c sgn to \c false if `t' is positive and to \c true otherwise, except for
NaN, which is an invalid argument.
def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(INT)))
def_API('Z3_fpa_get_numeral_sign', BOOL, (_in(CONTEXT), _in(AST), _out(BOOL)))
*/
bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, int * sgn);
bool Z3_API Z3_fpa_get_numeral_sign(Z3_context c, Z3_ast t, bool * sgn);
/**
\brief Return the significand value of a floating-point numeral as a string.

17
src/api/z3_optimization.h
View file

@ -379,6 +379,23 @@ extern "C" {
void* ctx,
Z3_model_eh model_eh);
/**
\brief Copy an optimization context from a source to a target context.
This function allows translating an optimization context from one Z3_context
to another. This is useful when working with multiple contexts and needing to
transfer optimization problems between them.
\param c Source context containing the optimization context to translate
\param o The optimization context to translate from the source context
\param target Target context where the optimization context will be created
\return A new optimization context in the target context with the same state
def_API('Z3_optimize_translate', OPTIMIZE, (_in(CONTEXT), _in(OPTIMIZE), _in(CONTEXT)))
*/
Z3_optimize Z3_API Z3_optimize_translate(Z3_context c, Z3_optimize o, Z3_context target);
/**@}*/
/**@}*/

4
src/api/z3_rcf.h
View file

@ -272,9 +272,9 @@ extern "C" {
\pre Z3_rcf_is_algebraic(ctx, a);
def_API('Z3_rcf_interval', INT, (_in(CONTEXT), _in(RCF_NUM), _out(INT), _out(INT), _out(RCF_NUM), _out(INT), _out(INT), _out(RCF_NUM)))
def_API('Z3_rcf_interval', INT, (_in(CONTEXT), _in(RCF_NUM), _out(BOOL), _out(BOOL), _out(RCF_NUM), _out(BOOL), _out(BOOL), _out(RCF_NUM)))
*/
int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, int * lower_is_inf, int * lower_is_open, Z3_rcf_num * lower, int * upper_is_inf, int * upper_is_open, Z3_rcf_num * upper);
int Z3_API Z3_rcf_interval(Z3_context c, Z3_rcf_num a, bool * lower_is_inf, bool * lower_is_open, Z3_rcf_num * lower, bool * upper_is_inf, bool * upper_is_open, Z3_rcf_num * upper);
/**
\brief Return the number of sign conditions of an algebraic number.

9
src/api/z3_replayer.cpp
View file

@ -662,6 +662,11 @@ struct z3_replayer::imp {
return v.data();
}
bool * get_bool_addr(unsigned pos) {
check_arg(pos, INT64);
return reinterpret_cast<bool*>(&(m_args[pos].m_int));
}
int * get_int_addr(unsigned pos) {
check_arg(pos, INT64);
return reinterpret_cast<int*>(&(m_args[pos].m_int));
@ -790,6 +795,10 @@ void ** z3_replayer::get_obj_array(unsigned pos) const {
return m_imp->get_obj_array(pos);
}
bool * z3_replayer::get_bool_addr(unsigned pos) {
return m_imp->get_bool_addr(pos);
}
int * z3_replayer::get_int_addr(unsigned pos) {
return m_imp->get_int_addr(pos);
}

1
src/api/z3_replayer.h
View file

@ -53,6 +53,7 @@ public:
Z3_symbol * get_symbol_array(unsigned pos) const;
void ** get_obj_array(unsigned pos) const;
bool * get_bool_addr(unsigned pos);
int * get_int_addr(unsigned pos);
int64_t * get_int64_addr(unsigned pos);
unsigned * get_uint_addr(unsigned pos);

10
src/ast/arith_decl_plugin.cpp
View file

@ -188,8 +188,12 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
m_to_real_decl = m->mk_func_decl(symbol("to_real"), i, r, func_decl_info(id, OP_TO_REAL));
m->inc_ref(m_to_real_decl);
m_r_to_real_decl = m->mk_func_decl(symbol("to_real"), r, r, func_decl_info(id, OP_TO_REAL));
m->inc_ref(m_r_to_real_decl);
m_to_int_decl = m->mk_func_decl(symbol("to_int"), r, i, func_decl_info(id, OP_TO_INT));
m->inc_ref(m_to_int_decl);
m_i_to_int_decl = m->mk_func_decl(symbol("to_int"), i, i, func_decl_info(id, OP_TO_INT));
m->inc_ref(m_i_to_int_decl);
m_is_int_decl = m->mk_func_decl(symbol("is_int"), r, m->mk_bool_sort(), func_decl_info(id, OP_IS_INT));
m->inc_ref(m_is_int_decl);
@ -311,6 +315,8 @@ void arith_decl_plugin::finalize() {
DEC_REF(m_i_rem_decl);
DEC_REF(m_to_real_decl);
DEC_REF(m_to_int_decl);
DEC_REF(m_r_to_real_decl);
DEC_REF(m_i_to_int_decl);
DEC_REF(m_is_int_decl);
DEC_REF(m_i_power_decl);
DEC_REF(m_r_power_decl);
@ -368,8 +374,8 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
return m_manager->mk_func_decl(symbol("^0"), m_real_decl, m_real_decl, m_real_decl, func_decl_info(m_family_id, OP_POWER0));
}
return m_manager->mk_func_decl(symbol("^0"), m_int_decl, m_int_decl, m_real_decl, func_decl_info(m_family_id, OP_POWER0));
case OP_TO_REAL: return m_to_real_decl;
case OP_TO_INT: return m_to_int_decl;
case OP_TO_REAL: return is_real ? m_r_to_real_decl : m_to_real_decl;
case OP_TO_INT: return is_real ? m_to_int_decl : m_i_to_int_decl;
case OP_IS_INT: return m_is_int_decl;
case OP_POWER: return is_real ? m_r_power_decl : m_i_power_decl;
case OP_ABS: return is_real ? m_r_abs_decl : m_i_abs_decl;

12
src/ast/arith_decl_plugin.h
View file

@ -120,11 +120,13 @@ protected:
func_decl * m_i_mod_decl;
func_decl * m_i_rem_decl;
func_decl * m_to_real_decl;
func_decl * m_to_int_decl;
func_decl * m_is_int_decl;
func_decl * m_r_power_decl;
func_decl * m_i_power_decl;
func_decl * m_to_real_decl = nullptr;
func_decl * m_to_int_decl = nullptr;
func_decl * m_r_to_real_decl = nullptr;
func_decl * m_i_to_int_decl = nullptr;
func_decl * m_is_int_decl = nullptr;
func_decl * m_r_power_decl = nullptr;
func_decl * m_i_power_decl = nullptr;
func_decl * m_r_abs_decl;
func_decl * m_i_abs_decl;

42
src/ast/array_decl_plugin.cpp
View file

@ -35,9 +35,7 @@ array_decl_plugin::array_decl_plugin():
m_set_complement_sym("complement"),
m_set_subset_sym("subset"),
m_array_ext_sym("array-ext"),
m_as_array_sym("as-array"),
m_set_has_size_sym("set-has-size"),
m_set_card_sym("card") {
m_as_array_sym("as-array") {
}
#define ARRAY_SORT_STR "Array"
@ -442,40 +440,6 @@ func_decl * array_decl_plugin::mk_set_subset(unsigned arity, sort * const * doma
func_decl_info(m_family_id, OP_SET_SUBSET));
}
func_decl * array_decl_plugin::mk_set_card(unsigned arity, sort * const* domain) {
if (arity != 1) {
m_manager->raise_exception("card takes only one argument");
return nullptr;
}
arith_util arith(*m_manager);
if (!is_array_sort(domain[0]) || !m_manager->is_bool(get_array_range(domain[0]))) {
m_manager->raise_exception("card expects an array of Booleans");
}
sort * int_sort = arith.mk_int();
return m_manager->mk_func_decl(m_set_card_sym, arity, domain, int_sort,
func_decl_info(m_family_id, OP_SET_CARD));
}
func_decl * array_decl_plugin::mk_set_has_size(unsigned arity, sort * const* domain) {
if (arity != 2) {
m_manager->raise_exception("set-has-size takes two arguments");
return nullptr;
}
m_manager->raise_exception("set-has-size is not supported");
// domain[0] is a Boolean array,
// domain[1] is Int
arith_util arith(*m_manager);
if (!arith.is_int(domain[1])) {
m_manager->raise_exception("set-has-size expects second argument to be an integer");
}
if (!is_array_sort(domain[0]) || !m_manager->is_bool(get_array_range(domain[0]))) {
m_manager->raise_exception("set-has-size expects first argument to be an array of Booleans");
}
sort * bool_sort = m_manager->mk_bool_sort();
return m_manager->mk_func_decl(m_set_has_size_sym, arity, domain, bool_sort,
func_decl_info(m_family_id, OP_SET_HAS_SIZE));
}
func_decl * array_decl_plugin::mk_as_array(func_decl * f) {
vector<parameter> parameters;
@ -541,10 +505,6 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
return mk_set_complement(arity, domain);
case OP_SET_SUBSET:
return mk_set_subset(arity, domain);
case OP_SET_HAS_SIZE:
return mk_set_has_size(arity, domain);
case OP_SET_CARD:
return mk_set_card(arity, domain);
case OP_AS_ARRAY: {
if (num_parameters != 1 ||
!parameters[0].is_ast() ||

20
src/ast/array_decl_plugin.h
View file

@ -62,8 +62,6 @@ enum array_op_kind {
OP_SET_DIFFERENCE,
OP_SET_COMPLEMENT,
OP_SET_SUBSET,
OP_SET_HAS_SIZE,
OP_SET_CARD,
OP_AS_ARRAY, // used for model construction
LAST_ARRAY_OP
};
@ -81,8 +79,6 @@ class array_decl_plugin : public decl_plugin {
symbol m_set_subset_sym;
symbol m_array_ext_sym;
symbol m_as_array_sym;
symbol m_set_has_size_sym;
symbol m_set_card_sym;
bool check_set_arguments(unsigned arity, sort * const * domain);
@ -110,10 +106,6 @@ class array_decl_plugin : public decl_plugin {
func_decl * mk_as_array(func_decl * f);
func_decl* mk_set_has_size(unsigned arity, sort * const* domain);
func_decl* mk_set_card(unsigned arity, sort * const* domain);
bool is_array_sort(sort* s) const;
public:
array_decl_plugin();
@ -173,8 +165,6 @@ public:
bool is_complement(expr* n) const { return is_app_of(n, m_fid, OP_SET_COMPLEMENT); }
bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); }
bool is_as_array(expr * n, func_decl*& f) const { return is_as_array(n) && (f = get_as_array_func_decl(n), true); }
bool is_set_has_size(expr* e) const { return is_app_of(e, m_fid, OP_SET_HAS_SIZE); }
bool is_set_card(expr* e) const { return is_app_of(e, m_fid, OP_SET_CARD); }
bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); }
bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); }
bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); }
@ -182,8 +172,6 @@ public:
bool is_union(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_UNION); }
bool is_intersect(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_INTERSECT); }
bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); }
bool is_set_has_size(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_HAS_SIZE); }
bool is_set_card(func_decl* f) const { return is_decl_of(f, m_fid, OP_SET_CARD); }
bool is_default(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_DEFAULT); }
bool is_default(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_DEFAULT); }
bool is_subset(expr const* n) const { return is_app_of(n, m_fid, OP_SET_SUBSET); }
@ -307,14 +295,6 @@ public:
return m_manager.mk_app(m_fid, OP_SET_UNION, s1, s2);
}
app* mk_has_size(expr* set, expr* n) {
return m_manager.mk_app(m_fid, OP_SET_HAS_SIZE, set, n);
}
app* mk_card(expr* set) {
return m_manager.mk_app(m_fid, OP_SET_CARD, set);
}
func_decl * mk_array_ext(sort* domain, unsigned i);
sort * mk_array_sort(sort* dom, sort* range) { return mk_array_sort(1, &dom, range); }

2
src/ast/converters/generic_model_converter.h
View file

@ -54,8 +54,6 @@ public:
void operator()(model_ref & md) override;
void operator()(expr_ref& fml) override { UNREACHABLE(); }
void cancel() override {}
void display(std::ostream & out) override;

10
src/ast/converters/model_converter.cpp
View file

@ -93,11 +93,6 @@ public:
this->m_c1->operator()(m);
}
void operator()(expr_ref & fml) override {
this->m_c2->operator()(fml);
this->m_c1->operator()(fml);
}
void operator()(labels_vec & r) override {
this->m_c2->operator()(r);
this->m_c1->operator()(r);
@ -157,11 +152,6 @@ public:
r.append(m_labels.size(), m_labels.data());
}
void operator()(expr_ref& fml) override {
model::scoped_model_completion _scm(m_model, false);
fml = (*m_model)(fml);
}
void get_units(obj_map<expr, bool>& fmls) override {
// no-op
}

2
src/ast/converters/model_converter.h
View file

@ -76,8 +76,6 @@ public:
virtual void operator()(model_ref & m) = 0;
virtual void operator()(labels_vec & r) {}
virtual void operator()(expr_ref& fml) { UNREACHABLE(); }
virtual model_converter * translate(ast_translation & translator) = 0;

2
src/ast/datatype_decl_plugin.cpp
View file

@ -305,7 +305,7 @@ namespace datatype {
sort* s = m_manager->mk_sort(name.get_symbol(),
sort_info(m_family_id, k, num_parameters, parameters, true));
def* d = nullptr;
if (m_defs.find(s->get_name(), d) && d->sort_size()) {
if (m_defs.find(s->get_name(), d) && d->sort_size() && d->params().size() == num_parameters - 1) {
obj_map<sort, sort_size> S;
for (unsigned i = 0; i + 1 < num_parameters; ++i) {
sort* r = to_sort(parameters[i + 1].get_ast());

914
src/ast/euf/euf_ac_plugin.cpp
View file

File diff suppressed because it is too large Load diff

122
src/ast/euf/euf_ac_plugin.h
View file

@ -36,37 +36,19 @@ namespace euf {
class ac_plugin : public plugin {
// enode structure for AC equivalences
struct node {
enode* n; // associated enode
node* root; // path compressed root
node* next; // next in equivalence class
justification j; // justification for equality
node* target = nullptr; // justified next
unsigned_vector shared; // shared occurrences
unsigned_vector eqs; // equality occurrences
unsigned id() const { return root->n->get_id(); }
static node* mk(region& r, enode* n);
struct stats {
unsigned m_num_superpositions = 0;// number of superpositions
};
class equiv {
node& n;
public:
class iterator {
node* m_first;
node* m_last;
public:
iterator(node* n, node* m) : m_first(n), m_last(m) {}
node* operator*() { return m_first; }
iterator& operator++() { if (!m_last) m_last = m_first; m_first = m_first->next; return *this; }
iterator operator++(int) { iterator tmp = *this; ++*this; return tmp; }
bool operator!=(iterator const& other) const { return m_last != other.m_last || m_first != other.m_first; }
};
equiv(node& _n) :n(_n) {}
equiv(node* _n) :n(*_n) {}
iterator begin() const { return iterator(&n, nullptr); }
iterator end() const { return iterator(&n, &n); }
// enode structure for AC equivalences
struct node {
enode* n; // associated enode
unsigned_vector shared; // shared occurrences
unsigned_vector eqs; // equality occurrences
bool is_zero = false;
unsigned id() const { return n->get_id(); }
static node* mk(region& r, enode* n);
};
struct bloom {
@ -75,7 +57,7 @@ namespace euf {
};
enum eq_status {
processed, to_simplify, is_dead
is_processed_eq, is_passive_eq, is_to_simplify_eq, is_reducing_eq, is_dead_eq
};
// represent equalities added by merge_eh and by superposition
@ -83,7 +65,7 @@ namespace euf {
eq(unsigned l, unsigned r, justification j):
l(l), r(r), j(j) {}
unsigned l, r; // refer to monomials
eq_status status = to_simplify;
eq_status status = is_to_simplify_eq;
justification j; // justification for equality
};
@ -140,7 +122,8 @@ namespace euf {
decl_kind m_op = null_decl_kind;
func_decl* m_decl = nullptr;
bool m_is_injective = false;
vector<eq> m_eqs;
vector<eq> m_active, m_passive;
enode_pair_vector m_queued;
ptr_vector<node> m_nodes;
bool_vector m_shared_nodes;
vector<monomial_t> m_monomials;
@ -149,6 +132,11 @@ namespace euf {
tracked_uint_set m_to_simplify_todo;
tracked_uint_set m_shared_todo;
uint64_t m_tick = 1;
symbol m_name;
unsigned m_fuel = 0;
unsigned m_fuel_inc = 3;
stats m_stats;
mutable symbol m_superposition_stats, m_eqs_stats;
@ -159,22 +147,21 @@ namespace euf {
// backtrackable state
enum undo_kind {
is_add_eq,
is_queue_eq,
is_add_monomial,
is_add_node,
is_merge_node,
is_update_eq,
is_add_shared_index,
is_add_eq_index,
is_register_shared,
is_update_shared
is_update_shared,
is_push_scope
};
svector<undo_kind> m_undo;
ptr_vector<node> m_node_trail;
unsigned m_queue_head = 0;
svector<std::pair<unsigned, shared>> m_update_shared_trail;
svector<std::tuple<node*, unsigned, unsigned>> m_merge_trail;
svector<std::pair<unsigned, eq>> m_update_eq_trail;
@ -192,6 +179,7 @@ namespace euf {
enode* from_monomial(ptr_vector<node> const& m);
monomial_t const& monomial(unsigned i) const { return m_monomials[i]; }
monomial_t& monomial(unsigned i) { return m_monomials[i]; }
void sort(monomial_t& monomial);
bool is_sorted(monomial_t const& monomial) const;
uint64_t filter(monomial_t& m);
@ -199,17 +187,42 @@ namespace euf {
bool can_be_subset(monomial_t& subset, ptr_vector<node> const& m, bloom& b);
bool are_equal(ptr_vector<node> const& a, ptr_vector<node> const& b);
bool are_equal(monomial_t& a, monomial_t& b);
bool backward_subsumes(unsigned src_eq, unsigned dst_eq);
bool are_equal(eq const& a, eq const& b) {
return are_equal(monomial(a.l), monomial(b.l)) && are_equal(monomial(a.r), monomial(b.r));
}
bool bloom_filter_is_correct(ptr_vector<node> const& m, bloom const& b) const;
bool well_formed(eq const& e) const;
bool is_reducing(eq const& e) const;
void backward_reduce(unsigned eq_id);
void backward_reduce(eq const& eq, unsigned dst);
bool backward_reduce_monomial(eq const& src, eq & dst, monomial_t& m);
void forward_subsume_new_eqs();
bool is_forward_subsumed(unsigned dst_eq);
bool forward_subsumes(unsigned src_eq, unsigned dst_eq);
bool backward_subsumes(unsigned src_eq, unsigned dst_eq);
void init_equation(eq const& e);
enode_vector m_units;
enode* get_unit(enode* n) const {
for (auto u : m_units) {
if (u->get_sort() == n->get_sort())
return u;
}
UNREACHABLE();
return nullptr;
}
bool init_equation(eq e, bool is_active);
void push_equation(enode* l, enode* r);
void pop_equation(enode* l, enode* r);
bool orient_equation(eq& e);
void set_status(unsigned eq_id, eq_status s);
unsigned pick_next_eq();
void forward_simplify(unsigned eq_id, unsigned using_eq);
bool backward_simplify(unsigned eq_id, unsigned using_eq);
unsigned_vector m_new_eqs;
void backward_simplify(unsigned eq_id, unsigned using_eq);
bool forward_simplify(unsigned eq_id, unsigned using_eq);
bool superpose(unsigned src_eq, unsigned dst_eq);
void deduplicate(monomial_t& a, monomial_t& b);
void deduplicate(ptr_vector<node>& a, ptr_vector<node>& b);
ptr_vector<node> m_src_r, m_src_l, m_dst_r, m_dst_l;
@ -228,9 +241,9 @@ namespace euf {
unsigned_vector m_eq_occurs;
bool_vector m_eq_seen;
unsigned_vector const& forward_iterator(unsigned eq);
unsigned_vector const& superpose_iterator(unsigned eq);
unsigned_vector const& backward_iterator(unsigned eq);
unsigned_vector const& superpose_iterator(unsigned eq);
unsigned_vector const& forward_iterator(unsigned eq);
void init_ref_counts(monomial_t const& monomial, ref_counts& counts) const;
void init_ref_counts(ptr_vector<node> const& monomial, ref_counts& counts) const;
void init_overlap_iterator(unsigned eq, monomial_t const& m);
@ -246,14 +259,15 @@ namespace euf {
bool reduce(ptr_vector<node>& m, justification& j);
void index_new_r(unsigned eq, monomial_t const& old_r, monomial_t const& new_r);
bool is_to_simplify(unsigned eq) const { return m_eqs[eq].status == eq_status::to_simplify; }
bool is_processed(unsigned eq) const { return m_eqs[eq].status == eq_status::processed; }
bool is_alive(unsigned eq) const { return m_eqs[eq].status != eq_status::is_dead; }
bool is_to_simplify(unsigned eq) const { return m_active[eq].status == eq_status::is_to_simplify_eq; }
bool is_processed(unsigned eq) const { return m_active[eq].status == eq_status::is_processed_eq; }
bool is_reducing(unsigned eq) const { return m_active[eq].status == eq_status::is_reducing_eq; }
bool is_active(unsigned eq) const { return m_active[eq].status != eq_status::is_dead_eq; }
justification justify_rewrite(unsigned eq1, unsigned eq2);
justification::dependency* justify_equation(unsigned eq);
justification::dependency* justify_monomial(justification::dependency* d, monomial_t const& m);
justification join(justification j1, unsigned eq);
justification join(justification j1, eq const& eq);
bool is_correct_ref_count(monomial_t const& m, ref_counts const& counts) const;
bool is_correct_ref_count(ptr_vector<node> const& m, ref_counts const& counts) const;
@ -273,11 +287,15 @@ namespace euf {
public:
ac_plugin(egraph& g, unsigned fid, unsigned op);
ac_plugin(egraph& g, char const* name, unsigned fid, unsigned op);
ac_plugin(egraph& g, func_decl* f);
void set_injective() { m_is_injective = true; }
void add_unit(enode*);
void add_zero(enode*);
theory_id get_id() const override { return m_fid; }
@ -289,23 +307,27 @@ namespace euf {
void undo() override;
void push_scope_eh() override;
void propagate() override;
std::ostream& display(std::ostream& out) const override;
void collect_statistics(statistics& st) const override;
void set_undo(std::function<void(void)> u) { m_undo_notify = u; }
struct eq_pp {
ac_plugin const& p; eq const& e;
eq_pp(ac_plugin const& p, eq const& e) : p(p), e(e) {};
eq_pp(ac_plugin const& p, unsigned eq_id): p(p), e(p.m_eqs[eq_id]) {}
eq_pp(ac_plugin const& p, unsigned eq_id): p(p), e(p.m_active[eq_id]) {}
std::ostream& display(std::ostream& out) const { return p.display_equation(out, e); }
};
struct eq_pp_ll {
ac_plugin const& p; eq const& e;
eq_pp_ll(ac_plugin const& p, eq const& e) : p(p), e(e) {};
eq_pp_ll(ac_plugin const& p, unsigned eq_id) : p(p), e(p.m_eqs[eq_id]) {}
eq_pp_ll(ac_plugin const& p, unsigned eq_id) : p(p), e(p.m_active[eq_id]) {}
std::ostream& display(std::ostream& out) const { return p.display_equation_ll(out, e); }
};

50
src/ast/euf/euf_arith_plugin.cpp
View file

@ -24,19 +24,63 @@ namespace euf {
arith_plugin::arith_plugin(egraph& g) :
plugin(g),
a(g.get_manager()),
m_add(g, get_id(), OP_ADD),
m_mul(g, get_id(), OP_MUL) {
m_add(g, "add", get_id(), OP_ADD),
m_mul(g, "mul", get_id(), OP_MUL) {
std::function<void(void)> uadd = [&]() { m_undo.push_back(undo_t::undo_add); };
m_add.set_undo(uadd);
std::function<void(void)> umul = [&]() { m_undo.push_back(undo_t::undo_mul); };
m_mul.set_undo(umul);
m_add.set_injective();
auto e = a.mk_int(0);
auto n = g.find(e) ? g.find(e) : g.mk(e, 0, 0, nullptr);
m_add.add_unit(n);
m_mul.add_zero(n);
e = a.mk_real(0);
n = g.find(e) ? g.find(e) : g.mk(e, 0, 0, nullptr);
m_add.add_unit(n);
m_mul.add_zero(n);
e = a.mk_int(1);
n = g.find(e) ? g.find(e) : g.mk(e, 0, 0, nullptr);
m_mul.add_unit(n);
e = a.mk_real(1);
n = g.find(e) ? g.find(e) : g.mk(e, 0, 0, nullptr);
m_mul.add_unit(n);
}
void arith_plugin::register_node(enode* n) {
TRACE(plugin, tout << g.bpp(n) << "\n");
m_add.register_node(n);
m_mul.register_node(n);
expr* e = n->get_expr(), * x, * y;
// x - y = x + (* -1 y)
if (a.is_sub(e, x, y)) {
auto e1 = a.mk_numeral(rational(-1), a.is_int(x));
auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr);
auto e2 = a.mk_mul(e1, y);
enode* es1[2] = { n1, g.find(y)};
auto mul = g.find(e2) ? g.find(e2) : g.mk(e2, 0, 2, es1);
enode* es2[2] = { g.find(x), mul };
expr* e_add = a.mk_add(x, e2);
auto add = g.find(e_add) ? g.find(e_add): g.mk(e_add, 0, 2, es2);
push_merge(n, add);
}
// c1 * c2 = c1*c2
rational r1, r2;
if (a.is_mul(e, x, y) && a.is_numeral(x, r1) && a.is_numeral(y, r2)) {
rational r = r1 * r2;
auto e1 = a.mk_numeral(r, a.is_int(x));
auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr);
push_merge(n, n1);
}
if (a.is_uminus(e, x)) {
NOT_IMPLEMENTED_YET();
}
}
void arith_plugin::merge_eh(enode* n1, enode* n2) {
@ -66,9 +110,7 @@ namespace euf {
}
std::ostream& arith_plugin::display(std::ostream& out) const {
out << "add\n";
m_add.display(out);
out << "mul\n";
m_mul.display(out);
return out;
}

10
src/ast/euf/euf_arith_plugin.h
View file

@ -43,9 +43,19 @@ namespace euf {
void undo() override;
void push_scope_eh() override {
m_add.push_scope_eh();
m_mul.push_scope_eh();
}
void propagate() override;
std::ostream& display(std::ostream& out) const override;
void collect_statistics(statistics& st) const override {
m_add.collect_statistics(st);
m_mul.collect_statistics(st);
}
};
}

52
src/ast/euf/euf_egraph.cpp
View file

@ -103,6 +103,9 @@ namespace euf {
m_scopes.push_back(m_updates.size());
m_region.push_scope();
m_updates.push_back(update_record(m_new_th_eqs_qhead, update_record::new_th_eq_qhead()));
for (auto p : m_plugins)
if (p)
p->push_scope_eh();
}
SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size());
}
@ -117,6 +120,7 @@ namespace euf {
enode* egraph::mk(expr* f, unsigned generation, unsigned num_args, enode *const* args) {
SASSERT(!find(f));
TRACE(euf, tout << "mk: " << mk_bounded_pp(f, m) << " generation: " << generation << " num_args: " << num_args << "\n";);
force_push();
enode *n = mk_enode(f, generation, num_args, args);
@ -157,6 +161,21 @@ namespace euf {
}
void egraph::propagate_plugins() {
if (m_plugins.empty())
return;
if (m_plugin_qhead < m_new_th_eqs.size())
m_updates.push_back(update_record(m_plugin_qhead, update_record::plugin_qhead()));
for (; m_plugin_qhead < m_new_th_eqs.size(); ++m_plugin_qhead) {
auto const& eq = m_new_th_eqs[m_plugin_qhead];
auto* p = get_plugin(eq.id());
if (!p)
continue;
if (eq.is_eq())
p->merge_eh(eq.child(), eq.root());
else
p->diseq_eh(eq.eq());
}
for (auto* p : m_plugins)
if (p)
p->propagate();
@ -167,23 +186,18 @@ namespace euf {
m_new_th_eqs.push_back(th_eq(id, v1, v2, c, r));
m_updates.push_back(update_record(update_record::new_th_eq()));
++m_stats.m_num_th_eqs;
auto* p = get_plugin(id);
if (p)
p->merge_eh(c, r);
}
void egraph::add_th_diseq(theory_id id, theory_var v1, theory_var v2, enode* eq) {
if (!th_propagates_diseqs(id))
return;
TRACE(euf_verbose, tout << "eq: " << v1 << " != " << v2 << "\n";);
m_new_th_eqs.push_back(th_eq(id, v1, v2, eq->get_expr()));
m_new_th_eqs.push_back(th_eq(id, v1, v2, eq));
m_updates.push_back(update_record(update_record::new_th_eq()));
auto* p = get_plugin(id);
if (p)
p->diseq_eh(eq);
++m_stats.m_num_th_diseqs;
}
void egraph::add_literal(enode* n, enode* ante) {
TRACE(euf, tout << "propagate " << bpp(n) << " " << bpp(ante) << "\n");
if (!m_on_propagate_literal)
@ -447,6 +461,9 @@ namespace euf {
case update_record::tag_t::is_new_th_eq_qhead:
m_new_th_eqs_qhead = p.qhead;
break;
case update_record::tag_t::is_plugin_qhead:
m_plugin_qhead = p.qhead;
break;
case update_record::tag_t::is_inconsistent:
m_inconsistent = p.m_inconsistent;
break;
@ -546,16 +563,18 @@ namespace euf {
void egraph::remove_parents(enode* r) {
TRACE(euf_verbose, tout << bpp(r) << "\n");
SASSERT(all_of(enode_parents(r), [&](enode* p) { return !p->is_marked1(); }));
TRACE(euf, tout << "remove_parents " << bpp(r) << "\n");
for (enode* p : enode_parents(r)) {
if (p->is_marked1())
continue;
if (p->cgc_enabled()) {
if (!p->is_cgr())
continue;
TRACE(euf, tout << "removing " << m_table.contains_ptr(p) << " " << bpp(p) << "\n");
SASSERT(m_table.contains_ptr(p));
p->mark1();
erase_from_table(p);
CTRACE(euf_verbose, m_table.contains_ptr(p), tout << bpp(p) << "\n"; display(tout));
CTRACE(euf, m_table.contains_ptr(p), tout << bpp(p) << "\n"; display(tout));
SASSERT(!m_table.contains_ptr(p));
}
else if (p->is_equality())
@ -564,15 +583,16 @@ namespace euf {
}
void egraph::reinsert_parents(enode* r1, enode* r2) {
TRACE(euf, tout << "reinsert_parents " << bpp(r1) << " " << bpp(r2) << "\n";);
for (enode* p : enode_parents(r1)) {
if (!p->is_marked1())
continue;
p->unmark1();
TRACE(euf_verbose, tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->cgc_enabled() << "\n";);
TRACE(euf, tout << "reinsert " << bpp(r1) << " " << bpp(r2) << " " << bpp(p) << " " << p->cgc_enabled() << "\n";);
if (p->cgc_enabled()) {
auto [p_other, comm] = insert_table(p);
SASSERT(m_table.contains_ptr(p) == (p_other == p));
CTRACE(euf_verbose, p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n");
CTRACE(euf, p_other != p, tout << "reinsert " << bpp(p) << " == " << bpp(p_other) << " " << p->value() << " " << p_other->value() << "\n");
if (p_other != p)
m_to_merge.push_back(to_merge(p_other, p, comm));
else
@ -903,12 +923,7 @@ namespace euf {
out << "n";
out << "#" << n->get_expr_id() << " := ";
expr* f = n->get_expr();
if (is_app(f))
out << mk_bounded_pp(f, m, 1) << " ";
else if (is_quantifier(f))
out << "q:" << f->get_id() << " ";
else
out << "v:" << f->get_id() << " ";
out << mk_bounded_pp(f, m, 1) << " ";
if (!n->is_root())
out << "[r " << n->get_root()->get_expr_id() << "] ";
if (!n->m_parents.empty()) {
@ -962,6 +977,9 @@ namespace euf {
st.update("euf propagations theory eqs", m_stats.m_num_th_eqs);
st.update("euf propagations theory diseqs", m_stats.m_num_th_diseqs);
st.update("euf propagations literal", m_stats.m_num_lits);
for (auto p : m_plugins)
if (p)
p->collect_statistics(st);
}
void egraph::copy_from(egraph const& src, std::function<void*(void*)>& copy_justification) {

12
src/ast/euf/euf_egraph.h
View file

@ -58,7 +58,7 @@ namespace euf {
theory_var m_v2;
union {
enode* m_child;
expr* m_eq;
enode* m_eq;
};
enode* m_root;
public:
@ -68,10 +68,10 @@ namespace euf {
theory_var v2() const { return m_v2; }
enode* child() const { SASSERT(is_eq()); return m_child; }
enode* root() const { SASSERT(is_eq()); return m_root; }
expr* eq() const { SASSERT(!is_eq()); return m_eq; }
enode* eq() const { SASSERT(!is_eq()); return m_eq; }
th_eq(theory_id id, theory_var v1, theory_var v2, enode* c, enode* r) :
m_id(id), m_v1(v1), m_v2(v2), m_child(c), m_root(r) {}
th_eq(theory_id id, theory_var v1, theory_var v2, expr* eq) :
th_eq(theory_id id, theory_var v1, theory_var v2, enode* eq) :
m_id(id), m_v1(v1), m_v2(v2), m_eq(eq), m_root(nullptr) {}
};
@ -116,6 +116,7 @@ namespace euf {
struct replace_th_var {};
struct new_th_eq {};
struct new_th_eq_qhead {};
struct plugin_qhead {};
struct inconsistent {};
struct value_assignment {};
struct lbl_hash {};
@ -125,7 +126,7 @@ namespace euf {
struct plugin_undo {};
enum class tag_t { is_set_parent, is_add_node, is_toggle_cgc, is_toggle_merge_tf, is_update_children,
is_add_th_var, is_replace_th_var, is_new_th_eq,
is_lbl_hash, is_new_th_eq_qhead,
is_lbl_hash, is_new_th_eq_qhead, is_plugin_qhead,
is_inconsistent, is_value_assignment, is_lbl_set, is_set_relevant,
is_plugin_undo };
tag_t tag;
@ -158,6 +159,8 @@ namespace euf {
tag(tag_t::is_new_th_eq), r1(nullptr), n1(nullptr), r2_num_parents(0) {}
update_record(unsigned qh, new_th_eq_qhead):
tag(tag_t::is_new_th_eq_qhead), r1(nullptr), n1(nullptr), qhead(qh) {}
update_record(unsigned qh, plugin_qhead) :
tag(tag_t::is_plugin_qhead), r1(nullptr), n1(nullptr), qhead(qh) {}
update_record(bool inc, inconsistent) :
tag(tag_t::is_inconsistent), r1(nullptr), n1(nullptr), m_inconsistent(inc) {}
update_record(enode* n, value_assignment) :
@ -196,6 +199,7 @@ namespace euf {
enode *m_n2 = nullptr;
justification m_justification;
unsigned m_new_th_eqs_qhead = 0;
unsigned m_plugin_qhead = 0;
svector<th_eq> m_new_th_eqs;
bool_vector m_th_propagates_diseqs;
enode_vector m_todo;

18
src/ast/euf/euf_mam.cpp
View file

@ -682,7 +682,8 @@ namespace euf {
m_region(ctx.get_region()) {
}
code_tree * mk_code_tree(func_decl * lbl, unsigned short num_args, bool filter_candidates) {
code_tree * mk_code_tree(app* p, unsigned short num_args, bool filter_candidates) {
func_decl* lbl = p->get_decl();
code_tree * r = alloc(code_tree,m_lbl_hasher, lbl, num_args, filter_candidates);
r->m_root = mk_init(lbl, num_args);
return r;
@ -1792,7 +1793,7 @@ namespace euf {
SASSERT(m.is_pattern(mp));
app * p = to_app(mp->get_arg(first_idx));
unsigned num_args = p->get_num_args();
code_tree * r = m_ct_manager.mk_code_tree(p->get_decl(), num_args, filter_candidates);
code_tree * r = m_ct_manager.mk_code_tree(p, num_args, filter_candidates);
init(r, qa, mp, first_idx);
linearise(r->m_root, first_idx);
if (is_ac(p->get_decl()))
@ -2345,7 +2346,7 @@ namespace euf {
}
bool interpreter::execute_core(code_tree * t, enode * n) {
TRACE(trigger_bug, tout << "interpreter::execute_core\n"; t->display(tout); tout << "\nenode\n" << mk_ismt2_pp(n->get_expr(), m) << "\n";);
TRACE(trigger_bug, tout << "interpreter::execute_core\n"; t->display(tout); tout << "\nenode: " << mk_ismt2_pp(n->get_expr(), m) << "\n";);
unsigned since_last_check = 0;
#ifdef _PROFILE_MAM
@ -2462,13 +2463,22 @@ namespace euf {
auto num_pat_args = static_cast<const initn*>(m_pc)->m_num_args;
for (unsigned i = 0; i < m_acargs.size(); ++i) {
auto* arg = m_acargs[i];
if (is_app(arg->get_expr()) && f == arg->get_decl()) {
if (!is_app(arg->get_expr()))
continue;
auto fa = arg->get_decl();
if (f == fa) {
m_acargs.append(arg->num_args(), arg->args());
m_acargs[i] = m_acargs.back();
m_acargs.pop_back();
--i;
}
}
TRACE(mam_bug, tout << "initac:\n";
for (auto arg : m_acargs) tout << mk_pp(arg->get_expr(), m) << "\n";
tout << "\n";
display_instr_input_reg(tout, m_pc);
);
if (num_pat_args > m_acargs.size())
goto backtrack;
m_acbitset.reset();

2
src/ast/euf/euf_plugin.cpp
View file

@ -35,7 +35,7 @@ namespace euf {
void plugin::push_merge(enode* a, enode* b) {
if (a->get_root() == b->get_root())
return; // already merged
TRACE(plugin, tout << g.bpp(a) << " == " << g.bpp(b) << "\n");
TRACE(plugin, tout << "push-merge " << g.bpp(a) << " == " << g.bpp(b) << "\n");
g.push_merge(a, b, justification::axiom(get_id()));
}

5
src/ast/euf/euf_plugin.h
View file

@ -19,6 +19,7 @@ Author:
#pragma once
#include "util/statistics.h"
#include "ast/euf/euf_enode.h"
#include "ast/euf/euf_justification.h"
@ -51,8 +52,12 @@ namespace euf {
virtual void propagate() = 0;
virtual void undo() = 0;
virtual void push_scope_eh() {}
virtual std::ostream& display(std::ostream& out) const = 0;
virtual void collect_statistics(statistics& st) const {}
};
}

3
src/ast/euf/ho_matcher.cpp
View file

@ -293,8 +293,7 @@ namespace euf {
// v - offset |-> t
if (is_meta_var(p, wi.pat_offset()) && is_closed(t, 0, wi.term_offset())) {
auto v = to_var(p);
auto idx = v->get_idx() - wi.pat_offset();
SASSERT(!m_subst.get(idx)); // reduce ensures meta variables are not in substitutions
SASSERT(!m_subst.get(v->get_idx() - wi.pat_offset())); // reduce ensures meta variables are not in substitutions
add_binding(v, wi.pat_offset(), t);
wi.set_done();
return true;

9
src/ast/euf/ho_matcher.h
View file

@ -100,14 +100,14 @@ namespace euf {
class match_goals {
protected:
ast_manager &m;
ho_matcher& ho;
ast_manager &m;
match_goal* m_expensive = nullptr, *m_cheap = nullptr;
match_goal* pop(match_goal*& q);
public:
match_goals(ho_matcher& em, ast_manager &m) : m(m), ho(em) {}
match_goals(ho_matcher& em, ast_manager& m) : ho(em), m(m) {}
bool empty() const { return m_cheap == nullptr && m_expensive == nullptr; }
void reset() { m_cheap = m_expensive = nullptr; }
void push(unsigned level, unsigned offset, expr_ref const& pat, expr_ref const& t);
@ -158,7 +158,6 @@ namespace euf {
};
class unitary_patterns {
ast_manager& m;
array_util a;
vector<expr_ref_vector> m_patterns;
vector<svector<lbool>> m_is_unitary;
@ -181,7 +180,7 @@ namespace euf {
}
public:
unitary_patterns(ast_manager& m) : m(m), a(m) {}
unitary_patterns(ast_manager& m) : a(m) {}
bool is_unitary(unsigned offset, expr* p) const {
return find(offset, p) == l_true;
@ -369,8 +368,8 @@ namespace euf {
ho_matcher(ast_manager& m, trail_stack &trail) :
m(m),
m_subst(m),
m_trail(trail),
m_subst(m),
m_goals(*this, m),
m_unitary(m),
m_rewriter(m),

25
src/ast/normal_forms/nnf.cpp
View file

@ -149,8 +149,10 @@ class skolemizer {
r = m_subst(body, substitution);
p = nullptr;
if (m_proofs_enabled) {
if (q->get_kind() == forall_k)
p = m.mk_skolemization(mk_not(m, q), mk_not(m, r));
if (q->get_kind() == forall_k) {
auto a = mk_not(m, q);
p = m.mk_skolemization(a , mk_not(m, r));
}
else
p = m.mk_skolemization(q, r);
}
@ -564,7 +566,8 @@ struct nnf::imp {
expr * _then = rs[2];
expr * _else = rs[3];
app * r = m.mk_and(m.mk_or(_not_cond, _then), m.mk_or(_cond, _else));
expr* a = m.mk_or(_not_cond, _then);
app * r = m.mk_and(a, m.mk_or(_cond, _else));
m_result_stack.shrink(fr.m_spos);
m_result_stack.push_back(r);
if (proofs_enabled()) {
@ -609,10 +612,14 @@ struct nnf::imp {
expr * not_rhs = rs[3];
app * r;
if (is_eq(t) == fr.m_pol)
r = m.mk_and(m.mk_or(not_lhs, rhs), m.mk_or(lhs, not_rhs));
else
r = m.mk_and(m.mk_or(lhs, rhs), m.mk_or(not_lhs, not_rhs));
if (is_eq(t) == fr.m_pol) {
expr* a = m.mk_or(not_lhs, rhs);
r = m.mk_and(a, m.mk_or(lhs, not_rhs));
}
else {
expr* a = m.mk_or(lhs, rhs);
r = m.mk_and(a, m.mk_or(not_lhs, not_rhs));
}
m_result_stack.shrink(fr.m_spos);
m_result_stack.push_back(r);
if (proofs_enabled()) {
@ -684,8 +691,8 @@ struct nnf::imp {
if (proofs_enabled()) {
expr_ref aux(m);
aux = m.mk_label(true, names.size(), names.data(), arg);
pr = m.mk_transitivity(mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux)),
m.mk_iff_oeq(m.mk_rewrite(aux, r)));
auto a = mk_proof(fr.m_pol, 1, &arg_pr, t, to_app(aux));
pr = m.mk_transitivity(a, m.mk_iff_oeq(m.mk_rewrite(aux, r)));
}
}
else {

1
src/ast/rewriter/CMakeLists.txt
View file

@ -46,7 +46,6 @@ z3_add_component(rewriter
COMPONENT_DEPENDENCIES
ast
params
automata
interval
polynomial
)

57
src/ast/rewriter/arith_rewriter.cpp
View file

@ -720,24 +720,36 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
}
expr* c = nullptr, *t = nullptr, *e = nullptr;
if (m.is_ite(arg1, c, t, e) && is_numeral(t, a1) && is_numeral(arg2, a2)) {
expr_ref a(m.mk_not(c), m);
switch (kind) {
case LE: result = a1 <= a2 ? m.mk_or(c, m_util.mk_le(e, arg2)) : m.mk_and(m.mk_not(c), m_util.mk_le(e, arg2)); return BR_REWRITE2;
case GE: result = a1 >= a2 ? m.mk_or(c, m_util.mk_ge(e, arg2)) : m.mk_and(m.mk_not(c), m_util.mk_ge(e, arg2)); return BR_REWRITE2;
case EQ: result = a1 == a2 ? m.mk_or(c, m.mk_eq(e, arg2)) : m.mk_and(m.mk_not(c), m_util.mk_eq(e, arg2)); return BR_REWRITE2;
case LE: result = a1 <= a2 ? m.mk_or(c, m_util.mk_le(e, arg2)) : m.mk_and(a, m_util.mk_le(e, arg2)); return BR_REWRITE2;
case GE: result = a1 >= a2 ? m.mk_or(c, m_util.mk_ge(e, arg2)) : m.mk_and(a, m_util.mk_ge(e, arg2)); return BR_REWRITE2;
case EQ: result = a1 == a2 ? m.mk_or(c, m.mk_eq(e, arg2)) : m.mk_and(a, m_util.mk_eq(e, arg2)); return BR_REWRITE2;
}
}
if (m.is_ite(arg1, c, t, e) && is_numeral(e, a1) && is_numeral(arg2, a2)) {
expr_ref a(m.mk_not(c), m);
switch (kind) {
case LE: result = a1 <= a2 ? m.mk_or(m.mk_not(c), m_util.mk_le(t, arg2)) : m.mk_and(c, m_util.mk_le(t, arg2)); return BR_REWRITE2;
case GE: result = a1 >= a2 ? m.mk_or(m.mk_not(c), m_util.mk_ge(t, arg2)) : m.mk_and(c, m_util.mk_ge(t, arg2)); return BR_REWRITE2;
case EQ: result = a1 == a2 ? m.mk_or(m.mk_not(c), m.mk_eq(t, arg2)) : m.mk_and(c, m_util.mk_eq(t, arg2)); return BR_REWRITE2;
case LE: result = a1 <= a2 ? m.mk_or(a, m_util.mk_le(t, arg2)) : m.mk_and(c, m_util.mk_le(t, arg2)); return BR_REWRITE2;
case GE: result = a1 >= a2 ? m.mk_or(a, m_util.mk_ge(t, arg2)) : m.mk_and(c, m_util.mk_ge(t, arg2)); return BR_REWRITE2;
case EQ: result = a1 == a2 ? m.mk_or(a, m.mk_eq(t, arg2)) : m.mk_and(c, m_util.mk_eq(t, arg2)); return BR_REWRITE2;
}
}
if (m.is_ite(arg1, c, t, e) && arg1->get_ref_count() == 1) {
switch (kind) {
case LE: result = m.mk_ite(c, m_util.mk_le(t, arg2), m_util.mk_le(e, arg2)); return BR_REWRITE2;
case GE: result = m.mk_ite(c, m_util.mk_ge(t, arg2), m_util.mk_ge(e, arg2)); return BR_REWRITE2;
case EQ: result = m.mk_ite(c, m.mk_eq(t, arg2), m.mk_eq(e, arg2)); return BR_REWRITE2;
case LE:
{
auto a = m_util.mk_le(t, arg2);
result = m.mk_ite(c, a, m_util.mk_le(e, arg2)); return BR_REWRITE2;
}
case GE: {
auto a = m_util.mk_ge(t, arg2);
result = m.mk_ite(c, a, m_util.mk_ge(e, arg2)); return BR_REWRITE2;
}
case EQ:{
auto a = m.mk_eq(t, arg2);
result = m.mk_ite(c, a, m.mk_eq(e, arg2)); return BR_REWRITE2;
}
}
}
if (m_util.is_to_int(arg2) && is_numeral(arg1)) {
@ -1413,12 +1425,25 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
}
}
expr* x, *y;
expr* x = nullptr, * y = nullptr, * z = nullptr;
if (is_num2 && v2.is_pos() && m_util.is_mul(arg1, x, y) && m_util.is_numeral(x, v1, is_int) && v1 > 0 && divides(v1, v2)) {
result = m_util.mk_mul(m_util.mk_int(v1), m_util.mk_mod(y, m_util.mk_int(v2/v1)));
return BR_REWRITE1;
}
// mod x -y = mod x y
if (m_util.is_mul(arg2, t1, t2) && m_util.is_numeral(t1, v1) && v1 == -1) {
result = m_util.mk_mod(arg1, t2);
return BR_REWRITE1;
}
if (m.is_ite(arg2, x, y, z)) {
expr_ref mod1(m_util.mk_mod(arg1, y), m);
expr_ref mod2(m_util.mk_mod(arg1, z), m);
result = m.mk_ite(x, mod1, mod2);
return BR_REWRITE3;
}
return BR_FAILED;
}
@ -1804,6 +1829,10 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
numeral a;
expr* x = nullptr;
if (m_util.is_int(arg)) {
result = arg;
return BR_DONE;
}
if (m_util.convert_int_numerals_to_real())
return BR_FAILED;
@ -1812,7 +1841,7 @@ br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
return BR_DONE;
}
if (m_util.is_to_real(arg, x)) {
if (m_util.is_to_real(arg, x) && m_util.is_int(x)) {
result = x;
return BR_DONE;
}
@ -1860,6 +1889,10 @@ br_status arith_rewriter::mk_to_real_core(expr * arg, expr_ref & result) {
result = m_util.mk_numeral(a, false);
return BR_DONE;
}
if (m_util.is_real(arg)) {
result = arg;
return BR_DONE;
}
// push to_real over OP_ADD, OP_MUL
if (m_push_to_real) {
if (m_util.is_add(arg) || m_util.is_mul(arg)) {
@ -1884,7 +1917,7 @@ br_status arith_rewriter::mk_is_int(expr * arg, expr_ref & result) {
return BR_DONE;
}
if (m_util.is_to_real(arg)) {
if (m_util.is_to_real(arg) && m_util.is_int(to_app(arg)->get_arg(0))) {
result = m.mk_true();
return BR_DONE;
}

7
src/ast/rewriter/bool_rewriter.cpp
View file

@ -781,9 +781,10 @@ br_status bool_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
m().is_value(t1) && m().is_value(e1) && m().is_value(t2) && m().is_value(e2)) {
expr_ref_vector args(m());
args.push_back(m().mk_or(c1, c2, m().mk_eq(e1, e2)));
args.push_back(m().mk_or(m().mk_not(c1), m().mk_not(c2), m().mk_eq(t1, t2)));
args.push_back(m().mk_or(m().mk_not(c1), c2, m().mk_eq(t1, e2)));
args.push_back(m().mk_or(c1, m().mk_not(c2), m().mk_eq(e1, t2)));
auto nc1 = m().mk_not(c1); auto nc2 = m().mk_not(c2);
args.push_back(m().mk_or(nc1, nc2, m().mk_eq(t1, t2)));
args.push_back(m().mk_or(nc1, c2, m().mk_eq(t1, e2)));
args.push_back(m().mk_or(c1, nc2, m().mk_eq(e1, t2)));
result = m().mk_and(args);
return BR_REWRITE_FULL;
}

2
src/ast/rewriter/bool_rewriter.h
View file

@ -63,7 +63,7 @@ class bool_rewriter {
bool m_elim_ite;
ptr_vector<expr> m_todo1, m_todo2;
unsigned_vector m_counts1, m_counts2;
expr_fast_mark1 m_marked;
expr_mark m_marked;
br_status mk_flat_and_core(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_flat_or_core(unsigned num_args, expr * const * args, expr_ref & result);

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

@ -2265,6 +2265,20 @@ br_status bv_rewriter::mk_bv_ext_rotate_left(expr * arg1, expr * arg2, expr_ref
unsigned shift = static_cast<unsigned>((r2 % numeral(bv_size)).get_uint64() % static_cast<uint64_t>(bv_size));
return mk_bv_rotate_left(shift, arg1, result);
}
expr* x = nullptr, * y = nullptr;
if (m_util.is_ext_rotate_right(arg1, x, y) && arg2 == y) {
// bv_ext_rotate_left(bv_ext_rotate_right(x, y), y) --> x
result = x;
return BR_DONE;
}
if (m_util.is_ext_rotate_left(arg1, x, y)) {
result = m_util.mk_bv_rotate_left(x, m_util.mk_bv_add(y, arg2));
return BR_REWRITE2;
}
if (m_util.is_ext_rotate_right(arg1, x, y)) {
result = m_util.mk_bv_rotate_left(x, m_util.mk_bv_sub(arg2, y));
return BR_REWRITE2;
}
return BR_FAILED;
}
@ -2275,6 +2289,20 @@ br_status bv_rewriter::mk_bv_ext_rotate_right(expr * arg1, expr * arg2, expr_ref
unsigned shift = static_cast<unsigned>((r2 % numeral(bv_size)).get_uint64() % static_cast<uint64_t>(bv_size));
return mk_bv_rotate_right(shift, arg1, result);
}
expr* x = nullptr, * y = nullptr;
if (m_util.is_ext_rotate_left(arg1, x, y) && arg2 == y) {
// bv_ext_rotate_right(bv_ext_rotate_left(x, y), y) --> x
result = x;
return BR_DONE;
}
if (m_util.is_ext_rotate_right(arg1, x, y)) {
result = m_util.mk_bv_rotate_right(x, m_util.mk_bv_add(y, arg2));
return BR_REWRITE2;
}
if (m_util.is_ext_rotate_left(arg1, x, y)) {
result = m_util.mk_bv_rotate_right(x, m_util.mk_bv_sub(arg2, y));
return BR_REWRITE2;
}
return BR_FAILED;
}

37
src/ast/rewriter/datatype_rewriter.cpp
View file

@ -27,7 +27,7 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
SASSERT(num_args == 1);
result = m_util.mk_is(m_util.get_recognizer_constructor(f), args[0]);
return BR_REWRITE1;
case OP_DT_IS:
case OP_DT_IS: {
//
// simplify is_cons(cons(x,y)) -> true
// simplify is_cons(nil) -> false
@ -37,23 +37,48 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
result = m().mk_true();
return BR_DONE;
}
if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0])))
if (!is_app(args[0]))
return BR_FAILED;
if (to_app(args[0])->get_decl() == m_util.get_recognizer_constructor(f))
app* a = to_app(args[0]);
if (m_util.is_update_field(a)) {
result = m().mk_app(f, a->get_arg(0));
return BR_REWRITE1;
}
if (!m_util.is_constructor(a))
return BR_FAILED;
if (a->get_decl() == m_util.get_recognizer_constructor(f))
result = m().mk_true();
else
result = m().mk_false();
return BR_DONE;
}
case OP_DT_ACCESSOR: {
//
// simplify head(cons(x,y)) -> x
//
SASSERT(num_args == 1);
if (!is_app(args[0]) || !m_util.is_constructor(to_app(args[0])))
if (!is_app(args[0]))
return BR_FAILED;
app* a = to_app(args[0]);
func_decl* c_decl = a->get_decl();
auto num_constructors = m_util.get_datatype_num_constructors(args[0]->get_sort());
if (m_util.is_update_field(a) && num_constructors == 1) {
auto dt = a->get_arg(0);
auto val = a->get_arg(1);
func_decl* acc = m_util.get_update_accessor(c_decl);
if (f == acc) {
result = val;
return BR_DONE;
}
result = m().mk_app(f, dt);
return BR_REWRITE1;
}
app * a = to_app(args[0]);
func_decl * c_decl = a->get_decl();
if (!m_util.is_constructor(to_app(args[0])))
return BR_FAILED;
if (c_decl != m_util.get_accessor_constructor(f))
return BR_FAILED;
ptr_vector<func_decl> const & acc = *m_util.get_constructor_accessors(c_decl);

3
src/ast/rewriter/recfun_rewriter.cpp
View file

@ -34,6 +34,9 @@ br_status recfun_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr *
for (unsigned i = 0; i < num_args; ++i)
if (!m.is_value(args[i]))
safe_to_subst = false;
for (auto t : subterms::all(expr_ref(r, m)))
if (is_uninterp(t))
return BR_FAILED;
// check if there is an argument that is a constructor
// such that the recursive function can be partially evaluated.

30
src/ast/rewriter/seq_axioms.cpp
View file

@ -1224,16 +1224,40 @@ namespace seq {
let n = len(x)
- len(a ++ b) = len(a) + len(b) if x = a ++ b
- len(unit(u)) = 1 if x = unit(u)
- len(extract(x, o, l)) = l if len(x) >= o + l etc
- len(str) = str.length() if x = str
- len(empty) = 0 if x = empty
- len(int.to.str(i)) >= 1 if x = int.to.str(i) and more generally if i = 0 then 1 else 1+floor(log(|i|))
- len(x) >= 0 otherwise
*/
void axioms::length_axiom(expr* n) {
expr* x = nullptr;
expr* x = nullptr, * y = nullptr, * offs = nullptr, * l = nullptr;
VERIFY(seq.str.is_length(n, x));
if (seq.str.is_concat(x) ||
seq.str.is_unit(x) ||
if (seq.str.is_concat(x) && to_app(x)->get_num_args() != 0) {
ptr_vector<expr> args;
for (auto arg : *to_app(x))
args.push_back(seq.str.mk_length(arg));
expr_ref len(a.mk_add(args), m);
add_clause(mk_eq(len, n));
}
else if (seq.str.is_extract(x, y, offs, l)) {
// len(extract(y, o, l)) = l if len(y) >= o + l, o >= 0, l >= 0
// len(extract(y, o, l)) = 0 if o < 0 or l <= 0 or len(y) < o
// len(extract(y, o, l)) = len(y) - o if o <= len(y) < o + l
expr_ref len_y(mk_len(y), m);
expr_ref z(a.mk_int(0), m);
expr_ref y_ge_l = mk_ge(a.mk_sub(len_y, a.mk_add(offs, l)), 0);
expr_ref y_ge_o = mk_ge(a.mk_sub(len_y, offs), 0);
expr_ref offs_ge_0 = mk_ge(offs, 0);
expr_ref l_ge_0 = mk_ge(l, 0);
add_clause(~offs_ge_0, ~l_ge_0, ~y_ge_l, mk_eq(n, l));
add_clause(offs_ge_0, mk_eq(n, z));
add_clause(l_ge_0, mk_eq(n, z));
add_clause(y_ge_o, mk_eq(n, z));
add_clause(~y_ge_o, y_ge_l, mk_eq(n, a.mk_sub(len_y, offs)));
}
else if (seq.str.is_unit(x) ||
seq.str.is_empty(x) ||
seq.str.is_string(x)) {
expr_ref len(n, m);

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

@ -29,8 +29,6 @@ Authors:
#include "ast/rewriter/var_subst.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "params/seq_rewriter_params.hpp"
#include "math/automata/automaton.h"
#include "math/automata/symbolic_automata_def.h"
expr_ref sym_expr::accept(expr* e) {
@ -57,7 +55,8 @@ expr_ref sym_expr::accept(expr* e) {
result = m.mk_bool_val((r1 <= r2) && (r2 <= r3));
}
else {
result = m.mk_and(u.mk_le(m_t, e), u.mk_le(e, m_s));
auto a = u.mk_le(m_t, e);
result = m.mk_and(a, u.mk_le(e, m_s));
}
break;
}
@ -83,320 +82,6 @@ struct display_expr1 {
}
};
class sym_expr_boolean_algebra : public boolean_algebra<sym_expr*> {
ast_manager& m;
expr_solver& m_solver;
expr_ref m_var;
typedef sym_expr* T;
public:
sym_expr_boolean_algebra(ast_manager& m, expr_solver& s):
m(m), m_solver(s), m_var(m) {}
T mk_false() override {
expr_ref fml(m.mk_false(), m);
return sym_expr::mk_pred(fml, m.mk_bool_sort()); // use of Bool sort for bound variable is arbitrary
}
T mk_true() override {
expr_ref fml(m.mk_true(), m);
return sym_expr::mk_pred(fml, m.mk_bool_sort());
}
T mk_and(T x, T y) override {
seq_util u(m);
if (x->is_char() && y->is_char()) {
if (x->get_char() == y->get_char()) {
return x;
}
if (m.are_distinct(x->get_char(), y->get_char())) {
expr_ref fml(m.mk_false(), m);
return sym_expr::mk_pred(fml, x->get_sort());
}
}
unsigned lo1, hi1, lo2, hi2;
if (x->is_range() && y->is_range() &&
u.is_const_char(x->get_lo(), lo1) && u.is_const_char(x->get_hi(), hi1) &&
u.is_const_char(y->get_lo(), lo2) && u.is_const_char(y->get_hi(), hi2)) {
lo1 = std::max(lo1, lo2);
hi1 = std::min(hi1, hi2);
if (lo1 > hi1) {
expr_ref fml(m.mk_false(), m);
return sym_expr::mk_pred(fml, x->get_sort());
}
expr_ref _start(u.mk_char(lo1), m);
expr_ref _stop(u.mk_char(hi1), m);
return sym_expr::mk_range(_start, _stop);
}
sort* s = x->get_sort();
if (m.is_bool(s)) s = y->get_sort();
var_ref v(m.mk_var(0, s), m);
expr_ref fml1 = x->accept(v);
expr_ref fml2 = y->accept(v);
if (m.is_true(fml1)) {
return y;
}
if (m.is_true(fml2)) {
return x;
}
if (fml1 == fml2) {
return x;
}
if (is_complement(fml1, fml2)) {
expr_ref ff(m.mk_false(), m);
return sym_expr::mk_pred(ff, x->get_sort());
}
expr_ref fml(m);
bool_rewriter br(m);
br.mk_and(fml1, fml2, fml);
return sym_expr::mk_pred(fml, x->get_sort());
}
bool is_complement(expr* f1, expr* f2) {
expr* f = nullptr;
return
(m.is_not(f1, f) && f == f2) ||
(m.is_not(f2, f) && f == f1);
}
T mk_or(T x, T y) override {
if (x->is_char() && y->is_char() &&
x->get_char() == y->get_char()) {
return x;
}
if (x == y) return x;
var_ref v(m.mk_var(0, x->get_sort()), m);
expr_ref fml1 = x->accept(v);
expr_ref fml2 = y->accept(v);
if (m.is_false(fml1)) return y;
if (m.is_false(fml2)) return x;
bool_rewriter br(m);
expr_ref fml(m);
br.mk_or(fml1, fml2, fml);
return sym_expr::mk_pred(fml, x->get_sort());
}
T mk_and(unsigned sz, T const* ts) override {
switch (sz) {
case 0: return mk_true();
case 1: return ts[0];
default: {
T t = ts[0];
for (unsigned i = 1; i < sz; ++i) {
t = mk_and(t, ts[i]);
}
return t;
}
}
}
T mk_or(unsigned sz, T const* ts) override {
switch (sz) {
case 0: return mk_false();
case 1: return ts[0];
default: {
T t = ts[0];
for (unsigned i = 1; i < sz; ++i) {
t = mk_or(t, ts[i]);
}
return t;
}
}
}
lbool is_sat(T x) override {
unsigned lo, hi;
seq_util u(m);
if (x->is_char()) {
return l_true;
}
if (x->is_range() && u.is_const_char(x->get_lo(), lo) && u.is_const_char(x->get_hi(), hi)) {
return (lo <= hi) ? l_true : l_false;
}
if (x->is_not() && x->get_arg()->is_range() && u.is_const_char(x->get_arg()->get_lo(), lo) && 0 < lo) {
return l_true;
}
if (!m_var || m_var->get_sort() != x->get_sort()) {
m_var = m.mk_fresh_const("x", x->get_sort());
}
expr_ref fml = x->accept(m_var);
if (m.is_true(fml)) {
return l_true;
}
if (m.is_false(fml)) {
return l_false;
}
return m_solver.check_sat(fml);
}
T mk_not(T x) override {
return sym_expr::mk_not(m, x);
}
};
re2automaton::re2automaton(ast_manager& m): m(m), u(m), m_ba(nullptr), m_sa(nullptr) {}
void re2automaton::set_solver(expr_solver* solver) {
m_solver = solver;
m_ba = alloc(sym_expr_boolean_algebra, m, *solver);
m_sa = alloc(symbolic_automata_t, sm, *m_ba.get());
}
eautomaton* re2automaton::mk_product(eautomaton* a1, eautomaton* a2) {
return m_sa->mk_product(*a1, *a2);
}
eautomaton* re2automaton::operator()(expr* e) {
eautomaton* r = re2aut(e);
if (r) {
r->compress();
bool_rewriter br(m);
TRACE(seq, display_expr1 disp(m); r->display(tout << mk_pp(e, m) << " -->\n", disp););
}
return r;
}
bool re2automaton::is_unit_char(expr* e, expr_ref& ch) {
zstring s;
expr* c = nullptr;
if (u.str.is_string(e, s) && s.length() == 1) {
ch = u.mk_char(s[0]);
return true;
}
if (u.str.is_unit(e, c)) {
ch = c;
return true;
}
return false;
}
eautomaton* re2automaton::re2aut(expr* e) {
SASSERT(u.is_re(e));
expr *e0, *e1, *e2;
scoped_ptr<eautomaton> a, b;
unsigned lo, hi;
zstring s1, s2;
if (u.re.is_to_re(e, e1)) {
return seq2aut(e1);
}
else if (u.re.is_concat(e, e1, e2) && (a = re2aut(e1)) && (b = re2aut(e2))) {
return eautomaton::mk_concat(*a, *b);
}
else if (u.re.is_union(e, e1, e2) && (a = re2aut(e1)) && (b = re2aut(e2))) {
return eautomaton::mk_union(*a, *b);
}
else if (u.re.is_star(e, e1) && (a = re2aut(e1))) {
a->add_final_to_init_moves();
a->add_init_to_final_states();
return a.detach();
}
else if (u.re.is_plus(e, e1) && (a = re2aut(e1))) {
a->add_final_to_init_moves();
return a.detach();
}
else if (u.re.is_opt(e, e1) && (a = re2aut(e1))) {
a = eautomaton::mk_opt(*a);
return a.detach();
}
else if (u.re.is_range(e, e1, e2)) {
expr_ref _start(m), _stop(m);
if (is_unit_char(e1, _start) &&
is_unit_char(e2, _stop)) {
TRACE(seq, tout << "Range: " << _start << " " << _stop << "\n";);
a = alloc(eautomaton, sm, sym_expr::mk_range(_start, _stop));
return a.detach();
}
else {
// if e1/e2 are not unit, (re.range e1 e2) is defined to be the empty language
return alloc(eautomaton, sm);
}
}
else if (u.re.is_complement(e, e0) && (a = re2aut(e0)) && m_sa) {
return m_sa->mk_complement(*a);
}
else if (u.re.is_loop(e, e1, lo, hi) && (a = re2aut(e1))) {
scoped_ptr<eautomaton> eps = eautomaton::mk_epsilon(sm);
b = eautomaton::mk_epsilon(sm);
while (hi > lo) {
scoped_ptr<eautomaton> c = eautomaton::mk_concat(*a, *b);
b = eautomaton::mk_union(*eps, *c);
--hi;
}
while (lo > 0) {
b = eautomaton::mk_concat(*a, *b);
--lo;
}
return b.detach();
}
else if (u.re.is_loop(e, e1, lo) && (a = re2aut(e1))) {
b = eautomaton::clone(*a);
b->add_final_to_init_moves();
b->add_init_to_final_states();
while (lo > 0) {
b = eautomaton::mk_concat(*a, *b);
--lo;
}
return b.detach();
}
else if (u.re.is_empty(e)) {
return alloc(eautomaton, sm);
}
else if (u.re.is_full_seq(e)) {
expr_ref tt(m.mk_true(), m);
sort *seq_s = nullptr, *char_s = nullptr;
VERIFY (u.is_re(e->get_sort(), seq_s));
VERIFY (u.is_seq(seq_s, char_s));
sym_expr* _true = sym_expr::mk_pred(tt, char_s);
return eautomaton::mk_loop(sm, _true);
}
else if (u.re.is_full_char(e)) {
expr_ref tt(m.mk_true(), m);
sort *seq_s = nullptr, *char_s = nullptr;
VERIFY (u.is_re(e->get_sort(), seq_s));
VERIFY (u.is_seq(seq_s, char_s));
sym_expr* _true = sym_expr::mk_pred(tt, char_s);
a = alloc(eautomaton, sm, _true);
return a.detach();
}
else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
eautomaton* r = m_sa->mk_product(*a, *b);
TRACE(seq, display_expr1 disp(m); a->display(tout << "a:", disp); b->display(tout << "b:", disp); r->display(tout << "intersection:", disp););
return r;
}
else {
TRACE(seq, tout << "not handled " << mk_pp(e, m) << "\n";);
}
return nullptr;
}
eautomaton* re2automaton::seq2aut(expr* e) {
SASSERT(u.is_seq(e));
zstring s;
expr* e1, *e2;
scoped_ptr<eautomaton> a, b;
if (u.str.is_concat(e, e1, e2) && (a = seq2aut(e1)) && (b = seq2aut(e2))) {
return eautomaton::mk_concat(*a, *b);
}
else if (u.str.is_unit(e, e1)) {
return alloc(eautomaton, sm, sym_expr::mk_char(m, e1));
}
else if (u.str.is_empty(e)) {
return eautomaton::mk_epsilon(sm);
}
else if (u.str.is_string(e, s)) {
unsigned init = 0;
eautomaton::moves mvs;
unsigned_vector final;
final.push_back(s.length());
for (unsigned k = 0; k < s.length(); ++k) {
// reference count?
mvs.push_back(eautomaton::move(sm, k, k+1, sym_expr::mk_char(m, u.str.mk_char(s, k))));
}
return alloc(eautomaton, sm, init, final, mvs);
}
return nullptr;
}
void seq_rewriter::updt_params(params_ref const & p) {
seq_rewriter_params sp(p);
@ -506,7 +191,9 @@ br_status seq_rewriter::mk_eq_helper(expr* a, expr* b, expr_ref& result) {
// sa in (ra n rb) u (C(ra) n C(rb))
if (is_not)
rb = re().mk_complement(rb);
expr* r = re().mk_union(re().mk_inter(ra, rb), re().mk_inter(re().mk_complement(ra), re().mk_complement(rb)));
auto a_ = re().mk_inter(ra, rb);
auto b_ = re().mk_complement(ra);
expr* r = re().mk_union(a_, re().mk_inter(b_, re().mk_complement(rb)));
result = re().mk_in_re(sa, r);
return BR_REWRITE_FULL;
}
@ -936,10 +623,14 @@ expr_ref seq_rewriter::mk_seq_rest(expr* t) {
expr_ref result(m());
expr* s, * j, * k;
rational jv;
if (str().is_extract(t, s, j, k) && m_autil.is_numeral(j, jv) && jv >= 0)
result = str().mk_substr(s, m_autil.mk_int(jv + 1), mk_sub(k, 1));
else
result = str().mk_substr(t, one(), mk_sub(str().mk_length(t), 1));
if (str().is_extract(t, s, j, k) && m_autil.is_numeral(j, jv) && jv >= 0) {
auto a = m_autil.mk_int(jv + 1);
result = str().mk_substr(s, a, mk_sub(k, 1));
}
else {
auto a = one();
result = str().mk_substr(t, a, mk_sub(str().mk_length(t), 1));
}
return result;
}
@ -970,7 +661,10 @@ expr_ref seq_rewriter::mk_seq_last(expr* t) {
* No: if k > |s| then substring(s,0,k) = substring(s,0,k-1)
*/
expr_ref seq_rewriter::mk_seq_butlast(expr* t) {
return expr_ref(str().mk_substr(t, zero(), m_autil.mk_sub(str().mk_length(t), one())), m());
auto b = zero();
auto c = str().mk_length(t);
auto a = str().mk_substr(t, b, m_autil.mk_sub(c, one()));
return expr_ref(a, m());
}
/*
@ -1690,9 +1384,16 @@ br_status seq_rewriter::mk_seq_nth(expr* a, expr* b, expr_ref& result) {
}
expr* la = str().mk_length(a);
result = m().mk_ite(m().mk_and(m_autil.mk_ge(b, zero()), m().mk_not(m_autil.mk_le(la, b))),
str().mk_nth_i(a, b),
str().mk_nth_u(a, b));
{
// deterministic evaluation order for guard components
auto ge0 = m_autil.mk_ge(b, zero());
auto le_la = m_autil.mk_le(la, b);
auto not_le = m().mk_not(le_la);
auto guard = m().mk_and(ge0, not_le);
auto t1 = str().mk_nth_i(a, b);
auto e1 = str().mk_nth_u(a, b);
result = m().mk_ite(guard, t1, e1);
}
return BR_REWRITE_FULL;
}
@ -1766,6 +1467,59 @@ br_status seq_rewriter::mk_seq_last_index(expr* a, expr* b, expr_ref& result) {
result = m_autil.mk_int(0);
return BR_DONE;
}
if (str().is_empty(b)) {
result = str().mk_length(a);
return BR_DONE;
}
expr_ref_vector as(m()), bs(m());
str().get_concat_units(a, as);
str().get_concat_units(b, bs);
auto is_suffix = [&](expr_ref_vector const& as, expr_ref_vector const& bs) {
if (as.size() < bs.size())
return l_undef;
for (unsigned j = 0; j < bs.size(); ++j) {
auto a = as.get(as.size() - j - 1);
auto b = bs.get(bs.size() - j - 1);
if (m().are_equal(a, b))
continue;
if (m().are_distinct(a, b))
return l_false;
return l_undef;
}
return l_true;
};
switch (compare_lengths(as, bs)) {
case shorter_c:
result = minus_one();
return BR_DONE;
case same_length_c:
result = m().mk_ite(m().mk_eq(a, b), zero(), minus_one());
return BR_REWRITE_FULL;
case longer_c: {
unsigned i = as.size();
while (i >= bs.size()) {
switch (is_suffix(as, bs)) {
case l_undef:
return BR_FAILED;
case l_true:
result = m_autil.mk_sub(str().mk_length(a), m_autil.mk_int(bs.size() - i));
return BR_REWRITE3;
case l_false:
as.pop_back();
--i;
break;
}
}
break;
}
default:
break;
}
return BR_FAILED;
}
@ -1810,17 +1564,20 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result
}
if (str().is_empty(b)) {
result = m().mk_ite(m().mk_and(m_autil.mk_le(zero(), c),
m_autil.mk_le(c, str().mk_length(a))),
c,
minus_one());
// enforce deterministic evaluation order for bounds checks
auto a1 = m_autil.mk_le(zero(), c);
auto b1 = m_autil.mk_le(c, str().mk_length(a));
auto cond = m().mk_and(a1, b1);
result = m().mk_ite(cond, c, minus_one());
return BR_REWRITE2;
}
if (str().is_empty(a)) {
expr* emp = str().mk_is_empty(b);
result = m().mk_ite(m().mk_and(m().mk_eq(c, zero()), emp), zero(), minus_one());
auto a1 = m().mk_eq(c, zero());
auto cond = m().mk_and(a1, emp);
result = m().mk_ite(cond, zero(), minus_one());
return BR_REWRITE2;
}
@ -2133,7 +1890,10 @@ br_status seq_rewriter::mk_seq_map(expr* f, expr* seqA, expr_ref& result) {
return BR_REWRITE2;
}
if (str().is_concat(seqA, s1, s2)) {
result = str().mk_concat(str().mk_map(f, s1), str().mk_map(f, s2));
// introduce temporaries to ensure deterministic evaluation order of recursive map calls
auto m1 = str().mk_map(f, s1);
auto m2 = str().mk_map(f, s2);
result = str().mk_concat(m1, m2);
return BR_REWRITE2;
}
return BR_FAILED;
@ -2153,7 +1913,9 @@ br_status seq_rewriter::mk_seq_mapi(expr* f, expr* i, expr* seqA, expr_ref& resu
}
if (str().is_concat(seqA, s1, s2)) {
expr_ref j(m_autil.mk_add(i, str().mk_length(s1)), m());
result = str().mk_concat(str().mk_mapi(f, i, s1), str().mk_mapi(f, j, s2));
auto left = str().mk_mapi(f, i, s1);
auto right = str().mk_mapi(f, j, s2);
result = str().mk_concat(left, right);
return BR_REWRITE2;
}
return BR_FAILED;
@ -2309,8 +2071,8 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
SASSERT(bs.size() > 1);
s1 = s1.extract(s2.length(), s1.length() - s2.length());
as[0] = str().mk_string(s1);
result = str().mk_prefix(str().mk_concat(as.size(), as.data(), sort_a),
str().mk_concat(bs.size()-1, bs.data()+1, sort_a));
auto a = str().mk_concat(as.size(), as.data(), sort_a);
result = str().mk_prefix(a, str().mk_concat(bs.size()-1, bs.data()+1, sort_a));
TRACE(seq, tout << s1 << " " << s2 << " " << result << "\n";);
return BR_REWRITE_FULL;
}
@ -2647,7 +2409,8 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
}
expr* b;
if (str().is_itos(a, b)) {
result = m().mk_ite(m_autil.mk_ge(b, zero()), b, minus_one());
auto a = m_autil.mk_ge(b, zero());
result = m().mk_ite(a, b, minus_one());
return BR_DONE;
}
if (str().is_ubv2s(a, b)) {
@ -2658,7 +2421,8 @@ br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
expr* c = nullptr, *t = nullptr, *e = nullptr;
if (m().is_ite(a, c, t, e)) {
result = m().mk_ite(c, str().mk_stoi(t), str().mk_stoi(e));
auto a = str().mk_stoi(t);
result = m().mk_ite(c, a, str().mk_stoi(e));
return BR_REWRITE_FULL;
}
@ -2721,46 +2485,6 @@ void seq_rewriter::add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned
}
bool seq_rewriter::is_sequence(eautomaton& aut, expr_ref_vector& seq) {
seq.reset();
unsigned state = aut.init();
uint_set visited;
eautomaton::moves mvs;
unsigned_vector states;
aut.get_epsilon_closure(state, states);
bool has_final = false;
for (unsigned i = 0; !has_final && i < states.size(); ++i) {
has_final = aut.is_final_state(states[i]);
}
aut.get_moves_from(state, mvs, true);
while (!has_final) {
if (mvs.size() != 1) {
return false;
}
if (visited.contains(state)) {
return false;
}
if (aut.is_final_state(mvs[0].src())) {
return false;
}
visited.insert(state);
sym_expr* t = mvs[0].t();
if (!t || !t->is_char()) {
return false;
}
seq.push_back(str().mk_unit(t->get_char()));
state = mvs[0].dst();
mvs.reset();
aut.get_moves_from(state, mvs, true);
states.reset();
has_final = false;
aut.get_epsilon_closure(state, states);
for (unsigned i = 0; !has_final && i < states.size(); ++i) {
has_final = aut.is_final_state(states[i]);
}
}
return mvs.empty();
}
bool seq_rewriter::is_sequence(expr* e, expr_ref_vector& seq) {
seq.reset();
@ -3006,7 +2730,10 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
zstring zs;
unsigned lo = 0, hi = 0;
if (re().is_concat(r, r1, r2)) {
result = re().mk_concat(re().mk_reverse(r2), re().mk_reverse(r1));
// deterministic evaluation order for reverse operands
auto a_rev = re().mk_reverse(r2);
auto b_rev = re().mk_reverse(r1);
result = re().mk_concat(a_rev, b_rev);
return BR_REWRITE2;
}
else if (re().is_star(r, r1)) {
@ -3018,15 +2745,22 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
return BR_REWRITE2;
}
else if (re().is_union(r, r1, r2)) {
result = re().mk_union(re().mk_reverse(r1), re().mk_reverse(r2));
// ensure deterministic evaluation order of parameters
auto a = re().mk_reverse(r1);
auto b = re().mk_reverse(r2);
result = re().mk_union(a, b);
return BR_REWRITE2;
}
else if (re().is_intersection(r, r1, r2)) {
result = re().mk_inter(re().mk_reverse(r1), re().mk_reverse(r2));
auto a = re().mk_reverse(r1);
auto b = re().mk_reverse(r2);
result = re().mk_inter(a, b);
return BR_REWRITE2;
}
else if (re().is_diff(r, r1, r2)) {
result = re().mk_diff(re().mk_reverse(r1), re().mk_reverse(r2));
auto a = re().mk_reverse(r1);
auto b = re().mk_reverse(r2);
result = re().mk_diff(a, b);
return BR_REWRITE2;
}
else if (m().is_ite(r, p, r1, r2)) {
@ -3070,8 +2804,9 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) {
return BR_DONE;
}
else if (re().is_to_re(r, s) && str().is_concat(s, s1, s2)) {
result = re().mk_concat(re().mk_reverse(re().mk_to_re(s2)),
re().mk_reverse(re().mk_to_re(s1)));
auto a_rev = re().mk_reverse(re().mk_to_re(s2));
auto b_rev = re().mk_reverse(re().mk_to_re(s1));
result = re().mk_concat(a_rev, b_rev);
return BR_REWRITE3;
}
else {
@ -3260,7 +2995,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
}
else {
// observe that the precondition |r1|>0 is is implied by c1 for use of mk_seq_first
m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(mk_seq_first(r1), e), c1);
{
auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort)));
auto eq_first = m().mk_eq(mk_seq_first(r1), e);
m_br.mk_and(is_non_empty, eq_first, c1);
}
m_br.mk_and(path, c1, c2);
if (m().is_false(c2))
result = nothing();
@ -3273,7 +3012,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
if (re().is_to_re(r2, r1)) {
// here r1 is a sequence
// observe that the precondition |r1|>0 of mk_seq_last is implied by c1
m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(mk_seq_last(r1), e), c1);
{
auto is_non_empty = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort)));
auto eq_last = m().mk_eq(mk_seq_last(r1), e);
m_br.mk_and(is_non_empty, eq_last, c1);
}
m_br.mk_and(path, c1, c2);
if (m().is_false(c2))
result = nothing();
@ -3305,8 +3048,15 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
result = mk_antimirov_deriv_union(c1, re().mk_ite_simplify(r1nullable, mk_antimirov_deriv(e, r2, path), nothing()));
}
else if (m().is_ite(r, c, r1, r2)) {
c1 = simplify_path(e, m().mk_and(c, path));
c2 = simplify_path(e, m().mk_and(m().mk_not(c), path));
{
auto cp = m().mk_and(c, path);
c1 = simplify_path(e, cp);
}
{
auto notc = m().mk_not(c);
auto np = m().mk_and(notc, path);
c2 = simplify_path(e, np);
}
if (m().is_false(c1))
result = mk_antimirov_deriv(e, r2, c2);
else if (m().is_false(c2))
@ -3321,7 +3071,11 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref
// SASSERT(u().is_char(c1));
// SASSERT(u().is_char(c2));
// case: c1 <= e <= c2
range = simplify_path(e, m().mk_and(u().mk_le(c1, e), u().mk_le(e, c2)));
// deterministic evaluation for range bounds
auto a_le = u().mk_le(c1, e);
auto b_le = u().mk_le(e, c2);
auto rng_cond = m().mk_and(a_le, b_le);
range = simplify_path(e, rng_cond);
psi = simplify_path(e, m().mk_and(path, range));
}
else if (!str().is_string(r1) && str().is_unit_string(r2, c2)) {
@ -3702,12 +3456,22 @@ expr_ref seq_rewriter::mk_regex_reverse(expr* r) {
result = mk_regex_concat(mk_regex_reverse(r2), mk_regex_reverse(r1));
else if (m().is_ite(r, c, r1, r2))
result = m().mk_ite(c, mk_regex_reverse(r1), mk_regex_reverse(r2));
else if (re().is_union(r, r1, r2))
result = re().mk_union(mk_regex_reverse(r1), mk_regex_reverse(r2));
else if (re().is_intersection(r, r1, r2))
result = re().mk_inter(mk_regex_reverse(r1), mk_regex_reverse(r2));
else if (re().is_diff(r, r1, r2))
result = re().mk_diff(mk_regex_reverse(r1), mk_regex_reverse(r2));
else if (re().is_union(r, r1, r2)) {
// enforce deterministic evaluation order
auto a1 = mk_regex_reverse(r1);
auto b1 = mk_regex_reverse(r2);
result = re().mk_union(a1, b1);
}
else if (re().is_intersection(r, r1, r2)) {
auto a1 = mk_regex_reverse(r1);
auto b1 = mk_regex_reverse(r2);
result = re().mk_inter(a1, b1);
}
else if (re().is_diff(r, r1, r2)) {
auto a1 = mk_regex_reverse(r1);
auto b1 = mk_regex_reverse(r2);
result = re().mk_diff(a1, b1);
}
else if (re().is_star(r, r1))
result = re().mk_star(mk_regex_reverse(r1));
else if (re().is_plus(r, r1))
@ -4285,8 +4049,13 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
// if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else []
//
hd = mk_seq_first(r1);
m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')),
m().mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele)), result);
// isolate nested conjunction for deterministic evaluation
auto a0 = u().mk_le(m_util.mk_char('0'), ele);
auto a1 = u().mk_le(ele, m_util.mk_char('9'));
auto a2 = m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort)));
auto a3 = m().mk_eq(hd, ele);
auto inner = m().mk_and(a2, a3);
m_br.mk_and(a0, a1, inner, result);
tl = re().mk_to_re(mk_seq_rest(r1));
return re_and(result, tl);
}
@ -4320,7 +4089,10 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) {
// tl = rest of reverse(r2) i.e. butlast of r2
//hd = str().mk_nth_i(r2, m_autil.mk_sub(str().mk_length(r2), one()));
hd = mk_seq_last(r2);
m_br.mk_and(m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result);
// factor nested constructor calls to enforce deterministic argument evaluation order
auto a_non_empty = m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort)));
auto a_eq = m().mk_eq(hd, ele);
m_br.mk_and(a_non_empty, a_eq, result);
tl = re().mk_to_re(mk_seq_butlast(r2));
return re_and(result, re().mk_reverse(tl));
}
@ -4605,9 +4377,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
(re().is_union(b, b1, eps) && re().is_epsilon(eps)) ||
(re().is_union(b, eps, b1) && re().is_epsilon(eps)))
{
result = m().mk_ite(m().mk_eq(str().mk_length(a), zero()),
m().mk_true(),
re().mk_in_re(a, b1));
// deterministic evaluation order: build sub-expressions first
auto len_a = str().mk_length(a);
auto is_empty = m().mk_eq(len_a, zero());
auto in_b1 = re().mk_in_re(a, b1);
result = m().mk_ite(is_empty, m().mk_true(), in_b1);
return BR_REWRITE_FULL;
}
if (str().is_empty(a)) {
@ -4637,9 +4411,10 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
expr_ref len_hd(m_autil.mk_int(re().min_length(hd)), m());
expr_ref len_a(str().mk_length(a), m());
expr_ref len_tl(m_autil.mk_sub(len_a, len_hd), m());
result = m().mk_and(m_autil.mk_ge(len_a, len_hd),
re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd),
re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl));
auto ge_len = m_autil.mk_ge(len_a, len_hd);
auto prefix = re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd);
auto suffix = re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl);
result = m().mk_and(ge_len, prefix, suffix);
return BR_REWRITE_FULL;
}
if (get_re_head_tail_reversed(b, hd, tl)) {
@ -4648,10 +4423,11 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
expr_ref len_a(str().mk_length(a), m());
expr_ref len_hd(m_autil.mk_sub(len_a, len_tl), m());
expr* s = nullptr;
result = m().mk_and(m_autil.mk_ge(len_a, len_tl),
re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd),
(re().is_to_re(tl, s) ? m().mk_eq(s, str().mk_substr(a, len_hd, len_tl)) :
re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl)));
auto ge_len = m_autil.mk_ge(len_a, len_tl);
auto prefix = re().mk_in_re(str().mk_substr(a, zero(), len_hd), hd);
auto tail_seq = str().mk_substr(a, len_hd, len_tl);
auto tail = (re().is_to_re(tl, s) ? m().mk_eq(s, tail_seq) : re().mk_in_re(tail_seq, tl));
result = m().mk_and(ge_len, prefix, tail);
return BR_REWRITE_FULL;
}
@ -4917,11 +4693,17 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
expr *e1 = nullptr, *e2 = nullptr;
if (re().is_intersection(a, e1, e2)) {
result = re().mk_union(re().mk_complement(e1), re().mk_complement(e2));
// enforce deterministic evaluation order for nested complement arguments
auto a1 = re().mk_complement(e1);
auto b1 = re().mk_complement(e2);
result = re().mk_union(a1, b1);
return BR_REWRITE2;
}
if (re().is_union(a, e1, e2)) {
result = re().mk_inter(re().mk_complement(e1), re().mk_complement(e2));
// enforce deterministic evaluation order for nested complement arguments
auto a1 = re().mk_complement(e1);
auto b1 = re().mk_complement(e2);
result = re().mk_inter(a1, b1);
return BR_REWRITE2;
}
if (re().is_empty(a)) {
@ -5314,7 +5096,9 @@ void seq_rewriter::elim_condition(expr* elem, expr_ref& cond) {
rep.insert(elem, solution);
rep(cond);
if (!is_uninterp_const(elem)) {
cond = m().mk_and(m().mk_eq(elem, solution), cond);
// ensure deterministic evaluation order when augmenting condition
auto eq_sol = m().mk_eq(elem, solution);
cond = m().mk_and(eq_sol, cond);
}
}
else if (all_ranges) {
@ -5377,11 +5161,16 @@ br_status seq_rewriter::reduce_re_is_empty(expr* r, expr_ref& result) {
}
// Partial DNF expansion:
else if (re().is_intersection(r, r1, r2) && re().is_union(r1, r3, r4)) {
result = eq_empty(re().mk_union(re().mk_inter(r3, r2), re().mk_inter(r4, r2)));
// enforce deterministic order for nested intersections inside union
auto a1 = re().mk_inter(r3, r2);
auto b1 = re().mk_inter(r4, r2);
result = eq_empty(re().mk_union(a1, b1));
return BR_REWRITE3;
}
else if (re().is_intersection(r, r1, r2) && re().is_union(r2, r3, r4)) {
result = eq_empty(re().mk_union(re().mk_inter(r3, r1), re().mk_inter(r4, r1)));
auto a1 = re().mk_inter(r3, r1);
auto b1 = re().mk_inter(r4, r1);
result = eq_empty(re().mk_union(a1, b1));
return BR_REWRITE3;
}
return BR_FAILED;
@ -6021,6 +5810,12 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) {
result = m_autil.mk_lt(s, zero());
return true;
}
// at(s, offset) = "" <=> len(s) <= offset or offset < 0
if (str().is_at(r, s, offset)) {
expr_ref len_s(str().mk_length(s), m());
result = m().mk_or(m_autil.mk_le(len_s, offset), m_autil.mk_lt(offset, zero()));
return true;
}
return false;
}

35
src/ast/rewriter/seq_rewriter.h
View file

@ -26,8 +26,6 @@ Notes:
#include "util/params.h"
#include "util/lbool.h"
#include "util/sign.h"
#include "math/automata/automaton.h"
#include "math/automata/symbolic_automata.h"
inline std::ostream& operator<<(std::ostream& out, expr_ref_pair_vector const& es) {
@ -81,33 +79,15 @@ public:
void dec_ref(sym_expr* s) { if (s) s->dec_ref(); }
};
#if 0
class expr_solver {
public:
virtual ~expr_solver() = default;
virtual lbool check_sat(expr* e) = 0;
};
#endif
typedef automaton<sym_expr, sym_expr_manager> eautomaton;
class re2automaton {
typedef boolean_algebra<sym_expr*> boolean_algebra_t;
typedef symbolic_automata<sym_expr, sym_expr_manager> symbolic_automata_t;
ast_manager& m;
sym_expr_manager sm;
seq_util u;
scoped_ptr<expr_solver> m_solver;
scoped_ptr<boolean_algebra_t> m_ba;
scoped_ptr<symbolic_automata_t> m_sa;
bool is_unit_char(expr* e, expr_ref& ch);
eautomaton* re2aut(expr* e);
eautomaton* seq2aut(expr* e);
public:
re2automaton(ast_manager& m);
eautomaton* operator()(expr* e);
void set_solver(expr_solver* solver);
bool has_solver() const { return m_solver; }
eautomaton* mk_product(eautomaton *a1, eautomaton *a2);
};
/**
\brief Cheap rewrite rules for seq constraints
@ -150,7 +130,7 @@ class seq_rewriter {
seq_util m_util;
arith_util m_autil;
bool_rewriter m_br;
re2automaton m_re2aut;
// re2automaton m_re2aut;
op_cache m_op_cache;
expr_ref_vector m_es, m_lhs, m_rhs;
bool m_coalesce_chars;
@ -340,7 +320,7 @@ class seq_rewriter {
void add_next(u_map<expr*>& next, expr_ref_vector& trail, unsigned idx, expr* cond);
bool is_sequence(expr* e, expr_ref_vector& seq);
bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
// bool is_sequence(eautomaton& aut, expr_ref_vector& seq);
bool get_lengths(expr* e, expr_ref_vector& lens, rational& pos);
bool reduce_value_clash(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
bool reduce_back(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_pair_vector& new_eqs);
@ -360,7 +340,8 @@ class seq_rewriter {
public:
seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m), m_autil(m), m_br(m, p), m_re2aut(m), m_op_cache(m), m_es(m),
m_util(m), m_autil(m), m_br(m, p), // m_re2aut(m),
m_op_cache(m), m_es(m),
m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
}
ast_manager & m() const { return m_util.get_manager(); }
@ -371,8 +352,6 @@ public:
void updt_params(params_ref const & p);
static void get_param_descrs(param_descrs & r);
void set_solver(expr_solver* solver) { m_re2aut.set_solver(solver); }
bool has_solver() { return m_re2aut.has_solver(); }
bool coalesce_chars() const { return m_coalesce_chars; }

7
src/ast/rewriter/th_rewriter.cpp
View file

@ -933,9 +933,6 @@ struct th_rewriter::imp : public rewriter_tpl<th_rewriter_cfg> {
return m_cfg.mk_eq(a, b);
}
void set_solver(expr_solver* solver) {
m_cfg.m_seq_rw.set_solver(solver);
}
};
th_rewriter::th_rewriter(ast_manager & m, params_ref const & p):
@ -1057,10 +1054,6 @@ expr_ref th_rewriter::mk_eq(expr* a, expr* b) {
return m_imp->mk_eq(a, b);
}
void th_rewriter::set_solver(expr_solver* solver) {
m_imp->set_solver(solver);
}
bool th_rewriter::reduce_quantifier(quantifier * old_q,
expr * new_body,

1
src/ast/rewriter/th_rewriter.h
View file

@ -74,7 +74,6 @@ public:
expr_dependency * get_used_dependencies();
void reset_used_dependencies();
void set_solver(expr_solver* solver);
};

7
src/ast/simplifiers/bound_simplifier.cpp
View file

@ -135,7 +135,12 @@ bool bound_simplifier::reduce_arg(expr* arg, expr_ref& result) {
}
void bound_simplifier::reduce() {
#if 0
smt_params_helper sp(p);
if (!sp.bound_simplifier())
return;
#endif
bool updated = true, found_bound = false;
for (unsigned i = 0; i < 5 && updated; ++i) {
updated = false;

74
src/ast/simplifiers/dependent_expr_state.h
View file

@ -33,6 +33,7 @@ Author:
#include "util/statistics.h"
#include "util/params.h"
#include "util/z3_exception.h"
#include "ast/ast_util.h"
#include "ast/converters/model_converter.h"
#include "ast/simplifiers/dependent_expr.h"
#include "ast/simplifiers/model_reconstruction_trail.h"
@ -113,9 +114,80 @@ public:
model_reconstruction_trail& model_trail() override { throw default_exception("unexpected access to model reconstruction"); }
bool updated() override { return false; }
void reset_updated() override {}
};
struct base_dependent_expr_state : public dependent_expr_state {
ast_manager& m;
model_reconstruction_trail m_reconstruction_trail;
bool m_updated = false;
bool m_inconsistent = false;
vector<dependent_expr> m_fmls;
base_dependent_expr_state(ast_manager& m) :dependent_expr_state(m), m(m), m_reconstruction_trail(m, m_trail) {}
unsigned qtail() const override { return m_fmls.size(); }
dependent_expr const& operator[](unsigned i) override { return m_fmls[i]; }
void update(unsigned i, dependent_expr const& j) override {
SASSERT(j.fml());
check_false(j.fml());
m_fmls[i] = j;
m_updated = true;
}
void add(dependent_expr const& j) override { m_updated = true; check_false(j.fml()); m_fmls.push_back(j); }
bool inconsistent() override { return m_inconsistent; }
bool updated() override { return m_updated; }
void reset_updated() override { m_updated = false; }
model_reconstruction_trail& model_trail() override { return m_reconstruction_trail; }
std::ostream& display(std::ostream& out) const override {
unsigned i = 0;
for (auto const& d : m_fmls) {
if (i > 0 && i == qhead())
out << "---- head ---\n";
out << d << "\n";
++i;
}
m_reconstruction_trail.display(out);
return out;
}
void check_false(expr* f) {
if (m.is_false(f))
m_inconsistent = true;
}
void replay(unsigned qhead, expr_ref_vector& assumptions) {
m_reconstruction_trail.replay(qhead, assumptions, *this);
}
void flatten_suffix() override {
expr_mark seen;
unsigned j = qhead();
expr_ref_vector pinned(m);
for (unsigned i = qhead(); i < qtail(); ++i) {
expr* f = m_fmls[i].fml(), * g = nullptr;
pinned.push_back(f);
if (seen.is_marked(f))
continue;
seen.mark(f, true);
if (m.is_true(f))
continue;
if (m.is_and(f)) {
auto* d = m_fmls[i].dep();
for (expr* arg : *to_app(f))
add(dependent_expr(m, arg, nullptr, d));
continue;
}
if (m.is_not(f, g) && m.is_or(g)) {
auto* d = m_fmls[i].dep();
for (expr* arg : *to_app(g))
add(dependent_expr(m, mk_not(m, arg), nullptr, d));
continue;
}
if (i != j)
m_fmls[j] = m_fmls[i];
++j;
}
m_fmls.shrink(j);
}
};
inline std::ostream& operator<<(std::ostream& out, dependent_expr_state& st) {
return st.display(out);
}

17
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -112,7 +112,7 @@ eliminate:
--*/
#include "params/smt_params_helper.hpp"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/recfun_decl_plugin.h"
@ -166,7 +166,7 @@ void elim_unconstrained::eliminate() {
expr_ref rr(m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz), m);
bool inverted = m_inverter(t->get_decl(), t->get_num_args(), m_args.data() + sz, r);
proof_ref pr(m);
if (inverted && m_enable_proofs) {
if (inverted && m_config.m_enable_proofs) {
expr * s = m.mk_app(t->get_decl(), t->get_num_args(), m_args.data() + sz);
expr * eq = m.mk_eq(s, r);
proof * pr1 = m.mk_def_intro(eq);
@ -267,7 +267,7 @@ void elim_unconstrained::reset_nodes() {
*/
void elim_unconstrained::init_nodes() {
m_enable_proofs = false;
m_config.m_enable_proofs = false;
m_trail.reset();
m_fmls.freeze_suffix();
@ -276,7 +276,7 @@ void elim_unconstrained::init_nodes() {
auto [f, p, d] = m_fmls[i]();
terms.push_back(f);
if (p)
m_enable_proofs = true;
m_config.m_enable_proofs = true;
}
m_heap.reset();
@ -303,7 +303,7 @@ void elim_unconstrained::init_nodes() {
for (expr* e : terms)
get_node(e).set_top();
m_inverter.set_produce_proofs(m_enable_proofs);
m_inverter.set_produce_proofs(m_config.m_enable_proofs);
}
@ -422,6 +422,8 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
}
void elim_unconstrained::reduce() {
if (!m_config.m_enabled)
return;
generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
m_inverter.set_model_converter(mc.get());
m_created_compound = true;
@ -436,3 +438,8 @@ void elim_unconstrained::reduce() {
mc->reset();
}
}
void elim_unconstrained::updt_params(params_ref const& p) {
smt_params_helper sp(p);
m_config.m_enabled = sp.elim_unconstrained();
}

9
src/ast/simplifiers/elim_unconstrained.h
View file

@ -79,6 +79,10 @@ class elim_unconstrained : public dependent_expr_simplifier {
unsigned m_num_eliminated = 0;
void reset() { m_num_eliminated = 0; }
};
struct config {
bool m_enabled = true;
bool m_enable_proofs = false;
};
expr_inverter m_inverter;
ptr_vector<node> m_nodes;
var_lt m_lt;
@ -86,8 +90,8 @@ class elim_unconstrained : public dependent_expr_simplifier {
expr_ref_vector m_trail;
expr_ref_vector m_args;
stats m_stats;
config m_config;
bool m_created_compound = false;
bool m_enable_proofs = false;
bool is_var_lt(int v1, int v2) const;
node& get_node(unsigned n) const { return *m_nodes[n]; }
@ -119,4 +123,7 @@ public:
void collect_statistics(statistics& st) const override { st.update("elim-unconstrained", m_stats.m_num_eliminated); }
void reset_statistics() override { m_stats.reset(); }
void updt_params(params_ref const& p) override;
};

356
src/ast/simplifiers/euf_completion.cpp
View file

@ -68,6 +68,8 @@ namespace euf {
m_mam(mam::mk(*this, *this)),
m_canonical(m),
m_eargs(m),
m_expr_trail(m),
m_consequences(m),
m_canonical_proofs(m),
// m_infer_patterns(m, m_smt_params),
m_deps(m),
@ -135,6 +137,7 @@ namespace euf {
};
m_matcher.set_on_match(on_match);
}
completion::~completion() {
@ -230,15 +233,59 @@ namespace euf {
read_egraph();
IF_VERBOSE(1, verbose_stream() << "(euf.completion :rounds " << rounds << " :instances " << m_stats.m_num_instances << " :stop " << should_stop() << ")\n");
}
map_congruences();
for (auto c : m_consequences)
add_consequence(c);
TRACE(euf_completion, m_egraph.display(tout));
}
void completion::map_congruences() {
unsigned sz = qtail();
for (unsigned i = qhead(); i < sz; ++i) {
auto [f, p, d] = m_fmls[i]();
if (is_congruences(f))
map_congruence(to_app(f)->get_arg(0));
}
}
void completion::map_congruence(expr* t) {
auto n = m_egraph.find(t);
if (!n)
return;
expr_ref_vector args(m);
expr_mark visited;
proof_ref pr(m);
expr_dependency_ref dep(m);
auto canon = get_canonical(n->get_expr(), pr, dep);
args.push_back(canon);
visited.mark(canon);
for (auto s : enode_class(n)) {
expr_ref r(s->get_expr(), m);
m_rewriter(r);
if (visited.is_marked(r))
continue;
visited.mark(r);
args.push_back(r);
}
expr_ref cong(m);
cong = m.mk_app(symbol("congruence"), args.size(), args.data(), m.mk_bool_sort());
m_fmls.add(dependent_expr(m, cong, nullptr, nullptr));
}
void completion::add_consequence(expr* f) {
expr_ref r(f, m);
m_rewriter(r);
f = r.get();
auto cons = m.mk_app(symbol("consequence"), 1, &f, m.mk_bool_sort());
m_fmls.add(dependent_expr(m, cons, nullptr, nullptr));
}
void completion::add_egraph() {
m_nodes_to_canonize.reset();
unsigned sz = qtail();
for (unsigned i = qhead(); i < sz; ++i) {
auto [f, p, d] = m_fmls[i]();
add_constraint(f, p, d);
}
m_should_propagate = true;
@ -248,9 +295,12 @@ namespace euf {
m_mam->propagate();
flush_binding_queue();
propagate_rules();
propagate_closures();
IF_VERBOSE(11, verbose_stream() << "propagate " << m_stats.m_num_instances << "\n");
if (!should_stop())
propagate_arithmetic();
if (!m_should_propagate && !should_stop())
propagate_all_rules();
propagate_all_rules();
}
TRACE(euf, m_egraph.display(tout));
}
@ -271,57 +321,79 @@ namespace euf {
for (auto* ch : enode_args(n))
m_nodes_to_canonize.push_back(ch);
};
expr* x, * y;
expr* x = nullptr, * y = nullptr, * nf = nullptr;
if (m.is_eq(f, x, y)) {
expr_ref x1(x, m);
expr_ref y1(y, m);
m_rewriter(x1);
m_rewriter(y1);
add_quantifiers(x1);
add_quantifiers(x);
add_quantifiers(y1);
enode* a = mk_enode(x1);
enode* a = mk_enode(x);
enode* b = mk_enode(y1);
if (a->get_root() == b->get_root())
return;
m_egraph.merge(a, b, to_ptr(push_pr_dep(pr, d)));
return;
expr_ref x1(x, m);
m_rewriter(x1);
// enode* a1 = mk_enode(x1);
// if (a->get_root() != a1->get_root())
// m_egraph.merge(a, a1, nullptr);
TRACE(euf, tout << "merge and propagate\n");
add_children(a);
add_children(b);
auto a1 = mk_enode(x);
if (a1->get_root() != a->get_root()) {
m_egraph.merge(a, a1, nullptr);
add_children(a1);
}
auto b1 = mk_enode(y);
if (b1->get_root() != b->get_root()) {
m_egraph.merge(b, b1, nullptr);
add_children(b1);
}
m_should_propagate = true;
if (m_side_condition_solver)
m_egraph.merge(a, b, to_ptr(push_pr_dep(pr, d)));
m_egraph.propagate();
m_should_propagate = true;
if (m_side_condition_solver && a->get_root() != b->get_root())
m_side_condition_solver->add_constraint(f, pr, d);
IF_VERBOSE(1, verbose_stream() << "eq: " << mk_pp(x1, m) << " == " << mk_pp(y1, m) << "\n");
IF_VERBOSE(1, verbose_stream() << "eq: " << a->get_root_id() << " " << b->get_root_id() << " "
<< mk_pp(x, m) << " == " << y1 << "\n");
}
else if (m.is_not(f, f)) {
enode* n = mk_enode(f);
else if (m.is_not(f, nf)) {
expr_ref f1(nf, m);
m_rewriter(f1);
enode* n = mk_enode(f1);
if (m.is_false(n->get_root()->get_expr()))
return;
add_quantifiers(f);
add_quantifiers(f1);
auto n_false = mk_enode(m.mk_false());
auto j = to_ptr(push_pr_dep(pr, d));
m_egraph.new_diseq(n, j);
m_egraph.merge(n, n_false, j);
if (nf != f1)
m_egraph.merge(n, mk_enode(nf), nullptr);
m_egraph.propagate();
add_children(n);
m_should_propagate = true;
if (m_side_condition_solver)
m_side_condition_solver->add_constraint(f, pr, d);
IF_VERBOSE(1, verbose_stream() << "not: " << mk_pp(f, m) << "\n");
IF_VERBOSE(1, verbose_stream() << "not: " << nf << "\n");
}
else if (is_congruences(f)) {
auto t = to_app(f)->get_arg(0);
expr_ref r(t, m);
m_rewriter(r);
auto a = mk_enode(t);
auto b = mk_enode(r);
m_egraph.merge(a, b, nullptr);
m_egraph.propagate();
}
else {
expr_ref f1(f, m);
if (!m.is_implies(f) && !is_quantifier(f)) {
m_rewriter(f1);
f = f1;
}
enode* n = mk_enode(f);
if (m.is_true(n->get_root()->get_expr()))
return;
IF_VERBOSE(1, verbose_stream() << "fml: " << mk_pp(f, m) << "\n");
m_egraph.merge(n, m_tt, to_ptr(push_pr_dep(pr, d)));
m_egraph.propagate();
add_children(n);
if (is_forall(f)) {
quantifier* q = to_quantifier(f);
@ -352,7 +424,7 @@ namespace euf {
}
add_rule(f, pr, d);
if (!is_forall(f) && !m.is_implies(f)) {
if (!is_forall(f) && !m.is_implies(f) && !m.is_or(f)) {
add_quantifiers(f);
if (m_side_condition_solver)
m_side_condition_solver->add_constraint(f, pr, d);
@ -388,18 +460,27 @@ namespace euf {
else if (is_quantifier(t)) {
auto q = to_quantifier(t);
auto nd = q->get_num_decls();
verbose_stream() << "bind " << mk_pp(q, m) << "\n";
IF_VERBOSE(1, verbose_stream() << "bind " << mk_pp(q, m) << "\n");
for (unsigned i = 0; i < nd; ++i) {
auto name = std::string("bound!") + std::to_string(bound.size());
auto b = m.mk_const(name, q->get_decl_sort(i));
// TODO: persist bound variables withn scope to avoid reference count crashes
if (b->get_ref_count() == 0) {
m_expr_trail.push_back(b);
get_trail().push(push_back_vector(m_expr_trail));
}
bound.push_back(b);
}
expr_ref inst = var_subst(m)(q->get_expr(), bound);
if (!m_egraph.find(inst)) {
expr_ref clos(m);
m_closures.insert(q, { bound, inst });
get_trail().push(insert_map(m_closures, q));
mk_enode(inst);
// ensure that inst occurs in a foreign context to enable equality propagation
// on inst.
func_decl* f = m.mk_func_decl(symbol("clos!"), inst->get_sort(), m.mk_bool_sort());
clos = m.mk_app(f, inst);
mk_enode(clos);
// TODO: handle nested quantifiers after m_closures is updated to
// index on sort declaration prefix together with quantifier
// add_quantifiers(bound, inst);
@ -445,13 +526,30 @@ namespace euf {
void completion::add_rule(expr* f, proof* pr, expr_dependency* d) {
expr* x = nullptr, * y = nullptr;
if (!m.is_implies(f, x, y))
return;
expr_ref_vector body(m);
proof_ref pr_i(m), pr0(m);
expr_ref_vector prs(m);
expr_ref head(y, m);
body.push_back(x);
expr_ref head(m);
if (m.is_implies(f, x, y)) {
head = y;
body.push_back(x);
}
else if (m.is_or(f)) {
for (auto arg : *to_app(f)) {
if (m.is_eq(arg)) {
if (head)
return;
head = arg;
}
else
body.push_back(arg);
}
if (!head)
return;
}
else
return;
flatten_and(body);
unsigned j = 0;
flet<bool> _propagate_with_solver(m_propagate_with_solver, true);
@ -552,6 +650,121 @@ namespace euf {
}
}
//
// extract shared arithmetic terms T
// extract shared variables V
// add t = rewriter(t) to E-graph
// solve for V by solver producing theta
// add theta to E-graph
// add theta to canonize (?)
//
void completion::propagate_arithmetic() {
ptr_vector<expr> shared_terms, shared_vars;
expr_mark visited;
arith_util a(m);
bool merged = false;
for (auto n : m_egraph.nodes()) {
expr* e = n->get_expr();
if (!is_app(e))
continue;
app* t = to_app(e);
bool is_arith = a.is_arith_expr(t);
for (auto arg : *t) {
bool is_arith_arg = a.is_arith_expr(arg);
if (is_arith_arg == is_arith)
continue;
if (visited.is_marked(arg))
continue;
visited.mark(arg);
if (is_arith_arg)
shared_terms.push_back(arg);
else
shared_vars.push_back(arg);
}
}
for (auto t : shared_terms) {
auto tn = m_egraph.find(t);
if (!tn)
continue;
expr_ref r(t, m);
m_rewriter(r);
if (r == t)
continue;
auto n = m_egraph.find(t);
auto t_root = tn->get_root();
if (n && n->get_root() == t_root)
continue;
if (!n)
n = mk_enode(r);
TRACE(euf_completion, tout << "propagate-arith: " << mk_pp(t, m) << " -> " << r << "\n");
m_egraph.merge(tn, n, nullptr);
merged = true;
}
visited.reset();
for (auto v : shared_vars) {
if (visited.is_marked(v))
continue;
visited.mark(v);
vector<side_condition_solver::solution> sol;
expr_ref term(m), guard(m);
sol.push_back({ v, term, guard });
m_side_condition_solver->solve_for(sol);
for (auto [v, t, g] : sol) {
if (!t)
continue;
visited.mark(v);
auto a = mk_enode(v);
auto b = mk_enode(t);
if (a->get_root() == b->get_root())
continue;
TRACE(euf_completion, tout << "propagate-arith: " << m_egraph.bpp(a) << " -> " << m_egraph.bpp(b) << "\n");
IF_VERBOSE(1, verbose_stream() << "propagate-arith: " << m_egraph.bpp(a) << " -> " << m_egraph.bpp(b) << "\n");
m_egraph.merge(a, b, nullptr); // TODO guard justifies reason.
merged = true;
}
}
if (merged) {
m_egraph.propagate();
m_should_propagate = true;
}
}
void completion::propagate_closures() {
for (auto [q, clos] : m_closures) {
expr* body = clos.second;
auto n = m_egraph.find(body);
SASSERT(n);
#if 0
verbose_stream() << "class of " << mk_pp(body, m) << "\n";
for (auto s : euf::enode_class(n)) {
verbose_stream() << mk_pp(s->get_expr(), m) << "\n";
}
#endif
if (n->is_root())
continue;
auto qn = m_egraph.find(q);
#if 0
verbose_stream() << "class of " << mk_pp(q, m) << "\n";
for (auto s : euf::enode_class(qn)) {
verbose_stream() << mk_pp(s->get_expr(), m) << "\n";
}
#endif
expr_ref new_body = expr_ref(n->get_root()->get_expr(), m);
expr_ref new_q = expr_abstract(m, clos.first, new_body);
new_q = m.update_quantifier(q, new_q);
auto new_qn = m_egraph.find(new_q);
if (!new_qn)
new_qn = m_egraph.mk(new_q, qn->generation(), 0, nullptr);
if (new_qn->get_root() == qn->get_root())
continue;
m_egraph.merge(new_qn, qn, nullptr); // todo track dependencies
m_should_propagate = true;
}
}
binding* completion::tmp_binding(quantifier* q, app* pat, euf::enode* const* _binding) {
if (q->get_num_decls() > m_tmp_binding_capacity) {
void* mem = memory::allocate(sizeof(binding) + q->get_num_decls() * sizeof(euf::enode*));
@ -584,7 +797,7 @@ namespace euf {
b = new (mem) binding(q, pat, max_generation, min_top, max_top);
b->init(b);
for (unsigned i = 0; i < n; ++i)
b->m_nodes[i] = _binding[i];
b->m_nodes[i] = _binding[i]->get_root();
m_bindings.insert(b);
get_trail().push(insert_map<bindings, binding*>(m_bindings, b));
@ -643,11 +856,13 @@ namespace euf {
void completion::apply_binding(binding& b, quantifier* q, expr_ref_vector const& s) {
var_subst subst(m);
expr_ref r = subst(q->get_expr(), s);
expr_ref r = subst(q->get_expr(), s);
scoped_generation sg(*this, b.m_max_top_generation + 1);
auto [pr, d] = get_dependency(q);
if (pr)
pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), r), s.size(), s.data());
m_consequences.push_back(r);
TRACE(euf_completion, tout << "new instantiation: " << r << " q: " << mk_pp(q, m) << "\n");
add_constraint(r, pr, d);
propagate_rules();
m_egraph.propagate();
@ -788,7 +1003,7 @@ namespace euf {
if (x1 == y1)
r = expr_ref(m.mk_true(), m);
else {
expr* c = get_canonical(x, pr3, d);
auto c = get_canonical(x, pr3, d);
if (c == x1)
r = m_rewriter.mk_eq(y1, c);
else if (c == y1)
@ -832,8 +1047,6 @@ namespace euf {
}
expr_ref completion::canonize(expr* f, proof_ref& pr, expr_dependency_ref& d) {
if (is_quantifier(f))
return expr_ref(canonize(to_quantifier(f), pr, d), m);
if (!is_app(f))
return expr_ref(f, m); // todo could normalize ground expressions under quantifiers
@ -862,13 +1075,29 @@ namespace euf {
return r;
}
expr_ref completion::canonize(quantifier* q, proof_ref& pr, expr_dependency_ref& d) {
expr_ref completion::get_canonical(quantifier* q, proof_ref& pr, expr_dependency_ref& d) {
std::pair<ptr_vector<expr>, expr*> clos;
// verbose_stream() << "canonize " << mk_pp(q, m) << "\n";
if (!m_closures.find(q, clos))
return expr_ref(q, m);
expr* body = clos.second;
expr_ref new_body = canonize(body, pr, d);
SASSERT(m_egraph.find(body));
#if 0
verbose_stream() << "class of " << mk_pp(body, m) << "\n";
for (auto s : euf::enode_class(n)) {
verbose_stream() << mk_pp(s->get_expr(), m) << "\n";
}
#endif
// auto n = m_egraph.find(q);
#if 0
verbose_stream() << "class of " << mk_pp(q, m) << "\n";
for (auto s : euf::enode_class(n)) {
verbose_stream() << mk_pp(s->get_expr(), m) << "\n";
}
#endif
expr_ref new_body = get_canonical(body, pr, d);
expr_ref result = expr_abstract(m, clos.first, new_body);
result = m.update_quantifier(q, result);
if (m.proofs_enabled()) {
// add proof rule
//
@ -881,20 +1110,38 @@ namespace euf {
}
expr* completion::get_canonical(expr* f, proof_ref& pr, expr_dependency_ref& d) {
expr_ref completion::get_canonical(expr* f, proof_ref& pr, expr_dependency_ref& d) {
expr_ref e(m);
if (has_quantifiers(f)) {
if (is_quantifier(f))
return get_canonical(to_quantifier(f), pr, d);
else if (is_app(f)) {
expr_ref_vector args(m);
for (auto arg : *to_app(f)) {
// TODO: pr reconstruction
args.push_back(get_canonical(arg, pr, d));
}
e = m.mk_app(to_app(f)->get_decl(), args);
if (!m_egraph.find(e))
return e;
f = e;
}
else
UNREACHABLE();
}
enode* n = m_egraph.find(f);
if (!n) verbose_stream() << "not found " << f->get_id() << " " << mk_pp(f, m) << "\n";
if (!n) n = mk_enode(f);
enode* r = n->get_root();
d = m.mk_join(d, explain_eq(n, r));
d = m.mk_join(d, m_deps.get(r->get_id(), nullptr));
if (m.proofs_enabled()) {
pr = prove_eq(n, r);
if (get_canonical_proof(r))
pr = m.mk_transitivity(pr, get_canonical_proof(r));
if (get_canonical_proof(r))
pr = m.mk_transitivity(pr, get_canonical_proof(r));
}
SASSERT(m_canonical.get(r->get_id()));
return m_canonical.get(r->get_id());
if (!m_canonical.get(r->get_id()))
m_canonical.setx(r->get_id(), r->get_expr());
return expr_ref(m_canonical.get(r->get_id()), m);
}
expr* completion::get_canonical(enode* n) {
@ -990,6 +1237,7 @@ namespace euf {
void completion::collect_statistics(statistics& st) const {
st.update("euf-completion-rewrites", m_stats.m_num_rewrites);
st.update("euf-completion-instances", m_stats.m_num_instances);
m_egraph.collect_statistics(st);
}
bool completion::is_gt(expr* lhs, expr* rhs) const {
@ -1098,8 +1346,8 @@ namespace euf {
proof_ref pr(m);
prs.reset();
for (enode* arg : enode_args(rep)) {
enode* rarg = arg->get_root();
expr* c = get_canonical(rarg);
auto rarg = arg->get_root();
auto c = get_canonical(rarg);
if (c) {
m_eargs.push_back(c);
new_arg |= c != arg->get_expr();

15
src/ast/simplifiers/euf_completion.h
View file

@ -128,7 +128,7 @@ namespace euf {
enode* m_tt, *m_ff;
ptr_vector<expr> m_todo;
enode_vector m_args, m_reps, m_nodes_to_canonize;
expr_ref_vector m_canonical, m_eargs;
expr_ref_vector m_canonical, m_eargs, m_expr_trail, m_consequences;
proof_ref_vector m_canonical_proofs;
// pattern_inference_rw m_infer_patterns;
bindings m_bindings;
@ -166,11 +166,18 @@ namespace euf {
void read_egraph();
expr_ref canonize(expr* f, proof_ref& pr, expr_dependency_ref& dep);
expr_ref canonize_fml(expr* f, proof_ref& pr, expr_dependency_ref& dep);
expr* get_canonical(expr* f, proof_ref& pr, expr_dependency_ref& d);
expr_ref get_canonical(expr* f, proof_ref& pr, expr_dependency_ref& d);
expr* get_canonical(enode* n);
proof* get_canonical_proof(enode* n);
void set_canonical(enode* n, expr* e, proof* pr);
void add_constraint(expr*f, proof* pr, expr_dependency* d);
void map_congruences();
void map_congruence(expr* t);
void add_consequence(expr* t);
bool is_congruences(expr* f) const {
return is_app(f) && to_app(f)->get_num_args() == 1 && symbol("congruences") == to_app(f)->get_decl()->get_name();
}
// Enable equality propagation inside of quantifiers
// add quantifier bodies as closure terms to the E-graph.
@ -181,9 +188,10 @@ namespace euf {
// Closure terms are re-abstracted by the canonizer.
void add_quantifiers(ptr_vector<expr>& bound, expr* t);
void add_quantifiers(expr* t);
expr_ref canonize(quantifier* q, proof_ref& pr, expr_dependency_ref& d);
expr_ref get_canonical(quantifier* q, proof_ref& pr, expr_dependency_ref& d);
obj_map<quantifier, std::pair<ptr_vector<expr>, expr*>> m_closures;
void propagate_arithmetic();
expr_dependency* explain_eq(enode* a, enode* b);
proof_ref prove_eq(enode* a, enode* b);
proof_ref prove_conflict();
@ -208,6 +216,7 @@ namespace euf {
void propagate_rule(conditional_rule& r);
void propagate_rules();
void propagate_all_rules();
void propagate_closures();
void clear_propagation_queue();
ptr_vector<conditional_rule> m_propagation_queue;
struct push_watch_rule;

2
src/ast/simplifiers/extract_eqs.cpp
View file

@ -115,7 +115,7 @@ namespace euf {
if (is_eq_of(x2, y1, z, s, t) && is_complementary(x1, y2))
eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(x1, s, t), m), d));
}
if (m.is_and(f, x1, y1) && m.is_or(x, x1, x2) && m.is_or(y1, y1, y2)) {
if (m.is_and(f, x1, y1) && m.is_or(x1, x1, x2) && m.is_or(y1, y1, y2)) {
expr* z = nullptr, *t = nullptr, *s = nullptr;
if (is_eq_of(x1, y1, z, s, t) && is_complementary(x2, y2))
eqs.push_back(dependent_eq(e.fml(), to_app(z), expr_ref(m.mk_ite(y2, s, t), m), d));

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

@ -80,6 +80,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
add_vars(v, free_vars);
st.add(dependent_expr(m, m.mk_eq(k, v), nullptr, nullptr));
}
m_trail_stack.push(value_trail(t->m_active));
t->m_active = false;
continue;
}
@ -90,6 +91,7 @@ void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumpt
TRACE(simplifier, tout << "replay removed " << r << "\n");
st.add(r);
}
m_trail_stack.push(value_trail(t->m_active));
t->m_active = false;
continue;
}

14
src/ast/simplifiers/solve_eqs.cpp
View file

@ -46,6 +46,7 @@ Outline of a presumably better scheme:
#include "ast/simplifiers/solve_context_eqs.h"
#include "ast/converters/generic_model_converter.h"
#include "params/tactic_params.hpp"
#include "params/smt_params_helper.hpp"
namespace euf {
@ -118,7 +119,10 @@ namespace euf {
SASSERT(j == var2id(v));
if (m_fmls.frozen(v))
continue;
if (!m_config.m_enable_non_ground && has_quantifiers(t))
continue;
bool is_safe = true;
unsigned todo_sz = todo.size();
@ -126,6 +130,8 @@ namespace euf {
// all time-stamps must be at or above current level
// unexplored variables that are part of substitution are appended to work list.
SASSERT(m_todo.empty());
m_todo.push_back(t);
expr_fast_mark1 visited;
while (!m_todo.empty()) {
@ -224,6 +230,9 @@ namespace euf {
void solve_eqs::reduce() {
if (!m_config.m_enabled)
return;
m_fmls.freeze_suffix();
for (extract_eq* ex : m_extract_plugins)
@ -330,6 +339,9 @@ namespace euf {
for (auto* ex : m_extract_plugins)
ex->updt_params(p);
m_rewriter.updt_params(p);
smt_params_helper sp(p);
m_config.m_enabled = sp.solve_eqs();
m_config.m_enable_non_ground = sp.solve_eqs_non_ground();
}
void solve_eqs::collect_param_descrs(param_descrs& r) {

2
src/ast/simplifiers/solve_eqs.h
View file

@ -41,6 +41,8 @@ namespace euf {
struct config {
bool m_context_solve = true;
unsigned m_max_occs = UINT_MAX;
bool m_enabled = true;
bool m_enable_non_ground = true;
};
stats m_stats;

6
src/ast/sls/sls_arith_base.cpp
View file

@ -2588,6 +2588,8 @@ namespace sls {
template<typename num_t>
void arith_base<num_t>::invariant() {
if (m.limit().is_canceled())
return;
for (unsigned v = 0; v < ctx.num_bool_vars(); ++v) {
auto ineq = get_ineq(v);
if (ineq)
@ -2622,6 +2624,8 @@ namespace sls {
};
for (var_t v = 0; v < m_vars.size(); ++v) {
if (!eval_is_correct(v)) {
if (m.limit().is_canceled())
return;
report_error(verbose_stream(), v);
TRACE(arith, report_error(tout, v));
UNREACHABLE();
@ -2707,6 +2711,8 @@ namespace sls {
void arith_base<num_t>::update_unchecked(var_t v, num_t const& new_value) {
auto& vi = m_vars[v];
auto old_value = value(v);
if (old_value == new_value)
return;
IF_VERBOSE(5, verbose_stream() << "update: v" << v << " " << mk_bounded_pp(vi.m_expr, m) << " := " << old_value << " -> " << new_value << "\n");
TRACE(arith, tout << "update: v" << v << " " << mk_bounded_pp(vi.m_expr, m) << " := " << old_value << " -> " << new_value << "\n");
vi.set_value(new_value);

31
src/ast/sls/sls_bv_tracker.h
View file

@ -42,8 +42,37 @@ class sls_tracker {
struct value_score {
value_score() : value(unsynch_mpz_manager::mk_z(0)) {};
value_score(value_score&&) noexcept = default;
value_score(const value_score &other) {
m = other.m;
if (other.m && !unsynch_mpz_manager::is_zero(other.value)) {
m->set(value, other.value);
}
score = other.score;
score_prune = other.score_prune;
has_pos_occ = other.has_pos_occ;
has_neg_occ = other.has_neg_occ;
distance = other.distance;
touched = other.touched;
}
~value_score() { if (m) m->del(value); }
value_score& operator=(value_score&&) = default;
value_score& operator=(value_score&&) noexcept = default;
value_score &operator=(const value_score &other) {
if (this != &other) {
if (m)
m->del(value);
m = other.m;
if (other.m && !unsynch_mpz_manager::is_zero(other.value)) {
m->set(value, other.value);
}
score = other.score;
score_prune = other.score_prune;
has_pos_occ = other.has_pos_occ;
has_neg_occ = other.has_neg_occ;
distance = other.distance;
touched = other.touched;
}
return *this;
}
unsynch_mpz_manager * m = nullptr;
mpz value;
double score = 0.0;

48
src/cmd_context/basic_cmds.cpp
View file

@ -334,6 +334,52 @@ public:
}
};
class prefer_cmd : public cmd {
expr *m_formula = nullptr;
public:
prefer_cmd() : cmd("prefer") {}
char const *get_usage() const override {
return "<formula>";
}
char const *get_descr(cmd_context &ctx) const override {
return "set a preferred formula for the solver";
}
unsigned get_arity() const override {
return 1;
}
void prepare(cmd_context &ctx) override {
m_formula = nullptr;
}
cmd_arg_kind next_arg_kind(cmd_context &ctx) const override {
return CPK_EXPR;
}
void set_next_arg(cmd_context &ctx, expr *e) override {
m_formula = e;
}
void execute(cmd_context &ctx) override {
SASSERT(m_formula);
ctx.set_preferred(m_formula);
}
};
class reset_preferences_cmd : public cmd {
public:
reset_preferences_cmd() : cmd("reset-preferences") {}
char const *get_usage() const override {
return "";
}
char const *get_descr(cmd_context &ctx) const override {
return "reset all preferred formulas";
}
unsigned get_arity() const override {
return 0;
}
void execute(cmd_context &ctx) override {
ctx.reset_preferred();
}
};
class set_get_option_cmd : public cmd {
protected:
symbol m_true;
@ -926,6 +972,8 @@ void install_basic_cmds(cmd_context & ctx) {
ctx.insert(alloc(get_info_cmd));
ctx.insert(alloc(set_info_cmd));
ctx.insert(alloc(set_initial_value_cmd));
ctx.insert(alloc(prefer_cmd));
ctx.insert(alloc(reset_preferences_cmd));
ctx.insert(alloc(get_consequences_cmd));
ctx.insert(alloc(builtin_cmd, "assert", "<term>", "assert term."));
ctx.insert(alloc(builtin_cmd, "check-sat", "<boolean-constants>*", "check if the current context is satisfiable. If a list of boolean constants B is provided, then check if the current context is consistent with assigning every constant in B to true."));

96
src/cmd_context/cmd_context.cpp
View file

@ -628,6 +628,7 @@ cmd_context::~cmd_context() {
finalize_tactic_manager();
m_proof_cmds = nullptr;
m_var2values.reset();
m_preferred = nullptr;
reset(true);
m_mcs.reset();
m_solver = nullptr;
@ -656,6 +657,8 @@ void cmd_context::set_opt(opt_wrapper* opt) {
for (auto const& [var, value] : m_var2values)
m_opt->initialize_value(var, value);
m_opt->set_logic(m_logic);
if (m_preferred)
m_opt->set_preferred(m_preferred.get());
}
void cmd_context::global_params_updated() {
@ -1217,32 +1220,65 @@ bool cmd_context::try_mk_builtin_app(symbol const & s, unsigned num_args, expr *
return nullptr != result.get();
}
bool cmd_context::try_mk_declared_app(symbol const & s, unsigned num_args, expr * const * args,
unsigned num_indices, parameter const * indices, sort * range,
expr_ref & result) {
bool cmd_context::try_mk_declared_app(symbol const &s, unsigned num_args, expr *const *args, unsigned num_indices,
parameter const *indices, sort *range, expr_ref &result) {
if (!m_func_decls.contains(s))
return false;
func_decls& fs = m_func_decls.find(s);
func_decls &fs = m_func_decls.find(s);
if (num_args == 0 && !range) {
if (fs.more_than_one())
throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) to disambiguate ", s);
func_decl * f = fs.first();
throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a "
"qualified expression (as <symbol> <sort>) to disambiguate ",
s);
func_decl *f = fs.first();
if (!f)
return false;
if (f->get_arity() != 0)
if (f->get_arity() != 0)
result = array_util(m()).mk_as_array(f);
else
else
result = m().mk_const(f);
return true;
}
func_decl * f = fs.find(m(), num_args, args, range);
if (!f)
return false;
if (well_sorted_check_enabled())
m().check_sort(f, num_args, args);
result = m().mk_app(f, num_args, args);
return true;
func_decl *f = fs.find(m(), num_args, args, range);
if (f) {
if (f && well_sorted_check_enabled())
m().check_sort(f, num_args, args);
result = m().mk_app(f, num_args, args);
return true;
}
// f could be declared as an array and applied without explicit select
if (num_args > 0 && !range) {
if (fs.more_than_one())
throw cmd_exception("ambiguous constant reference, more than one constant with the same sort, use a "
"qualified expression (as <symbol> <sort>) to disambiguate ",
s);
func_decl *f = fs.first();
if (!f)
return false;
if (f->get_arity() != 0)
return false;
array_util au(m());
auto s = f->get_range();
if (!au.is_array(s))
return false;
unsigned sz = get_array_arity(s);
if (sz != num_args)
return false;
for (unsigned i = 0; i < sz; i++)
if (args[i]->get_sort() != get_array_domain(s, i))
return false;
expr_ref_vector new_args(m());
new_args.push_back(m().mk_const(f));
for (unsigned i = 0; i < num_args; i++)
new_args.push_back(args[i]);
result = au.mk_select(new_args.size(), new_args.data());
return true;
}
return false;
}
bool cmd_context::try_mk_macro_app(symbol const & s, unsigned num_args, expr * const * args,
@ -1518,6 +1554,8 @@ void cmd_context::reset(bool finalize) {
m_dt_eh = nullptr;
m_std_subst = nullptr;
m_rev_subst = nullptr;
m_preferred = nullptr;
m_var2values.reset();
if (m_manager) {
dealloc(m_pmanager);
m_pmanager = nullptr;
@ -1884,6 +1922,27 @@ void cmd_context::set_initial_value(expr* var, expr* value) {
m_var2values.push_back({expr_ref(var, m()), expr_ref(value, m())});
}
void cmd_context::set_preferred(expr* fmla) {
if (!m_preferred) {
auto p = alloc(preferred_value_propagator, m());
m_preferred = p;
if (get_solver()) {
get_solver()->user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh);
get_solver()->user_propagate_register_decide(p->decide_eh);
}
}
if (get_opt())
get_opt()->set_preferred(m_preferred.get());
m_preferred->set_preferred(fmla);
}
void cmd_context::reset_preferred() {
if (!m_scopes.empty())
throw default_exception("reset-preferred can only be invoked at base level");
if (m_preferred)
m_preferred->reset_preferred();
}
void cmd_context::display_model(model_ref& mdl) {
if (mdl) {
@ -2261,8 +2320,13 @@ void cmd_context::mk_solver() {
m_params.get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled);
m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic);
m_solver = mk_slice_solver(m_solver.get());
if (m_simplifier_factory)
if (m_simplifier_factory)
m_solver = mk_simplifier_solver(m_solver.get(), &m_simplifier_factory);
if (m_preferred) {
auto p = m_preferred.get();
m_solver->user_propagate_init(p, p->push_eh, p->pop_eh, p->fresh_eh);
m_solver->user_propagate_register_decide(p->decide_eh);
}
}

28
src/cmd_context/cmd_context.h
View file

@ -39,6 +39,7 @@ Notes:
#include "solver/check_logic.h"
#include "solver/progress_callback.h"
#include "solver/simplifier_solver.h"
#include "solver/preferred_value_propagator.h"
#include "cmd_context/pdecl.h"
#include "cmd_context/tactic_manager.h"
#include "params/context_params.h"
@ -163,6 +164,9 @@ struct builtin_decl {
};
class opt_wrapper : public check_sat_result {
protected:
preferred_value_propagator *m_preferred = nullptr;
public:
opt_wrapper(ast_manager& m): check_sat_result(m) {}
virtual bool empty() = 0;
@ -176,7 +180,7 @@ public:
virtual void get_box_model(model_ref& mdl, unsigned index) = 0;
virtual void updt_params(params_ref const& p) = 0;
virtual void initialize_value(expr* var, expr* value) = 0;
void set_preferred(preferred_value_propagator *p) { m_preferred = p; }
};
class ast_context_params : public context_params {
@ -265,6 +269,7 @@ protected:
dictionary<object_ref*> m_object_refs; // anything that can be named.
dictionary<sexpr*> m_user_tactic_decls;
vector<std::pair<expr_ref, expr_ref>> m_var2values;
scoped_ptr<preferred_value_propagator> m_preferred;
dictionary<func_decls> m_func_decls;
obj_map<func_decl, symbol> m_func_decl2alias;
@ -429,6 +434,8 @@ public:
void set_solver(solver* s) { m_solver = s; }
void set_proof_cmds(proof_cmds* pc) { m_proof_cmds = pc; }
void set_initial_value(expr* var, expr* value);
void set_preferred(expr *fmla);
void reset_preferred();
void set_solver_factory(solver_factory * s);
void set_simplifier_factory(simplifier_factory& sf) { m_simplifier_factory = sf; }
@ -575,22 +582,3 @@ public:
std::ostream & operator<<(std::ostream & out, cmd_context::status st);
class th_solver : public expr_solver {
cmd_context& m_ctx;
params_ref m_params;
ref<solver> m_solver;
public:
th_solver(cmd_context& ctx): m_ctx(ctx) {}
lbool check_sat(expr* e) override {
if (!m_solver) {
m_solver = m_ctx.get_solver_factory()(m_ctx.m(), m_params, false, true, false, symbol::null);
}
m_solver->push();
m_solver->assert_expr(e);
lbool r = m_solver->check_sat(0,nullptr);
m_solver->pop(1);
return r;
}
};

1
src/cmd_context/eval_cmd.cpp
View file

@ -75,7 +75,6 @@ public:
unsigned rlimit = m_params.get_uint("rlimit", 0);
// md->compress();
model_evaluator ev(*(md.get()), m_params);
ev.set_solver(alloc(th_solver, ctx));
cancel_eh<reslimit> eh(ctx.m().limit());
{
scoped_ctrl_c ctrlc(eh);

2
src/cmd_context/simplify_cmd.cpp
View file

@ -69,8 +69,6 @@ public:
if (m_params.get_bool("som", false))
m_params.set_bool("flat", true);
th_rewriter s(ctx.m(), m_params);
th_solver solver(ctx);
s.set_solver(alloc(th_solver, ctx));
unsigned cache_sz;
unsigned num_steps = 0;
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);

6
src/math/automata/CMakeLists.txt
View file

@ -1,6 +0,0 @@
z3_add_component(automata
SOURCES
automaton.cpp
COMPONENT_DEPENDENCIES
util
)

23
src/math/automata/automaton.cpp
View file

@ -1,23 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
automaton.cpp
Abstract:
Symbolic Automaton, a la Margus Veanes Automata library.
Author:
Nikolaj Bjorner (nbjorner) 2015-12-23.
Revision History:
--*/
#include "math/automata/automaton.h"
template class automaton<unsigned>;

Some files were not shown because too many files have changed in this diff Show more