1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 spacer_mev_array.h 7 8 Abstract: 9 10 Utilities to evaluate arrays in the model. 11 12 Author: 13 based on model_evaluator in muz/pdr/pdr_util.h 14 15 Revision History: 16 17 --*/ 18 #pragma once 19 20 #include"ast/ast.h" 21 #include"ast/rewriter/rewriter_types.h" 22 #include"util/params.h" 23 #include"ast/array_decl_plugin.h" 24 25 /** 26 * based on model_evaluator in muz/pdr/pdr_util.h 27 */ 28 class model_evaluator_array_util { 29 ast_manager& m; 30 array_util m_array; 31 32 void eval_exprs(model& mdl, expr_ref_vector& es); 33 34 bool extract_array_func_interp(model& mdl, expr* a, vector<expr_ref_vector>& stores, expr_ref& else_case); 35 36 public: 37 model_evaluator_array_util(ast_manager & m)38 model_evaluator_array_util (ast_manager& m): 39 m (m), 40 m_array (m) 41 {} 42 43 /** 44 * best effort evaluator of extensional array equality. 45 */ 46 void eval_array_eq(model& mdl, app* e, expr* arg1, expr* arg2, expr_ref& res); 47 48 void eval(model& mdl, expr* e, expr_ref& r, bool model_completion = true); 49 }; 50 51