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