Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/alpha_equivalence.cpp	Lines:	76	120	63.3 %
Date:	2021-09-30	Branches:	151	464	32.5 %


/******************************************************************************
 * 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.
 * ****************************************************************************
 *
 * Alpha equivalence checking.
 */

#include "theory/quantifiers/alpha_equivalence.h"

#include "proof/method_id.h"
#include "proof/proof.h"
#include "proof/proof_node.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

struct sortTypeOrder {
  expr::TermCanonize* d_tu;
  bool operator() (TypeNode i, TypeNode j) {
    return d_tu->getIdForType( i )<d_tu->getIdForType( j );
  }
};

Node AlphaEquivalenceTypeNode::registerNode(
    Node q,
    Node t,
    std::vector<TypeNode>& typs,
    std::map<TypeNode, size_t>& typCount)
{
  AlphaEquivalenceTypeNode* aetn = this;
  size_t index = 0;
  while (index < typs.size())
  {
    TypeNode curr = typs[index];
    Assert(typCount.find(curr) != typCount.end());
    Trace("aeq-debug") << "[" << curr << " " << typCount[curr] << "] ";
    std::pair<TypeNode, size_t> key(curr, typCount[curr]);
    aetn = &(aetn->d_children[key]);
    index = index + 1;
  }
  Trace("aeq-debug") << " : ";
  std::map<Node, Node>::iterator it = aetn->d_quant.find(t);
  if (it != aetn->d_quant.end())
  {
    return it->second;
  }
  aetn->d_quant[t] = q;
  return q;
}

Node AlphaEquivalenceDb::addTerm(Node q)
{
  Assert(q.getKind() == FORALL);
  Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
  //construct canonical quantified formula
  Node t = d_tc->getCanonicalTerm(q[1], d_sortCommutativeOpChildren);
  Trace("aeq") << "  canonical form: " << t << std::endl;
  return addTermToTypeTrie(t, q);
}

Node AlphaEquivalenceDb::addTermWithSubstitution(Node q,
                                                 std::vector<Node>& vars,
                                                 std::vector<Node>& subs)
{
  Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
  // construct canonical quantified formula with visited cache
  std::map<TNode, Node> visited;
  Node t = d_tc->getCanonicalTerm(q[1], visited, d_sortCommutativeOpChildren);
  // only need to store BOUND_VARIABLE in substitution
  std::map<Node, TNode>& bm = d_bvmap[q];
  for (const std::pair<const TNode, Node>& b : visited)
  {
    if (b.first.getKind() == BOUND_VARIABLE)
    {
      Assert(b.second.getKind() == BOUND_VARIABLE);
      bm[b.second] = b.first;
    }
  }
  Node qret = addTermToTypeTrie(t, q);
  if (qret != q)
  {
    Assert(d_bvmap.find(qret) != d_bvmap.end());
    std::map<Node, TNode>& bmr = d_bvmap[qret];
    std::map<Node, TNode>::iterator itb;
    for (const std::pair<const Node, TNode>& b : bmr)
    {
      itb = bm.find(b.first);
      if (itb == bm.end())
      {
        // didn't use the same variables, fail
        vars.clear();
        subs.clear();
        break;
      }
      // otherwise, we map the variable in the returned quantified formula
      // to the variable that used the same canonical variable
      vars.push_back(b.second);
      subs.push_back(itb->second);
    }
  }
  return qret;
}

Node AlphaEquivalenceDb::addTermToTypeTrie(Node t, Node q)
{
  //compute variable type counts
  std::map<TypeNode, size_t> typCount;
  std::vector< TypeNode > typs;
  for (const Node& v : q[0])
  {
    TypeNode tn = v.getType();
    typCount[tn]++;
    if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){
      typs.push_back( tn );
    }
  }
  sortTypeOrder sto;
  sto.d_tu = d_tc;
  std::sort( typs.begin(), typs.end(), sto );
  Trace("aeq-debug") << "  ";
  Node ret = d_ae_typ_trie.registerNode(q, t, typs, typCount);
  Trace("aeq") << "  ...result : " << ret << std::endl;
  return ret;
}

