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