Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/conv_proof_generator.cpp	Lines:	266	315	84.4 %
Date:	2021-11-05	Branches:	561	1597	35.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, 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 term conversion proof generator utility.
 */

#include "proof/conv_proof_generator.h"

#include <sstream>

#include "expr/term_context.h"
#include "expr/term_context_stack.h"
#include "proof/proof_checker.h"
#include "proof/proof_node.h"
#include "proof/proof_node_algorithm.h"

using namespace cvc5::kind;

namespace cvc5 {

std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
{
  switch (tcpol)
  {
    case TConvPolicy::FIXPOINT: out << "FIXPOINT"; break;
    case TConvPolicy::ONCE: out << "ONCE"; break;
    default: out << "TConvPolicy:unknown"; break;
  }
  return out;
}

std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol)
{
  switch (tcpol)
  {
    case TConvCachePolicy::STATIC: out << "STATIC"; break;
    case TConvCachePolicy::DYNAMIC: out << "DYNAMIC"; break;
    case TConvCachePolicy::NEVER: out << "NEVER"; break;
    default: out << "TConvCachePolicy:unknown"; break;
  }
  return out;
}

TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
                                         context::Context* c,
                                         TConvPolicy pol,
                                         TConvCachePolicy cpol,
                                         std::string name,
                                         TermContext* tccb,
                                         bool rewriteOps)
    : d_proof(pnm, nullptr, c, name + "::LazyCDProof"),
      d_preRewriteMap(c ? c : &d_context),
      d_postRewriteMap(c ? c : &d_context),
      d_policy(pol),
      d_cpolicy(cpol),
      d_name(name),
      d_tcontext(tccb),
      d_rewriteOps(rewriteOps)
{
}

TConvProofGenerator::~TConvProofGenerator() {}

void TConvProofGenerator::addRewriteStep(Node t,
                                         Node s,
                                         ProofGenerator* pg,
                                         bool isPre,
                                         PfRule trustId,
                                         bool isClosed,
                                         uint32_t tctx)
{
  Node eq = registerRewriteStep(t, s, tctx, isPre);
  if (!eq.isNull())
  {
    d_proof.addLazyStep(eq, pg, trustId, isClosed);
  }
}

void TConvProofGenerator::addRewriteStep(
    Node t, Node s, ProofStep ps, bool isPre, uint32_t tctx)
{
  Node eq = registerRewriteStep(t, s, tctx, isPre);
  if (!eq.isNull())
  {
    d_proof.addStep(eq, ps);
  }
}

void TConvProofGenerator::addRewriteStep(Node t,
                                         Node s,
                                         PfRule id,
                                         const std::vector<Node>& children,
                                         const std::vector<Node>& args,
                                         bool isPre,
                                         uint32_t tctx)
{
  Node eq = registerRewriteStep(t, s, tctx, isPre);
  if (!eq.isNull())
  {
    d_proof.addStep(eq, id, children, args);
  }
}

bool TConvProofGenerator::hasRewriteStep(Node t,
                                         uint32_t tctx,
                                         bool isPre) const
{
  return !getRewriteStep(t, tctx, isPre).isNull();
}

Node TConvProofGenerator::getRewriteStep(Node t,
                                         uint32_t tctx,
                                         bool isPre) const
{
  Node thash = t;
  if (d_tcontext != nullptr)
  {
    thash = TCtxNode::computeNodeHash(t, tctx);
  }
  return getRewriteStepInternal(thash, isPre);
}

Node TConvProofGenerator::registerRewriteStep(Node t,
                                              Node s,
                                              uint32_t tctx,
                                              bool isPre)
{
  Assert(!t.isNull());
  Assert(!s.isNull());

  if (t == s)
  {
    return Node::null();
  }
  Node thash = t;
  if (d_tcontext != nullptr)
  {
    thash = TCtxNode::computeNodeHash(t, tctx);
  }
  else
  {
    // don't use term context ids if not using term context
    Assert(tctx == 0);
  }
  // should not rewrite term to two different things
  if (!getRewriteStepInternal(thash, isPre).isNull())
  {
    Assert(getRewriteStepInternal(thash, isPre) == s)
        << identify() << " rewriting " << t << " to both " << s << " and "
        << getRewriteStepInternal(thash, isPre);
    return Node::null();
  }
  NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
  rm[thash] = s;
  if (d_cpolicy == TConvCachePolicy::DYNAMIC)
  {
    // clear the cache
    d_cache.clear();
  }
  return t.eqNode(s);
}

