Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_invariance.cpp	Lines:	119	136	87.5 %
Date:	2021-09-13	Branches:	223	528	42.2 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, 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 techniques for sygus invariance tests.
 */

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

#include "theory/quantifiers/sygus/sygus_pbe.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include "theory/quantifiers/sygus/term_database_sygus.h"
#include "theory/rewriter.h"

using namespace cvc5::kind;
using namespace std;

namespace cvc5 {
namespace theory {
namespace quantifiers {

void EvalSygusInvarianceTest::init(Node conj, Node var, Node res)
{
  d_terms.clear();
  // simple miniscope
  if ((conj.getKind() == AND || conj.getKind() == OR) && res.isConst())
  {
    for (const Node& c : conj)
    {
      d_terms.push_back(c);
    }
    d_kind = conj.getKind();
    d_is_conjunctive = res.getConst<bool>() == (d_kind == AND);
  }
  else
  {
    d_terms.push_back(conj);
    d_is_conjunctive = true;
  }
  d_var = var;
  d_result = res;
}

bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
{
  TNode tnvn = nvn;
  std::unordered_map<TNode, TNode> cache;
  for (const Node& c : d_terms)
  {
    Node conj_subs = c.substitute(d_var, tnvn, cache);
    Node conj_subs_unfold = tds->rewriteNode(conj_subs);
    Trace("sygus-cref-eval2-debug")
        << "  ...check unfolding : " << conj_subs_unfold << std::endl;
    Trace("sygus-cref-eval2-debug")
        << "  ......from : " << conj_subs << std::endl;
    if (conj_subs_unfold != d_result)
    {
      if (d_is_conjunctive)
      {
        // ti /--> true  implies and( t1, ..., tn ) /--> true, where "/-->" is
        // "does not evaluate to".
        return false;
      }
    }
    else if (!d_is_conjunctive)
    {
      // ti --> true  implies or( t1, ..., tn ) --> true
      return true;
    }
    Trace("sygus-cref-eval2") << "Evaluation min explain : " << conj_subs
                              << " still evaluates to " << d_result
                              << " regardless of ";
    Trace("sygus-cref-eval2") << x << std::endl;
  }
  return d_is_conjunctive;
}

void EquivSygusInvarianceTest::init(
    TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr)
{
  // compute the current examples
  d_bvr = bvr;
  Assert(tds != nullptr);
  if (aconj != nullptr)
  {
    ExampleEvalCache* eec = aconj->getExampleEvalCache(e);
    if (eec != nullptr)
    {
      // get the result of evaluating bvr on the examples of enumerator e.
      eec->evaluateVec(bvr, d_exo, false);
      d_conj = aconj;
      d_enum = e;
    }
  }
}

bool EquivSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
{
  TypeNode tn = nvn.getType();
  Node nbv = tds->sygusToBuiltin(nvn, tn);
  Node nbvr = Rewriter::callExtendedRewrite(nbv);
  Trace("sygus-sb-mexp-debug") << "  min-exp check : " << nbv << " -> " << nbvr
                               << std::endl;
  bool exc_arg = false;
  // equivalent / singular up to normalization
  if (nbvr == d_bvr)
  {
    // gives the same result : then the explanation for the child is irrelevant
    exc_arg = true;
    Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
                           << " is rewritten to " << nbvr;
    Trace("sygus-sb-mexp") << " regardless of the content of "
                           << tds->sygusToBuiltin(x) << std::endl;
  }
  else
  {
    if (nbvr.isVar())
    {
      TypeNode xtn = x.getType();
      if (xtn == tn)
      {
        Node bx = tds->sygusToBuiltin(x, xtn);
        Assert(bx.getType() == nbvr.getType());
        if (nbvr == bx)
        {
          Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
                                 << " always rewrites to argument " << nbvr
                                 << std::endl;
          // rewrites to the variable : then the explanation of this is
          // irrelevant as well
          exc_arg = true;
          d_bvr = nbvr;
        }
      }
    }
  }
  // equivalent under examples
  if (!exc_arg)
  {
    if (!d_enum.isNull())
    {
      bool ex_equiv = true;
      ExampleEvalCache* eec = d_conj->getExampleEvalCache(d_enum);
      Assert(eec != nullptr);
      for (unsigned j = 0, esize = d_exo.size(); j < esize; j++)
      {
        Node nbvr_ex = eec->evaluate(nbvr, j);
        if (nbvr_ex != d_exo[j])
        {
          ex_equiv = false;
          break;
        }
      }
      if (ex_equiv)
      {
        Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn);
        Trace("sygus-sb-mexp")
            << " is the same w.r.t. examples regardless of the content of "
            << tds->sygusToBuiltin(x) << std::endl;
        exc_arg = true;
      }
    }
  }
  return exc_arg;
}

bool DivByZeroSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
{
  TypeNode tn = nvn.getType();
  Node nbv = tds->sygusToBuiltin(nvn, tn);
  Node nbvr = Rewriter::callExtendedRewrite(nbv);
  if (tds->involvesDivByZero(nbvr))
  {
    Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
                           << " involves div-by-zero regardless of "
                           << tds->sygusToBuiltin(x) << std::endl;
    return true;
  }
  return false;
}

void NegContainsSygusInvarianceTest::init(Node e,
                                          std::vector<std::vector<Node> >& ex,
                                          std::vector<Node>& exo,
                                          std::vector<unsigned>& ncind)
{
  Assert(ex.size() == exo.size());
  d_enum = e;
  d_ex.insert(d_ex.end(), ex.begin(), ex.end());
  d_exo.insert(d_exo.end(), exo.begin(), exo.end());
  d_neg_con_indices.insert(d_neg_con_indices.end(), ncind.begin(), ncind.end());
}

bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds,
                                               Node nvn,
                                               Node x)
{
  if (!d_enum.isNull())
  {
    TypeNode tn = nvn.getType();
    Node nbv = tds->sygusToBuiltin(nvn, tn);
    Node nbvr = Rewriter::callExtendedRewrite(nbv);
    // if for any of the examples, it is not contained, then we can exclude
    for (unsigned i = 0; i < d_neg_con_indices.size(); i++)
    {
      unsigned ii = d_neg_con_indices[i];
      Assert(ii < d_exo.size());
      Node nbvre = tds->evaluateBuiltin(tn, nbvr, d_ex[ii]);
      Node out = d_exo[ii];
      Node cont =
          NodeManager::currentNM()->mkNode(kind::STRING_CONTAINS, out, nbvre);
      Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl;
      Node contr = Rewriter::rewrite(cont);
      if (!contr.isConst())
      {
        if (d_isUniversal)
        {
          return false;
        }
      }
      else if (contr.getConst<bool>() == d_isUniversal)
      {
        if (Trace.isOn("sygus-pbe-cterm"))
        {
          Trace("sygus-pbe-cterm")
              << "PBE-cterm : enumerator : do not consider ";
          Trace("sygus-pbe-cterm")
              << nbv << " for any " << tds->sygusToBuiltin(x) << " since "
              << std::endl;
          Trace("sygus-pbe-cterm") << "   PBE-cterm :    for input example : ";
          for (unsigned j = 0, size = d_ex[ii].size(); j < size; j++)
          {
            Trace("sygus-pbe-cterm") << d_ex[ii][j] << " ";
          }
          Trace("sygus-pbe-cterm") << std::endl;
          Trace("sygus-pbe-cterm")
              << "   PBE-cterm :     this rewrites to : " << nbvre << std::endl;
          Trace("sygus-pbe-cterm")
              << "   PBE-cterm : and is not in output : " << out << std::endl;
        }
        return !d_isUniversal;
      }
      Trace("sygus-pbe-cterm-debug2")
          << "...check failed, rewrites to : " << contr << std::endl;
    }
  }
  return d_isUniversal;
}

}  // 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, Mathias Preiner, 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 techniques for sygus invariance tests.
14		*/
15
16		#include "theory/quantifiers/sygus/sygus_invariance.h"
17
18		#include "theory/quantifiers/sygus/sygus_pbe.h"
19		#include "theory/quantifiers/sygus/synth_conjecture.h"
20		#include "theory/quantifiers/sygus/term_database_sygus.h"
21		#include "theory/rewriter.h"
22
23		using namespace cvc5::kind;
24		using namespace std;
25
26		namespace cvc5 {
27		namespace theory {
28		namespace quantifiers {
29
30	13701	void EvalSygusInvarianceTest::init(Node conj, Node var, Node res)
31		{
32	13701	d_terms.clear();
33		// simple miniscope
34	13701	if ((conj.getKind() == AND \|\| conj.getKind() == OR) && res.isConst())
35		{
36	819	for (const Node& c : conj)
37		{
38	546	d_terms.push_back(c);
39		}
40	273	d_kind = conj.getKind();
41	273	d_is_conjunctive = res.getConst<bool>() == (d_kind == AND);
42		}
43		else
44		{
45	13428	d_terms.push_back(conj);
46	13428	d_is_conjunctive = true;
47		}
48	13701	d_var = var;
49	13701	d_result = res;
50	13701	}
51
52	44301	bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
53		{
54	88602	TNode tnvn = nvn;
55	88602	std::unordered_map<TNode, TNode> cache;
56	48349	for (const Node& c : d_terms)
57		{
58	48606	Node conj_subs = c.substitute(d_var, tnvn, cache);
59	48606	Node conj_subs_unfold = tds->rewriteNode(conj_subs);
60	89116	Trace("sygus-cref-eval2-debug")
61	44558	<< " ...check unfolding : " << conj_subs_unfold << std::endl;
62	89116	Trace("sygus-cref-eval2-debug")
63	44558	<< " ......from : " << conj_subs << std::endl;
64	44558	if (conj_subs_unfold != d_result)
65		{
66	40510	if (d_is_conjunctive)
67		{
68		// ti /--> true implies and( t1, ..., tn ) /--> true, where "/-->" is
69		// "does not evaluate to".
70	40510	return false;
71		}
72		}
73	4048	else if (!d_is_conjunctive)
74		{
75		// ti --> true implies or( t1, ..., tn ) --> true
76		return true;
77		}
78	8096	Trace("sygus-cref-eval2") << "Evaluation min explain : " << conj_subs
79	4048	<< " still evaluates to " << d_result
80	4048	<< " regardless of ";
81	4048	Trace("sygus-cref-eval2") << x << std::endl;
82		}
83	3791	return d_is_conjunctive;
84		}
85
86	1647	void EquivSygusInvarianceTest::init(
87		TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr)
88		{
89		// compute the current examples
90	1647	d_bvr = bvr;
91	1647	Assert(tds != nullptr);
92	1647	if (aconj != nullptr)
93		{
94	1647	ExampleEvalCache* eec = aconj->getExampleEvalCache(e);
95	1647	if (eec != nullptr)
96		{
97		// get the result of evaluating bvr on the examples of enumerator e.
98	121	eec->evaluateVec(bvr, d_exo, false);
99	121	d_conj = aconj;
100	121	d_enum = e;
101		}
102		}
103	1647	}
104
105	5607	bool EquivSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
106		{
107	11214	TypeNode tn = nvn.getType();
108	11214	Node nbv = tds->sygusToBuiltin(nvn, tn);
109	11214	Node nbvr = Rewriter::callExtendedRewrite(nbv);
110	11214	Trace("sygus-sb-mexp-debug") << " min-exp check : " << nbv << " -> " << nbvr
111	5607	<< std::endl;
112	5607	bool exc_arg = false;
113		// equivalent / singular up to normalization
114	5607	if (nbvr == d_bvr)
115		{
116		// gives the same result : then the explanation for the child is irrelevant
117	79	exc_arg = true;
118	158	Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
119	79	<< " is rewritten to " << nbvr;
120	158	Trace("sygus-sb-mexp") << " regardless of the content of "
121	79	<< tds->sygusToBuiltin(x) << std::endl;
122		}
123		else
124		{
125	5528	if (nbvr.isVar())
126		{
127	452	TypeNode xtn = x.getType();
128	226	if (xtn == tn)
129		{
130	210	Node bx = tds->sygusToBuiltin(x, xtn);
131	105	Assert(bx.getType() == nbvr.getType());
132	105	if (nbvr == bx)
133		{
134	210	Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
135	105	<< " always rewrites to argument " << nbvr
136	105	<< std::endl;
137		// rewrites to the variable : then the explanation of this is
138		// irrelevant as well
139	105	exc_arg = true;
140	105	d_bvr = nbvr;
141		}
142		}
143		}
144		}
145		// equivalent under examples
146	5607	if (!exc_arg)
147		{
148	5423	if (!d_enum.isNull())
149		{
150	381	bool ex_equiv = true;
151	381	ExampleEvalCache* eec = d_conj->getExampleEvalCache(d_enum);
152	381	Assert(eec != nullptr);
153	391	for (unsigned j = 0, esize = d_exo.size(); j < esize; j++)
154		{
155	400	Node nbvr_ex = eec->evaluate(nbvr, j);
156	390	if (nbvr_ex != d_exo[j])
157		{
158	380	ex_equiv = false;
159	380	break;
160		}
161		}
162	381	if (ex_equiv)
163		{
164	1	Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn);
165	2	Trace("sygus-sb-mexp")
166	1	<< " is the same w.r.t. examples regardless of the content of "
167	1	<< tds->sygusToBuiltin(x) << std::endl;
168	1	exc_arg = true;
169		}
170		}
171		}
172	11214	return exc_arg;
173		}
174
175	2	bool DivByZeroSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
176		{
177	4	TypeNode tn = nvn.getType();
178	4	Node nbv = tds->sygusToBuiltin(nvn, tn);
179	4	Node nbvr = Rewriter::callExtendedRewrite(nbv);
180	2	if (tds->involvesDivByZero(nbvr))
181		{
182	2	Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
183	1	<< " involves div-by-zero regardless of "
184	1	<< tds->sygusToBuiltin(x) << std::endl;
185	1	return true;
186		}
187	1	return false;
188		}
189
190	50	void NegContainsSygusInvarianceTest::init(Node e,
191		std::vector<std::vector<Node> >& ex,
192		std::vector<Node>& exo,
193		std::vector<unsigned>& ncind)
194		{
195	50	Assert(ex.size() == exo.size());
196	50	d_enum = e;
197	50	d_ex.insert(d_ex.end(), ex.begin(), ex.end());
198	50	d_exo.insert(d_exo.end(), exo.begin(), exo.end());
199	50	d_neg_con_indices.insert(d_neg_con_indices.end(), ncind.begin(), ncind.end());
200	50	}
201
202	65	bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds,
203		Node nvn,
204		Node x)
205		{
206	65	if (!d_enum.isNull())
207		{
208	127	TypeNode tn = nvn.getType();
209	127	Node nbv = tds->sygusToBuiltin(nvn, tn);
210	127	Node nbvr = Rewriter::callExtendedRewrite(nbv);
211		// if for any of the examples, it is not contained, then we can exclude
212	5967	for (unsigned i = 0; i < d_neg_con_indices.size(); i++)
213		{
214	5905	unsigned ii = d_neg_con_indices[i];
215	5905	Assert(ii < d_exo.size());
216	11807	Node nbvre = tds->evaluateBuiltin(tn, nbvr, d_ex[ii]);
217	11807	Node out = d_exo[ii];
218		Node cont =
219	11807	NodeManager::currentNM()->mkNode(kind::STRING_CONTAINS, out, nbvre);
220	5905	Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl;
221	11807	Node contr = Rewriter::rewrite(cont);
222	5905	if (!contr.isConst())
223		{
224	5905	if (d_isUniversal)
225		{
226	3	return false;
227		}
228		}
229		else if (contr.getConst<bool>() == d_isUniversal)
230		{
231		if (Trace.isOn("sygus-pbe-cterm"))
232		{
233		Trace("sygus-pbe-cterm")
234		<< "PBE-cterm : enumerator : do not consider ";
235		Trace("sygus-pbe-cterm")
236		<< nbv << " for any " << tds->sygusToBuiltin(x) << " since "
237		<< std::endl;
238		Trace("sygus-pbe-cterm") << " PBE-cterm : for input example : ";
239		for (unsigned j = 0, size = d_ex[ii].size(); j < size; j++)
240		{
241		Trace("sygus-pbe-cterm") << d_ex[ii][j] << " ";
242		}
243		Trace("sygus-pbe-cterm") << std::endl;
244		Trace("sygus-pbe-cterm")
245		<< " PBE-cterm : this rewrites to : " << nbvre << std::endl;
246		Trace("sygus-pbe-cterm")
247		<< " PBE-cterm : and is not in output : " << out << std::endl;
248		}
249		return !d_isUniversal;
250		}
251	11804	Trace("sygus-pbe-cterm-debug2")
252	5902	<< "...check failed, rewrites to : " << contr << std::endl;
253		}
254		}
255	62	return d_isUniversal;
256		}
257
258		} // namespace quantifiers
259		} // namespace theory
260	29514	} // namespace cvc5