Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_invariance.cpp	Lines:	111	138	80.4 %
Date:	2021-08-15	Branches:	203	530	38.3 %


/******************************************************************************
 * 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;
}

Node EvalSygusInvarianceTest::doEvaluateWithUnfolding(TermDbSygus* tds, Node n)
{
  return tds->evaluateWithUnfolding(n, d_visited);
}

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