added currying for uf proofs; still needs debugging

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index e1f85b93f57cd77422b2c2a3b0c21e6994b69460..0c3c597dab7ee795af7c4779517bffe4d052d22a 100644 (file)
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -131,6 +131,7 @@ void LFSCProof::toStream(std::ostream& out) {
   std::ostringstream paren;
   out << "(check \n";
   d_theoryProof->printDeclarations(out, paren);
+  d_theoryProof->printAssertions(out, paren); 
   out << "(: (holds cln) \n";
   d_cnfProof->printAtomMapping(out, paren);
   d_cnfProof->printClauses(out, paren);

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 948ced393072d3d3fa04b8e773e41af6c40b2388..ecd9f9810a7825ebb76d89026a9171df5c5a7d03 100644 (file)
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -21,7 +21,12 @@ using namespace CVC4;
 
 TheoryProof::TheoryProof()
   : d_atomSet()
+  , d_inputFormulas()
+  , d_termDeclarations()
+  , d_sortDeclarations()
+  , d_declarationCache()
 {}
+
 void TheoryProof::addAtom(Expr atom) {
   d_atomSet.insert(atom); 
   Assert (atom.getKind() == kind::EQUAL);
@@ -29,20 +34,30 @@ void TheoryProof::addAtom(Expr atom) {
   addDeclaration(atom[1]); 
 }
 
+void TheoryProof::assertFormula(Expr formula) {
+  d_inputFormulas.insert(formula);
+  addDeclaration(formula); 
+}
+
 void TheoryProof::addDeclaration(Expr term) {
+  if (d_declarationCache.count(term))
+    return;
+  
   Type type = term.getType();
   if (type.isSort())
     d_sortDeclarations.insert(type);
   if (term.getKind() == kind::APPLY_UF) {
     Expr function = term.getOperator();
     d_termDeclarations.insert(function);
-    Assert (term.getNumChildren() == 1);
-    addDeclaration(term[0]); 
-  } else {
-    Assert (term.isVariable()); 
+  } else if (term.isVariable()) {
     Assert (type.isSort()); 
     d_termDeclarations.insert(term);
   }
+  // recursively declare all other terms
+  for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+    addDeclaration(term[i]); 
+  }
+  d_declarationCache.insert(term); 
 }
 
 void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) {
@@ -50,22 +65,88 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) {
     os << term; 
     return;
   }
-  Assert (term.getKind() == kind::APPLY_UF && term.getNumChildren() == 1);
+  std::ostringstream paren; 
+  Assert (term.getKind() == kind::APPLY_UF);
   Expr func = term.getOperator();
   os << "(apply _ _ " << func << " ";
-  printTerm(term[0], os);
-  os <<")"; 
+  for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+    printTerm(term[i], os);
+    if (i < term.getNumChildren() - 1) {
+      os << "(apply _ _ " << func << " ";
+      paren << ")"; 
+    }
+    os << ")" ; 
+  }
+  os << paren.str(); 
+}
+
+std::string toLFSCKind(Kind kind) {
+  switch(kind) {
+  case kind::OR : return "or";
+  case kind::AND: return "and";
+  case kind::XOR: return "xor";
+  case kind::EQUAL: return "=";
+  case kind::IMPLIES: return "impl";
+  case kind::NOT: return "not";
+  default:
+    Unreachable(); 
+  }
 }
 
 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);
-  os << ")"; 
+  // should make this more general and overall sane
+  Assert (atom.getType().isBoolean());
+  Kind kind = atom.getKind(); 
+  // this is the only predicate we have
+  if (kind == kind::EQUAL) {
+    os << "(";
+    os <<"= ";
+    os << atom[0].getType() <<" "; 
+    printTerm(atom[0], os);
+    os <<" "; 
+    printTerm(atom[1], os);
+    os <<")"; 
+  } else if ( kind == kind::OR ||
+              kind == kind::AND ||
+              kind == kind::XOR ||
+              kind == kind::IMPLIES ||
+              kind == kind::NOT) {
+    // print the boolean operators
+    os << "(";
+    os << toLFSCKind(kind);
+    if (atom.getNumChildren() > 2) {
+      std::ostringstream paren;
+      os << " ";
+      for (unsigned i =0; i < atom.getNumChildren(); ++i) {
+        printFormula(atom[i], os);
+        os << " ";
+        if (i < atom.getNumChildren() - 2) {
+          os << "("<< toLFSCKind(kind) << " "; 
+          paren << ")"; 
+        }
+      }
+      os << paren.str() <<")"; 
+    } else {
+      // this is for binary and unary operators 
+      for (unsigned i = 0; i < atom.getNumChildren(); ++i) {
+        os <<" ";
+        printFormula(atom[i], os); 
+      }
+      os <<")"; 
+    }
+  } else {
+    Assert (false); 
+  }
+}
+
+void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) {
+  unsigned counter = 0; 
+  for (ExprSet::const_iterator it = d_inputFormulas.begin(); it != d_inputFormulas.end(); ++it) {
+    os << "(% A" << counter++ << " (th_holds ";
+    printFormula(*it,  os);
+    os << ")\n";
+    paren <<")"; 
+  }
 }
 
 void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) {
@@ -76,7 +157,7 @@ void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) {
   }
 
   // declaring the terms
