summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/arith_static_learner.cpp12
-rw-r--r--src/theory/arith/arith_static_learner.h8
-rw-r--r--src/theory/arith/theory_arith.cpp2
-rw-r--r--src/theory/arith/theory_arith.h3
-rw-r--r--src/theory/arrays/theory_arrays.cpp6
-rw-r--r--src/theory/arrays/theory_arrays.h6
-rw-r--r--src/theory/booleans/circuit_propagator.h2
-rw-r--r--src/theory/bv/theory_bv.h4
-rw-r--r--src/theory/shared_terms_database.h2
-rw-r--r--src/theory/theory_engine.h2
10 files changed, 24 insertions, 23 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 5b8d3befc..9ae7cd1c2 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -145,8 +145,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
break;
case CONST_RATIONAL:
// Mark constants as minmax
- d_minMap[n] = n.getConst<Rational>();
- d_maxMap[n] = n.getConst<Rational>();
+ d_minMap.insert(n, n.getConst<Rational>());
+ d_maxMap.insert(n, n.getConst<Rational>());
break;
case OR: {
// Look for things like "x = 0 OR x = 1" (that are defTrue) and
@@ -248,7 +248,7 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
DeltaRational min = std::min(first, second);
CDNodeToMinMaxMap::const_iterator minFind = d_minMap.find(n);
if (minFind == d_minMap.end() || (*minFind).second < min) {
- d_minMap[n] = min;
+ d_minMap.insert(n, min);
Node nGeqMin;
if (min.getInfinitesimalPart() == 0) {
nGeqMin = NodeBuilder<2>(kind::GEQ) << n << mkRationalNode(min.getNoninfinitesimalPart());
@@ -267,7 +267,7 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
DeltaRational max = std::max(first, second);
CDNodeToMinMaxMap::const_iterator maxFind = d_maxMap.find(n);
if (maxFind == d_maxMap.end() || (*maxFind).second > max) {
- d_maxMap[n] = max;
+ d_maxMap.insert(n, max);
Node nLeqMax;
if (max.getInfinitesimalPart() == 0) {
nLeqMax = NodeBuilder<2>(kind::LEQ) << n << mkRationalNode(max.getNoninfinitesimalPart());
@@ -398,7 +398,7 @@ void ArithStaticLearner::addBound(TNode n) {
/* fall through */
case kind::LEQ:
if (maxFind == d_maxMap.end() || (*maxFind).second > bound) {
- d_maxMap[n[0]] = bound;
+ d_maxMap.insert(n[0], bound);
Debug("arith::static") << "adding bound " << n << endl;
}
break;
@@ -407,7 +407,7 @@ void ArithStaticLearner::addBound(TNode n) {
/* fall through */
case kind::GEQ:
if (minFind == d_minMap.end() || (*minFind).second < bound) {
- d_minMap[n[0]] = bound;
+ d_minMap.insert(n[0], bound);
Debug("arith::static") << "adding bound " << n << endl;
}
break;
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index b047018e8..0de28c5ab 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -27,7 +27,7 @@
#include "context/context.h"
#include "context/cdlist.h"
-#include "context/cdhashmap.h"
+#include "context/cdtrail_hashmap.h"
#include <set>
namespace CVC4 {
@@ -41,8 +41,7 @@ private:
* (=> _ (= x c))
* where c is a constant.
*/
- //typedef __gnu_cxx::hash_map<Node, std::set<Node>, NodeHashFunction> VarToNodeSetMap;
- typedef context::CDHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap;
+ typedef context::CDTrailHashMap<Node, Node, NodeHashFunction> CDNodeToNodeListMap;
// The domain is an implicit list OR(x, OR(y, ..., FALSE ))
// or FALSE
CDNodeToNodeListMap d_miplibTrick;
@@ -50,8 +49,7 @@ private:
/**
* Map from a node to it's minimum and maximum.
*/
- //typedef __gnu_cxx::hash_map<Node, DeltaRational, NodeHashFunction> NodeToMinMaxMap;
- typedef context::CDHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap;
+ typedef context::CDTrailHashMap<Node, DeltaRational, NodeHashFunction> CDNodeToMinMaxMap;
CDNodeToMinMaxMap d_minMap;
CDNodeToMinMaxMap d_maxMap;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 6ec6c7090..d2814348a 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1369,7 +1369,7 @@ Constraint TheoryArith::constraintFromFactQueue(){
if(assertion != reAssertion){
Debug("arith::nf") << "getting non-nf assertion " << assertion << " |-> " << reAssertion << endl;
Assert(constraint != NullConstraint);
- d_assertionsThatDoNotMatchTheirLiterals[assertion] = constraint;
+ d_assertionsThatDoNotMatchTheirLiterals.insert(assertion, constraint);
}
}
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 6a83c501b..b791186cf 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -22,6 +22,7 @@
#include "context/context.h"
#include "context/cdlist.h"
#include "context/cdhashset.h"
+#include "context/cdinsert_hashmap.h"
#include "context/cdqueue.h"
#include "expr/node.h"
@@ -135,7 +136,7 @@ private:
* A superset of all of the assertions that currently are not the literal for
* their constraint do not match constraint literals. Not just the witnesses.
*/
- context::CDHashMap<TNode, Constraint, TNodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals;
+ context::CDInsertHashMap<Node, Constraint, NodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals;
/**
* (For the moment) the type hierarchy goes as:
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index a05d30517..aabd3a62d 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -537,7 +537,7 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) {
void TheoryArrays::computeCareGraph()
{
if (d_sharedArrays.size() > 0) {
- context::CDHashSet<TNode, TNodeHashFunction>::iterator it1 = d_sharedArrays.begin(), it2, iend = d_sharedArrays.end();
+ CDNodeSet::key_iterator it1 = d_sharedArrays.key_begin(), it2, iend = d_sharedArrays.key_end();
for (; it1 != iend; ++it1) {
for (it2 = it1, ++it2; it2 != iend; ++it2) {
if ((*it1).getType() != (*it2).getType()) {
@@ -1261,7 +1261,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
void TheoryArrays::queueRowLemma(RowLemmaType lem)
{
- if (d_conflict || d_RowAlreadyAdded.count(lem) != 0) {
+ if (d_conflict || d_RowAlreadyAdded.contains(lem)) {
return;
}
TNode a = lem.first;
@@ -1407,7 +1407,7 @@ void TheoryArrays::dischargeLemmas()
for (unsigned count = 0; count < sz; ++count) {
RowLemmaType l = d_RowQueue.front();
d_RowQueue.pop();
- if (d_RowAlreadyAdded.count(l) != 0) {
+ if (d_RowAlreadyAdded.contains(l)) {
continue;
}
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 240cfad9a..172482e71 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -333,8 +333,10 @@ class TheoryArrays : public Theory {
context::CDQueue<RowLemmaType> d_RowQueue;
context::CDHashSet<RowLemmaType, RowLemmaTypeHashFunction > d_RowAlreadyAdded;
- context::CDHashSet<TNode, TNodeHashFunction> d_sharedArrays;
- context::CDHashSet<TNode, TNodeHashFunction> d_sharedOther;
+ typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+
+ CDNodeSet d_sharedArrays;
+ CDNodeSet d_sharedOther;
context::CDO<bool> d_sharedTerms;
context::CDList<TNode> d_reads;
std::hash_map<TNode, Node, TNodeHashFunction> d_diseqCache;
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index e62f9b7a1..aec0cff58 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -118,7 +118,7 @@ private:
/** Nodes that have been attached already (computed forward edges for) */
// All the nodes we've visited so far
- context::CDHashSet<TNode, TNodeHashFunction> d_seen;
+ context::CDHashSet<Node, NodeHashFunction> d_seen;
/**
* Assignment status of each node.
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 0c8df3fca..e38f3568c 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -40,8 +40,8 @@ class TheoryBV : public Theory {
context::Context* d_context;
/** Context dependent set of atoms we already propagated */
- context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
- context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet;
+ context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
+ context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
BitblastSolver d_bitblastSolver;
EqualitySolver d_equalitySolver;
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index 655918986..c7036a9ad 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -66,7 +66,7 @@ private:
AlreadyNotifiedMap d_alreadyNotifiedMap;
/** The registered equalities for propagation */
- typedef context::CDHashSet<TNode, TNodeHashFunction> RegisteredEqualitiesSet;
+ typedef context::CDHashSet<Node, NodeHashFunction> RegisteredEqualitiesSet;
RegisteredEqualitiesSet d_registeredEqualities;
private:
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 063943056..27371eac3 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -190,7 +190,7 @@ class TheoryEngine {
* context-dependent set of those theory-propagable literals that
* have been propagated.
*/
- context::CDHashSet<TNode, TNodeHashFunction> d_hasPropagated;
+ context::CDHashSet<Node, NodeHashFunction> d_hasPropagated;
/**
* Statistics for a particular theory.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback