(proof-new) Update Theory interface for proof-new (#4648)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 11 Jul 2020 00:03:24 +0000 (19:03 -0500)
committerGitHub <noreply@github.com>
Sat, 11 Jul 2020 00:03:24 +0000 (19:03 -0500)
commitc5a6aa2e03b05a5db6150563a4d5994abf5b24e9
treec15020e9c60baafd1fa285be3d7488b06ea688be
parent88da95573d600f2af8538c3c5a29459a1146127c
(proof-new) Update Theory interface for proof-new (#4648)

This includes 4 changes:

Theory constructor takes a ProofNodeManager,
Theory::explain returns a TrustNode (of kind PROP_EXP),
Theory::expandDefinitions returns a TrustNode (of kind REWRITE),
Theory::ppRewrite returns a TrustNode (of kind REWRITE).
These are all currently planned updates to the interface of Theory.
This PR also connects some of the existing proof rule checkers into the proof checker, if one is provided to the constructor. It updates TheoryEngine and other places to process TrustNode in trivial ways (converting them into Node). These calls will later be updated as needed for proof support.

This PR is also contingent on the performance tests for proof-new on SMT-LIB.
35 files changed:
src/proof/theory_proof.cpp
src/smt/process_assertions.cpp
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/booleans/theory_bool.cpp
src/theory/booleans/theory_bool.h
src/theory/builtin/theory_builtin.cpp
src/theory/builtin/theory_builtin.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/quantifiers/theory_quantifiers.cpp
src/theory/quantifiers/theory_quantifiers.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/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.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/theory_engine.h
src/theory/theory_preprocessor.cpp
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h
test/unit/theory/theory_engine_white.h
test/unit/theory/theory_white.h