fixed proof regression script and added a new uf test case

5 files changed, 42 insertions, 14 deletions

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index cb22ca819..8e9c4cd21 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -33,7 +33,8 @@ CnfProof::CnfProof(CnfStream* stream)
 
 Expr CnfProof::getAtom(prop::SatVariable var) {
   prop::SatLiteral lit (var); 
-  Expr atom = d_cnfStream->getNode(lit).toExpr();
+  Node node = d_cnfStream->getNode(lit); 
+  Expr atom = node.toExpr();
   return atom; 
 }
 
@@ -45,9 +46,16 @@ void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) {
   ProofManager::var_iterator end = ProofManager::currentPM()->end_vars();
   
   for (;it != end;  ++it) {
-    Expr atom = getAtom(*it);
     os << "(decl_atom ";
-    LFSCTheoryProof::printFormula(atom, os);
+    
+    if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) {
+      Expr atom = getAtom(*it);
+      LFSCTheoryProof::printFormula(atom, os);
+    } else {
+      // print fake atoms for all other logics
+      os << "true "; 
+    }
+
     os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n";
     paren << ")))"; 
   }
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 23ba0e4e7..110e6b79a 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -21,6 +21,8 @@
 #include "proof/cnf_proof.h"
 #include "proof/theory_proof.h"
 #include "util/cvc4_assert.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
 
 namespace CVC4 {
 
@@ -68,12 +70,13 @@ ProofManager* ProofManager::currentPM() {
   }
 }
 
-Proof* ProofManager::getProof() {
+Proof* ProofManager::getProof(SmtEngine* smt) {
   if (currentPM()->d_fullProof != NULL)
     return currentPM()->d_fullProof;
   Assert (currentPM()->d_format == LFSC);
 
-  currentPM()->d_fullProof = new LFSCProof((LFSCSatProof*)getSatProof(),
+  currentPM()->d_fullProof = new LFSCProof(smt,
+                                           (LFSCSatProof*)getSatProof(),
                                            (LFSCCnfProof*)getCnfProof(),
                                            (LFSCTheoryProof*)getTheoryProof()); 
   return currentPM()->d_fullProof;
@@ -138,19 +141,27 @@ void ProofManager::addAssertion(Expr formula) {
   d_inputFormulas.insert(formula); 
 }
 
+void ProofManager::setLogic(const std::string& logic_string) {
+  d_logic = logic_string; 
+}
+
 
-LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
+LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
   : d_satProof(sat)
   , d_cnfProof(cnf)
   , d_theoryProof(theory)
+  , d_smtEngine(smtEngine)
 {
   d_satProof->constructProof();
 }
 
 void LFSCProof::toStream(std::ostream& out) {
+  smt::SmtScope scope(d_smtEngine);
   std::ostringstream paren;
   out << "(check \n";
-  d_theoryProof->printAssertions(out, paren); 
+  if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) {
+    d_theoryProof->printAssertions(out, paren);
+  }
   out << "(: (holds cln) \n";
   d_cnfProof->printAtomMapping(out, paren);
   d_cnfProof->printClauses(out, paren);
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 7642ba776..82a1bd6be 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -36,6 +36,9 @@ namespace CVC4 {
 namespace prop {
   class CnfStream;
 }
+
+class SmtEngine; 
+
 typedef int ClauseId;
 
 class Proof;
@@ -91,6 +94,8 @@ class ProofManager {
   static bool isInitialized; 
   ProofManager(ProofFormat format = LFSC);
   ~ProofManager(); 
+protected:
+  std::string d_logic;
 public:
   static ProofManager* currentPM();
   // initialization 
@@ -98,7 +103,7 @@ public:
   static void         initCnfProof(CVC4::prop::CnfStream* cnfStream);
   static void         initTheoryProof();
   
-  static Proof*       getProof();
+  static Proof*       getProof(SmtEngine* smt);
   static SatProof*    getSatProof();
   static CnfProof*    getCnfProof();
   static TheoryProof* getTheoryProof();
@@ -131,14 +136,18 @@ public:
   static std::string getVarName(prop::SatVariable var);
   static std::string getAtomName(prop::SatVariable var);
   static std::string getLitName(prop::SatLiteral lit);
+  
+  void setLogic(const std::string& logic_string);
+  const std::string getLogic() const { return d_logic; }
 };/* class ProofManager */
 
 class LFSCProof : public Proof {
   LFSCSatProof* d_satProof;
   LFSCCnfProof* d_cnfProof;
-  LFSCTheoryProof* d_theoryProof; 
+  LFSCTheoryProof* d_theoryProof;
+  SmtEngine* d_smtEngine; 
 public:
-  LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); 
+  LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); 
   virtual void toStream(std::ostream& out);
   virtual ~LFSCProof() {}
 };
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 2ac468b47..da9df0d42 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -579,9 +579,9 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
     res->addStep(lit, res_id, !sign(lit)); 
   }
   registerResolution(d_emptyClauseId, res);
-  // FIXME: massive hack
-  Proof* proof = ProofManager::getProof();
-  proof->toStream(std::cout); 
+  // // FIXME: massive hack
+  // Proof* proof = ProofManager::getProof();
+  // proof->toStream(std::cout); 
 }
 
 /// CRef manager
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 4ce804a74..696bd8309 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -167,7 +167,7 @@ void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) {
   // declaring the terms
   for (ExprSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) {
     Expr term = *it;
-    
+
     os << "(% " << term << " (term "; 
     paren <<")";