From 60888a93eb24d4f5ce0b3defaaeccfba2c977af7 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 16 Jun 2018 13:42:26 -0700 Subject: [PATCH] Minor fixes to model --- src/model/model.h | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/src/model/model.h b/src/model/model.h index 3fda2832f..429e7b51a 100644 --- a/src/model/model.h +++ b/src/model/model.h @@ -24,10 +24,13 @@ Revision History: #include "util/ref.h" #include "ast/ast_translation.h" +class model; +typedef ref model_ref; + class model : public model_core { protected: typedef obj_map*> sort2universe; - + ptr_vector m_usorts; sort2universe m_usort2universe; model_evaluator m_mev; @@ -42,10 +45,10 @@ public: void copy_usort_interps(model const & source); model * copy() const; - + bool eval(func_decl * f, expr_ref & r) const { return model_core::eval(f, r); } bool eval(expr * e, expr_ref & result, bool model_completion = false); - + expr * get_some_value(sort * s) override; ptr_vector const & get_universe(sort * s) const override; unsigned get_num_uninterpreted_sorts() const override; @@ -78,25 +81,21 @@ public: bool m_old_completion; model& m_model; public: - scoped_model_completion(model& m, bool c): + scoped_model_completion(model& m, bool c): m_old_completion(m.m_mev.get_model_completion()), m_model(m) { m.set_model_completion(c); } -#if 0 - scoped_model_completion(model_ref& m, bool c): + scoped_model_completion(model_ref& m, bool c): m_old_completion(m->m_mev.get_model_completion()), m_model(*m.get()) { m->set_model_completion(c); } -#endif ~scoped_model_completion() { m_model.set_model_completion(m_old_completion); } }; - + }; -typedef ref model_ref; #endif /* MODEL_H_ */ -