diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-14 01:41:24 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-13 23:41:24 -0700 |
commit | 1cd3c3c5dad84093aa6b2db164798c8fff473fec (patch) | |
tree | 2cb4fe22f3ca9c97cf93c77aa50c5d08b30dc7d0 /src/theory/quantifiers | |
parent | 34043bdcd93860969cfd9e87c683340175c640b9 (diff) |
Debug instantiations output (#4739)
This prints # instantiations per round (during solving) for each quantified formula with `--debug-inst`, giving output like this:
```
(num-instantiations myQuant1 1)
(num-instantiations myQuant2 1)
unsat
```
It also changes the default value of print-inst-full to match the behavior of unsat-cores vs unsat-cores-full (by default, nameless quantifiers are ignored).
It fixes an issue with qid, where mkVar was accidentally used instead of mkConst, leading to assertion failures in debug. Marking major since this fixes debug regress1.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/instantiate.cpp | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/instantiate.h | 8 |
2 files changed, 21 insertions, 3 deletions
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index deed76fc9..c9048fc95 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -783,7 +783,7 @@ Node Instantiate::getInstantiatedConjunction(Node q) return ret; } -void Instantiate::debugPrint() +void Instantiate::debugPrint(std::ostream& out) { // debug information if (Trace.isOn("inst-per-quant-round")) @@ -795,6 +795,20 @@ void Instantiate::debugPrint() d_temp_inst_debug[i.first] = 0; } } + if (options::debugInst()) + { + bool isFull = options::printInstFull(); + for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug) + { + std::stringstream ss; + if (!printQuant(i.first, ss, isFull)) + { + continue; + } + out << "(num-instantiations " << ss.str() << " " << i.second << ")" + << std::endl; + } + } } void Instantiate::debugPrintModel() diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 630efe72c..16ff1f2c3 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -202,8 +202,12 @@ class Instantiate : public QuantifiersUtil Node getTermForType(TypeNode tn); //--------------------------------------end general utilities - /** debug print, called once per instantiation round. */ - void debugPrint(); + /** + * Debug print, called once per 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); /** debug print model, called once, before we terminate with sat/unknown. */ void debugPrintModel(); |