[proof-new] Registering proof checkers uniformly from the SMT solver (#6275)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Mon, 5 Apr 2021 18:47:40 +0000 (15:47 -0300)
committerGitHub <noreply@github.com>
Mon, 5 Apr 2021 18:47:40 +0000 (18:47 +0000)
commitb75f48683c08e66e0d47d29c5262f32f33b36c49
tree0a76b276add9a8d0acd3a52167747e5664f12569
parentca5fd891038a93bd63b3863faa8c5e39fff88ed0
[proof-new] Registering proof checkers uniformly from the SMT solver (#6275)

Each theory has its own proof checker, responsible for checking the rules pertaining to that theory. The main proof checker uses these specialized checkers. Previously the main proof checker (of the proof node manager used across the SMT solver) was connected to these theory proof checkers during initialization of the theory. This commit adds an interface to the theories for retrieving its proof checker (analogous to how one retrieves the rewriter of a theory) which is used by a new method in the theory engine to register a theory proof checker to a given proof checker according to a theory id.

This is in preparation for the new unsat cores based on proofs.
35 files changed:
src/smt/smt_solver.cpp
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_private.cpp
src/theory/arith/theory_arith_private.h
src/theory/arrays/theory_arrays.cpp
src/theory/arrays/theory_arrays.h
src/theory/bags/theory_bags.cpp
src/theory/bags/theory_bags.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/bv_solver_simple.cpp
src/theory/bv/bv_solver_simple.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/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/theory_uf.cpp
src/theory/uf/theory_uf.h
test/unit/test_smt.h