Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/proof_equality_engine.cpp	Lines:	206	263	78.3 %
Date:	2021-09-17	Branches:	472	1328	35.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Gereon Kremer, Aina Niemetz
 *
 * 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.
 * ****************************************************************************
 *
 * Implementation of the proof-producing equality engine.
 */

#include "theory/uf/proof_equality_engine.h"

#include "proof/lazy_proof_chain.h"
#include "proof/proof_node.h"
#include "proof/proof_node_manager.h"
#include "theory/rewriter.h"
#include "theory/uf/eq_proof.h"
#include "theory/uf/equality_engine.h"
#include "theory/uf/proof_checker.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace eq {

ProofEqEngine::ProofEqEngine(context::Context* c,
                             context::UserContext* u,
                             EqualityEngine& ee,
                             ProofNodeManager* pnm)
    : EagerProofGenerator(pnm, u, "pfee::" + ee.identify()),
      d_ee(ee),
      d_factPg(c, pnm),
      d_assumpPg(pnm),
      d_pnm(pnm),
      d_proof(pnm, nullptr, c, "pfee::LazyCDProof::" + ee.identify()),
      d_keep(c)
{
  NodeManager* nm = NodeManager::currentNM();
  d_true = nm->mkConst(true);
  d_false = nm->mkConst(false);
  AlwaysAssert(pnm != nullptr)
      << "Should not construct ProofEqEngine without proof node manager";
}

bool ProofEqEngine::assertFact(Node lit,
                               PfRule id,
                               const std::vector<Node>& exp,
                               const std::vector<Node>& args)
{
  Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
                << ", args = " << args << std::endl;

  Node atom = lit.getKind() == NOT ? lit[0] : lit;
  bool polarity = lit.getKind() != NOT;
  // register the step in the proof
  if (holds(atom, polarity))
  {
    // we do not process this fact if it already holds
    return false;
  }
  // Buffer the step in the fact proof generator. We do this instead of
  // adding explict steps to the lazy proof d_proof since CDProof has
  // (at most) one proof for each formula. Thus, we "claim" only the
  // formula that is proved by this fact. Otherwise, aliasing may occur,
  // which leads to cyclic or bogus proofs.
  ProofStep ps;
  ps.d_rule = id;
  ps.d_children = exp;
  ps.d_args = args;
  d_factPg.addStep(lit, ps);
  // add lazy step to proof
  d_proof.addLazyStep(lit, &d_factPg);
  // second, assert it to the equality engine
  Node reason = NodeManager::currentNM()->mkAnd(exp);
  return assertFactInternal(atom, polarity, reason);
}

bool ProofEqEngine::assertFact(Node lit,
                               PfRule id,
                               Node exp,
                               const std::vector<Node>& args)
{
  Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
                << ", args = " << args << std::endl;
  Node atom = lit.getKind() == NOT ? lit[0] : lit;
  bool polarity = lit.getKind() != NOT;
  // register the step in the proof
  if (holds(atom, polarity))
  {
    // we do not process this fact if it already holds
    return false;
  }
  // must extract the explanation as a vector
  std::vector<Node> expv;
  // Flatten (single occurrences) of AND. We do not allow nested AND, it is
  // the responsibilty of the caller to ensure these do not occur.
  if (exp != d_true)
  {
    if (exp.getKind() == AND)
    {
      for (const Node& expc : exp)
      {
        // should not have doubly nested AND
        Assert(expc.getKind() != AND);
        expv.push_back(expc);
      }
    }
    else
    {
      expv.push_back(exp);
    }
  }
  // buffer the step in the fact proof generator
  ProofStep ps;
  ps.d_rule = id;
  ps.d_children = expv;
  ps.d_args = args;
  d_factPg.addStep(lit, ps);
  // add lazy step to proof
  d_proof.addLazyStep(lit, &d_factPg);
  // second, assert it to the equality engine
  return assertFactInternal(atom, polarity, exp);
}

bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb)
{
  Trace("pfee") << "pfee::assertFact " << lit << ", exp = " << exp
                << " via buffer with " << psb.getNumSteps() << " steps"
                << std::endl;
  Node atom = lit.getKind() == NOT ? lit[0] : lit;
  bool polarity = lit.getKind() != NOT;
  if (holds(atom, polarity))
  {
    // we do not process this fact if it already holds
    return false;
  }
  // buffer the steps in the fact proof generator
  const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
  for (const std::pair<Node, ProofStep>& step : steps)
  {
    d_factPg.addStep(step.first, step.second);
  }
  // add lazy step to proof
  d_proof.addLazyStep(lit, &d_factPg);
  // second, assert it to the equality engine
  return assertFactInternal(atom, polarity, exp);
}

bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg)
{
  Trace("pfee") << "pfee::assertFact " << lit << ", exp = " << exp
                << " via generator" << std::endl;
  Node atom = lit.getKind() == NOT ? lit[0] : lit;
  bool polarity = lit.getKind() != NOT;
  if (holds(atom, polarity))
  {
    // we do not process this fact if it already holds
    return false;
  }
  // note the proof generator is responsible for remembering the explanation
  d_proof.addLazyStep(lit, pg);
  // second, assert it to the equality engine
  return assertFactInternal(atom, polarity, exp);
}

TrustNode ProofEqEngine::assertConflict(Node lit)
{
  Trace("pfee") << "pfee::assertConflict " << lit << std::endl;
  std::vector<TNode> assumps;
  explainWithProof(lit, assumps, &d_proof);
  // lit may not be equivalent to false, but should rewrite to false
  if (lit != d_false)
  {
    Assert(Rewriter::rewrite(lit) == d_false)
        << "pfee::assertConflict: conflict literal is not rewritable to "
           "false";
    std::vector<Node> exp;
    exp.push_back(lit);
    std::vector<Node> args;
    if (!d_proof.addStep(d_false, PfRule::MACRO_SR_PRED_ELIM, exp, args))
    {
      Assert(false) << "pfee::assertConflict: failed conflict step";
      return TrustNode::null();
    }
  }
  return ensureProofForFact(
      d_false, assumps, TrustNodeKind::CONFLICT, &d_proof);
}

TrustNode ProofEqEngine::assertConflict(PfRule id,
                                        const std::vector<Node>& exp,
                                        const std::vector<Node>& args)
{
  Trace("pfee") << "pfee::assertConflict " << id << ", exp = " << exp
                << ", args = " << args << std::endl;
  // conflict is same as lemma concluding false
  return assertLemma(d_false, id, exp, {}, args);
}

TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
                                        ProofGenerator* pg)
{
  Assert(pg != nullptr);
  Trace("pfee") << "pfee::assertConflict " << exp << " via generator"
                << std::endl;
  return assertLemma(d_false, exp, {}, pg);
}

TrustNode ProofEqEngine::assertLemma(Node conc,
                                     PfRule id,
                                     const std::vector<Node>& exp,
                                     const std::vector<Node>& noExplain,
                                     const std::vector<Node>& args)
{
  Trace("pfee") << "pfee::assertLemma " << conc << " " << id
                << ", exp = " << exp << ", noExplain = " << noExplain
                << ", args = " << args << std::endl;
  Assert(conc != d_true);
  LazyCDProof tmpProof(d_pnm, &d_proof);
  LazyCDProof* curr;
  TrustNodeKind tnk;
  // same policy as above: for conflicts, use existing lazy proof
  if (conc == d_false && noExplain.empty())
  {
    curr = &d_proof;
    tnk = TrustNodeKind::CONFLICT;
  }
  else
  {
    curr = &tmpProof;
    tnk = TrustNodeKind::LEMMA;
  }
  // explain each literal in the vector
  std::vector<TNode> assumps;
  explainVecWithProof(tnk, assumps, exp, noExplain, curr);
  // Register the proof step. We use a separate lazy CDProof which will make
  // calls to curr above for the proofs of the literals in exp.
  LazyCDProof outer(d_pnm, curr);
  if (!outer.addStep(conc, id, exp, args))
  {
    // a step went wrong, e.g. during checking
    Assert(false) << "pfee::assertConflict: register proof step";
    return TrustNode::null();
  }
  // Now get the proof for conc.
  return ensureProofForFact(conc, assumps, tnk, &outer);
}

TrustNode ProofEqEngine::assertLemma(Node conc,
                                     const std::vector<Node>& exp,
                                     const std::vector<Node>& noExplain,
                                     ProofGenerator* pg)
{
  Assert(pg != nullptr);
  Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
                << ", noExplain = " << noExplain << " via generator"
                << std::endl;
  LazyCDProof tmpProof(d_pnm, &d_proof);
  LazyCDProof* curr;
  TrustNodeKind tnk;
  // same policy as above: for conflicts, use existing lazy proof
  if (conc == d_false && noExplain.empty())
  {
    curr = &d_proof;
    tnk = TrustNodeKind::CONFLICT;
  }
  else
  {
    curr = &tmpProof;
    tnk = TrustNodeKind::LEMMA;
  }
  // explain each literal in the vector
  std::vector<TNode> assumps;
  explainVecWithProof(tnk, assumps, exp, noExplain, curr);
  // We use a lazy proof chain here. The provided proof generator sets up the
  // "skeleton" that is the base of the proof we are constructing. The call to
  // LazyCDProofChain::getProofFor will expand the leaves of this proof via
  // calls to curr.
  LazyCDProofChain outer(d_pnm, true, nullptr, curr, false);
  outer.addLazyStep(conc, pg);
  return ensureProofForFact(conc, assumps, tnk, &outer);
}

TrustNode ProofEqEngine::explain(Node conc)
{
  Trace("pfee") << "pfee::explain " << conc << std::endl;
  LazyCDProof tmpProof(d_pnm, &d_proof);
  std::vector<TNode> assumps;
  explainWithProof(conc, assumps, &tmpProof);
  return ensureProofForFact(conc, assumps, TrustNodeKind::PROP_EXP, &tmpProof);
}

void ProofEqEngine::explainVecWithProof(TrustNodeKind& tnk,
                                        std::vector<TNode>& assumps,
                                        const std::vector<Node>& exp,
                                        const std::vector<Node>& noExplain,
                                        LazyCDProof* curr)
{
  std::vector<Node> expn;
  for (const Node& e : exp)
  {
    if (std::find(noExplain.begin(), noExplain.end(), e) == noExplain.end())
    {
      explainWithProof(e, assumps, curr);
    }
    else
    {
      // it did not have a proof; it was an assumption of the previous rule
      assumps.push_back(e);
      // it is not a conflict, since it may involve new literals
      tnk = TrustNodeKind::LEMMA;
      // ensure this is an assumption
      curr->addLazyStep(e, &d_assumpPg);
    }
  }
}

TrustNode ProofEqEngine::ensureProofForFact(Node conc,
                                            const std::vector<TNode>& assumps,
                                            TrustNodeKind tnk,
                                            ProofGenerator* curr)
{
  Trace("pfee-proof") << std::endl;
  Trace("pfee-proof") << "pfee::ensureProofForFact: input " << conc << " via "
                      << assumps << ", TrustNodeKind=" << tnk << std::endl;
  NodeManager* nm = NodeManager::currentNM();
  // The proof
  std::shared_ptr<ProofNode> pf;
  ProofGenerator* pfg = nullptr;
  // the explanation is the conjunction of assumptions
  Node exp;
  // If proofs are enabled, generate the proof and possibly modify the
  // assumptions to match SCOPE.
  Assert(curr != nullptr);
  Trace("pfee-proof") << "pfee::ensureProofForFact: make proof for fact"
                      << std::endl;
  // get the proof for conc
  std::shared_ptr<ProofNode> pfBody = curr->getProofFor(conc);
  if (pfBody == nullptr)
  {
    Trace("pfee-proof")
        << "pfee::ensureProofForFact: failed to make proof for fact"
        << std::endl
        << std::endl;
    // should have existed
    Assert(false) << "pfee::assertConflict: failed to get proof for " << conc;
    return TrustNode::null();
  }
  // clone it so that we have a fresh copy
  pfBody = d_pnm->clone(pfBody);
  Trace("pfee-proof") << "pfee::ensureProofForFact: add scope" << std::endl;
  // The free assumptions must be closed by assumps, which should be passed
  // as arguments of SCOPE. However, some of the free assumptions may not
  // literally be equal to assumps, for instance, due to symmetry. In other
  // words, the SCOPE could be closing (= x y) in a proof with free
  // assumption (= y x). We modify the proof leaves to account for this
  // below.

  std::vector<Node> scopeAssumps;
  // we first ensure the assumptions are flattened
  for (const TNode& a : assumps)
  {
    if (a.getKind() == AND)
    {
      scopeAssumps.insert(scopeAssumps.end(), a.begin(), a.end());
    }
    else
    {
      scopeAssumps.push_back(a);
    }
  }
  // Scope the proof constructed above, and connect the formula with the proof
  // minimize the assumptions.
  pf = d_pnm->mkScope(pfBody, scopeAssumps, true, true);
  // If we have no assumptions, and are proving an explanation for propagation
  if (scopeAssumps.empty() && tnk == TrustNodeKind::PROP_EXP)
  {
    // Must add "true" as an explicit argument. This is to ensure that the
    // propagation F from true proves (=> true F) instead of F, since this is
    // the form required by TrustNodeKind::PROP_EXP. We do not ensure closed or
    // minimize here, since we already ensured the proof was closed above, and
    // we do not want to minimize, or else "true" would be omitted.
    scopeAssumps.push_back(nm->mkConst(true));
    pf = d_pnm->mkScope(pf, scopeAssumps, false);
  }
  exp = nm->mkAnd(scopeAssumps);
  // Make the lemma or conflict node. This must exactly match the conclusion
  // of SCOPE below.
  Node formula;
  if (tnk == TrustNodeKind::CONFLICT)
  {
    // conflict is negated
    Assert(conc == d_false);
    formula = exp;
  }
  else
  {
    formula =
        exp == d_true
            ? conc
            : (conc == d_false ? exp.negate() : nm->mkNode(IMPLIES, exp, conc));
  }
  Trace("pfee-proof") << "pfee::ensureProofForFact: formula is " << formula
                      << std::endl;
  // should always be non-null
  Assert(pf != nullptr);
  if (Trace.isOn("pfee-proof") || Trace.isOn("pfee-proof-final"))
  {
    Trace("pfee-proof") << "pfee::ensureProofForFact: printing proof"
                        << std::endl;
    std::stringstream ss;
    pf->printDebug(ss);
    Trace("pfee-proof") << "pfee::ensureProofForFact: Proof is " << ss.str()
                        << std::endl;
  }
  // Should be a closed proof now. If it is not, then the overall proof
  // is malformed.
  Assert(pf->isClosed());
  pfg = this;
  // set the proof for the conflict or lemma, which can be queried later
  switch (tnk)
  {
    case TrustNodeKind::CONFLICT: setProofForConflict(formula, pf); break;
    case TrustNodeKind::LEMMA: setProofForLemma(formula, pf); break;
    case TrustNodeKind::PROP_EXP: setProofForPropExp(conc, exp, pf); break;
    default:
      pfg = nullptr;
      Unhandled() << "Unhandled trust node kind " << tnk;
      break;
  }
  Trace("pfee-proof") << "pfee::ensureProofForFact: finish" << std::endl
                      << std::endl;
  // we can provide a proof for conflict, lemma or explained propagation
  switch (tnk)
  {
    case TrustNodeKind::CONFLICT:
      return TrustNode::mkTrustConflict(formula, pfg);
    case TrustNodeKind::LEMMA: return TrustNode::mkTrustLemma(formula, pfg);
    case TrustNodeKind::PROP_EXP:
      return TrustNode::mkTrustPropExp(conc, exp, pfg);
    default: Unhandled() << "Unhandled trust node kind " << tnk; break;
  }
  return TrustNode::null();
}

