Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.

* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line

1 files changed, 9 insertions, 10 deletions

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 457023a59..739299b7d 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -13,7 +13,7 @@
  **
  ** A manager for UfProofs.
  **
- ** 
+ **
  **/
 
 
@@ -24,33 +24,32 @@
 #include "util/proof.h"
 #include "expr/expr.h"
 #include <ext/hash_set>
-#include <iostream> 
+#include <iostream>
 
 namespace CVC4 {
 
-  typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; 
-  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; 
+  typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet;
+  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
 
   class TheoryProof {
   protected:
     ExprSet d_termDeclarations;
-    SortSet d_sortDeclarations; 
+    SortSet d_sortDeclarations;
     ExprSet d_declarationCache;
-    
-    void addDeclaration(Expr atom); 
+
   public:
     TheoryProof();
     virtual ~TheoryProof() {}
     virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0;
+    void addDeclaration(Expr atom);
   };
 
   class LFSCTheoryProof: public TheoryProof {
-    static void printTerm(Expr term, std::ostream& os);
     void printDeclarations(std::ostream& os, std::ostream& paren);
   public:
-    static void printFormula(Expr atom, std::ostream& os);
+    static void printTerm(Expr term, std::ostream& os);
     virtual void printAssertions(std::ostream& os, std::ostream& paren);
-  }; 
+  };
 } /* CVC4 namespace */
 
 #endif /* __CVC4__THEORY_PROOF_H */