/* -------------------------------------------------------------------------- */
NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
- : PreprocessingPass(preprocContext, "non-clausal-simp")
+ : PreprocessingPass(preprocContext, "non-clausal-simp"),
+ d_pnm(preprocContext->getProofNodeManager()),
+ d_llpg(d_pnm ? new smt::PreprocessProofGenerator(
+ d_pnm,
+ preprocContext->getUserContext(),
+ "NonClausalSimp::llpg")
+ : nullptr),
+ d_llra(d_pnm ? new LazyCDProof(d_pnm,
+ nullptr,
+ preprocContext->getUserContext(),
+ "NonClausalSimp::llra")
+ : nullptr),
+ d_tsubsList(preprocContext->getUserContext())
{
}
<< "conflict in non-clausal propagation" << std::endl;
Assert(!options::unsatCores());
assertionsToPreprocess->clear();
- Node n = NodeManager::currentNM()->mkConst<bool>(false);
- assertionsToPreprocess->push_back(n);
+ assertionsToPreprocess->pushBackTrusted(conf);
if (options::unsatCores())
{
- ProofManager::currentPM()->addDependence(n, Node::null());
+ ProofManager::currentPM()->addDependence(conf.getNode(), Node::null());
}
propagator->setNeedsFinish(true);
return PreprocessingPassResult::CONFLICT;
<< "Iterate through " << propagator->getLearnedLiterals().size()
<< " learned literals." << std::endl;
// No conflict, go through the literals and solve them
+ context::Context* u = d_preprocContext->getUserContext();
TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions();
CVC4_UNUSED SubstitutionMap& top_level_substs = ttls.get();
- SubstitutionMap constantPropagations(d_preprocContext->getUserContext());
- TrustSubstitutionMap tnewSubstituions(d_preprocContext->getUserContext(),
- nullptr);
- SubstitutionMap& newSubstitutions = tnewSubstituions.get();
- SubstitutionMap::iterator pos;
+ // constant propagations
+ std::shared_ptr<TrustSubstitutionMap> constantPropagations =
+ std::make_shared<TrustSubstitutionMap>(
+ u, d_pnm, "NonClausalSimp::cprop", PfRule::PREPROCESS_LEMMA);
+ SubstitutionMap& cps = constantPropagations->get();
+ // new substitutions
+ std::shared_ptr<TrustSubstitutionMap> newSubstitutions =
+ std::make_shared<TrustSubstitutionMap>(
+ u, d_pnm, "NonClausalSimp::newSubs", PfRule::PREPROCESS_LEMMA);
+ SubstitutionMap& nss = newSubstitutions->get();
+
size_t j = 0;
std::vector<TrustNode>& learned_literals = propagator->getLearnedLiterals();
+ // if proofs are enabled, we will need to track the proofs of learned literals
+ if (isProofEnabled())
+ {
+ d_tsubsList.push_back(constantPropagations);
+ d_tsubsList.push_back(newSubstitutions);
+ for (const TrustNode& tll : learned_literals)
+ {
+ d_llpg->notifyNewTrustedAssert(tll);
+ }
+ }
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].getNode();
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);
- }
+ // process the learned literal with substitutions and const propagations
+ learnedLiteral = processLearnedLit(
+ learnedLiteral, newSubstitutions.get(), constantPropagations.get());
Trace("non-clausal-simplify")
<< "Process learnedLiteral, after constProp : " << learnedLiteral
<< std::endl;
Assert(!options::unsatCores());
assertionsToPreprocess->clear();
Node n = NodeManager::currentNM()->mkConst<bool>(false);
- assertionsToPreprocess->push_back(n);
+ assertionsToPreprocess->push_back(n, false, false, d_llpg.get());
if (options::unsatCores())
{
ProofManager::currentPM()->addDependence(n, Node::null());
// Solve it with the corresponding theory, possibly adding new
// substitutions to newSubstitutions
Trace("non-clausal-simplify") << "solving " << learnedLiteral << std::endl;
+
TrustNode tlearnedLiteral =
- TrustNode::mkTrustLemma(learnedLiteral, nullptr);
+ TrustNode::mkTrustLemma(learnedLiteral, d_llpg.get());
Theory::PPAssertStatus solveStatus =
d_preprocContext->getTheoryEngine()->solve(tlearnedLiteral,
- tnewSubstituions);
+ *newSubstitutions.get());
switch (solveStatus)
{
// 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);
+ Assert(Rewriter::rewrite(nss.apply(learnedLiteral)).isConst());
// else fall through
break;
}
c = learnedLiteral[1];
}
Assert(!t.isConst());
- Assert(constantPropagations.apply(t) == t);
+ Assert(cps.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);
- // false); return;
- // }
- // top_level_substs.simplifyRHS(constantPropagations);
+ Assert(nss.apply(t) == t);
+ // also add to learned literal
+ ProofGenerator* cpg = constantPropagations->addSubstitutionSolved(
+ t, c, tlearnedLiteral);
+ // We need to justify (= t c) as a literal, since it is reasserted
+ // to the assertion pipeline below. We do this with the proof
+ // generator returned by the above call.
+ if (isProofEnabled())
+ {
+ d_llpg->notifyNewAssert(t.eqNode(c), cpg);
+ }
}
else
{
// 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)
+ for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.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));
+ Node app = nss.apply((*pos).second);
+ Assert(nss.apply(app) == app);
}
- for (pos = constantPropagations.begin(); pos != constantPropagations.end();
- ++pos)
+ for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.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);
+ Assert(cps.apply((*pos).second) == (*pos).second);
}
#endif /* CVC4_ASSERTIONS */
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
{
Node assertion = (*assertionsToPreprocess)[i];
- Node assertionNew = newSubstitutions.apply(assertion);
+ TrustNode assertionNew = newSubstitutions->apply(assertion);
Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl;
- Trace("non-clausal-simplify")
- << "assertionNew = " << assertionNew << std::endl;
- if (assertion != assertionNew)
+ if (!assertionNew.isNull())
{
- assertion = Rewriter::rewrite(assertionNew);
Trace("non-clausal-simplify")
- << "rewrite(assertion) = " << assertion << std::endl;
+ << "assertionNew = " << assertionNew.getNode() << std::endl;
+ assertionsToPreprocess->replaceTrusted(i, assertionNew);
+ assertion = assertionNew.getNode();
+ Assert(Rewriter::rewrite(assertion) == assertion);
}
- Assert(Rewriter::rewrite(assertion) == assertion);
for (;;)
{
- assertionNew = constantPropagations.apply(assertion);
- if (assertionNew == assertion)
+ assertionNew = constantPropagations->apply(assertion);
+ if (assertionNew.isNull())
{
break;
}
+ Assert(assertionNew.getNode() != assertion);
+ assertionsToPreprocess->replaceTrusted(i, assertionNew);
+ assertion = assertionNew.getNode();
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;
+ << "assertionNew = " << assertion << std::endl;
}
s.insert(assertion);
- assertionsToPreprocess->replace(i, assertion);
Trace("non-clausal-simplify")
<< "non-clausal preprocessed: " << assertion << std::endl;
}
TheoryModel* m = d_preprocContext->getTheoryEngine()->getModel();
Assert(m != nullptr);
NodeManager* nm = NodeManager::currentNM();
- for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos)
+ for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos)
{
Node lhs = (*pos).first;
- Node rhs = newSubstitutions.apply((*pos).second);
+ TrustNode trhs = newSubstitutions->apply((*pos).second);
+ Node rhs = trhs.isNull() ? (*pos).second : trhs.getNode();
// 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 (!assertionsToPreprocess->storeSubstsInAsserts()
Trace("non-clausal-simplify")
<< "substitute: will notify SAT layer of substitution: " << eq
<< std::endl;
- assertionsToPreprocess->addSubstitutionNode(eq);
+ trhs = newSubstitutions->apply((*pos).first);
+ Assert(!trhs.isNull());
+ assertionsToPreprocess->addSubstitutionNode(trhs.getProven(),
+ trhs.getGenerator());
}
}
Assert(assertionsToPreprocess->getRealAssertionsEnd()
<= assertionsToPreprocess->size());
+ // Learned literals to conjoin. If proofs are enabled, all these are
+ // justified by d_llpg.
std::vector<Node> learnedLitsToConjoin;
for (size_t i = 0; i < learned_literals.size(); ++i)
{
Node learned = learned_literals[i].getNode();
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);
- }
+ // process learned literal
+ learned = processLearnedLit(
+ learned, newSubstitutions.get(), constantPropagations.get());
if (s.find(learned) != s.end())
{
continue;
}
learned_literals.clear();
- for (pos = constantPropagations.begin(); pos != constantPropagations.end();
- ++pos)
+ for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.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);
- }
+ // process learned literal (substitutions only)
+ cProp = processLearnedLit(cProp, newSubstitutions.get(), nullptr);
if (s.find(cProp) != s.end())
{
continue;
// 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);
+ ttls.addSubstitutions(*newSubstitutions.get());
if (!learnedLitsToConjoin.empty())
{
size_t replIndex = assertionsToPreprocess->getRealAssertionsEnd() - 1;
Node newConj = NodeManager::currentNM()->mkAnd(learnedLitsToConjoin);
- assertionsToPreprocess->conjoin(replIndex, newConj);
+ Trace("non-clausal-simplify")
+ << "non-clausal simplification, reassert: " << newConj << std::endl;
+ ProofGenerator* pg = nullptr;
+ if (isProofEnabled())
+ {
+ // justify in d_llra
+ for (const Node& lit : learnedLitsToConjoin)
+ {
+ d_llra->addLazyStep(lit, d_llpg.get());
+ }
+ if (learnedLitsToConjoin.size() > 1)
+ {
+ d_llra->addStep(newConj, PfRule::AND_INTRO, learnedLitsToConjoin, {});
+ pg = d_llra.get();
+ }
+ else
+ {
+ // otherwise we ask the learned literal proof generator directly
+ pg = d_llpg.get();
+ }
+ }
+ // ------- from d_llpg --------- from d_llpg
+ // conj[0] .... d_conj[n]
+ // -------------------------------- AND_INTRO
+ // newConj
+ // where newConj is conjoined at the given index
+ assertionsToPreprocess->conjoin(replIndex, newConj, pg);
}
propagator->setNeedsFinish(true);
return PreprocessingPassResult::NO_CONFLICT;
-} // namespace passes
+}
-/* -------------------------------------------------------------------------- */
+bool NonClausalSimp::isProofEnabled() const { return d_pnm != nullptr; }
+
+Node NonClausalSimp::processLearnedLit(Node lit,
+ theory::TrustSubstitutionMap* subs,
+ theory::TrustSubstitutionMap* cp)
+{
+ TrustNode tlit;
+ if (subs != nullptr)
+ {
+ tlit = subs->apply(lit);
+ if (!tlit.isNull())
+ {
+ lit = processRewrittenLearnedLit(tlit);
+ }
+ Trace("non-clausal-simplify")
+ << "Process learnedLiteral, after newSubs : " << lit << std::endl;
+ }
+ // apply to fixed point
+ if (cp != nullptr)
+ {
+ for (;;)
+ {
+ tlit = cp->apply(lit);
+ if (tlit.isNull())
+ {
+ break;
+ }
+ Assert(lit != tlit.getNode());
+ lit = processRewrittenLearnedLit(tlit);
+ d_statistics.d_numConstantProps += 1;
+ }
+ }
+ return lit;
+}
+
+Node NonClausalSimp::processRewrittenLearnedLit(theory::TrustNode trn)
+{
+ if (isProofEnabled())
+ {
+ d_llpg->notifyTrustedPreprocessed(trn);
+ }
+ // return the node
+ return trn.getNode();
+}
} // namespace passes
} // namespace preprocessing
projects / cvc5.git / commitdiff