From: lianah <lianahady@gmail.com>
Date: Tue, 8 Oct 2013 20:50:28 +0000 (-0400)
Subject: fixed uf proof with holes bugs
X-Git-Tag: cvc5-1.0.0~7283
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3361081acd11178d0eb580ce91279a2ecaa7aa65;p=cvc5.git

fixed uf proof with holes bugs
---

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index caafa6b83..d73202147 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -41,33 +41,46 @@ void CnfProof::setTheoryProof(TheoryProof* theory_proof) {
   d_theoryProof = theory_proof; 
 }
 
-void CnfProof::addInputClause(ClauseId id, const ::Minisat::Clause& clause) {
-  d_inputClauses.insert(std::make_pair(id, clause)); 
-}
-
-void CnfProof::addTheoryLemma(ClauseId id, const ::Minisat::Clause& clause) {
-  d_theoryLemmas.insert(std::make_pair(id, clause)); 
+void CnfProof::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) {
+  for (unsigned i = 0; i < clause->size(); ++i) {
+    SatLiteral lit = clause->operator[](i); 
+    addVariable(lit.getSatVariable()); 
+  }
+  if (kind == INPUT) {
+    d_inputClauses.insert(std::make_pair(id, clause));
+    return;
+  }
+  Assert (kind == THEORY_LEMMA);
+  d_theoryLemmas.insert(std::make_pair(id, clause));
 }
 
-void CnfProof::addVariable(unsigned var) {
+void CnfProof::addVariable(prop::SatVariable var) {
   d_propVars.insert(var); 
-  Expr atom = getAtom(var);
+  Expr atom = getAtom(var); 
   getTheoryProof()->addAtom(atom); 
 }
 
-Expr CnfProof::getAtom(unsigned var) {
-  Minisat::Lit m_lit = Minisat::mkLit(var); 
-  prop::SatLiteral sat_lit = prop::MinisatSatSolver::toSatLiteral(m_lit); 
-  Expr atom = d_cnfStream->getNode(sat_lit).toExpr();
+Expr CnfProof::getAtom(prop::SatVariable var) {
+  prop::SatLiteral lit (var); 
+  Expr atom = d_cnfStream->getNode(lit).toExpr();
   return atom; 
 }
 
+CnfProof::~CnfProof() {
+  for (IdToClause::iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) {
+    delete it->second; 
+  }
+  for (IdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) {
+    delete it->second; 
+  }
+}
+
 void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) {
   for (VarSet::iterator it = d_propVars.begin();it != d_propVars.end();  ++it) {
     Expr atom = getAtom(*it);
     os << "(decl_atom ";
     getTheoryProof()->printFormula(atom, os);
-    os << " (\\ " << ProofManager::getVarPrefix() <<*it << " (\\ " << ProofManager::getAtomPrefix() <<*it << "\n";
+    os << " (\\ " << ProofManager::printVarName(*it) << " (\\ " << ProofManager::printAtomName(*it) << "\n";
     paren << ")))"; 
   }
 }
@@ -78,44 +91,44 @@ void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) {
 }
 
 void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
+  os << " ;; Input Clauses \n";  
   for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) {
     ClauseId id = it->first;
-    const Minisat::Clause& clause = it->second;
-    os << " ;; input clause \n";  
+    const prop::SatClause* clause = it->second;
     os << "(satlem _ _ ";
     std::ostringstream clause_paren; 
-    printClause(clause, os, clause_paren);
+    printClause(*clause, os, clause_paren);
     os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getInputClausePrefix() << id <<"\n"; 
+    os << "( \\ " << ProofManager::printInputClauseName(id) << "\n"; 
     paren << "))"; 
   }
 }
 
 
 void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) {
-  for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) {
+  os << " ;; Theory Lemmas \n";  
+  for (IdToClause::const_iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) {
     ClauseId id = it->first;
-    const Minisat::Clause& clause = it->second;
-    os << " ;; theory lemma \n";  
+    const prop::SatClause* clause = it->second;
     os << "(satlem _ _ ";
     std::ostringstream clause_paren; 
-    printClause(clause, os, clause_paren);
+    printClause(*clause, os, clause_paren);
     os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getLemmaClausePrefix() << id <<"\n"; 
+    os << "( \\ " << ProofManager::printLemmaClauseName(id) <<"\n"; 
     paren << "))"; 
   }
 }
 
-void LFSCCnfProof::printClause(const Minisat::Clause& clause, std::ostream& os, std::ostream& paren) {
-  for (int i = 0; i < clause.size(); ++i) {
-    Minisat::Lit lit = clause[i];
-    unsigned var = Minisat::var(lit);
-    if (sign(lit)) {
-      os << "(asf _ _ _ " << ProofManager::getAtomPrefix()<< var <<" (\\ " << ProofManager::getLitPrefix() << Minisat::toInt(lit) << " ";
-      paren << ")"; 
+void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren) {
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    prop::SatLiteral lit = clause[i];
+    prop::SatVariable var = lit.getSatVariable(); 
+    if (lit.isNegated()) {
+      os << "(ast _ _ _ " << ProofManager::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " ";
+      paren << "))"; 
     } else {
-      os << "(ast _ _ _ " << ProofManager::getAtomPrefix()<< var <<" (\\ " << ProofManager::getLitPrefix() << Minisat::toInt(lit) << " ";
-      paren << ")"; 
+      os << "(asf _ _ _ " << ProofManager::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " ";
+      paren << "))"; 
     }
   }
 }
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 8acb7a50f..010b1429d 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -32,8 +32,8 @@ namespace prop {
 class CnfStream;
 }
 
-typedef __gnu_cxx::hash_map < ClauseId, ::Minisat::Clause > IdToClause; 
-typedef __gnu_cxx::hash_set<unsigned > VarSet;
+typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; 
+typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet;
 
 class TheoryProof; 
   
@@ -46,22 +46,21 @@ protected:
   TheoryProof* d_theoryProof;
   TheoryProof* getTheoryProof();
 
-  Expr getAtom(unsigned var);
+  Expr getAtom(prop::SatVariable var);
 public:
   CnfProof(CVC4::prop::CnfStream* cnfStream);
-  void addInputClause(ClauseId id, const ::Minisat::Clause& clause);
-  void addTheoryLemma(ClauseId id, const ::Minisat::Clause& clause);
-  void addVariable(unsigned var); 
+  void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind);
+  void addVariable(prop::SatVariable var); 
   void setTheoryProof(TheoryProof* theory_proof);
   virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0;
   virtual void printClauses(std::ostream& os, std::ostream& paren) = 0;
-
+  virtual ~CnfProof(); 
 };
 
 class LFSCCnfProof: public CnfProof {
   void printInputClauses(std::ostream& os, std::ostream& paren);
   void printTheoryLemmas(std::ostream& os, std::ostream& paren);
-  void printClause(const Minisat::Clause& clause, std::ostream& os, std::ostream& paren);
+  void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren);
 public:
   LFSCCnfProof(CVC4::prop::CnfStream* cnfStream)
     : CnfProof(cnfStream)
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 7ca1a1e65..e1f85b93f 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -24,6 +24,13 @@
 
 namespace CVC4 {
 
+std::string append(const std::string& str, uint64_t num) {
+  std::ostringstream os;
+  os << str << num; 
+  return os.str(); 
+}
+
+
 bool          ProofManager::isInitialized = false;
 ProofManager* ProofManager::proofManager = NULL;
 
@@ -98,6 +105,15 @@ void ProofManager::initTheoryProof() {
   currentPM()->d_theoryProof = new LFSCTheoryProof();
 }
 
+
+std::string ProofManager::printInputClauseName(ClauseId id) {return append("pb", id); }
+std::string ProofManager::printLemmaClauseName(ClauseId id) { return append("lem", id); }
+std::string ProofManager::printLearntClauseName(ClauseId id) { return append("cl", id); }
+std::string ProofManager::printVarName(prop::SatVariable var) { return append("v", var); }
+std::string ProofManager::printAtomName(prop::SatVariable var) { return append("a", var); }
+std::string ProofManager::printLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); }
+
+
 LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
   : d_satProof(sat)
   , d_cnfProof(cnf)
@@ -119,7 +135,7 @@ void LFSCProof::toStream(std::ostream& out) {
   d_cnfProof->printAtomMapping(out, paren);
   d_cnfProof->printClauses(out, paren);
   d_satProof->printResolutions(out, paren); 
-  paren <<"))";
+  paren <<")))\n;;";
   out << paren.str(); 
 }
 
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 4ae8a6dae..d4f1d6528 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -25,6 +25,7 @@
 #include "proof/proof.h"
 #include "util/proof.h"
 
+
 // forward declarations
 namespace Minisat {
   class Solver;
@@ -35,6 +36,7 @@ namespace CVC4 {
 namespace prop {
   class CnfStream;
 }
+typedef int ClauseId;
 
 class Proof;
 class SatProof;
@@ -44,13 +46,20 @@ class TheoryProof;
 class LFSCSatProof;
 class LFSCCnfProof;
 class LFSCTheoryProof;
-  
+
+namespace prop {
+typedef uint64_t SatVariable;
+class SatLiteral;
+}
+
 // different proof modes
 enum ProofFormat {
   LFSC,
   NATIVE
 };/* enum ProofFormat */
 
+std::string append(const std::string& str, uint64_t num);
+
 class ProofManager {
   SatProof*   d_satProof;
   CnfProof*   d_cnfProof;
@@ -74,12 +83,13 @@ public:
   static TheoryProof* getTheoryProof();
 
   // variable prefixes
-  static std::string getInputClausePrefix() { return "pb"; }
-  static std::string getLemmaClausePrefix() { return "lem"; }
-  static std::string getLearntClausePrefix() { return "cl"; }
-  static std::string getVarPrefix() { return "v"; }
-  static std::string getAtomPrefix() { return "a"; }
-  static std::string getLitPrefix() {return "l"; }
+  static std::string printInputClauseName(ClauseId id);
+  static std::string printLemmaClauseName(ClauseId id);
+  static std::string printLearntClauseName(ClauseId id);
+
+  static std::string printVarName(prop::SatVariable var);
+  static std::string printAtomName(prop::SatVariable var);
+  static std::string printLitName(prop::SatLiteral lit);
 };/* class ProofManager */
 
 class LFSCProof : public Proof {
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index dc83e6aa3..e8c63bb74 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -19,10 +19,11 @@
 #include "proof/cnf_proof.h"
 #include "proof/proof_manager.h"
 #include "prop/minisat/core/Solver.h"
+#include "prop/minisat/minisat.h"
 
 using namespace std;
 using namespace Minisat;
-
+using namespace CVC4::prop;
 namespace CVC4 {
 
 /// some helper functions 
@@ -277,7 +278,7 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) {
   return d_unitId[toInt(lit)]; 
 }
 
-::Minisat::CRef SatProof::getClauseRef(ClauseId id) {
+Minisat::CRef SatProof::getClauseRef(ClauseId id) {
   if (d_idClause.find(id) == d_idClause.end()) {
     Debug("proof:sat") << "proof:getClauseRef cannot find clause "<<id<<" "
                        << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "")
@@ -290,7 +291,7 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) {
 Clause& SatProof::getClause(CRef ref) {
   return d_solver->ca[ref]; 
 }
-::Minisat::Lit SatProof::getUnit(ClauseId id) {
+Minisat::Lit SatProof::getUnit(ClauseId id) {
   Assert (d_idUnit.find(id) != d_idUnit.end());
   return d_idUnit[id]; 
 }
@@ -379,7 +380,7 @@ ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) {
        d_lemmaClauses.insert(newId); 
      }
    }
-   Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " << kind << "\n"; 
+   Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n"; 
    return d_clauseId[clause]; 
 }
 
@@ -575,7 +576,7 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
     Assert (d_storedUnitConflict); 
     conflict_id = d_unitConflictId; 
   } else {
-    Assert (!d_storedUnitConflict); 
+    Assert (!d_storedUnitConflict);
     conflict_id = registerClause(conflict_ref); //FIXME
   }
 
@@ -625,6 +626,12 @@ void SatProof::markDeleted(CRef clause) {
 }
 
 void SatProof::constructProof() {
+  // if (isLemmaClause(d_conflictId)) {
+  //   addClauseToCnfProof(d_emptyClauseId, THEORY_LEMMA);
+  // }
+  // if (isInputClause(d_emptyClauseId)) {
+  //   addClauseToCnfProof(d_emptyClauseId, INPUT); 
+  // }
   collectClauses(d_emptyClauseId); 
 }
 
@@ -643,18 +650,34 @@ void SatProof::constructProof() {
 std::string SatProof::clauseName(ClauseId id) {
   ostringstream os;
   if (isInputClause(id)) {
-    os << ProofManager::getInputClausePrefix()<<id;
+    os << ProofManager::printInputClauseName(id); 
     return os.str(); 
   } else 
   if (isLemmaClause(id)) {
-    os << ProofManager::getLemmaClausePrefix()<<id;
+    os << ProofManager::printLemmaClauseName(id); 
     return os.str(); 
   }else {
-    os << ProofManager::getLearntClausePrefix()<<id;
+    os << ProofManager::printLearntClauseName(id);
     return os.str(); 
   }
 }
 
+void SatProof::addClauseToCnfProof(ClauseId id, ClauseKind kind) {
+  if (isUnit(id)) {
+    Minisat::Lit lit = getUnit(id);
+    prop::SatLiteral sat_lit = MinisatSatSolver::toSatLiteral(lit);
+    prop::SatClause* clause = new SatClause();
+    clause->push_back(sat_lit); 
+    getCnfProof()->addClause(id, clause, kind); 
+    return; 
+  }
+  CRef ref = getClauseRef(id);
+  const Clause& minisat_cl = getClause(ref);
+  SatClause* clause = new SatClause();
+  MinisatSatSolver::toSatClause(minisat_cl, *clause);  
+  getCnfProof()->addClause(id, clause, kind); 
+}
+
 void SatProof::collectClauses(ClauseId id) {
   if (d_seenLearnt.find(id) != d_seenLearnt.end()) {
     return; 
@@ -667,17 +690,14 @@ void SatProof::collectClauses(ClauseId id) {
   }
 
   if (isInputClause(id)) {
-    CRef input_ref = getClauseRef(id);
-    const Clause& cl = getClause(input_ref);
-    getCnfProof()->addInputClause(id, cl); 
+    addClauseToCnfProof(id, INPUT); 
     d_seenInput.insert(id);
     return; 
   }
   else if (isLemmaClause(id)) {
-    CRef lemma_ref = getClauseRef(id);
-    const Clause& cl = getClause(lemma_ref);
-    getCnfProof()->addTheoryLemma(id, cl); 
-    d_seenLemmas.insert(id); 
+    addClauseToCnfProof(id, THEORY_LEMMA); 
+    d_seenLemmas.insert(id);
+    return; 
   } 
   else {
     d_seenLearnt.insert(id); 
@@ -716,7 +736,7 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream&
   out << clauseName(start_id) << " ";
   
   for(unsigned i = 0; i < steps.size(); i++) {
-    out << clauseName(steps[i].id) << " "<<ProofManager::getVarPrefix() << var(steps[i].lit) <<")"; 
+    out << clauseName(steps[i].id) << " "<<ProofManager::printVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")"; 
   }
   
   if (id == d_emptyClauseId) {
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 0ab86b554..5a1fa4680 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -36,7 +36,7 @@ namespace Minisat {
 
 #include "prop/minisat/core/SolverTypes.h"
 #include "util/proof.h"
-
+#include "prop/sat_solver_types.h"
 namespace std {
   using namespace __gnu_cxx;
 }/* std namespace */
@@ -89,7 +89,6 @@ typedef std::hash_map < ClauseId, ResChain*>      IdResMap;
 typedef std::hash_set < ClauseId >                IdHashSet;
 typedef std::vector   < ResChain* >               ResStack; 
 
-typedef std::hash_set < unsigned >                     VarSet; 
 typedef std::set < ClauseId >                     IdSet; 
 typedef std::vector < ::Minisat::Lit >              LitVector; 
 typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause;
@@ -255,6 +254,7 @@ protected:
   void collectClauses(ClauseId id);
   CnfProof* d_cnfProof; 
   CnfProof* getCnfProof();
+  void addClauseToCnfProof(ClauseId id, ClauseKind kind);
 public:
   void setCnfProof(CnfProof* cnfProof);
   virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0;
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 224c74e2c..948ced393 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -35,7 +35,9 @@ void TheoryProof::addDeclaration(Expr term) {
     d_sortDeclarations.insert(type);
   if (term.getKind() == kind::APPLY_UF) {
     Expr function = term.getOperator();
-    d_termDeclarations.insert(function); 
+    d_termDeclarations.insert(function);
+    Assert (term.getNumChildren() == 1);
+    addDeclaration(term[0]); 
   } else {
     Assert (term.isVariable()); 
     Assert (type.isSort()); 
@@ -48,10 +50,8 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) {
     os << term; 
     return;
   }
-  Assert (term.getKind() == kind::APPLY_UF);
+  Assert (term.getKind() == kind::APPLY_UF && term.getNumChildren() == 1);
   Expr func = term.getOperator();
-  // only support unary functions so far
-  Assert (func.getNumChildren() == 1); 
   os << "(apply _ _ " << func << " ";
   printTerm(term[0], os);
   os <<")"; 
@@ -61,6 +61,7 @@ void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) {
   // should make this more general 
   Assert (atom.getKind() == kind::EQUAL);
   os << "(= ";
+  os << atom[0].getType() <<" "; 
   printTerm(atom[0], os);
   os << " ";
   printTerm(atom[1], os);
@@ -70,7 +71,7 @@ void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) {
 void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) {
   // declaring the sorts
   for (SortSet::const_iterator it = d_sortDeclarations.begin(); it != d_sortDeclarations.end(); ++it) {
-    os << "(% " << *it << "sort \n";
+    os << "(% " << *it << " sort \n";
     paren << ")"; 
   }
 
@@ -78,13 +79,13 @@ void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) {
   for (TermSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) {
     Expr term = *it;
     
-    os << "(% " << term << "(term "; 
+    os << "(% " << term << " (term "; 
     paren <<")"; 
 
     Type type = term.getType();
     if (type.isFunction()) {
       FunctionType ftype = (FunctionType)type; 
-      Assert (ftype.getArity() == 2);
+      Assert (ftype.getArity() == 1);
       Type arg_type = ftype.getArgTypes()[0];
       Type result_type = ftype.getRangeType();
       os << "(arrow " << arg_type << " " << result_type << "))\n"; 
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 960f2ad62..98e43aaf0 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -103,6 +103,13 @@ void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
   Assert((unsigned)clause.size() == sat_clause.size());
 }
 
+void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
+                                       SatClause& sat_clause) {
+  for (int i = 0; i < clause.size(); ++i) {
+    sat_clause.push_back(toSatLiteral(clause[i]));
+  }
+  Assert((unsigned)clause.size() == sat_clause.size());
+}
 
 void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy)
 {
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index ec49b5f71..27258b3c2 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -51,7 +51,7 @@ public:
 
   static void  toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
   static void  toSatClause    (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause);
-
+  static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
   void initialize(context::Context* context, TheoryProxy* theoryProxy);
 
   void addClause(SatClause& clause, bool removable);
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index ab2bcda47..8fee0d11e 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -135,6 +135,10 @@ public:
     return (size_t)d_value;
   }
 
+  uint64_t toInt() const {
+    return d_value; 
+  }
+  
   /**
    * Returns true if the literal is undefined.
    */