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