From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Sun, 15 Aug 2010 21:35:42 +0000 (+0000)
Subject: (no commit message)
X-Git-Tag: cvc5-1.0.0~8891
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5e857e4329c7e02b236a466e49009cfac0fa1d4a;p=cvc5.git

---

diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index dbd32c062..2cdba2d27 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -1,7 +1,9 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+	-D __STDC_LIMIT_MACROS \
+	-D __STDC_FORMAT_MACROS \
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -I@srcdir@/minisat
+AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libprop.la
 
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index e95322348..5d88a9240 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -84,7 +84,7 @@ void CnfStream::cacheTranslation(TNode node, SatLiteral lit) {
 }
 
 SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
-  SatLiteral lit = SatLiteral(d_satSolver->newVar(theoryLiteral));
+  SatLiteral lit = Minisat::mkLit(d_satSolver->newVar(theoryLiteral));
   cacheTranslation(node, lit);
   if (theoryLiteral) {
     d_nodeCache[lit] = node;
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 2e74a954c..8581cd9a0 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -51,37 +51,37 @@ class CnfStream;
 #ifdef __CVC4_USE_MINISAT
 
 /** Type of the SAT variables */
-typedef minisat::Var SatVariable;
+typedef Minisat::Var SatVariable;
 
 /** Type of the Sat literals */
-typedef minisat::Lit SatLiteral;
+typedef Minisat::Lit SatLiteral;
 
 /** Type of the SAT clauses */
-typedef minisat::vec<SatLiteral> SatClause;
+typedef Minisat::vec<SatLiteral> SatClause;
 
-typedef minisat::lbool SatLiteralValue;
+typedef Minisat::lbool SatLiteralValue;
 
 /**
  * Returns the variable of the literal.
  * @param lit the literal
  */
 inline SatVariable literalToVariable(SatLiteral lit) {
-  return minisat::var(lit);
+  return Minisat::var(lit);
 }
 
 inline bool literalSign(SatLiteral lit) {
-  return minisat::sign(lit);
+  return Minisat::sign(lit);
 }
 
 static inline size_t
 hashSatLiteral(const SatLiteral& literal) {
-  return (size_t) minisat::toInt(literal);
+  return (size_t) Minisat::toInt(literal);
 }
 
 inline std::string stringOfLiteralValue(SatLiteralValue val) {
-  if( val == minisat::l_False ) {
+  if( val == l_False ) {
     return "0";
-  } else if (val == minisat::l_True ) {
+  } else if (val == l_True ) {
     return "1";
   } else { // unknown
     return "_";
@@ -134,7 +134,7 @@ class SatSolver : public SatInputInterface {
 #ifdef __CVC4_USE_MINISAT
 
   /** Minisat solver */
-  minisat::SimpSolver* d_minisat;
+  Minisat::SimpSolver* d_minisat;
 
   class Statistics {
   private:
@@ -165,7 +165,7 @@ class SatSolver : public SatInputInterface {
       StatisticsRegistry::registerStat(&d_statMaxLiterals);
       StatisticsRegistry::registerStat(&d_statTotLiterals);
     }
-    void init(minisat::SimpSolver* d_minisat){
+    void init(Minisat::SimpSolver* d_minisat){
       d_statStarts.setData(d_minisat->starts);
       d_statDecisions.setData(d_minisat->decisions);
       d_statRndDecisions.setData(d_minisat->rnd_decisions);
@@ -230,13 +230,11 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   d_statistics()
 {
   // Create the solver
-  d_minisat = new minisat::SimpSolver(this, d_context);
+  d_minisat = new Minisat::SimpSolver(this, d_context);
   // Setup the verbosity
   d_minisat->verbosity = (options->verbosity > 0) ? 1 : -1;
   // Do not delete the satisfied clauses, just the learnt ones
   d_minisat->remove_satisfied = false;
-  // Make minisat reuse the literal values
-  d_minisat->polarity_mode = minisat::SimpSolver::polarity_user;
 
   // No random choices
   if(Debug.isOn("no_rnd_decisions")){
@@ -255,7 +253,7 @@ inline bool SatSolver::solve() {
 }
 
 inline void SatSolver::addClause(SatClause& clause, bool lemma) {
-  d_minisat->addClause(clause, lemma ? minisat::Solver::CLAUSE_LEMMA : minisat::Solver::CLAUSE_PROBLEM);
+  d_minisat->addClause(clause, lemma ? Minisat::Solver::CLAUSE_LEMMA : Minisat::Solver::CLAUSE_PROBLEM);
 }
 
 inline SatVariable SatSolver::newVar(bool theoryAtom) {