AlphaEquivalence::AlphaEquivalence(Env& env)
    : EnvObj(env),
      d_termCanon(),
      d_aedb(&d_termCanon, true),
      d_pnm(env.getProofNodeManager()),
      d_pfAlpha(d_pnm ? new EagerProofGenerator(d_pnm) : nullptr)
{
}

TrustNode AlphaEquivalence::reduceQuantifier(Node q)
{
  Assert(q.getKind() == FORALL);
  Node ret;
  std::vector<Node> vars;
  std::vector<Node> subs;
  if (isProofEnabled())
  {
    ret = d_aedb.addTermWithSubstitution(q, vars, subs);
  }
  else
  {
    ret = d_aedb.addTerm(q);
  }
  if (ret == q)
  {
    return TrustNode::null();
  }
  Node lem;
  ProofGenerator* pg = nullptr;
  // lemma ( q <=> d_quant )
  // Notice that we infer this equivalence regardless of whether q or ret
  // have annotations (e.g. user patterns, names, etc.).
  Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
  Trace("alpha-eq") << "  " << q << std::endl;
  Trace("alpha-eq") << "  " << ret << std::endl;
  lem = ret.eqNode(q);
  if (q.getNumChildren() == 3)
  {
    Notice() << "Ignoring annotated quantified formula based on alpha "
                "equivalence: "
             << q << std::endl;
  }
  // if successfully computed the substitution above
  if (isProofEnabled() && !vars.empty())
  {
    std::vector<Node> pfArgs;
    pfArgs.push_back(ret);
    for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
    {
      pfArgs.push_back(vars[i].eqNode(subs[i]));
      Trace("alpha-eq") << "subs: " << vars[i] << " -> " << subs[i]
                        << std::endl;
    }
    CDProof cdp(d_pnm);
    Node sret =
        ret.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
    std::vector<Node> transEq;
    Node eq = ret.eqNode(sret);
    transEq.push_back(eq);
    // ---------- ALPHA_EQUIV
    // ret = sret
    cdp.addStep(eq, PfRule::ALPHA_EQUIV, {}, pfArgs);
    // if not syntactically equal, maybe it can be transformed
    bool success = false;
    if (sret == q)
    {
      success = true;
    }
    else
    {
      Node eq2 = sret.eqNode(q);
      transEq.push_back(eq2);
      Node eq2r = extendedRewrite(eq2);
      if (eq2r.isConst() && eq2r.getConst<bool>())
      {
        // ---------- MACRO_SR_PRED_INTRO
        // sret = q
        std::vector<Node> pfArgs2;
        pfArgs2.push_back(eq2);
        addMethodIds(pfArgs2,
                     MethodId::SB_DEFAULT,
                     MethodId::SBA_SEQUENTIAL,
                     MethodId::RW_EXT_REWRITE);
        cdp.addStep(eq2, PfRule::MACRO_SR_PRED_INTRO, {}, pfArgs2);
        success = true;
      }
    }
    // if successful, store the proof and remember the proof generator
    if (success)
    {
      if (transEq.size() > 1)
      {
        // TRANS of ALPHA_EQ and MACRO_SR_PRED_INTRO steps from above
        cdp.addStep(lem, PfRule::TRANS, transEq, {});
      }
      std::shared_ptr<ProofNode> pn = cdp.getProofFor(lem);
      Trace("alpha-eq") << "Proof is " << *pn.get() << std::endl;
      d_pfAlpha->setProofFor(lem, pn);
      pg = d_pfAlpha.get();
    }
  }
  return TrustNode::mkTrustLemma(lem, pg);
}

