1 /*++ 2 Copyright (c) 2015 Microsoft Corporation 3 4 Module Name: 5 6 qe_datatypes.h 7 8 Abstract: 9 10 Model based projection for algebraic datatypes 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/datatype_decl_plugin.h" 24 #include "qe/mbp/mbp_plugin.h" 25 26 namespace mbp { 27 28 class datatype_project_plugin : public project_plugin { 29 struct imp; 30 imp* m_imp; 31 public: 32 datatype_project_plugin(ast_manager& m); 33 ~datatype_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 family_id get_family_id() override; 37 vector<def> project(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; 38 void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override; 39 40 }; 41 42 }; 43 44