Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/expr/term_conversion_proof_generator.cpp	Lines:	260	315	82.5 %
Date:	2021-05-22	Branches:	546	1599	34.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 "expr/term_conversion_proof_generator.h"

#include <sstream>

#include "expr/proof_checker.h"
#include "expr/proof_node.h"
#include "expr/proof_node_algorithm.h"
#include "expr/term_context.h"
#include "expr/term_context_stack.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") << "Printing 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") << "... 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") << "... 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 "expr/term_conversion_proof_generator.h"
17
18		#include <sstream>
19
20		#include "expr/proof_checker.h"
21		#include "expr/proof_node.h"
22		#include "expr/proof_node_algorithm.h"
23		#include "expr/term_context.h"
24		#include "expr/term_context_stack.h"
25
26		using namespace cvc5::kind;
27
28		namespace cvc5 {
29
30	94370	std::ostream& operator<<(std::ostream& out, TConvPolicy tcpol)
31		{
32	94370	switch (tcpol)
33		{
34	85472	case TConvPolicy::FIXPOINT: out << "FIXPOINT"; break;
35	8898	case TConvPolicy::ONCE: out << "ONCE"; break;
36		default: out << "TConvPolicy:unknown"; break;
37		}
38	94370	return out;
39		}
40
41	94370	std::ostream& operator<<(std::ostream& out, TConvCachePolicy tcpol)
42		{
43	94370	switch (tcpol)
44		{
45	57088	case TConvCachePolicy::STATIC: out << "STATIC"; break;
46		case TConvCachePolicy::DYNAMIC: out << "DYNAMIC"; break;
47	37282	case TConvCachePolicy::NEVER: out << "NEVER"; break;
48		default: out << "TConvCachePolicy:unknown"; break;
49		}
50	94370	return out;
51		}
52
53	33163	TConvProofGenerator::TConvProofGenerator(ProofNodeManager* pnm,
54		context::Context* c,
55		TConvPolicy pol,
56		TConvCachePolicy cpol,
57		std::string name,
58		TermContext* tccb,
59	33163	bool rewriteOps)
60	66326	: 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	99489	d_rewriteOps(rewriteOps)
68		{
69	33163	}
70
71	54820	TConvProofGenerator::~TConvProofGenerator() {}
72
73	322804	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	645608	Node eq = registerRewriteStep(t, s, tctx, isPre);
82	322804	if (!eq.isNull())
83		{
84	322719	d_proof.addLazyStep(eq, pg, trustId, isClosed);
85		}
86	322804	}
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	281178	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	562356	Node eq = registerRewriteStep(t, s, tctx, isPre);
107	281178	if (!eq.isNull())
108		{
109	195913	d_proof.addStep(eq, id, children, args);
110		}
111	281178	}
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	603982	Node TConvProofGenerator::registerRewriteStep(Node t,
133		Node s,
134		uint32_t tctx,
135		bool isPre)
136		{
137	603982	Assert(!t.isNull());
138	603982	Assert(!s.isNull());
139
140	603982	if (t == s)
141		{
142		return Node::null();
143		}
144	1207964	Node thash = t;
145	603982	if (d_tcontext != nullptr)
146		{
147	70286	thash = TCtxNode::computeNodeHash(t, tctx);
148		}
149		else
150		{
151		// don't use term context ids if not using term context
152	533696	Assert(tctx == 0);
153		}
154		// should not rewrite term to two different things
155	603982	if (!getRewriteStepInternal(thash, isPre).isNull())
156		{
157	170700	Assert(getRewriteStepInternal(thash, isPre) == s)
158	85350	<< identify() << " rewriting " << t << " to both " << s << " and "
159	85350	<< getRewriteStepInternal(thash, isPre);
160	85350	return Node::null();
161		}
162	518632	NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
163	518632	rm[thash] = s;
164	518632	if (d_cpolicy == TConvCachePolicy::DYNAMIC)
165		{
166		// clear the cache
167		d_cache.clear();
168		}
169	518632	return t.eqNode(s);
170		}
171
172	86549	std::shared_ptr<ProofNode> TConvProofGenerator::getProofFor(Node f)
173		{
174	173098	Trace("tconv-pf-gen") << "TConvProofGenerator::getProofFor: " << identify()
175	86549	<< ": " << f << std::endl;
176	86549	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	173098	d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProof");
188	86549	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	173098	Node conc = getProofForRewriting(f[0], lpf, d_tcontext);
198	86549	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") << "Printing 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	173098	std::shared_ptr<ProofNode> pfn = lpf.getProofFor(f);
234	86549	Trace("tconv-pf-gen") << "... success" << std::endl;
235	86549	Assert (pfn!=nullptr);
236	86549	Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl;
237	86549	return pfn;
238		}
239
240	7821	std::shared_ptr<ProofNode> TConvProofGenerator::getProofForRewriting(Node n)
241		{
242		LazyCDProof lpf(
243	15642	d_proof.getManager(), &d_proof, nullptr, d_name + "::LazyCDProofRew");
244	15642	Node conc = getProofForRewriting(n, lpf, d_tcontext);
245	7821	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	7821	std::shared_ptr<ProofNode> pfn = lpf.getProofFor(conc);
253	7821	Assert(pfn != nullptr);
254	7821	Trace("tconv-pf-gen-debug") << "... proof is " << *pfn << std::endl;
255	15642	return pfn;
256		}
257
258	94370	Node TConvProofGenerator::getProofForRewriting(Node t,
259		LazyCDProof& pf,
260		TermContext* tctx)
261		{
262	94370	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	188740	std::unordered_map<Node, Node> visited;
270		// the rewritten form of terms we have processed so far
271	188740	std::unordered_map<Node, Node> rewritten;
272	94370	std::unordered_map<Node, Node>::iterator it;
273	94370	std::unordered_map<Node, Node>::iterator itr;
274	94370	std::map<Node, std::shared_ptr<ProofNode> >::iterator itc;
275	188740	Trace("tconv-pf-gen-rewrite")
276	188740	<< "TConvProofGenerator::getProofForRewriting: " << toStringDebug()
277	94370	<< std::endl;
278	94370	Trace("tconv-pf-gen-rewrite") << "Input: " << t << std::endl;
279		// if provided, we use term context for cache
280	188740	std::shared_ptr<TCtxStack> visitctx;
281		// otherwise, visit is used if we don't have a term context
282	188740	std::vector<TNode> visit;
283	188740	Node tinitialHash;
284	94370	if (tctx != nullptr)
285		{
286	18450	visitctx = std::make_shared<TCtxStack>(tctx);
287	18450	visitctx->pushInitial(t);
288	18450	tinitialHash = TCtxNode::computeNodeHash(t, tctx->initialValue());
289		}
290		else
291		{
292	75920	visit.push_back(t);
293	75920	tinitialHash = t;
294		}
295	188740	Node cur;
296	94370	uint32_t curCVal = 0;
297	188740	Node curHash;
298	4932932	do
299		{
300		// pop the top element
301	5027302	if (tctx != nullptr)
302		{
303	1782304	std::pair<Node, uint32_t> curPair = visitctx->getCurrent();
304	891152	cur = curPair.first;
305	891152	curCVal = curPair.second;
306	891152	curHash = TCtxNode::computeNodeHash(cur, curCVal);
307	891152	visitctx->pop();
308		}
309		else
310		{
311	4136150	cur = visit.back();
312	4136150	curHash = cur;
313	4136150	visit.pop_back();
314		}
315	5027302	Trace("tconv-pf-gen-rewrite") << "* visit : " << curHash << std::endl;
316		// has the proof for cur been cached?
317	5027302	itc = d_cache.find(curHash);
318	5027302	if (itc != d_cache.end())
319		{
320	1659450	Node res = itc->second->getResult();
321	829725	Assert(res.getKind() == EQUAL);
322	829725	Assert(!res[1].isNull());
323	829725	visited[curHash] = res[1];
324	829725	pf.addProof(itc->second);
325	829725	continue;
326		}
327	4197577	it = visited.find(curHash);
328	4197577	if (it == visited.end())
329		{
330	1625158	Trace("tconv-pf-gen-rewrite") << "- previsit" << std::endl;
331	1625158	visited[curHash] = Node::null();
332		// did we rewrite the current node (at pre-rewrite)?
333	3250316	Node rcur = getRewriteStepInternal(curHash, true);
334	1625158	if (!rcur.isNull())
335		{
336	284208	Trace("tconv-pf-gen-rewrite")
337	142104	<< "*** " << 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	142104	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	132683	rewritten[curHash] = rcur;
346	132683	if (tctx != nullptr)
347		{
348	47557	visitctx->push(cur, curCVal);
349	47557	visitctx->push(rcur, curCVal);
350		}
351		else
352		{
353	85126	visit.push_back(cur);
354	85126	visit.push_back(rcur);
355		}
356		}
357		else
358		{
359	9421	Assert(d_policy == TConvPolicy::ONCE);
360	18842	Trace("tconv-pf-gen-rewrite") << "-> (once, prewrite) " << curHash
361	9421	<< " = " << rcur << std::endl;
362		// not rewriting again, rcur is final
363	9421	Assert(!rcur.isNull());
364	9421	visited[curHash] = rcur;
365	9421	doCache(curHash, cur, rcur, pf);
366		}
367		}
368	1483054	else if (tctx != nullptr)
369		{
370	281900	visitctx->push(cur, curCVal);
371		// visit operator if apply uf
372	281900	if (d_rewriteOps && cur.getKind() == APPLY_UF)
373		{
374		visitctx->pushOp(cur, curCVal);
375		}
376	281900	visitctx->pushChildren(cur, curCVal);
377		}
378		else
379		{
380	1201154	visit.push_back(cur);
381		// visit operator if apply uf
382	1201154	if (d_rewriteOps && cur.getKind() == APPLY_UF)
383		{
384	73305	visit.push_back(cur.getOperator());
385		}
386	1201154	visit.insert(visit.end(), cur.begin(), cur.end());
387		}
388		}
389	2572419	else if (it->second.isNull())
390		{
391	1697456	itr = rewritten.find(curHash);
392	1697456	if (itr != rewritten.end())
393		{
394		// only can generate partially rewritten nodes when rewrite again is
395		// true.
396	248804	Assert(d_policy != TConvPolicy::ONCE);
397		// if it was rewritten, check the status of the rewritten node,
398		// which should be finished now
399	497608	Node rcur = itr->second;
400	497608	Trace("tconv-pf-gen-rewrite")
401	248804	<< "- postvisit, previously rewritten to " << rcur << std::endl;
402	497608	Node rcurHash = rcur;
403	248804	if (tctx != nullptr)
404		{
405	55057	rcurHash = TCtxNode::computeNodeHash(rcur, curCVal);
406		}
407	248804	Assert(cur != rcur);
408		// the final rewritten form of cur is the final form of rcur
409	497608	Node rcurFinal = visited[rcurHash];
410	248804	Assert(!rcurFinal.isNull());
411	248804	if (rcurFinal != rcur)
412		{
413		// must connect via TRANS
414	158500	std::vector<Node> pfChildren;
415	79250	pfChildren.push_back(cur.eqNode(rcur));
416	79250	pfChildren.push_back(rcur.eqNode(rcurFinal));
417	158500	Node result = cur.eqNode(rcurFinal);
418	79250	pf.addStep(result, PfRule::TRANS, pfChildren, {});
419		}
420	497608	Trace("tconv-pf-gen-rewrite")
421	248804	<< "-> (rewritten postrewrite) " << curHash << " = " << rcurFinal
422	248804	<< std::endl;
423	248804	visited[curHash] = rcurFinal;
424	248804	doCache(curHash, cur, rcurFinal, pf);
425		}
426		else
427		{
428	1448652	Trace("tconv-pf-gen-rewrite") << "- postvisit" << std::endl;
429	2897304	Node ret = cur;
430	2897304	Node retHash = curHash;
431	1448652	bool childChanged = false;
432	2897304	std::vector<Node> children;
433	1448652	Kind ck = cur.getKind();
434	1448652	if (d_rewriteOps && ck == APPLY_UF)
435		{
436		// the operator of APPLY_UF is visited
437	146610	Node cop = cur.getOperator();
438	73305	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	73305	it = visited.find(cop);
447		}
448	73305	Assert(it != visited.end());
449	73305	Assert(!it->second.isNull());
450	73305	childChanged = childChanged \|\| cop != it->second;
451	146610	children.push_back(it->second);
452		}
453	1375347	else if (cur.getMetaKind() == metakind::PARAMETERIZED)
454		{
455		// all other parametrized operators are unchanged
456	104848	children.push_back(cur.getOperator());
457		}
458		// get the results of the children
459	1448652	if (tctx != nullptr)
460		{
461	760730	for (size_t i = 0, nchild = cur.getNumChildren(); i < nchild; i++)
462		{
463	959936	Node cn = cur[i];
464	479968	uint32_t cnval = tctx->computeValue(cur, curCVal, i);
465	959936	Node cnHash = TCtxNode::computeNodeHash(cn, cnval);
466	479968	it = visited.find(cnHash);
467	479968	Assert(it != visited.end());
468	479968	Assert(!it->second.isNull());
469	479968	childChanged = childChanged \|\| cn != it->second;
470	479968	children.push_back(it->second);
471		}
472		}
473		else
474		{
475		// can use simple loop if not term-context-sensitive
476	3478198	for (const Node& cn : cur)
477		{
478	2310308	it = visited.find(cn);
479	2310308	Assert(it != visited.end());
480	2310308	Assert(!it->second.isNull());
481	2310308	childChanged = childChanged \|\| cn != it->second;
482	2310308	children.push_back(it->second);
483		}
484		}
485	1448652	if (childChanged)
486		{
487	289844	ret = nm->mkNode(ck, children);
488	289844	rewritten[curHash] = ret;
489		// congruence to show (cur = ret)
490	289844	PfRule congRule = PfRule::CONG;
491	579688	std::vector<Node> pfChildren;
492	579688	std::vector<Node> pfArgs;
493	289844	pfArgs.push_back(ProofRuleChecker::mkKindNode(ck));
494	289844	if (ck == APPLY_UF && children[0] != cur.getOperator())
495		{
496		// use HO_CONG if the operator changed
497	207	congRule = PfRule::HO_CONG;
498	207	pfChildren.push_back(cur.getOperator().eqNode(children[0]));
499		}
500	289637	else if (kind::metaKindOf(ck) == kind::metakind::PARAMETERIZED)
501		{
502	21766	pfArgs.push_back(cur.getOperator());
503		}
504	995227	for (size_t i = 0, size = cur.getNumChildren(); i < size; i++)
505		{
506	705383	if (cur[i] == ret[i])
507		{
508		// ensure REFL proof for unchanged children
509	215579	pf.addStep(cur[i].eqNode(cur[i]), PfRule::REFL, {}, {cur[i]});
510		}
511	705383	pfChildren.push_back(cur[i].eqNode(ret[i]));
512		}
513	579688	Node result = cur.eqNode(ret);
514	289844	pf.addStep(result, congRule, pfChildren, pfArgs);
515		// must update the hash
516	289844	retHash = ret;
517	289844	if (tctx != nullptr)
518		{
519	88824	retHash = TCtxNode::computeNodeHash(ret, curCVal);
520		}
521		}
522	1158808	else if (tctx != nullptr)
523		{
524		// now we need the hash
525	191938	retHash = TCtxNode::computeNodeHash(cur, curCVal);
526		}
527		// did we rewrite ret (at post-rewrite)?
528	2897304	Node rret = getRewriteStepInternal(retHash, false);
529	1448652	if (!rret.isNull() && d_policy == TConvPolicy::FIXPOINT)
530		{
531	163438	Trace("tconv-pf-gen-rewrite")
532	81719	<< "*** " << 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	81719	rewritten[retHash] = rret;
537	81719	if (tctx != nullptr)
538		{
539	6362	if (cur != ret)
540		{
541	1138	visitctx->push(cur, curCVal);
542		}
543	6362	visitctx->push(ret, curCVal);
544	6362	visitctx->push(rret, curCVal);
545		}
546		else
547		{
548	75357	if (cur != ret)
549		{
550	42816	visit.push_back(cur);
551		}
552	75357	visit.push_back(ret);
553	75357	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	1366933	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	1366933	ret = rret.isNull() ? ret : rret;
570	2733866	Trace("tconv-pf-gen-rewrite")
571	1366933	<< "-> (postrewrite) " << curHash << " = " << ret << std::endl;
572		// it is final
573	1366933	Assert(!ret.isNull());
574	1366933	visited[curHash] = ret;
575	1366933	doCache(curHash, cur, ret, pf);
576		}
577		}
578		}
579		else
580		{
581	874963	Trace("tconv-pf-gen-rewrite") << "- already visited" << std::endl;
582		}
583	5027302	} while (!(tctx != nullptr ? visitctx->empty() : visit.empty()));
584	94370	Assert(visited.find(tinitialHash) != visited.end());
585	94370	Assert(!visited.find(tinitialHash)->second.isNull());
586	188740	Trace("tconv-pf-gen-rewrite")
587	94370	<< "...finished, return " << visited[tinitialHash] << std::endl;
588		// return the conclusion of the overall proof
589	188740	return t.eqNode(visited[tinitialHash]);
590		}
591
592	1625158	void TConvProofGenerator::doCache(Node curHash,
593		Node cur,
594		Node r,
595		LazyCDProof& pf)
596		{
597	1625158	if (d_cpolicy != TConvCachePolicy::NEVER)
598		{
599	974944	Node eq = cur.eqNode(r);
600	487472	d_cache[curHash] = pf.getProofFor(eq);
601		}
602	1625158	}
603
604	3763142	Node TConvProofGenerator::getRewriteStepInternal(Node t, bool isPre) const
605		{
606	3763142	const NodeNodeMap& rm = isPre ? d_preRewriteMap : d_postRewriteMap;
607	3763142	NodeNodeMap::const_iterator it = rm.find(t);
608	3763142	if (it == rm.end())
609		{
610	3368619	return Node::null();
611		}
612	394523	return (*it).second;
613		}
614	292078	std::string TConvProofGenerator::identify() const { return d_name; }
615
616	94370	std::string TConvProofGenerator::toStringDebug() const
617		{
618	188740	std::stringstream ss;
619	188740	ss << identify() << " (policy=" << d_policy << ", cache policy=" << d_cpolicy
620	94370	<< (d_tcontext != nullptr ? ", term-context-sensitive" : "") << ")";
621	188740	return ss.str();
622		}
623
624	28194	} // namespace cvc5