diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-01 10:07:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-01 10:07:39 -0500 |
| commit | bdf46b42d6bd66121a5b5175a81408cd64d7ecfa (patch) | |
| tree | 2aae6c707375616964afd88437be3b48f1dbe45a /src/theory/quantifiers/instantiate.h | |
| parent | d288f52dd82fe6590950758289e86ebcb039350d (diff) | |
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.
Diffstat (limited to 'src/theory/quantifiers/instantiate.h')
| -rw-r--r-- | src/theory/quantifiers/instantiate.h | 7 |
1 files changed, 3 insertions, 4 deletions
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<Node, std::vector<Node> > d_recordedInst; /** statistics for debugging total instantiations per quantifier per round */ - std::map<Node, uint32_t> d_temp_inst_debug; + std::map<Node, uint32_t> d_instDebugTemp; /** list of all instantiations produced for each quantifier * |