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/quantifiers | |
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/quantifiers')
-rw-r--r-- | src/theory/quantifiers/quantifiers_state.cpp | 30 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_state.h | 40 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 4 |
4 files changed, 77 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quantifiers_state.cpp b/src/theory/quantifiers/quantifiers_state.cpp new file mode 100644 index 000000000..67fad6f64 --- /dev/null +++ b/src/theory/quantifiers/quantifiers_state.cpp @@ -0,0 +1,30 @@ +/********************* */ +/*! \file quantifiers_state.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utility for quantifiers state + **/ + +#include "theory/quantifiers/quantifiers_state.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +QuantifiersState::QuantifiersState(context::Context* c, + context::UserContext* u, + Valuation val) + : TheoryState(c, u, val) +{ +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/quantifiers_state.h b/src/theory/quantifiers/quantifiers_state.h new file mode 100644 index 000000000..a6611e734 --- /dev/null +++ b/src/theory/quantifiers/quantifiers_state.h @@ -0,0 +1,40 @@ +/********************* */ +/*! \file quantifiers_state.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utility for quantifiers state + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H +#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H + +#include "theory/theory_state.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** + * The quantifiers state. + */ +class QuantifiersState : public TheoryState +{ + public: + QuantifiersState(context::Context* c, context::UserContext* u, Valuation val); + ~QuantifiersState() {} +}; + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_STATE_H */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 04e83032b..261fd65e6 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -42,7 +42,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, Valuation valuation, const LogicInfo& logicInfo, ProofNodeManager* pnm) - : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm) + : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm), + d_qstate(c, u, valuation) { out.handleUserAttribute( "fun-def", this ); out.handleUserAttribute( "sygus", this ); @@ -59,6 +60,8 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, // add the proof rules d_qChecker.registerTo(pc); } + // indicate we are using the quantifiers theory state object + d_theoryState = &d_qstate; } TheoryQuantifiers::~TheoryQuantifiers() { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index c378f3537..6f8256c21 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -24,9 +24,9 @@ #include "theory/output_channel.h" #include "theory/quantifiers/proof_checker.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/quantifiers/quantifiers_state.h" #include "theory/theory.h" #include "theory/valuation.h" -#include "util/statistics_registry.h" namespace CVC4 { namespace theory { @@ -69,6 +69,8 @@ class TheoryQuantifiers : public Theory { QuantifiersRewriter d_rewriter; /** The proof rule checker */ QuantifiersProofRuleChecker d_qChecker; + /** The quantifiers state */ + QuantifiersState d_qstate; };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ |