1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 theory_datatype.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-10-31. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "util/union_find.h" 22 #include "ast/array_decl_plugin.h" 23 #include "ast/datatype_decl_plugin.h" 24 #include "model/datatype_factory.h" 25 #include "smt/smt_theory.h" 26 #include "smt/params/theory_datatype_params.h" 27 28 namespace smt { 29 class theory_datatype : public theory { 30 typedef union_find<theory_datatype> th_union_find; 31 32 struct var_data { 33 ptr_vector<enode> m_recognizers; //!< recognizers of this equivalence class that are being watched. 34 enode * m_constructor; //!< constructor of this equivalence class, 0 if there is no constructor in the eqc. var_datavar_data35 var_data(): 36 m_constructor(nullptr) { 37 } 38 }; 39 40 struct stats { 41 unsigned m_occurs_check, m_splits; 42 unsigned m_assert_cnstr, m_assert_accessor, m_assert_update_field; resetstats43 void reset() { memset(this, 0, sizeof(stats)); } statsstats44 stats() { reset(); } 45 }; 46 47 datatype_util m_util; 48 array_util m_autil; 49 ptr_vector<var_data> m_var_data; 50 th_union_find m_find; 51 trail_stack m_trail_stack; 52 datatype_factory * m_factory; 53 stats m_stats; 54 is_constructor(app * f)55 bool is_constructor(app * f) const { return m_util.is_constructor(f); } is_recognizer(app * f)56 bool is_recognizer(app * f) const { return m_util.is_recognizer(f); } is_accessor(app * f)57 bool is_accessor(app * f) const { return m_util.is_accessor(f); } is_update_field(app * f)58 bool is_update_field(app * f) const { return m_util.is_update_field(f); } 59 is_constructor(enode * n)60 bool is_constructor(enode * n) const { return is_constructor(n->get_expr()); } is_recognizer(enode * n)61 bool is_recognizer(enode * n) const { return is_recognizer(n->get_expr()); } is_accessor(enode * n)62 bool is_accessor(enode * n) const { return is_accessor(n->get_expr()); } is_update_field(enode * n)63 bool is_update_field(enode * n) const { return m_util.is_update_field(n->get_expr()); } 64 65 void assert_eq_axiom(enode * lhs, expr * rhs, literal antecedent); 66 void assert_is_constructor_axiom(enode * n, func_decl * c, literal antecedent); 67 void assert_accessor_axioms(enode * n); 68 void assert_update_field_axioms(enode * n); 69 void add_recognizer(theory_var v, enode * recognizer); 70 void propagate_recognizer(theory_var v, enode * r); 71 void sign_recognizer_conflict(enode * c, enode * r); 72 73 typedef enum { ENTER, EXIT } stack_op; 74 typedef obj_map<enode, enode*> parent_tbl; 75 typedef std::pair<stack_op, enode*> stack_entry; 76 77 ptr_vector<enode> m_to_unmark; 78 ptr_vector<enode> m_to_unmark2; 79 enode_pair_vector m_used_eqs; // conflict, if any 80 parent_tbl m_parent; // parent explanation for occurs_check 81 svector<stack_entry> m_stack; // stack for DFS for occurs_check 82 literal_vector m_lits; 83 84 void clear_mark(); 85 86 void oc_mark_on_stack(enode * n); oc_on_stack(enode * n)87 bool oc_on_stack(enode * n) const { return n->get_root()->is_marked(); } 88 89 void oc_mark_cycle_free(enode * n); oc_cycle_free(enode * n)90 bool oc_cycle_free(enode * n) const { return n->get_root()->is_marked2(); } 91 92 void oc_push_stack(enode * n); 93 ptr_vector<enode> m_array_args; 94 ptr_vector<enode> const& get_array_args(enode* n); 95 96 // class for managing state of final_check 97 class final_check_st { 98 theory_datatype * th; 99 public: 100 final_check_st(theory_datatype * th); 101 ~final_check_st(); 102 }; 103 104 enode * oc_get_cstor(enode * n); 105 bool occurs_check(enode * n); 106 bool occurs_check_enter(enode * n); 107 void occurs_check_explain(enode * top, enode * root); 108 void explain_is_child(enode* parent, enode* child); 109 110 void mk_split(theory_var v); 111 112 void display_var(std::ostream & out, theory_var v) const; 113 114 protected: 115 theory_var mk_var(enode * n) override; 116 bool internalize_atom(app * atom, bool gate_ctx) override; 117 bool internalize_term(app * term) override; 118 void apply_sort_cnstr(enode * n, sort * s) override; 119 void new_eq_eh(theory_var v1, theory_var v2) override; 120 bool use_diseqs() const override; 121 void new_diseq_eh(theory_var v1, theory_var v2) override; 122 void assign_eh(bool_var v, bool is_true) override; 123 void relevant_eh(app * n) override; 124 void push_scope_eh() override; 125 void pop_scope_eh(unsigned num_scopes) override; 126 final_check_status final_check_eh() override; 127 void reset_eh() override; restart_eh()128 void restart_eh() override { m_util.reset(); } 129 bool is_shared(theory_var v) const override; 130 theory_datatype_params const& params() const; 131 public: 132 theory_datatype(context& ctx); 133 ~theory_datatype() override; 134 theory * mk_fresh(context * new_ctx) override; 135 void display(std::ostream & out) const override; 136 void collect_statistics(::statistics & st) const override; 137 void init_model(model_generator & m) override; 138 model_value_proc * mk_value(enode * n, model_generator & m) override; get_trail_stack()139 trail_stack & get_trail_stack() { return m_trail_stack; } 140 virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var); after_merge_eh(theory_var r1,theory_var r2,theory_var v1,theory_var v2)141 static void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {} 142 void unmerge_eh(theory_var v1, theory_var v2); get_name()143 char const * get_name() const override { return "datatype"; } 144 bool include_func_interp(func_decl* f) override; 145 146 }; 147 148 }; 149 150 151