summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt4
-rw-r--r--src/theory/arith/arith_state.cpp38
-rw-r--r--src/theory/arith/arith_state.h57
-rw-r--r--src/theory/arith/theory_arith.cpp6
-rw-r--r--src/theory/arith/theory_arith.h7
-rw-r--r--src/theory/arith/theory_arith_private.h15
-rw-r--r--src/theory/arrays/theory_arrays.cpp5
-rw-r--r--src/theory/arrays/theory_arrays.h2
-rw-r--r--src/theory/bv/theory_bv.cpp6
-rw-r--r--src/theory/bv/theory_bv.h2
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp6
-rw-r--r--src/theory/datatypes/theory_datatypes.h2
-rw-r--r--src/theory/fp/theory_fp.cpp5
-rw-r--r--src/theory/fp/theory_fp.h2
-rw-r--r--src/theory/quantifiers/quantifiers_state.cpp30
-rw-r--r--src/theory/quantifiers/quantifiers_state.h40
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp5
-rw-r--r--src/theory/quantifiers/theory_quantifiers.h4
-rw-r--r--src/theory/sep/theory_sep.cpp6
-rw-r--r--src/theory/sep/theory_sep.h2
-rw-r--r--src/theory/uf/theory_uf.cpp5
-rw-r--r--src/theory/uf/theory_uf.h2
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback