diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-04 22:26:40 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-04 22:26:40 +0000 |
commit | 3609fb41d7744b3a7d74e44f7bedc4d4c522c938 (patch) | |
tree | 011a3fa796fdb98bb3b9a1b425d12c678535f294 /src/theory | |
parent | 468c5bc5d8b63ec6818813270225e09383dd79ff (diff) |
Added preprocessing pass that propagates unconstrained values - solves all of
the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/booleans/circuit_propagator.h | 16 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_normalization.h | 6 | ||||
-rw-r--r-- | src/theory/substitutions.cpp | 11 | ||||
-rw-r--r-- | src/theory/substitutions.h | 6 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 9 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 5 |
7 files changed, 48 insertions, 9 deletions
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 1341c048a..85d6fbdf8 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -31,7 +31,9 @@ libtheory_la_SOURCES = \ term_registration_visitor.h \ term_registration_visitor.cpp \ ite_simplifier.h \ - ite_simplifier.cpp + ite_simplifier.cpp \ + unconstrained_simplifier.h \ + unconstrained_simplifier.cpp nodist_libtheory_la_SOURCES = \ rewriter_tables.h \ diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index f5e4f4630..60e48dba2 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -68,10 +68,6 @@ public: private: - /** Back edges from nodes to where they are used */ - typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; - BackEdgesMap d_backEdges; - /** The propagation queue */ std::vector<TNode> d_propagationQueue; @@ -111,6 +107,15 @@ private: */ DataClearer< std::vector<Node> > d_learnedLiteralClearer; + /** Back edges from nodes to where they are used */ + typedef std::hash_map<Node, std::vector<Node>, NodeHashFunction> BackEdgesMap; + BackEdgesMap d_backEdges; + + /** + * Similar data clearer for back edges. + */ + DataClearer<BackEdgesMap> d_backEdgesClearer; + /** Nodes that have been attached already (computed forward edges for) */ // All the nodes we've visited so far context::CDHashSet<TNode, TNodeHashFunction> d_seen; @@ -231,12 +236,13 @@ public: */ CircuitPropagator(context::Context* context, std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true) : - d_backEdges(), d_propagationQueue(), d_propagationQueueClearer(context, d_propagationQueue), d_conflict(context, false), d_learnedLiterals(outLearnedLiterals), d_learnedLiteralClearer(context, outLearnedLiterals), + d_backEdges(), + d_backEdgesClearer(context, d_backEdges), d_seen(context), d_state(context), d_forwardPropagation(enableForward), diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h index 5be052947..197134b6a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h +++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h @@ -405,6 +405,9 @@ Node RewriteRule<SolveEq>::apply(TNode node) { updateCoefMap(left[i], size, leftMap, leftConst); } } + else if (left.getKind() == kind::BITVECTOR_NOT && left[0] == right) { + return utils::mkFalse(); + } else { updateCoefMap(left, size, leftMap, leftConst); } @@ -415,6 +418,9 @@ Node RewriteRule<SolveEq>::apply(TNode node) { updateCoefMap(right[i], size, rightMap, rightConst); } } + else if (right.getKind() == kind::BITVECTOR_NOT && right[0] == left) { + return utils::mkFalse(); + } else { updateCoefMap(right, size, rightMap, rightConst); } diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index caf7566b9..b7ad1d174 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -71,6 +71,10 @@ Node SubstitutionMap::internalSubstitute(TNode t, NodeCache& substitutionCache) } // Mark the substitution and continue Node result = builder; + find = substitutionCache.find(result); + if (find != substitutionCache.end()) { + result = find->second; + } Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << t << "): setting " << current << " -> " << result << std::endl; substitutionCache[current] = result; toVisit.pop_back(); @@ -114,13 +118,16 @@ void SubstitutionMap::addSubstitution(TNode x, TNode t, bool invalidateCache) { d_substitutions[(*it).first] = internalSubstitute((*it).second, tempCache); } - // Put the new substitution in - d_substitutions[x] = t; + // Put the new substitution in, but apply existing substitutions to rhs first + d_substitutions[x] = apply(t); // Also invalidate the cache if (invalidateCache) { d_cacheInvalidated = true; } + else { + d_substitutionCache[x] = d_substitutions[x]; + } } static bool check(TNode node, const SubstitutionMap::NodeMap& substitutions) CVC4_UNUSED; diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index 958f50276..711ff9b72 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -107,6 +107,12 @@ public: void addSubstitution(TNode x, TNode t, bool invalidateCache = true); /** + * Returns true iff x is in the substitution map + */ + bool hasSubstitution(TNode x) + { return d_substitutions.find(x) != d_substitutions.end(); } + + /** * Apply the substitutions to the node. */ Node apply(TNode t); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f72275cb2..4ed0bcb60 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -62,7 +62,8 @@ TheoryEngine::TheoryEngine(context::Context* context, d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"), d_inPreregister(false), d_preRegistrationVisitor(this, context), - d_sharedTermsVisitor(d_sharedTerms) + d_sharedTermsVisitor(d_sharedTerms), + d_unconstrainedSimp(context, logicInfo) { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { d_theoryTable[theoryId] = NULL; @@ -1011,3 +1012,9 @@ Node TheoryEngine::ppSimpITE(TNode assertion) result = Rewriter::rewrite(result); return result; } + + +void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions) +{ + d_unconstrainedSimp.processAssertions(assertions); +} diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 019818a5f..bc9f4c889 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -42,6 +42,7 @@ #include "util/hash.h" #include "util/cache.h" #include "theory/ite_simplifier.h" +#include "theory/unconstrained_simplifier.h" namespace CVC4 { @@ -734,8 +735,12 @@ private: /** For preprocessing pass simplifying ITEs */ ITESimplifier d_iteSimplifier; + /** For preprocessing pass simplifying unconstrained expressions */ + UnconstrainedSimplifier d_unconstrainedSimp; + public: Node ppSimpITE(TNode assertion); + void ppUnconstrainedSimp(std::vector<Node>& assertions); };/* class TheoryEngine */ |