diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 15:16:43 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-25 17:39:21 -0500 |
commit | 195dffbb7468e814d3dc3226666688869c13ba3d (patch) | |
tree | 4c4915245a90615ea36cbcfbb4a8a6dcc910c384 /src/theory/theory.h | |
parent | 73760b3c213733fc98d67f9ceeb74d06b01a3777 (diff) |
Fix errors and reduce warnings on clang (merge from mdeters/clang)
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index e76441f6b..5b2032430 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -50,13 +50,13 @@ namespace theory { class QuantifiersEngine; class TheoryModel; -namespace rrinst{ -class CandidateGenerator; -} +namespace rrinst { + class CandidateGenerator; +}/* CVC4::theory::rrinst namespace */ namespace eq { -class EqualityEngine; -} + class EqualityEngine; +}/* CVC4::theory::eq namespace */ /** * Information about an assertion for the theories. @@ -787,14 +787,10 @@ public: std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const; };/* class Theory */ -std::ostream& operator<<(std::ostream& os, Theory::Effort level); - -namespace eq{ - class EqualityEngine; -} - +std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); +inline std::ostream& operator<<(std::ostream& out, const theory::Assertion& a); -inline Assertion Theory::get() { +inline theory::Assertion Theory::get() { Assert( !done(), "Theory::get() called with assertion queue empty!" ); // Get the assertion @@ -810,7 +806,9 @@ inline Assertion Theory::get() { return fact; } -}/* CVC4::theory namespace */ +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) { @@ -831,6 +829,7 @@ inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertSta return out; } +}/* CVC4::theory namespace */ }/* CVC4 namespace */ #endif /* __CVC4__THEORY__THEORY_H */ |