diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-01-29 19:34:57 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-29 19:34:57 -0300 |
commit | 9ae030595825ad57bdbf55d856627318913c2fcf (patch) | |
tree | a6b0b6c8e444777a2fba3c3b6fcd4bbddcd417ab /src | |
parent | 50c3dee5c8a4855023df826e1a733ea3c6076774 (diff) |
[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.
Diffstat (limited to 'src')
-rw-r--r-- | src/options/smt_options.toml | 7 | ||||
-rw-r--r-- | src/smt/set_defaults.cpp | 9 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 40 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 6 |
4 files changed, 51 insertions, 11 deletions
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 @@ -248,6 +248,13 @@ header = "options/smt_options.h" 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" long = "dump-unsat-cores" 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<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 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 */ @@ -1101,6 +1102,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 * hold references to objects that belong to theory solvers, which are |