diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-26 12:18:26 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-26 12:18:26 -0500 |
| commit | d7ef769395f75b7acae3dd36df587a4438db5673 (patch) | |
| tree | defd160b2d8c73bb4bff5b0fc6bdf9ed0541befb /src/theory/theory.cpp | |
| parent | 0a4ee1ac60e6b914ca8173c773eb9db54cdf0f61 (diff) | |
Send external equalities from collapse selector as lemmas (#5346)
In 20e58d4, a policy change was made for datatypes to keep more inferences as internal facts.
This leads to a crash (issue #5344) where the equality status of two BV terms is asked by TheoryDatatypes, where the TheoryBV was not informed of the term, as datatypes kept it internal.
This refines the policy further such that the collapse selector rule is processed as a lemma for terms of external type. The reason is that this rule may generate new terms of external type. Other rules like unification retain the internal fact policy, as they do not generate new terms.
Fixes #5344.
FYI @barrettcw
Diffstat (limited to 'src/theory/theory.cpp')
| -rw-r--r-- | src/theory/theory.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 681f3bca1..78fe6927f 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -437,6 +437,7 @@ EqualityStatus Theory::getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; } + Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl; Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b)); // Check for equality (simplest) |