diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-24 13:13:06 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-24 13:13:06 -0600 |
| commit | 36b5281d3a4d58df5a4e68eca3d41568f1650769 (patch) | |
| tree | 9fe99b5e64322f0cb6c7b567393c05fcea29306f /src/theory/quantifiers/ematching/ho_trigger.h | |
| parent | 9d8a3b458b11961026ee1e58782ff073de29f93b (diff) | |
Initial cleaning of triggers (#5795)
In preparation for splitting trigger.h/cpp into multiple files.
This updates the code to conform to guidelines. No major changes, apart from a heuristic related to "pure theory triggers" is deleted and simplified.
Diffstat (limited to 'src/theory/quantifiers/ematching/ho_trigger.h')
| -rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index a369aa7c5..d9636cd65 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -122,7 +122,7 @@ class HigherOrderTrigger : public Trigger * Extends Trigger::addInstantiations to also send * lemmas based on addHoTypeMatchPredicateLemmas. */ - int addInstantiations() override; + uint64_t addInstantiations() override; protected: /** @@ -158,7 +158,7 @@ class HigherOrderTrigger : public Trigger * * TODO: we may eliminate this based on how github issue #1115 is resolved. */ - int addHoTypeMatchPredicateLemmas(); + uint64_t addHoTypeMatchPredicateLemmas(); /** send instantiation * * Sends an instantiation that is equivalent to m via |