diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 16:05:37 +0000 |
---|---|---|
committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-06-12 16:05:37 +0000 |
commit | 5032c2163edcdfe554bd6d8d2c59bb7e4ecf9325 (patch) | |
tree | f2dae737adc3353e8c137b5d4c0acaf67e7726aa /src | |
parent | f4b04f156d1dd90bd3d14b611e40057e02101219 (diff) |
Enabling constant propagation
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 66 |
1 files changed, 37 insertions, 29 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5874692b5..3d2a971be 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -140,7 +140,7 @@ class SmtEnginePrivate { * then nothing has been pushed out yet. */ context::CDO<theory::SubstitutionMap::iterator> d_lastSubstitutionPos; - static const bool d_doConstantProp = false; + static const bool d_doConstantProp = true; /** * Runs the nonclausal solver and tries to solve all the assigned @@ -868,7 +868,6 @@ void SmtEnginePrivate::nonClausalSimplify() { learnedLiteralNew = constantPropagations.apply(learnedLiteral); if (learnedLiteralNew == learnedLiteral) { break; - } ++d_smt.d_numConstantProps; learnedLiteral = theory::Rewriter::rewrite(learnedLiteralNew); } @@ -899,13 +898,14 @@ void SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "solved " << learnedLiteral << endl; Assert(theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(learnedLiteral)).isConst()); - vector<pair<Node, Node> > equations; - constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true); - if (equations.empty()) { - break; - } - Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); + // vector<pair<Node, Node> > equations; + // constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true); + // if (equations.empty()) { + // break; + // } + // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); // else fall through + break; } case Theory::PP_ASSERT_STATUS_CONFLICT: // If in conflict, we return false @@ -931,15 +931,16 @@ void SmtEnginePrivate::nonClausalSimplify() { Assert(!t.isConst()); Assert(constantPropagations.apply(t) == t); Assert(d_topLevelSubstitutions.apply(t) == t); - vector<pair<Node,Node> > equations; - constantPropagations.simplifyLHS(t, c, equations, true); - if (!equations.empty()) { - Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); - d_assertionsToPreprocess.clear(); - d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); - return; - } - d_topLevelSubstitutions.simplifyRHS(constantPropagations); + constantPropagations.addSubstitution(t, c, true, false, false); + // vector<pair<Node,Node> > equations;a + // constantPropagations.simplifyLHS(t, c, equations, true); + // if (!equations.empty()) { + // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); + // d_assertionsToPreprocess.clear(); + // d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false)); + // return; + // } + // d_topLevelSubstitutions.simplifyRHS(constantPropagations); } else { // Keep the literal @@ -967,6 +968,13 @@ void SmtEnginePrivate::nonClausalSimplify() { d_lastSubstitutionPos = pos; ++pos; } + 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); } #ifdef CVC4_ASSERTIONS @@ -984,18 +992,18 @@ void SmtEnginePrivate::nonClausalSimplify() { 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)); - } + // 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 |