Extend the standard Theory template based on equality engine (#4929)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 24 Aug 2020 14:43:06 +0000 (09:43 -0500)
committerGitHub <noreply@github.com>
Mon, 24 Aug 2020 14:43:06 +0000 (09:43 -0500)
commit983f41ea94f68e90d24e353ae3fd1aca04ac56ff
tree511720f4a1431b7e5b77712cfbbc512d7311ad5b
parent413da163bd36c8a9651308d7249e9aaf811872af
Extend the standard Theory template based on equality engine (#4929)

Apart from { quantifiers, bool, builtin }, each Theory now has an official equality engine. This PR elaborates on the standard recommended template that Theory should follow, which applies to all theories, regardless of whether they have an equality engine.

This includes:

A standard check method. The Theory is now expected to implement 4 callbacks (preCheck, postCheck, preNotifyFact, notifyFact).
A standard collectModelInfo method. The Theory is now expected to implement 2 callbacks (computeRelevantTerms, collectModelValues).
Additionally, 2 more methods have an obvious default:
(1) getEqualityStatus, which returns information based on an equality engine if it exists,
(2) addSharedTerm, which adds the term as a trigger term to the equality engine of the theory if it exists. Notice that for the sake of more consistent naming, theories now implement notifySharedTerm (previously TheoryEngine called theory-independent addSharedTermInternal which called addSharedTerm, this is updated now to addSharedTerm/notifySharedTerm).

Other methods will not be standardized yet e.g. preRegisterTerm, since they vary per theory.

FYI @barrettcw

Each theory on the branch https://github.com/ajreynol/CVC4/tree/centralEe conforms to this template (e.g. they do not override check or collectModelInfo). The next step will be to pull the new implementation of each Theory from that branch.
21 files changed:
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.h
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/theory_datatypes.h
src/theory/fp/theory_fp.cpp
src/theory/fp/theory_fp.h
src/theory/sep/theory_sep.cpp
src/theory/sep/theory_sep.h
src/theory/sets/theory_sets.cpp
src/theory/sets/theory_sets.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory.cpp
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h