1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 smt_bool_var_data.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2008-02-25. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "smt/smt_b_justification.h" 22 23 namespace smt { 24 25 struct bool_var_data { 26 private: 27 b_justification m_justification; 28 public: 29 unsigned m_scope_lvl:24; //!< scope level of when the variable was assigned. 30 unsigned m_mark:1; 31 unsigned m_assumption:1; 32 unsigned m_phase_available:1; 33 unsigned m_phase:1; 34 private: 35 unsigned m_eq:1; 36 unsigned m_true_first:1; //!< If True, when case splitting try the true phase first. Otherwise, you default phase selection heuristic. 37 unsigned m_enode:1; //!< has enode associated with it. 38 unsigned m_quantifier:1; //!< true if bool var is attached to a quantifier 39 unsigned m_iscope_lvl:23; //!< scope level of when the variable was internalized. 40 unsigned m_atom:1; //!< logical or of m_eq, m_enode, m_quantifier, and m_notify_theory != 0 41 unsigned m_notify_theory:8; 42 update_atom_flagbool_var_data43 void update_atom_flag() { 44 m_atom = m_eq || m_notify_theory != 0 || m_quantifier || m_enode; 45 } 46 public: 47 get_intern_levelbool_var_data48 unsigned get_intern_level() const { return m_iscope_lvl; } 49 justificationbool_var_data50 b_justification justification() const { return m_justification; } 51 set_axiombool_var_data52 void set_axiom() { m_justification = b_justification::mk_axiom(); } 53 set_null_justificationbool_var_data54 void set_null_justification() { m_justification = null_b_justification; } 55 set_justificationbool_var_data56 void set_justification(b_justification const& j) { m_justification = j; } 57 is_atombool_var_data58 bool is_atom() const { return m_atom; } 59 get_theorybool_var_data60 theory_id get_theory() const { 61 return m_notify_theory == 0 ? null_theory_id : static_cast<theory_id>(m_notify_theory); 62 } 63 is_theory_atombool_var_data64 bool is_theory_atom() const { return m_notify_theory != 0; } 65 set_notify_theorybool_var_data66 void set_notify_theory(theory_id thid) { 67 SASSERT(thid > 0 && thid <= 255); 68 m_notify_theory = thid; 69 m_atom = true; 70 } 71 reset_notify_theorybool_var_data72 void reset_notify_theory() { 73 m_notify_theory = 0; 74 update_atom_flag(); 75 } 76 is_enodebool_var_data77 bool is_enode() const { return m_enode; } 78 set_enode_flagbool_var_data79 void set_enode_flag() { 80 m_enode = true; 81 m_atom = true; 82 } 83 reset_enode_flagbool_var_data84 void reset_enode_flag() { 85 m_enode = false; 86 update_atom_flag(); 87 } 88 is_quantifierbool_var_data89 bool is_quantifier() const { return m_quantifier; } 90 set_quantifier_flagbool_var_data91 void set_quantifier_flag() { 92 m_quantifier = true; 93 m_atom = true; 94 } 95 is_eqbool_var_data96 bool is_eq() const { return m_eq; } 97 set_eq_flagbool_var_data98 void set_eq_flag() { 99 m_eq = true; 100 m_atom = true; 101 } 102 reset_eq_flagbool_var_data103 void reset_eq_flag() { 104 m_eq = false; 105 update_atom_flag(); 106 } 107 try_true_firstbool_var_data108 bool try_true_first() const { return m_true_first; } 109 set_true_first_flagbool_var_data110 void set_true_first_flag() { 111 m_true_first = true; 112 } 113 reset_true_first_flagbool_var_data114 void reset_true_first_flag() { 115 m_true_first = false; 116 } 117 initbool_var_data118 void init(unsigned iscope_lvl) { 119 m_justification = null_b_justification; 120 m_scope_lvl = 0; 121 m_mark = false; 122 m_assumption = false; 123 m_phase_available = false; 124 m_phase = false; 125 m_iscope_lvl = iscope_lvl; 126 m_eq = false; 127 m_true_first = false; 128 m_notify_theory = 0; 129 m_enode = false; 130 m_quantifier = false; 131 m_atom = false; 132 } 133 }; 134 }; 135 136 137