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-05-22	Branches:	171	382	44.8 %


/******************************************************************************
 * 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"

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