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.cpp | |
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.cpp')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index a73425a80..1378b4edf 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -250,11 +250,17 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { return newId; } -void EqualityEngine::addFunctionKind(Kind fun, bool interpreted) { +void EqualityEngine::addFunctionKind(Kind fun, bool interpreted, bool extOperator) { d_congruenceKinds |= fun; - if (interpreted && fun != kind::EQUAL) { - Debug("equality::evaluation") << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted " << std::endl; - d_congruenceKindsInterpreted |= fun; + if (fun != kind::EQUAL) { + if (interpreted) { + Debug("equality::evaluation") << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted " << std::endl; + d_congruenceKindsInterpreted |= fun; + } + if (extOperator) { + Debug("equality::extoperator") << d_name << "::eq::addFunctionKind(): " << fun << " is an external operator kind " << std::endl; + d_congruenceKindsExtOperators |= fun; + } } } @@ -297,7 +303,7 @@ void EqualityEngine::addTermInternal(TNode t, bool isOperator) { } else if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) { TNode tOp = t.getOperator(); // Add the operator - addTermInternal(tOp, true); + addTermInternal(tOp, !isExternalOperatorKind(t.getKind())); result = getNodeId(tOp); // Add all the children and Curryfy bool isInterpreted = isInterpretedFunctionKind(t.getKind()); |