Limit trigger terms to shared terms in arrays (#4932)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 21 Aug 2020 22:53:46 +0000 (17:53 -0500)
committerGitHub <noreply@github.com>
Fri, 21 Aug 2020 22:53:46 +0000 (15:53 -0700)
commit9ea213066b989a8154b1ebd40ebea3bc7e18c42d
treec4179264e0f6407d161fc1187a6e2d0c3110a278
parent05c6ae0bda064083efb7941e1ceb0869cb1b1090
Limit trigger terms to shared terms in arrays (#4932)

There is a non-standard use of trigger terms in the array theory via `EqualityEngine::addTriggerTerm`.

Trigger terms are only supposed to be shared terms, and are added to the equality engine for the sake of propagating equalities between shared terms.  The array theory does two non-standard things:
(1) it registers (possibly) non-shared terms as triggers in its `preRegisterInternal` method,
(2) it filters propagations between anything except non-shared arrays in its `eqNotifyTriggerTermEquality` method.

The latter is only necessary because of the former.  It is unnecessary to do *either* of these things. Instead, the array theory should simply add the terms to the equality engine (as non-triggers) during preRegisterInternal.  Note that it additionally correctly adds trigger terms in its `notifySharedTerm` method.

With this commit, the array theory uses the equality engine (wrt propagation) in a standard way.
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h