Head

GCC Code Coverage Report

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