diff options
author | Clark Barrett <barrett@cs.stanford.edu> | 2017-04-21 21:45:23 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-04-21 21:45:23 -0700 |
commit | 58c004370561c582a090020113d8781b2ff6ac42 (patch) | |
tree | 4c828e4565de11cac246e6bd90e7c956171d4c84 | |
parent | 5a38d9222e6039121b8e61602289254c22f3935e (diff) | |
parent | fdd9d43ba0102f4d77f1a8a2cf826091731e1983 (diff) |
Merge pull request #151 from 4tXJ7f/fix_debug
Move assertion out of loop for better performance
-rw-r--r-- | src/smt/smt_engine.cpp | 65 |
1 files changed, 35 insertions, 30 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a95ce7b8d..31b62f25a 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2997,39 +2997,44 @@ bool SmtEnginePrivate::nonClausalSimplify() { } break; } + } #ifdef CVC4_ASSERTIONS - // Check data structure invariants: - // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations - // 2. each lhs of constantPropagations rewrites to itself - // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a - // constant propagation too - // 4. each lhs of constantPropagations is different from each rhs - for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) { - Assert((*pos).first.isVar()); - Assert(d_topLevelSubstitutions.apply((*pos).first) == (*pos).first); - Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second); - Assert(newSubstitutions.apply(newSubstitutions.apply((*pos).second)) == newSubstitutions.apply((*pos).second)); - } - for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) { - Assert((*pos).second.isConst()); - Assert(Rewriter::rewrite((*pos).first) == (*pos).first); - // Node newLeft = d_topLevelSubstitutions.apply((*pos).first); - // if (newLeft != (*pos).first) { - // newLeft = Rewriter::rewrite(newLeft); - // Assert(newLeft == (*pos).second || - // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second)); - // } - // newLeft = constantPropagations.apply((*pos).first); - // if (newLeft != (*pos).first) { - // newLeft = Rewriter::rewrite(newLeft); - // Assert(newLeft == (*pos).second || - // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second)); - // } - Assert(constantPropagations.apply((*pos).second) == (*pos).second); - } -#endif /* CVC4_ASSERTIONS */ + // NOTE: When debugging this code, consider moving this check inside of the + // loop over d_nonClausalLearnedLiterals. This check has been moved outside + // because it is costly for certain inputs (see bug 508). + // + // Check data structure invariants: + // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations + // 2. each lhs of constantPropagations rewrites to itself + // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a + // constant propagation too + // 4. each lhs of constantPropagations is different from each rhs + for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) { + Assert((*pos).first.isVar()); + Assert(d_topLevelSubstitutions.apply((*pos).first) == (*pos).first); + Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second); + Assert(newSubstitutions.apply(newSubstitutions.apply((*pos).second)) == newSubstitutions.apply((*pos).second)); } + for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) { + Assert((*pos).second.isConst()); + Assert(Rewriter::rewrite((*pos).first) == (*pos).first); + // Node newLeft = d_topLevelSubstitutions.apply((*pos).first); + // if (newLeft != (*pos).first) { + // newLeft = Rewriter::rewrite(newLeft); + // Assert(newLeft == (*pos).second || + // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second)); + // } + // newLeft = constantPropagations.apply((*pos).first); + // if (newLeft != (*pos).first) { + // newLeft = Rewriter::rewrite(newLeft); + // Assert(newLeft == (*pos).second || + // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second)); + // } + Assert(constantPropagations.apply((*pos).second) == (*pos).second); + } +#endif /* CVC4_ASSERTIONS */ + // Resize the learnt Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl; d_nonClausalLearnedLiterals.resize(j); |