From ecf15ab07d006d213f8754fd5aeb8dd2e7ac7bc8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 16 May 2018 16:42:51 -0700
Subject: [PATCH] add model_evaluator_util features to model_evalautor

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/model_evaluator.cpp | 43 +++++++++++++++++++++++++++++++++++
 src/model/model_evaluator.h   | 10 +++++++-
 2 files changed, 52 insertions(+), 1 deletion(-)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 0b25a250b..07ee125f8 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -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);
+}
+
+
+
diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h
index bd2b2d664..6ae7d8891 100644
--- a/src/model/model_evaluator.h
+++ b/src/model/model_evaluator.h
@@ -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;
 };