[proof-new] Connecting new unsat cores (#5834)

Allows one to generate unsat cores from the new proof infrastructure. For new this is controlled by a new option, --check-unsat-cores-new.

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 33d21612b683064702b879e35807feb9843523a2..ed056ac9f4dda466f536352e2402a273e1bbc9db 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -247,6 +247,13 @@ header = "options/smt_options.h"
   type       = "bool"
   help       = "after UNSAT/VALID, produce and check an unsat core (expensive)"
 
+[[option]]
+  name       = "checkUnsatCoresNew"
+  category   = "regular"
+  long       = "check-unsat-cores-new"
+  type       = "bool"
+  help       = "after UNSAT/VALID, produce and check an unsat core (expensive) using the new proof infrastructure"
+
 [[option]]
   name       = "dumpUnsatCores"
   category   = "regular"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 3c70d8a57a2489490473f14587c481ff2b12d833..26f5745ca5ed720c5d2ac9ef78ded5cbf3b16bbe 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -65,12 +65,16 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     Notice() << "SmtEngine: setting dumpUnsatCores" << std::endl;
     options::dumpUnsatCores.set(true);
   }
-  if (options::checkUnsatCores() || options::dumpUnsatCores()
-      || options::unsatAssumptions())
+  if (options::checkUnsatCores() || options::checkUnsatCoresNew()
+      || options::dumpUnsatCores() || options::unsatAssumptions())
   {
     Notice() << "SmtEngine: setting unsatCores" << std::endl;
     options::unsatCores.set(true);
   }
+  if (options::checkUnsatCoresNew())
+  {
+    options::proofNew.set(true);
+  }
   if (options::bitvectorAigSimplifications.wasSetByUser())
   {
     Notice() << "SmtEngine: setting bitvectorAig" << std::endl;
@@ -245,6 +249,7 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     // Note we allow E-matching by default to support combinations of sequences
     // and quantifiers.
   }
+
   if (options::arraysExp())
   {
     if (!logic.isQuantified())

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4d3665da63b992a8d382fc9a6527493420acfd0d..09d54d6d82c83559271a05c78960e7c0025e0f8f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -53,6 +53,7 @@
 #include "smt/smt_engine_stats.h"
 #include "smt/smt_solver.h"
 #include "smt/sygus_solver.h"
+#include "smt/unsat_core_manager.h"
 #include "theory/quantifiers/instantiation_list.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
@@ -88,6 +89,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
       d_model(nullptr),
       d_checkModels(nullptr),
       d_pfManager(nullptr),
+      d_ucManager(nullptr),
       d_rewriter(new theory::Rewriter()),
       d_definedFunctions(nullptr),
       d_sygusSolver(nullptr),
@@ -153,7 +155,7 @@ SmtEngine::SmtEngine(NodeManager* nm, Options* optr)
 
   // d_proofManager must be created before Options has been finished
   // being parsed from the input file. Because of this, we cannot trust
-  // that options::proof() is set correctly yet.
+  // that options::unsatCores() is set correctly yet.
 #ifdef CVC4_PROOF
   d_proofManager.reset(new ProofManager(getUserContext()));
 #endif
@@ -224,6 +226,8 @@ void SmtEngine::finishInit()
   {
     d_pfManager.reset(new PfManager(getUserContext(), this));
     PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
+    // start the unsat core manager
+    d_ucManager.reset(new UnsatCoreManager());
     // use this proof node manager
     pnm = d_pfManager->getProofNodeManager();
     // enable proof support in the rewriter
@@ -332,6 +336,7 @@ SmtEngine::~SmtEngine()
 #endif
     d_rewriter.reset(nullptr);
     d_pfManager.reset(nullptr);
+    d_ucManager.reset(nullptr);
 
     d_absValues.reset(nullptr);
     d_asserts.reset(nullptr);
@@ -988,8 +993,10 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
       }
     }
     // Check that UNSAT results generate an unsat core correctly.
-    if(options::checkUnsatCores()) {
-      if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+    if (options::checkUnsatCores() || options::checkUnsatCoresNew())
+    {
+      if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+      {
         TimerStat::CodeTimer checkUnsatCoreTimer(d_stats->d_checkUnsatCoreTime);
         checkUnsatCore();
       }
@@ -1417,9 +1424,21 @@ UnsatCore SmtEngine::getUnsatCoreInternal()
         "Cannot get an unsat core unless immediately preceded by "
         "UNSAT/ENTAILED response.");
   }
