From 3234db430074e278258e6d687c07146a59769a92 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 28 Jan 2021 13:27:27 -0600 Subject: Use standard equality engine information in quantifiers state (#5824) This refactors quantifiers so that it uses the standard interfaces for setting up an equality engine and using it via TheoryState. This eliminates the need for several special interfaces including getMasterEqualityEngine, CombinationEngine::getCoreEqualityEngine, and most uses of EqualityQuery. --- src/theory/quantifiers/relevant_domain.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/theory/quantifiers/relevant_domain.h') diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 6da4ce75a..36364191c 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -84,7 +84,7 @@ class RelevantDomain : public QuantifiersUtil /** remove redundant terms for d_terms, removes * duplicates modulo equality. */ - void removeRedundantTerms( QuantifiersEngine * qe ); + void removeRedundantTerms(QuantifiersState& qs); /** is n in this relevant domain? */ bool hasTerm( Node n ) { return std::find( d_terms.begin(), d_terms.end(), n )!=d_terms.end(); } -- cgit v1.2.3