std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
{
  Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << identify()
                        << ": " << f << std::endl;
  if (f.getKind() != EQUAL)
  {
    std::stringstream serr;
    serr << "TConvProofGenerator::getProofFor: " << identify()
         << ": fail, non-equality " << f;
    Unhandled() << serr.str();
    Trace("tconv-pf-gen") << serr.str() << std::endl;
    return nullptr;
  }
  // we use the existing proofs
  LazyCDProof lpf(
      d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof");
  if (f[0] == f[1])
  {
    // assertion failure in debug
    Assert(false) << "TConvProofGenerator::getProofFor: " << identify()
                  << ": don't ask for trivial proofs";
    lpf.addStep(f, PfRule::REFL, {}, {f[0]});
  }
  else
  {
    Node conc = getProofForRewriting(f[0], lpf, d_tcontext);
    if (conc != f)
    {
      bool debugTraceEnabled = Trace.isOn("tconv-pf-gen-debug");
      Assert(conc.getKind() == EQUAL && conc[0] == f[0]);
      std::stringstream serr;
      serr << "TConvProofGenerator::getProofFor: " << toStringDebug()
           << ": failed, mismatch";
      if (!debugTraceEnabled)
      {
        serr << " (see -t tconv-pf-gen-debug for details)";
      }
      serr << std::endl;
      serr << "                   source: " << f[0] << std::endl;
      serr << "     requested conclusion: " << f[1] << std::endl;
      serr << "conclusion from generator: " << conc[1] << std::endl;

      if (debugTraceEnabled)
      {
        Trace("tconv-pf-gen-debug") << "Rewrite steps:" << std::endl;
        for (size_t r = 0; r < 2; r++)
        {
          const NodeNodeMap& rm = r == 0 ? d_preRewriteMap : d_postRewriteMap;
          serr << "Rewrite steps (" << (r == 0 ? "pre" : "post")
               << "):" << std::endl;
          for (NodeNodeMap::const_iterator it = rm.begin(); it != rm.end();
               ++it)
          {
            serr << (*it).first << " -> " << (*it).second << std::endl;
          }
        }
      }
      Unhandled() << serr.str();
      return nullptr;
    }
  }
  std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f);
  Trace("tconv-pf-gen") << "... success" << std::endl;
  Assert(pfn != nullptr);
  Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
  return pfn;
}

std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
{
  LazyCDProof lpf(
      d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProofRew");
  Node conc = getProofForRewriting(n, lpf, d_tcontext);
  if (conc[1] == n)
  {
    // assertion failure in debug
    Assert(false) << "TConvProofGenerator::getProofForRewriting: " << identify()
                  << ": don't ask for trivial proofs";
    lpf.addStep(conc, PfRule::REFL, {}, {n});
  }
  std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc);
  Assert(pfn != nullptr);
  Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
  return pfn;
}

Node TConvProofGenerator::getProofForRewriting(Node t,
                                               LazyCDProof& pf,
                                               TermContext* tctx)
{
  NodeManager* nm = NodeManager::currentNM();
  // Invariant: if visited[hash(t)] = s or rewritten[hash(t)] = s and t,s are
  // distinct, then pf is able to generate a proof of t=s. We must
  // Node in the domains of the maps below due to hashing creating new (SEXPR)
  // nodes.

  // the final rewritten form of terms
  std::unordered_map<Node, Node> visited;
  // the rewritten form of terms we have processed so far
  std::unordered_map<Node, Node> rewritten;
  std::unordered_map<Node, Node>::iterator it;
  std::unordered_map<Node, Node>::iterator itr;
  std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
  Trace("tconv-pf-gen-rewrite")
      << "TConvProofGenerator::getProofForRewriting: " << toStringDebug()
      << std::endl;
  Trace("tconv-pf-gen-rewrite") << "Input: " << t << std::endl;
  // if provided, we use term context for cache
  std::shared_ptr<TCtxStack> visitctx;
  // otherwise, visit is used if we don't have a term context
  std::vector<TNode> visit;
  Node tinitialHash;
  if (tctx != nullptr)
  {
    visitctx = std::make_shared<TCtxStack>(tctx);
    visitctx->pushInitial(t);
    tinitialHash = TCtxNode::computeNodeHash(t, tctx->initialValue());
  }
  else
  {
    visit.push_back(t);
    tinitialHash = t;
  }
  Node cur;
  uint32_t curCVal = 0;
  Node curHash;
  do
  {
    // pop the top element
    if (tctx != nullptr)
    {
      std::pair<Node, uint32_t> curPair = visitctx->getCurrent();
      cur = curPair.first;
      curCVal = curPair.second;
      curHash = TCtxNode::computeNodeHash(cur, curCVal);
      visitctx->pop();
    }
    else
    {
      cur = visit.back();
      curHash = cur;
      visit.pop_back();
    }
    Trace("tconv-pf-gen-rewrite") << "* visit : " << curHash << std::endl;
    // has the proof for cur been cached?
    itc = d_cache.find(curHash);
    if (itc != d_cache.end())
    {
      Node res = itc->second->getResult();
      Assert(res.getKind() == EQUAL);
      Assert(!res[1].isNull());
      visited[curHash] = res[1];
      pf.addProof(itc->second);
      continue;
    }
    it = visited.find(curHash);
    if (it == visited.end())
    {
      Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl;
      visited[curHash] = Node::null();
      // did we rewrite the current node (at pre-rewrite)?
      Node rcur = getRewriteStepInternal(curHash, true);
      if (!rcur.isNull())
      {
        Trace("tconv-pf-gen-rewrite")
            << "*** " << curHash << " prerewrites to " << rcur << std::endl;
        // d_proof has a proof of cur = rcur. Hence there is nothing
        // to do here, as pf will reference d_proof to get its proof.
        if (d_policy == TConvPolicy::FIXPOINT)
        {
          // It may be the case that rcur also rewrites, thus we cannot assign
          // the final rewritten form for cur yet. Instead we revisit cur after
          // finishing visiting rcur.
          rewritten[curHash] = rcur;
          if (tctx != nullptr)
          {
            visitctx->push(cur, curCVal);
            visitctx->push(rcur, curCVal);
          }
          else
          {
            visit.push_back(cur);
            visit.push_back(rcur);
          }
        }
        else
        {
          Assert(d_policy == TConvPolicy::ONCE);
          Trace("tconv-pf-gen-rewrite") << "-> (once, prewrite) " << curHash
                                        << " = " << rcur << std::endl;
          // not rewriting again, rcur is final
          Assert(!rcur.isNull());
          visited[curHash] = rcur;
          doCache(curHash, cur, rcur, pf);
        }
      }
      else if (tctx != nullptr)
      {
        visitctx->push(cur, curCVal);
        // visit operator if apply uf
        if (d_rewriteOps && cur.getKind() == APPLY_UF)
        {
          visitctx->pushOp(cur, curCVal);
        }
        visitctx->pushChildren(cur, curCVal);
      }
      else
      {
        visit.push_back(cur);
        // visit operator if apply uf
        if (d_rewriteOps && cur.getKind() == APPLY_UF)
        {
          visit.push_back(cur.getOperator());
        }
        visit.insert(visit.end(), cur.begin(), cur.end());
      }
    }
    else if (it->second.isNull())
    {
      itr = rewritten.find(curHash);
      if (itr != rewritten.end())
      {
        // only can generate partially rewritten nodes when rewrite again is
        // true.
        Assert(d_policy != TConvPolicy::ONCE);
        // if it was rewritten, check the status of the rewritten node,
        // which should be finished now
        Node rcur = itr->second;
        Trace("tconv-pf-gen-rewrite")
            << "- postvisit, previously rewritten to " << rcur << std::endl;
        Node rcurHash = rcur;
        if (tctx != nullptr)
        {
          rcurHash = TCtxNode::computeNodeHash(rcur, curCVal);
        }
        Assert(cur != rcur);
        // the final rewritten form of cur is the final form of rcur
        Node rcurFinal = visited[rcurHash];
        Assert(!rcurFinal.isNull());
        if (rcurFinal != rcur)
        {
          // must connect via TRANS
          std::vector<Node> pfChildren;
          pfChildren.push_back(cur.eqNode(rcur));
          pfChildren.push_back(rcur.eqNode(rcurFinal));
          Node result = cur.eqNode(rcurFinal);
          pf.addStep(result, PfRule::TRANS, pfChildren, {});
        }
        Trace("tconv-pf-gen-rewrite")
            << "-> (rewritten postrewrite) " << curHash << " = " << rcurFinal
            << std::endl;
        visited[curHash] = rcurFinal;
        doCache(curHash, cur, rcurFinal, pf);
      }
      else
      {
        Trace("tconv-pf-gen-rewrite") << "- postvisit" << std::endl;
        Node ret = cur;
        Node retHash = curHash;
        bool childChanged = false;
        std::vector<Node> children;
        Kind ck = cur.getKind();
        if (d_rewriteOps && ck == APPLY_UF)
        {
          // the operator of APPLY_UF is visited
          Node cop = cur.getOperator();
          if (tctx != nullptr)
          {
            uint32_t coval = tctx->computeValueOp(cur, curCVal);
            Node coHash = TCtxNode::computeNodeHash(cop, coval);
            it = visited.find(coHash);
          }
          else
          {
            it = visited.find(cop);
          }
          Assert(it != visited.end());
          Assert(!it->second.isNull());
          childChanged = childChanged || cop != it->second;
          children.push_back(it->second);
        }
        else if (cur.getMetaKind() == metakind::PARAMETERIZED)
        {
          // all other parametrized operators are unchanged
          children.push_back(cur.getOperator());
        }
        // get the results of the children
        if (tctx != nullptr)
        {
          for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
          {
            Node cn = cur[i];
            uint32_t cnval = tctx->computeValue(cur, curCVal, i);
            Node cnHash = TCtxNode::computeNodeHash(cn, cnval);
            it = visited.find(cnHash);
            Assert(it != visited.end());
            Assert(!it->second.isNull());
            childChanged = childChanged || cn != it->second;
            children.push_back(it->second);
          }
        }
        else
        {
          // can use simple loop if not term-context-sensitive
          for (const Node& cn : cur)
          {
            it = visited.find(cn);
            Assert(it != visited.end());
            Assert(!it->second.isNull());
            childChanged = childChanged || cn != it->second;
            children.push_back(it->second);
          }
        }
        if (childChanged)
        {
          ret = nm->mkNode(ck, children);
          rewritten[curHash] = ret;
          // congruence to show (cur = ret)
          PfRule congRule = PfRule::CONG;
          std::vector<Node> pfChildren;
          std::vector<Node> pfArgs;
          pfArgs.push_back(ProofRuleChecker::mkKindNode(ck));
          if (ck == APPLY_UF && children[0] != cur.getOperator())
          {
            // use HO_CONG if the operator changed
            congRule = PfRule::HO_CONG;
            pfChildren.push_back(cur.getOperator().eqNode(children[0]));
          }
          else if (kind::metaKindOf(ck) == kind::metakind::PARAMETERIZED)
          {
            pfArgs.push_back(cur.getOperator());
          }
          for (size_t i = 0, size = cur.getNumChildren(); i < size; i++)
          {
            if (cur[i] == ret[i])
            {
              // ensure REFL proof for unchanged children
              pf.addStep(cur[i].eqNode(cur[i]), PfRule::REFL, {}, {cur[i]});
            }
            pfChildren.push_back(cur[i].eqNode(ret[i]));
          }
          Node result = cur.eqNode(ret);
          pf.addStep(result, congRule, pfChildren, pfArgs);
          // must update the hash
          retHash = ret;
          if (tctx != nullptr)
          {
            retHash = TCtxNode::computeNodeHash(ret, curCVal);
          }
        }
        else if (tctx != nullptr)
        {
          // now we need the hash
          retHash = TCtxNode::computeNodeHash(cur, curCVal);
        }
        // did we rewrite ret (at post-rewrite)?
        Node rret = getRewriteStepInternal(retHash, false);
        if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT)
        {
          Trace("tconv-pf-gen-rewrite")
              << "*** " << retHash << " postrewrites to " << rret << std::endl;
          // d_proof should have a proof of ret = rret, hence nothing to do
          // here, for the same reasons as above. It also may be the case that
          // rret rewrites, hence we must revisit ret.
          rewritten[retHash] = rret;
          if (tctx != nullptr)
          {
            if (cur != ret)
            {
              visitctx->push(cur, curCVal);
            }
            visitctx->push(ret, curCVal);
            visitctx->push(rret, curCVal);
          }
          else
          {
            if (cur != ret)
            {
              visit.push_back(cur);
            }
            visit.push_back(ret);
            visit.push_back(rret);
          }
        }
        else
        {
          // If we changed due to congruence, and then rewrote, then we
          // require a trans step to connect here
          if (!rret.isNull() && childChanged)
          {
            std::vector<Node> pfChildren;
            pfChildren.push_back(cur.eqNode(ret));
            pfChildren.push_back(ret.eqNode(rret));
            Node result = cur.eqNode(rret);
            pf.addStep(result, PfRule::TRANS, pfChildren, {});
          }
          // take its rewrite if it rewrote and we have ONCE rewriting policy
          ret = rret.isNull() ? ret : rret;
          Trace("tconv-pf-gen-rewrite")
              << "-> (postrewrite) " << curHash << " = " << ret << std::endl;
          // it is final
          Assert(!ret.isNull());
          visited[curHash] = ret;
          doCache(curHash, cur, ret, pf);
        }
      }
    }
    else
    {
      Trace("tconv-pf-gen-rewrite") << "- already visited" << std::endl;
    }
  } while (!(tctx != nullptr ? visitctx->empty() : visit.empty()));
  Assert(visited.find(tinitialHash) != visited.end());
  Assert(!visited.find(tinitialHash)->second.isNull());
  Trace("tconv-pf-gen-rewrite")
      << "...finished, return " << visited[tinitialHash] << std::endl;
  // return the conclusion of the overall proof
  return t.eqNode(visited[tinitialHash]);
}

void TConvProofGenerator::doCache(Node curHash,
                                  Node cur,
                                  Node r,
                                  LazyCDProof& pf)
{
  if (d_cpolicy != TConvCachePolicy::NEVER)
  {
    Node eq = cur.eqNode(r);
    d_cache[curHash] = pf.getProofFor(eq);
  }
}

Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const
{
  const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
  NodeNodeMap::const_iterator it = rm.find(t);
  if (it == rm.end())
  {
    return Node::null();
  }
  return (*it).second;
}
std::string TConvProofGenerator::identify() const { return d_name; }

std::string TConvProofGenerator::toStringDebug() const
{
  std::stringstream ss;
  ss << identify() << " (policy=" << d_policy << ", cache policy=" << d_cpolicy
     << (d_tcontext != nullptr ? ", term-context-sensitive" : "") << ")";
  return ss.str();
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, 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 term conversion proof generator utility.
14		*/
15
16		#include "proof/conv_proof_generator.h"
17
18		#include <sstream>
19
20		#include "expr/term_context.h"
21		#include "expr/term_context_stack.h"
22		#include "proof/proof_checker.h"
23		#include "proof/proof_node.h"
24		#include "proof/proof_node_algorithm.h"
25
26		using namespace cvc5::kind;
27
28		namespace cvc5 {
29
30	108309	std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
31		{
32	108309	switch (tcpol)
33		{
34	97125	case TConvPolicy::FIXPOINT: out << "FIXPOINT"; break;
35	11184	case TConvPolicy::ONCE: out << "ONCE"; break;
36		default: out << "TConvPolicy:unknown"; break;
37		}
38	108309	return out;
39		}
40
41	108309	std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol)
42		{
43	108309	switch (tcpol)
44		{
45	68985	case TConvCachePolicy::STATIC: out << "STATIC"; break;
46		case TConvCachePolicy::DYNAMIC: out << "DYNAMIC"; break;
47	39324	case TConvCachePolicy::NEVER: out << "NEVER"; break;
48		default: out << "TConvCachePolicy:unknown"; break;
49		}
50	108309	return out;
51		}
52
53	72266	TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
54		context::Context* c,
55		TConvPolicy pol,
56		TConvCachePolicy cpol,
57		std::string name,
58		TermContext* tccb,
59	72266	bool rewriteOps)
60	144532	: d_proof(pnm, nullptr, c, name + "::LazyCDProof"),
61		d_preRewriteMap(c ? c : &d_context),
62		d_postRewriteMap(c ? c : &d_context),
63		d_policy(pol),
64		d_cpolicy(cpol),
65		d_name(name),
66		d_tcontext(tccb),
67	216798	d_rewriteOps(rewriteOps)
68		{
69	72266	}
70
71	127197	TConvProofGenerator::~TConvProofGenerator() {}
72
73	594949	void TConvProofGenerator::addRewriteStep(Node t,
74		Node s,
75		ProofGenerator* pg,
76		bool isPre,
77		PfRule trustId,
78		bool isClosed,
79		uint32_t tctx)
80		{
81	1189898	Node eq = registerRewriteStep(t, s, tctx, isPre);
82	594949	if (!eq.isNull())
83		{
84	594845	d_proof.addLazyStep(eq, pg, trustId, isClosed);
85		}
86	594949	}
87
88		void TConvProofGenerator::addRewriteStep(
89		Node t, Node s, ProofStep ps, bool isPre, uint32_t tctx)
90		{
91		Node eq = registerRewriteStep(t, s, tctx, isPre);
92		if (!eq.isNull())
93		{
94		d_proof.addStep(eq, ps);
95		}
96		}
97
98	368732	void TConvProofGenerator::addRewriteStep(Node t,
99		Node s,
100		PfRule id,
101		const std::vector<Node>& children,
102		const std::vector<Node>& args,
103		bool isPre,
104		uint32_t tctx)
105		{
106	737464	Node eq = registerRewriteStep(t, s, tctx, isPre);
107	368732	if (!eq.isNull())
108		{
109	267113	d_proof.addStep(eq, id, children, args);
110		}
111	368732	}
112
113		bool TConvProofGenerator::hasRewriteStep(Node t,
114		uint32_t tctx,
115		bool isPre) const
116		{
117		return !getRewriteStep(t, tctx, isPre).isNull();
118		}
119
120		Node TConvProofGenerator::getRewriteStep(Node t,
121		uint32_t tctx,
122		bool isPre) const
123		{
124		Node thash = t;
125		if (d_tcontext != nullptr)
126		{
127		thash = TCtxNode::computeNodeHash(t, tctx);
128		}
129		return getRewriteStepInternal(thash, isPre);
130		}
131
132	963681	Node TConvProofGenerator::registerRewriteStep(Node t,
133		Node s,
134		uint32_t tctx,
135		bool isPre)
136		{
137	963681	Assert(!t.isNull());
138	963681	Assert(!s.isNull());
139
140	963681	if (t == s)
141		{
142	1	return Node::null();
143		}
144	1927360	Node thash = t;
145	963680	if (d_tcontext != nullptr)
146		{
147	81642	thash = TCtxNode::computeNodeHash(t, tctx);
148		}
149		else
150		{
151		// don't use term context ids if not using term context
152	882038	Assert(tctx == 0);
153		}
154		// should not rewrite term to two different things
155	963680	if (!getRewriteStepInternal(thash, isPre).isNull())
156		{
157	203444	Assert(getRewriteStepInternal(thash, isPre) == s)
158	101722	<< identify() << " rewriting " << t << " to both " << s << " and "
159	101722	<< getRewriteStepInternal(thash, isPre);
160	101722	return Node::null();
161		}
162	861958	NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
163	861958	rm[thash] = s;
164	861958	if (d_cpolicy == TConvCachePolicy::DYNAMIC)
165		{
166		// clear the cache
167		d_cache.clear();
168		}
169	861958	return t.eqNode(s);
170		}
171
172	99220	std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
173		{
174	198440	Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << identify()
175	99220	<< ": " << f << std::endl;
176	99220	if (f.getKind() != EQUAL)
177		{
178		std::stringstream serr;
179		serr << "TConvProofGenerator::getProofFor: " << identify()
180		<< ": fail, non-equality " << f;
181		Unhandled() << serr.str();
182		Trace("tconv-pf-gen") << serr.str() << std::endl;
183		return nullptr;
184		}
185		// we use the existing proofs
186		LazyCDProof lpf(
187	198440	d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof");
188	99220	if (f[0] == f[1])
189		{
190		// assertion failure in debug
191		Assert(false) << "TConvProofGenerator::getProofFor: " << identify()
192		<< ": don't ask for trivial proofs";
193		lpf.addStep(f, PfRule::REFL, {}, {f[0]});
194		}
195		else
196		{
197	198440	Node conc = getProofForRewriting(f[0], lpf, d_tcontext);
198	99220	if (conc != f)
199		{
200		bool debugTraceEnabled = Trace.isOn("tconv-pf-gen-debug");
201		Assert(conc.getKind() == EQUAL && conc[0] == f[0]);
202		std::stringstream serr;
203		serr << "TConvProofGenerator::getProofFor: " << toStringDebug()
204		<< ": failed, mismatch";
205		if (!debugTraceEnabled)
206		{
207		serr << " (see -t tconv-pf-gen-debug for details)";
208		}
209		serr << std::endl;
210		serr << " source: " << f[0] << std::endl;
211		serr << " requested conclusion: " << f[1] << std::endl;
212		serr << "conclusion from generator: " << conc[1] << std::endl;
213
214		if (debugTraceEnabled)
215		{
216		Trace("tconv-pf-gen-debug") << "Rewrite steps:" << std::endl;
217		for (size_t r = 0; r < 2; r++)
218		{
219		const NodeNodeMap& rm = r == 0 ? d_preRewriteMap : d_postRewriteMap;
220		serr << "Rewrite steps (" << (r == 0 ? "pre" : "post")
221		<< "):" << std::endl;
222		for (NodeNodeMap::const_iterator it = rm.begin(); it != rm.end();
223		++it)
224		{
225		serr << (it).first << " -> " << (it).second << std::endl;
226		}
227		}
228		}
229		Unhandled() << serr.str();
230		return nullptr;
231		}
232		}
233	198440	std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f);
234	99220	Trace("tconv-pf-gen") << "... success" << std::endl;
235	99220	Assert(pfn != nullptr);
236	99220	Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
237	99220	return pfn;
238		}
239
240	9089	std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
241		{
242		LazyCDProof lpf(
243	18178	d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProofRew");
244	18178	Node conc = getProofForRewriting(n, lpf, d_tcontext);
245	9089	if (conc[1] == n)
246		{
247		// assertion failure in debug
248		Assert(false) << "TConvProofGenerator::getProofForRewriting: " << identify()
249		<< ": don't ask for trivial proofs";
250		lpf.addStep(conc, PfRule::REFL, {}, {n});
251		}
252	9089	std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc);
253	9089	Assert(pfn != nullptr);
254	9089	Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
255	18178	return pfn;
256		}
257
258	108309	Node TConvProofGenerator::getProofForRewriting(Node t,
259		LazyCDProof& pf,
260		TermContext* tctx)
261		{
262	108309	NodeManager* nm = NodeManager::currentNM();
263		// Invariant: if visited[hash(t)] = s or rewritten[hash(t)] = s and t,s are
264		// distinct, then pf is able to generate a proof of t=s. We must
265		// Node in the domains of the maps below due to hashing creating new (SEXPR)
266		// nodes.
267
268		// the final rewritten form of terms
269	216618	std::unordered_map<Node, Node> visited;
270		// the rewritten form of terms we have processed so far
271	216618	std::unordered_map<Node, Node> rewritten;
272	108309	std::unordered_map<Node, Node>::iterator it;
273	108309	std::unordered_map<Node, Node>::iterator itr;
274	108309	std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
275	216618	Trace("tconv-pf-gen-rewrite")
276	216618	<< "TConvProofGenerator::getProofForRewriting: " << toStringDebug()
277	108309	<< std::endl;
278	108309	Trace("tconv-pf-gen-rewrite") << "Input: " << t << std::endl;
279		// if provided, we use term context for cache
280	216618	std::shared_ptr<TCtxStack> visitctx;
281		// otherwise, visit is used if we don't have a term context
282	216618	std::vector<TNode> visit;
283	216618	Node tinitialHash;
284	108309	if (tctx != nullptr)
285		{
286	19386	visitctx = std::make_shared<TCtxStack>(tctx);
287	19386	visitctx->pushInitial(t);
288	19386	tinitialHash = TCtxNode::computeNodeHash(t, tctx->initialValue());
289		}
290		else
291		{
292	88923	visit.push_back(t);
293	88923	tinitialHash = t;
294		}
295	216618	Node cur;
296	108309	uint32_t curCVal = 0;
297	216618	Node curHash;
298	4983368	do
299		{
300		// pop the top element
301	5091677	if (tctx != nullptr)
302		{
303	1499078	std::pair<Node, uint32_t> curPair = visitctx->getCurrent();
304	749539	cur = curPair.first;
305	749539	curCVal = curPair.second;
306	749539	curHash = TCtxNode::computeNodeHash(cur, curCVal);
307	749539	visitctx->pop();
308		}
309		else
310		{
311	4342138	cur = visit.back();
312	4342138	curHash = cur;
313	4342138	visit.pop_back();
314		}
315	5091677	Trace("tconv-pf-gen-rewrite") << "* visit : " << curHash << std::endl;
316		// has the proof for cur been cached?
317	5091677	itc = d_cache.find(curHash);
318	5091677	if (itc != d_cache.end())
319		{
320	1927794	Node res = itc->second->getResult();
321	963897	Assert(res.getKind() == EQUAL);
322	963897	Assert(!res[1].isNull());
323	963897	visited[curHash] = res[1];
324	963897	pf.addProof(itc->second);
325	963897	continue;
326		}
327	4127780	it = visited.find(curHash);
328	4127780	if (it == visited.end())
329		{
330	1686766	Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl;
331	1686766	visited[curHash] = Node::null();
332		// did we rewrite the current node (at pre-rewrite)?
333	3373532	Node rcur = getRewriteStepInternal(curHash, true);
334	1686766	if (!rcur.isNull())
335		{
336	363972	Trace("tconv-pf-gen-rewrite")
337	181986	<< "*** " << curHash << " prerewrites to " << rcur << std::endl;
338		// d_proof has a proof of cur = rcur. Hence there is nothing
339		// to do here, as pf will reference d_proof to get its proof.
340	181986	if (d_policy == TConvPolicy::FIXPOINT)
341		{
342		// It may be the case that rcur also rewrites, thus we cannot assign
343		// the final rewritten form for cur yet. Instead we revisit cur after
344		// finishing visiting rcur.
345	171472	rewritten[curHash] = rcur;
346	171472	if (tctx != nullptr)
347		{
348	49467	visitctx->push(cur, curCVal);
349	49467	visitctx->push(rcur, curCVal);
350		}
351		else
352		{
353	122005	visit.push_back(cur);
354	122005	visit.push_back(rcur);
355		}
356		}
357		else
358		{
359	10514	Assert(d_policy == TConvPolicy::ONCE);
360	21028	Trace("tconv-pf-gen-rewrite") << "-> (once, prewrite) " << curHash
361	10514	<< " = " << rcur << std::endl;
362		// not rewriting again, rcur is final
363	10514	Assert(!rcur.isNull());
364	10514	visited[curHash] = rcur;
365	10514	doCache(curHash, cur, rcur, pf);
366		}
367		}
368	1504780	else if (tctx != nullptr)
369		{
370	268685	visitctx->push(cur, curCVal);
371		// visit operator if apply uf
372	268685	if (d_rewriteOps && cur.getKind() == APPLY_UF)
373		{
374		visitctx->pushOp(cur, curCVal);
375		}
376	268685	visitctx->pushChildren(cur, curCVal);
377		}
378		else
379		{
380	1236095	visit.push_back(cur);
381		// visit operator if apply uf
382	1236095	if (d_rewriteOps && cur.getKind() == APPLY_UF)
383		{
384	74550	visit.push_back(cur.getOperator());
385		}
386	1236095	visit.insert(visit.end(), cur.begin(), cur.end());
387		}
388		}
389	2441014	else if (it->second.isNull())
390		{
391	1781508	itr = rewritten.find(curHash);
392	1781508	if (itr != rewritten.end())
393		{
394		// only can generate partially rewritten nodes when rewrite again is
395		// true.
396	326197	Assert(d_policy != TConvPolicy::ONCE);
397		// if it was rewritten, check the status of the rewritten node,
398		// which should be finished now
399	652394	Node rcur = itr->second;
400	652394	Trace("tconv-pf-gen-rewrite")
401	326197	<< "- postvisit, previously rewritten to " << rcur << std::endl;
402	652394	Node rcurHash = rcur;
403	326197	if (tctx != nullptr)
404		{
405	53373	rcurHash = TCtxNode::computeNodeHash(rcur, curCVal);
406		}
407	326197	Assert(cur != rcur);
408		// the final rewritten form of cur is the final form of rcur
409	652394	Node rcurFinal = visited[rcurHash];
410	326197	Assert(!rcurFinal.isNull());
411	326197	if (rcurFinal != rcur)
412		{
413		// must connect via TRANS
414	237168	std::vector<Node> pfChildren;
415	118584	pfChildren.push_back(cur.eqNode(rcur));
416	118584	pfChildren.push_back(rcur.eqNode(rcurFinal));
417	237168	Node result = cur.eqNode(rcurFinal);
418	118584	pf.addStep(result, PfRule::TRANS, pfChildren, {});
419		}
420	652394	Trace("tconv-pf-gen-rewrite")
421	326197	<< "-> (rewritten postrewrite) " << curHash << " = " << rcurFinal
422	326197	<< std::endl;
423	326197	visited[curHash] = rcurFinal;
424	326197	doCache(curHash, cur, rcurFinal, pf);
425		}
426		else
427		{
428	1455311	Trace("tconv-pf-gen-rewrite") << "- postvisit" << std::endl;
429	2910622	Node ret = cur;
430	2910622	Node retHash = curHash;
431	1455311	bool childChanged = false;
432	2910622	std::vector<Node> children;
433	1455311	Kind ck = cur.getKind();
434	1455311	if (d_rewriteOps && ck == APPLY_UF)
435		{
436		// the operator of APPLY_UF is visited
437	149100	Node cop = cur.getOperator();
438	74550	if (tctx != nullptr)
439		{
440		uint32_t coval = tctx->computeValueOp(cur, curCVal);
441		Node coHash = TCtxNode::computeNodeHash(cop, coval);
442		it = visited.find(coHash);
443		}
444		else
445		{
446	74550	it = visited.find(cop);
447		}
448	74550	Assert(it != visited.end());
449	74550	Assert(!it->second.isNull());
450	74550	childChanged = childChanged \|\| cop != it->second;
451	149100	children.push_back(it->second);
452		}
453	1380761	else if (cur.getMetaKind() == metakind::PARAMETERIZED)
454		{
455		// all other parametrized operators are unchanged
456	80932	children.push_back(cur.getOperator());
457		}
458		// get the results of the children
459	1455311	if (tctx != nullptr)
460		{
461	621236	for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
462		{
463	707742	Node cn = cur[i];
464	353871	uint32_t cnval = tctx->computeValue(cur, curCVal, i);
465	707742	Node cnHash = TCtxNode::computeNodeHash(cn, cnval);
466	353871	it = visited.find(cnHash);
467	353871	Assert(it != visited.end());
468	353871	Assert(!it->second.isNull());
469	353871	childChanged = childChanged \|\| cn != it->second;
470	353871	children.push_back(it->second);
471		}
472		}
473		else
474		{
475		// can use simple loop if not term-context-sensitive
476	3453636	for (const Node& cn : cur)
477		{
478	2265690	it = visited.find(cn);
479	2265690	Assert(it != visited.end());
480	2265690	Assert(!it->second.isNull());
481	2265690	childChanged = childChanged \|\| cn != it->second;
482	2265690	children.push_back(it->second);
483		}
484		}
485	1455311	if (childChanged)
486		{
487	356878	ret = nm->mkNode(ck, children);
488	356878	rewritten[curHash] = ret;
489		// congruence to show (cur = ret)
490	356878	PfRule congRule = PfRule::CONG;
491	713756	std::vector<Node> pfChildren;
492	713756	std::vector<Node> pfArgs;
493	356878	pfArgs.push_back(ProofRuleChecker::mkKindNode(ck));
494	356878	if (ck == APPLY_UF && children[0] != cur.getOperator())
495		{
496		// use HO_CONG if the operator changed
497	215	congRule = PfRule::HO_CONG;
498	215	pfChildren.push_back(cur.getOperator().eqNode(children[0]));
499		}
500	356663	else if (kind::metaKindOf(ck) == kind::metakind::PARAMETERIZED)
501		{
502	23047	pfArgs.push_back(cur.getOperator());
503		}
504	1229156	for (size_t i = 0, size = cur.getNumChildren(); i < size; i++)
505		{
506	872278	if (cur[i] == ret[i])
507		{
508		// ensure REFL proof for unchanged children
509	247503	pf.addStep(cur[i].eqNode(cur[i]), PfRule::REFL, {}, {cur[i]});
510		}
511	872278	pfChildren.push_back(cur[i].eqNode(ret[i]));
512		}
513	713756	Node result = cur.eqNode(ret);
514	356878	pf.addStep(result, congRule, pfChildren, pfArgs);
515		// must update the hash
516	356878	retHash = ret;
517	356878	if (tctx != nullptr)
518		{
519	90186	retHash = TCtxNode::computeNodeHash(ret, curCVal);
520		}
521		}
522	1098433	else if (tctx != nullptr)
523		{
524		// now we need the hash
525	177179	retHash = TCtxNode::computeNodeHash(cur, curCVal);
526		}
527		// did we rewrite ret (at post-rewrite)?
528	2910622	Node rret = getRewriteStepInternal(retHash, false);
529	1455311	if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT)
530		{
531	210512	Trace("tconv-pf-gen-rewrite")
532	105256	<< "*** " << retHash << " postrewrites to " << rret << std::endl;
533		// d_proof should have a proof of ret = rret, hence nothing to do
534		// here, for the same reasons as above. It also may be the case that
535		// rret rewrites, hence we must revisit ret.
536	105256	rewritten[retHash] = rret;
537	105256	if (tctx != nullptr)
538		{
539	2586	if (cur != ret)
540		{
541	1321	visitctx->push(cur, curCVal);
542		}
543	2586	visitctx->push(ret, curCVal);
544	2586	visitctx->push(rret, curCVal);
545		}
546		else
547		{
548	102670	if (cur != ret)
549		{
550	64505	visit.push_back(cur);
551		}
552	102670	visit.push_back(ret);
553	102670	visit.push_back(rret);
554		}
555		}
556		else
557		{
558		// If we changed due to congruence, and then rewrote, then we
559		// require a trans step to connect here
560	1350055	if (!rret.isNull() && childChanged)
561		{
562	12512	std::vector<Node> pfChildren;
563	6256	pfChildren.push_back(cur.eqNode(ret));
564	6256	pfChildren.push_back(ret.eqNode(rret));
565	12512	Node result = cur.eqNode(rret);
566	6256	pf.addStep(result, PfRule::TRANS, pfChildren, {});
567		}
568		// take its rewrite if it rewrote and we have ONCE rewriting policy
569	1350055	ret = rret.isNull() ? ret : rret;
570	2700110	Trace("tconv-pf-gen-rewrite")
571	1350055	<< "-> (postrewrite) " << curHash << " = " << ret << std::endl;
572		// it is final
573	1350055	Assert(!ret.isNull());
574	1350055	visited[curHash] = ret;
575	1350055	doCache(curHash, cur, ret, pf);
576		}
577		}
578		}
579		else
580		{
581	659506	Trace("tconv-pf-gen-rewrite") << "- already visited" << std::endl;
582		}
583	5091677	} while (!(tctx != nullptr ? visitctx->empty() : visit.empty()));
584	108309	Assert(visited.find(tinitialHash) != visited.end());
585	108309	Assert(!visited.find(tinitialHash)->second.isNull());
586	216618	Trace("tconv-pf-gen-rewrite")
587	108309	<< "...finished, return " << visited[tinitialHash] << std::endl;
588		// return the conclusion of the overall proof
589	216618	return t.eqNode(visited[tinitialHash]);
590		}
591
592	1686766	void TConvProofGenerator::doCache(Node curHash,
593		Node cur,
594		Node r,
595		LazyCDProof& pf)
596		{
597	1686766	if (d_cpolicy != TConvCachePolicy::NEVER)
598		{
599	1293124	Node eq = cur.eqNode(r);
600	646562	d_cache[curHash] = pf.getProofFor(eq);
601		}
602	1686766	}
603
604	4207479	Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const
605		{
606	4207479	const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
607	4207479	NodeNodeMap::const_iterator it = rm.find(t);
608	4207479	if (it == rm.end())
609		{
610	3705575	return Node::null();
611		}
612	501904	return (*it).second;
613		}
614	314634	std::string TConvProofGenerator::identify() const { return d_name; }
615
616	108309	std::string TConvProofGenerator::toStringDebug() const
617		{
618	216618	std::stringstream ss;
619	216618	ss << identify() << " (policy=" << d_policy << ", cache policy=" << d_cpolicy
620	108309	<< (d_tcontext != nullptr ? ", term-context-sensitive" : "") << ")";
621	216618	return ss.str();
622		}
623
624	31125	} // namespace cvc5