mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
user propagator
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
5e5ef50dbc
commit
96f10b8c1c
|
|
@ -1843,7 +1843,7 @@ _lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
|
|||
|
||||
push_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p)
|
||||
pop_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
|
||||
fresh_eh_type = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p)
|
||||
fresh_eh_type = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
|
||||
|
||||
fixed_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint, ctypes.c_void_p)
|
||||
final_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
|
||||
|
|
|
|||
|
|
@ -116,6 +116,8 @@ namespace api {
|
|||
DEBUG_CODE(warning_msg("Uncollected memory: %d: %s", kv.m_key, typeid(*val).name()););
|
||||
dealloc(val);
|
||||
}
|
||||
if (m_params.owns_manager())
|
||||
m_manager.detach();
|
||||
}
|
||||
|
||||
context::set_interruptable::set_interruptable(context & ctx, event_handler & i):
|
||||
|
|
|
|||
|
|
@ -896,9 +896,15 @@ extern "C" {
|
|||
Z3_TRY;
|
||||
RESET_ERROR_CODE();
|
||||
init_solver(c, s);
|
||||
std::function<void(void*)> _push = push_eh;
|
||||
std::function<void(void*,unsigned)> _pop = pop_eh;
|
||||
std::function<void*(void*)> _fresh = fresh_eh;
|
||||
solver::push_eh_t _push = push_eh;
|
||||
solver::pop_eh_t _pop = pop_eh;
|
||||
solver::fresh_eh_t _fresh = [&](void * user_ctx, ast_manager& m, void*& _ctx) {
|
||||
context_params params;
|
||||
params.set_foreign_manager(&m);
|
||||
auto* ctx = reinterpret_cast<Z3_context>(alloc(api::context, ¶ms, false));
|
||||
_ctx = ctx;
|
||||
return fresh_eh(user_ctx, ctx);
|
||||
};
|
||||
to_solver_ref(s)->user_propagate_init(user_context, _push, _pop, _fresh);
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
|
@ -955,11 +961,11 @@ extern "C" {
|
|||
Z3_CATCH_RETURN(0);
|
||||
}
|
||||
|
||||
void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback s, unsigned sz, unsigned const* ids, Z3_ast conseq) {
|
||||
void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback s, unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, Z3_ast conseq) {
|
||||
Z3_TRY;
|
||||
LOG_Z3_solver_propagate_consequence(c, s, sz, ids, conseq);
|
||||
LOG_Z3_solver_propagate_consequence(c, s, num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, conseq);
|
||||
RESET_ERROR_CODE();
|
||||
reinterpret_cast<solver::propagate_callback*>(s)->propagate(sz, ids, to_expr(conseq));
|
||||
reinterpret_cast<solver::propagate_callback*>(s)->propagate(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, to_expr(conseq));
|
||||
Z3_CATCH;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -10506,30 +10506,39 @@ def TransitiveClosure(f):
|
|||
|
||||
|
||||
class PropClosures:
|
||||
# import thread
|
||||
def __init__(self):
|
||||
self.bases = {}
|
||||
# self.lock = thread.Lock()
|
||||
self.lock = None
|
||||
|
||||
def set_threaded():
|
||||
if self.lock is None:
|
||||
import threading
|
||||
self.lock = threading.thread.Lock()
|
||||
|
||||
def get(self, ctx):
|
||||
# self.lock.acquire()
|
||||
if self.lock: self.lock.acquire()
|
||||
r = self.bases[ctx]
|
||||
# self.lock.release()
|
||||
if self.lock: self.lock.release()
|
||||
return r
|
||||
|
||||
def set(self, ctx, r):
|
||||
# self.lock.acquire()
|
||||
if self.lock: self.lock.acquire()
|
||||
self.bases[ctx] = r
|
||||
# self.lock.release()
|
||||
if self.lock: self.lock.release()
|
||||
|
||||
def insert(self, r):
|
||||
# self.lock.acquire()
|
||||
if self.lock: self.lock.acquire()
|
||||
id = len(self.bases) + 3
|
||||
self.bases[id] = r
|
||||
# self.lock.release()
|
||||
if self.lock: self.lock.release()
|
||||
return id
|
||||
|
||||
_prop_closures = PropClosures()
|
||||
_prop_closures = None
|
||||
|
||||
def ensure_prop_closures():
|
||||
global _prop_closures
|
||||
if _prop_closures is None:
|
||||
_prop_closures = PropClosures()
|
||||
|
||||
def user_prop_push(ctx):
|
||||
_prop_closures.get(ctx).push();
|
||||
|
|
@ -10537,9 +10546,10 @@ def user_prop_push(ctx):
|
|||
def user_prop_pop(ctx, num_scopes):
|
||||
_prop_closures.get(ctx).pop(num_scopes)
|
||||
|
||||
def user_prop_fresh(ctx):
|
||||
prop = _prop_closures.get(ctx)
|
||||
new_prop = UsePropagateBase(None, prop.ctx)
|
||||
def user_prop_fresh(id, ctx):
|
||||
prop = _prop_closures.get(id)
|
||||
_prop_closures.set_threaded()
|
||||
new_prop = UsePropagateBase(None, ctx)
|
||||
_prop_closures.set(new_prop.id, new_prop.fresh())
|
||||
return ctypes.c_void_p(new_prop.id)
|
||||
|
||||
|
|
@ -10577,66 +10587,104 @@ _user_prop_diseq = eq_eh_type(user_prop_diseq)
|
|||
|
||||
class UserPropagateBase:
|
||||
|
||||
#
|
||||
# Either solver is set or ctx is set.
|
||||
# Propagators that are created throuh callbacks
|
||||
# to "fresh" inherit the context of that is supplied
|
||||
# as argument to the callback.
|
||||
# This context should not be deleted. It is owned by the solver.
|
||||
#
|
||||
def __init__(self, s, ctx = None):
|
||||
assert s is None or ctx is None
|
||||
ensure_prop_closures()
|
||||
self.solver = s
|
||||
self.ctx = s.ctx if s is not None else ctx
|
||||
self._ctx = None
|
||||
self.cb = None
|
||||
self.id = _prop_closures.insert(self)
|
||||
self.fixed = None
|
||||
self.final = None
|
||||
self.eq = None
|
||||
self.diseq = None
|
||||
if ctx:
|
||||
self._ctx = Context()
|
||||
Z3_del_context(self._ctx.ctx)
|
||||
self._ctx.ctx = ctx
|
||||
self._ctx.eh = Z3_set_error_handler(ctx, z3_error_handler)
|
||||
Z3_set_ast_print_mode(ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
|
||||
if s:
|
||||
Z3_solver_propagate_init(s.ctx.ref(),
|
||||
Z3_solver_propagate_init(self.ctx_ref(),
|
||||
s.solver,
|
||||
ctypes.c_void_p(self.id),
|
||||
_user_prop_push,
|
||||
_user_prop_pop,
|
||||
_user_prop_fresh)
|
||||
|
||||
|
||||
def __del__(self):
|
||||
if self._ctx:
|
||||
self._ctx.ctx = None
|
||||
|
||||
def ctx(self):
|
||||
if self._ctx:
|
||||
return self._ctx
|
||||
else:
|
||||
return self.solver.ctx
|
||||
|
||||
def ctx_ref(self):
|
||||
return self.ctx().ref()
|
||||
|
||||
def add_fixed(self, fixed):
|
||||
assert not self.fixed
|
||||
Z3_solver_propagate_fixed(self.ctx.ref(), self.solver.solver, _user_prop_fixed)
|
||||
assert not self._ctx
|
||||
Z3_solver_propagate_fixed(self.ctx_ref(), self.solver.solver, _user_prop_fixed)
|
||||
self.fixed = fixed
|
||||
|
||||
def add_final(self, final):
|
||||
assert not self.final
|
||||
Z3_solver_propagate_final(self.ctx.ref(), self.solver.solver, _user_prop_final)
|
||||
assert not self._ctx
|
||||
Z3_solver_propagate_final(self.ctx_ref(), self.solver.solver, _user_prop_final)
|
||||
self.final = final
|
||||
|
||||
def add_eq(self, eq):
|
||||
assert not self.eq
|
||||
Z3_solver_propagate_eq(self.ctx.ref(), self.solver.solver, _user_prop_eq)
|
||||
assert not self._ctx
|
||||
Z3_solver_propagate_eq(self.ctx_ref(), self.solver.solver, _user_prop_eq)
|
||||
self.eq = eq
|
||||
|
||||
def add_diseq(self, diseq):
|
||||
assert not self.diseq
|
||||
Z3_solver_propagate_diseq(self.ctx.ref(), self.solver.solver, _user_prop_diseq)
|
||||
assert not self._ctx
|
||||
Z3_solver_propagate_diseq(self.ctx_ref(), self.solver.solver, _user_prop_diseq)
|
||||
self.diseq = diseq
|
||||
|
||||
def push(self):
|
||||
raise Z3Exception("push has not been overwritten")
|
||||
raise Z3Exception("push needs to be overwritten")
|
||||
|
||||
def pop(self, num_scopes):
|
||||
raise Z3Exception("pop has not been overwritten")
|
||||
raise Z3Exception("pop needs to be overwritten")
|
||||
|
||||
def fresh(self):
|
||||
raise Z3Exception("fresh has not been overwritten")
|
||||
raise Z3Exception("fresh needs to be overwritten")
|
||||
|
||||
def add(self, e):
|
||||
assert self.solver
|
||||
return Z3_solver_propagate_register(self.ctx.ref(), self.solver.solver, e.ast)
|
||||
assert not self._ctx
|
||||
return Z3_solver_propagate_register(self.ctx_ref(), self.solver.solver, e.ast)
|
||||
|
||||
#
|
||||
# Propagation can only be invoked as during a fixed-callback.
|
||||
#
|
||||
def propagate(self, ids, e):
|
||||
sz = len(ids)
|
||||
_ids = (ctypes.c_uint * sz)()
|
||||
for i in range(sz):
|
||||
def propagate(self, e, ids, eqs = []):
|
||||
num_fixed = len(ids)
|
||||
_ids = (ctypes.c_uint * num_fixed)()
|
||||
for i in range(num_fixed):
|
||||
_ids[i] = ids[i]
|
||||
Z3_solver_propagate_consequence(self.ctx.ref(), ctypes.c_void_p(self.cb), sz, _ids, e.ast)
|
||||
num_eqs = len(eqs)
|
||||
_lhs = (ctypes.c_uint * num_eqs)()
|
||||
_rhs = (ctypes.c_uint * num_eqs)()
|
||||
for i in range(num_eqs):
|
||||
_lhs[i] = eqs[i][0]
|
||||
_rhs[i] = eqs[i][1]
|
||||
Z3_solver_propagate_consequence(self.ctx_ref(), ctypes.c_void_p(self.cb), num_fixed, _ids, num_eqs, _lhs, _rhs, e.ast)
|
||||
|
||||
def conflict(self, ids):
|
||||
self.propagate(ids, BoolVal(False, self.ctx))
|
||||
self.propagate(ids, BoolVal(False, self.ctx_ref()))
|
||||
|
|
|
|||
|
|
@ -1420,7 +1420,7 @@ typedef void Z3_error_handler(Z3_context c, Z3_error_code e);
|
|||
*/
|
||||
typedef void Z3_push_eh(void* ctx);
|
||||
typedef void Z3_pop_eh(void* ctx, unsigned num_scopes);
|
||||
typedef void* Z3_fresh_eh(void* ctx);
|
||||
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);
|
||||
|
|
@ -6586,10 +6586,10 @@ extern "C" {
|
|||
The callback adds a propagation consequence based on the fixed values of the
|
||||
\c ids.
|
||||
|
||||
def_API('Z3_solver_propagate_consequence', VOID, (_in(CONTEXT), _in(SOLVER_CALLBACK), _in(UINT), _in_array(2, UINT), _in(AST)))
|
||||
def_API('Z3_solver_propagate_consequence', VOID, (_in(CONTEXT), _in(SOLVER_CALLBACK), _in(UINT), _in_array(2, UINT), _in(UINT), _in_array(4, UINT), _in_array(4, UINT), _in(AST)))
|
||||
*/
|
||||
|
||||
void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback, unsigned sz, unsigned const* ids, Z3_ast conseq);
|
||||
void Z3_API Z3_solver_propagate_consequence(Z3_context c, Z3_solver_callback, unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, Z3_ast conseq);
|
||||
|
||||
/**
|
||||
\brief Check whether the assertions in a given solver are consistent or not.
|
||||
|
|
|
|||
|
|
@ -24,19 +24,6 @@ Notes:
|
|||
#include "solver/solver.h"
|
||||
|
||||
context_params::context_params() {
|
||||
m_unsat_core = false;
|
||||
m_model = true;
|
||||
m_model_validate = false;
|
||||
m_dump_models = false;
|
||||
m_auto_config = true;
|
||||
m_proof = false;
|
||||
m_trace = false;
|
||||
m_debug_ref_count = false;
|
||||
m_smtlib2_compliant = false;
|
||||
m_well_sorted_check = false;
|
||||
m_timeout = UINT_MAX;
|
||||
m_rlimit = 0;
|
||||
m_statistics = false;
|
||||
updt_params();
|
||||
}
|
||||
|
||||
|
|
@ -204,6 +191,8 @@ void context_params::get_solver_params(ast_manager const & m, params_ref & p, bo
|
|||
}
|
||||
|
||||
ast_manager * context_params::mk_ast_manager() {
|
||||
if (m_manager)
|
||||
return m_manager;
|
||||
ast_manager * r = alloc(ast_manager,
|
||||
m_proof ? PGM_ENABLED : PGM_DISABLED,
|
||||
m_trace ? m_trace_file_name.c_str() : nullptr);
|
||||
|
|
|
|||
|
|
@ -26,24 +26,24 @@ class context_params {
|
|||
void set_bool(bool & opt, char const * param, char const * value);
|
||||
void set_uint(unsigned & opt, char const * param, char const * value);
|
||||
|
||||
unsigned m_rlimit;
|
||||
unsigned m_rlimit { 0 };
|
||||
ast_manager* m_manager { nullptr };
|
||||
|
||||
public:
|
||||
bool m_auto_config;
|
||||
bool m_proof;
|
||||
bool m_auto_config { true };
|
||||
bool m_proof { false };
|
||||
std::string m_dot_proof_file;
|
||||
bool m_interpolants;
|
||||
bool m_debug_ref_count;
|
||||
bool m_trace;
|
||||
bool m_debug_ref_count { false };
|
||||
bool m_trace { false };
|
||||
std::string m_trace_file_name;
|
||||
bool m_well_sorted_check;
|
||||
bool m_model;
|
||||
bool m_model_validate;
|
||||
bool m_dump_models;
|
||||
bool m_unsat_core;
|
||||
bool m_smtlib2_compliant; // it must be here because it enable/disable the use of coercions in the ast_manager.
|
||||
unsigned m_timeout;
|
||||
bool m_statistics;
|
||||
bool m_well_sorted_check { false };
|
||||
bool m_model { true };
|
||||
bool m_model_validate { false };
|
||||
bool m_dump_models { false };
|
||||
bool m_unsat_core { false };
|
||||
bool m_smtlib2_compliant { false }; // it must be here because it enable/disable the use of coercions in the ast_manager.
|
||||
unsigned m_timeout { UINT_MAX } ;
|
||||
bool m_statistics { false };
|
||||
|
||||
unsigned rlimit() const { return m_rlimit; }
|
||||
context_params();
|
||||
|
|
@ -74,6 +74,9 @@ public:
|
|||
\brief Create an AST manager using this configuration.
|
||||
*/
|
||||
ast_manager * mk_ast_manager();
|
||||
|
||||
void set_foreign_manager(ast_manager* m) { m_manager = m; }
|
||||
bool owns_manager() const { return m_manager != nullptr; }
|
||||
};
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -183,13 +183,14 @@ namespace smt {
|
|||
|
||||
dst_ctx.setup_context(dst_ctx.m_fparams.m_auto_config);
|
||||
dst_ctx.internalize_assertions();
|
||||
|
||||
dst_ctx.copy_user_propagator(src_ctx);
|
||||
|
||||
TRACE("smt_context",
|
||||
src_ctx.display(tout);
|
||||
dst_ctx.display(tout););
|
||||
}
|
||||
|
||||
|
||||
context::~context() {
|
||||
flush();
|
||||
m_asserted_formulas.finalize();
|
||||
|
|
@ -205,6 +206,19 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
void context::copy_user_propagator(context& src_ctx) {
|
||||
if (!src_ctx.m_user_propagator)
|
||||
return;
|
||||
ast_translation tr(src_ctx.m, m, false);
|
||||
auto* p = get_theory(m.mk_family_id("user_propagator"));
|
||||
m_user_propagator = reinterpret_cast<user_propagator*>(p);
|
||||
SASSERT(m_user_propagator);
|
||||
for (unsigned i = 0; i < src_ctx.m_user_propagator->get_num_vars(); ++i) {
|
||||
app* e = src_ctx.m_user_propagator->get_expr(i);
|
||||
m_user_propagator->add_expr(tr(e));
|
||||
}
|
||||
}
|
||||
|
||||
context * context::mk_fresh(symbol const * l, smt_params * p, params_ref const& pa) {
|
||||
context * new_ctx = alloc(context, m, p ? *p : m_fparams, pa);
|
||||
new_ctx->m_is_auxiliary = true;
|
||||
|
|
@ -2950,10 +2964,10 @@ namespace smt {
|
|||
}
|
||||
|
||||
void context::user_propagate_init(
|
||||
void* ctx,
|
||||
std::function<void(void*)>& push_eh,
|
||||
std::function<void(void*, unsigned)>& pop_eh,
|
||||
std::function<void*(void*)>& fresh_eh) {
|
||||
void* ctx,
|
||||
solver::push_eh_t& push_eh,
|
||||
solver::pop_eh_t& pop_eh,
|
||||
solver::fresh_eh_t& fresh_eh) {
|
||||
setup_context(m_fparams.m_auto_config);
|
||||
m_user_propagator = alloc(user_propagator, *this);
|
||||
m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
|
||||
|
|
@ -2963,7 +2977,7 @@ namespace smt {
|
|||
}
|
||||
|
||||
bool context::watches_fixed(enode* n) const {
|
||||
return m_user_propagator && n->get_th_var(m_user_propagator->get_family_id()) != null_theory_var;
|
||||
return m_user_propagator && m_user_propagator->has_fixed() && n->get_th_var(m_user_propagator->get_family_id()) != null_theory_var;
|
||||
}
|
||||
|
||||
void context::assign_fixed(enode* n, expr* val, unsigned sz, literal const* explain) {
|
||||
|
|
|
|||
|
|
@ -1573,6 +1573,8 @@ namespace smt {
|
|||
|
||||
void log_stats();
|
||||
|
||||
void copy_user_propagator(context& src);
|
||||
|
||||
public:
|
||||
context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref());
|
||||
|
||||
|
|
@ -1688,10 +1690,10 @@ namespace smt {
|
|||
* user-propagator
|
||||
*/
|
||||
void user_propagate_init(
|
||||
void* ctx,
|
||||
std::function<void(void*)>& push_eh,
|
||||
std::function<void(void*, unsigned)>& pop_eh,
|
||||
std::function<void*(void*)>& fresh_eh);
|
||||
void* ctx,
|
||||
solver::push_eh_t& push_eh,
|
||||
solver::pop_eh_t& pop_eh,
|
||||
solver::fresh_eh_t& fresh_eh);
|
||||
|
||||
void user_propagate_register_final(solver::final_eh_t& final_eh) {
|
||||
if (!m_user_propagator)
|
||||
|
|
|
|||
|
|
@ -234,10 +234,10 @@ namespace smt {
|
|||
}
|
||||
|
||||
void user_propagate_init(
|
||||
void* ctx,
|
||||
std::function<void(void*)>& push_eh,
|
||||
std::function<void(void*, unsigned)>& pop_eh,
|
||||
std::function<void*(void*)>& fresh_eh) {
|
||||
void* ctx,
|
||||
solver::push_eh_t& push_eh,
|
||||
solver::pop_eh_t& pop_eh,
|
||||
solver::fresh_eh_t& fresh_eh) {
|
||||
m_kernel.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
|
||||
}
|
||||
|
||||
|
|
@ -474,10 +474,10 @@ namespace smt {
|
|||
}
|
||||
|
||||
void kernel::user_propagate_init(
|
||||
void* ctx,
|
||||
std::function<void(void*)>& push_eh,
|
||||
std::function<void(void*, unsigned)>& pop_eh,
|
||||
std::function<void*(void*)>& fresh_eh) {
|
||||
void* ctx,
|
||||
solver::push_eh_t& push_eh,
|
||||
solver::pop_eh_t& pop_eh,
|
||||
solver::fresh_eh_t& fresh_eh) {
|
||||
m_imp->user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -290,9 +290,9 @@ namespace smt {
|
|||
*/
|
||||
void user_propagate_init(
|
||||
void* ctx,
|
||||
std::function<void(void*)>& push_eh,
|
||||
std::function<void(void*, unsigned)>& pop_eh,
|
||||
std::function<void*(void*)>& fresh_eh);
|
||||
solver::push_eh_t& push_eh,
|
||||
solver::pop_eh_t& pop_eh,
|
||||
solver::fresh_eh_t& fresh_eh);
|
||||
|
||||
void user_propagate_register_fixed(solver::fixed_eh_t& fixed_eh);
|
||||
|
||||
|
|
|
|||
|
|
@ -212,7 +212,7 @@ namespace {
|
|||
void* ctx,
|
||||
std::function<void(void*)>& push_eh,
|
||||
std::function<void(void*, unsigned)>& pop_eh,
|
||||
std::function<void*(void*)>& fresh_eh) override {
|
||||
solver::fresh_eh_t& fresh_eh) override {
|
||||
m_context.user_propagate_init(ctx, push_eh, pop_eh, fresh_eh);
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -23,11 +23,13 @@ Author:
|
|||
using namespace smt;
|
||||
|
||||
user_propagator::user_propagator(context& ctx):
|
||||
theory(ctx, ctx.get_manager().mk_family_id("user_propagator")),
|
||||
m_qhead(0),
|
||||
m_num_scopes(0)
|
||||
theory(ctx, ctx.get_manager().mk_family_id("user_propagator"))
|
||||
{}
|
||||
|
||||
user_propagator::~user_propagator() {
|
||||
dealloc(m_api_context);
|
||||
}
|
||||
|
||||
void user_propagator::force_push() {
|
||||
for (; m_num_scopes > 0; --m_num_scopes) {
|
||||
theory::push_scope_eh();
|
||||
|
|
@ -36,9 +38,6 @@ void user_propagator::force_push() {
|
|||
}
|
||||
}
|
||||
|
||||
// TODO: check type of 'e', either Bool or Bit-vector.
|
||||
//
|
||||
|
||||
unsigned user_propagator::add_expr(expr* e) {
|
||||
force_push();
|
||||
enode* n = ensure_enode(e);
|
||||
|
|
@ -49,13 +48,13 @@ unsigned user_propagator::add_expr(expr* e) {
|
|||
return v;
|
||||
}
|
||||
|
||||
void user_propagator::propagate(unsigned sz, unsigned const* ids, expr* conseq) {
|
||||
m_prop.push_back(prop_info(sz, ids, expr_ref(conseq, m)));
|
||||
void user_propagator::propagate(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) {
|
||||
m_prop.push_back(prop_info(num_fixed, fixed_ids, num_eqs, eq_lhs, eq_rhs, expr_ref(conseq, m)));
|
||||
}
|
||||
|
||||
theory * user_propagator::mk_fresh(context * new_ctx) {
|
||||
auto* th = alloc(user_propagator, *new_ctx);
|
||||
void* ctx = m_fresh_eh(m_user_context);
|
||||
void* ctx = m_fresh_eh(m_user_context, new_ctx->get_manager(), th->m_api_context);
|
||||
th->add(ctx, m_push_eh, m_pop_eh, m_fresh_eh);
|
||||
if ((bool)m_fixed_eh) th->register_fixed(m_fixed_eh);
|
||||
if ((bool)m_final_eh) th->register_final(m_final_eh);
|
||||
|
|
@ -110,9 +109,12 @@ void user_propagator::propagate() {
|
|||
justification* js;
|
||||
while (qhead < m_prop.size() && !ctx.inconsistent()) {
|
||||
auto const& prop = m_prop[qhead];
|
||||
m_lits.reset();
|
||||
m_lits.reset();
|
||||
eqs.reset();
|
||||
for (unsigned id : prop.m_ids)
|
||||
m_lits.append(m_id2justification[id]);
|
||||
for (auto const& p : prop.m_eqs)
|
||||
eqs.push_back(enode_pair(get_enode(p.first), get_enode(p.second)));
|
||||
if (m.is_false(prop.m_conseq)) {
|
||||
js = ctx.mk_justification(
|
||||
ext_theory_conflict_justification(
|
||||
|
|
@ -126,10 +128,16 @@ void user_propagator::propagate() {
|
|||
get_id(), ctx.get_region(), m_lits.size(), m_lits.c_ptr(), eqs.size(), eqs.c_ptr(), lit));
|
||||
ctx.assign(lit, js);
|
||||
}
|
||||
++m_stats.m_num_propagations;
|
||||
++qhead;
|
||||
}
|
||||
ctx.push_trail(value_trail<context, unsigned>(m_qhead));
|
||||
m_qhead = qhead;
|
||||
}
|
||||
|
||||
void user_propagator::collect_statistics(::statistics & st) const {
|
||||
st.update("user-propagations", m_stats.m_num_propagations);
|
||||
st.update("user-watched", get_num_vars());
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -29,45 +29,59 @@ Notes:
|
|||
|
||||
namespace smt {
|
||||
class user_propagator : public theory, public solver::propagate_callback {
|
||||
void* m_user_context;
|
||||
std::function<void(void*)> m_push_eh;
|
||||
std::function<void(void*, unsigned)> m_pop_eh;
|
||||
std::function<void*(void*)> m_fresh_eh;
|
||||
solver::final_eh_t m_final_eh;
|
||||
solver::fixed_eh_t m_fixed_eh;
|
||||
solver::eq_eh_t m_eq_eh;
|
||||
solver::eq_eh_t m_diseq_eh;
|
||||
|
||||
struct prop_info {
|
||||
unsigned_vector m_ids;
|
||||
expr_ref m_conseq;
|
||||
prop_info(unsigned sz, unsigned const* ids, expr_ref const& c):
|
||||
m_ids(sz, ids),
|
||||
svector<std::pair<unsigned, unsigned>> m_eqs;
|
||||
prop_info(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr_ref const& c):
|
||||
m_ids(num_fixed, fixed_ids),
|
||||
m_conseq(c)
|
||||
{}
|
||||
{
|
||||
for (unsigned i = 0; i < num_eqs; ++i)
|
||||
m_eqs.push_back(std::make_pair(eq_lhs[i], eq_rhs[i]));
|
||||
}
|
||||
};
|
||||
unsigned m_qhead;
|
||||
|
||||
struct stats {
|
||||
unsigned m_num_propagations;
|
||||
stats() { reset(); }
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
};
|
||||
|
||||
void* m_user_context;
|
||||
solver::push_eh_t m_push_eh;
|
||||
solver::pop_eh_t m_pop_eh;
|
||||
solver::fresh_eh_t m_fresh_eh;
|
||||
solver::final_eh_t m_final_eh;
|
||||
solver::fixed_eh_t m_fixed_eh;
|
||||
solver::eq_eh_t m_eq_eh;
|
||||
solver::eq_eh_t m_diseq_eh;
|
||||
void* m_api_context { nullptr };
|
||||
|
||||
unsigned m_qhead { 0 };
|
||||
vector<prop_info> m_prop;
|
||||
unsigned_vector m_prop_lim;
|
||||
vector<literal_vector> m_id2justification;
|
||||
unsigned m_num_scopes;
|
||||
unsigned m_num_scopes { 0 };
|
||||
literal_vector m_lits;
|
||||
stats m_stats;
|
||||
|
||||
void force_push();
|
||||
|
||||
public:
|
||||
user_propagator(context& ctx);
|
||||
|
||||
~user_propagator() override {}
|
||||
~user_propagator() override;
|
||||
|
||||
/*
|
||||
* \brief initial setup for user propagator.
|
||||
*/
|
||||
void add(
|
||||
void* ctx,
|
||||
std::function<void(void*)>& push_eh,
|
||||
std::function<void(void*, unsigned)>& pop_eh,
|
||||
std::function<void*(void*)>& fresh_eh) {
|
||||
void* ctx,
|
||||
solver::push_eh_t& push_eh,
|
||||
solver::pop_eh_t& pop_eh,
|
||||
solver::fresh_eh_t& fresh_eh) {
|
||||
m_user_context = ctx;
|
||||
m_push_eh = push_eh;
|
||||
m_pop_eh = pop_eh;
|
||||
|
|
@ -81,7 +95,9 @@ namespace smt {
|
|||
void register_eq(solver::eq_eh_t& eq_eh) { m_eq_eh = eq_eh; }
|
||||
void register_diseq(solver::eq_eh_t& diseq_eh) { m_diseq_eh = diseq_eh; }
|
||||
|
||||
void propagate(unsigned sz, unsigned const* ids, expr* conseq) override;
|
||||
bool has_fixed() const { return (bool)m_fixed_eh; }
|
||||
|
||||
void propagate(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* lhs, unsigned const* rhs, expr* conseq) override;
|
||||
|
||||
void new_fixed_eh(theory_var v, expr* value, unsigned num_lits, literal const* jlits);
|
||||
|
||||
|
|
@ -99,7 +115,7 @@ namespace smt {
|
|||
void push_scope_eh() override;
|
||||
void pop_scope_eh(unsigned num_scopes) override;
|
||||
void restart_eh() override {}
|
||||
void collect_statistics(::statistics & st) const override {}
|
||||
void collect_statistics(::statistics & st) const override;
|
||||
model_value_proc * mk_value(enode * n, model_generator & mg) override { return nullptr; }
|
||||
void init_model(model_generator & m) override {}
|
||||
bool include_func_interp(func_decl* f) override { return false; }
|
||||
|
|
|
|||
|
|
@ -239,22 +239,26 @@ public:
|
|||
|
||||
virtual expr_ref get_implied_upper_bound(expr* e) = 0;
|
||||
|
||||
virtual void user_propagate_init(
|
||||
void* ctx,
|
||||
std::function<void(void*)>& push_eh,
|
||||
std::function<void(void*, unsigned)>& pop_eh,
|
||||
std::function<void*(void*)>& fresh_eh) {
|
||||
throw default_exception("user-propagators are only supported on the SMT solver");
|
||||
}
|
||||
|
||||
class propagate_callback {
|
||||
public:
|
||||
virtual void propagate(unsigned sz, unsigned const* ids, expr* conseq) = 0;
|
||||
virtual void propagate(unsigned num_fixed, unsigned const* fixed_ids, unsigned num_eqs, unsigned const* eq_lhs, unsigned const* eq_rhs, expr* conseq) = 0;
|
||||
};
|
||||
|
||||
typedef std::function<void(void*, solver::propagate_callback*)> final_eh_t;
|
||||
typedef std::function<void(void*, solver::propagate_callback*, unsigned, expr*)> fixed_eh_t;
|
||||
typedef std::function<void(void*, solver::propagate_callback*, unsigned, unsigned)> eq_eh_t;
|
||||
typedef std::function<void*(void*, ast_manager&, void*&)> fresh_eh_t;
|
||||
typedef std::function<void(void*)> push_eh_t;
|
||||
typedef std::function<void(void*,unsigned)> pop_eh_t;
|
||||
|
||||
virtual void user_propagate_init(
|
||||
void* ctx,
|
||||
push_eh_t& push_eh,
|
||||
pop_eh_t& pop_eh,
|
||||
fresh_eh_t& fresh_eh) {
|
||||
throw default_exception("user-propagators are only supported on the SMT solver");
|
||||
}
|
||||
|
||||
|
||||
virtual void user_propagate_register_fixed(fixed_eh_t& fixed_eh) {
|
||||
throw default_exception("user-propagators are only supported on the SMT solver");
|
||||
|
|
|
|||
Loading…
Reference in a new issue