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