Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/preprocessing/passes/non_clausal_simp.cpp	Lines:	217	225	96.4 %
Date:	2021-08-03	Branches:	490	1182	41.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Andrew Reynolds, Gereon Kremer
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * 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 <vector>

#include "context/cdo.h"
#include "options/smt_options.h"
#include "preprocessing/assertion_pipeline.h"
#include "preprocessing/preprocessing_pass_context.h"
#include "smt/preprocess_proof_generator.h"
#include "smt/smt_statistics_registry.h"
#include "theory/booleans/circuit_propagator.h"
#include "theory/theory.h"
#include "theory/theory_engine.h"
#include "theory/theory_model.h"
#include "theory/trust_substitutions.h"

using namespace cvc5;
using namespace cvc5::theory;

namespace cvc5 {
namespace preprocessing {
namespace passes {

/* -------------------------------------------------------------------------- */

NonClausalSimp::Statistics::Statistics()
    : d_numConstantProps(smtStatisticsRegistry().registerInt(
        "preprocessing::passes::NonClausalSimp::NumConstantProps"))
{
}


/* -------------------------------------------------------------------------- */

NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
    : 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())
{
}

PreprocessingPassResult NonClausalSimp::applyInternal(
    AssertionPipeline* assertionsToPreprocess)
{
  d_preprocContext->spendResource(Resource::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;
  for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
  {
    Assert(Rewriter::rewrite((*assertionsToPreprocess)[i])
           == (*assertionsToPreprocess)[i]);
    // Don't reprocess substitutions
    if (assertionsToPreprocess->isSubstsIndex(i))
    {
      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;
  TrustNode conf = propagator->propagate();
  if (!conf.isNull())
  {
    // If in conflict, just return false
    Trace("non-clausal-simplify")
        << "conflict in non-clausal propagation" << std::endl;
    assertionsToPreprocess->clear();
    assertionsToPreprocess->pushBackTrusted(conf);
    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
  context::Context* u = d_preprocContext->getUserContext();
  TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions();
  CVC5_UNUSED SubstitutionMap& top_level_substs = ttls.get();
  // 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);
    // 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;
    // 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].getNode() << std::endl;
        assertionsToPreprocess->clear();
        Node n = NodeManager::currentNM()->mkConst<bool>(false);
        assertionsToPreprocess->push_back(n, false, false, d_llpg.get());
        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;

    TrustNode tlearnedLiteral =
        TrustNode::mkTrustLemma(learnedLiteral, d_llpg.get());
    Theory::PPAssertStatus solveStatus =
        d_preprocContext->getTheoryEngine()->solve(tlearnedLiteral,
                                                   *newSubstitutions.get());

    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(nss.apply(learnedLiteral)).isConst());
        // 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;
        assertionsToPreprocess->clear();
        Node n = NodeManager::currentNM()->mkConst<bool>(false);
        assertionsToPreprocess->push_back(n);
        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(cps.apply(t, true) == t);
          Assert(top_level_substs.apply(t) == t);
          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
        {
          // Keep the literal
          learned_literals[j++] = learned_literals[i];
          // Its a literal that could not be processed as a substitution or
          // conflict. In this case, we notify the context of the learned
          // literal, which will process it with the learned literal manager.
          d_preprocContext->notifyLearnedLiteral(learnedLiteral);
        }
        break;
    }
  }

#ifdef CVC5_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 (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);
    Node app = nss.apply((*pos).second);
    Assert(nss.apply(app) == app);
  }
  for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos)
  {
    Assert((*pos).second.isConst());
    Assert(Rewriter::rewrite((*pos).first) == (*pos).first);
    Assert(cps.apply((*pos).second) == (*pos).second);
  }
#endif /* CVC5_ASSERTIONS */

  // Resize the learnt
  Trace("non-clausal-simplify")
      << "Resize non-clausal learned literals to " << j << std::endl;
  learned_literals.resize(j);