bool AlphaEquivalence::isProofEnabled() const { return d_pfAlpha != nullptr; }

}  // namespace quantifiers
}  // namespace theory
}  // 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		* Alpha equivalence checking.
14		*/
15
16		#include "theory/quantifiers/alpha_equivalence.h"
17
18		#include "proof/method_id.h"
19		#include "proof/proof.h"
20		#include "proof/proof_node.h"
21
22		using namespace cvc5::kind;
23
24		namespace cvc5 {
25		namespace theory {
26		namespace quantifiers {
27
28		struct sortTypeOrder {
29		expr::TermCanonize* d_tu;
30	8484	bool operator() (TypeNode i, TypeNode j) {
31	8484	return d_tu->getIdForType( i )<d_tu->getIdForType( j );
32		}
33		};
34
35	11289	Node AlphaEquivalenceTypeNode::registerNode(
36		Node q,
37		Node t,
38		std::vector<TypeNode>& typs,
39		std::map<TypeNode, size_t>& typCount)
40		{
41	11289	AlphaEquivalenceTypeNode* aetn = this;
42	11289	size_t index = 0;
43	44337	while (index < typs.size())
44		{
45	33048	TypeNode curr = typs[index];
46	16524	Assert(typCount.find(curr) != typCount.end());
47	16524	Trace("aeq-debug") << "[" << curr << " " << typCount[curr] << "] ";
48	33048	std::pair<TypeNode, size_t> key(curr, typCount[curr]);
49	16524	aetn = &(aetn->d_children[key]);
50	16524	index = index + 1;
51		}
52	11289	Trace("aeq-debug") << " : ";
53	11289	std::map<Node, Node>::iterator it = aetn->d_quant.find(t);
54	11289	if (it != aetn->d_quant.end())
55		{
56	757	return it->second;
57		}
58	10532	aetn->d_quant[t] = q;
59	10532	return q;
60		}
61
62	11246	Node AlphaEquivalenceDb::addTerm(Node q)
63		{
64	11246	Assert(q.getKind() == FORALL);
65	11246	Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
66		//construct canonical quantified formula
67	22492	Node t = d_tc->getCanonicalTerm(q[1], d_sortCommutativeOpChildren);
68	11246	Trace("aeq") << " canonical form: " << t << std::endl;
69	22492	return addTermToTypeTrie(t, q);
70		}
71
72	43	Node AlphaEquivalenceDb::addTermWithSubstitution(Node q,
73		std::vector<Node>& vars,
74		std::vector<Node>& subs)
75		{
76	43	Trace("aeq") << "Alpha equivalence : register " << q << std::endl;
77		// construct canonical quantified formula with visited cache
78	86	std::map<TNode, Node> visited;
79	86	Node t = d_tc->getCanonicalTerm(q[1], visited, d_sortCommutativeOpChildren);
80		// only need to store BOUND_VARIABLE in substitution
81	43	std::map<Node, TNode>& bm = d_bvmap[q];
82	781	for (const std::pair<const TNode, Node>& b : visited)
83		{
84	738	if (b.first.getKind() == BOUND_VARIABLE)
85		{
86	80	Assert(b.second.getKind() == BOUND_VARIABLE);
87	80	bm[b.second] = b.first;
88		}
89		}
90	43	Node qret = addTermToTypeTrie(t, q);
91	43	if (qret != q)
92		{
93		Assert(d_bvmap.find(qret) != d_bvmap.end());
94		std::map<Node, TNode>& bmr = d_bvmap[qret];
95		std::map<Node, TNode>::iterator itb;
96		for (const std::pair<const Node, TNode>& b : bmr)
97		{
98		itb = bm.find(b.first);
99		if (itb == bm.end())
100		{
101		// didn't use the same variables, fail
102		vars.clear();
103		subs.clear();
104		break;
105		}
106		// otherwise, we map the variable in the returned quantified formula
107		// to the variable that used the same canonical variable
108		vars.push_back(b.second);
109		subs.push_back(itb->second);
110		}
111		}
112	86	return qret;
113		}
114
115	11289	Node AlphaEquivalenceDb::addTermToTypeTrie(Node t, Node q)
116		{
117		//compute variable type counts
118	22578	std::map<TypeNode, size_t> typCount;
119	22578	std::vector< TypeNode > typs;
120	36501	for (const Node& v : q[0])
121		{
122	50424	TypeNode tn = v.getType();
123	25212	typCount[tn]++;
124	25212	if( std::find( typs.begin(), typs.end(), tn )==typs.end() ){
125	16524	typs.push_back( tn );
126		}
127		}
128		sortTypeOrder sto;
129	11289	sto.d_tu = d_tc;
130	11289	std::sort( typs.begin(), typs.end(), sto );
131	11289	Trace("aeq-debug") << " ";
132	11289	Node ret = d_ae_typ_trie.registerNode(q, t, typs, typCount);
133	11289	Trace("aeq") << " ...result : " << ret << std::endl;
134	22578	return ret;
135		}
136
137	4769	AlphaEquivalence::AlphaEquivalence(Env& env)
138		: EnvObj(env),
139		d_termCanon(),
140		d_aedb(&d_termCanon, true),
141	4769	d_pnm(env.getProofNodeManager()),
142	9538	d_pfAlpha(d_pnm ? new EagerProofGenerator(d_pnm) : nullptr)
143		{
144	4769	}
145
146	11289	TrustNode AlphaEquivalence::reduceQuantifier(Node q)
147		{
148	11289	Assert(q.getKind() == FORALL);
149	22578	Node ret;
150	22578	std::vector<Node> vars;
151	22578	std::vector<Node> subs;
152	11289	if (isProofEnabled())
153		{
154	43	ret = d_aedb.addTermWithSubstitution(q, vars, subs);
155		}
156		else
157		{
158	11246	ret = d_aedb.addTerm(q);
159		}
160	11289	if (ret == q)
161		{
162	10553	return TrustNode::null();
163		}
164	1472	Node lem;
165	736	ProofGenerator* pg = nullptr;
166		// lemma ( q <=> d_quant )
167		// Notice that we infer this equivalence regardless of whether q or ret
168		// have annotations (e.g. user patterns, names, etc.).
169	736	Trace("alpha-eq") << "Alpha equivalent : " << std::endl;
170	736	Trace("alpha-eq") << " " << q << std::endl;
171	736	Trace("alpha-eq") << " " << ret << std::endl;
172	736	lem = ret.eqNode(q);
173	736	if (q.getNumChildren() == 3)
174		{
175	25	Notice() << "Ignoring annotated quantified formula based on alpha "
176		"equivalence: "
177		<< q << std::endl;
178		}
179		// if successfully computed the substitution above
180	736	if (isProofEnabled() && !vars.empty())
181		{
182		std::vector<Node> pfArgs;
183		pfArgs.push_back(ret);
184		for (size_t i = 0, nvars = vars.size(); i < nvars; i++)
185		{
186		pfArgs.push_back(vars[i].eqNode(subs[i]));
187		Trace("alpha-eq") << "subs: " << vars[i] << " -> " << subs[i]
188		<< std::endl;
189		}
190		CDProof cdp(d_pnm);
191		Node sret =
192		ret.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
193		std::vector<Node> transEq;
194		Node eq = ret.eqNode(sret);
195		transEq.push_back(eq);
196		// ---------- ALPHA_EQUIV
197		// ret = sret
198		cdp.addStep(eq, PfRule::ALPHA_EQUIV, {}, pfArgs);
199		// if not syntactically equal, maybe it can be transformed
200		bool success = false;
201		if (sret == q)
202		{
203		success = true;
204		}
205		else
206		{
207		Node eq2 = sret.eqNode(q);
208		transEq.push_back(eq2);
209		Node eq2r = extendedRewrite(eq2);
210		if (eq2r.isConst() && eq2r.getConst<bool>())
211		{
212		// ---------- MACRO_SR_PRED_INTRO
213		// sret = q
214		std::vector<Node> pfArgs2;
215		pfArgs2.push_back(eq2);
216		addMethodIds(pfArgs2,
217		MethodId::SB_DEFAULT,
218		MethodId::SBA_SEQUENTIAL,
219		MethodId::RW_EXT_REWRITE);
220		cdp.addStep(eq2, PfRule::MACRO_SR_PRED_INTRO, {}, pfArgs2);
221		success = true;
222		}
223		}
224		// if successful, store the proof and remember the proof generator
225		if (success)
226		{
227		if (transEq.size() > 1)
228		{
229		// TRANS of ALPHA_EQ and MACRO_SR_PRED_INTRO steps from above
230		cdp.addStep(lem, PfRule::TRANS, transEq, {});
231		}
232		std::shared_ptr<ProofNode> pn = cdp.getProofFor(lem);
233		Trace("alpha-eq") << "Proof is " << *pn.get() << std::endl;
234		d_pfAlpha->setProofFor(lem, pn);
235		pg = d_pfAlpha.get();
236		}
237		}
238	736	return TrustNode::mkTrustLemma(lem, pg);
239		}
240
241	12025	bool AlphaEquivalence::isProofEnabled() const { return d_pfAlpha != nullptr; }
242
243		} // namespace quantifiers
244		} // namespace theory
245	22755	} // namespace cvc5