diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-13 16:08:01 -0500 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2017-09-13 14:08:01 -0700 |
commit | 85a1160aa4cced39808e3e73ceff0e0b5ddc6f66 (patch) | |
tree | a1e4dfc3fe59f5af0bf5e6bff581f61fcbe9e2e4 /src/theory/uf/equality_engine.h | |
parent | 3a00b0c4586ef61c93b7b7320cce4d720014f2bf (diff) |
Modify equality engine to allow operators to be marked as external terms (#1082)
This is required for reasoning higher-order, since we may have equalities between functions, which are operators of APPLY_UF terms.
This commit gets around the previous 1% slowdown by modifying the changes to the equality engine to be minimal impact. Previously the "isInternal" flag could be reset to false after a term is marked as internal=true. This provides an interface for whether operators of a kind should be marked as internal=false from the start. When using higher-order, APPLY_UF operators will be marked as being external when the higher-order option ufHo is set to true.
This has <.001% impact on performance on QF smtlib : https://www.starexec.org/starexec/secure/details/job.jsp?id=24445
Diffstat (limited to 'src/theory/uf/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 5be32ab90..9638b9f09 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -230,6 +230,9 @@ private: /** The map of kinds to be treated as interpreted function applications (for evaluation of constants) */ KindMap d_congruenceKindsInterpreted; + /** The map of kinds with operators to be considered external (for higher-order) */ + KindMap d_congruenceKindsExtOperators; + /** Objects that need to be notified during equality path reconstruction */ std::map<unsigned, const PathReconstructionNotify*> d_pathReconstructionTriggers; @@ -714,9 +717,13 @@ public: } /** - * Add a kind to treat as function applications. + * Add a kind to treat as function applications. + * When extOperator is true, this equality engine will treat the operators of this kind + * as "external" e.g. not internal nodes (see d_isInternal). This means that we will + * consider equivalence classes containing the operators of such terms, and "hasTerm" will + * return true. */ - void addFunctionKind(Kind fun, bool interpreted = false); + void addFunctionKind(Kind fun, bool interpreted = false, bool extOperator = false); /** * Returns true if this kind is used for congruence closure. @@ -733,6 +740,13 @@ public: } /** + * Returns true if this kind has an operator that is considered external (e.g. not internal). + */ + bool isExternalOperatorKind(Kind fun) const { + return d_congruenceKindsExtOperators.tst(fun); + } + + /** * Check whether the node is already in the database. */ bool hasTerm(TNode t) const; |