1 /*++
2 Copyright (c) 2014 Microsoft Corporation
3 
4 Module Name:
5 
6     theory_fpa.h
7 
8 Abstract:
9 
10     Floating-Point Theory Plugin
11 
12 Author:
13 
14     Christoph (cwinter) 2014-04-23
15 
16 Revision History:
17 
18 --*/
19 #pragma once
20 
21 #include "smt/smt_theory.h"
22 #include "util/trail.h"
23 #include "ast/fpa/fpa2bv_converter.h"
24 #include "ast/fpa/fpa2bv_rewriter.h"
25 #include "ast/rewriter/th_rewriter.h"
26 #include "model/fpa_factory.h"
27 #include "smt/smt_model_generator.h"
28 
29 namespace smt {
30 
31     class theory_fpa : public theory {
32     protected:
33         typedef trail_stack<theory_fpa> th_trail_stack;
34 
35 
36         class fpa_value_proc : public model_value_proc {
37         protected:
38             theory_fpa  & m_th;
39             ast_manager & m;
40             fpa_util    & m_fu;
41             bv_util     & m_bu;
42             buffer<model_value_dependency> m_deps;
43             unsigned m_ebits;
44             unsigned m_sbits;
45 
46         public:
fpa_value_proc(theory_fpa * th,unsigned ebits,unsigned sbits)47             fpa_value_proc(theory_fpa * th, unsigned ebits, unsigned sbits) :
48                 m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util),
49                 m_ebits(ebits), m_sbits(sbits) {}
50 
~fpa_value_proc()51             ~fpa_value_proc() override {}
52 
add_dependency(enode * e)53             void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
54 
get_dependencies(buffer<model_value_dependency> & result)55             void get_dependencies(buffer<model_value_dependency> & result) override {
56                 result.append(m_deps);
57             }
58 
59             app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
60         };
61 
62         class fpa_rm_value_proc : public model_value_proc {
63             theory_fpa  & m_th;
64             ast_manager & m;
65             fpa_util    & m_fu;
66             bv_util     & m_bu;
67             buffer<model_value_dependency> m_deps;
68 
69         public:
fpa_rm_value_proc(theory_fpa * th)70             fpa_rm_value_proc(theory_fpa * th) :
71                 m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) { (void) m_th; }
72 
add_dependency(enode * e)73             void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
74 
get_dependencies(buffer<model_value_dependency> & result)75             void get_dependencies(buffer<model_value_dependency> & result) override {
76                 result.append(m_deps);
77             }
78 
~fpa_rm_value_proc()79             ~fpa_rm_value_proc() override {}
80             app * mk_value(model_generator & mg, expr_ref_vector const & values) override;
81         };
82 
83     protected:
84         th_rewriter               m_th_rw;
85         fpa2bv_converter_wrapped  m_converter;
86         fpa2bv_rewriter           m_rw;
87         th_trail_stack            m_trail_stack;
88         fpa_value_factory *       m_factory;
89         fpa_util                & m_fpa_util;
90         bv_util                 & m_bv_util;
91         arith_util              & m_arith_util;
92         obj_map<expr, expr*>      m_conversions;
93         bool                      m_is_initialized;
94         obj_hashtable<func_decl>  m_is_added_to_model;
95 
96         final_check_status final_check_eh() override;
97         bool internalize_atom(app * atom, bool gate_ctx) override;
98         bool internalize_term(app * term) override;
99         void apply_sort_cnstr(enode * n, sort * s) override;
100         void new_eq_eh(theory_var, theory_var) override;
101         void new_diseq_eh(theory_var, theory_var) override;
102         void push_scope_eh() override;
103         void pop_scope_eh(unsigned num_scopes) override;
104         void reset_eh() override;
105         theory* mk_fresh(context* new_ctx) override;
get_name()106         char const * get_name() const override { return "fpa"; }
107 
108         model_value_proc * mk_value(enode * n, model_generator & mg) override;
109 
110         void assign_eh(bool_var v, bool is_true) override;
111         void relevant_eh(app * n) override;
112         void init_model(model_generator & m) override;
113         void finalize_model(model_generator & mg) override;
114 
115     public:
116         theory_fpa(context& ctx);
117         ~theory_fpa() override;
118 
119         void display(std::ostream & out) const override;
120 
121     protected:
122         expr_ref mk_side_conditions();
123         expr_ref convert(expr * e);
124 
125         void attach_new_th_var(enode * n);
126         void assert_cnstr(expr * e);
127 
128 
129         enode* ensure_enode(expr* e);
get_root(expr * a)130         enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }
131         app* get_ite_value(expr* e);
132     };
133 
134 };
135 
136