Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_invariance.h	Lines:	18	20	90.0 %
Date:	2021-08-14	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);

  /** do evaluate with unfolding, using the cache of this class */
  Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n);

 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;
  /** cache of n -> the simplified form of eval( n ) */
  std::unordered_map<Node, Node> d_visited;
};

/** 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	26661	class SygusInvarianceTest
45		{
46		public:
47	26661	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	64297	bool is_invariant(TermDbSygus* tds, Node nvn, Node x)
59		{
60	64297	if (invariant(tds, nvn, x))
61		{
62	4859	d_update_nvn = nvn;
63	4859	return true;
64		}
65	59438	return false;
66		}
67		/** get updated term */
68	16392	Node getUpdatedTerm() { return d_update_nvn; }
69		/** set updated term */
70	8196	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	24882	class EvalSygusInvarianceTest : public SygusInvarianceTest
99		{
100		public:
101	24882	EvalSygusInvarianceTest()
102	24882	: d_kind(kind::UNDEFINED_KIND), d_is_conjunctive(false)
103		{
104	24882	}
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		/** do evaluate with unfolding, using the cache of this class */
115		Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n);
116
117		protected:
118		/** does d_terms{ d_var -> nvn } still rewrite to d_result? */
119		bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
120
121		private:
122		/** the formulas we are evaluating */
123		std::vector<Node> d_terms;
124		/** the variable */
125		TNode d_var;
126		/** the result of the evaluation */
127		Node d_result;
128		/** the parent kind we are checking, undefined if size(d_terms) is 1. */
129		Kind d_kind;
130		/** whether we are conjunctive
131		*
132		* If this flag is true, then the evaluation tests:
133		* d_terms[1] {d_var -> n} = d_result ... d_term[k] {d_var -> n} = d_result
134		* should be processed conjunctively, that is,
135		* <d_kind>(d_terms) { d_var -> n } = d_result only if each of the above
136		* holds. If this flag is false, then these tests are interpreted
137		* disjunctively, i.e. if one child test succeeds, the overall test succeeds.
138		*/
139		bool d_is_conjunctive;
140		/** cache of n -> the simplified form of eval( n ) */
141		std::unordered_map<Node, Node> d_visited;
142		};
143
144		/** EquivSygusInvarianceTest
145		*
146		* This class tests whether a builtin version of a
147		* sygus term is equivalent up to rewriting to a RHS value bvr.
148		*
149		* For example,
150		*
151		* ite( t>0, 0, 0 ) + s*0 ----> 0
152		*
153		* This test is invariant on the condition t>0 and s, since:
154		*
155		* ite( _, 0, 0 ) + _*0 ----> 0
156		*
157		* for any values of _.
158		*
159		* It also manages the case where the rewriting is invariant
160		* wrt a finite set of examples occurring in the conjecture.
161		* (EX1) : For example if our input examples are:
162		* (x,y,z) = (3,2,4), (5,2,6), (3,2,1)
163		* On these examples, we have:
164		*
165		* ite( x>y, z, 0) ---> 4,6,1
166		*
167		* which is invariant on the second argument:
168		*
169		* ite( x>y, z, _) ---> 4,6,1
170		*
171		* For details, see Reynolds et al SYNT 2017.
172		*/
173	1729	class EquivSygusInvarianceTest : public SygusInvarianceTest
174		{
175		public:
176	1729	EquivSygusInvarianceTest() : d_conj(nullptr) {}
177
178		/** initialize this invariance test
179		* tn is the sygus type for e
180		* aconj/e are used for conjecture-specific symmetry breaking
181		* bvr is the builtin version of the right hand side of the rewrite that we
182		* are checking for invariance
183		*/
184		void init(
185		TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr);
186
187		protected:
188		/** checks whether the analog of nvn still rewrites to d_bvr */
189		bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
190
191		private:
192		/** the conjecture associated with the enumerator d_enum */
193		SynthConjecture* d_conj;
194		/** the enumerator associated with the term for which this test is for */
195		Node d_enum;
196		/** the RHS of the evaluation */
197		Node d_bvr;
198		/** the result of the examples
199		* In (EX1), this is (4,6,1)
200		*/
201		std::vector<Node> d_exo;
202		};
203
204		/** DivByZeroSygusInvarianceTest
205		*
206		* This class tests whether a sygus term involves
207		* division by zero.
208		*
209		* For example the test for:
210		* ( x + ( y/0 )*2 )
211		* is invariant on the contents of _ below:
212		* ( _ + ( _/0 )*_ )
213		*/
214		class DivByZeroSygusInvarianceTest : public SygusInvarianceTest
215		{
216		public:
217		DivByZeroSygusInvarianceTest() {}
218
219		protected:
220		/** checks whether nvn involves division by zero. */
221		bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
222		};
223
224		/** NegContainsSygusInvarianceTest
225		*
226		* This class is used to construct a minimal shape of a term that cannot
227		* be contained in at least one output of an I/O pair.
228		*
229		* Say our PBE conjecture is:
230		*
231		* exists f.
232		* f( "abc" ) = "abc abc" ^
233		* f( "de" ) = "de de"
234		*
235		* Then, this class is used when there is a candidate solution t[x1]
236		* such that either:
237		* contains( "abc abc", t["abc"] ) ---> false or
238		* contains( "de de", t["de"] ) ---> false
239		*
240		* It is used to determine whether certain generalizations of t[x1]
241		* are still sufficient to falsify one of the above containments.
242		*
243		* For example:
244		*
245		* The test for str.++( x1, "d" ) is invariant on its first argument
246		* ...since contains( "abc abc", str.++( _, "d" ) ) ---> false
247		* The test for str.replace( "de", x1, "b" ) is invariant on its third argument
248		* ...since contains( "abc abc", str.replace( "de", "abc", _ ) ) ---> false
249		*/
250	50	class NegContainsSygusInvarianceTest : public SygusInvarianceTest
251		{
252		public:
253	50	NegContainsSygusInvarianceTest() : d_isUniversal(false) {}
254
255		/** initialize this invariance test
256		* e is the enumerator which we are reasoning about (associated with a synth
257		* fun).
258		* ex is the list of inputs,
259		* exo is the list of outputs,
260		* ncind is the set of possible example indices to check invariance of
261		* non-containment.
262		* For example, in the above example, when t[x1] = "ab", then this
263		* has the index 1 since contains("de de", "ab") ---> false but not
264		* the index 0 since contains("abc abc","ab") ---> true.
265		*/
266		void init(Node e,
267		std::vector<std::vector<Node> >& ex,
268		std::vector<Node>& exo,
269		std::vector<unsigned>& ncind);
270		/** set universal
271		*
272		* This updates the semantics of this check such that all instead of some
273		* examples must fail the containment test.
274		*/
275	3	void setUniversal() { d_isUniversal = true; }
276
277		protected:
278		/**
279		* Checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i; if
280		* d_isUniversal is true, then we check if the rewrite holds for all I/O
281		* pairs.
282		*/
283		bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
284
285		private:
286		/** The enumerator whose value we are considering in this invariance test */
287		Node d_enum;
288		/** The input examples */
289		std::vector<std::vector<Node> > d_ex;
290		/** The output examples for the enumerator */
291		std::vector<Node> d_exo;
292		/** The set of I/O pair indices i such that
293		* contains( out_i, nvn[in_i] ) ---> false
294		*/
295		std::vector<unsigned> d_neg_con_indices;
296		/** requires not being in all examples */
297		bool d_isUniversal;
298		};
299
300		} // namespace quantifiers
301		} // namespace theory
302		} // namespace cvc5
303
304		#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */