1 /** 2 Copyright (c) 2017 Arie Gurfinkel 3 4 Deprecated implementation of model evaluator. To be removed. 5 */ 6 #pragma once 7 8 #include "ast/ast.h" 9 #include "ast/ast_pp.h" 10 #include "util/obj_hashtable.h" 11 #include "util/ref_vector.h" 12 #include "util/trace.h" 13 #include "util/vector.h" 14 #include "ast/arith_decl_plugin.h" 15 #include "ast/array_decl_plugin.h" 16 #include "ast/bv_decl_plugin.h" 17 18 namespace old { 19 class model_evaluator { 20 ast_manager& m; 21 arith_util m_arith; 22 array_util m_array; 23 obj_map<expr, rational> m_numbers; 24 expr_ref_vector m_refs; 25 obj_map<expr, expr*> m_values; 26 model_ref m_model; 27 28 //00 -- non-visited 29 //01 -- X 30 //10 -- false 31 //11 -- true 32 expr_mark m1; 33 expr_mark m2; 34 35 /// used by collect() 36 expr_mark m_visited; 37 38 39 40 void reset(); 41 42 /// caches the values of all constants in the given model 43 void setup_model(const model_ref& model); 44 /// caches the value of an expression 45 void assign_value(expr* e, expr* v); 46 47 /// extracts an implicant of the conjunction of formulas 48 void collect(ptr_vector<expr> const& formulas, ptr_vector<expr>& tocollect); 49 50 /// one-round of extracting an implicant of e. The implicant 51 /// literals are stored in tocollect. The worklist is stored in todo 52 void process_formula(app* e, ptr_vector<expr>& todo, ptr_vector<expr>& tocollect); 53 void eval_arith(app* e); 54 void eval_basic(app* e); 55 void eval_eq(app* e, expr* arg1, expr* arg2); 56 void eval_array_eq(app* e, expr* arg1, expr* arg2); 57 void inherit_value(expr* e, expr* v); 58 is_unknown(expr * x)59 bool is_unknown(expr* x) { return !m1.is_marked(x) && !m2.is_marked(x); } set_unknown(expr * x)60 void set_unknown(expr* x) { m1.mark(x, false); m2.mark(x, false); } is_x(expr * x)61 bool is_x(expr* x) { return !m1.is_marked(x) && m2.is_marked(x); } is_false(expr * x)62 bool is_false(expr* x) { return m1.is_marked(x) && !m2.is_marked(x); } is_true(expr * x)63 bool is_true(expr* x) { return m1.is_marked(x) && m2.is_marked(x); } set_x(expr * x)64 void set_x(expr* x) { SASSERT(is_unknown(x)); m2.mark(x); } set_v(expr * x)65 void set_v(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); } set_false(expr * x)66 void set_false(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); } set_true(expr * x)67 void set_true(expr* x) { SASSERT(is_unknown(x)); m1.mark(x); m2.mark(x); } set_bool(expr * x,bool v)68 void set_bool(expr* x, bool v) { if(v) { set_true(x); } else { set_false(x); } } get_number(expr * x)69 rational const& get_number(expr* x) const { return m_numbers.find(x); } set_number(expr * x,rational const & v)70 void set_number(expr* x, rational const& v) 71 { 72 set_v(x); 73 m_numbers.insert(x, v); 74 TRACE("spacer_verbose", tout << mk_pp(x, m) << " " << v << "\n";); 75 } get_value(expr * x)76 expr* get_value(expr* x) { return m_values.find(x); } set_value(expr * x,expr * v)77 void set_value(expr* x, expr* v) 78 { set_v(x); m_refs.push_back(v); m_values.insert(x, v); } 79 80 81 /// evaluates all sub-formulas and terms of the input in the current model. 82 /// Caches the result 83 void eval_fmls(ptr_vector<expr> const & formulas); 84 85 /// calls eval_fmls(). Then checks whether all formulas are 86 /// TRUE. Returns false if at lest one formula is unknown (X) 87 bool check_model(ptr_vector<expr> const & formulas); 88 89 bool extract_array_func_interp(expr* a, vector<expr_ref_vector>& stores, 90 expr_ref& else_case); 91 92 void eval_exprs(expr_ref_vector& es); 93 94 public: model_evaluator(ast_manager & m)95 model_evaluator(ast_manager& m) : m(m), m_arith(m), m_array(m), m_refs(m) {} 96 97 98 /** 99 \brief extract literals from formulas that satisfy formulas. 100 101 \pre model satisfies formulas 102 */ 103 void minimize_literals(ptr_vector<expr> const & formulas, const model_ref& mdl, 104 expr_ref_vector& result); 105 106 expr_ref eval_heavy(const model_ref& mdl, expr* fml); 107 108 expr_ref eval(const model_ref& mdl, expr* e); 109 expr_ref eval(const model_ref& mdl, func_decl* d); 110 }; 111 } 112 113 114 115