1 /*++
2 Copyright (c) 2015 Microsoft Corporation
3 
4 Module Name:
5 
6     mbp_arrays.h
7 
8 Abstract:
9 
10     Model based projection for arrays
11 
12 Author:
13 
14     Nikolaj Bjorner (nbjorner) 2015-06-13
15 
16 Revision History:
17 
18 --*/
19 
20 
21 #pragma once
22 
23 #include "ast/array_decl_plugin.h"
24 #include "qe/mbp/mbp_plugin.h"
25 
26 namespace mbp {
27 
28     class array_project_plugin : public project_plugin {
29         struct imp;
30         imp* m_imp;
31     public:
32         array_project_plugin(ast_manager& m);
33         ~array_project_plugin() override;
34         bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override;
35         bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
36         void operator()(model& model, app_ref_vector& vars, expr_ref& fml, app_ref_vector& aux_vars, bool reduce_all_selects);
37         family_id get_family_id() override;
38         vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override;
39         void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override;
40 
41     };
42 
43 };
44 
45