diff options
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 * |