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.
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
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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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
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(){
#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 {
d_proofRecorder = proofRecorder;
}
+ private:
+ /** The state object wrapping TheoryArithPrivate */
+ ArithState d_astate;
};/* class TheoryArith */
}/* CVC4::theory::arith namespace */
/** 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.
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),
// 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() {
/** 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;
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);
}
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() {}
/** The theory rewriter for this theory. */
TheoryBVRewriter d_rewriter;
+ /** A (default) theory state object */
+ TheoryState d_state;
friend class LazyBitblaster;
friend class TLazyBitblaster;
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() {
/** The theory rewriter for this theory. */
DatatypesRewriter d_rewriter;
+ /** A (default) theory state object */
+ TheoryState d_state;
};/* class TheoryDatatypes */
}/* CVC4::theory::datatypes namespace */
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; }
/** The theory rewriter for this theory. */
TheoryFpRewriter d_rewriter;
+ /** A (default) theory state object */
+ TheoryState d_state;
}; /* class TheoryFp */
} // namespace fp
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
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 );
// add the proof rules
d_qChecker.registerTo(pc);
}
+ // indicate we are using the quantifiers theory state object
+ d_theoryState = &d_qstate;
}
TheoryQuantifiers::~TheoryQuantifiers() {
#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 {
QuantifiersRewriter d_rewriter;
/** The proof rule checker */
QuantifiersProofRuleChecker d_qChecker;
+ /** The quantifiers state */
+ QuantifiersState d_qstate;
};/* class TheoryQuantifiers */
}/* CVC4::theory::quantifiers namespace */
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),
{
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() {
bool d_bounds_init;
TheorySepRewriter d_rewriter;
+ /** A (default) theory state object */
+ TheoryState d_state;
Node mkAnd( std::vector< TNode >& assumptions );
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 );
{
d_ufProofChecker.registerTo(pc);
}
+ // indicate we are using the default theory state object
+ d_theoryState = &d_state;
}
TheoryUF::~TheoryUF() {
TheoryUfRewriter d_rewriter;
/** Proof rule checker */
UfProofRuleChecker d_ufProofChecker;
+ /** A (default) theory state object */
+ TheoryState d_state;
};/* class TheoryUF */
}/* CVC4::theory::uf namespace */
projects / cvc5.git / commitdiff