Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_invariance.cpp	Lines:	119	136	87.5 %
Date:	2021-11-07	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	35302	void EvalSygusInvarianceTest::init(Node conj, Node var, Node res)
31		{
32	35302	d_terms.clear();
33		// simple miniscope
34	35302	if ((conj.getKind() == AND \|\| conj.getKind() == OR) && res.isConst())
35		{
36	2778	for (const Node& c : conj)
37		{
38	1852	d_terms.push_back(c);
39		}
40	926	d_kind = conj.getKind();
41	926	d_is_conjunctive = res.getConst<bool>() == (d_kind == AND);
42		}
43		else
44		{
45	34376	d_terms.push_back(conj);
46	34376	d_is_conjunctive = true;
47		}
48	35302	d_var = var;
49	35302	d_result = res;
50	35302	}
51
52	127581	bool EvalSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
53		{
54	255162	TNode tnvn = nvn;
55	255162	std::unordered_map<TNode, TNode> cache;
56	137691	for (const Node& c : d_terms)
57		{
58	138553	Node conj_subs = c.substitute(d_var, tnvn, cache);
59	138553	Node conj_subs_unfold = tds->rewriteNode(conj_subs);
60	256886	Trace("sygus-cref-eval2-debug")
61	128443	<< " ...check unfolding : " << conj_subs_unfold << std::endl;
62	256886	Trace("sygus-cref-eval2-debug")
63	128443	<< " ......from : " << conj_subs << std::endl;
64	128443	if (conj_subs_unfold != d_result)
65		{
66	118333	if (d_is_conjunctive)
67		{
68		// ti /--> true implies and( t1, ..., tn ) /--> true, where "/-->" is
69		// "does not evaluate to".
70	118333	return false;
71		}
72		}
73	10110	else if (!d_is_conjunctive)
74		{
75		// ti --> true implies or( t1, ..., tn ) --> true
76		return true;
77		}
78	20220	Trace("sygus-cref-eval2") << "Evaluation min explain : " << conj_subs
79	10110	<< " still evaluates to " << d_result
80	10110	<< " regardless of ";
81	10110	Trace("sygus-cref-eval2") << x << std::endl;
82		}
83	9248	return d_is_conjunctive;
84		}
85
86	4454	void EquivSygusInvarianceTest::init(
87		TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr)
88		{
89		// compute the current examples
90	4454	d_bvr = bvr;
91	4454	Assert(tds != nullptr);
92	4454	if (aconj != nullptr)
93		{
94	4454	ExampleEvalCache* eec = aconj->getExampleEvalCache(e);
95	4454	if (eec != nullptr)
96		{
97		// get the result of evaluating bvr on the examples of enumerator e.
98	930	eec->evaluateVec(bvr, d_exo, false);
99	930	d_conj = aconj;
100	930	d_enum = e;
101		}
102		}
103	4454	}
104
105	15903	bool EquivSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
106		{
107	31806	TypeNode tn = nvn.getType();
108	31806	Node nbv = tds->sygusToBuiltin(nvn, tn);
109	31806	Node nbvr = Rewriter::callExtendedRewrite(nbv);
110	31806	Trace("sygus-sb-mexp-debug") << " min-exp check : " << nbv << " -> " << nbvr
111	15903	<< std::endl;
112	15903	bool exc_arg = false;
113		// equivalent / singular up to normalization
114	15903	if (nbvr == d_bvr)
115		{
116		// gives the same result : then the explanation for the child is irrelevant
117	170	exc_arg = true;
118	340	Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
119	170	<< " is rewritten to " << nbvr;
120	340	Trace("sygus-sb-mexp") << " regardless of the content of "
121	170	<< tds->sygusToBuiltin(x) << std::endl;
122		}
123		else
124		{
125	15733	if (nbvr.isVar())
126		{
127	932	TypeNode xtn = x.getType();
128	466	if (xtn == tn)
129		{
130	436	Node bx = tds->sygusToBuiltin(x, xtn);
131	218	Assert(bx.getType() == nbvr.getType());
132	218	if (nbvr == bx)
133		{
134	436	Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
135	218	<< " always rewrites to argument " << nbvr
136	218	<< std::endl;
137		// rewrites to the variable : then the explanation of this is
138		// irrelevant as well
139	218	exc_arg = true;
140	218	d_bvr = nbvr;
141		}
142		}
143		}
144		}
145		// equivalent under examples
146	15903	if (!exc_arg)
147		{
148	15515	if (!d_enum.isNull())
149		{
150	2828	bool ex_equiv = true;
151	2828	ExampleEvalCache* eec = d_conj->getExampleEvalCache(d_enum);
152	2828	Assert(eec != nullptr);
153	2896	for (unsigned j = 0, esize = d_exo.size(); j < esize; j++)
154		{
155	2954	Node nbvr_ex = eec->evaluate(nbvr, j);
156	2886	if (nbvr_ex != d_exo[j])
157		{
158	2818	ex_equiv = false;
159	2818	break;
160		}
161		}
162	2828	if (ex_equiv)
163		{
164	10	Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn);
165	20	Trace("sygus-sb-mexp")
166	10	<< " is the same w.r.t. examples regardless of the content of "
167	10	<< tds->sygusToBuiltin(x) << std::endl;
168	10	exc_arg = true;
169		}
170		}
171		}
172	31806	return exc_arg;
173		}
174
175	4	bool DivByZeroSygusInvarianceTest::invariant(TermDbSygus* tds, Node nvn, Node x)
176		{
177	8	TypeNode tn = nvn.getType();
178	8	Node nbv = tds->sygusToBuiltin(nvn, tn);
179	8	Node nbvr = Rewriter::callExtendedRewrite(nbv);
180	4	if (tds->involvesDivByZero(nbvr))
181		{
182	4	Trace("sygus-sb-mexp") << "sb-min-exp : " << tds->sygusToBuiltin(nvn)
183	2	<< " involves div-by-zero regardless of "
184	2	<< tds->sygusToBuiltin(x) << std::endl;
185	2	return true;
186		}
187	2	return false;
188		}
189
190	96	void NegContainsSygusInvarianceTest::init(Node e,
191		std::vector<std::vector<Node> >& ex,
192		std::vector<Node>& exo,
193		std::vector<unsigned>& ncind)
194		{
195	96	Assert(ex.size() == exo.size());
196	96	d_enum = e;
197	96	d_ex.insert(d_ex.end(), ex.begin(), ex.end());
198	96	d_exo.insert(d_exo.end(), exo.begin(), exo.end());
199	96	d_neg_con_indices.insert(d_neg_con_indices.end(), ncind.begin(), ncind.end());
200	96	}
201
202	130	bool NegContainsSygusInvarianceTest::invariant(TermDbSygus* tds,
203		Node nvn,
204		Node x)
205		{
206	130	if (!d_enum.isNull())
207		{
208	254	TypeNode tn = nvn.getType();
209	254	Node nbv = tds->sygusToBuiltin(nvn, tn);
210	254	Node nbvr = Rewriter::callExtendedRewrite(nbv);
211		// if for any of the examples, it is not contained, then we can exclude
212	11934	for (unsigned i = 0; i < d_neg_con_indices.size(); i++)
213		{
214	11810	unsigned ii = d_neg_con_indices[i];
215	11810	Assert(ii < d_exo.size());
216	23614	Node nbvre = tds->evaluateBuiltin(tn, nbvr, d_ex[ii]);
217	23614	Node out = d_exo[ii];
218		Node cont =
219	23614	NodeManager::currentNM()->mkNode(kind::STRING_CONTAINS, out, nbvre);
220	11810	Trace("sygus-pbe-cterm-debug") << "Check: " << cont << std::endl;
221	23614	Node contr = Rewriter::rewrite(cont);
222	11810	if (!contr.isConst())
223		{
224	11810	if (d_isUniversal)
225		{
226	6	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	23608	Trace("sygus-pbe-cterm-debug2")
252	11804	<< "...check failed, rewrites to : " << contr << std::endl;
253		}
254		}
255	124	return d_isUniversal;
256		}
257
258		} // namespace quantifiers
259		} // namespace theory
260	31137	} // namespace cvc5