summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp51
1 files changed, 26 insertions, 25 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 837968aa2..704303826 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -18,7 +18,8 @@
#include <algorithm>
#include <cctype>
-#include <ext/hash_map>
+#include <unordered_map>
+#include <unordered_set>
#include <iterator>
#include <sstream>
#include <stack>
@@ -463,8 +464,8 @@ class PrintSuccessListener : public Listener {
class SmtEnginePrivate : public NodeManagerListener {
SmtEngine& d_smt;
- typedef hash_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
- typedef hash_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
+ typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
+ typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
/**
* Manager for limiting time and abstract resource usage.
@@ -634,7 +635,7 @@ private:
* conjuncts.
*/
size_t removeFromConjunction(Node& n,
- const std::hash_set<unsigned long>& toRemove);
+ const std::unordered_set<unsigned long>& toRemove);
/** Scrub miplib encodings. */
void doMiplibTrick();
@@ -2255,7 +2256,7 @@ bool SmtEngine::isDefinedFunction( Expr func ){
return d_definedFunctions->find(nf) != d_definedFunctions->end();
}
-Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
+Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
stack< triple<Node, Node, bool> > worklist;
@@ -2295,7 +2296,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
}
// maybe it's in the cache
- hash_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
+ unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
if(cacheHit != cache.end()) {
TNode ret = (*cacheHit).second;
result.push(ret.isNull() ? n : ret);
@@ -2427,7 +2428,7 @@ struct intToBV_stack_element {
: node(node), children_added(false) {}
};/* struct intToBV_stack_element */
-typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
Node SmtEnginePrivate::intToBVMakeBinary(TNode n, NodeMap& cache) {
// Do a topological sort of the subexpressions and substitute them
@@ -3031,7 +3032,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl;
d_nonClausalLearnedLiterals.resize(j);
- hash_set<TNode, TNodeHashFunction> s;
+ unordered_set<TNode, TNodeHashFunction> s;
Trace("debugging") << "NonClausal simplify pre-preprocess\n";
for (unsigned i = 0; i < d_assertions.size(); ++ i) {
Node assertion = d_assertions[i];
@@ -3266,7 +3267,7 @@ void SmtEnginePrivate::traceBackToAssertions(const std::vector<Node>& nodes, std
}
}
-size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set<unsigned long>& toRemove) {
+size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::unordered_set<unsigned long>& toRemove) {
Assert(n.getKind() == kind::AND);
size_t removals = 0;
for(Node::iterator j = n.begin(); j != n.end(); ++j) {
@@ -3320,12 +3321,12 @@ void SmtEnginePrivate::doMiplibTrick() {
Assert(!options::incrementalSolving());
const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
- hash_set<unsigned long> removeAssertions;
+ unordered_set<unsigned long> removeAssertions;
NodeManager* nm = NodeManager::currentNM();
Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
- hash_map<TNode, Node, TNodeHashFunction> intVars;
+ unordered_map<TNode, Node, TNodeHashFunction> intVars;
for(vector<Node>::const_iterator i = d_boolVars.begin(); i != d_boolVars.end(); ++i) {
if(d_propagator.isAssigned(*i)) {
Debug("miplib") << "ineligible: " << *i << " because assigned " << d_propagator.getAssignment(*i) << endl;
@@ -3819,9 +3820,9 @@ Result SmtEngine::quickCheck() {
}
-void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache)
+void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache)
{
- hash_map<Node, bool, NodeHashFunction>::iterator it;
+ unordered_map<Node, bool, NodeHashFunction>::iterator it;
it = cache.find(n);
if (it != cache.end()) {
return;
@@ -3845,9 +3846,9 @@ void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<N
}
-bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache)
+bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache)
{
- hash_map<Node, bool, NodeHashFunction>::iterator it;
+ unordered_map<Node, bool, NodeHashFunction>::iterator it;
it = cache.find(n);
if (it != cache.end()) {
return (*it).second;
@@ -3918,7 +3919,7 @@ void SmtEnginePrivate::processAssertions() {
Chat() << "expanding definitions..." << endl;
Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
for(unsigned i = 0; i < d_assertions.size(); ++ i) {
d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
}
@@ -3937,8 +3938,8 @@ void SmtEnginePrivate::processAssertions() {
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
if( options::nlExtPurify() ){
- hash_map<Node, Node, NodeHashFunction> cache;
- hash_map<Node, Node, NodeHashFunction> bcache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> bcache;
std::vector< Node > var_eq;
for (unsigned i = 0; i < d_assertions.size(); ++ i) {
d_assertions.replace(i, purifyNlTerms(d_assertions[i], cache, bcache, var_eq));
@@ -3959,7 +3960,7 @@ void SmtEnginePrivate::processAssertions() {
if (options::solveRealAsInt()) {
Chat() << "converting reals to ints..." << endl;
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
std::vector< Node > var_eq;
for(unsigned i = 0; i < d_assertions.size(); ++ i) {
d_assertions.replace(i, realToInt(d_assertions[i], cache, var_eq));
@@ -3975,7 +3976,7 @@ void SmtEnginePrivate::processAssertions() {
if (options::solveIntAsBV() > 0) {
Chat() << "converting ints to bit-vectors..." << endl;
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
for(unsigned i = 0; i < d_assertions.size(); ++ i) {
d_assertions.replace(i, intToBV(d_assertions[i], cache));
}
@@ -4203,7 +4204,7 @@ void SmtEnginePrivate::processAssertions() {
// For each skolem variable sk, let iteExpr = iteMap(sk) be the ite expr mapped to by sk.
// cache for expression traversal
- hash_map<Node, bool, NodeHashFunction> cache;
+ unordered_map<Node, bool, NodeHashFunction> cache;
// First, find all skolems that appear in the substitution map - their associated iteExpr will need
// to be moved to the main assertion set
@@ -4656,7 +4657,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L
if(Dump.isOn("benchmark")) {
Dump("benchmark") << ExpandDefinitionsCommand(e);
}
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true);
n = postprocess(n, TypeNode::fromType(e.getType()));
@@ -4701,7 +4702,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin
TypeNode expectedType = n.getType();
// Expand, then normalize
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
n = d_private->expandDefinitions(n, cache);
// There are two ways model values for terms are computed (for historical
// reasons). One way is that used in check-model; the other is that
@@ -4814,7 +4815,7 @@ CVC4::SExpr SmtEngine::getAssignment() {
Trace("smt") << "--- getting value of " << *i << endl;
// Expand, then normalize
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
Node n = d_private->expandDefinitions(*i, cache);
n = Rewriter::rewrite(n);
@@ -5056,7 +5057,7 @@ void SmtEngine::checkModel(bool hardFailure) {
// Apply any define-funs from the problem.
{
- hash_map<Node, Node, NodeHashFunction> cache;
+ unordered_map<Node, Node, NodeHashFunction> cache;
n = d_private->expandDefinitions(n, cache);
}
Notice() << "SmtEngine::checkModel(): -- expands to " << n << endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback