mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

add model_evaluator_util features to model_evalautor

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-16 16:42:51 -07:00 committed by Arie Gurfinkel
parent 8d312f9d1f
commit ecf15ab07d
2 changed files with 52 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/model/model_evaluator.cpp
View file

@ -562,6 +562,12 @@ void model_evaluator::reset(params_ref const & p) {
updt_params(p);
}
void model_evaluator::reset(model_core &model, params_ref const& p) {
dealloc(m_imp);
m_imp = alloc(imp, model, 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);
@ -574,3 +580,40 @@ expr_ref model_evaluator::operator()(expr * t) {
this->operator()(t, result);
return result;
}
bool model_evaluator::is_true(expr* t) {
expr_ref tmp(m());
return eval(t, tmp, true) && m().is_true(tmp);
}
bool model_evaluator::is_false(expr* t) {
expr_ref tmp(m());
return eval(t, tmp, true) && m().is_false(tmp);
}
bool model_evaluator::is_true(expr_ref_vector const& ts) {
for (expr* t : ts) if (!is_true(t)) return false;
return true;
}
bool model_evaluator::eval(expr* t, expr_ref& r, bool model_completion) {
set_model_completion(model_completion);
try {
r = (*this)(t);
return true;
}
catch (model_evaluator_exception &ex) {
(void)ex;
TRACE("model_evaluator", tout << ex.msg () << "\n";);
return false;
}
}
bool model_evaluator::eval(expr_ref_vector const& ts, expr_ref& r, bool model_completion) {
expr_ref tmp(m());
tmp = mk_and(ts);
return eval(tmp, r, model_completion);
}

10
src/model/model_evaluator.h
View file

@ -43,11 +43,19 @@ public:
static void get_param_descrs(param_descrs & r);
void operator()(expr * t, expr_ref & r);
expr_ref operator()(expr* t);
// exception safe
bool eval(expr* t, expr_ref& r, bool model_completion = true);
bool eval(expr_ref_vector const& ts, expr_ref& r, bool model_completion = true);
bool is_true(expr * t);
bool is_false(expr * t);
bool is_true(expr_ref_vector const& ts);
void cleanup(params_ref const & p = params_ref());
void reset(params_ref const & p = params_ref());
void reset(model_core& model, params_ref const & p = params_ref());
unsigned get_num_steps() const;
};