diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-05 18:29:34 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-23 13:21:47 -0500 |
commit | ff7d33c2f75668fde0f149943e3cf1bedad1102f (patch) | |
tree | b2533c2a7bf09602d567379ea1dc3bacc9f059c3 /src/smt | |
parent | b2bb2138543e75f64c3a794df940a221e4b5a97b (diff) |
Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.
* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/options | 10 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 31 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 7 | ||||
-rw-r--r-- | src/smt/smt_engine_check_proof.cpp | 61 | ||||
-rw-r--r-- | src/smt/smt_engine_scope.h | 10 |
5 files changed, 102 insertions, 17 deletions
diff --git a/src/smt/options b/src/smt/options index 69b5102de..b76822caf 100644 --- a/src/smt/options +++ b/src/smt/options @@ -22,14 +22,16 @@ option expandDefinitions expand-definitions bool :default false always expand symbol definitions in output common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h" support the get-value and get-model commands -option checkProofs check-proofs --check-proofs bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - after UNSAT/VALID, machine-check the generated proof -option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" +option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions -option dumpModels --dump-models bool :default false +option dumpModels --dump-models bool :default false :link --produce-models output models after every SAT/INVALID/UNKNOWN response option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on proof generation +option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + after UNSAT/VALID, machine-check the generated proof +option dumpProofs --dump-proofs bool :default false :link --proof + output proofs after every UNSAT/VALID response # this is just a placeholder for later; it doesn't show up in command-line options listings undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation (NOT YET SUPPORTED) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1f83bb547..ec37eaf26 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -46,8 +46,10 @@ #include "theory/theory_engine.h" #include "theory/bv/theory_bv_rewriter.h" #include "proof/proof_manager.h" +#include "main/options.h" #include "util/proof.h" #include "proof/proof.h" +#include "proof/proof_manager.h" #include "util/boolean_simplification.h" #include "util/node_visitor.h" #include "util/configuration.h" @@ -157,6 +159,8 @@ struct SmtEngineStatistics { IntStat d_numAssertionsPost; /** time spent in checkModel() */ TimerStat d_checkModelTime; + /** time spent in checkProof() */ + TimerStat d_checkProofTime; /** time spent in PropEngine::checkSat() */ TimerStat d_solveTime; /** time spent in pushing/popping */ @@ -183,11 +187,11 @@ struct SmtEngineStatistics { d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0), d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0), d_checkModelTime("smt::SmtEngine::checkModelTime"), + d_checkProofTime("smt::SmtEngine::checkProofTime"), d_solveTime("smt::SmtEngine::solveTime"), d_pushPopTime("smt::SmtEngine::pushPopTime"), d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"), d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0) - { StatisticsRegistry::registerStat(&d_definitionExpansionTime); @@ -667,6 +671,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_decisionEngine(NULL), d_theoryEngine(NULL), d_propEngine(NULL), + d_proofManager(NULL), d_definedFunctions(NULL), d_assertionList(NULL), d_assignments(NULL), @@ -696,6 +701,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_statisticsRegistry = new StatisticsRegistry(); d_stats = new SmtEngineStatistics(); + PROOF( d_proofManager = new ProofManager(); ); + // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic)); @@ -763,6 +770,7 @@ void SmtEngine::finishInit() { if(options::cumulativeMillisecondLimit() != 0) { setTimeLimit(options::cumulativeMillisecondLimit(), true); } + PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); } @@ -777,16 +785,11 @@ void SmtEngine::finalOptionsAreSet() { } if(options::checkModels()) { - if(! options::produceModels()) { - Notice() << "SmtEngine: turning on produce-models to support check-model" << endl; - setOption("produce-models", SExpr("true")); - } if(! options::interactive()) { - Notice() << "SmtEngine: turning on interactive-mode to support check-model" << endl; + Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl; setOption("interactive-mode", SExpr("true")); } } - if(options::produceAssignments() && !options::produceModels()) { Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl; setOption("produce-models", SExpr("true")); @@ -3291,9 +3294,6 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc finalOptionsAreSet(); doPendingPops(); - - PROOF( ProofManager::currentPM()->addAssertion(ex); ); - Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl; if(d_queryMade && !options::incrementalSolving()) { @@ -3308,6 +3308,8 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); // Ensure expr is type-checked at this point. ensureBoolean(e); + // Give it to proof manager + PROOF( ProofManager::currentPM()->addAssertion(e); ); } // check to see if a postsolve() is pending @@ -3361,6 +3363,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc // Check that UNSAT results generate a proof correctly. if(options::checkProofs()) { if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); checkProof(); } } @@ -3384,9 +3387,10 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // Substitute out any abstract values in ex Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr(); - // Ensure that the expression is type-checked at this point, and Boolean ensureBoolean(e); + // Give it to proof manager + PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); ); // check to see if a postsolve() is pending if(d_needPostsolve) { @@ -3437,6 +3441,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept // Check that UNSAT results generate a proof correctly. if(options::checkProofs()) { if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) { + TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); checkProof(); } } @@ -3449,7 +3454,9 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log SmtScope smts(this); finalOptionsAreSet(); doPendingPops(); - PROOF( ProofManager::currentPM()->addAssertion(ex);); + + PROOF( ProofManager::currentPM()->addAssertion(ex); ); + Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl; // Substitute out any abstract values in ex diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 0781ac1c0..8e400468c 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -56,6 +56,8 @@ class SmtEngine; class DecisionEngine; class TheoryEngine; +class ProofManager; + class Model; class StatisticsRegistry; @@ -83,6 +85,7 @@ namespace smt { class BooleanTermConverter; void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); + ProofManager* currentProofManager(); struct CommandCleanup; typedef context::CDList<Command*, CommandCleanup> CommandList; @@ -135,8 +138,11 @@ class CVC4_PUBLIC SmtEngine { TheoryEngine* d_theoryEngine; /** The propositional engine */ prop::PropEngine* d_propEngine; + /** The proof manager */ + ProofManager* d_proofManager; /** An index of our defined functions */ DefinedFunctionMap* d_definedFunctions; + /** * The assertion list (before any conversion) for supporting * getAssertions(). Only maintained if in interactive mode. @@ -327,6 +333,7 @@ class CVC4_PUBLIC SmtEngine { friend class ::CVC4::smt::BooleanTermConverter; friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*); friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException); + friend ProofManager* ::CVC4::smt::currentProofManager(); // to access d_modelCommands friend class ::CVC4::Model; friend class ::CVC4::theory::TheoryModel; diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp index e4de1029b..a731ff024 100644 --- a/src/smt/smt_engine_check_proof.cpp +++ b/src/smt/smt_engine_check_proof.cpp @@ -16,16 +16,75 @@ **/ #include "smt/smt_engine.h" +#include "util/statistics_registry.h" #include "check.h" +#include <cstdlib> +#include <cstring> +#include <fstream> +#include <string> +#include <unistd.h> + using namespace CVC4; using namespace std; +namespace CVC4 { + +namespace proof { + extern const char *const plf_signatures; +}/* CVC4::proof namespace */ + +namespace smt { + +class UnlinkProofFile { + string d_filename; +public: + UnlinkProofFile(const char* filename) : d_filename(filename) {} + ~UnlinkProofFile() { unlink(d_filename.c_str()); } +};/* class UnlinkProofFile */ + +}/* CVC4::smt namespace */ + +}/* CVC4 namespace */ + void SmtEngine::checkProof() { #ifdef CVC4_PROOF - //TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime); + Chat() << "generating proof..." << endl; + + Proof* pf = getProof(); + + Chat() << "checking proof..." << endl; + + if(!d_logic.isPure(theory::THEORY_BOOL) && + !d_logic.isPure(theory::THEORY_UF)) { + // no checking for these yet + Notice() << "Notice: no proof-checking for non-UF proofs yet" << endl; + return; + } + + char* pfFile = strdup("/tmp/cvc4_proof.XXXXXX"); + int fd = mkstemp(pfFile); + + // ensure this temp file is removed after + smt::UnlinkProofFile unlinker(pfFile); + + ofstream pfStream(pfFile); + pfStream << proof::plf_signatures << endl; + pf->toStream(pfStream); + pfStream.close(); + args a; + a.show_runs = false; + a.no_tail_calls = false; + a.compile_scc = false; + a.compile_scc_debug = false; + a.run_scc = false; + a.use_nested_app = false; + a.compile_lib = false; + init(); + check_file(pfFile, args()); + close(fd); #else /* CVC4_PROOF */ diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h index 21644d3f4..2389181b5 100644 --- a/src/smt/smt_engine_scope.h +++ b/src/smt/smt_engine_scope.h @@ -22,10 +22,14 @@ #include "util/cvc4_assert.h" #include "expr/node_manager.h" #include "util/output.h" +#include "proof/proof.h" #pragma once namespace CVC4 { + +class ProofManager; + namespace smt { extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current; @@ -35,6 +39,12 @@ inline SmtEngine* currentSmtEngine() { return s_smtEngine_current; } +inline ProofManager* currentProofManager() { + Assert(PROOF_ON()); + Assert(s_smtEngine_current != NULL); + return s_smtEngine_current->d_proofManager; +} + class SmtScope : public NodeManagerScope { /** The old NodeManager, to be restored on destruction. */ SmtEngine* d_oldSmtEngine; |