From: Haniel Barbosa Date: Fri, 29 Jan 2021 22:34:57 +0000 (-0300) Subject: [proof-new] Connecting new unsat cores (#5834) X-Git-Tag: cvc5-1.0.0~2338 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9ae030595825ad57bdbf55d856627318913c2fcf;p=cvc5.git [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 33d21612b..ed056ac9f 100644 --- 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 3c70d8a57..26f5745ca 100644 --- 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 4d3665da6..09d54d6d8 100644 --- 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& 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 pfn = d_pfManager->getFinalProof( + pe->getProof(), *d_asserts, *d_definedFunctions); + std::vector 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 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 a1fc809e4..eb8eb6ca0 100644 --- 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 d_pfManager; + /** + * The unsat core manager, which produces unsat cores and related information + * from refutations. */ + std::unique_ptr 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 607a79f0d..9c36ac561 100644 --- 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