Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/conv_proof_generator.cpp	Lines:	253	315	80.3 %
Date:	2021-09-29	Branches:	521	1597	32.6 %


/******************************************************************************
 * 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	275	std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
31		{
32	275	switch (tcpol)
33		{
34	225	case TConvPolicy::FIXPOINT: out << "FIXPOINT"; break;
35	50	case TConvPolicy::ONCE: out << "ONCE"; break;
36		default: out << "TConvPolicy:unknown"; break;
37		}
38	275	return out;
39		}
40
41	275	std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol)
42		{
43	275	switch (tcpol)
44		{
45	43	case TConvCachePolicy::STATIC: out << "STATIC"; break;
46		case TConvCachePolicy::DYNAMIC: out << "DYNAMIC"; break;
47	232	case TConvCachePolicy::NEVER: out << "NEVER"; break;
48		default: out << "TConvCachePolicy:unknown"; break;
49		}
50	275	return out;
51		}
52
53	1086	TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
54		context::Context* c,
55		TConvPolicy pol,
56		TConvCachePolicy cpol,
57		std::string name,
58		TermContext* tccb,
59	1086	bool rewriteOps)
60	2172	: 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	3258	d_rewriteOps(rewriteOps)
68		{
69	1086	}
70
71	2028	TConvProofGenerator::~TConvProofGenerator() {}
72
73	735	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	1470	Node eq = registerRewriteStep(t, s, tctx, isPre);
82	735	if (!eq.isNull())
83		{
84	735	d_proof.addLazyStep(eq, pg, trustId, isClosed);
85		}
86	735	}
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	4522	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	9044	Node eq = registerRewriteStep(t, s, tctx, isPre);
107	4522	if (!eq.isNull())
108		{
109	3304	d_proof.addStep(eq, id, children, args);
110		}
111	4522	}
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	5257	Node TConvProofGenerator::registerRewriteStep(Node t,
133		Node s,
134		uint32_t tctx,
135		bool isPre)
136		{
137	5257	Assert(!t.isNull());
138	5257	Assert(!s.isNull());
139
140	5257	if (t == s)
141		{
142		return Node::null();
143		}
144	10514	Node thash = t;
145	5257	if (d_tcontext != nullptr)
146		{
147	1479	thash = TCtxNode::computeNodeHash(t, tctx);
148		}
149		else
150		{
151		// don't use term context ids if not using term context
152	3778	Assert(tctx == 0);
153		}
154		// should not rewrite term to two different things
155	5257	if (!getRewriteStepInternal(thash, isPre).isNull())
156		{
157	2436	Assert(getRewriteStepInternal(thash, isPre) == s)
158	1218	<< identify() << " rewriting " << t << " to both " << s << " and "
159	1218	<< getRewriteStepInternal(thash, isPre);
160	1218	return Node::null();
161		}
162	4039	NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
163	4039	rm[thash] = s;
164	4039	if (d_cpolicy == TConvCachePolicy::DYNAMIC)
165		{
166		// clear the cache
167		d_cache.clear();
168		}
169	4039	return t.eqNode(s);
170		}
171
172	274	std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
173		{
174	548	Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << identify()
175	274	<< ": " << f << std::endl;
176	274	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	548	d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof");
188	274	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	548	Node conc = getProofForRewriting(f[0], lpf, d_tcontext);
198	274	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	548	std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f);
234	274	Trace("tconv-pf-gen") << "... success" << std::endl;
235	274	Assert(pfn != nullptr);
236	274	Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
237	274	return pfn;
238		}
239
240	1	std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
241		{
242		LazyCDProof lpf(
243	2	d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProofRew");
244	2	Node conc = getProofForRewriting(n, lpf, d_tcontext);
245	1	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	1	std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc);
253	1	Assert(pfn != nullptr);
254	1	Trace("tconv-pf-gen-debug-pf") << "... proof is " << *pfn << std::endl;
255	2	return pfn;
256		}
257
258	275	Node TConvProofGenerator::getProofForRewriting(Node t,
259		LazyCDProof& pf,
260		TermContext* tctx)
261		{
262	275	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	550	std::unordered_map<Node, Node> visited;
270		// the rewritten form of terms we have processed so far
271	550	std::unordered_map<Node, Node> rewritten;
272	275	std::unordered_map<Node, Node>::iterator it;
273	275	std::unordered_map<Node, Node>::iterator itr;
274	275	std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
275	550	Trace("tconv-pf-gen-rewrite")
276	550	<< "TConvProofGenerator::getProofForRewriting: " << toStringDebug()
277	275	<< std::endl;
278	275	Trace("tconv-pf-gen-rewrite") << "Input: " << t << std::endl;
279		// if provided, we use term context for cache
280	550	std::shared_ptr<TCtxStack> visitctx;
281		// otherwise, visit is used if we don't have a term context
282	550	std::vector<TNode> visit;
283	550	Node tinitialHash;
284	275	if (tctx != nullptr)
285		{
286	182	visitctx = std::make_shared<TCtxStack>(tctx);
287	182	visitctx->pushInitial(t);
288	182	tinitialHash = TCtxNode::computeNodeHash(t, tctx->initialValue());
289		}
290		else
291		{
292	93	visit.push_back(t);
293	93	tinitialHash = t;
294		}
295	550	Node cur;
296	275	uint32_t curCVal = 0;
297	550	Node curHash;
298	5884	do
299		{
300		// pop the top element
301	6159	if (tctx != nullptr)
302		{
303	11256	std::pair<Node, uint32_t> curPair = visitctx->getCurrent();
304	5628	cur = curPair.first;
305	5628	curCVal = curPair.second;
306	5628	curHash = TCtxNode::computeNodeHash(cur, curCVal);
307	5628	visitctx->pop();
308		}
309		else
310		{
311	531	cur = visit.back();
312	531	curHash = cur;
313	531	visit.pop_back();
314		}
315	6159	Trace("tconv-pf-gen-rewrite") << "* visit : " << curHash << std::endl;
316		// has the proof for cur been cached?
317	6159	itc = d_cache.find(curHash);
318	6159	if (itc != d_cache.end())
319		{
320	240	Node res = itc->second->getResult();
321	120	Assert(res.getKind() == EQUAL);
322	120	Assert(!res[1].isNull());
323	120	visited[curHash] = res[1];
324	120	pf.addProof(itc->second);
325	120	continue;
326		}
327	6039	it = visited.find(curHash);
328	6039	if (it == visited.end())
329		{
330	2617	Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl;
331	2617	visited[curHash] = Node::null();
332		// did we rewrite the current node (at pre-rewrite)?
333	5234	Node rcur = getRewriteStepInternal(curHash, true);
334	2617	if (!rcur.isNull())
335		{
336	676	Trace("tconv-pf-gen-rewrite")
337	338	<< "*** " << 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	338	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	288	rewritten[curHash] = rcur;
346	288	if (tctx != nullptr)
347		{
348	256	visitctx->push(cur, curCVal);
349	256	visitctx->push(rcur, curCVal);
350		}
351		else
352		{
353	32	visit.push_back(cur);
354	32	visit.push_back(rcur);
355		}
356		}
357		else
358		{
359	50	Assert(d_policy == TConvPolicy::ONCE);
360	100	Trace("tconv-pf-gen-rewrite") << "-> (once, prewrite) " << curHash
361	50	<< " = " << rcur << std::endl;
362		// not rewriting again, rcur is final
363	50	Assert(!rcur.isNull());
364	50	visited[curHash] = rcur;
365	50	doCache(curHash, cur, rcur, pf);
366		}
367		}
368	2279	else if (tctx != nullptr)
369		{
370	2146	visitctx->push(cur, curCVal);
371		// visit operator if apply uf
372	2146	if (d_rewriteOps && cur.getKind() == APPLY_UF)
373		{
374		visitctx->pushOp(cur, curCVal);
375		}
376	2146	visitctx->pushChildren(cur, curCVal);
377		}
378		else
379		{
380	133	visit.push_back(cur);
381		// visit operator if apply uf
382	133	if (d_rewriteOps && cur.getKind() == APPLY_UF)
383		{
384	5	visit.push_back(cur.getOperator());
385		}
386	133	visit.insert(visit.end(), cur.begin(), cur.end());
387		}
388		}
389	3422	else if (it->second.isNull())
390		{
391	2592	itr = rewritten.find(curHash);
392	2592	if (itr != rewritten.end())
393		{
394		// only can generate partially rewritten nodes when rewrite again is
395		// true.
396	328	Assert(d_policy != TConvPolicy::ONCE);
397		// if it was rewritten, check the status of the rewritten node,
398		// which should be finished now
399	656	Node rcur = itr->second;
400	656	Trace("tconv-pf-gen-rewrite")
401	328	<< "- postvisit, previously rewritten to " << rcur << std::endl;
402	656	Node rcurHash = rcur;
403	328	if (tctx != nullptr)
404		{
405	256	rcurHash = TCtxNode::computeNodeHash(rcur, curCVal);
406		}
407	328	Assert(cur != rcur);
408		// the final rewritten form of cur is the final form of rcur
409	656	Node rcurFinal = visited[rcurHash];
410	328	Assert(!rcurFinal.isNull());
411	328	if (rcurFinal != rcur)
412		{
413		// must connect via TRANS
414	56	std::vector<Node> pfChildren;
415	28	pfChildren.push_back(cur.eqNode(rcur));
416	28	pfChildren.push_back(rcur.eqNode(rcurFinal));
417	56	Node result = cur.eqNode(rcurFinal);
418	28	pf.addStep(result, PfRule::TRANS, pfChildren, {});
419		}
420	656	Trace("tconv-pf-gen-rewrite")
421	328	<< "-> (rewritten postrewrite) " << curHash << " = " << rcurFinal
422	328	<< std::endl;
423	328	visited[curHash] = rcurFinal;
424	328	doCache(curHash, cur, rcurFinal, pf);
425		}
426		else
427		{
428	2264	Trace("tconv-pf-gen-rewrite") << "- postvisit" << std::endl;
429	4528	Node ret = cur;
430	4528	Node retHash = curHash;
431	2264	bool childChanged = false;
432	4528	std::vector<Node> children;
433	2264	Kind ck = cur.getKind();
434	2264	if (d_rewriteOps && ck == APPLY_UF)
435		{
436		// the operator of APPLY_UF is visited
437	10	Node cop = cur.getOperator();
438	5	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	5	it = visited.find(cop);
447		}
448	5	Assert(it != visited.end());
449	5	Assert(!it->second.isNull());
450	5	childChanged = childChanged \|\| cop != it->second;
451	10	children.push_back(it->second);
452		}
453	2259	else if (cur.getMetaKind() == metakind::PARAMETERIZED)
454		{
455		// all other parametrized operators are unchanged
456	9	children.push_back(cur.getOperator());
457		}
458		// get the results of the children
459	2264	if (tctx != nullptr)
460		{
461	4934	for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
462		{
463	5576	Node cn = cur[i];
464	2788	uint32_t cnval = tctx->computeValue(cur, curCVal, i);
465	5576	Node cnHash = TCtxNode::computeNodeHash(cn, cnval);
466	2788	it = visited.find(cnHash);
467	2788	Assert(it != visited.end());
468	2788	Assert(!it->second.isNull());
469	2788	childChanged = childChanged \|\| cn != it->second;
470	2788	children.push_back(it->second);
471		}
472		}
473		else
474		{
475		// can use simple loop if not term-context-sensitive
476	259	for (const Node& cn : cur)
477		{
478	141	it = visited.find(cn);
479	141	Assert(it != visited.end());
480	141	Assert(!it->second.isNull());
481	141	childChanged = childChanged \|\| cn != it->second;
482	141	children.push_back(it->second);
483		}
484		}
485	2264	if (childChanged)
486		{
487	202	ret = nm->mkNode(ck, children);
488	202	rewritten[curHash] = ret;
489		// congruence to show (cur = ret)
490	202	PfRule congRule = PfRule::CONG;
491	404	std::vector<Node> pfChildren;
492	404	std::vector<Node> pfArgs;
493	202	pfArgs.push_back(ProofRuleChecker::mkKindNode(ck));
494	202	if (ck == APPLY_UF && children[0] != cur.getOperator())
495		{
496		// use HO_CONG if the operator changed
497		congRule = PfRule::HO_CONG;
498		pfChildren.push_back(cur.getOperator().eqNode(children[0]));
499		}
500	202	else if (kind::metaKindOf(ck) == kind::metakind::PARAMETERIZED)
501		{
502		pfArgs.push_back(cur.getOperator());
503		}
504	776	for (size_t i = 0, size = cur.getNumChildren(); i < size; i++)
505		{
506	574	if (cur[i] == ret[i])
507		{
508		// ensure REFL proof for unchanged children
509	288	pf.addStep(cur[i].eqNode(cur[i]), PfRule::REFL, {}, {cur[i]});
510		}
511	574	pfChildren.push_back(cur[i].eqNode(ret[i]));
512		}
513	404	Node result = cur.eqNode(ret);
514	202	pf.addStep(result, congRule, pfChildren, pfArgs);
515		// must update the hash
516	202	retHash = ret;
517	202	if (tctx != nullptr)
518		{
519	182	retHash = TCtxNode::computeNodeHash(ret, curCVal);
520		}
521		}
522	2062	else if (tctx != nullptr)
523		{
524		// now we need the hash
525	1964	retHash = TCtxNode::computeNodeHash(cur, curCVal);
526		}
527		// did we rewrite ret (at post-rewrite)?
528	4528	Node rret = getRewriteStepInternal(retHash, false);
529	2264	if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT)
530		{
531	50	Trace("tconv-pf-gen-rewrite")
532	25	<< "*** " << 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	25	rewritten[retHash] = rret;
537	25	if (tctx != nullptr)
538		{
539		if (cur != ret)
540		{
541		visitctx->push(cur, curCVal);
542		}
543		visitctx->push(ret, curCVal);
544		visitctx->push(rret, curCVal);
545		}
546		else
547		{
548	25	if (cur != ret)
549		{
550	15	visit.push_back(cur);
551		}
552	25	visit.push_back(ret);
553	25	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	2239	if (!rret.isNull() && childChanged)
561		{
562		std::vector<Node> pfChildren;
563		pfChildren.push_back(cur.eqNode(ret));
564		pfChildren.push_back(ret.eqNode(rret));
565		Node result = cur.eqNode(rret);
566		pf.addStep(result, PfRule::TRANS, pfChildren, {});
567		}
568		// take its rewrite if it rewrote and we have ONCE rewriting policy
569	2239	ret = rret.isNull() ? ret : rret;
570	4478	Trace("tconv-pf-gen-rewrite")
571	2239	<< "-> (postrewrite) " << curHash << " = " << ret << std::endl;
572		// it is final
573	2239	Assert(!ret.isNull());
574	2239	visited[curHash] = ret;
575	2239	doCache(curHash, cur, ret, pf);
576		}
577		}
578		}
579		else
580		{
581	830	Trace("tconv-pf-gen-rewrite") << "- already visited" << std::endl;
582		}
583	6159	} while (!(tctx != nullptr ? visitctx->empty() : visit.empty()));
584	275	Assert(visited.find(tinitialHash) != visited.end());
585	275	Assert(!visited.find(tinitialHash)->second.isNull());
586	550	Trace("tconv-pf-gen-rewrite")
587	275	<< "...finished, return " << visited[tinitialHash] << std::endl;
588		// return the conclusion of the overall proof
589	550	return t.eqNode(visited[tinitialHash]);
590		}
591
592	2617	void TConvProofGenerator::doCache(Node curHash,
593		Node cur,
594		Node r,
595		LazyCDProof& pf)
596		{
597	2617	if (d_cpolicy != TConvCachePolicy::NEVER)
598		{
599	282	Node eq = cur.eqNode(r);
600	141	d_cache[curHash] = pf.getProofFor(eq);
601		}
602	2617	}
603
604	11356	Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const
605		{
606	11356	const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
607	11356	NodeNodeMap::const_iterator it = rm.find(t);
608	11356	if (it == rm.end())
609		{
610	8557	return Node::null();
611		}
612	2799	return (*it).second;
613		}
614	5304	std::string TConvProofGenerator::identify() const { return d_name; }
615
616	275	std::string TConvProofGenerator::toStringDebug() const
617		{
618	550	std::stringstream ss;
619	550	ss << identify() << " (policy=" << d_policy << ", cache policy=" << d_cpolicy
620	275	<< (d_tcontext != nullptr ? ", term-context-sensitive" : "") << ")";
621	550	return ss.str();
622		}
623
624	22746	} // namespace cvc5