From 1ed3b1803bd0a25c56a62d290cd5dcb64c5085ce Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Mon, 26 Mar 2012 14:22:38 +0000 Subject: [PATCH] More cleaning up. --- src/prop/Makefile.am | 5 +- src/prop/bvminisat/bvminisat.cpp | 32 +++---- src/prop/bvminisat/bvminisat.h | 14 +-- src/prop/minisat/minisat.cpp | 24 ++--- src/prop/minisat/minisat.h | 12 +-- src/prop/prop_engine.cpp | 29 +++--- src/prop/sat_solver.cpp | 51 ----------- src/prop/sat_solver.h | 145 ++++++++++++++++++++++-------- src/prop/sat_solver_factory.cpp | 36 ++++++++ src/prop/sat_solver_factory.h | 38 ++++++++ src/theory/bv/bv_sat.cpp | 3 +- test/unit/prop/cnf_stream_black.h | 16 ++-- 12 files changed, 252 insertions(+), 153 deletions(-) delete mode 100644 src/prop/sat_solver.cpp create mode 100644 src/prop/sat_solver_factory.cpp create mode 100644 src/prop/sat_solver_factory.h diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 832255621..c1dc3b828 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -16,7 +16,8 @@ libprop_la_SOURCES = \ cnf_stream.h \ cnf_stream.cpp \ sat_solver.h \ - sat_solver.cpp - + sat_solver_factory.h \ + sat_solver_factory.cpp + SUBDIRS = minisat bvminisat diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 3d2d4c9ea..c4c21e126 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -54,11 +54,11 @@ void MinisatSatSolver::interrupt(){ d_minisat->interrupt(); } -SatLiteralValue MinisatSatSolver::solve(){ +SatValue MinisatSatSolver::solve(){ return toSatLiteralValue(d_minisat->solve()); } -SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){ +SatValue MinisatSatSolver::solve(long unsigned int& resource){ Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; if(resource == 0) { d_minisat->budgetOff(); @@ -67,14 +67,14 @@ SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){ } BVMinisat::vec empty; unsigned long conflictsBefore = d_minisat->conflicts; - SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); + SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); d_minisat->clearInterrupt(); resource = d_minisat->conflicts - conflictsBefore; Trace("limit") << " & assumptions){ +SatValue MinisatSatSolver::solve(const context::CDList & assumptions){ Debug("sat::minisat") << "Solve with assumptions "; context::CDList::const_iterator it = assumptions.begin(); BVMinisat::vec assump; @@ -85,7 +85,7 @@ SatLiteralValue MinisatSatSolver::solve(const context::CDList & assu } Debug("sat::minisat") <<"\n"; - SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); + SatValue result = toSatLiteralValue(d_minisat->solve(assump)); return result; } @@ -97,14 +97,14 @@ void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) { } } -SatLiteralValue MinisatSatSolver::value(SatLiteral l){ +SatValue MinisatSatSolver::value(SatLiteral l){ Unimplemented(); - return SatValUnknown; + return SAT_VALUE_UNKNOWN; } -SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){ +SatValue MinisatSatSolver::modelValue(SatLiteral l){ Unimplemented(); - return SatValUnknown; + return SAT_VALUE_UNKNOWN; } void MinisatSatSolver::unregisterVar(SatLiteral lit) { @@ -150,16 +150,16 @@ SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) { BVMinisat::sign(lit)); } -SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) { - if(res) return SatValTrue; - else return SatValFalse; +SatValue MinisatSatSolver::toSatLiteralValue(bool res) { + if(res) return SAT_VALUE_TRUE; + else return SAT_VALUE_FALSE; } -SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) { - if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue; - if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown; +SatValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) { + if(res == (BVMinisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE; + if(res == (BVMinisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN; Assert(res == (BVMinisat::lbool((uint8_t)1))); - return SatValFalse; + return SAT_VALUE_FALSE; } void MinisatSatSolver::toMinisatClause(SatClause& clause, diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index ed164904e..043aa5d24 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -38,13 +38,13 @@ public: void interrupt(); - SatLiteralValue solve(); - SatLiteralValue solve(long unsigned int&); - SatLiteralValue solve(const context::CDList & assumptions); + SatValue solve(); + SatValue solve(long unsigned int&); + SatValue solve(const context::CDList & assumptions); void getUnsatCore(SatClause& unsatCore); - SatLiteralValue value(SatLiteral l); - SatLiteralValue modelValue(SatLiteral l); + SatValue value(SatLiteral l); + SatValue modelValue(SatLiteral l); void unregisterVar(SatLiteral lit); void renewVar(SatLiteral lit, int level = -1); @@ -56,8 +56,8 @@ public: static SatVariable toSatVariable(BVMinisat::Var var); static BVMinisat::Lit toMinisatLit(SatLiteral lit); static SatLiteral toSatLiteral(BVMinisat::Lit lit); - static SatLiteralValue toSatLiteralValue(bool res); - static SatLiteralValue toSatLiteralValue(BVMinisat::lbool res); + static SatValue toSatLiteralValue(bool res); + static SatValue toSatLiteralValue(BVMinisat::lbool res); static void toMinisatClause(SatClause& clause, BVMinisat::vec& minisat_clause); static void toSatClause (BVMinisat::vec& clause, SatClause& sat_clause); diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index ede18c585..1ec81a4f6 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -57,16 +57,16 @@ SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) { Minisat::sign(lit)); } -SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) { - if(res) return SatValTrue; - else return SatValFalse; +SatValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) { + if(res) return SAT_VALUE_TRUE; + else return SAT_VALUE_FALSE; } -SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { - if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue; - if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown; +SatValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { + if(res == (Minisat::lbool((uint8_t)0))) return SAT_VALUE_TRUE; + if(res == (Minisat::lbool((uint8_t)2))) return SAT_VALUE_UNKNOWN; Assert(res == (Minisat::lbool((uint8_t)1))); - return SatValFalse; + return SAT_VALUE_FALSE; } @@ -121,7 +121,7 @@ SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) { } -SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) { +SatValue DPLLMinisatSatSolver::solve(unsigned long& resource) { Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; if(resource == 0) { d_minisat->budgetOff(); @@ -130,14 +130,14 @@ SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) { } Minisat::vec empty; unsigned long conflictsBefore = d_minisat->conflicts; - SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); + SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); d_minisat->clearInterrupt(); resource = d_minisat->conflicts - conflictsBefore; Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl; return result; } -SatLiteralValue DPLLMinisatSatSolver::solve() { +SatValue DPLLMinisatSatSolver::solve() { d_minisat->budgetOff(); return toSatLiteralValue(d_minisat->solve()); } @@ -147,11 +147,11 @@ void DPLLMinisatSatSolver::interrupt() { d_minisat->interrupt(); } -SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) { +SatValue DPLLMinisatSatSolver::value(SatLiteral l) { return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); } -SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){ +SatValue DPLLMinisatSatSolver::modelValue(SatLiteral l){ return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); } diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index dc06753ab..549c0b679 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -44,8 +44,8 @@ public: static SatVariable toSatVariable(Minisat::Var var); static Minisat::Lit toMinisatLit(SatLiteral lit); static SatLiteral toSatLiteral(Minisat::Lit lit); - static SatLiteralValue toSatLiteralValue(bool res); - static SatLiteralValue toSatLiteralValue(Minisat::lbool res); + static SatValue toSatLiteralValue(bool res); + static SatValue toSatLiteralValue(Minisat::lbool res); static void toMinisatClause(SatClause& clause, Minisat::vec& minisat_clause); static void toSatClause (Minisat::vec& clause, SatClause& sat_clause); @@ -56,14 +56,14 @@ public: SatVariable newVar(bool theoryAtom = false); - SatLiteralValue solve(); - SatLiteralValue solve(long unsigned int&); + SatValue solve(); + SatValue solve(long unsigned int&); void interrupt(); - SatLiteralValue value(SatLiteral l); + SatValue value(SatLiteral l); - SatLiteralValue modelValue(SatLiteral l); + SatValue modelValue(SatLiteral l); bool properExplanation(SatLiteral lit, SatLiteral expl) const; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 0fa13dc04..7d4cb7b1c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -20,6 +20,7 @@ #include "prop/prop_engine.h" #include "prop/theory_proxy.h" #include "prop/sat_solver.h" +#include "prop/sat_solver_factory.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" @@ -121,7 +122,7 @@ void PropEngine::printSatisfyingAssignment(){ SatLiteral l = curr.second.literal; if(!l.isNegated()) { Node n = curr.first; - SatLiteralValue value = d_satSolver->modelValue(l); + SatValue value = d_satSolver->modelValue(l); Debug("prop-value") << "'" << l << "' " << value << " " << n << endl; } } @@ -150,26 +151,26 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) { d_interrupted = false; // Check the problem - SatLiteralValue result = d_satSolver->solve(resource); + SatValue result = d_satSolver->solve(resource); millis = d_satTimer.elapsed(); - if( result == SatValUnknown ) { + if( result == SAT_VALUE_UNKNOWN ) { Result::UnknownExplanation why = d_satTimer.expired() ? Result::TIMEOUT : (d_interrupted ? Result::INTERRUPTED : Result::RESOURCEOUT); return Result(Result::SAT_UNKNOWN, why); } - if( result == SatValTrue && Debug.isOn("prop") ) { + if( result == SAT_VALUE_TRUE && Debug.isOn("prop") ) { printSatisfyingAssignment(); } Debug("prop") << "PropEngine::checkSat() => " << result << endl; - if(result == SatValTrue && d_theoryEngine->isIncomplete()) { + if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) { return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE); } - return Result(result == SatValTrue ? Result::SAT : Result::UNSAT); + return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT); } Node PropEngine::getValue(TNode node) const { @@ -178,13 +179,13 @@ Node PropEngine::getValue(TNode node) const { SatLiteral lit = d_cnfStream->getLiteral(node); - SatLiteralValue v = d_satSolver->value(lit); - if(v == SatValTrue) { + SatValue v = d_satSolver->value(lit); + if(v == SAT_VALUE_TRUE) { return NodeManager::currentNM()->mkConst(true); - } else if(v == SatValFalse) { + } else if(v == SAT_VALUE_FALSE) { return NodeManager::currentNM()->mkConst(false); } else { - Assert(v == SatValUnknown); + Assert(v == SAT_VALUE_UNKNOWN); return Node::null(); } } @@ -203,15 +204,15 @@ bool PropEngine::hasValue(TNode node, bool& value) const { SatLiteral lit = d_cnfStream->getLiteral(node); - SatLiteralValue v = d_satSolver->value(lit); - if(v == SatValTrue) { + SatValue v = d_satSolver->value(lit); + if(v == SAT_VALUE_TRUE) { value = true; return true; - } else if(v == SatValFalse) { + } else if(v == SAT_VALUE_FALSE) { value = false; return true; } else { - Assert(v == SatValUnknown); + Assert(v == SAT_VALUE_UNKNOWN); return false; } } diff --git a/src/prop/sat_solver.cpp b/src/prop/sat_solver.cpp deleted file mode 100644 index d3710b617..000000000 --- a/src/prop/sat_solver.cpp +++ /dev/null @@ -1,51 +0,0 @@ -/********************* */ -/*! \file sat.cpp - ** \verbatim - ** Original author: cconway - ** Major contributors: dejan, taking, mdeters, lianah - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "prop/prop_engine.h" -#include "prop/sat_solver.h" -#include "context/context.h" -#include "theory/theory_engine.h" -#include "expr/expr_stream.h" -#include "prop/theory_proxy.h" - -#include "prop/minisat/minisat.h" -#include "prop/bvminisat/bvminisat.h" - -using namespace std; - -namespace CVC4 { -namespace prop { - -string SatLiteral::toString() { - ostringstream os; - os << (isNegated()? "~" : "") << getSatVariable() << " "; - return os.str(); -} - -BVSatSolverInterface* SatSolverFactory::createMinisat() { - return new MinisatSatSolver(); -} - -DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat(){ - return new DPLLMinisatSatSolver(); -} - - -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index e54f551fa..eb694852c 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -16,7 +16,7 @@ ** SAT Solver. **/ -#include "cvc4_private.h" +#include "cvc4_public.h" #ifndef __CVC4__PROP__SAT_MODULE_H #define __CVC4__PROP__SAT_MODULE_H @@ -31,55 +31,134 @@ namespace prop { class TheoryProxy; -enum SatLiteralValue { - SatValUnknown, - SatValTrue, - SatValFalse +/** + * Boolean values of the SAT solver. + */ +enum SatValue { + SAT_VALUE_UNKNOWN, + SAT_VALUE_TRUE, + SAT_VALUE_FALSE }; +/** + * A variable of the SAT solver. + */ typedef uint64_t SatVariable; -// special constant + +/** + * Undefined SAT solver variable. + */ const SatVariable undefSatVariable = SatVariable(-1); +/** + * A SAT literal is a variable or an negated variable. + */ class SatLiteral { + + /** + * The value holds the variable and a bit noting if the variable is negated. + */ uint64_t d_value; + public: - SatLiteral() : - d_value(undefSatVariable) + + /** + * Construct an undefined SAT literal. + */ + SatLiteral() + : d_value(undefSatVariable) {} - SatLiteral(SatVariable var, bool negated = false) { d_value = var + var + (int)negated; } - SatLiteral operator~() { + /** + * Construct a literal given a possible negated variable. + */ + SatLiteral(SatVariable var, bool negated = false) { + d_value = var + var + (int)negated; + } + + /** + * Returns the variable of the literal. + */ + SatVariable getSatVariable() const { + return d_value >> 1; + } + + /** + * Returns true if the literal is a negated variable. + */ + bool isNegated() const { + return d_value & 1; + } + + /** + * Negate the given literal. + */ + SatLiteral operator ~ () const { return SatLiteral(getSatVariable(), !isNegated()); } - bool operator==(const SatLiteral& other) const { + + /** + * Compare two literals for equality. + */ + bool operator == (const SatLiteral& other) const { return d_value == other.d_value; } - bool operator!=(const SatLiteral& other) const { + + /** + * Compare two literals for dis-equality. + */ + bool operator != (const SatLiteral& other) const { return !(*this == other); } - std::string toString(); - bool isNegated() const { return d_value & 1; } - size_t toHash() const {return (size_t)d_value; } - bool isNull() const { return d_value == (uint64_t)-1; } - SatVariable getSatVariable() const {return d_value >> 1; } + + /** + * Returns a string representation of the literal. + */ + std::string toString() const { + std::ostringstream os; + os << (isNegated()? "~" : "") << getSatVariable() << " "; + return os.str(); + } + + /** + * Returns the hash value of a literal. + */ + size_t hash() const { + return (size_t)d_value; + } + + /** + * Returns true if the literal is undefined. + */ + bool isNull() const { + return getSatVariable() == undefSatVariable; + } }; -// special constant +/** + * A constant representing a undefined literal. + */ const SatLiteral undefSatLiteral = SatLiteral(undefSatVariable); - +/** + * Helper for hashing the literals. + */ struct SatLiteralHashFunction { inline size_t operator() (const SatLiteral& literal) const { - return literal.toHash(); + return literal.hash(); } }; +/** + * A SAT clause is a vector of literals. + */ typedef std::vector SatClause; class SatSolver { + public: - /** Virtual destructor to make g++ happy */ + + /** Virtual destructor */ virtual ~SatSolver() { } /** Assert a clause in the solver. */ @@ -90,19 +169,19 @@ public: /** Check the satisfiability of the added clauses */ - virtual SatLiteralValue solve() = 0; + virtual SatValue solve() = 0; /** Check the satisfiability of the added clauses */ - virtual SatLiteralValue solve(long unsigned int&) = 0; + virtual SatValue solve(long unsigned int&) = 0; /** Interrupt the solver */ virtual void interrupt() = 0; /** Call value() during the search.*/ - virtual SatLiteralValue value(SatLiteral l) = 0; + virtual SatValue value(SatLiteral l) = 0; /** Call modelValue() when the search is done.*/ - virtual SatLiteralValue modelValue(SatLiteral l) = 0; + virtual SatValue modelValue(SatLiteral l) = 0; virtual void unregisterVar(SatLiteral lit) = 0; @@ -115,7 +194,7 @@ public: class BVSatSolverInterface: public SatSolver { public: - virtual SatLiteralValue solve(const context::CDList & assumptions) = 0; + virtual SatValue solve(const context::CDList & assumptions) = 0; virtual void markUnremovable(SatLiteral lit) = 0; @@ -135,12 +214,6 @@ public: }; -class SatSolverFactory { -public: - static BVSatSolverInterface* createMinisat(); - static DPLLSatSolverInterface* createDPLLMinisat(); -}; - }/* prop namespace */ inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { @@ -157,16 +230,16 @@ inline std::ostream& operator <<(std::ostream& out, const prop::SatClause& claus return out; } -inline std::ostream& operator <<(std::ostream& out, prop::SatLiteralValue val) { +inline std::ostream& operator <<(std::ostream& out, prop::SatValue val) { std::string str; switch(val) { - case prop::SatValUnknown: + case prop::SAT_VALUE_UNKNOWN: str = "_"; break; - case prop::SatValTrue: + case prop::SAT_VALUE_TRUE: str = "1"; break; - case prop::SatValFalse: + case prop::SAT_VALUE_FALSE: str = "0"; break; default: diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp new file mode 100644 index 000000000..fbb244789 --- /dev/null +++ b/src/prop/sat_solver_factory.cpp @@ -0,0 +1,36 @@ +/********************* */ +/*! \file sat_solver_factory.h + ** \verbatim + ** Original author: lianah + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver creation facility. + ** + ** SAT Solver. + **/ + +#include "prop/sat_solver_factory.h" +#include "prop/minisat/minisat.h" +#include "prop/bvminisat/bvminisat.h" + +using namespace CVC4; +using namespace prop; + +BVSatSolverInterface* SatSolverFactory::createMinisat() { + return new MinisatSatSolver(); +} + +DPLLSatSolverInterface* SatSolverFactory::createDPLLMinisat() { + return new DPLLMinisatSatSolver(); +} + + + + diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h new file mode 100644 index 000000000..09d66b8d4 --- /dev/null +++ b/src/prop/sat_solver_factory.h @@ -0,0 +1,38 @@ +/********************* */ +/*! \file sat_solver_factory.h + ** \verbatim + ** Original author: dejan + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief SAT Solver. + ** + ** SAT Solver creation facility + **/ + +#pragma once + +#include "cvc4_public.h" + +#include "prop/sat_solver.h" + +namespace CVC4 { +namespace prop { + +class SatSolverFactory { +public: + static BVSatSolverInterface* createMinisat(); + static DPLLSatSolverInterface* createDPLLMinisat(); +}; + +} +} + + + diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp index f580aee44..6f91335ce 100644 --- a/src/theory/bv/bv_sat.cpp +++ b/src/theory/bv/bv_sat.cpp @@ -22,6 +22,7 @@ #include "theory/rewriter.h" #include "prop/cnf_stream.h" #include "prop/sat_solver.h" +#include "prop/sat_solver_factory.h" using namespace std; @@ -184,7 +185,7 @@ void Bitblaster::assertToSat(TNode lit) { bool Bitblaster::solve() { Trace("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; - return SatValTrue == d_satSolver->solve(d_assertedAtoms); + return SAT_VALUE_TRUE == d_satSolver->solve(d_assertedAtoms); } void Bitblaster::getConflict(std::vector& conflict) { diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h index d1f79f6ab..5c20b534d 100644 --- a/test/unit/prop/cnf_stream_black.h +++ b/test/unit/prop/cnf_stream_black.h @@ -84,20 +84,20 @@ public: void interrupt() { } - SatLiteralValue solve() { - return SatValUnknown; + SatValue solve() { + return SAT_VALUE_UNKNOWN; } - SatLiteralValue solve(long unsigned int& resource) { - return SatValUnknown; + SatValue solve(long unsigned int& resource) { + return SAT_VALUE_UNKNOWN; } - SatLiteralValue value(SatLiteral l) { - return SatValUnknown; + SatValue value(SatLiteral l) { + return SAT_VALUE_UNKNOWN; } - SatLiteralValue modelValue(SatLiteral l) { - return SatValUnknown; + SatValue modelValue(SatLiteral l) { + return SAT_VALUE_UNKNOWN; } bool properExplanation(SatLiteral lit, SatLiteral expl) const { -- 2.30.2