summaryrefslogtreecommitdiff
path: root/src/theory/sets/theory_sets.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-08-12 09:18:24 -0500
committerGitHub <noreply@github.com>2020-08-12 09:18:24 -0500
commitc5a7dc772788ea3f1d568da0d8ef4effca080b9c (patch)
tree09fa1ad24590ed4512cbc22ee71c9c813ad6408a /src/theory/sets/theory_sets.h
parent558ceb2f64877fa2cc5f1cd448147e529b5c1c02 (diff)
Fix connection to master equality engine in sets (#4877)
This corrects an issue introduced by a merge of a previous commit (b5b2858) which dropped the connection from sets to its master equality engine. Fixes several issues in sets regressions, including a timeout in regress0.
Diffstat (limited to 'src/theory/sets/theory_sets.h')
-rw-r--r--src/theory/sets/theory_sets.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index f1b59e419..505ba9547 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -65,6 +65,7 @@ class TheorySets : public Theory
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
void presolve() override;
void propagate(Effort) override;
+ void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
bool isEntailed(Node n, bool pol);
/* equality engine */
virtual eq::EqualityEngine* getEqualityEngine() override;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback