1 /*++ 2 Copyright (c) 2014 Microsoft Corporation 3 4 Module Name: 5 6 fpa_solver.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 "sat/smt/euf_solver.h" 22 #include "ast/fpa/fpa2bv_converter.h" 23 #include "ast/fpa/fpa2bv_rewriter.h" 24 25 namespace fpa { 26 27 typedef euf::enode enode; 28 typedef euf::theory_var theory_var; 29 30 class solver : public euf::th_euf_solver { 31 protected: 32 th_rewriter m_th_rw; 33 fpa2bv_converter_wrapped m_converter; 34 fpa2bv_rewriter m_rw; 35 fpa_util & m_fpa_util; 36 bv_util & m_bv_util; 37 arith_util & m_arith_util; 38 obj_map<expr, expr*> m_conversions; 39 svector<std::tuple<enode*, bool, bool>> m_nodes; 40 unsigned m_nodes_qhead = 0; 41 42 bool visit(expr* e) override; 43 bool visited(expr* e) override; 44 bool post_visit(expr* e, bool sign, bool root) override; 45 46 expr_ref convert(expr* e); 47 sat::literal_vector mk_side_conditions(); 48 void attach_new_th_var(enode* n); 49 void activate(expr* e); 50 void unit_propagate(std::tuple<enode*, bool, bool> const& t); 51 void ensure_equality_relation(theory_var x, theory_var y); 52 53 public: 54 solver(euf::solver& ctx); 55 ~solver() override; 56 57 void asserted(sat::literal l) override; 58 void new_eq_eh(euf::th_eq const& eq) override; use_diseqs()59 bool use_diseqs() const override { return true; } 60 void new_diseq_eh(euf::th_eq const& eq) override; 61 62 sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; 63 void internalize(expr* e, bool redundant) override; 64 void apply_sort_cnstr(euf::enode* n, sort* s) override; 65 66 std::ostream& display(std::ostream& out) const override; display_justification(std::ostream & out,sat::ext_justification_idx idx)67 std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override { UNREACHABLE(); return out; } display_constraint(std::ostream & out,sat::ext_constraint_idx idx)68 std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const override { UNREACHABLE(); return out; } 69 void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override; 70 bool add_dep(euf::enode* n, top_sort<euf::enode>& dep) override; 71 void finalize_model(model& mdl) override; 72 73 bool unit_propagate() override; get_antecedents(sat::literal l,sat::ext_justification_idx idx,sat::literal_vector & r,bool probing)74 void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override { UNREACHABLE(); } 75 sat::check_result check() override; 76 clone(euf::solver & ctx)77 euf::th_solver* clone(euf::solver& ctx) override { return alloc(solver, ctx); } 78 79 }; 80 81 } 82 83 84