--- /dev/null
+/********************* */
+/*! \file non_clausal_simp.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Non-clausal simplification preprocessing pass.
+ **
+ ** Run the nonclausal solver and try to solve all assigned theory literals.
+ **/
+
+#include "preprocessing/passes/non_clausal_simp.h"
+
+#include "context/cdo.h"
+#include "options/proof_options.h"
+#include "smt/smt_statistics_registry.h"
+#include "theory/theory_model.h"
+
+#include <vector>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+/* -------------------------------------------------------------------------- */
+
+NonClausalSimp::Statistics::Statistics()
+ : d_numConstantProps(
+ "preprocessing::passes::NonClausalSimp::NumConstantProps", 0)
+{
+ smtStatisticsRegistry()->registerStat(&d_numConstantProps);
+}
+
+NonClausalSimp::Statistics::~Statistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
+}
+
+/* -------------------------------------------------------------------------- */
+
+NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
+ : PreprocessingPass(preprocContext, "non-clausal-simp")
+{
+}
+
+PreprocessingPassResult NonClausalSimp::applyInternal(
+ AssertionPipeline* assertionsToPreprocess)
+{
+ Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
+
+ d_preprocContext->spendResource(options::preprocessStep());
+
+ theory::booleans::CircuitPropagator* propagator =
+ d_preprocContext->getCircuitPropagator();
+
+ for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+ {
+ Trace("non-clausal-simplify") << "Assertion #" << i << " : "
+ << (*assertionsToPreprocess)[i] << std::endl;
+ }
+
+ if (propagator->getNeedsFinish())
+ {
+ propagator->finish();
+ propagator->setNeedsFinish(false);
+ }
+ propagator->initialize();
+
+ // Assert all the assertions to the propagator
+ Trace("non-clausal-simplify") << "asserting to propagator" << std::endl;
+ context::CDO<unsigned>& substs_index =
+ assertionsToPreprocess->getSubstitutionsIndex();
+ for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+ {
+ Assert(Rewriter::rewrite((*assertionsToPreprocess)[i])
+ == (*assertionsToPreprocess)[i]);
+ // Don't reprocess substitutions
+ if (substs_index > 0 && i == substs_index)
+ {
+ continue;
+ }
+ Trace("non-clausal-simplify")
+ << "asserting " << (*assertionsToPreprocess)[i] << std::endl;
+ Debug("cores") << "propagator->assertTrue: " << (*assertionsToPreprocess)[i]
+ << std::endl;
+ propagator->assertTrue((*assertionsToPreprocess)[i]);
+ }
+
+ Trace("non-clausal-simplify") << "propagating" << std::endl;
+ if (propagator->propagate())
+ {
+ // If in conflict, just return false
+ Trace("non-clausal-simplify")
+ << "conflict in non-clausal propagation" << std::endl;
+ Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
+ assertionsToPreprocess->clear();
+ Node n = NodeManager::currentNM()->mkConst<bool>(false);
+ assertionsToPreprocess->push_back(n);
+ PROOF(ProofManager::currentPM()->addDependence(n, Node::null()));
+ propagator->setNeedsFinish(true);
+ return PreprocessingPassResult::CONFLICT;
+ }
+
+ Trace("non-clausal-simplify")
+ << "Iterate through " << propagator->getLearnedLiterals().size()
+ << " learned literals." << std::endl;
+ // No conflict, go through the literals and solve them
+ SubstitutionMap& top_level_substs =
+ assertionsToPreprocess->getTopLevelSubstitutions();
+ SubstitutionMap constantPropagations(d_preprocContext->getUserContext());
+ SubstitutionMap newSubstitutions(d_preprocContext->getUserContext());
+ SubstitutionMap::iterator pos;
+ size_t j = 0;
+ std::vector<Node>& 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];
+ Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
+ Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral);
+ Trace("non-clausal-simplify")
+ << "Process learnedLiteral : " << learnedLiteral << std::endl;
+ Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral);
+ if (learnedLiteral != learnedLiteralNew)
+ {
+ learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
+ }
+ Trace("non-clausal-simplify")
+ << "Process learnedLiteral, after newSubs : " << learnedLiteral
+ << std::endl;
+ for (;;)
+ {
+ learnedLiteralNew = constantPropagations.apply(learnedLiteral);
+ if (learnedLiteralNew == learnedLiteral)
+ {
+ break;
+ }
+ d_statistics.d_numConstantProps += 1;
+ learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
+ }
+ Trace("non-clausal-simplify")
+ << "Process learnedLiteral, after constProp : " << learnedLiteral
+ << std::endl;
+ // It might just simplify to a constant
+ if (learnedLiteral.isConst())
+ {
+ if (learnedLiteral.getConst<bool>())
+ {
+ // If the learned literal simplifies to true, it's redundant
+ continue;
+ }
+ else
+ {
+ // If the learned literal simplifies to false, we're in conflict
+ Trace("non-clausal-simplify")
+ << "conflict with " << learned_literals[i] << std::endl;
+ Assert(!options::unsatCores());
+ assertionsToPreprocess->clear();
+ Node n = NodeManager::currentNM()->mkConst<bool>(false);
+ assertionsToPreprocess->push_back(n);
+ PROOF(ProofManager::currentPM()->addDependence(n, Node::null()));
+ propagator->setNeedsFinish(true);
+ return PreprocessingPassResult::CONFLICT;
+ }
+ }
+
+ // Solve it with the corresponding theory, possibly adding new
+ // substitutions to newSubstitutions
+ Trace("non-clausal-simplify") << "solving " << learnedLiteral << std::endl;
+
+ Theory::PPAssertStatus solveStatus =
+ d_preprocContext->getTheoryEngine()->solve(learnedLiteral,
+ newSubstitutions);
+
+ switch (solveStatus)
+ {
+ case Theory::PP_ASSERT_STATUS_SOLVED:
+ {
+ // The literal should rewrite to true
+ Trace("non-clausal-simplify")
+ << "solved " << learnedLiteral << std::endl;
+ Assert(Rewriter::rewrite(newSubstitutions.apply(learnedLiteral))
+ .isConst());
+ // vector<pair<Node, Node> > equations;
+ // constantPropagations.simplifyLHS(top_level_substs, 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
+ Trace("non-clausal-simplify")
+ << "conflict while solving " << learnedLiteral << std::endl;
+ Assert(!options::unsatCores());
+ assertionsToPreprocess->clear();
+ Node n = NodeManager::currentNM()->mkConst<bool>(false);
+ assertionsToPreprocess->push_back(n);
+ PROOF(ProofManager::currentPM()->addDependence(n, Node::null()));
+ propagator->setNeedsFinish(true);
+ return PreprocessingPassResult::CONFLICT;
+ }
+ default:
+ if (learnedLiteral.getKind() == kind::EQUAL
+ && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst()))
+ {
+ // constant propagation
+ TNode t;
+ TNode c;
+ if (learnedLiteral[0].isConst())
+ {
+ t = learnedLiteral[1];
+ c = learnedLiteral[0];
+ }
+ else
+ {
+ t = learnedLiteral[0];
+ c = learnedLiteral[1];
+ }
+ Assert(!t.isConst());
+ Assert(constantPropagations.apply(t) == t);
+ Assert(top_level_substs.apply(t) == t);
+ Assert(newSubstitutions.apply(t) == t);
+ constantPropagations.addSubstitution(t, c);
+ // 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); assertionsToPreprocess->clear();
+ // Node n = NodeManager::currentNM()->mkConst<bool>(false);
+ // assertionsToPreprocess->push_back(n);
+ // PROOF(ProofManager::currentPM()->addDependence(n, Node::null()));
+ // false); return;
+ // }
+ // top_level_substs.simplifyRHS(constantPropagations);
+ }
+ else
+ {
+ // Keep the literal
+ learned_literals[j++] = learned_literals[i];
+ }
+ break;
+ }
+ }
+
+#ifdef CVC4_ASSERTIONS
+ // NOTE: When debugging this code, consider moving this check inside of the
+ // loop over propagator->getLearnedLiterals(). 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 top_level_substs, does not appear anywhere in rhs of
+ // top_level_substs 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(top_level_substs.apply((*pos).first) == (*pos).first);
+ Assert(top_level_substs.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 = top_level_substs.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("non-clausal-simplify")
+ << "Resize non-clausal learned literals to " << j << std::endl;
+ learned_literals.resize(j);
+
+ unordered_set<TNode, TNodeHashFunction> s;
+ for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+ {
+ Node assertion = (*assertionsToPreprocess)[i];
+ Node assertionNew = newSubstitutions.apply(assertion);
+ Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl;
+ Trace("non-clausal-simplify")
+ << "assertionNew = " << assertionNew << std::endl;
+ if (assertion != assertionNew)
+ {
+ assertion = Rewriter::rewrite(assertionNew);
+ Trace("non-clausal-simplify")
+ << "rewrite(assertion) = " << assertion << std::endl;
+ }
+ Assert(Rewriter::rewrite(assertion) == assertion);
+ for (;;)
+ {
+ assertionNew = constantPropagations.apply(assertion);
+ if (assertionNew == assertion)
+ {
+ break;
+ }
+ d_statistics.d_numConstantProps += 1;
+ Trace("non-clausal-simplify")
+ << "assertionNew = " << assertionNew << std::endl;
+ assertion = Rewriter::rewrite(assertionNew);
+ Trace("non-clausal-simplify")
+ << "assertionNew = " << assertionNew << std::endl;
+ }
+ s.insert(assertion);
+ assertionsToPreprocess->replace(i, assertion);
+ Trace("non-clausal-simplify")
+ << "non-clausal preprocessed: " << assertion << std::endl;
+ }
+
+ // add substitutions to model, or as assertions if needed (when incremental)
+ TheoryModel* m = d_preprocContext->getTheoryEngine()->getModel();
+ Assert(m != nullptr);
+ NodeManager* nm = NodeManager::currentNM();
+ NodeBuilder<> substitutionsBuilder(kind::AND);
+ for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos)
+ {
+ Node lhs = (*pos).first;
+ Node rhs = newSubstitutions.apply((*pos).second);
+ // If using incremental, we must check whether this variable has occurred
+ // before now. If it hasn't we can add this as a substitution.
+ if (substs_index == 0
+ || d_preprocContext->getSymsInAssertions().find(lhs)
+ == d_preprocContext->getSymsInAssertions().end())
+ {
+ Trace("non-clausal-simplify")
+ << "substitute: " << lhs << " " << rhs << std::endl;
+ m->addSubstitution(lhs, rhs);
+ }
+ else
+ {
+ // if it has, the substitution becomes an assertion
+ Node eq = nm->mkNode(kind::EQUAL, lhs, rhs);
+ Trace("non-clausal-simplify")
+ << "substitute: will notify SAT layer of substitution: " << eq
+ << std::endl;
+ substitutionsBuilder << eq;
+ }
+ }
+ // add to the last assertion if necessary
+ if (substitutionsBuilder.getNumChildren() > 0)
+ {
+ substitutionsBuilder << (*assertionsToPreprocess)[substs_index];
+ assertionsToPreprocess->replace(
+ substs_index, Rewriter::rewrite(Node(substitutionsBuilder)));
+ }
+
+ NodeBuilder<> learnedBuilder(kind::AND);
+ Assert(assertionsToPreprocess->getRealAssertionsEnd()
+ <= assertionsToPreprocess->size());
+ learnedBuilder << (*assertionsToPreprocess)
+ [assertionsToPreprocess->getRealAssertionsEnd() - 1];
+
+ for (size_t i = 0; i < learned_literals.size(); ++i)
+ {
+ Node learned = learned_literals[i];
+ Assert(top_level_substs.apply(learned) == learned);
+ Node learnedNew = newSubstitutions.apply(learned);
+ if (learned != learnedNew)
+ {
+ learned = Rewriter::rewrite(learnedNew);
+ }
+ Assert(Rewriter::rewrite(learned) == learned);
+ for (;;)
+ {
+ learnedNew = constantPropagations.apply(learned);
+ if (learnedNew == learned)
+ {
+ break;
+ }
+ d_statistics.d_numConstantProps += 1;
+ learned = Rewriter::rewrite(learnedNew);
+ }
+ if (s.find(learned) != s.end())
+ {
+ continue;
+ }
+ s.insert(learned);
+ learnedBuilder << learned;
+ Trace("non-clausal-simplify")
+ << "non-clausal learned : " << learned << std::endl;
+ }
+ learned_literals.clear();
+
+ for (pos = constantPropagations.begin(); pos != constantPropagations.end();
+ ++pos)
+ {
+ Node cProp = (*pos).first.eqNode((*pos).second);
+ Assert(top_level_substs.apply(cProp) == cProp);
+ Node cPropNew = newSubstitutions.apply(cProp);
+ if (cProp != cPropNew)
+ {
+ cProp = Rewriter::rewrite(cPropNew);
+ Assert(Rewriter::rewrite(cProp) == cProp);
+ }
+ if (s.find(cProp) != s.end())
+ {
+ continue;
+ }
+ s.insert(cProp);
+ learnedBuilder << cProp;
+ Trace("non-clausal-simplify")
+ << "non-clausal constant propagation : " << cProp << std::endl;
+ }
+
+ // Add new substitutions to topLevelSubstitutions
+ // Note that we don't have to keep rhs's in full solved form
+ // because SubstitutionMap::apply does a fixed-point iteration when
+ // substituting
+ top_level_substs.addSubstitutions(newSubstitutions);
+
+ if (learnedBuilder.getNumChildren() > 1)
+ {
+ assertionsToPreprocess->replace(
+ assertionsToPreprocess->getRealAssertionsEnd() - 1,
+ Rewriter::rewrite(Node(learnedBuilder)));
+ }
+
+ propagator->setNeedsFinish(true);
+ return PreprocessingPassResult::NO_CONFLICT;
+} // namespace passes
+
+/* -------------------------------------------------------------------------- */
+
+} // namespace passes
+} // namespace preprocessing
+} // namespace CVC4
#include "preprocessing/passes/int_to_bv.h"
#include "preprocessing/passes/ite_removal.h"
#include "preprocessing/passes/ite_simp.h"
-#include "preprocessing/passes/nl_ext_purify.h"
#include "preprocessing/passes/miplib_trick.h"
+#include "preprocessing/passes/nl_ext_purify.h"
+#include "preprocessing/passes/non_clausal_simp.h"
#include "preprocessing/passes/pseudo_boolean_processor.h"
#include "preprocessing/passes/quantifier_macros.h"
#include "preprocessing/passes/quantifiers_preprocess.h"
typedef unordered_map<Node, Node, NodeHashFunction> NodeToNodeHashMap;
typedef unordered_map<Node, bool, NodeHashFunction> NodeToBoolHashMap;
- typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
/**
* Manager for limiting time and abstract resource usage.
*/
SubstitutionMap d_abstractValueMap;
- /**
- * The (user-context-dependent) set of symbols that occur in at least one
- * assertion in the current user context. This is used by the
- * nonClausalSimplify pass.
- */
- NodeSet d_symsInAssertions;
-
/**
* A mapping of all abstract values (actual value |-> abstract) that
* we've handed out. This is necessary to ensure that we give the
std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
PreprocessingPassRegistry d_preprocessingPassRegistry;
- static const bool d_doConstantProp = true;
-
- /**
- * Runs the nonclausal solver and tries to solve all the assigned
- * theory literals.
- *
- * Returns false if the formula simplifies to "false"
- */
- bool nonClausalSimplify();
-
- /** record symbols in assertions
- *
- * This method is called when a set of assertions is finalized. It adds
- * the symbols to d_symsInAssertions that occur in assertions.
- */
- void recordSymbolsInAssertions(const std::vector<Node>& assertions);
-
/**
* Helper function to fix up assertion list to restore invariants needed after
* ite removal.
d_assertionsProcessed(smt.d_userContext, false),
d_fakeContext(),
d_abstractValueMap(&d_fakeContext),
- d_symsInAssertions(smt.d_userContext),
d_abstractValues(),
d_simplifyAssertionsDepth(0),
// d_needsExpandDefs(true), //TODO?
new ITESimp(d_preprocessingPassContext.get()));
std::unique_ptr<NlExtPurify> nlExtPurify(
new NlExtPurify(d_preprocessingPassContext.get()));
+ std::unique_ptr<NonClausalSimp> nonClausalSimp(
+ new NonClausalSimp(d_preprocessingPassContext.get()));
std::unique_ptr<MipLibTrick> mipLibTrick(
new MipLibTrick(d_preprocessingPassContext.get()));
std::unique_ptr<QuantifiersPreprocess> quantifiersPreprocess(
d_preprocessingPassRegistry.registerPass("global-negate",
std::move(globalNegate));
d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
+ d_preprocessingPassRegistry.registerPass("ite-removal",
+ std::move(iteRemoval));
d_preprocessingPassRegistry.registerPass("ite-simp", std::move(iteSimp));
d_preprocessingPassRegistry.registerPass("nl-ext-purify",
std::move(nlExtPurify));
+ d_preprocessingPassRegistry.registerPass("non-clausal-simp",
+ std::move(nonClausalSimp));
d_preprocessingPassRegistry.registerPass("miplib-trick",
std::move(mipLibTrick));
d_preprocessingPassRegistry.registerPass("quantifiers-preprocess",
std::move(quantifiersPreprocess));
d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
std::move(pbProc));
- d_preprocessingPassRegistry.registerPass("ite-removal",
- std::move(iteRemoval));
d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt));
d_preprocessingPassRegistry.registerPass("rewrite", std::move(rewrite));
d_preprocessingPassRegistry.registerPass("sep-skolem-emp",
}
}
-// returns false if it learns a conflict
-bool SmtEnginePrivate::nonClausalSimplify() {
- spendResource(options::preprocessStep());
- d_smt.finalOptionsAreSet();
-
- if(options::unsatCores() || options::fewerPreprocessingHoles()) {
- return true;
- }
-
- TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime);
-
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl;
- for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- Trace("simplify") << "Assertion #" << i << " : " << d_assertions[i] << std::endl;
- }
-
- if (d_propagator.getNeedsFinish())
- {
- d_propagator.finish();
- d_propagator.setNeedsFinish(false);
- }
- d_propagator.initialize();
-
- // Assert all the assertions to the propagator
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "asserting to propagator" << endl;
- CDO<unsigned>& substs_index = d_assertions.getSubstitutionsIndex();
- for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
- // Don't reprocess substitutions
- if (substs_index > 0 && i == substs_index)
- {
- continue;
- }
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions[i] << endl;
- Debug("cores") << "d_propagator assertTrue: " << d_assertions[i] << std::endl;
- d_propagator.assertTrue(d_assertions[i]);
- }
-
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "propagating" << endl;
- if (d_propagator.propagate()) {
- // If in conflict, just return false
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "conflict in non-clausal propagation" << endl;
- Node falseNode = NodeManager::currentNM()->mkConst<bool>(false);
- Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
- d_assertions.clear();
- addFormula(falseNode, false, false);
- d_propagator.setNeedsFinish(true);
- return false;
- }
-
- Trace("simplify") << "Iterate through "
- << d_propagator.getLearnedLiterals().size()
- << " learned literals." << std::endl;
- // No conflict, go through the literals and solve them
- SubstitutionMap& top_level_substs = d_assertions.getTopLevelSubstitutions();
- SubstitutionMap constantPropagations(d_smt.d_context);
- SubstitutionMap newSubstitutions(d_smt.d_context);
- SubstitutionMap::iterator pos;
- size_t j = 0;
- std::vector<Node>& learned_literals = d_propagator.getLearnedLiterals();
- for (size_t i = 0, i_end = learned_literals.size(); i < i_end; ++i)
- {
- // Simplify the literal we learned wrt previous substitutions
- Node learnedLiteral = learned_literals[i];
- Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
- Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral);
- Trace("simplify") << "Process learnedLiteral : " << learnedLiteral << std::endl;
- Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral);
- if (learnedLiteral != learnedLiteralNew) {
- learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
- }
- Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral << std::endl;
- for (;;) {
- learnedLiteralNew = constantPropagations.apply(learnedLiteral);
- if (learnedLiteralNew == learnedLiteral) {
- break;
- }
- ++d_smt.d_stats->d_numConstantProps;
- learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
- }
- Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral << std::endl;
- // It might just simplify to a constant
- if (learnedLiteral.isConst()) {
- if (learnedLiteral.getConst<bool>()) {
- // If the learned literal simplifies to true, it's redundant
- continue;
- } else {
- // If the learned literal simplifies to false, we're in conflict
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "conflict with " << learned_literals[i] << endl;
- Assert(!options::unsatCores());
- d_assertions.clear();
- addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
- d_propagator.setNeedsFinish(true);
- return false;
- }
- }
-
- // Solve it with the corresponding theory, possibly adding new
- // substitutions to newSubstitutions
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "solving " << learnedLiteral << endl;
-
- Theory::PPAssertStatus solveStatus =
- d_smt.d_theoryEngine->solve(learnedLiteral, newSubstitutions);
-
- switch (solveStatus) {
- case Theory::PP_ASSERT_STATUS_SOLVED: {
- // The literal should rewrite to true
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "solved " << learnedLiteral << endl;
- Assert(Rewriter::rewrite(newSubstitutions.apply(learnedLiteral)).isConst());
- // vector<pair<Node, Node> > equations;
- // constantPropagations.simplifyLHS(top_level_substs, 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
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "conflict while solving "
- << learnedLiteral << endl;
- Assert(!options::unsatCores());
- d_assertions.clear();
- addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
- d_propagator.setNeedsFinish(true);
- return false;
- default:
- if (d_doConstantProp && learnedLiteral.getKind() == kind::EQUAL && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst())) {
- // constant propagation
- TNode t;
- TNode c;
- if (learnedLiteral[0].isConst()) {
- t = learnedLiteral[1];
- c = learnedLiteral[0];
- }
- else {
- t = learnedLiteral[0];
- c = learnedLiteral[1];
- }
- Assert(!t.isConst());
- Assert(constantPropagations.apply(t) == t);
- Assert(top_level_substs.apply(t) == t);
- Assert(newSubstitutions.apply(t) == t);
- constantPropagations.addSubstitution(t, c);
- // 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_assertions.clear();
- // addFormula(NodeManager::currentNM()->mkConst<bool>(false), false,
- // false); return;
- // }
- // top_level_substs.simplifyRHS(constantPropagations);
- }
- else {
- // Keep the literal
- learned_literals[j++] = learned_literals[i];
- }
- break;
- }
- }
-
-#ifdef CVC4_ASSERTIONS
- // NOTE: When debugging this code, consider moving this check inside of the
- // loop over d_propagator.getLearnedLiterals(). 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 top_level_substs, does not appear anywhere in rhs of
- // top_level_substs 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(top_level_substs.apply((*pos).first) == (*pos).first);
- Assert(top_level_substs.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 = top_level_substs.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;
- learned_literals.resize(j);
-
- 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];
- Node assertionNew = newSubstitutions.apply(assertion);
- Trace("debugging") << "assertion = " << assertion << endl;
- Trace("debugging") << "assertionNew = " << assertionNew << endl;
- if (assertion != assertionNew) {
- assertion = Rewriter::rewrite(assertionNew);
- Trace("debugging") << "rewrite(assertion) = " << assertion << endl;
- }
- Assert(Rewriter::rewrite(assertion) == assertion);
- for (;;) {
- assertionNew = constantPropagations.apply(assertion);
- if (assertionNew == assertion) {
- break;
- }
- ++d_smt.d_stats->d_numConstantProps;
- Trace("debugging") << "assertionNew = " << assertionNew << endl;
- assertion = Rewriter::rewrite(assertionNew);
- Trace("debugging") << "assertionNew = " << assertionNew << endl;
- }
- Trace("debugging") << "\n";
- s.insert(assertion);
- d_assertions.replace(i, assertion);
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "non-clausal preprocessed: "
- << assertion << endl;
- }
-
- // add substitutions to model, or as assertions if needed (when incremental)
- TheoryModel* m = d_smt.d_theoryEngine->getModel();
- Assert(m != nullptr);
- NodeManager* nm = NodeManager::currentNM();
- NodeBuilder<> substitutionsBuilder(kind::AND);
- for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos)
- {
- Node lhs = (*pos).first;
- Node rhs = newSubstitutions.apply((*pos).second);
- // If using incremental, we must check whether this variable has occurred
- // before now. If it hasn't we can add this as a substitution.
- if (substs_index == 0
- || d_symsInAssertions.find(lhs) == d_symsInAssertions.end())
- {
- Trace("simplify")
- << "SmtEnginePrivate::nonClausalSimplify(): substitute: " << lhs
- << " " << rhs << endl;
- m->addSubstitution(lhs, rhs);
- }
- else
- {
- // if it has, the substitution becomes an assertion
- Node eq = nm->mkNode(kind::EQUAL, lhs, rhs);
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- "substitute: will notify SAT layer of substitution: "
- << eq << endl;
- substitutionsBuilder << eq;
- }
- }
- // add to the last assertion if necessary
- if (substitutionsBuilder.getNumChildren() > 0)
- {
- substitutionsBuilder << d_assertions[substs_index];
- d_assertions.replace(substs_index,
- Rewriter::rewrite(Node(substitutionsBuilder)));
- }
-
- NodeBuilder<> learnedBuilder(kind::AND);
- Assert(d_assertions.getRealAssertionsEnd() <= d_assertions.size());
- learnedBuilder << d_assertions[d_assertions.getRealAssertionsEnd() - 1];
-
- for (size_t i = 0; i < learned_literals.size(); ++i)
- {
- Node learned = learned_literals[i];
- Assert(top_level_substs.apply(learned) == learned);
- Node learnedNew = newSubstitutions.apply(learned);
- if (learned != learnedNew) {
- learned = Rewriter::rewrite(learnedNew);
- }
- Assert(Rewriter::rewrite(learned) == learned);
- for (;;) {
- learnedNew = constantPropagations.apply(learned);
- if (learnedNew == learned) {
- break;
- }
- ++d_smt.d_stats->d_numConstantProps;
- learned = Rewriter::rewrite(learnedNew);
- }
- if (s.find(learned) != s.end()) {
- continue;
- }
- s.insert(learned);
- learnedBuilder << learned;
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "non-clausal learned : "
- << learned << endl;
- }
- learned_literals.clear();
-
- for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
- Node cProp = (*pos).first.eqNode((*pos).second);
- Assert(top_level_substs.apply(cProp) == cProp);
- Node cPropNew = newSubstitutions.apply(cProp);
- if (cProp != cPropNew) {
- cProp = Rewriter::rewrite(cPropNew);
- Assert(Rewriter::rewrite(cProp) == cProp);
- }
- if (s.find(cProp) != s.end()) {
- continue;
- }
- s.insert(cProp);
- learnedBuilder << cProp;
- Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
- << "non-clausal constant propagation : "
- << cProp << endl;
- }
-
- // Add new substitutions to topLevelSubstitutions
- // Note that we don't have to keep rhs's in full solved form
- // because SubstitutionMap::apply does a fixed-point iteration when substituting
- top_level_substs.addSubstitutions(newSubstitutions);
-
- if(learnedBuilder.getNumChildren() > 1) {
- d_assertions.replace(d_assertions.getRealAssertionsEnd() - 1,
- Rewriter::rewrite(Node(learnedBuilder)));
- }
-
- d_propagator.setNeedsFinish(true);
- return true;
-}
-
// returns false if simplification led to "false"
bool SmtEnginePrivate::simplifyAssertions()
{
Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
- dumpAssertions("pre-nonclausal", d_assertions);
-
- if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
- // Perform non-clausal simplification
- Chat() << "...performing nonclausal simplification..." << endl;
- Trace("simplify") << "SmtEnginePrivate::simplify(): "
- << "performing non-clausal simplification" << endl;
- bool noConflict = nonClausalSimplify();
- if(!noConflict) {
- return false;
+ if (options::simplificationMode() != SIMPLIFICATION_MODE_NONE)
+ {
+ if (!options::unsatCores() && !options::fewerPreprocessingHoles())
+ {
+ // Perform non-clausal simplification
+ PreprocessingPassResult res =
+ d_preprocessingPassRegistry.getPass("non-clausal-simp")
+ ->apply(&d_assertions);
+ if (res == PreprocessingPassResult::CONFLICT)
+ {
+ return false;
+ }
}
// We piggy-back off of the BackEdgesMap in the CircuitPropagator to
}
}
- dumpAssertions("post-nonclausal", d_assertions);
Trace("smt") << "POST nonClausalSimplify" << endl;
Debug("smt") << " d_assertions : " << d_assertions.size() << endl;
if (options::doITESimp()
&& (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat()))
{
- Chat() << "...doing ITE simplification..." << endl;
PreprocessingPassResult res =
d_preprocessingPassRegistry.getPass("ite-simp")->apply(&d_assertions);
if (res == PreprocessingPassResult::CONFLICT)
->apply(&d_assertions);
}
- if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
- Chat() << "...doing another round of nonclausal simplification..." << endl;
- Trace("simplify") << "SmtEnginePrivate::simplify(): "
- << " doing repeated simplification" << endl;
- bool noConflict = nonClausalSimplify();
- if(!noConflict) {
+ if (options::repeatSimp()
+ && options::simplificationMode() != SIMPLIFICATION_MODE_NONE
+ && !options::unsatCores() && !options::fewerPreprocessingHoles())
+ {
+ PreprocessingPassResult res =
+ d_preprocessingPassRegistry.getPass("non-clausal-simp")
+ ->apply(&d_assertions);
+ if (res == PreprocessingPassResult::CONFLICT)
+ {
return false;
}
}
cache[n] = true;
}
-void SmtEnginePrivate::recordSymbolsInAssertions(
- const std::vector<Node>& assertions)
-{
- std::unordered_set<TNode, TNodeHashFunction> visited;
- std::unordered_set<Node, NodeHashFunction> syms;
- for (TNode cn : assertions)
- {
- expr::getSymbols(cn, syms, visited);
- }
- for (const Node& s : syms)
- {
- d_symsInAssertions.insert(s);
- }
-}
-
bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache)
{
unordered_map<Node, bool, NodeHashFunction>::iterator it;
// if incremental, compute which variables are assigned
if (options::incrementalSolving())
{
- recordSymbolsInAssertions(d_assertions.ref());
+ d_preprocessingPassContext->recordSymbolsInAssertions(d_assertions.ref());
}
// Push the formula to SAT
projects / cvc5.git / commitdiff