From: Andrew Reynolds Date: Thu, 19 Aug 2021 18:32:50 +0000 (-0500) Subject: Refactor proof output for TPTP (#7029) X-Git-Tag: cvc5-1.0.0~1368 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c8b6b29616fa0183cb90e83d1ef72c9ebdb28587;p=cvc5.git Refactor proof output for TPTP (#7029) This eliminates the old option "inst format mode" and makes proof output for TPTP organized as an ordinary proof output format. --- diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 55661a094..42a63b47c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -209,34 +209,6 @@ void OptionsHandler::setBitblastAig(const std::string& option, } } -// printer/options_handlers.h -const std::string OptionsHandler::s_instFormatHelp = "\ -Inst format modes currently supported by the --inst-format option:\n\ -\n\ -default \n\ -+ Print instantiations as a list in the output language format.\n\ -\n\ -szs\n\ -+ Print instantiations as SZS compliant proof.\n\ -"; - -InstFormatMode OptionsHandler::stringToInstFormatMode(const std::string& option, - const std::string& flag, - const std::string& optarg) -{ - if(optarg == "default") { - return InstFormatMode::DEFAULT; - } else if(optarg == "szs") { - return InstFormatMode::SZS; - } else if(optarg == "help") { - puts(s_instFormatHelp.c_str()); - exit(1); - } else { - throw OptionException(std::string("unknown option for --inst-format: `") + - optarg + "'. Try --inst-format help."); - } -} - void OptionsHandler::setProduceAssertions(const std::string& option, const std::string& flag, bool value) diff --git a/src/options/options_handler.h b/src/options/options_handler.h index f19e63445..d6b81525d 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -183,10 +183,6 @@ public: /** Pointer to the containing Options object.*/ Options* d_options; - - /* Help strings */ - static const std::string s_instFormatHelp; - }; /* class OptionHandler */ } // namespace options diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml index 433e6f613..a8b11c197 100644 --- a/src/options/printer_options.toml +++ b/src/options/printer_options.toml @@ -16,25 +16,6 @@ name = "Printing" name = "table" help = "Print functional expressions over finite domains in a table format." -[[option]] - name = "instFormatMode" - category = "regular" - long = "inst-format=MODE" - type = "InstFormatMode" - default = "InstFormatMode::DEFAULT" - handler = "stringToInstFormatMode" - includes = ["options/printer_modes.h"] - help = "print format mode for instantiations, see --inst-format=help" -# InstFormatMode is currently exported as public so we can't auto genenerate -# the enum. -# help_mode = "Inst format modes." -#[[option.mode.DEFAULT]] -# name = "default" -# help = "Print instantiations as a list in the output language format." -#[[option.mode.SZS]] -# name = "szs" -# help = "Print instantiations as SZS compliant proof." - [[option]] name = "flattenHOChains" category = "regular" diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index f0458793e..071f14dec 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -18,6 +18,9 @@ name = "Proof" [[option.mode.VERIT]] name = "verit" help = "Output veriT proof" +[[option.mode.TPTP]] + name = "tptp" + help = "Output TPTP proof (work in progress)" [[option]] name = "proofPrintConclusion" diff --git a/src/smt/command.cpp b/src/smt/command.cpp index bb501fa5c..7aa05dde1 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -2047,11 +2047,9 @@ GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {} bool GetInstantiationsCommand::isEnabled(api::Solver* solver, const api::Result& res) { - return (solver->getOptions().printer.instFormatMode - != options::InstFormatMode::SZS - && (res.isSat() - || (res.isSatUnknown() - && res.getUnknownExplanation() == api::Result::INCOMPLETE))) + return (res.isSat() + || (res.isSatUnknown() + && res.getUnknownExplanation() == api::Result::INCOMPLETE)) || res.isUnsat() || res.isEntailed(); } void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm) diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp index 2c04b9e76..718d6cd6d 100644 --- a/src/smt/proof_manager.cpp +++ b/src/smt/proof_manager.cpp @@ -23,17 +23,19 @@ #include "proof/proof_node_algorithm.h" #include "proof/proof_node_manager.h" #include "smt/assertions.h" +#include "smt/env.h" #include "smt/preprocess_proof_generator.h" #include "smt/proof_post_processor.h" namespace cvc5 { namespace smt { -PfManager::PfManager(context::UserContext* u, SmtEngine* smte) - : d_pchecker(new ProofChecker(options::proofPedantic())), +PfManager::PfManager(Env& env, SmtEngine* smte) + : d_env(env), + d_pchecker(new ProofChecker(options::proofPedantic())), d_pnm(new ProofNodeManager(d_pchecker.get())), d_pppg(new PreprocessProofGenerator( - d_pnm.get(), u, "smt::PreprocessProofGenerator")), + d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")), d_pfpp(new ProofPostproccess( d_pnm.get(), smte, @@ -157,6 +159,13 @@ void PfManager::printProof(std::ostream& out, proof::DotPrinter dotPrinter; dotPrinter.print(out, fp.get()); } + else if (options::proofFormatMode() == options::ProofFormatMode::TPTP) + { + out << "% SZS output start Proof for " << d_env.getFilename() << std::endl; + // TODO (proj #37) print in TPTP compliant format + out << *fp; + out << "% SZS output end Proof for " << d_env.getFilename() << std::endl; + } else { out << "(proof\n"; diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h index 57478573c..fd24f62f6 100644 --- a/src/smt/proof_manager.h +++ b/src/smt/proof_manager.h @@ -23,6 +23,7 @@ namespace cvc5 { +class Env; class ProofChecker; class ProofNode; class ProofNodeManager; @@ -70,7 +71,7 @@ class ProofPostproccess; class PfManager { public: - PfManager(context::UserContext* u, SmtEngine* smte); + PfManager(Env& env, SmtEngine* smte); ~PfManager(); /** * Print the proof on the given output stream. @@ -116,6 +117,8 @@ class PfManager */ void getAssertions(Assertions& as, std::vector& assertions); + /** Reference to the env of SmtEngine */ + Env& d_env; /** The false node */ Node d_false; /** For the new proofs module */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 78bb9044a..0ddac7202 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -203,7 +203,7 @@ void SmtEngine::finishInit() // ensure bound variable uses canonical bound variables getNodeManager()->getBoundVarManager()->enableKeepCacheValues(); // make the proof manager - d_pfManager.reset(new PfManager(getUserContext(), this)); + d_pfManager.reset(new PfManager(*d_env.get(), this)); PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator(); // start the unsat core manager d_ucManager.reset(new UnsatCoreManager()); @@ -1599,10 +1599,6 @@ std::string SmtEngine::getProof() void SmtEngine::printInstantiations( std::ostream& out ) { SmtScope smts(this); finishInit(); - if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) - { - out << "% SZS output start Proof for " << d_env->getFilename() << std::endl; - } QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations"); // First, extract and print the skolemizations @@ -1689,10 +1685,6 @@ void SmtEngine::printInstantiations( std::ostream& out ) { { out << "none" << std::endl; } - if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) - { - out << "% SZS output end Proof for " << d_env->getFilename() << std::endl; - } } void SmtEngine::getInstantiationTermVectors(