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

build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-08-13 16:40:41 -07:00
parent 7d391d44a2
commit 094e41d21d
2 changed files with 28 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/api/julia/z3jl.cpp
View file

@ -451,7 +451,9 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
.method("add", static_cast<void (optimize::*)(expr const &)>(&optimize::add))
.method("add", static_cast<optimize::handle (optimize::*)(expr const &, unsigned)>(&optimize::add))
.method("add", static_cast<void (optimize::*)(expr const &, expr const &)>(&optimize::add))
.method("add", static_cast<optimize::handle (optimize::*)(expr const &, char const *)>(&optimize::add))
.method("add", static_cast<optimize::handle (optimize::*)(expr const &, unsigned)>(&optimize::add_soft))
.method("add_soft", static_cast<optimize::handle (optimize::*)(expr const &, unsigned)>(&optimize::add_soft))
.method("add_soft", static_cast<optimize::handle (optimize::*)(expr const &, char const *)>(&optimize::add_soft))
.MM(optimize, maximize)
.MM(optimize, minimize)
.MM(optimize, push)
@ -713,4 +715,4 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
.method("parse_string", static_cast<expr_vector (context::*)(char const*, sort_vector const&, func_decl_vector const&)>(&context::parse_string))
.method("parse_file", static_cast<expr_vector (context::*)(char const*)>(&context::parse_file))
.method("parse_file", static_cast<expr_vector (context::*)(char const*, sort_vector const&, func_decl_vector const&)>(&context::parse_file));
}
}

40
src/model/model_evaluator.cpp
View file

@ -160,11 +160,20 @@ struct evaluator_cfg : public default_rewriter_cfg {
family_id fid = f->get_family_id();
bool _is_uninterp = fid != null_family_id && m.get_plugin(fid)->is_considered_uninterpreted(f);
br_status st = BR_FAILED;
#if 1
struct pp {
func_decl* f;
expr_ref& r;
pp(func_decl* f, expr_ref& r) :f(f), r(r) {}
~pp() { TRACE("model_evaluator", tout << mk_pp(f, r.m()) << " " << r << "\n";); }
};
pp _pp(f, result);
#endif
if (num == 0 && (fid == null_family_id || _is_uninterp || m_ar.is_as_array(f))) {
expr * val = m_model.get_const_interp(f);
if (val != nullptr) {
result = val;
st = m_ar.is_as_array(val)? BR_REWRITE1 : BR_DONE;
st = m_ar.is_as_array(val) /* || m.is_eq(val)*/ ? BR_REWRITE1 : BR_DONE;
TRACE("model_evaluator", tout << result << "\n";);
return st;
}
@ -250,6 +259,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
expr* def = nullptr;
if (m_def_cache.find(g, def)) {
result = def;
TRACE("model_evaluator", tout << result << "\n";);
return BR_DONE;
}
func_interp * fi = m_model.get_func_interp(g);
@ -282,17 +292,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
args.append(stores[i].size(), stores[i].c_ptr());
val = m_ar.mk_store(args);
}
TRACE("model_evaluator", tout << val << "\n";);
}
}
bool get_macro(func_decl * f, expr * & def, quantifier * & , proof * &) {
#define TRACE_MACRO TRACE("model_evaluator", tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ")\n";);
func_interp * fi = m_model.get_func_interp(f);
def = nullptr;
if (fi != nullptr) {
TRACE_MACRO;
if (fi->is_partial()) {
if (m_model_completion) {
sort * s = f->get_range();
@ -304,24 +311,22 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
def = fi->get_interp();
SASSERT(def != nullptr);
return true;
}
if (m_model_completion &&
else if (m_model_completion &&
(f->get_family_id() == null_family_id ||
m.get_plugin(f->get_family_id())->is_considered_uninterpreted(f)))
{
TRACE_MACRO;
m.get_plugin(f->get_family_id())->is_considered_uninterpreted(f))) {
sort * s = f->get_range();
expr * val = m_model.get_some_value(s);
func_interp * new_fi = alloc(func_interp, m, f->get_arity());
new_fi->set_else(val);
m_model.register_decl(f, new_fi);
def = val;
return true;
SASSERT(def != nullptr);
}
return false;
CTRACE("model_evaluator", def != nullptr, tout << "get_macro for " << f->get_name() << " (model completion: " << m_model_completion << ") " << mk_pp(def, m) << "\n";);
return def != nullptr;
}
br_status evaluate_partial_theory_func(func_decl * f,
@ -560,7 +565,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
func_decl* f = m_ar.get_as_array_func_decl(to_app(a));
func_interp* g = m_model.get_func_interp(f);
if (!g) return false;
if (!g) {
TRACE("model_evaluator", tout << "no interpretation for " << mk_pp(f, m) << "\n";);
return false;
}
else_case = g->get_else();
if (!else_case) {
TRACE("model_evaluator", tout << "no else case " << mk_pp(a, m) << "\n";);
@ -669,8 +677,8 @@ void model_evaluator::reset(model_core &model, params_ref const& p) {
void model_evaluator::operator()(expr * t, expr_ref & result) {
TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
m_imp->operator()(t, result);
TRACE("model_evaluator", tout << result << "\n";);
m_imp->expand_stores(result);
TRACE("model_evaluator", tout << result << "\n";);
}
expr_ref model_evaluator::operator()(expr * t) {