Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/uf/proof_equality_engine.cpp	Lines:	207	264	78.4 %
Date:	2021-11-07	Branches:	482	1348	35.8 %


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