diff options
Diffstat (limited to 'src/prop/sat_solver.h')
| -rw-r--r-- | src/prop/sat_solver.h | 12 |
1 files changed, 2 insertions, 10 deletions
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index d4b08ab71..1526e91b9 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -33,11 +33,6 @@ namespace CVC4 { -namespace proof { -class ClausalBitVectorProof; -class ResolutionBitVectorProof; -} // namespace proof - namespace prop { class TheoryProxy; @@ -58,7 +53,7 @@ public: /** Add a clause corresponding to rhs = l1 xor .. xor ln */ virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0; - + /** * Create a new boolean variable in the solver. * @param isTheoryAtom is this a theory atom that needs to be asserted to theory @@ -84,6 +79,7 @@ public: virtual SatValue solve(const std::vector<SatLiteral>& assumptions) { Unimplemented() << "Solving under assumptions not implemented"; + return SAT_VALUE_UNKNOWN; }; /** Interrupt the solver */ @@ -101,10 +97,6 @@ public: /** Check if the solver is in an inconsistent state */ virtual bool ok() const = 0; - virtual void setResolutionProofLog(proof::ResolutionBitVectorProof* bvp) {} - - virtual void setClausalProofLog(proof::ClausalBitVectorProof* drat_proof) {} - };/* class SatSolver */ |