From bdf46b42d6bd66121a5b5175a81408cd64d7ecfa Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 1 Jul 2021 10:07:39 -0500 Subject: Add option to limit the number of instantiation rounds (#6818) This adds an option to limit the number of instantiation rounds used by quantifiers engine. This option may be generally useful for making quantifiers terminating. It also is necessary to update the new default behavior of SyGuS + recursive functions. A followup PR will make sygus verification calls set the option added on this PR automatically, so that we use incomplete + termination strategies for (non-PBE) sygus in the presence of recursive functions. This PR also makes minor improvements to the quantifier utility infrastructure. --- src/theory/quantifiers/instantiate.h | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'src/theory/quantifiers/instantiate.h') diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 95a396d51..eddc7470b 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -110,7 +110,6 @@ class Instantiate : public QuantifiersUtil TermRegistry& tr, ProofNodeManager* pnm = nullptr); ~Instantiate(); - /** reset */ bool reset(Theory::Effort e) override; /** register quantifier */ @@ -237,11 +236,11 @@ class Instantiate : public QuantifiersUtil //--------------------------------------end general utilities /** - * Debug print, called once per instantiation round. This prints + * Called once at the end of each instantiation round. This prints * instantiations added this round to trace inst-per-quant-round, if * applicable, and prints to out if the option debug-inst is enabled. */ - void debugPrint(std::ostream& out); + void notifyEndRound(); /** debug print model, called once, before we terminate with sat/unknown. */ void debugPrintModel(); @@ -339,7 +338,7 @@ class Instantiate : public QuantifiersUtil */ std::map > d_recordedInst; /** statistics for debugging total instantiations per quantifier per round */ - std::map d_temp_inst_debug; + std::map d_instDebugTemp; /** list of all instantiations produced for each quantifier * -- cgit v1.2.3