diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-10 22:15:38 +0000 |
commit | d6b37239a2e525e7878d3bb0b4372a8dabc340a9 (patch) | |
tree | 3db6b54c8b5873db1e6c91b1577d431d74632c66 /src/theory/shared_data.h | |
parent | 7a059452ebf5729723f610da9258a47007e38253 (diff) |
additional model gen and SMT-LIBv2 compliance work: (get-assignment) now supported; work on Result type (biggest noticeable change is that CVC4 now outputs lowercase "sat" and "unsat"), Options class moved to src/smt, to allow for future work on runtime configuration via (set-option) command
Diffstat (limited to 'src/theory/shared_data.h')
-rw-r--r-- | src/theory/shared_data.h | 43 |
1 files changed, 26 insertions, 17 deletions
diff --git a/src/theory/shared_data.h b/src/theory/shared_data.h index 0b21eedae..181508c54 100644 --- a/src/theory/shared_data.h +++ b/src/theory/shared_data.h @@ -51,8 +51,8 @@ namespace theory { class SharedData : public context::ContextObj { private: /** - * Bit-vector representation of list of theories needing to be notified if - * this shared term is no longer the representative + * Bit-vector representation of list of theories needing to be + * notified if this shared term is no longer the representative */ uint64_t d_theories; @@ -72,25 +72,29 @@ private: SharedData* d_proofNext; /** - * In order to precisely reconstruct the equality that justifies this node - * being equal to the node at d_proofNext, we need to know whether this edge - * has been switched. Value is meaningless at the proof root. + * In order to precisely reconstruct the equality that justifies + * this node being equal to the node at d_proofNext, we need to know + * whether this edge has been switched. Value is meaningless at the + * proof root. */ bool d_edgeReversed; /** - * The theory that can explain the equality of this node and the node at - * d_proofNext. Not valid if this is proof root. + * The theory that can explain the equality of this node and the + * node at d_proofNext. Not valid if this is proof root. */ theory::Theory* d_explainingTheory; /** - * This is a pointer back to the node associated with this SharedData object. + * This is a pointer back to the node associated with this + * SharedData object. * * The following invariant should be maintained: - * (n.getAttribute(SharedAttr()))->d_rep == n - * i.e. rep is equal to the node that maps to the SharedData using SharedAttr. * + * (n.getAttribute(SharedAttr()))->d_rep == n + * + * i.e. rep is equal to the node that maps to the SharedData using + * SharedAttr. */ TNode d_rep; @@ -133,8 +137,8 @@ public: void setSize(unsigned size) { makeCurrent(); d_size = size; } /** - * Returns the find pointer of the SharedData. - * If this is the representative of the equivalence class, then getFind() == this + * Returns the find pointer of the SharedData. If this is the + * representative of the equivalence class, then getFind() == this */ SharedData* getFind() const { return d_find; } @@ -169,13 +173,15 @@ public: void setEdgeReversed(bool value) { makeCurrent(); d_edgeReversed = value; } /** - * Get the original equality that created the link from this node to the next - * proof node. + * Get the original equality that created the link from this node to + * the next proof node. */ Node getEquality() const { return d_edgeReversed - ? NodeManager::currentNM()->mkNode(kind::EQUAL, d_proofNext->getRep(), d_rep) - : NodeManager::currentNM()->mkNode(kind::EQUAL, d_rep, d_proofNext->getRep()); + ? NodeManager::currentNM()->mkNode(kind::EQUAL, + d_proofNext->getRep(), d_rep) + : NodeManager::currentNM()->mkNode(kind::EQUAL, + d_rep, d_proofNext->getRep()); } /** @@ -186,7 +192,10 @@ public: /** * Set the explaining theory */ - void setExplainingTheory(theory::Theory* t) { makeCurrent(); d_explainingTheory = t; } + void setExplainingTheory(theory::Theory* t) { + makeCurrent(); + d_explainingTheory = t; + } /** * Get the shared term associated with this data |