diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-02-07 15:00:41 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-07 15:00:41 -0800 |
commit | 7d325a44dcfce54dd9195b7ee49fb93a1aed3a06 (patch) | |
tree | 4701b7f24cb8a9a696b99242c23668b17c819236 /src/prop/cryptominisat.h | |
parent | b661071c238ea32e72ee6bddbff65f38328dd345 (diff) |
Cleanup Cryptominisat header. (#1561)
Clang formatted sat_solver_factor.cpp
Diffstat (limited to 'src/prop/cryptominisat.h')
-rw-r--r-- | src/prop/cryptominisat.h | 45 |
1 files changed, 3 insertions, 42 deletions
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index bb2f47783..fca2c7aa1 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -87,46 +87,7 @@ public: Statistics d_statistics; }; -} // CVC4::prop -} // CVC4 -#else // CVC4_USE_CRYPTOMINISAT - -namespace CVC4 { -namespace prop { - -class CryptoMinisatSolver : public SatSolver { - -public: - CryptoMinisatSolver(StatisticsRegistry* registry, - const std::string& name = "") { Unreachable(); } - /** Assert a clause in the solver. */ - ClauseId addClause(SatClause& clause, bool removable) { - Unreachable(); - } - - /** Return true if the solver supports native xor resoning */ - bool nativeXor() { Unreachable(); } - - /** Add a clause corresponding to rhs = l1 xor .. xor ln */ - ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { - Unreachable(); - } - - SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase) { Unreachable(); } - SatVariable trueVar() { Unreachable(); } - SatVariable falseVar() { Unreachable(); } - SatValue solve() { Unreachable(); } - SatValue solve(long unsigned int&) { Unreachable(); } - void interrupt() { Unreachable(); } - SatValue value(SatLiteral l) { Unreachable(); } - SatValue modelValue(SatLiteral l) { Unreachable(); } - unsigned getAssertionLevel() const { Unreachable(); } - bool ok() const { return false;}; - - -};/* class CryptoMinisatSolver */ -} // CVC4::prop -} // CVC4 - -#endif // CVC4_USE_CRYPTOMINISAT +} // namespace prop +} // namespace CVC4 +#endif // CVC4_USE_CRYPTOMINISAT |