-  for (TermSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) {
+  for (ExprSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) {
     Expr term = *it;
     
     os << "(% " << term << " (term "; 
@@ -84,11 +165,21 @@ void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) {
 
     Type type = term.getType();
     if (type.isFunction()) {
-      FunctionType ftype = (FunctionType)type; 
-      Assert (ftype.getArity() == 1);
-      Type arg_type = ftype.getArgTypes()[0];
-      Type result_type = ftype.getRangeType();
-      os << "(arrow " << arg_type << " " << result_type << "))\n"; 
+      std::ostringstream fparen; 
+      FunctionType ftype = (FunctionType)type;
+      std::vector<Type> args = ftype.getArgTypes();
+      args.push_back(ftype.getRangeType()); 
+      os << "(arrow "; 
+      for (unsigned i = 0; i < args.size(); i++) {
+        Type arg_type = args[i];
+        Assert (arg_type.isSort());
+        os << arg_type << " ";  
+        if (i < args.size() - 2) {
+          os << "(arrow ";
+          fparen <<")"; 
+        }
+      }
+      os << fparen.str() << "))\n"; 
     } else {
       Assert (term.isVariable());
       Assert (type.isSort());

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index ac8f9f7b8fe07ec58655aea612edcd312699a1cb..b09641fec35a46ac9a146e2cd3bdcc928174b4b2 100644 (file)
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -28,28 +28,33 @@
 
 namespace CVC4 {
 
-  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > AtomSet;
-  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > TermSet; 
+  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
   typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; 
   
   class TheoryProof {
   protected:
-    AtomSet d_atomSet;
-    TermSet d_termDeclarations;
+    ExprSet d_atomSet;
+    ExprSet d_inputFormulas;
+    ExprSet d_termDeclarations;
     SortSet d_sortDeclarations; 
+    ExprSet d_declarationCache;
+    
     void addDeclaration(Expr atom); 
   public:
     TheoryProof();
     void addAtom(Expr atom); 
+    void assertFormula(Expr formula); 
     virtual void printFormula(Expr atom, std::ostream& os) = 0;
-    virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; 
+    virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0;
+    virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0;
   };
 
   class LFSCTheoryProof: public TheoryProof {
     void printTerm(Expr term, std::ostream& os); 
   public:
     virtual void printFormula(Expr atom, std::ostream& os);
-    virtual void printDeclarations(std::ostream& os, std::ostream& paren); 
+    virtual void printDeclarations(std::ostream& os, std::ostream& paren);
+    virtual void printAssertions(std::ostream& os, std::ostream& paren);
   }; 
 } /* CVC4 namespace */
 #endif /* __CVC4__THEORY_PROOF_H */

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index be6acd09cc3c953b8bce463a53cc15e382228621..5a3334d647f7d56d981be54ec66738344bb349d7 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -38,6 +38,7 @@
 #include "expr/node.h"
 #include "expr/node_self_iterator.h"
 #include "prop/prop_engine.h"
+#include "proof/theory_proof.h"
 #include "smt/modal_exception.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -46,6 +47,7 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "proof/proof_manager.h"
 #include "util/proof.h"
+#include "proof/proof.h"
 #include "util/boolean_simplification.h"
 #include "util/node_visitor.h"
 #include "util/configuration.h"
@@ -3103,6 +3105,11 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
 
 Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) {
   Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
+  // PROOF (
+  ProofManager* pm = ProofManager::currentPM();
+  TheoryProof* pf = pm->getTheoryProof();
+  pf->assertFormula(ex);
+         //  ); 
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
@@ -3246,6 +3253,8 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
 
 Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, LogicException) {
   Assert(ex.getExprManager() == d_exprManager);
+  //PROOF (
+  ProofManager::currentPM()->getTheoryProof()->assertFormula(ex); //); 
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();