From f5746ca4a24c1b9f05f5528bc66016668d9a7863 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 10 Sep 2018 17:16:28 -0700 Subject: [PATCH] Refactor non-clausal simplify preprocessing pass. (#2425) --- src/Makefile.am | 2 + src/preprocessing/passes/non_clausal_simp.cpp | 460 ++++++++++++++++++ src/preprocessing/passes/non_clausal_simp.h | 57 +++ .../preprocessing_pass_context.cpp | 20 +- .../preprocessing_pass_context.h | 23 +- src/smt/smt_engine.cpp | 441 ++--------------- 6 files changed, 590 insertions(+), 413 deletions(-) create mode 100644 src/preprocessing/passes/non_clausal_simp.cpp create mode 100644 src/preprocessing/passes/non_clausal_simp.h diff --git a/src/Makefile.am b/src/Makefile.am index 55b395e7a..e11a1374d 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -89,6 +89,8 @@ libcvc4_la_SOURCES = \ preprocessing/passes/ite_removal.h \ preprocessing/passes/ite_simp.cpp \ preprocessing/passes/ite_simp.h \ + preprocessing/passes/non_clausal_simp.cpp \ + preprocessing/passes/non_clausal_simp.h \ preprocessing/passes/nl_ext_purify.cpp \ preprocessing/passes/nl_ext_purify.h \ preprocessing/passes/pseudo_boolean_processor.cpp \ diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp new file mode 100644 index 000000000..e2ce1c301 --- /dev/null +++ b/src/preprocessing/passes/non_clausal_simp.cpp @@ -0,0 +1,460 @@ +/********************* */ +/*! \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 + +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& 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(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& 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()) + { + // 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(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 > 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(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 > 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(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 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 diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h new file mode 100644 index 000000000..2a244d7ad --- /dev/null +++ b/src/preprocessing/passes/non_clausal_simp.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file non_clausal_simp.h + ** \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. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H +#define __CVC4__PREPROCESSING__PASSES__NON_CLAUSAL_SIMP_H + +#include + +#include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class NonClausalSimp : public PreprocessingPass +{ + public: + NonClausalSimp(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + struct Statistics + { + IntStat d_numConstantProps; + Statistics(); + ~Statistics(); + }; + + Statistics d_statistics; + + /** Learned literals */ + std::vector d_nonClausalLearnedLiterals; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index af66c2a2a..15f5d3eb0 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -16,6 +16,8 @@ #include "preprocessing_pass_context.h" +#include "expr/node_algorithm.h" + namespace CVC4 { namespace preprocessing { @@ -27,7 +29,8 @@ PreprocessingPassContext::PreprocessingPassContext( : d_smt(smt), d_resourceManager(resourceManager), d_iteRemover(iteRemover), - d_circuitPropagator(circuitPropagator) + d_circuitPropagator(circuitPropagator), + d_symsInAssertions(smt->d_userContext) { } @@ -43,5 +46,20 @@ void PreprocessingPassContext::enableIntegers() req.enableIntegers(); } +void PreprocessingPassContext::recordSymbolsInAssertions( + const std::vector& assertions) +{ + std::unordered_set visited; + std::unordered_set syms; + for (TNode cn : assertions) + { + expr::getSymbols(cn, syms, visited); + } + for (const Node& s : syms) + { + d_symsInAssertions.insert(s); + } +} + } // namespace preprocessing } // namespace CVC4 diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index a2e83aa4c..ae989d700 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -55,6 +55,11 @@ class PreprocessingPassContext return d_circuitPropagator; } + context::CDHashSet& getSymsInAssertions() + { + return d_symsInAssertions; + } + void spendResource(unsigned amount) { d_resourceManager->spendResource(amount); @@ -68,9 +73,18 @@ class PreprocessingPassContext /* Enable Integers. */ void enableIntegers(); + /** 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& assertions); + private: - /* Pointer to the SmtEngine that this context was created in. */ + /** Pointer to the SmtEngine that this context was created in. */ SmtEngine* d_smt; + + /** Pointer to the ResourceManager for this context. */ ResourceManager* d_resourceManager; /** Instance of the ITE remover */ @@ -78,6 +92,13 @@ class PreprocessingPassContext /** Instance of the circuit propagator */ theory::booleans::CircuitPropagator* d_circuitPropagator; + + /** + * The (user-context-dependent) set of symbols that occur in at least one + * assertion in the current user context. + */ + context::CDHashSet d_symsInAssertions; + }; // class PreprocessingPassContext } // namespace preprocessing diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 17edaad41..8cd236a89 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -84,8 +84,9 @@ #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" @@ -449,7 +450,6 @@ class SmtEnginePrivate : public NodeManagerListener { typedef unordered_map NodeToNodeHashMap; typedef unordered_map NodeToBoolHashMap; - typedef context::CDHashSet NodeSet; /** * Manager for limiting time and abstract resource usage. @@ -505,13 +505,6 @@ class SmtEnginePrivate : public NodeManagerListener { */ 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 @@ -544,23 +537,6 @@ class SmtEnginePrivate : public NodeManagerListener { std::unique_ptr 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& assertions); - /** * Helper function to fix up assertion list to restore invariants needed after * ite removal. @@ -595,7 +571,6 @@ class SmtEnginePrivate : public NodeManagerListener { 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? @@ -2618,6 +2593,8 @@ void SmtEnginePrivate::finishInit() new ITESimp(d_preprocessingPassContext.get())); std::unique_ptr nlExtPurify( new NlExtPurify(d_preprocessingPassContext.get())); + std::unique_ptr nonClausalSimp( + new NonClausalSimp(d_preprocessingPassContext.get())); std::unique_ptr mipLibTrick( new MipLibTrick(d_preprocessingPassContext.get())); std::unique_ptr quantifiersPreprocess( @@ -2668,17 +2645,19 @@ void SmtEnginePrivate::finishInit() 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", @@ -2895,354 +2874,6 @@ static void dumpAssertions(const char* key, } } -// 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& 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(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& 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()) { - // 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(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 > 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(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 > 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(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 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() { @@ -3253,16 +2884,18 @@ 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 @@ -3286,7 +2919,6 @@ bool SmtEnginePrivate::simplifyAssertions() } } - dumpAssertions("post-nonclausal", d_assertions); Trace("smt") << "POST nonClausalSimplify" << endl; Debug("smt") << " d_assertions : " << d_assertions.size() << endl; @@ -3304,7 +2936,6 @@ bool SmtEnginePrivate::simplifyAssertions() 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) @@ -3324,12 +2955,15 @@ bool SmtEnginePrivate::simplifyAssertions() ->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; } } @@ -3438,21 +3072,6 @@ void SmtEnginePrivate::collectSkolems(TNode n, set& skolemSet, unordered_ cache[n] = true; } -void SmtEnginePrivate::recordSymbolsInAssertions( - const std::vector& assertions) -{ - std::unordered_set visited; - std::unordered_set 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& cache) { unordered_map::iterator it; @@ -3871,7 +3490,7 @@ void SmtEnginePrivate::processAssertions() { // 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 -- 2.30.2