Remove spurious theory methods calls (#4931)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 21 Aug 2020 20:58:46 +0000 (15:58 -0500)
committerGitHub <noreply@github.com>
Fri, 21 Aug 2020 20:58:46 +0000 (15:58 -0500)
commit05c6ae0bda064083efb7941e1ceb0869cb1b1090
treefb9497cf16421d7488b31bc7e702ea0826e61aa6
parentb8301cde27c455c8da3e9017072a577a0816939b
Remove spurious theory methods calls (#4931)

This PR removes spurious theory method calls that are not implemented.

It also renames a common "propagate(TNode lit)" pattern to "propagateLit(TNode lit)" to avoid confusion with "propagate(Effort e)".
20 files changed:
src/theory/arrays/kinds
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/datatypes/kinds
src/theory/datatypes/theory_datatypes.cpp
src/theory/datatypes/theory_datatypes.h
src/theory/sep/kinds
src/theory/sep/theory_sep.cpp
src/theory/sep/theory_sep.h
src/theory/sets/kinds
src/theory/sets/theory_sets.cpp
src/theory/sets/theory_sets.h
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/strings/kinds
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/uf/kinds
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h