Merge branch 'master' into fixCMSBuildPRfixCMSBuildPR

1 files changed, 12 insertions, 94 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 98e865478..81d4f594d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -62,7 +62,6 @@
 #include "options/open_ostream.h"
 #include "options/option_exception.h"
 #include "options/printer_options.h"
-#include "options/proof_options.h"
 #include "options/prop_options.h"
 #include "options/quantifiers_options.h"
 #include "options/sep_options.h"
@@ -75,9 +74,7 @@
 #include "preprocessing/preprocessing_pass_context.h"
 #include "preprocessing/preprocessing_pass_registry.h"
 #include "printer/printer.h"
-#include "proof/proof.h"
 #include "proof/proof_manager.h"
-#include "proof/theory_proof.h"
 #include "proof/unsat_core.h"
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
@@ -113,14 +110,9 @@
 #include "theory/theory_model.h"
 #include "theory/theory_traits.h"
 #include "util/hash.h"
-#include "util/proof.h"
 #include "util/random.h"
 #include "util/resource_manager.h"
 
-#if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
-#include "lfscc.h"
-#endif
-
 using namespace std;
 using namespace CVC4;
 using namespace CVC4::smt;
@@ -131,10 +123,6 @@ using namespace CVC4::theory;
 
 namespace CVC4 {
 
-namespace proof {
-extern const char* const plf_signatures;
-}  // namespace proof
-
 namespace smt {
 
 }/* namespace CVC4::smt */
@@ -307,15 +295,6 @@ void SmtEngine::finishInit()
     d_abductSolver.reset(new AbductionSolver(this));
   }
 
-  PROOF( ProofManager::currentPM()->setLogic(d_logic); );
-  PROOF({
-    TheoryEngine* te = d_smtSolver->getTheoryEngine();
-    for (TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id)
-    {
-      ProofManager::currentPM()->getTheoryProofEngine()->finishRegisterTheory(
-          te->theoryOf(id));
-    }
-  });
   d_pp->finishInit();
 
   AlwaysAssert(getPropEngine()->getAssertionLevel() == 0)
@@ -709,9 +688,18 @@ void SmtEngine::defineFunction(Expr func,
   ss << language::SetLanguage(
             language::SetLanguage::getLanguage(Dump.getStream()))
      << func;
-  DefineFunctionCommand c(ss.str(), func, formals, formula, global);
+  std::vector<Node> nFormals;
+  nFormals.reserve(formals.size());
+
+  for (const Expr& formal : formals)
+  {
+    nFormals.push_back(formal.getNode());
+  }
+
+  DefineFunctionNodeCommand nc(
+      ss.str(), func.getNode(), nFormals, formula.getNode());
   d_dumpm->addToModelCommandAndDump(
-      c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
+      nc, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
 
   // type check body
   debugCheckFunctionBody(formula, formals, func);
@@ -891,7 +879,7 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
     std::stringstream ss;
     ss << "Cannot " << c
        << " since model is not available. Perhaps the most recent call to "
-          "check-sat was interupted?";
+          "check-sat was interrupted?";
     throw RecoverableModalException(ss.str().c_str());
   }
 
@@ -1005,12 +993,6 @@ Result SmtEngine::checkSatInternal(const vector<Node>& assumptions,
         checkModel();
       }
     }
-    // Check that UNSAT results generate a proof correctly.
-    if(options::checkProofs()) {
-      if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
-        checkProof();
-      }
-    }
     // Check that UNSAT results generate an unsat core correctly.
     if(options::checkUnsatCores()) {
       if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
@@ -1476,43 +1458,6 @@ Expr SmtEngine::getSepHeapExpr() { return getSepHeapAndNilExpr().first; }
 
 Expr SmtEngine::getSepNilExpr() { return getSepHeapAndNilExpr().second; }
 
-void SmtEngine::checkProof()
-{
-#if (IS_LFSC_BUILD && IS_PROOFS_BUILD)
-
-  Chat() << "generating proof..." << endl;
-
-  const Proof& pf = getProof();
-
-  Chat() << "checking proof..." << endl;
-
-  std::string logicString = d_logic.getLogicString();
-
-  std::stringstream pfStream;
-
-  pfStream << proof::plf_signatures << endl;
-  int64_t sizeBeforeProof = static_cast<int64_t>(pfStream.tellp());
-
-  pf.toStream(pfStream);
-  d_stats->d_proofsSize +=
-      static_cast<int64_t>(pfStream.tellp()) - sizeBeforeProof;
-
-  {
-    TimerStat::CodeTimer checkProofTimer(d_stats->d_lfscCheckProofTime);
-    lfscc_init();
-    lfscc_check_file(pfStream, false, false, false, false, false, false, false);
-  }
-  // FIXME: we should actually call lfscc_cleanup here, but lfscc_cleanup
-  // segfaults on regress0/bv/core/bitvec7.smt
-  // lfscc_cleanup();
-
-#else  /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
-  Unreachable()
-      << "This version of CVC4 was built without proof support; cannot check "
-         "proofs.";
-#endif /* (IS_LFSC_BUILD && IS_PROOFS_BUILD) */
-}
-
 UnsatCore SmtEngine::getUnsatCoreInternal()
 {
 #if IS_PROOFS_BUILD
@@ -1548,7 +1493,6 @@ void SmtEngine::checkUnsatCore() {
   coreChecker.setIsInternalSubsolver();
   coreChecker.setLogic(getLogicInfo());
   coreChecker.getOptions().set(options::checkUnsatCores, false);
-  coreChecker.getOptions().set(options::checkProofs, false);
 
   Notice() << "SmtEngine::checkUnsatCore(): pushing core assertions (size == " << core.size() << ")" << endl;
   for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
@@ -1823,32 +1767,6 @@ UnsatCore SmtEngine::getUnsatCore() {
   return getUnsatCoreInternal();
 }
 
-// TODO(#1108): Simplify the error reporting of this method.
-const Proof& SmtEngine::getProof()
-{
-  Trace("smt") << "SMT getProof()" << endl;
-  SmtScope smts(this);
-  finishInit();
-  if(Dump.isOn("benchmark")) {
-    Dump("benchmark") << GetProofCommand();
-  }
-#if IS_PROOFS_BUILD
-  if(!options::proof()) {
-    throw ModalException("Cannot get a proof when produce-proofs option is off.");
-  }
-  if (d_state->getMode() != SmtMode::UNSAT)
-  {
-    throw RecoverableModalException(
-        "Cannot get a proof unless immediately preceded by UNSAT/ENTAILED "
-        "response.");
-  }
-
-  return ProofManager::getProof(this);
-#else /* IS_PROOFS_BUILD */
-  throw ModalException("This build of CVC4 doesn't have proof support.");
-#endif /* IS_PROOFS_BUILD */
-}
-
 void SmtEngine::printInstantiations( std::ostream& out ) {
   SmtScope smts(this);
   finishInit();