summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_split.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2021-03-26 11:47:22 -0500
committerGitHub <noreply@github.com>2021-03-26 11:47:22 -0500
commit72f70f1573651bcbf5f327c7a3411ece0e607e3f (patch)
treed2e57f33fdbb6a260b0f523aa4cf2b621474e374 /src/theory/quantifiers/quant_split.h
parentfa6c3db414d27f47e0bee55480df939e78c14eb3 (diff)
Pass term registry to quantifiers modules (#6216)
Diffstat (limited to 'src/theory/quantifiers/quant_split.h')
-rw-r--r--src/theory/quantifiers/quant_split.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index d91b00146..13af881ee 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.h
@@ -52,7 +52,8 @@ class QuantDSplit : public QuantifiersModule {
QuantDSplit(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantifiersRegistry& qr);
+ QuantifiersRegistry& qr,
+ TermRegistry& tr);
/** determine whether this quantified formula will be reduced */
void checkOwnership(Node q) override;
/* whether this module needs to check this round */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback