diff options
Diffstat (limited to 'src/preprocessing/passes/non_clausal_simp.cpp')
| -rw-r--r-- | src/preprocessing/passes/non_clausal_simp.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp index a3650c988..2b788098a 100644 --- a/src/preprocessing/passes/non_clausal_simp.cpp +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -93,7 +93,8 @@ PreprocessingPassResult NonClausalSimp::applyInternal( } Trace("non-clausal-simplify") << "propagating" << std::endl; - if (propagator->propagate()) + TrustNode conf = propagator->propagate(); + if (!conf.isNull()) { // If in conflict, just return false Trace("non-clausal-simplify") @@ -122,11 +123,11 @@ PreprocessingPassResult NonClausalSimp::applyInternal( SubstitutionMap& newSubstitutions = tnewSubstituions.get(); SubstitutionMap::iterator pos; size_t j = 0; - std::vector<Node>& learned_literals = propagator->getLearnedLiterals(); + std::vector<TrustNode>& learned_literals = propagator->getLearnedLiterals(); for (size_t i = 0, size = learned_literals.size(); i < size; ++i) { // Simplify the literal we learned wrt previous substitutions - Node learnedLiteral = learned_literals[i]; + Node learnedLiteral = learned_literals[i].getNode(); Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral); Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral); Trace("non-clausal-simplify") @@ -164,7 +165,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( { // If the learned literal simplifies to false, we're in conflict Trace("non-clausal-simplify") - << "conflict with " << learned_literals[i] << std::endl; + << "conflict with " << learned_literals[i].getNode() << std::endl; Assert(!options::unsatCores()); assertionsToPreprocess->clear(); Node n = NodeManager::currentNM()->mkConst<bool>(false); @@ -385,7 +386,7 @@ PreprocessingPassResult NonClausalSimp::applyInternal( for (size_t i = 0; i < learned_literals.size(); ++i) { - Node learned = learned_literals[i]; + Node learned = learned_literals[i].getNode(); Assert(top_level_substs.apply(learned) == learned); Node learnedNew = newSubstitutions.apply(learned); if (learned != learnedNew) @@ -452,7 +453,6 @@ PreprocessingPassResult NonClausalSimp::applyInternal( return PreprocessingPassResult::NO_CONFLICT; } // namespace passes - /* -------------------------------------------------------------------------- */ } // namespace passes |