diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:45:45 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-25 20:45:45 +0000 |
commit | 70c23e23c3bfc8aa3fdf285fc643b0438359d22a (patch) | |
tree | 3f8f1797e0f8dd3d977f983c1ab823c682f51551 /src/prop/theory_proxy.h | |
parent | 0d080430206880ffc19050acfa01aae1475f1978 (diff) |
moving minisat implementation into their respective directories (regular and bv)
Diffstat (limited to 'src/prop/theory_proxy.h')
-rw-r--r-- | src/prop/theory_proxy.h | 35 |
1 files changed, 0 insertions, 35 deletions
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 2934bcad9..8b585710f 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -123,41 +123,6 @@ inline TheoryProxy::TheoryProxy(PropEngine* propEngine, }/* CVC4::prop namespace */ -inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { - out << lit.toString(); - return out; -} - -inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& clause) { - out << "clause:"; - for(unsigned i = 0; i < clause.size(); ++i) { - out << " " << clause[i]; - } - out << ";"; - return out; -} - -inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) { - std::string str; - switch(val) { - case prop::SatValUnknown: - str = "_"; - break; - case prop::SatValTrue: - str = "1"; - break; - case prop::SatValFalse: - str = "0"; - break; - default: - str = "Error"; - break; - } - - out << str; - return out; -} - }/* CVC4 namespace */ #endif /* __CVC4__PROP__SAT_H */ |