  std::unordered_set<TNode> s;
  for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
  {
    Node assertion = (*assertionsToPreprocess)[i];
    TrustNode assertionNew = newSubstitutions->applyTrusted(assertion);
    Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl;
    if (!assertionNew.isNull())
    {
      Trace("non-clausal-simplify")
          << "assertionNew = " << assertionNew.getNode() << std::endl;
      assertionsToPreprocess->replaceTrusted(i, assertionNew);
      assertion = assertionNew.getNode();
      Assert(Rewriter::rewrite(assertion) == assertion);
    }
    for (;;)
    {
      assertionNew = constantPropagations->applyTrusted(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 = " << assertion << std::endl;
    }
    s.insert(assertion);
    Trace("non-clausal-simplify")
        << "non-clausal preprocessed: " << assertion << std::endl;
  }

  // If necessary, add as assertions if needed (when incremental). This is
  // necessary because certain variables cannot truly be eliminated when
  // we are in incremental mode. For example, say our first call to check-sat
  // is a formula F containing variable x. On the second call to check-sat,
  // say we solve a top-level assertion (= x t). Since the solver already has
  // constraints involving x, we must still keep (= x t) as an assertion.
  // However, notice that we do not retract the substitution { x -> t }. This
  // means that all *subsequent* assertions after (= x t) will replace x by t.
  if (assertionsToPreprocess->storeSubstsInAsserts())
  {
    for (const std::pair<const Node, const Node>& pos: nss)
    {
      Node lhs = pos.first;
      // If using incremental, we must check whether this variable has occurred
      // before now. If it has, we must add as an assertion.
      if (d_preprocContext->getSymsInAssertions().contains(lhs))
      {
        // if it has, the substitution becomes an assertion
        TrustNode trhs = newSubstitutions->applyTrusted(lhs);
        Assert(!trhs.isNull());
        Trace("non-clausal-simplify")
            << "substitute: will notify SAT layer of substitution: "
            << trhs.getProven() << std::endl;
        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);
    // process learned literal
    learned = processLearnedLit(
        learned, newSubstitutions.get(), constantPropagations.get());
    if (s.find(learned) != s.end())
    {
      continue;
    }
    s.insert(learned);
    learnedLitsToConjoin.push_back(learned);
    Trace("non-clausal-simplify")
        << "non-clausal learned : " << learned << std::endl;
  }
  learned_literals.clear();

  for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos)
  {
    Node cProp = (*pos).first.eqNode((*pos).second);
    Assert(top_level_substs.apply(cProp) == cProp);
    // process learned literal (substitutions only)
    cProp = processLearnedLit(cProp, newSubstitutions.get(), nullptr);
    if (s.find(cProp) != s.end())
    {
      continue;
    }
    s.insert(cProp);
    learnedLitsToConjoin.push_back(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
  ttls.addSubstitutions(*newSubstitutions.get());

  if (!learnedLitsToConjoin.empty())
  {
    size_t replIndex = assertionsToPreprocess->getRealAssertionsEnd() - 1;
    Node newConj = NodeManager::currentNM()->mkAnd(learnedLitsToConjoin);
    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);

  // Note that typically ttls.apply(assert)==assert here.
  // However, this invariant is invalidated for cases where we use explicit
  // equality assertions for variables solved in incremental mode that already
  // exist in assertions, as described above.

  return PreprocessingPassResult::NO_CONFLICT;
}

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->applyTrusted(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->applyTrusted(lit);
      if (tlit.isNull())
      {
        break;
      }
      Assert(lit != tlit.getNode());
      lit = processRewrittenLearnedLit(tlit);
      d_statistics.d_numConstantProps += 1;
    }
  }
  return lit;
}

Node NonClausalSimp::processRewrittenLearnedLit(TrustNode trn)
{
  if (isProofEnabled())
  {
    d_llpg->notifyTrustedPreprocessed(trn);
  }
  // return the node
  return trn.getNode();
}

}  // namespace passes
}  // namespace preprocessing
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Andrew Reynolds, Gereon Kremer
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Non-clausal simplification preprocessing pass.
14		*
15		* Run the nonclausal solver and try to solve all assigned theory literals.
16		*/
17
18		#include "preprocessing/passes/non_clausal_simp.h"
19
20		#include <vector>
21
22		#include "context/cdo.h"
23		#include "options/smt_options.h"
24		#include "preprocessing/assertion_pipeline.h"
25		#include "preprocessing/preprocessing_pass_context.h"
26		#include "smt/preprocess_proof_generator.h"
27		#include "smt/smt_statistics_registry.h"
28		#include "theory/booleans/circuit_propagator.h"
29		#include "theory/theory.h"
30		#include "theory/theory_engine.h"
31		#include "theory/theory_model.h"
32		#include "theory/trust_substitutions.h"
33
34		using namespace cvc5;
35		using namespace cvc5::theory;
36
37		namespace cvc5 {
38		namespace preprocessing {
39		namespace passes {
40
41		/* -------------------------------------------------------------------------- */
42
43	9841	NonClausalSimp::Statistics::Statistics()
44	9841	: d_numConstantProps(smtStatisticsRegistry().registerInt(
45	9841	"preprocessing::passes::NonClausalSimp::NumConstantProps"))
46		{
47	9841	}
48
49
50		/* -------------------------------------------------------------------------- */
51
52	9841	NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext)
53		: PreprocessingPass(preprocContext, "non-clausal-simp"),
54	9841	d_pnm(preprocContext->getProofNodeManager()),
55	9841	d_llpg(d_pnm ? new smt::PreprocessProofGenerator(
56		d_pnm,
57	3759	preprocContext->getUserContext(),
58	3759	"NonClausalSimp::llpg")
59		: nullptr),
60	9841	d_llra(d_pnm ? new LazyCDProof(d_pnm,
61		nullptr,
62	3759	preprocContext->getUserContext(),
63	3759	"NonClausalSimp::llra")
64		: nullptr),
65	54400	d_tsubsList(preprocContext->getUserContext())
66		{
67	9841	}
68
69	11013	PreprocessingPassResult NonClausalSimp::applyInternal(
70		AssertionPipeline* assertionsToPreprocess)
71		{
72	11013	d_preprocContext->spendResource(Resource::PreprocessStep);
73
74		theory::booleans::CircuitPropagator* propagator =
75	11013	d_preprocContext->getCircuitPropagator();
76
77	95550	for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
78		{
79	169074	Trace("non-clausal-simplify") << "Assertion #" << i << " : "
80	84537	<< (*assertionsToPreprocess)[i] << std::endl;
81		}
82
83	11013	if (propagator->getNeedsFinish())
84		{
85	4203	propagator->finish();
86	4203	propagator->setNeedsFinish(false);
87		}
88	11013	propagator->initialize();
89
90		// Assert all the assertions to the propagator
91	11013	Trace("non-clausal-simplify") << "asserting to propagator" << std::endl;
92	95550	for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
93		{
94	84537	Assert(Rewriter::rewrite((*assertionsToPreprocess)[i])
95		== (*assertionsToPreprocess)[i]);
96		// Don't reprocess substitutions
97	84537	if (assertionsToPreprocess->isSubstsIndex(i))
98		{
99	3039	continue;
100		}
101	162996	Trace("non-clausal-simplify")
102	81498	<< "asserting " << (*assertionsToPreprocess)[i] << std::endl;
103	162996	Debug("cores") << "propagator->assertTrue: " << (*assertionsToPreprocess)[i]
104	81498	<< std::endl;
105	81498	propagator->assertTrue((*assertionsToPreprocess)[i]);
106		}
107
108	11013	Trace("non-clausal-simplify") << "propagating" << std::endl;
109	22026	TrustNode conf = propagator->propagate();
110	11013	if (!conf.isNull())
111		{
112		// If in conflict, just return false
113	1860	Trace("non-clausal-simplify")
114	930	<< "conflict in non-clausal propagation" << std::endl;
115	930	assertionsToPreprocess->clear();
116	930	assertionsToPreprocess->pushBackTrusted(conf);
117	930	propagator->setNeedsFinish(true);
118	930	return PreprocessingPassResult::CONFLICT;
119		}
120
121	20166	Trace("non-clausal-simplify")
122	20166	<< "Iterate through " << propagator->getLearnedLiterals().size()
123	10083	<< " learned literals." << std::endl;
124		// No conflict, go through the literals and solve them
125	10083	context::Context* u = d_preprocContext->getUserContext();
126	10083	TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions();
127	10083	CVC5_UNUSED SubstitutionMap& top_level_substs = ttls.get();
128		// constant propagations
129		std::shared_ptr<TrustSubstitutionMap> constantPropagations =
130		std::make_shared<TrustSubstitutionMap>(
131	20166	u, d_pnm, "NonClausalSimp::cprop", PfRule::PREPROCESS_LEMMA);
132	10083	SubstitutionMap& cps = constantPropagations->get();
133		// new substitutions
134		std::shared_ptr<TrustSubstitutionMap> newSubstitutions =
135		std::make_shared<TrustSubstitutionMap>(
136	20166	u, d_pnm, "NonClausalSimp::newSubs", PfRule::PREPROCESS_LEMMA);
137	10083	SubstitutionMap& nss = newSubstitutions->get();
138
139	10083	size_t j = 0;
140	10083	std::vector<TrustNode>& learned_literals = propagator->getLearnedLiterals();
141		// if proofs are enabled, we will need to track the proofs of learned literals
142	10083	if (isProofEnabled())
143		{
144	1804	d_tsubsList.push_back(constantPropagations);
145	1804	d_tsubsList.push_back(newSubstitutions);
146	30090	for (const TrustNode& tll : learned_literals)
147		{
148	28286	d_llpg->notifyNewTrustedAssert(tll);
149		}
150		}
151	124013	for (size_t i = 0, size = learned_literals.size(); i < size; ++i)
152		{
153		// Simplify the literal we learned wrt previous substitutions
154	227477	Node learnedLiteral = learned_literals[i].getNode();
155	114089	Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
156	114089	Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral);
157		// process the learned literal with substitutions and const propagations
158	114089	learnedLiteral = processLearnedLit(
159		learnedLiteral, newSubstitutions.get(), constantPropagations.get());
160	228178	Trace("non-clausal-simplify")
161	114089	<< "Process learnedLiteral, after constProp : " << learnedLiteral
162	114089	<< std::endl;
163		// It might just simplify to a constant
164	114089	if (learnedLiteral.isConst())
165		{
166	701	if (learnedLiteral.getConst<bool>())
167		{
168		// If the learned literal simplifies to true, it's redundant
169	542	continue;
170		}
171		else
172		{
173		// If the learned literal simplifies to false, we're in conflict
174	318	Trace("non-clausal-simplify")
175	159	<< "conflict with " << learned_literals[i].getNode() << std::endl;
176	159	assertionsToPreprocess->clear();
177	318	Node n = NodeManager::currentNM()->mkConst<bool>(false);
178	159	assertionsToPreprocess->push_back(n, false, false, d_llpg.get());
179	159	propagator->setNeedsFinish(true);
180	159	return PreprocessingPassResult::CONFLICT;
181		}
182		}
183
184		// Solve it with the corresponding theory, possibly adding new
185		// substitutions to newSubstitutions
186	113388	Trace("non-clausal-simplify") << "solving " << learnedLiteral << std::endl;
187
188		TrustNode tlearnedLiteral =
189	226776	TrustNode::mkTrustLemma(learnedLiteral, d_llpg.get());
190		Theory::PPAssertStatus solveStatus =
191	340164	d_preprocContext->getTheoryEngine()->solve(tlearnedLiteral,
192	226776	*newSubstitutions.get());
193
194	113388	switch (solveStatus)
195		{
196	48111	case Theory::PP_ASSERT_STATUS_SOLVED:
197		{
198		// The literal should rewrite to true
199	96222	Trace("non-clausal-simplify")
200	48111	<< "solved " << learnedLiteral << std::endl;
201	48111	Assert(Rewriter::rewrite(nss.apply(learnedLiteral)).isConst());
202		// else fall through
203	48111	break;
204		}
205		case Theory::PP_ASSERT_STATUS_CONFLICT:
206		{
207		// If in conflict, we return false
208		Trace("non-clausal-simplify")
209		<< "conflict while solving " << learnedLiteral << std::endl;
210		assertionsToPreprocess->clear();
211		Node n = NodeManager::currentNM()->mkConst<bool>(false);
212		assertionsToPreprocess->push_back(n);
213		propagator->setNeedsFinish(true);
214		return PreprocessingPassResult::CONFLICT;
215		}
216	65277	default:
217	130554	if (learnedLiteral.getKind() == kind::EQUAL
218	130554	&& (learnedLiteral[0].isConst() \|\| learnedLiteral[1].isConst()))
219		{
220		// constant propagation
221	11026	TNode t;
222	11026	TNode c;
223	5513	if (learnedLiteral[0].isConst())
224		{
225	208	t = learnedLiteral[1];
226	208	c = learnedLiteral[0];
227		}
228		else
229		{
230	5305	t = learnedLiteral[0];
231	5305	c = learnedLiteral[1];
232		}
233	5513	Assert(!t.isConst());
234	5513	Assert(cps.apply(t, true) == t);
235	5513	Assert(top_level_substs.apply(t) == t);
236	5513	Assert(nss.apply(t) == t);
237		// also add to learned literal
238	11026	ProofGenerator* cpg = constantPropagations->addSubstitutionSolved(
239	5513	t, c, tlearnedLiteral);
240		// We need to justify (= t c) as a literal, since it is reasserted
241		// to the assertion pipeline below. We do this with the proof
242		// generator returned by the above call.
243	5513	if (isProofEnabled())
244		{
245	1444	d_llpg->notifyNewAssert(t.eqNode(c), cpg);
246		}
247		}
248		else
249		{
250		// Keep the literal
251	59764	learned_literals[j++] = learned_literals[i];
252		// Its a literal that could not be processed as a substitution or
253		// conflict. In this case, we notify the context of the learned
254		// literal, which will process it with the learned literal manager.
255	59764	d_preprocContext->notifyLearnedLiteral(learnedLiteral);
256		}
257	65277	break;
258		}
259		}
260
261		#ifdef CVC5_ASSERTIONS
262		// NOTE: When debugging this code, consider moving this check inside of the
263		// loop over propagator->getLearnedLiterals(). This check has been moved
264		// outside because it is costly for certain inputs (see bug 508).
265		//
266		// Check data structure invariants:
267		// 1. for each lhs of top_level_substs, does not appear anywhere in rhs of
268		// top_level_substs or anywhere in constantPropagations
269		// 2. each lhs of constantPropagations rewrites to itself
270		// 3. if l -> r is a constant propagation and l is a subterm of l' with l' ->
271		// r' another constant propagation, then l'[l/r] -> r' should be a
272		// constant propagation too
273		// 4. each lhs of constantPropagations is different from each rhs
274	57434	for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos)
275		{
276	47510	Assert((*pos).first.isVar());
277	47510	Assert(top_level_substs.apply((pos).first) == (pos).first);
278	47510	Assert(top_level_substs.apply((pos).second) == (pos).second);
279	95020	Node app = nss.apply((*pos).second);
280	47510	Assert(nss.apply(app) == app);
281		}
282	15415	for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos)
283		{
284	5491	Assert((*pos).second.isConst());
285	5491	Assert(Rewriter::rewrite((pos).first) == (pos).first);
286	5491	Assert(cps.apply((pos).second) == (pos).second);
287		}
288		#endif /* CVC5_ASSERTIONS */
289
290		// Resize the learnt
291	19848	Trace("non-clausal-simplify")
292	9924	<< "Resize non-clausal learned literals to " << j << std::endl;
293	9924	learned_literals.resize(j);
294
295	19848	std::unordered_set<TNode> s;
296	89588	for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
297		{
298	159328	Node assertion = (*assertionsToPreprocess)[i];
299	159328	TrustNode assertionNew = newSubstitutions->applyTrusted(assertion);
300	79664	Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl;
301	79664	if (!assertionNew.isNull())
302		{
303	57424	Trace("non-clausal-simplify")
304	28712	<< "assertionNew = " << assertionNew.getNode() << std::endl;
305	28712	assertionsToPreprocess->replaceTrusted(i, assertionNew);
306	28712	assertion = assertionNew.getNode();
307	28712	Assert(Rewriter::rewrite(assertion) == assertion);
308		}
309		for (;;)
310		{
311	81748	assertionNew = constantPropagations->applyTrusted(assertion);
312	80706	if (assertionNew.isNull())
313		{
314	79664	break;
315		}
316	1042	Assert(assertionNew.getNode() != assertion);
317	1042	assertionsToPreprocess->replaceTrusted(i, assertionNew);
318	1042	assertion = assertionNew.getNode();
319	1042	d_statistics.d_numConstantProps += 1;
320	2084	Trace("non-clausal-simplify")
321	1042	<< "assertionNew = " << assertion << std::endl;
322		}
323	79664	s.insert(assertion);
324	159328	Trace("non-clausal-simplify")
325	79664	<< "non-clausal preprocessed: " << assertion << std::endl;
326		}
327
328		// If necessary, add as assertions if needed (when incremental). This is
329		// necessary because certain variables cannot truly be eliminated when
330		// we are in incremental mode. For example, say our first call to check-sat
331		// is a formula F containing variable x. On the second call to check-sat,
332		// say we solve a top-level assertion (= x t). Since the solver already has
333		// constraints involving x, we must still keep (= x t) as an assertion.
334		// However, notice that we do not retract the substitution { x -> t }. This
335		// means that all subsequent assertions after (= x t) will replace x by t.
336	9924	if (assertionsToPreprocess->storeSubstsInAsserts())
337		{
338	5469	for (const std::pair<const Node, const Node>& pos: nss)
339		{
340	5290	Node lhs = pos.first;
341		// If using incremental, we must check whether this variable has occurred
342		// before now. If it has, we must add as an assertion.
343	2645	if (d_preprocContext->getSymsInAssertions().contains(lhs))
344		{
345		// if it has, the substitution becomes an assertion
346	2734	TrustNode trhs = newSubstitutions->applyTrusted(lhs);
347	1367	Assert(!trhs.isNull());
348	2734	Trace("non-clausal-simplify")
349	1367	<< "substitute: will notify SAT layer of substitution: "
350	1367	<< trhs.getProven() << std::endl;
351	1367	assertionsToPreprocess->addSubstitutionNode(trhs.getProven(),
352		trhs.getGenerator());
353		}
354		}
355		}
356
357	9924	Assert(assertionsToPreprocess->getRealAssertionsEnd()
358		<= assertionsToPreprocess->size());
359		// Learned literals to conjoin. If proofs are enabled, all these are
360		// justified by d_llpg.
361	19848	std::vector<Node> learnedLitsToConjoin;
362
363	69132	for (size_t i = 0; i < learned_literals.size(); ++i)
364		{
365	97274	Node learned = learned_literals[i].getNode();
366	59208	Assert(top_level_substs.apply(learned) == learned);
367		// process learned literal
368	59208	learned = processLearnedLit(
369		learned, newSubstitutions.get(), constantPropagations.get());
370	59208	if (s.find(learned) != s.end())
371		{
372	21142	continue;
373		}
374	38066	s.insert(learned);
375	38066	learnedLitsToConjoin.push_back(learned);
376	76132	Trace("non-clausal-simplify")
377	38066	<< "non-clausal learned : " << learned << std::endl;
378		}
379	9924	learned_literals.clear();
380
381	15415	for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos)
382		{
383	10875	Node cProp = (pos).first.eqNode((pos).second);
384	5491	Assert(top_level_substs.apply(cProp) == cProp);
385		// process learned literal (substitutions only)
386	5491	cProp = processLearnedLit(cProp, newSubstitutions.get(), nullptr);
387	5491	if (s.find(cProp) != s.end())
388		{
389	107	continue;
390		}
391	5384	s.insert(cProp);
392	5384	learnedLitsToConjoin.push_back(cProp);
393	10768	Trace("non-clausal-simplify")
394	5384	<< "non-clausal constant propagation : " << cProp << std::endl;
395		}
396
397		// Add new substitutions to topLevelSubstitutions
398		// Note that we don't have to keep rhs's in full solved form
399		// because SubstitutionMap::apply does a fixed-point iteration when
400		// substituting
401	9924	ttls.addSubstitutions(*newSubstitutions.get());
402
403	9924	if (!learnedLitsToConjoin.empty())
404		{
405	2457	size_t replIndex = assertionsToPreprocess->getRealAssertionsEnd() - 1;
406	4914	Node newConj = NodeManager::currentNM()->mkAnd(learnedLitsToConjoin);
407	4914	Trace("non-clausal-simplify")
408	2457	<< "non-clausal simplification, reassert: " << newConj << std::endl;
409	2457	ProofGenerator* pg = nullptr;
410	2457	if (isProofEnabled())
411		{
412		// justify in d_llra
413	15321	for (const Node& lit : learnedLitsToConjoin)
414		{
415	14883	d_llra->addLazyStep(lit, d_llpg.get());
416		}
417	438	if (learnedLitsToConjoin.size() > 1)
418		{
419	324	d_llra->addStep(newConj, PfRule::AND_INTRO, learnedLitsToConjoin, {});
420	324	pg = d_llra.get();
421		}
422		else
423		{
424		// otherwise we ask the learned literal proof generator directly
425	114	pg = d_llpg.get();
426		}
427		}
428		// ------- from d_llpg --------- from d_llpg
429		// conj[0] .... d_conj[n]
430		// -------------------------------- AND_INTRO
431		// newConj
432		// where newConj is conjoined at the given index
433	2457	assertionsToPreprocess->conjoin(replIndex, newConj, pg);
434		}
435
436	9924	propagator->setNeedsFinish(true);
437
438		// Note that typically ttls.apply(assert)==assert here.
439		// However, this invariant is invalidated for cases where we use explicit
440		// equality assertions for variables solved in incremental mode that already
441		// exist in assertions, as described above.
442
443	9924	return PreprocessingPassResult::NO_CONFLICT;
444		}
445
446	58903	bool NonClausalSimp::isProofEnabled() const { return d_pnm != nullptr; }
447
448	178788	Node NonClausalSimp::processLearnedLit(Node lit,
449		theory::TrustSubstitutionMap* subs,
450		theory::TrustSubstitutionMap* cp)
451		{
452	357576	TrustNode tlit;
453	178788	if (subs != nullptr)
454		{
455	178788	tlit = subs->applyTrusted(lit);
456	178788	if (!tlit.isNull())
457		{
458	40708	lit = processRewrittenLearnedLit(tlit);
459		}
460	357576	Trace("non-clausal-simplify")
461	178788	<< "Process learnedLiteral, after newSubs : " << lit << std::endl;
462		}
463		// apply to fixed point
464	178788	if (cp != nullptr)
465		{
466		for (;;)
467		{
468	173581	tlit = cp->applyTrusted(lit);
469	173439	if (tlit.isNull())
470		{
471	173297	break;
472		}
473	142	Assert(lit != tlit.getNode());
474	142	lit = processRewrittenLearnedLit(tlit);
475	142	d_statistics.d_numConstantProps += 1;
476		}
477		}
478	357576	return lit;
479		}
480
481	40850	Node NonClausalSimp::processRewrittenLearnedLit(TrustNode trn)
482		{
483	40850	if (isProofEnabled())
484		{
485	15195	d_llpg->notifyTrustedPreprocessed(trn);
486		}
487		// return the node
488	40850	return trn.getNode();
489		}
490
491		} // namespace passes
492		} // namespace preprocessing
493	29286	} // namespace cvc5