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

Minor fixes to model

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-16 13:42:26 -07:00
parent 450da5ea0c
commit 60888a93eb
1 changed files with 9 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/model/model.h
View file

@ -24,10 +24,13 @@ Revision History:
#include "util/ref.h"
#include "ast/ast_translation.h"
class model;
typedef ref<model> model_ref;
class model : public model_core {
protected:
typedef obj_map<sort, ptr_vector<expr>*> sort2universe;
ptr_vector<sort> 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<expr> 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> model_ref;
#endif /* MODEL_H_ */