mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

expose propagate created

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-17 16:12:47 -08:00
parent e1ffaa7faf
commit 8ca023d541
12 changed files with 67 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/api/api_solver.cpp
View file

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

15
src/api/z3_api.h
View file

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

2
src/ast/ast.h
View file

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

2
src/ast/recfun_decl_plugin.h
View file

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

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

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

4
src/smt/params/preprocessor_params.cpp
View file

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

6
src/smt/params/preprocessor_params.h
View file

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

8
src/smt/smt_setup.cpp
View file

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

14
src/solver/assertions/asserted_formulas.cpp
View file

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

6
src/solver/assertions/asserted_formulas.h
View file

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

8
src/util/zstring.cpp
View file

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

14
src/util/zstring.h
View file

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