(proof-new) Add interface for trusted substitution and update ppAssert (#5193)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 6 Oct 2020 15:02:54 +0000 (10:02 -0500)
committerGitHub <noreply@github.com>
Tue, 6 Oct 2020 15:02:54 +0000 (10:02 -0500)
commit2d8889f935ca78ef4a5555f0e6bbed76dbc559d7
tree2d83522cd3d1e0d711773a45de0d2be2952dbb7c
parent6d663abe421c07976755c224180b1a1ee93442f6
(proof-new) Add interface for trusted substitution and update ppAssert (#5193)

The current work on proof-new involves proofs for preprocessing. The biggest issue currently is that our preprocessing passes do not track proofs for substitutions.

This adds a "trusted substitution" class with is a layer on substitution map. The proof aspect of this class is not yet implemented, this PR just adds its interface.

This also updates Theory::ppAssert to take a TrustSubstitutionMap instead of a SubstitutionMap, since eventually we will require proofs to be provided for substitutions that are added to this map.
27 files changed:
src/CMakeLists.txt
src/preprocessing/passes/miplib_trick.cpp
src/preprocessing/passes/non_clausal_simp.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/booleans/theory_bool.cpp
src/theory/booleans/theory_bool.h
src/theory/bv/bv_solver.h
src/theory/bv/bv_solver_lazy.cpp
src/theory/bv/bv_solver_lazy.h
src/theory/bv/bv_solver_simple.h
src/theory/bv/theory_bv.cpp
src/theory/bv/theory_bv.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/theory.cpp
src/theory/theory.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/trust_substitutions.cpp [new file with mode: 0644]
src/theory/trust_substitutions.h [new file with mode: 0644]