diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-21 12:09:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-21 12:09:33 -0500 |
| commit | 44fd0bd8441d9dcce5aa9173757c9d8173924c17 (patch) | |
| tree | db47d0c29fffeca7301d83ab6ef4320ccd37701b /src/theory/arrays/theory_arrays.h | |
| parent | 63e7c6bb6d9c99a5282241be8b32a04ea67dfb8d (diff) | |
(proof-new) Add the arrays proof checker (#5047)
Includes adding the standard method for constructing the extensionality skolem using the skolem manager.
Diffstat (limited to 'src/theory/arrays/theory_arrays.h')
| -rw-r--r-- | src/theory/arrays/theory_arrays.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index dea3d4136..a35074f15 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -26,6 +26,7 @@ #include "context/cdhashset.h" #include "context/cdqueue.h" #include "theory/arrays/array_info.h" +#include "theory/arrays/proof_checker.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -341,6 +342,9 @@ class TheoryArrays : public Theory { /** The notify class for d_equalityEngine */ NotifyClass d_notify; + /** The proof checker */ + ArraysProofRuleChecker d_pchecker; + /** Conflict when merging constants */ void conflict(TNode a, TNode b); |