Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_grammar_red.cpp	Lines:	77	79	97.5 %
Date:	2021-09-30	Branches:	171	380	45.0 %


/******************************************************************************
 * 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 sygus_grammar_red.
 */

#include "theory/quantifiers/sygus/sygus_grammar_red.h"

#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/sygus_datatype.h"
#include "options/quantifiers_options.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"

using namespace std;
using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace quantifiers {

void SygusRedundantCons::initialize(TermDbSygus* tds, TypeNode tn)
{
  Assert(tds != nullptr);
  Trace("sygus-red") << "Compute redundant cons for " << tn << std::endl;
  d_type = tn;
  Assert(tn.isDatatype());
  tds->registerSygusType(tn);
  const DType& dt = tn.getDType();
  Assert(dt.isSygus());
  TypeNode btn = dt.getSygusType();
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
  {
    Trace("sygus-red") << "  Is " << dt[i].getName() << " a redundant operator?"
                       << std::endl;
    Node sop = dt[i].getSygusOp();
    if (sop.getAttribute(SygusAnyConstAttribute()))
    {
      // the any constant constructor is never redundant
      d_sygus_red_status.push_back(0);
      continue;
    }
    std::map<int, Node> pre;
    // We do not do beta reduction, since we want the arguments to match the
    // the types of the datatype.
    Node g = tds->mkGeneric(dt, i, pre, false);
    Trace("sygus-red-debug") << "  ...pre-rewrite : " << g << std::endl;
    d_gen_terms[i] = g;
    // is the operator a lambda of the form (lambda x1...xn. f(x1...xn))?
    bool lamInOrder = false;
    if (sop.getKind() == LAMBDA && sop[0].getNumChildren() == sop[1].getNumChildren())
    {
      Assert(g.getNumChildren()==sop[0].getNumChildren());
      lamInOrder = true;
      for (size_t j = 0, nchild = sop[1].getNumChildren(); j < nchild; j++)
      {
        if (sop[0][j] != sop[1][j])
        {
          // arguments not in order
          lamInOrder = false;
          break;
        }
      }
    }
    // a list of variants of the generic term (see getGenericList).
    std::vector<Node> glist;
    if (lamInOrder)
    {
      // If it is a lambda whose arguments are one-to-one with the datatype
      // arguments, then we can add variants of this operator by permuting
      // the argument list (see getGenericList).
      Assert(g.getNumChildren()==dt[i].getNumArgs());
      for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
      {
        pre[j] = g[j];
      }
      getGenericList(tds, dt, i, 0, pre, glist);
    }
    else
    {
      // It is a builtin (possibly) ground term. Its children do not correspond
      // one-to-one with the arugments of the constructor. Hence, we consider
      // only g itself as a variant.
      glist.push_back(g);
    }
    // call the extended rewriter
    bool red = false;
    for (const Node& gr : glist)
    {
      Trace("sygus-red-debug") << "  ...variant : " << gr << std::endl;
      std::map<Node, unsigned>::iterator itg = d_gen_cons.find(gr);
      if (itg != d_gen_cons.end() && itg->second != i)
      {
        red = true;
        Trace("sygus-red") << "  ......redundant, since a variant of " << g
                           << " and " << d_gen_terms[itg->second]
                           << " both rewrite to " << gr << std::endl;
        break;
      }
      else
      {
        d_gen_cons[gr] = i;
        Trace("sygus-red") << "  ......not redundant." << std::endl;
      }
    }
    d_sygus_red_status.push_back(red ? 1 : 0);
  }
  Trace("sygus-red") << "Compute redundant cons for " << tn << " finished"
                     << std::endl;
}

void SygusRedundantCons::getRedundant(std::vector<unsigned>& indices)
{
  const DType& dt = d_type.getDType();
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
  {
    if (isRedundant(i))
    {
      indices.push_back(i);
    }
  }
}

bool SygusRedundantCons::isRedundant(unsigned i)
{
  Assert(i < d_sygus_red_status.size());
  return d_sygus_red_status[i] == 1;
}

void SygusRedundantCons::getGenericList(TermDbSygus* tds,
                                        const DType& dt,
                                        unsigned c,
                                        unsigned index,
                                        std::map<int, Node>& pre,
                                        std::vector<Node>& terms)
{
  if (index == dt[c].getNumArgs())
  {
    Node gt = tds->mkGeneric(dt, c, pre);
    gt = Rewriter::callExtendedRewrite(gt);
    terms.push_back(gt);
    return;
  }
  // with no swap
  getGenericList(tds, dt, c, index + 1, pre, terms);
  // swapping is exponential, only use for operators with small # args.
  if (dt[c].getNumArgs() <= 5)
  {
    TypeNode atype = tds->getArgType(dt[c], index);
    for (unsigned s = index + 1, nargs = dt[c].getNumArgs(); s < nargs; s++)
    {
      if (tds->getArgType(dt[c], s) == atype)
      {
        // swap s and index
        Node tmp = pre[s];
        pre[s] = pre[index];
        pre[index] = tmp;
        getGenericList(tds, dt, c, index + 1, pre, terms);
        // revert
        tmp = pre[s];
        pre[s] = pre[index];
        pre[index] = tmp;
      }
    }
  }
}

}  // 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		* Implementation of sygus_grammar_red.
14		*/
15
16		#include "theory/quantifiers/sygus/sygus_grammar_red.h"
17
18		#include "expr/dtype.h"
19		#include "expr/dtype_cons.h"
20		#include "expr/sygus_datatype.h"
21		#include "options/quantifiers_options.h"
22		#include "theory/quantifiers/sygus/term_database_sygus.h"
23		#include "theory/quantifiers/term_util.h"
24		#include "theory/rewriter.h"
25
26		using namespace std;
27		using namespace cvc5::kind;
28
29		namespace cvc5 {
30		namespace theory {
31		namespace quantifiers {
32
33	446	void SygusRedundantCons::initialize(TermDbSygus* tds, TypeNode tn)
34		{
35	446	Assert(tds != nullptr);
36	446	Trace("sygus-red") << "Compute redundant cons for " << tn << std::endl;
37	446	d_type = tn;
38	446	Assert(tn.isDatatype());
39	446	tds->registerSygusType(tn);
40	446	const DType& dt = tn.getDType();
41	446	Assert(dt.isSygus());
42	892	TypeNode btn = dt.getSygusType();
43	2605	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
44		{
45	4318	Trace("sygus-red") << " Is " << dt[i].getName() << " a redundant operator?"
46	2159	<< std::endl;
47	4318	Node sop = dt[i].getSygusOp();
48	2159	if (sop.getAttribute(SygusAnyConstAttribute()))
49		{
50		// the any constant constructor is never redundant
51		d_sygus_red_status.push_back(0);
52		continue;
53		}
54	4318	std::map<int, Node> pre;
55		// We do not do beta reduction, since we want the arguments to match the
56		// the types of the datatype.
57	4318	Node g = tds->mkGeneric(dt, i, pre, false);
58	2159	Trace("sygus-red-debug") << " ...pre-rewrite : " << g << std::endl;
59	2159	d_gen_terms[i] = g;
60		// is the operator a lambda of the form (lambda x1...xn. f(x1...xn))?
61	2159	bool lamInOrder = false;
62	2159	if (sop.getKind() == LAMBDA && sop[0].getNumChildren() == sop[1].getNumChildren())
63		{
64	951	Assert(g.getNumChildren()==sop[0].getNumChildren());
65	951	lamInOrder = true;
66	2743	for (size_t j = 0, nchild = sop[1].getNumChildren(); j < nchild; j++)
67		{
68	1798	if (sop[0][j] != sop[1][j])
69		{
70		// arguments not in order
71	6	lamInOrder = false;
72	6	break;
73		}
74		}
75		}
76		// a list of variants of the generic term (see getGenericList).
77	4318	std::vector<Node> glist;
78	2159	if (lamInOrder)
79		{
80		// If it is a lambda whose arguments are one-to-one with the datatype
81		// arguments, then we can add variants of this operator by permuting
82		// the argument list (see getGenericList).
83	945	Assert(g.getNumChildren()==dt[i].getNumArgs());
84	2734	for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
85		{
86	1789	pre[j] = g[j];
87		}
88	945	getGenericList(tds, dt, i, 0, pre, glist);
89		}
90		else
91		{
92		// It is a builtin (possibly) ground term. Its children do not correspond
93		// one-to-one with the arugments of the constructor. Hence, we consider
94		// only g itself as a variant.
95	1214	glist.push_back(g);
96		}
97		// call the extended rewriter
98	2159	bool red = false;
99	5017	for (const Node& gr : glist)
100		{
101	2879	Trace("sygus-red-debug") << " ...variant : " << gr << std::endl;
102	2879	std::map<Node, unsigned>::iterator itg = d_gen_cons.find(gr);
103	2879	if (itg != d_gen_cons.end() && itg->second != i)
104		{
105	21	red = true;
106	42	Trace("sygus-red") << " ......redundant, since a variant of " << g
107	21	<< " and " << d_gen_terms[itg->second]
108	21	<< " both rewrite to " << gr << std::endl;
109	21	break;
110		}
111		else
112		{
113	2858	d_gen_cons[gr] = i;
114	2858	Trace("sygus-red") << " ......not redundant." << std::endl;
115		}
116		}
117	2159	d_sygus_red_status.push_back(red ? 1 : 0);
118		}
119	892	Trace("sygus-red") << "Compute redundant cons for " << tn << " finished"
120	446	<< std::endl;
121	446	}
122
123	446	void SygusRedundantCons::getRedundant(std::vector<unsigned>& indices)
124		{
125	446	const DType& dt = d_type.getDType();
126	2605	for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
127		{
128	2159	if (isRedundant(i))
129		{
130	21	indices.push_back(i);
131		}
132		}
133	446	}
134
135	2159	bool SygusRedundantCons::isRedundant(unsigned i)
136		{
137	2159	Assert(i < d_sygus_red_status.size());
138	2159	return d_sygus_red_status[i] == 1;
139		}
140
141	4287	void SygusRedundantCons::getGenericList(TermDbSygus* tds,
142		const DType& dt,
143		unsigned c,
144		unsigned index,
145		std::map<int, Node>& pre,
146		std::vector<Node>& terms)
147		{
148	4287	if (index == dt[c].getNumArgs())
149		{
150	3368	Node gt = tds->mkGeneric(dt, c, pre);
151	1684	gt = Rewriter::callExtendedRewrite(gt);
152	1684	terms.push_back(gt);
153	1684	return;
154		}
155		// with no swap
156	2603	getGenericList(tds, dt, c, index + 1, pre, terms);
157		// swapping is exponential, only use for operators with small # args.
158	2603	if (dt[c].getNumArgs() <= 5)
159		{
160	5206	TypeNode atype = tds->getArgType(dt[c], index);
161	3654	for (unsigned s = index + 1, nargs = dt[c].getNumArgs(); s < nargs; s++)
162		{
163	1051	if (tds->getArgType(dt[c], s) == atype)
164		{
165		// swap s and index
166	1478	Node tmp = pre[s];
167	739	pre[s] = pre[index];
168	739	pre[index] = tmp;
169	739	getGenericList(tds, dt, c, index + 1, pre, terms);
170		// revert
171	739	tmp = pre[s];
172	739	pre[s] = pre[index];
173	739	pre[index] = tmp;
174		}
175		}
176		}
177		}
178
179		} // namespace quantifiers
180		} // namespace theory
181	22755	} // namespace cvc5