bool ProofEqEngine::assertFactInternal(TNode atom, bool polarity, TNode reason)
{
  Trace("pfee-debug") << "pfee::assertFactInternal: " << atom << " " << polarity
                      << " " << reason << std::endl;
  bool ret;
  if (atom.getKind() == EQUAL)
  {
    ret = d_ee.assertEquality(atom, polarity, reason);
  }
  else
  {
    ret = d_ee.assertPredicate(atom, polarity, reason);
  }
  if (ret)
  {
    // must reference count the new atom and explanation
    d_keep.insert(atom);
    d_keep.insert(reason);
  }
  return ret;
}

bool ProofEqEngine::holds(TNode atom, bool polarity)
{
  if (atom.getKind() == EQUAL)
  {
    if (!d_ee.hasTerm(atom[0]) || !d_ee.hasTerm(atom[1]))
    {
      return false;
    }
    return polarity ? d_ee.areEqual(atom[0], atom[1])
                    : d_ee.areDisequal(atom[0], atom[1], false);
  }
  if (!d_ee.hasTerm(atom))
  {
    return false;
  }
  TNode b = polarity ? d_true : d_false;
  return d_ee.areEqual(atom, b);
}

void ProofEqEngine::explainWithProof(Node lit,
                                     std::vector<TNode>& assumps,
                                     LazyCDProof* curr)
{
  if (std::find(assumps.begin(), assumps.end(), lit) != assumps.end())
  {
    return;
  }
  std::shared_ptr<eq::EqProof> pf = std::make_shared<eq::EqProof>();
  Trace("pfee-proof") << "pfee::explainWithProof: " << lit << std::endl;
  bool polarity = lit.getKind() != NOT;
  TNode atom = polarity ? lit : lit[0];
  Assert(atom.getKind() != AND);
  std::vector<TNode> tassumps;
  if (atom.getKind() == EQUAL)
  {
    if (atom[0] == atom[1])
    {
      return;
    }
    Assert(d_ee.hasTerm(atom[0]));
    Assert(d_ee.hasTerm(atom[1]));
    if (!polarity)
    {
      // ensure the explanation exists
      AlwaysAssert(d_ee.areDisequal(atom[0], atom[1], true));
    }
    d_ee.explainEquality(atom[0], atom[1], polarity, tassumps, pf.get());
  }
  else
  {
    Assert(d_ee.hasTerm(atom));
    d_ee.explainPredicate(atom, polarity, tassumps, pf.get());
  }
  Trace("pfee-proof") << "...got " << tassumps << std::endl;
  // avoid duplicates
  for (TNode a : tassumps)
  {
    if (a == lit)
    {
      assumps.push_back(a);
    }
    else if (std::find(assumps.begin(), assumps.end(), a) == assumps.end())
    {
      assumps.push_back(a);
    }
  }
  if (Trace.isOn("pfee-proof"))
  {
    Trace("pfee-proof") << "pfee::explainWithProof: add to proof ---"
                        << std::endl;
    std::stringstream sse;
    pf->debug_print(sse);
    Trace("pfee-proof") << sse.str() << std::endl;
    Trace("pfee-proof") << "---" << std::endl;
  }
  // add the steps in the equality engine proof to the Proof
  pf->addToProof(curr);
  Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl;
}

}  // namespace eq
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Gereon Kremer, Aina Niemetz
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		* Implementation of the proof-producing equality engine.
14		*/
15
16		#include "theory/uf/proof_equality_engine.h"
17
18		#include "proof/lazy_proof_chain.h"
19		#include "proof/proof_node.h"
20		#include "proof/proof_node_manager.h"
21		#include "theory/rewriter.h"
22		#include "theory/uf/eq_proof.h"
23		#include "theory/uf/equality_engine.h"
24		#include "theory/uf/proof_checker.h"
25
26		using namespace cvc5::kind;
27
28		namespace cvc5 {
29		namespace theory {
30		namespace eq {
31
32	13110	ProofEqEngine::ProofEqEngine(context::Context* c,
33		context::UserContext* u,
34		EqualityEngine& ee,
35	13110	ProofNodeManager* pnm)
36	26220	: EagerProofGenerator(pnm, u, "pfee::" + ee.identify()),
37		d_ee(ee),
38		d_factPg(c, pnm),
39		d_assumpPg(pnm),
40		d_pnm(pnm),
41	26220	d_proof(pnm, nullptr, c, "pfee::LazyCDProof::" + ee.identify()),
42	65550	d_keep(c)
43		{
44	13110	NodeManager* nm = NodeManager::currentNM();
45	13110	d_true = nm->mkConst(true);
46	13110	d_false = nm->mkConst(false);
47	13110	AlwaysAssert(pnm != nullptr)
48		<< "Should not construct ProofEqEngine without proof node manager";
49	13110	}
50
51		bool ProofEqEngine::assertFact(Node lit,
52		PfRule id,
53		const std::vector<Node>& exp,
54		const std::vector<Node>& args)
55		{
56		Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
57		<< ", args = " << args << std::endl;
58
59		Node atom = lit.getKind() == NOT ? lit[0] : lit;
60		bool polarity = lit.getKind() != NOT;
61		// register the step in the proof
62		if (holds(atom, polarity))
63		{
64		// we do not process this fact if it already holds
65		return false;
66		}
67		// Buffer the step in the fact proof generator. We do this instead of
68		// adding explict steps to the lazy proof d_proof since CDProof has
69		// (at most) one proof for each formula. Thus, we "claim" only the
70		// formula that is proved by this fact. Otherwise, aliasing may occur,
71		// which leads to cyclic or bogus proofs.
72		ProofStep ps;
73		ps.d_rule = id;
74		ps.d_children = exp;
75		ps.d_args = args;
76		d_factPg.addStep(lit, ps);
77		// add lazy step to proof
78		d_proof.addLazyStep(lit, &d_factPg);
79		// second, assert it to the equality engine
80		Node reason = NodeManager::currentNM()->mkAnd(exp);
81		return assertFactInternal(atom, polarity, reason);
82		}
83
84	1588	bool ProofEqEngine::assertFact(Node lit,
85		PfRule id,
86		Node exp,
87		const std::vector<Node>& args)
88		{
89	3176	Trace("pfee") << "pfee::assertFact " << lit << " " << id << ", exp = " << exp
90	1588	<< ", args = " << args << std::endl;
91	3176	Node atom = lit.getKind() == NOT ? lit[0] : lit;
92	1588	bool polarity = lit.getKind() != NOT;
93		// register the step in the proof
94	1588	if (holds(atom, polarity))
95		{
96		// we do not process this fact if it already holds
97	482	return false;
98		}
99		// must extract the explanation as a vector
100	2212	std::vector<Node> expv;
101		// Flatten (single occurrences) of AND. We do not allow nested AND, it is
102		// the responsibilty of the caller to ensure these do not occur.
103	1106	if (exp != d_true)
104		{
105	683	if (exp.getKind() == AND)
106		{
107	171	for (const Node& expc : exp)
108		{
109		// should not have doubly nested AND
110	114	Assert(expc.getKind() != AND);
111	114	expv.push_back(expc);
112		}
113		}
114		else
115		{
116	626	expv.push_back(exp);
117		}
118		}
119		// buffer the step in the fact proof generator
120	2212	ProofStep ps;
121	1106	ps.d_rule = id;
122	1106	ps.d_children = expv;
123	1106	ps.d_args = args;
124	1106	d_factPg.addStep(lit, ps);
125		// add lazy step to proof
126	1106	d_proof.addLazyStep(lit, &d_factPg);
127		// second, assert it to the equality engine
128	1106	return assertFactInternal(atom, polarity, exp);
129		}
130
131		bool ProofEqEngine::assertFact(Node lit, Node exp, ProofStepBuffer& psb)
132		{
133		Trace("pfee") << "pfee::assertFact " << lit << ", exp = " << exp
134		<< " via buffer with " << psb.getNumSteps() << " steps"
135		<< std::endl;
136		Node atom = lit.getKind() == NOT ? lit[0] : lit;
137		bool polarity = lit.getKind() != NOT;
138		if (holds(atom, polarity))
139		{
140		// we do not process this fact if it already holds
141		return false;
142		}
143		// buffer the steps in the fact proof generator
144		const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
145		for (const std::pair<Node, ProofStep>& step : steps)
146		{
147		d_factPg.addStep(step.first, step.second);
148		}
149		// add lazy step to proof
150		d_proof.addLazyStep(lit, &d_factPg);
151		// second, assert it to the equality engine
152		return assertFactInternal(atom, polarity, exp);
153		}
154
155	125790	bool ProofEqEngine::assertFact(Node lit, Node exp, ProofGenerator* pg)
156		{
157	251580	Trace("pfee") << "pfee::assertFact " << lit << ", exp = " << exp
158	125790	<< " via generator" << std::endl;
159	251580	Node atom = lit.getKind() == NOT ? lit[0] : lit;
160	125790	bool polarity = lit.getKind() != NOT;
161	125790	if (holds(atom, polarity))
162		{
163		// we do not process this fact if it already holds
164	38275	return false;
165		}
166		// note the proof generator is responsible for remembering the explanation
167	87515	d_proof.addLazyStep(lit, pg);
168		// second, assert it to the equality engine
169	87515	return assertFactInternal(atom, polarity, exp);
170		}
171
172	2589	TrustNode ProofEqEngine::assertConflict(Node lit)
173		{
174	2589	Trace("pfee") << "pfee::assertConflict " << lit << std::endl;
175	5178	std::vector<TNode> assumps;
176	2589	explainWithProof(lit, assumps, &d_proof);
177		// lit may not be equivalent to false, but should rewrite to false
178	2589	if (lit != d_false)
179		{
180	2589	Assert(Rewriter::rewrite(lit) == d_false)
181		<< "pfee::assertConflict: conflict literal is not rewritable to "
182		"false";
183	5178	std::vector<Node> exp;
184	2589	exp.push_back(lit);
185	5178	std::vector<Node> args;
186	2589	if (!d_proof.addStep(d_false, PfRule::MACRO_SR_PRED_ELIM, exp, args))
187		{
188		Assert(false) << "pfee::assertConflict: failed conflict step";
189		return TrustNode::null();
190		}
191		}
192		return ensureProofForFact(
193	2589	d_false, assumps, TrustNodeKind::CONFLICT, &d_proof);
194		}
195
196	2	TrustNode ProofEqEngine::assertConflict(PfRule id,
197		const std::vector<Node>& exp,
198		const std::vector<Node>& args)
199		{
200	4	Trace("pfee") << "pfee::assertConflict " << id << ", exp = " << exp
201	2	<< ", args = " << args << std::endl;
202		// conflict is same as lemma concluding false
203	2	return assertLemma(d_false, id, exp, {}, args);
204		}
205
206	449	TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
207		ProofGenerator* pg)
208		{
209	449	Assert(pg != nullptr);
210	898	Trace("pfee") << "pfee::assertConflict " << exp << " via generator"
211	449	<< std::endl;
212	449	return assertLemma(d_false, exp, {}, pg);
213		}
214
215	53	TrustNode ProofEqEngine::assertLemma(Node conc,
216		PfRule id,
217		const std::vector<Node>& exp,
218		const std::vector<Node>& noExplain,
219		const std::vector<Node>& args)
220		{
221	106	Trace("pfee") << "pfee::assertLemma " << conc << " " << id
222	53	<< ", exp = " << exp << ", noExplain = " << noExplain
223	53	<< ", args = " << args << std::endl;
224	53	Assert(conc != d_true);
225	106	LazyCDProof tmpProof(d_pnm, &d_proof);
226		LazyCDProof* curr;
227		TrustNodeKind tnk;
228		// same policy as above: for conflicts, use existing lazy proof
229	53	if (conc == d_false && noExplain.empty())
230		{
231	2	curr = &d_proof;
232	2	tnk = TrustNodeKind::CONFLICT;
233		}
234		else
235		{
236	51	curr = &tmpProof;
237	51	tnk = TrustNodeKind::LEMMA;
238		}
239		// explain each literal in the vector
240	106	std::vector<TNode> assumps;
241	53	explainVecWithProof(tnk, assumps, exp, noExplain, curr);
242		// Register the proof step. We use a separate lazy CDProof which will make
243		// calls to curr above for the proofs of the literals in exp.
244	106	LazyCDProof outer(d_pnm, curr);
245	53	if (!outer.addStep(conc, id, exp, args))
246		{
247		// a step went wrong, e.g. during checking
248		Assert(false) << "pfee::assertConflict: register proof step";
249		return TrustNode::null();
250		}
251		// Now get the proof for conc.
252	53	return ensureProofForFact(conc, assumps, tnk, &outer);
253		}
254
255	5382	TrustNode ProofEqEngine::assertLemma(Node conc,
256		const std::vector<Node>& exp,
257		const std::vector<Node>& noExplain,
258		ProofGenerator* pg)
259		{
260	5382	Assert(pg != nullptr);
261	10764	Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
262	5382	<< ", noExplain = " << noExplain << " via generator"
263	5382	<< std::endl;
264	10764	LazyCDProof tmpProof(d_pnm, &d_proof);
265		LazyCDProof* curr;
266		TrustNodeKind tnk;
267		// same policy as above: for conflicts, use existing lazy proof
268	5382	if (conc == d_false && noExplain.empty())
269		{
270	449	curr = &d_proof;
271	449	tnk = TrustNodeKind::CONFLICT;
272		}
273		else
274		{
275	4933	curr = &tmpProof;
276	4933	tnk = TrustNodeKind::LEMMA;
277		}
278		// explain each literal in the vector
279	10764	std::vector<TNode> assumps;
280	5382	explainVecWithProof(tnk, assumps, exp, noExplain, curr);
281		// We use a lazy proof chain here. The provided proof generator sets up the
282		// "skeleton" that is the base of the proof we are constructing. The call to
283		// LazyCDProofChain::getProofFor will expand the leaves of this proof via
284		// calls to curr.
285	10764	LazyCDProofChain outer(d_pnm, true, nullptr, curr, false);
286	5382	outer.addLazyStep(conc, pg);
287	10764	return ensureProofForFact(conc, assumps, tnk, &outer);
288		}
289
290	55556	TrustNode ProofEqEngine::explain(Node conc)
291		{
292	55556	Trace("pfee") << "pfee::explain " << conc << std::endl;
293	111112	LazyCDProof tmpProof(d_pnm, &d_proof);
294	111112	std::vector<TNode> assumps;
295	55556	explainWithProof(conc, assumps, &tmpProof);
296	111112	return ensureProofForFact(conc, assumps, TrustNodeKind::PROP_EXP, &tmpProof);
297		}
298
299	5435	void ProofEqEngine::explainVecWithProof(TrustNodeKind& tnk,
300		std::vector<TNode>& assumps,
301		const std::vector<Node>& exp,
302		const std::vector<Node>& noExplain,
303		LazyCDProof* curr)
304		{
305	10870	std::vector<Node> expn;
306	20511	for (const Node& e : exp)
307		{
308	15076	if (std::find(noExplain.begin(), noExplain.end(), e) == noExplain.end())
309		{
310	14223	explainWithProof(e, assumps, curr);
311		}
312		else
313		{
314		// it did not have a proof; it was an assumption of the previous rule
315	853	assumps.push_back(e);
316		// it is not a conflict, since it may involve new literals
317	853	tnk = TrustNodeKind::LEMMA;
318		// ensure this is an assumption
319	853	curr->addLazyStep(e, &d_assumpPg);
320		}
321		}
322	5435	}
323
324	63580	TrustNode ProofEqEngine::ensureProofForFact(Node conc,
325		const std::vector<TNode>& assumps,
326		TrustNodeKind tnk,
327		ProofGenerator* curr)
328		{
329	63580	Trace("pfee-proof") << std::endl;
330	127160	Trace("pfee-proof") << "pfee::ensureProofForFact: input " << conc << " via "
331	63580	<< assumps << ", TrustNodeKind=" << tnk << std::endl;
332	63580	NodeManager* nm = NodeManager::currentNM();
333		// The proof
334	127160	std::shared_ptr<ProofNode> pf;
335	63580	ProofGenerator* pfg = nullptr;
336		// the explanation is the conjunction of assumptions
337	127160	Node exp;
338		// If proofs are enabled, generate the proof and possibly modify the
339		// assumptions to match SCOPE.
340	63580	Assert(curr != nullptr);
341	127160	Trace("pfee-proof") << "pfee::ensureProofForFact: make proof for fact"
342	63580	<< std::endl;
343		// get the proof for conc
344	127160	std::shared_ptr<ProofNode> pfBody = curr->getProofFor(conc);
345	63580	if (pfBody == nullptr)
346		{
347		Trace("pfee-proof")
348		<< "pfee::ensureProofForFact: failed to make proof for fact"
349		<< std::endl
350		<< std::endl;
351		// should have existed
352		Assert(false) << "pfee::assertConflict: failed to get proof for " << conc;
353		return TrustNode::null();
354		}
355		// clone it so that we have a fresh copy
356	63580	pfBody = d_pnm->clone(pfBody);
357	63580	Trace("pfee-proof") << "pfee::ensureProofForFact: add scope" << std::endl;
358		// The free assumptions must be closed by assumps, which should be passed
359		// as arguments of SCOPE. However, some of the free assumptions may not
360		// literally be equal to assumps, for instance, due to symmetry. In other
361		// words, the SCOPE could be closing (= x y) in a proof with free
362		// assumption (= y x). We modify the proof leaves to account for this
363		// below.
364
365	127160	std::vector<Node> scopeAssumps;
366		// we first ensure the assumptions are flattened
367	357600	for (const TNode& a : assumps)
368		{
369	294020	if (a.getKind() == AND)
370		{
371	4880	scopeAssumps.insert(scopeAssumps.end(), a.begin(), a.end());
372		}
373		else
374		{
375	289140	scopeAssumps.push_back(a);
376		}
377		}
378		// Scope the proof constructed above, and connect the formula with the proof
379		// minimize the assumptions.
380	63580	pf = d_pnm->mkScope(pfBody, scopeAssumps, true, true);
381		// If we have no assumptions, and are proving an explanation for propagation
382	63580	if (scopeAssumps.empty() && tnk == TrustNodeKind::PROP_EXP)
383		{
384		// Must add "true" as an explicit argument. This is to ensure that the
385		// propagation F from true proves (=> true F) instead of F, since this is
386		// the form required by TrustNodeKind::PROP_EXP. We do not ensure closed or
387		// minimize here, since we already ensured the proof was closed above, and
388		// we do not want to minimize, or else "true" would be omitted.
389	1600	scopeAssumps.push_back(nm->mkConst(true));
390	1600	pf = d_pnm->mkScope(pf, scopeAssumps, false);
391		}
392	63580	exp = nm->mkAnd(scopeAssumps);
393		// Make the lemma or conflict node. This must exactly match the conclusion
394		// of SCOPE below.
395	127160	Node formula;
396	63580	if (tnk == TrustNodeKind::CONFLICT)
397		{
398		// conflict is negated
399	3040	Assert(conc == d_false);
400	3040	formula = exp;
401		}
402		else
403		{
404	60540	formula =
405	60540	exp == d_true
406	179124	? conc
407	58044	: (conc == d_false ? exp.negate() : nm->mkNode(IMPLIES, exp, conc));
408		}
409	127160	Trace("pfee-proof") << "pfee::ensureProofForFact: formula is " << formula
410	63580	<< std::endl;
411		// should always be non-null
412	63580	Assert(pf != nullptr);
413	63580	if (Trace.isOn("pfee-proof") \|\| Trace.isOn("pfee-proof-final"))
414		{
415		Trace("pfee-proof") << "pfee::ensureProofForFact: printing proof"
416		<< std::endl;
417		std::stringstream ss;
418		pf->printDebug(ss);
419		Trace("pfee-proof") << "pfee::ensureProofForFact: Proof is " << ss.str()
420		<< std::endl;
421		}
422		// Should be a closed proof now. If it is not, then the overall proof
423		// is malformed.
424	63580	Assert(pf->isClosed());
425	63580	pfg = this;
426		// set the proof for the conflict or lemma, which can be queried later
427	63580	switch (tnk)
428		{
429	3040	case TrustNodeKind::CONFLICT: setProofForConflict(formula, pf); break;
430	4984	case TrustNodeKind::LEMMA: setProofForLemma(formula, pf); break;
431	55556	case TrustNodeKind::PROP_EXP: setProofForPropExp(conc, exp, pf); break;
432		default:
433		pfg = nullptr;
434		Unhandled() << "Unhandled trust node kind " << tnk;
435		break;
436		}
437	127160	Trace("pfee-proof") << "pfee::ensureProofForFact: finish" << std::endl
438	63580	<< std::endl;
439		// we can provide a proof for conflict, lemma or explained propagation
440	63580	switch (tnk)
441		{
442	3040	case TrustNodeKind::CONFLICT:
443	3040	return TrustNode::mkTrustConflict(formula, pfg);
444	4984	case TrustNodeKind::LEMMA: return TrustNode::mkTrustLemma(formula, pfg);
445	55556	case TrustNodeKind::PROP_EXP:
446	55556	return TrustNode::mkTrustPropExp(conc, exp, pfg);
447		default: Unhandled() << "Unhandled trust node kind " << tnk; break;
448		}
449		return TrustNode::null();
450		}
451
452	88621	bool ProofEqEngine::assertFactInternal(TNode atom, bool polarity, TNode reason)
453		{
454	177242	Trace("pfee-debug") << "pfee::assertFactInternal: " << atom << " " << polarity
455	88621	<< " " << reason << std::endl;
456		bool ret;
457	88621	if (atom.getKind() == EQUAL)
458		{
459	85736	ret = d_ee.assertEquality(atom, polarity, reason);
460		}
461		else
462		{
463	2885	ret = d_ee.assertPredicate(atom, polarity, reason);
464		}
465	88621	if (ret)
466		{
467		// must reference count the new atom and explanation
468	88621	d_keep.insert(atom);
469	88621	d_keep.insert(reason);
470		}
471	88621	return ret;
472		}
473
474	127378	bool ProofEqEngine::holds(TNode atom, bool polarity)
475		{
476	127378	if (atom.getKind() == EQUAL)
477		{
478	124460	if (!d_ee.hasTerm(atom[0]) \|\| !d_ee.hasTerm(atom[1]))
479		{
480	37097	return false;
481		}
482	253880	return polarity ? d_ee.areEqual(atom[0], atom[1])
483	166517	: d_ee.areDisequal(atom[0], atom[1], false);
484		}
485	2918	if (!d_ee.hasTerm(atom))
486		{
487	1827	return false;
488		}
489	2182	TNode b = polarity ? d_true : d_false;
490	1091	return d_ee.areEqual(atom, b);
491		}
492
493	72368	void ProofEqEngine::explainWithProof(Node lit,
494		std::vector<TNode>& assumps,
495		LazyCDProof* curr)
496		{
497	72368	if (std::find(assumps.begin(), assumps.end(), lit) != assumps.end())
498		{
499	22	return;
500		}
501	144714	std::shared_ptr<eq::EqProof> pf = std::make_shared<eq::EqProof>();
502	72357	Trace("pfee-proof") << "pfee::explainWithProof: " << lit << std::endl;
503	72357	bool polarity = lit.getKind() != NOT;
504	144714	TNode atom = polarity ? lit : lit[0];
505	72357	Assert(atom.getKind() != AND);
506	144714	std::vector<TNode> tassumps;
507	72357	if (atom.getKind() == EQUAL)
508		{
509	69062	if (atom[0] == atom[1])
510		{
511		return;
512		}
513	69062	Assert(d_ee.hasTerm(atom[0]));
514	69062	Assert(d_ee.hasTerm(atom[1]));
515	69062	if (!polarity)
516		{
517		// ensure the explanation exists
518	3688	AlwaysAssert(d_ee.areDisequal(atom[0], atom[1], true));
519		}
520	69062	d_ee.explainEquality(atom[0], atom[1], polarity, tassumps, pf.get());
521		}
522		else
523		{
524	3295	Assert(d_ee.hasTerm(atom));
525	3295	d_ee.explainPredicate(atom, polarity, tassumps, pf.get());
526		}
527	72357	Trace("pfee-proof") << "...got " << tassumps << std::endl;
528		// avoid duplicates
529	459581	for (TNode a : tassumps)
530		{
531	387224	if (a == lit)
532		{
533	4338	assumps.push_back(a);
534		}
535	382886	else if (std::find(assumps.begin(), assumps.end(), a) == assumps.end())
536		{
537	288829	assumps.push_back(a);
538		}
539		}
540	72357	if (Trace.isOn("pfee-proof"))
541		{
542		Trace("pfee-proof") << "pfee::explainWithProof: add to proof ---"
543		<< std::endl;
544		std::stringstream sse;
545		pf->debug_print(sse);
546		Trace("pfee-proof") << sse.str() << std::endl;
547		Trace("pfee-proof") << "---" << std::endl;
548		}
549		// add the steps in the equality engine proof to the Proof
550	72357	pf->addToProof(curr);
551	72357	Trace("pfee-proof") << "pfee::explainWithProof: finished" << std::endl;
552		}
553
554		} // namespace eq
555		} // namespace theory
556	29577	} // namespace cvc5