diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/CMakeLists.txt | 4 | ||||
-rw-r--r-- | src/theory/arith/arith_state.cpp | 38 | ||||
-rw-r--r-- | src/theory/arith/arith_state.h | 57 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 6 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.h | 7 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.h | 15 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.cpp | 5 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.cpp | 6 | ||||
-rw-r--r-- | src/theory/bv/theory_bv.h | 2 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 6 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.cpp | 5 | ||||
-rw-r--r-- | src/theory/fp/theory_fp.h | 2 | ||||
-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 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 6 | ||||
-rw-r--r-- | src/theory/sep/theory_sep.h | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 5 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 2 |
22 files changed, 234 insertions, 17 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f1e01a7cb..f9d7f833e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -292,6 +292,8 @@ libcvc4_add_sources( theory/arith/arith_msum.h theory/arith/arith_rewriter.cpp theory/arith/arith_rewriter.h + theory/arith/arith_state.cpp + theory/arith/arith_state.h theory/arith/arith_static_learner.cpp theory/arith/arith_static_learner.h theory/arith/arith_utilities.cpp @@ -604,6 +606,8 @@ libcvc4_add_sources( theory/quantifiers/quantifiers_attributes.h theory/quantifiers/quantifiers_rewriter.cpp theory/quantifiers/quantifiers_rewriter.h + theory/quantifiers/quantifiers_state.cpp + theory/quantifiers/quantifiers_state.h theory/quantifiers/query_generator.cpp theory/quantifiers/query_generator.h theory/quantifiers/relevant_domain.cpp diff --git a/src/theory/arith/arith_state.cpp b/src/theory/arith/arith_state.cpp new file mode 100644 index 000000000..c4678fab1 --- /dev/null +++ b/src/theory/arith/arith_state.cpp @@ -0,0 +1,38 @@ +/********************* */ +/*! \file arith_state.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Arithmetic theory state. + **/ + +#include "theory/arith/arith_state.h" + +#include "theory/arith/theory_arith_private.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +ArithState::ArithState(TheoryArithPrivate& parent, + context::Context* c, + context::UserContext* u, + Valuation val) + : TheoryState(c, u, val), d_parent(parent) +{ +} + +bool ArithState::isInConflict() const +{ + return d_parent.anyConflict() || d_conflict; +} + +} // namespace arith +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h new file mode 100644 index 000000000..5d775755b --- /dev/null +++ b/src/theory/arith/arith_state.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file arith_state.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 Arithmetic theory state. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__ARITH__ARITH_STATE_H +#define CVC4__THEORY__ARITH__ARITH_STATE_H + +#include "theory/theory_state.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +class TheoryArithPrivate; + +/** + * The arithmetic state. + * + * Note this object is intended to use TheoryArithPrivate + * as a black box, and moreover the internals of TheoryArithPrivate will not + * be refactored to use this state. Instead, the main theory solver TheoryArith + * will be refactored to be a standard layer on top of TheoryArithPrivate, + * which will include using this state in the standard way. + */ +class ArithState : public TheoryState +{ + public: + ArithState(TheoryArithPrivate& parent, + context::Context* c, + context::UserContext* u, + Valuation val); + ~ArithState() {} + /** Are we currently in conflict? */ + bool isInConflict() const override; + + private: + /** reference to parent */ + TheoryArithPrivate& d_parent; +}; + +} // namespace arith +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b95b5e243..4e0582f50 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -41,9 +41,13 @@ TheoryArith::TheoryArith(context::Context* c, d_internal( new TheoryArithPrivate(*this, c, u, out, valuation, logicInfo, pnm)), d_ppRewriteTimer("theory::arith::ppRewriteTimer"), - d_proofRecorder(nullptr) + d_proofRecorder(nullptr), + d_astate(*d_internal, c, u, valuation) { smtStatisticsRegistry()->registerStat(&d_ppRewriteTimer); + + // indicate we are using the theory state object + d_theoryState = &d_astate; } TheoryArith::~TheoryArith(){ 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 */ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 4c4aedf00..d96b5e2d3 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -324,17 +324,20 @@ public: /** This is a conflict that is magically known to hold. */ void raiseBlackBoxConflict(Node bb); -private: + /** + * Returns true iff a conflict has been raised. This method is public since + * it is needed by the ArithState class to know whether we are in conflict. + */ + bool anyConflict() const + { + return !conflictQueueEmpty() || !d_blackBoxConflict.get().isNull(); + } + private: inline bool conflictQueueEmpty() const { return d_conflicts.empty(); } - /** Returns true iff a conflict has been raised. */ - inline bool anyConflict() const { - return !conflictQueueEmpty() || !d_blackBoxConflict.get().isNull(); - } - /** * Outputs the contents of d_conflicts onto d_out. * The conditions of anyConflict() must hold. diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 4cc51a87e..9c1e22940 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -82,7 +82,7 @@ TheoryArrays::TheoryArrays(context::Context* c, name + "theory::arrays::number of setModelVal conflicts", 0), d_ppEqualityEngine(u, name + "theory::arrays::pp", true), d_ppFacts(u), - // d_ppCache(u), + d_state(c, u, valuation), d_literalsToPropagate(c), d_literalsToPropagateIndex(c, 0), d_isPreRegistered(c), @@ -132,6 +132,9 @@ TheoryArrays::TheoryArrays(context::Context* c, // The preprocessing congruence kinds d_ppEqualityEngine.addFunctionKind(kind::SELECT); d_ppEqualityEngine.addFunctionKind(kind::STORE); + + // indicate we are using the default theory state object + d_theoryState = &d_state; } TheoryArrays::~TheoryArrays() { diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index b69450ac4..2d09c55fe 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -194,6 +194,8 @@ class TheoryArrays : public Theory { /** The theory rewriter for this theory. */ TheoryArraysRewriter d_rewriter; + /** A (default) theory state object */ + TheoryState d_state; public: PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override; diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index ced320d92..2c095e198 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -74,7 +74,8 @@ TheoryBV::TheoryBV(context::Context* c, d_calledPreregister(false), d_needsLastCallCheck(false), d_extf_range_infer(u), - d_extf_collapse_infer(u) + d_extf_collapse_infer(u), + d_state(c, u, valuation) { d_extTheory->addFunctionKind(kind::BITVECTOR_TO_NAT); d_extTheory->addFunctionKind(kind::INT_TO_BITVECTOR); @@ -109,6 +110,9 @@ TheoryBV::TheoryBV(context::Context* c, } d_subtheories.emplace_back(bb_solver); d_subtheoryMap[SUB_BITBLAST] = bb_solver; + + // indicate we are using the default theory state object + d_theoryState = &d_state; } TheoryBV::~TheoryBV() {} diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 0e8877359..11440cb81 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -275,6 +275,8 @@ class TheoryBV : public Theory { /** The theory rewriter for this theory. */ TheoryBVRewriter d_rewriter; + /** A (default) theory state object */ + TheoryState d_state; friend class LazyBitblaster; friend class TLazyBitblaster; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index ee750e646..08ec4322e 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -61,12 +61,16 @@ TheoryDatatypes::TheoryDatatypes(Context* c, d_functionTerms(c), d_singleton_eq(u), d_lemmas_produced_c(u), - d_sygusExtension(nullptr) + d_sygusExtension(nullptr), + d_state(c, u, valuation) { d_true = NodeManager::currentNM()->mkConst( true ); d_zero = NodeManager::currentNM()->mkConst( Rational(0) ); d_dtfCounter = 0; + + // indicate we are using the default theory state object + d_theoryState = &d_state; } TheoryDatatypes::~TheoryDatatypes() { diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 37848f10e..0465a7788 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -366,6 +366,8 @@ private: /** The theory rewriter for this theory. */ DatatypesRewriter d_rewriter; + /** A (default) theory state object */ + TheoryState d_state; };/* class TheoryDatatypes */ }/* CVC4::theory::datatypes namespace */ diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp index ff0855889..82086aafe 100644 --- a/src/theory/fp/theory_fp.cpp +++ b/src/theory/fp/theory_fp.cpp @@ -119,8 +119,11 @@ TheoryFp::TheoryFp(context::Context* c, d_toRealMap(u), realToFloatMap(u), floatToRealMap(u), - abstractionMap(u) + abstractionMap(u), + d_state(c, u, valuation) { + // indicate we are using the default theory state object + d_theoryState = &d_state; } /* TheoryFp::TheoryFp() */ TheoryRewriter* TheoryFp::getTheoryRewriter() { return &d_rewriter; } diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h index 2584d574e..ad052f92a 100644 --- a/src/theory/fp/theory_fp.h +++ b/src/theory/fp/theory_fp.h @@ -153,6 +153,8 @@ class TheoryFp : public Theory { /** The theory rewriter for this theory. */ TheoryFpRewriter d_rewriter; + /** A (default) theory state object */ + TheoryState d_state; }; /* class TheoryFp */ } // namespace fp 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 */ diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index edb5dd0ae..f75eb4472 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -47,6 +47,8 @@ TheorySep::TheorySep(context::Context* c, ProofNodeManager* pnm) : Theory(THEORY_SEP, c, u, out, valuation, logicInfo, pnm), d_lemmas_produced_c(u), + d_bounds_init(false), + d_state(c, u, valuation), d_notify(*this), d_conflict(c, false), d_reduce(u), @@ -56,7 +58,9 @@ TheorySep::TheorySep(context::Context* c, { d_true = NodeManager::currentNM()->mkConst<bool>(true); d_false = NodeManager::currentNM()->mkConst<bool>(false); - d_bounds_init = false; + + // indicate we are using the default theory state object + d_theoryState = &d_state; } TheorySep::~TheorySep() { diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index 40182fc19..b178b97db 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -58,6 +58,8 @@ class TheorySep : public Theory { bool d_bounds_init; TheorySepRewriter d_rewriter; + /** A (default) theory state object */ + TheoryState d_state; Node mkAnd( std::vector< TNode >& assumptions ); diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 7bca9da74..c8ae3d844 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -56,7 +56,8 @@ TheoryUF::TheoryUF(context::Context* c, d_ho(nullptr), d_conflict(c, false), d_functionsTerms(c), - d_symb(u, instanceName) + d_symb(u, instanceName), + d_state(c, u, valuation) { d_true = NodeManager::currentNM()->mkConst( true ); @@ -65,6 +66,8 @@ TheoryUF::TheoryUF(context::Context* c, { d_ufProofChecker.registerTo(pc); } + // indicate we are using the default theory state object + d_theoryState = &d_state; } TheoryUF::~TheoryUF() { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 414a2dd6a..4d0a3126f 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -219,6 +219,8 @@ private: TheoryUfRewriter d_rewriter; /** Proof rule checker */ UfProofRuleChecker d_ufProofChecker; + /** A (default) theory state object */ + TheoryState d_state; };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ |