diff options
Diffstat (limited to 'src/theory/quantifiers/equality_query.h')
| -rw-r--r-- | src/theory/quantifiers/equality_query.h | 29 |
1 files changed, 13 insertions, 16 deletions
diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 1000b97e9..7766a335a 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -27,22 +27,19 @@ namespace theory { namespace quantifiers { /** EqualityQueryQuantifiersEngine class -* This is a wrapper class around an equality engine that is used for -* queries required by algorithms in the quantifiers theory. -* It uses an equality engine, as determined by the quantifiers engine it points -* to. -* -* The main extension of this class wrt EqualityQuery is the function -* getInternalRepresentative, which is used by instantiation-based methods -* that are agnostic with respect to choosing terms within an equivalence class. -* Examples of such methods are finite model finding and enumerative -* instantiation. -* Method getInternalRepresentative returns the "best" representative based on -* the internal heuristic, -* which is currently based on choosing the term that was previously chosen as a -* representative -* earliest. -*/ + * + * This is a wrapper class around an equality engine that is used for + * queries required by algorithms in the quantifiers theory. It uses an equality + * engine, as determined by the quantifiers engine it points to. + * + * The main extension of this class wrt EqualityQuery is the function + * getInternalRepresentative, which is used by instantiation-based methods + * that are agnostic with respect to choosing terms within an equivalence class. + * Examples of such methods are finite model finding and enumerative + * instantiation. Method getInternalRepresentative returns the "best" + * representative based on the internal heuristic, which is currently based on + * choosing the term that was previously chosen as a representative earliest. + */ class EqualityQueryQuantifiersEngine : public EqualityQuery { public: |