From bc6604441b7af1c138a9e5cd3f2c2ac09955b4f2 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 14:32:43 -0400 Subject: [PATCH] Helpers in model_core --- src/model/model_core.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/model/model_core.h b/src/model/model_core.h index d705e432d..7f5051386 100644 --- a/src/model/model_core.h +++ b/src/model/model_core.h @@ -48,6 +48,14 @@ public: func_interp * get_func_interp(func_decl * d) const { func_interp * fi; return m_finterp.find(d, fi) ? fi : nullptr; } bool eval(func_decl * f, expr_ref & r) const; + bool is_true_decl(func_decl *f) const { + expr_ref r(m); + return eval(f, r) && m.is_true(r); + } + bool is_false_decl(func_decl *f) const { + expr_ref r(m); + return eval(f, r) && m.is_false(r); + } unsigned get_num_constants() const { return m_const_decls.size(); } unsigned get_num_functions() const { return m_func_decls.size(); }