diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-20 15:50:38 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-20 15:50:38 -0500 |
| commit | 01a9d18f2b2ce20cf7a0672a865cf0c2873d6f6a (patch) | |
| tree | 52e7dfc5d157b11fa4bd00855ad46238b6615338 /src/theory/arith/theory_arith.h | |
| parent | c110363ccf39c9415c1a32bda6273fe8221db182 (diff) | |
Add TheoryState objects to each Theory (#4920)
This initializes all theories with a TheoryState object (apart from bool and builtin which do not require one).
Two additional theories are known to require special state objects: TheoryArith, which has a custom way of detecting when in conflict, and TheoryQuantifiers, which can leverage a special state object for the purposes of refactoring and splitting apart QuantifiersEngine further. All other theories use default TheoryState objects.
Notice this PR does not update the theories to use these states yet, it simply adds the objects.
Diffstat (limited to 'src/theory/arith/theory_arith.h')
| -rw-r--r-- | src/theory/arith/theory_arith.h | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index ad3b91b07..d0147fe9f 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -17,11 +17,11 @@ #pragma once -#include "theory/theory.h" #include "expr/node.h" #include "proof/arith_proof_recorder.h" +#include "theory/arith/arith_state.h" #include "theory/arith/theory_arith_private_forward.h" - +#include "theory/theory.h" namespace CVC4 { namespace theory { @@ -115,6 +115,9 @@ class TheoryArith : public Theory { d_proofRecorder = proofRecorder; } + private: + /** The state object wrapping TheoryArithPrivate */ + ArithState d_astate; };/* class TheoryArith */ }/* CVC4::theory::arith namespace */ |