-
-  d_proofManager->traceUnsatCore();  // just to trigger core creation
-  return UnsatCore(d_proofManager->extractUnsatCore());
+  // use old proof infrastructure
+  if (!d_pfManager)
+  {
+    d_proofManager->traceUnsatCore();  // just to trigger core creation
+    return UnsatCore(d_proofManager->extractUnsatCore());
+  }
+  // generate with new proofs
+  PropEngine* pe = getPropEngine();
+  Assert(pe != nullptr);
+  Assert(pe->getProof() != nullptr);
+  std::shared_ptr<ProofNode> pfn = d_pfManager->getFinalProof(
+      pe->getProof(), *d_asserts, *d_definedFunctions);
+  std::vector<Node> core;
+  d_ucManager->getUnsatCore(pfn, *d_asserts, core);
+  return UnsatCore(core);
 #else  /* IS_PROOFS_BUILD */
   throw ModalException(
       "This build of CVC4 doesn't have proof support (required for unsat "
@@ -1438,6 +1457,9 @@ void SmtEngine::checkUnsatCore() {
   std::unique_ptr<SmtEngine> coreChecker;
   initializeSubsolver(coreChecker);
   coreChecker->getOptions().set(options::checkUnsatCores, false);
+  // disable all proof options
+  coreChecker->getOptions().set(options::proofNew, false);
+  coreChecker->getOptions().set(options::checkUnsatCoresNew, false);
 
   // set up separation logic heap if necessary
   TypeNode sepLocType, sepDataType;
@@ -1491,12 +1513,12 @@ void SmtEngine::checkModel(bool hardFailure) {
   d_checkModels->checkModel(m, al, hardFailure);
 }
 
-// TODO(#1108): Simplify the error reporting of this method.
 UnsatCore SmtEngine::getUnsatCore() {
-  Trace("smt") << "SMT getUnsatCore()" << endl;
+  Trace("smt") << "SMT getUnsatCore()" << std::endl;
   SmtScope smts(this);
   finishInit();
-  if(Dump.isOn("benchmark")) {
+  if (Dump.isOn("benchmark"))
+  {
     getOutputManager().getPrinter().toStreamCmdGetUnsatCore(
         getOutputManager().getDumpOut());
   }

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a1fc809e4679694fd4aa78300dfe9383f0e68760..eb8eb6ca011bb20daa8e79f083d3f9a615ef3aef 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -118,6 +118,7 @@ struct SmtEngineStatistics;
 class SmtScope;
 class ProcessAssertions;
 class PfManager;
+class UnsatCoreManager;
 
 ProofManager* currentProofManager();
 }/* CVC4::smt namespace */
@@ -1100,6 +1101,11 @@ class CVC4_PUBLIC SmtEngine
    */
   std::unique_ptr<smt::PfManager> d_pfManager;
 
+  /**
+   * The unsat core manager, which produces unsat cores and related information
+   * from refutations. */
+  std::unique_ptr<smt::UnsatCoreManager> d_ucManager;
+
   /**
    * The rewriter associated with this SmtEngine. We have a different instance
    * of the rewriter for each SmtEngine instance. This is because rewriters may

diff --git a/test/regress/regress1/fmf/PUZ001+1.smt2 b/test/regress/regress1/fmf/PUZ001+1.smt2
index 607a79f0de1aab7669fc5774c3862c4530c7c9ac..9c36ac56198a559ffe562595271dd2de51fa9e40 100644 (file)
--- a/test/regress/regress1/fmf/PUZ001+1.smt2
+++ b/test/regress/regress1/fmf/PUZ001+1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --no-check-unsat-core
+; COMMAND-LINE: --finite-model-find --no-check-unsat-cores
 ; EXPECT: unsat
 ;%------------------------------------------------------------------------------
 ;% File     : PUZ001+1 : TPTP v5.4.0. Released v2.0.0.
@@ -53,7 +53,7 @@
 (declare-fun richer__smt2_2 ( sort__smt2 sort__smt2 ) Bool)
 
 ; pel55_1 axiom
-(assert (exists ((?X sort__smt2)) 
+(assert (exists ((?X sort__smt2))
     (and (lives__smt2_1 ?X)
         (killed__smt2_2 ?X agatha__smt2_0))))
 
@@ -67,44 +67,44 @@
 (assert (lives__smt2_1 charles__smt2_0))
 
 ; pel55_3 axiom
-(assert (forall ((?X sort__smt2)) 
+(assert (forall ((?X sort__smt2))
     (=> (lives__smt2_1 ?X)
         (or (= ?X agatha__smt2_0)
             (= ?X butler__smt2_0)
             (= ?X charles__smt2_0)))))
 
 ; pel55_4 axiom
-(assert (forall ((?X sort__smt2) (?Y sort__smt2)) 
+(assert (forall ((?X sort__smt2) (?Y sort__smt2))
     (=> (killed__smt2_2 ?X ?Y)
         (hates__smt2_2 ?X ?Y))))
 
 ; pel55_5 axiom
-(assert (forall ((?X sort__smt2) (?Y sort__smt2)) 
+(assert (forall ((?X sort__smt2) (?Y sort__smt2))
     (=> (killed__smt2_2 ?X ?Y)
         (not (richer__smt2_2 ?X ?Y)))))
 
 ; pel55_6 axiom
-(assert (forall ((?X sort__smt2)) 
+(assert (forall ((?X sort__smt2))
     (=> (hates__smt2_2 agatha__smt2_0 ?X)
         (not (hates__smt2_2 charles__smt2_0 ?X)))))
 
 ; pel55_7 axiom
-(assert (forall ((?X sort__smt2)) 
+(assert (forall ((?X sort__smt2))
     (=> (not (= ?X butler__smt2_0))
         (hates__smt2_2 agatha__smt2_0 ?X))))
 
 ; pel55_8 axiom
-(assert (forall ((?X sort__smt2)) 
+(assert (forall ((?X sort__smt2))
     (=> (not (richer__smt2_2 ?X agatha__smt2_0))
         (hates__smt2_2 butler__smt2_0 ?X))))
 
 ; pel55_9 axiom
-(assert (forall ((?X sort__smt2)) 
+(assert (forall ((?X sort__smt2))
     (=> (hates__smt2_2 agatha__smt2_0 ?X)
         (hates__smt2_2 butler__smt2_0 ?X))))
 
 ; pel55_10 axiom
-(assert (forall ((?X sort__smt2)) 
+(assert (forall ((?X sort__smt2))
 (exists ((?Y sort__smt2)) (not (hates__smt2_2 ?X ?Y)))))
 
 ; pel55_11 axiom