From: Andrew Reynolds Date: Wed, 4 Aug 2021 19:19:51 +0000 (-0500) Subject: Add optional debug information for dumping instantiations (#6950) X-Git-Tag: cvc5-1.0.0~1407 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e29a86f380354371dee1e5032034a2fe5edfee16;p=cvc5.git Add optional debug information for dumping instantiations (#6950) This complete the implementation of dump-instantiations-debug. With this option, we can print the source of instantiations. For example: $ cvc5 regress1/quantifiers/dump-inst-proof.smt2 --dump-instantiations-debug --produce-proofs unsat (instantiations (forall ((x Int)) (or (P x) (Q x))) (! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (P x) true)))) ) (instantiations (forall ((x Int)) (or (not (S x)) (not (Q x)))) (! ( 2 ) :source QUANTIFIERS_INST_E_MATCHING_SIMPLE ((not (= (S x) false)))) ) --- diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index bf658dfe0..5431a8348 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -174,7 +174,8 @@ bool CommandExecutor::doCommandSingleton(Command* cmd) getterCommands.emplace_back(new GetProofCommand()); } - if (d_solver->getOptions().driver.dumpInstantiations + if ((d_solver->getOptions().driver.dumpInstantiations + || d_solver->getOptions().driver.dumpInstantiationsDebug) && GetInstantiationsCommand::isEnabled(d_solver.get(), res)) { getterCommands.emplace_back(new GetInstantiationsCommand()); diff --git a/src/options/main_options.toml b/src/options/main_options.toml index 19bb97f34..869d411bd 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -112,6 +112,14 @@ public = true default = "false" help = "output instantiations of quantified formulas after every UNSAT/VALID response" +[[option]] + name = "dumpInstantiationsDebug" + category = "regular" + long = "dump-instantiations-debug" + type = "bool" + default = "false" + help = "output instantiations of quantified formulas after every UNSAT/VALID response, with debug information" + [[option]] name = "dumpUnsatCores" category = "regular" @@ -134,4 +142,4 @@ public = true long = "force-no-limit-cpu-while-dump" type = "bool" default = "false" - help = "Force no CPU limit when dumping models and proofs" \ No newline at end of file + help = "Force no CPU limit when dumping models and proofs" diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index b733f62ce..69727e1a2 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -101,14 +101,29 @@ void Printer::toStream(std::ostream& out, const UnsatCore& core) const void Printer::toStream(std::ostream& out, const InstantiationList& is) const { out << "(instantiations " << is.d_quant << std::endl; - for (const std::vector& i : is.d_inst) + for (const InstantiationVec& i : is.d_inst) { - out << " ( "; - for (const Node& n : i) + out << " "; + if (i.d_id != theory::InferenceId::UNKNOWN) + { + out << "(! "; + } + out << "( "; + for (const Node& n : i.d_vec) { out << n << " "; } - out << ")" << std::endl; + out << ")"; + if (i.d_id != theory::InferenceId::UNKNOWN) + { + out << " :source " << i.d_id; + if (!i.d_pfArg.isNull()) + { + out << " " << i.d_pfArg; + } + out << ")"; + } + out << std::endl; } out << ")" << std::endl; } diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp index ad9a8f844..66f9fde7c 100644 --- a/src/smt/proof_post_processor.cpp +++ b/src/smt/proof_post_processor.cpp @@ -1182,7 +1182,10 @@ bool ProofPostprocessCallback::addToTransChildren(Node eq, ProofPostprocessFinalCallback::ProofPostprocessFinalCallback( ProofNodeManager* pnm) : d_ruleCount(smtStatisticsRegistry().registerHistogram( - "finalProof::ruleCount")), + "finalProof::ruleCount")), + d_instRuleIds( + smtStatisticsRegistry().registerHistogram( + "finalProof::instRuleId")), d_totalRuleCount( smtStatisticsRegistry().registerInt("finalProof::totalRuleCount")), d_minPedanticLevel( @@ -1227,6 +1230,20 @@ bool ProofPostprocessFinalCallback::shouldUpdate(std::shared_ptr pn, // record stats for the rule d_ruleCount << r; ++d_totalRuleCount; + // take stats on the instantiations in the proof + if (r == PfRule::INSTANTIATE) + { + Node q = pn->getChildren()[0]->getResult(); + const std::vector& args = pn->getArguments(); + if (args.size() > q[0].getNumChildren()) + { + InferenceId id; + if (getInferenceId(args[q[0].getNumChildren()], id)) + { + d_instRuleIds << id; + } + } + } return false; } diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h index f9e93fa91..056f77695 100644 --- a/src/smt/proof_post_processor.h +++ b/src/smt/proof_post_processor.h @@ -24,6 +24,7 @@ #include "proof/proof_node_updater.h" #include "smt/witness_form.h" +#include "theory/inference_id.h" #include "util/statistics_stats.h" namespace cvc5 { @@ -256,6 +257,11 @@ class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback private: /** Counts number of postprocessed proof nodes for each kind of proof rule */ HistogramStat d_ruleCount; + /** + * Counts number of postprocessed proof nodes of rule INSTANTIATE that were + * marked with the given inference id. + */ + HistogramStat d_instRuleIds; /** Total number of postprocessed rule applications */ IntStat d_totalRuleCount; /** The minimum pedantic level of any rule encountered */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 55f3d1c5f..5f3920929 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1561,7 +1561,7 @@ UnsatCore SmtEngine::getUnsatCore() { } void SmtEngine::getRelevantInstantiationTermVectors( - std::map>>& insts) + std::map& insts, bool getDebugInfo) { Assert(d_state->getMode() == SmtMode::UNSAT); // generate with new proofs @@ -1570,7 +1570,7 @@ void SmtEngine::getRelevantInstantiationTermVectors( Assert(pe->getProof() != nullptr); std::shared_ptr pfn = d_pfManager->getFinalProof(pe->getProof(), *d_asserts); - d_ucManager->getRelevantInstantiations(pfn, insts); + d_ucManager->getRelevantInstantiations(pfn, insts, getDebugInfo); } std::string SmtEngine::getProof() @@ -1635,11 +1635,36 @@ void SmtEngine::printInstantiations( std::ostream& out ) { } // Second, extract and print the instantiations - std::map>> insts; - getInstantiationTermVectors(insts); - for (const std::pair>>& i : insts) + std::map rinsts; + if (d_env->getOptions().smt.produceProofs + && (!d_env->getOptions().smt.unsatCores + || d_env->getOptions().smt.unsatCoresMode + == options::UnsatCoresMode::FULL_PROOF) + && getSmtMode() == SmtMode::UNSAT) { - if (i.second.empty()) + // minimize instantiations based on proof manager + getRelevantInstantiationTermVectors(rinsts, + options::dumpInstantiationsDebug()); + } + else + { + std::map>> insts; + getInstantiationTermVectors(insts); + for (const std::pair>>& i : insts) + { + // convert to instantiation list + Node q = i.first; + InstantiationList& ilq = rinsts[q]; + ilq.initialize(q); + for (const std::vector& ii : i.second) + { + ilq.d_inst.push_back(InstantiationVec(ii)); + } + } + } + for (std::pair& i : rinsts) + { + if (i.second.d_inst.empty()) { // no instantiations, skip continue; @@ -1653,22 +1678,23 @@ void SmtEngine::printInstantiations( std::ostream& out ) { // must have a name if (d_env->getOptions().printer.printInstMode == options::PrintInstMode::NUM) { - out << "(num-instantiations " << name << " " << i.second.size() << ")" - << std::endl; + out << "(num-instantiations " << name << " " << i.second.d_inst.size() + << ")" << std::endl; } else { + // take the name + i.second.d_quant = name; Assert(d_env->getOptions().printer.printInstMode == options::PrintInstMode::LIST); - InstantiationList ilist(name, i.second); - out << ilist; + out << i.second; } printed = true; } // if we did not print anything, we indicate this if (!printed) { - out << "No instantiations" << std::endl; + out << "none" << std::endl; } if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS) { @@ -1681,21 +1707,10 @@ void SmtEngine::getInstantiationTermVectors( { SmtScope smts(this); finishInit(); - if (d_env->getOptions().smt.produceProofs - && (!d_env->getOptions().smt.unsatCores - || d_env->getOptions().smt.unsatCoresMode == options::UnsatCoresMode::FULL_PROOF) - && getSmtMode() == SmtMode::UNSAT) - { - // minimize instantiations based on proof manager - getRelevantInstantiationTermVectors(insts); - } - else - { - QuantifiersEngine* qe = - getAvailableQuantifiersEngine("getInstantiationTermVectors"); - // otherwise, just get the list of all instantiations - qe->getInstantiationTermVectors(insts); - } + QuantifiersEngine* qe = + getAvailableQuantifiersEngine("getInstantiationTermVectors"); + // get the list of all instantiations + qe->getInstantiationTermVectors(insts); } bool SmtEngine::getSynthSolutions(std::map& solMap) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 68b1caad0..d00fa0c76 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -46,6 +46,7 @@ class LogicRequest; class StatisticsRegistry; class Printer; class ResourceManager; +struct InstantiationList; /* -------------------------------------------------------------------------- */ @@ -673,7 +674,7 @@ class CVC5_EXPORT SmtEngine * refutation. */ void getRelevantInstantiationTermVectors( - std::map>>& insts); + std::map& insts, bool getDebugInfo = false); /** * Get instantiation term vectors, which maps each instantiated quantified * formula to the list of instantiations for that quantified formula. This diff --git a/src/smt/unsat_core_manager.cpp b/src/smt/unsat_core_manager.cpp index 22304f9e8..01025e505 100644 --- a/src/smt/unsat_core_manager.cpp +++ b/src/smt/unsat_core_manager.cpp @@ -56,12 +56,13 @@ void UnsatCoreManager::getUnsatCore(std::shared_ptr pfn, void UnsatCoreManager::getRelevantInstantiations( std::shared_ptr pfn, - std::map>>& insts) + std::map& insts, + bool getDebugInfo) { std::unordered_map visited; std::unordered_map::iterator it; std::vector> visit; - + std::map::iterator itq; std::shared_ptr cur; visit.push_back(pfn); do @@ -82,8 +83,27 @@ void UnsatCoreManager::getRelevantInstantiations( Node q = cs[0]->getResult(); // the instantiation is a prefix of the arguments up to the number of // variables - insts[q].push_back( - {instTerms.begin(), instTerms.begin() + q[0].getNumChildren()}); + itq = insts.find(q); + if (itq == insts.end()) + { + insts[q].initialize(q); + itq = insts.find(q); + } + itq->second.d_inst.push_back(InstantiationVec( + {instTerms.begin(), instTerms.begin() + q[0].getNumChildren()})); + if (getDebugInfo) + { + std::vector extraArgs(instTerms.begin() + q[0].getNumChildren(), + instTerms.end()); + if (extraArgs.size() >= 1) + { + getInferenceId(extraArgs[0], itq->second.d_inst.back().d_id); + } + if (extraArgs.size() >= 2) + { + itq->second.d_inst.back().d_pfArg = extraArgs[1]; + } + } } for (const std::shared_ptr& cp : cs) { diff --git a/src/smt/unsat_core_manager.h b/src/smt/unsat_core_manager.h index e064b83a7..eb71c67ca 100644 --- a/src/smt/unsat_core_manager.h +++ b/src/smt/unsat_core_manager.h @@ -21,6 +21,7 @@ #include "context/cdlist.h" #include "expr/node.h" #include "proof/proof_node.h" +#include "theory/quantifiers/instantiation_list.h" namespace cvc5 { @@ -61,9 +62,9 @@ class UnsatCoreManager * matrix with each row corresponding to the terms with which the respective * quantified formula is instiated. */ - void getRelevantInstantiations( - std::shared_ptr pfn, - std::map>>& insts); + void getRelevantInstantiations(std::shared_ptr pfn, + std::map& insts, + bool getDebugInfo = false); }; /* class UnsatCoreManager */ diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 8ed30ea98..bf13b75b1 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -16,6 +16,7 @@ #include "theory/inference_id.h" #include +#include "proof/proof_checker.h" #include "util/rational.h" namespace cvc5 { @@ -426,5 +427,16 @@ Node mkInferenceIdNode(InferenceId i) return NodeManager::currentNM()->mkConst(Rational(static_cast(i))); } +bool getInferenceId(TNode n, InferenceId& i) +{ + uint32_t index; + if (!ProofRuleChecker::getUInt32(n, index)) + { + return false; + } + i = static_cast(index); + return true; +} + } // namespace theory } // namespace cvc5 diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index b2bfe3657..e93803170 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -823,6 +823,9 @@ std::ostream& operator<<(std::ostream& out, InferenceId i); /** Make node from inference id */ Node mkInferenceIdNode(InferenceId i); +/** get an inference identifier from a node, return false if we fail */ +bool getInferenceId(TNode n, InferenceId& i); + } // namespace theory } // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index 3e3249629..63aabbfd6 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -59,7 +59,6 @@ Trigger::Trigger(QuantifiersState& qs, Node np = ensureGroundTermPreprocessed(val, n, d_groundTerms); d_nodes.push_back(np); } - d_trNode = NodeManager::currentNM()->mkNode(SEXPR, d_nodes); if (Trace.isOn("trigger")) { QuantAttributes& qa = d_qreg.getQuantAttributes(); @@ -70,18 +69,19 @@ Trigger::Trigger(QuantifiersState& qs, Trace("trigger") << " " << n << std::endl; } } + std::vector extNodes; + for (const Node& nt : d_nodes) + { + // note we must display the original form, so we go back to bound vars + Node ns = d_qreg.substituteInstConstantsToBoundVariables(nt, q); + extNodes.push_back(ns); + } + d_trNode = NodeManager::currentNM()->mkNode(SEXPR, extNodes); if (Output.isOn(options::OutputTag::TRIGGER)) { QuantAttributes& qa = d_qreg.getQuantAttributes(); - Output(options::OutputTag::TRIGGER) - << "(trigger " << qa.quantToString(q) << " ("; - for (size_t i = 0, nnodes = d_nodes.size(); i < nnodes; i++) - { - // note we must display the original form, so we go back to bound vars - Node ns = d_qreg.substituteInstConstantsToBoundVariables(d_nodes[i], q); - Output(options::OutputTag::TRIGGER) << (i > 0 ? " " : "") << ns; - } - Output(options::OutputTag::TRIGGER) << "))" << std::endl; + Output(options::OutputTag::TRIGGER) << "(trigger " << qa.quantToString(q) + << " " << d_trNode << ")" << std::endl; } QuantifiersStatistics& stats = qs.getStats(); if( d_nodes.size()==1 ){ diff --git a/src/theory/quantifiers/instantiation_list.cpp b/src/theory/quantifiers/instantiation_list.cpp index db2e167fb..f4b52619a 100644 --- a/src/theory/quantifiers/instantiation_list.cpp +++ b/src/theory/quantifiers/instantiation_list.cpp @@ -20,6 +20,14 @@ namespace cvc5 { +InstantiationVec::InstantiationVec(const std::vector& vec, + theory::InferenceId id, + Node pfArg) + : d_vec(vec), d_id(id), d_pfArg(pfArg) +{ +} + +void InstantiationList::initialize(Node q) { d_quant = q; } std::ostream& operator<<(std::ostream& out, const InstantiationList& ilist) { Printer::getPrinter(options::outputLanguage())->toStream(out, ilist); diff --git a/src/theory/quantifiers/instantiation_list.h b/src/theory/quantifiers/instantiation_list.h index d97383ba0..5e292375a 100644 --- a/src/theory/quantifiers/instantiation_list.h +++ b/src/theory/quantifiers/instantiation_list.h @@ -22,20 +22,33 @@ #include #include "expr/node.h" +#include "theory/inference_id.h" namespace cvc5 { +struct InstantiationVec +{ + public: + InstantiationVec(const std::vector& vec, + theory::InferenceId id = theory::InferenceId::UNKNOWN, + Node pfArg = Node::null()); + /** The vector of terms */ + std::vector d_vec; + /** The inference id */ + theory::InferenceId d_id; + /** The proof argument */ + Node d_pfArg; +}; + /** A list of instantiations for a quantified formula */ struct InstantiationList { - InstantiationList(Node q, const std::vector >& inst) - : d_quant(q), d_inst(inst) - { - } + /** Initialize */ + void initialize(Node q); /** The quantified formula */ Node d_quant; /** The instantiation list */ - std::vector > d_inst; + std::vector d_inst; }; /** Print the instantiation list to stream out */