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, 37 insertions, 5 deletions

diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 9a2dbe655..0a932f906 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -13,7 +13,7 @@
  **
  ** A manager for CnfProofs.
  **
- ** 
+ **
  **/
 
 #ifndef __CVC4__CNF_PROOF_H
@@ -25,36 +25,68 @@
 
 #include <ext/hash_set>
 #include <ext/hash_map>
-#include <iostream> 
+#include <iostream>
 
 namespace CVC4 {
 namespace prop {
-class CnfStream;
+  class CnfStream;
 }
 
+class CnfProof;
+
+class AtomIterator {
+  CnfProof& d_cnf;
+  ProofManager::var_iterator d_it;
+
+public:
+  AtomIterator(CnfProof& cnf, const ProofManager::var_iterator& it)
+    : d_cnf(cnf), d_it(it)
+  {}
+  inline Expr operator*();
+  AtomIterator& operator++() { ++d_it; return *this; }
+  AtomIterator operator++(int) { AtomIterator x = *this; ++d_it; return x; }
+  bool operator==(const AtomIterator& it) const { return &d_cnf == &it.d_cnf && d_it == it.d_it; }
+  bool operator!=(const AtomIterator& it) const { return !(*this == it); }
+};/* class AtomIterator */
+
 class CnfProof {
 protected:
   CVC4::prop::CnfStream* d_cnfStream;
   Expr getAtom(prop::SatVariable var);
+  friend class AtomIterator;
 public:
   CnfProof(CVC4::prop::CnfStream* cnfStream);
 
+  typedef AtomIterator iterator;
+  virtual iterator begin_atom_mapping() = 0;
+  virtual iterator end_atom_mapping() = 0;
+
   virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0;
   virtual void printClauses(std::ostream& os, std::ostream& paren) = 0;
-  virtual ~CnfProof(); 
+  virtual ~CnfProof();
 };
 
-class LFSCCnfProof: public CnfProof {
+class LFSCCnfProof : public CnfProof {
   void printInputClauses(std::ostream& os, std::ostream& paren);
   void printTheoryLemmas(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)
   {}
+
+  virtual iterator begin_atom_mapping();
+  virtual iterator end_atom_mapping();
+
   virtual void printAtomMapping(std::ostream& os, std::ostream& paren);
   virtual void printClauses(std::ostream& os, std::ostream& paren);
 };
 
+inline Expr AtomIterator::operator*() {
+  return d_cnf.getAtom(*d_it);
+}
+
 } /* CVC4 namespace */
+
 #endif /* __CVC4__CNF_PROOF_H */