diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index ea009b1bc..bb5ab9752 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -964,4 +964,23 @@ extern "C" {
Z3_CATCH;
}
+ void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh) {
+ Z3_TRY;
+ RESET_ERROR_CODE();
+ user_propagator::register_created_eh_t c = (void(*)(void*, user_propagator::callback*, expr*, unsigned))created_eh;
+ to_solver_ref(s)->user_propagate_register_created(c);
+ Z3_CATCH;
+ }
+
+ Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_solver s, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range) {
+ Z3_TRY;
+ LOG_Z3_solver_propagate_declare(c, s, name, n, domain, range);
+ RESET_ERROR_CODE();
+ func_decl* f = to_solver_ref(s)->user_propagate_declare(to_symbol(name), n, to_sorts(domain), to_sort(range));
+ mk_c(c)->save_ast_trail(f);
+ RETURN_Z3(of_func_decl(f));
+ Z3_CATCH_RETURN(nullptr);
+ }
+
+
};
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 767eebc43..899a5e7d1 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -1430,6 +1430,7 @@ typedef void* Z3_fresh_eh(void* ctx, Z3_context new_context);
typedef void Z3_fixed_eh(void* ctx, Z3_solver_callback cb, unsigned id, Z3_ast value);
typedef void Z3_eq_eh(void* ctx, Z3_solver_callback cb, unsigned x, unsigned y);
typedef void Z3_final_eh(void* ctx, Z3_solver_callback cb);
+typedef void Z3_created_eh(void* ctx, Z3_solver_callback cb, Z3_ast e, unsigned id);
/**
@@ -6676,6 +6677,20 @@ extern "C" {
*/
void Z3_API Z3_solver_propagate_diseq(Z3_context c, Z3_solver s, Z3_eq_eh eq_eh);
+ /**
+ * \brief register a callback when a new expression with a registered function is used by the solver
+ * The registered function appears at the top level and is created using \c Z3_solver_declare.
+ */
+ void Z3_API Z3_solver_propagate_created(Z3_context c, Z3_solver s, Z3_created_eh created_eh);
+
+ /**
+ \brief Create a registered function. Expressions used by the solver \c s that uses the registered function
+ at top level cause the callback propagate_created to be invoked.
+
+ def_API('Z3_solver_propagate_declare', FUNC_DECL, (_in(CONTEXT), _in(SOLVER), _in(SYMBOL), _in(UINT), _in_array(3, SORT), _in(SORT)))
+ */
+ Z3_func_decl Z3_API Z3_solver_propagate_declare(Z3_context c, Z3_solver s, Z3_symbol name, unsigned n, Z3_sort* domain, Z3_sort range);
+
/**
\brief register an expression to propagate on with the solver.
Only expressions of type Bool and type Bit-Vector can be registered for propagation.
diff --git a/src/ast/ast.h b/src/ast/ast.h
index b04e67003..13898c2a6 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -845,7 +845,7 @@ class quantifier : public expr {
char m_patterns_decls[0];
static unsigned get_obj_size(unsigned num_decls, unsigned num_patterns, unsigned num_no_patterns) {
- return sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*);
+ return (unsigned)(sizeof(quantifier) + num_decls * (sizeof(sort *) + sizeof(symbol)) + (num_patterns + num_no_patterns) * sizeof(expr*));
}
quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, sort* s,
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 1146b7aaf..dd07e8baf 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -305,7 +305,7 @@ namespace recfun {
m_pred(pred), m_cdef(&d), m_args(args) {}
body_expansion(body_expansion const & from):
m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {}
- body_expansion(body_expansion && from) :
+ body_expansion(body_expansion && from) noexcept :
m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {}
std::ostream& display(std::ostream& out) const;
diff --git a/src/ast/rewriter/maximize_ac_sharing.h b/src/ast/rewriter/maximize_ac_sharing.h
index 53e102b74..a2741aa89 100644
--- a/src/ast/rewriter/maximize_ac_sharing.h
+++ b/src/ast/rewriter/maximize_ac_sharing.h
@@ -46,7 +46,7 @@ class maximize_ac_sharing : public default_rewriter_cfg {
entry(func_decl * d = nullptr, expr * arg1 = nullptr, expr * arg2 = nullptr):m_decl(d), m_arg1(arg1), m_arg2(arg2) {
SASSERT((d == 0 && arg1 == 0 && arg2 == 0) || (d != 0 && arg1 != 0 && arg2 != 0));
- if (arg1->get_id() > arg2->get_id())
+ if (arg1 && arg2 && arg1->get_id() > arg2->get_id())
std::swap(m_arg1, m_arg2);
}
diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp
index a87d4959d..9fcb09843 100644
--- a/src/smt/params/preprocessor_params.cpp
+++ b/src/smt/params/preprocessor_params.cpp
@@ -40,8 +40,8 @@ void preprocessor_params::display(std::ostream & out) const {
pattern_inference_params::display(out);
bit_blaster_params::display(out);
- DISPLAY_PARAM(m_lift_ite);
- DISPLAY_PARAM(m_ng_lift_ite);
+ DISPLAY_PARAM((int)m_lift_ite);
+ DISPLAY_PARAM((int)m_ng_lift_ite);
DISPLAY_PARAM(m_pull_cheap_ite);
DISPLAY_PARAM(m_pull_nested_quantifiers);
DISPLAY_PARAM(m_eliminate_term_ite);
diff --git a/src/smt/params/preprocessor_params.h b/src/smt/params/preprocessor_params.h
index a0d56182a..53568c366 100644
--- a/src/smt/params/preprocessor_params.h
+++ b/src/smt/params/preprocessor_params.h
@@ -21,7 +21,7 @@ Revision History:
#include "params/pattern_inference_params.h"
#include "params/bit_blaster_params.h"
-enum lift_ite_kind {
+enum class lift_ite_kind {
LI_NONE,
LI_CONSERVATIVE,
LI_FULL
@@ -50,8 +50,8 @@ struct preprocessor_params : public pattern_inference_params,
public:
preprocessor_params(params_ref const & p = params_ref()):
- m_lift_ite(LI_NONE),
- m_ng_lift_ite(LI_NONE),
+ m_lift_ite(lift_ite_kind::LI_NONE),
+ m_ng_lift_ite(lift_ite_kind::LI_NONE),
m_pull_cheap_ite(false),
m_pull_nested_quantifiers(false),
m_eliminate_term_ite(false),
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index ba601272d..2d131c6ab 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -643,8 +643,8 @@ namespace smt {
// It destroys the existing patterns.
// m_params.m_macro_finder = true;
- if (m_params.m_ng_lift_ite == LI_NONE)
- m_params.m_ng_lift_ite = LI_CONSERVATIVE;
+ if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE)
+ m_params.m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE;
TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";);
m_context.register_plugin(alloc(smt::theory_i_arith, m_context));
setup_arrays();
@@ -668,8 +668,8 @@ namespace smt {
m_params.m_qi_lazy_threshold = 20;
//
m_params.m_macro_finder = true;
- if (m_params.m_ng_lift_ite == LI_NONE)
- m_params.m_ng_lift_ite = LI_CONSERVATIVE;
+ if (m_params.m_ng_lift_ite == lift_ite_kind::LI_NONE)
+ m_params.m_ng_lift_ite = lift_ite_kind::LI_CONSERVATIVE;
m_params.m_pi_max_multi_patterns = 10; //<< it was used for SMT-COMP
m_params.m_array_lazy_ieq = true;
m_params.m_array_lazy_ieq_delay = 4;
diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp
index b3be7e8ab..1b8bfe9dd 100644
--- a/src/solver/assertions/asserted_formulas.cpp
+++ b/src/solver/assertions/asserted_formulas.cpp
@@ -71,12 +71,12 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & sp, params_re
void asserted_formulas::setup() {
switch (m_smt_params.m_lift_ite) {
- case LI_FULL:
- m_smt_params.m_ng_lift_ite = LI_NONE;
+ case lift_ite_kind::LI_FULL:
+ m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE;
break;
- case LI_CONSERVATIVE:
- if (m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE)
- m_smt_params.m_ng_lift_ite = LI_NONE;
+ case lift_ite_kind::LI_CONSERVATIVE:
+ if (m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE)
+ m_smt_params.m_ng_lift_ite = lift_ite_kind::LI_NONE;
break;
default:
break;
@@ -281,8 +281,8 @@ void asserted_formulas::reduce() {
if (!invoke(m_reduce_asserted_formulas)) return;
if (!invoke(m_pull_nested_quantifiers)) return;
if (!invoke(m_lift_ite)) return;
- m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == LI_CONSERVATIVE);
- m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == LI_CONSERVATIVE);
+ m_lift_ite.m_functor.set_conservative(m_smt_params.m_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
+ m_ng_lift_ite.m_functor.set_conservative(m_smt_params.m_ng_lift_ite == lift_ite_kind::LI_CONSERVATIVE);
if (!invoke(m_ng_lift_ite)) return;
if (!invoke(m_elim_term_ite)) return;
if (!invoke(m_refine_inj_axiom)) return;
diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h
index 95848133c..23a4f5a0a 100644
--- a/src/solver/assertions/asserted_formulas.h
+++ b/src/solver/assertions/asserted_formulas.h
@@ -154,7 +154,7 @@ class asserted_formulas {
public:
elim_term_ite_fn(asserted_formulas& af): simplify_fmls(af, "elim-term-ite"), m_elim(af.m, af.m_defined_names) {}
void simplify(justified_expr const& j, expr_ref& n, proof_ref& p) override { m_elim(j.get_fml(), n, p); }
- bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != LI_FULL; }
+ bool should_apply() const override { return af.m_smt_params.m_eliminate_term_ite && af.m_smt_params.m_lift_ite != lift_ite_kind::LI_FULL; }
void post_op() override { af.m_formulas.append(m_elim.new_defs()); af.reduce_and_solve(); m_elim.reset(); }
void push() { m_elim.push(); }
void pop(unsigned n) { m_elim.pop(n); }
@@ -187,8 +187,8 @@ class asserted_formulas {
MK_SIMPLIFIERF(cheap_quant_fourier_motzkin, elim_bounds_rw, "cheap-fourier-motzkin", af.m_smt_params.m_eliminate_bounds && af.has_quantifiers(), true);
MK_SIMPLIFIERF(elim_bvs_from_quantifiers, bv_elim_rw, "eliminate-bit-vectors-from-quantifiers", af.m_smt_params.m_bb_quantifiers, true);
MK_SIMPLIFIERF(apply_bit2int, bit2int, "propagate-bit-vector-over-integers", af.m_smt_params.m_simplify_bit2int, true);
- MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != LI_NONE, true);
- MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != LI_NONE, true);
+ MK_SIMPLIFIERF(lift_ite, push_app_ite_rw, "lift-ite", af.m_smt_params.m_lift_ite != lift_ite_kind::LI_NONE, true);
+ MK_SIMPLIFIERF(ng_lift_ite, ng_push_app_ite_rw, "lift-ite", af.m_smt_params.m_ng_lift_ite != lift_ite_kind::LI_NONE, true);
reduce_asserted_formulas_fn m_reduce_asserted_formulas;
diff --git a/src/util/zstring.cpp b/src/util/zstring.cpp
index 534999606..e73c4cd52 100644
--- a/src/util/zstring.cpp
+++ b/src/util/zstring.cpp
@@ -87,12 +87,12 @@ zstring::zstring(char const* s) {
string_encoding zstring::get_encoding() {
if (gparams::get_value("encoding") == "unicode")
- return unicode;
+ return string_encoding::unicode;
if (gparams::get_value("encoding") == "bmp")
- return bmp;
+ return string_encoding::bmp;
if (gparams::get_value("encoding") == "ascii")
- return ascii;
- return unicode;
+ return string_encoding::ascii;
+ return string_encoding::unicode;
}
bool zstring::well_formed() const {
diff --git a/src/util/zstring.h b/src/util/zstring.h
index c5606b267..cb462238a 100644
--- a/src/util/zstring.h
+++ b/src/util/zstring.h
@@ -21,7 +21,7 @@ Author:
#include "util/buffer.h"
#include "util/rational.h"
-enum string_encoding {
+enum class string_encoding {
ascii, // exactly 8 bits
unicode,
bmp // basic multilingual plane; exactly 16 bits
@@ -41,22 +41,22 @@ public:
static unsigned ascii_num_bits() { return 8; }
static unsigned max_char() {
switch (get_encoding()) {
- case unicode:
+ case string_encoding::unicode:
return unicode_max_char();
- case bmp:
+ case string_encoding::bmp:
return bmp_max_char();
- case ascii:
+ case string_encoding::ascii:
return ascii_max_char();
}
return unicode_max_char();
}
static unsigned num_bits() {
switch (get_encoding()) {
- case unicode:
+ case string_encoding::unicode:
return unicode_num_bits();
- case bmp:
+ case string_encoding::bmp:
return bmp_num_bits();
- case ascii:
+ case string_encoding::ascii:
return ascii_num_bits();
}
return unicode_num_bits();