Simplify lemma interface (#5819)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 28 Jan 2021 20:01:26 +0000 (14:01 -0600)
committerGitHub <noreply@github.com>
Thu, 28 Jan 2021 20:01:26 +0000 (14:01 -0600)
commite234ff58f561ac97642df15c698962faa9d1e5e4
treecfac18adaeb0fccc348b81e84c854400d38a01fe
parent3234db430074e278258e6d687c07146a59769a92
Simplify lemma interface (#5819)

This makes it so that TheoryEngine::lemma returns void not LemmaStatus.

Currently, there was only one use of LemmaStatus by theory solvers, which was CEGQI using it as a way of getting the preprocessed form of a lemma. This makes it so that there is an explicit method in Valuation for getting the preprocessed form of a term + its skolems and their definition assertions.

It also simplifies a few things, e.g. Valuation calls are forwarded to PropEngine instead of going through TheoryEngine. It fixes a few issues in TermFormulaRemoval related to getSkolems.
22 files changed:
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/prop/theory_proxy.h
src/smt/term_formula_removal.cpp
src/smt/term_formula_removal.h
src/theory/combination_care_graph.cpp
src/theory/combination_engine.cpp
src/theory/combination_engine.h
src/theory/engine_output_channel.cpp
src/theory/engine_output_channel.h
src/theory/fp/theory_fp.cpp
src/theory/output_channel.cpp
src/theory/output_channel.h
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/theory_test_utils.h
src/theory/valuation.cpp
src/theory/valuation.h
test/unit/theory/theory_engine_white.h
test/unit/theory/theory_white.h