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