From: Guy <katz911@gmail.com>
Date: Mon, 20 Jun 2016 21:20:15 +0000 (-0700)
Subject: Addressed a bug that occurs when proof production is triggered via text flags in... 
X-Git-Tag: cvc5-1.0.0~6049^2~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a592e0137504c5788084cb8e150f46f109f566d7;p=cvc5.git

Addressed a bug that occurs when proof production is triggered via text flags in the input.
Separated some initialization into two phases:
1. Those that can be done when the proof compiliation flag is set
2. Those that can be done only when the --proof option is set.
For #2, deferred their execution until the text flags in the input have been processed
---

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 45b1f046e..d61261b38 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -96,7 +96,6 @@ CnfProof* ProofManager::getCnfProof() {
 }
 
 TheoryProofEngine* ProofManager::getTheoryProofEngine() {
-  Assert (options::proof());
   Assert (currentPM()->d_theoryProof != NULL);
   return currentPM()->d_theoryProof;
 }
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 7fa11cc5f..634b2b738 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -79,7 +79,6 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
       if (id == theory::THEORY_BV) {
         BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this);
         d_theoryProofTable[id] = bvp;
-        ((theory::bv::TheoryBV*)th)->setProofLog( bvp );
         return;
       }
 
@@ -98,6 +97,19 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
   }
 }
 
+void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) {
+  if (th) {
+    theory::TheoryId id = th->getId();
+    if (id == theory::THEORY_BV) {
+      Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end());
+
+      BitVectorProof *bvp = (BitVectorProof *)d_theoryProofTable[id];
+      ((theory::bv::TheoryBV*)th)->setProofLog( bvp );
+      return;
+    }
+  }
+}
+
 TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) {
   // The UF theory handles queries for the Builtin theory.
   if (id == theory::THEORY_BUILTIN) {
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index f6f00fa11..5907f9bd5 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -130,10 +130,19 @@ public:
 
   /**
    * Ensures that a theory proof class for the given theory is created.
+   * This method can be invoked regardless of whether the "proof" option
+   * has been set.
    *
    * @param theory
    */
   void registerTheory(theory::Theory* theory);
+  /**
+   * Additional configuration of the theory proof class for the given theory.
+   * This method should only be invoked when the "proof" option has been set.
+   *
+   * @param theory
+   */
+  void finishRegisterTheory(theory::Theory* theory);
 
   theory::TheoryId getTheoryForLemma(const prop::SatClause* clause);
   TheoryProof* getTheoryProof(theory::TheoryId id);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 69a150cc9..08495c936 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1083,7 +1083,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
     TheoryConstructor::addTheory(d_theoryEngine, id);
     //register with proof engine if applicable
-    THEORY_PROOF(ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id)); );
+#ifdef CVC4_PROOF
+    ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id));
+#endif
   }
 
   d_private->addUseTheoryListListener(d_theoryEngine);
@@ -1152,6 +1154,13 @@ void SmtEngine::finishInit() {
   d_dumpCommands.clear();
 
   PROOF( ProofManager::currentPM()->setLogic(d_logic); );
+  PROOF({
+      for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
+        ProofManager::currentPM()->getTheoryProofEngine()->
+          finishRegisterTheory(d_theoryEngine->theoryOf(id));
+      }
+    });
+
   Trace("smt-debug") << "SmtEngine::finishInit done" << std::endl;
 }
 
@@ -1846,7 +1855,7 @@ void SmtEngine::setDefaults() {
   }
   //counterexample-guided instantiation for non-sygus
   // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
-  if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) || 
+  if( ( d_logic.isQuantified() && ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) ||
       options::cbqiAll() ){
     if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );