diff options
author | Tim King <taking@google.com> | 2017-03-27 09:40:30 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2017-03-27 09:40:30 -0700 |
commit | 7b89724488085d7eed3e37520ca11d8cd1e18120 (patch) | |
tree | 0d04fdd6a44fb2b32dac3971fb8cee68a291fd08 /src/theory/theory.h | |
parent | 0be62eeea95eaf27913e792c17dd79afb96b16cb (diff) |
Moving the theory::Assertion struct into its own file.
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 53 |
1 files changed, 10 insertions, 43 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index fd8cffa9f..0bea566b1 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -35,6 +35,7 @@ #include "smt/command.h" #include "smt/dump.h" #include "smt/logic_request.h" +#include "theory/assertion.h" #include "theory/logic_info.h" #include "theory/output_channel.h" #include "theory/valuation.h" @@ -62,53 +63,23 @@ namespace eq { class EqualityEngine; }/* CVC4::theory::eq namespace */ -/** - * Information about an assertion for the theories. - */ -struct Assertion { - - /** The assertion */ - Node assertion; - /** Has this assertion been preregistered with this theory */ - bool isPreregistered; - - Assertion(TNode assertion, bool isPreregistered) - : assertion(assertion), isPreregistered(isPreregistered) {} - - /** - * Convert the assertion to a TNode. - */ - operator TNode () const { - return assertion; - } - - /** - * Convert the assertion to a Node. - */ - operator Node () const { - return assertion; - } - -};/* struct Assertion */ /** - * A (oredered) pair of terms a theory cares about. + * A (ordered) pair of terms a theory cares about. */ struct CarePair { - - TNode a, b; - TheoryId theory; - -public: + public: + const TNode a, b; + const TheoryId theory; CarePair(TNode a, TNode b, TheoryId theory) - : a(a < b ? a : b), b(a < b ? b : a), theory(theory) {} + : a(a < b ? a : b), b(a < b ? b : a), theory(theory) {} - bool operator == (const CarePair& other) const { + bool operator==(const CarePair& other) const { return (theory == other.theory) && (a == other.a) && (b == other.b); } - bool operator < (const CarePair& other) const { + bool operator<(const CarePair& other) const { if (theory < other.theory) return true; if (theory > other.theory) return false; if (a < other.a) return true; @@ -116,7 +87,7 @@ public: return b < other.b; } -};/* struct CarePair */ +}; /* struct CarePair */ /** * A set of care pairs. @@ -924,7 +895,7 @@ public: };/* class Theory */ std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); -inline std::ostream& operator<<(std::ostream& out, const theory::Assertion& a); + inline theory::Assertion Theory::get() { Assert( !done(), "Theory::get() called with assertion queue empty!" ); @@ -942,10 +913,6 @@ inline theory::Assertion Theory::get() { return fact; } -inline std::ostream& operator<<(std::ostream& out, const theory::Assertion& a) { - return out << a.assertion; -} - inline std::ostream& operator<<(std::ostream& out, const CVC4::theory::Theory& theory) { return out << theory.identify(); |