Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_invariance.h	Lines:	20	20	100.0 %
Date:	2021-09-10	Branches:	9	16	56.3 %


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

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H

#include <unordered_map>
#include <vector>

#include "expr/node.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class TermDbSygus;
class SynthConjecture;

/* SygusInvarianceTest
*
* This class is the standard interface for term generalization
* in SyGuS. Its interface is a single function is_variant,
* which is a virtual condition for SyGuS terms.
*
* The common use case of invariance tests is when constructing
* minimal explanations for refinement lemmas in the
* counterexample-guided inductive synthesis (CEGIS) loop.
* See sygus_explain.h for more details.
*/
class SygusInvarianceTest
{
 public:
  virtual ~SygusInvarianceTest() {}

  /** Is nvn invariant with respect to this test ?
   *
   * - nvn is the term to check whether it is invariant.
   * - x is a variable such that the previous call to
   *   is_invariant (if any) was with term nvn_prev, and
   *   nvn is equal to nvn_prev with some subterm
   *   position replaced by x. This is typically used
   *   for debugging only.
   */
  bool is_invariant(TermDbSygus* tds, Node nvn, Node x)
  {
    if (invariant(tds, nvn, x))
    {
      d_update_nvn = nvn;
      return true;
    }
    return false;
  }
  /** get updated term */
  Node getUpdatedTerm() { return d_update_nvn; }
  /** set updated term */
  void setUpdatedTerm(Node n) { d_update_nvn = n; }
 protected:
  /** result of the node that satisfies this invariant */
  Node d_update_nvn;
  /** check whether nvn[ x ] is invariant */
  virtual bool invariant(TermDbSygus* tds, Node nvn, Node x) = 0;
};

/** EquivSygusInvarianceTest
*
* This class tests whether a term evaluates via evaluation
* operators in the deep embedding (Section 4 of Reynolds
* et al. CAV 2015) to fixed term d_result.
*
* For example, consider a SyGuS evaluation function eval
* for a synthesis conjecture with arguments x and y.
* Notice that the term t = (mult x y) is such that:
*   eval( t, 0, 1 ) ----> 0
* This test is invariant on the content of the second
* argument of t, noting that:
*   eval( (mult x _), 0, 1 ) ----> 0
* as well, via a call to EvalSygusInvarianceTest::invariant.
*
* Another example, t = ite( gt( x, y ), x, y ) is such that:
*   eval( t, 2, 3 ) ----> 3
* This test is invariant on the second child of t, noting:
*   eval( ite( gt( x, y ), _, y ), 2, 3 ) ----> 3
*/
class EvalSygusInvarianceTest : public SygusInvarianceTest
{
 public:
  EvalSygusInvarianceTest()
      : d_kind(kind::UNDEFINED_KIND), d_is_conjunctive(false)
  {
  }

  /** initialize this invariance test
   *
   * This sets d_terms/d_var/d_result, where we are checking whether:
   *   <d_kind>(d_terms) { d_var -> n } ----> d_result.
   * for terms n.
   */
  void init(Node conj, Node var, Node res);

 protected:
  /** does d_terms{ d_var -> nvn } still rewrite to d_result? */
  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;

 private:
  /** the formulas we are evaluating */
  std::vector<Node> d_terms;
  /** the variable */
  TNode d_var;
  /** the result of the evaluation */
  Node d_result;
  /** the parent kind we are checking, undefined if size(d_terms) is 1. */
  Kind d_kind;
  /** whether we are conjunctive
   *
   * If this flag is true, then the evaluation tests:
   *   d_terms[1] {d_var -> n} = d_result ... d_term[k] {d_var -> n} = d_result
   * should be processed conjunctively, that is,
   * <d_kind>(d_terms) { d_var -> n } = d_result only if each of the above
   * holds. If this flag is false, then these tests are interpreted
   * disjunctively, i.e. if one child test succeeds, the overall test succeeds.
   */
  bool d_is_conjunctive;
};

/** EquivSygusInvarianceTest
*
* This class tests whether a builtin version of a
* sygus term is equivalent up to rewriting to a RHS value bvr.
*
* For example,
*
* ite( t>0, 0, 0 ) + s*0 ----> 0
*
* This test is invariant on the condition t>0 and s, since:
*
* ite( _, 0, 0 ) + _*0 ----> 0
*
* for any values of _.
*
* It also manages the case where the rewriting is invariant
* wrt a finite set of examples occurring in the conjecture.
* (EX1) : For example if our input examples are:
* (x,y,z) = (3,2,4), (5,2,6), (3,2,1)
* On these examples, we have:
*
* ite( x>y, z, 0) ---> 4,6,1
*
* which is invariant on the second argument:
*
* ite( x>y, z, _) ---> 4,6,1
*
* For details, see Reynolds et al SYNT 2017.
*/
class EquivSygusInvarianceTest : public SygusInvarianceTest
{
 public:
  EquivSygusInvarianceTest() : d_conj(nullptr) {}

  /** initialize this invariance test
   * tn is the sygus type for e
   * aconj/e are used for conjecture-specific symmetry breaking
   * bvr is the builtin version of the right hand side of the rewrite that we
   * are checking for invariance
   */
  void init(
      TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr);

 protected:
  /** checks whether the analog of nvn still rewrites to d_bvr */
  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;

 private:
  /** the conjecture associated with the enumerator d_enum */
  SynthConjecture* d_conj;
  /** the enumerator associated with the term for which this test is for */
  Node d_enum;
  /** the RHS of the evaluation */
  Node d_bvr;
  /** the result of the examples
   * In (EX1), this is (4,6,1)
   */
  std::vector<Node> d_exo;
};

/** DivByZeroSygusInvarianceTest
 *
 * This class tests whether a sygus term involves
 * division by zero.
 *
 * For example the test for:
 *    ( x + ( y/0 )*2 )
 * is invariant on the contents of _ below:
 *    ( _ + ( _/0 )*_ )
 */
class DivByZeroSygusInvarianceTest : public SygusInvarianceTest
{
 public:
  DivByZeroSygusInvarianceTest() {}

 protected:
  /** checks whether nvn involves division by zero. */
  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
};

/** NegContainsSygusInvarianceTest
*
* This class is used to construct a minimal shape of a term that cannot
* be contained in at least one output of an I/O pair.
*
* Say our PBE conjecture is:
*
* exists f.
*   f( "abc" ) = "abc abc" ^
*   f( "de" ) = "de de"
*
* Then, this class is used when there is a candidate solution t[x1]
* such that either:
*   contains( "abc abc", t["abc"] ) ---> false or
*   contains( "de de", t["de"] ) ---> false
*
* It is used to determine whether certain generalizations of t[x1]
* are still sufficient to falsify one of the above containments.
*
* For example:
*
* The test for str.++( x1, "d" ) is invariant on its first argument
*   ...since contains( "abc abc", str.++( _, "d" ) ) ---> false
* The test for str.replace( "de", x1, "b" ) is invariant on its third argument
*   ...since contains( "abc abc", str.replace( "de", "abc", _ ) ) ---> false
*/
class NegContainsSygusInvarianceTest : public SygusInvarianceTest
{
 public:
  NegContainsSygusInvarianceTest() : d_isUniversal(false) {}

  /** initialize this invariance test
   *  e is the enumerator which we are reasoning about (associated with a synth
   *    fun).
   *  ex is the list of inputs,
   *  exo is the list of outputs,
   *  ncind is the set of possible example indices to check invariance of
   *  non-containment.
   *    For example, in the above example, when t[x1] = "ab", then this
   *    has the index 1 since contains("de de", "ab") ---> false but not
   *    the index 0 since contains("abc abc","ab") ---> true.
   */
  void init(Node e,
            std::vector<std::vector<Node> >& ex,
            std::vector<Node>& exo,
            std::vector<unsigned>& ncind);
  /** set universal
   *
   * This updates the semantics of this check such that *all* instead of some
   * examples must fail the containment test.
   */
  void setUniversal() { d_isUniversal = true; }

 protected:
  /**
   * Checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i; if
   * d_isUniversal is true, then we check if the rewrite holds for *all* I/O
   * pairs.
   */
  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;

 private:
  /** The enumerator whose value we are considering in this invariance test */
  Node d_enum;
  /** The input examples */
  std::vector<std::vector<Node> > d_ex;
  /** The output examples for the enumerator */
  std::vector<Node> d_exo;
  /** The set of I/O pair indices i such that
   *    contains( out_i, nvn[in_i] ) ---> false
   */
  std::vector<unsigned> d_neg_con_indices;
  /** requires not being in all examples */
  bool d_isUniversal;
};

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, Tim King
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		* Sygus invariance tests.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
19		#define CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
20
21		#include <unordered_map>
22		#include <vector>
23
24		#include "expr/node.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace quantifiers {
29
30		class TermDbSygus;
31		class SynthConjecture;
32
33		/* SygusInvarianceTest
34		*
35		* This class is the standard interface for term generalization
36		* in SyGuS. Its interface is a single function is_variant,
37		* which is a virtual condition for SyGuS terms.
38		*
39		* The common use case of invariance tests is when constructing
40		* minimal explanations for refinement lemmas in the
41		* counterexample-guided inductive synthesis (CEGIS) loop.
42		* See sygus_explain.h for more details.
43		*/
44	16573	class SygusInvarianceTest
45		{
46		public:
47	16573	virtual ~SygusInvarianceTest() {}
48
49		/** Is nvn invariant with respect to this test ?
50		*
51		* - nvn is the term to check whether it is invariant.
52		* - x is a variable such that the previous call to
53		* is_invariant (if any) was with term nvn_prev, and
54		* nvn is equal to nvn_prev with some subterm
55		* position replaced by x. This is typically used
56		* for debugging only.
57		*/
58	49975	bool is_invariant(TermDbSygus* tds, Node nvn, Node x)
59		{
60	49975	if (invariant(tds, nvn, x))
61		{
62	3977	d_update_nvn = nvn;
63	3977	return true;
64		}
65	45998	return false;
66		}
67		/** get updated term */
68	14642	Node getUpdatedTerm() { return d_update_nvn; }
69		/** set updated term */
70	7321	void setUpdatedTerm(Node n) { d_update_nvn = n; }
71		protected:
72		/** result of the node that satisfies this invariant */
73		Node d_update_nvn;
74		/** check whether nvn[ x ] is invariant */
75		virtual bool invariant(TermDbSygus* tds, Node nvn, Node x) = 0;
76		};
77
78		/** EquivSygusInvarianceTest
79		*
80		* This class tests whether a term evaluates via evaluation
81		* operators in the deep embedding (Section 4 of Reynolds
82		* et al. CAV 2015) to fixed term d_result.
83		*
84		* For example, consider a SyGuS evaluation function eval
85		* for a synthesis conjecture with arguments x and y.
86		* Notice that the term t = (mult x y) is such that:
87		* eval( t, 0, 1 ) ----> 0
88		* This test is invariant on the content of the second
89		* argument of t, noting that:
90		* eval( (mult x _), 0, 1 ) ----> 0
91		* as well, via a call to EvalSygusInvarianceTest::invariant.
92		*
93		* Another example, t = ite( gt( x, y ), x, y ) is such that:
94		* eval( t, 2, 3 ) ----> 3
95		* This test is invariant on the second child of t, noting:
96		* eval( ite( gt( x, y ), _, y ), 2, 3 ) ----> 3
97		*/
98	14875	class EvalSygusInvarianceTest : public SygusInvarianceTest
99		{
100		public:
101	14875	EvalSygusInvarianceTest()
102	14875	: d_kind(kind::UNDEFINED_KIND), d_is_conjunctive(false)
103		{
104	14875	}
105
106		/** initialize this invariance test
107		*
108		* This sets d_terms/d_var/d_result, where we are checking whether:
109		* <d_kind>(d_terms) { d_var -> n } ----> d_result.
110		* for terms n.
111		*/
112		void init(Node conj, Node var, Node res);
113
114		protected:
115		/** does d_terms{ d_var -> nvn } still rewrite to d_result? */
116		bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
117
118		private:
119		/** the formulas we are evaluating */
120		std::vector<Node> d_terms;
121		/** the variable */
122		TNode d_var;
123		/** the result of the evaluation */
124		Node d_result;
125		/** the parent kind we are checking, undefined if size(d_terms) is 1. */
126		Kind d_kind;
127		/** whether we are conjunctive
128		*
129		* If this flag is true, then the evaluation tests:
130		* d_terms[1] {d_var -> n} = d_result ... d_term[k] {d_var -> n} = d_result
131		* should be processed conjunctively, that is,
132		* <d_kind>(d_terms) { d_var -> n } = d_result only if each of the above
133		* holds. If this flag is false, then these tests are interpreted
134		* disjunctively, i.e. if one child test succeeds, the overall test succeeds.
135		*/
136		bool d_is_conjunctive;
137		};
138
139		/** EquivSygusInvarianceTest
140		*
141		* This class tests whether a builtin version of a
142		* sygus term is equivalent up to rewriting to a RHS value bvr.
143		*
144		* For example,
145		*
146		* ite( t>0, 0, 0 ) + s*0 ----> 0
147		*
148		* This test is invariant on the condition t>0 and s, since:
149		*
150		* ite( _, 0, 0 ) + _*0 ----> 0
151		*
152		* for any values of _.
153		*
154		* It also manages the case where the rewriting is invariant
155		* wrt a finite set of examples occurring in the conjecture.
156		* (EX1) : For example if our input examples are:
157		* (x,y,z) = (3,2,4), (5,2,6), (3,2,1)
158		* On these examples, we have:
159		*
160		* ite( x>y, z, 0) ---> 4,6,1
161		*
162		* which is invariant on the second argument:
163		*
164		* ite( x>y, z, _) ---> 4,6,1
165		*
166		* For details, see Reynolds et al SYNT 2017.
167		*/
168	1647	class EquivSygusInvarianceTest : public SygusInvarianceTest
169		{
170		public:
171	1647	EquivSygusInvarianceTest() : d_conj(nullptr) {}
172
173		/** initialize this invariance test
174		* tn is the sygus type for e
175		* aconj/e are used for conjecture-specific symmetry breaking
176		* bvr is the builtin version of the right hand side of the rewrite that we
177		* are checking for invariance
178		*/
179		void init(
180		TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr);
181
182		protected:
183		/** checks whether the analog of nvn still rewrites to d_bvr */
184		bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
185
186		private:
187		/** the conjecture associated with the enumerator d_enum */
188		SynthConjecture* d_conj;
189		/** the enumerator associated with the term for which this test is for */
190		Node d_enum;
191		/** the RHS of the evaluation */
192		Node d_bvr;
193		/** the result of the examples
194		* In (EX1), this is (4,6,1)
195		*/
196		std::vector<Node> d_exo;
197		};
198
199		/** DivByZeroSygusInvarianceTest
200		*
201		* This class tests whether a sygus term involves
202		* division by zero.
203		*
204		* For example the test for:
205		* ( x + ( y/0 )*2 )
206		* is invariant on the contents of _ below:
207		* ( _ + ( _/0 )*_ )
208		*/
209	1	class DivByZeroSygusInvarianceTest : public SygusInvarianceTest
210		{
211		public:
212	1	DivByZeroSygusInvarianceTest() {}
213
214		protected:
215		/** checks whether nvn involves division by zero. */
216		bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
217		};
218
219		/** NegContainsSygusInvarianceTest
220		*
221		* This class is used to construct a minimal shape of a term that cannot
222		* be contained in at least one output of an I/O pair.
223		*
224		* Say our PBE conjecture is:
225		*
226		* exists f.
227		* f( "abc" ) = "abc abc" ^
228		* f( "de" ) = "de de"
229		*
230		* Then, this class is used when there is a candidate solution t[x1]
231		* such that either:
232		* contains( "abc abc", t["abc"] ) ---> false or
233		* contains( "de de", t["de"] ) ---> false
234		*
235		* It is used to determine whether certain generalizations of t[x1]
236		* are still sufficient to falsify one of the above containments.
237		*
238		* For example:
239		*
240		* The test for str.++( x1, "d" ) is invariant on its first argument
241		* ...since contains( "abc abc", str.++( _, "d" ) ) ---> false
242		* The test for str.replace( "de", x1, "b" ) is invariant on its third argument
243		* ...since contains( "abc abc", str.replace( "de", "abc", _ ) ) ---> false
244		*/
245	50	class NegContainsSygusInvarianceTest : public SygusInvarianceTest
246		{
247		public:
248	50	NegContainsSygusInvarianceTest() : d_isUniversal(false) {}
249
250		/** initialize this invariance test
251		* e is the enumerator which we are reasoning about (associated with a synth
252		* fun).
253		* ex is the list of inputs,
254		* exo is the list of outputs,
255		* ncind is the set of possible example indices to check invariance of
256		* non-containment.
257		* For example, in the above example, when t[x1] = "ab", then this
258		* has the index 1 since contains("de de", "ab") ---> false but not
259		* the index 0 since contains("abc abc","ab") ---> true.
260		*/
261		void init(Node e,
262		std::vector<std::vector<Node> >& ex,
263		std::vector<Node>& exo,
264		std::vector<unsigned>& ncind);
265		/** set universal
266		*
267		* This updates the semantics of this check such that all instead of some
268		* examples must fail the containment test.
269		*/
270	3	void setUniversal() { d_isUniversal = true; }
271
272		protected:
273		/**
274		* Checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i; if
275		* d_isUniversal is true, then we check if the rewrite holds for all I/O
276		* pairs.
277		*/
278		bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
279
280		private:
281		/** The enumerator whose value we are considering in this invariance test */
282		Node d_enum;
283		/** The input examples */
284		std::vector<std::vector<Node> > d_ex;
285		/** The output examples for the enumerator */
286		std::vector<Node> d_exo;
287		/** The set of I/O pair indices i such that
288		* contains( out_i, nvn[in_i] ) ---> false
289		*/
290		std::vector<unsigned> d_neg_con_indices;
291		/** requires not being in all examples */
292		bool d_isUniversal;
293		};
294
295		} // namespace quantifiers
296		} // namespace theory
297		} // namespace cvc5
298
299		#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */