Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/sygus/sygus_explain.h	Lines:	4	4	100.0 %
Date:	2021-09-16	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner, Gereon Kremer
 *
 * 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 explanations
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
#define CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H

#include <vector>

#include "expr/node.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class SygusInvarianceTest;
class TermDbSygus;

/** Recursive term builder
 *
 * This is a utility used to generate variants
 * of a term n, where subterms of n can be replaced
 * by others via calls to replaceChild(...).
 *
 * This class maintains a "context", which indicates
 * a position in term n. Below, we call the subterm of
 * the initial term n at this position the "active term".
 *
 */
class TermRecBuild
{
 public:
  TermRecBuild() {}
  /** set the initial term to n
   *
   * The context initially empty, that is,
   * the active term is initially n.
   */
  void init(Node n);

  /** push the context
   *
   * This updates the context so that the
   * active term is updated to curr[p], where
   * curr is the previously active term.
   */
  void push(unsigned p);

  /** pop the context */
  void pop();
  /** indicates that the i^th child of the active
   * term should be replaced by r in calls to build().
   */
  void replaceChild(unsigned i, Node r);
  /** get the i^th child of the active term */
  Node getChild(unsigned i);
  /** build the (modified) version of the term
   * we initialized via the call to init().
   */
  Node build(unsigned p = 0);

 private:
  /** stack of active terms */
  std::vector<Node> d_term;
  /** stack of children of active terms
   * Notice that these may be modified with calls to replaceChild(...).
   */
  std::vector<std::vector<Node> > d_children;
  /** stack the kind of active terms */
  std::vector<Kind> d_kind;
  /** stack of whether the active terms had an operator */
  std::vector<bool> d_has_op;
  /** stack of positions that were pushed via calls to push(...) */
  std::vector<unsigned> d_pos;
  /** add term to the context stack */
  void addTerm(Node n);
};

/*The SygusExplain utility
 *
 * This class is used to produce explanations for refinement lemmas
 * in the counterexample-guided inductive synthesis (CEGIS) loop.
 *
 * When given an invariance test T traverses the AST of a given term,
 * uses TermRecBuild to replace various subterms by fresh variables and
 * recheck whether the invariant, as specified by T still holds.
 * If it does, then we may exclude the explanation for that subterm.
 *
 * For example, say we have that the current value of
 * (datatype) sygus term n is:
 *  (if (gt x 0) 0 0)
 * where if, gt, x, 0 are datatype constructors.
 * The explanation returned by getExplanationForEquality
 * below for n and the above term is:
 *   { ((_ is if) n), ((_ is geq) n.0),
 *     ((_ is x) n.0.0), ((_ is 0) n.0.1),
 *     ((_ is 0) n.1), ((_ is 0) n.2) }
 *
 * This class can also return more precise
 * explanations based on a property that holds for
 * variants of n. For instance,
 * say we find that n's builtin analog rewrites to 0:
 *  ite( x>0, 0, 0 ) ----> 0
 * and we would like to find the minimal explanation for
 * why the builtin analog of n rewrites to 0.
 * We use the invariance test EquivSygusInvarianceTest
 * (see sygus_invariance.h) for doing this.
 * Using the SygusExplain::getExplanationFor method below,
 * this will invoke the invariant test to check, e.g.
 *   ite( x>0, 0, y1 ) ----> 0 ? fail
 *   ite( x>0, y2, 0 ) ----> 0 ? fail
 *   ite( y3, 0, 0 ) ----> 0 ? success
 * where y1, y2, y3 are fresh variables.
 * Hence the explanation for the condition x>0 is irrelevant.
 * This gives us the explanation:
 *   { ((_ is if) n), ((_ is 0) n.1), ((_ is 0) n.2) }
 * indicating that all terms of the form:
 *   (if _ 0 0) have a builtin equivalent that rewrites to 0.
 *
 * For details, see Reynolds et al SYNT 2017.
 *
 * Below, we let [[exp]]_n denote the term induced by
 * the explanation exp for n.
 * For example:
 *   exp = { ((_ is plus) n), ((_ is y) n.1) }
 * is such that:
 *   [[exp]]_n = (plus w y)
 * where w is a fresh variable.
 */
class SygusExplain
{
 public:
  SygusExplain(TermDbSygus* tdb) : d_tdb(tdb) {}
  ~SygusExplain() {}
  /** get explanation for equality
   *
   * This function constructs an explanation, stored in exp, such that:
   * - All formulas in exp are of the form ((_ is C) ns), where ns
   *   is a chain of selectors applied to n, and
   * - exp => ( n = vn )
   */
  void getExplanationForEquality(Node n, Node vn, std::vector<Node>& exp);
  /** returns the conjunction of exp computed in the above function */
  Node getExplanationForEquality(Node n, Node vn);

  /** get explanation for equality
   *
   * This is identical to the above function except that we
   * take an additional argument cexc, which says which
   * children of vn should be excluded from the explanation.
   *
   * For example, if vn = plus( plus( x, x ), y ) and cexc is { 0 -> true },
   * then the following is appended to exp :
   *   { ((_ is plus) n), ((_ is y) n.1) }
   * where notice that the 0^th argument of vn is excluded.
   */
  void getExplanationForEquality(Node n,
                                 Node vn,
                                 std::vector<Node>& exp,
                                 std::map<unsigned, bool>& cexc);
  /** returns the conjunction of exp computed in the above function */
  Node getExplanationForEquality(Node n,
                                 Node vn,
                                 std::map<unsigned, bool>& cexc);

  /** get explanation for
   *
   * This function constructs an explanation, stored in exp, such that:
   * - All formulas in exp are of the form ((_ is C) ns), where ns
   *   is a chain of selectors applied to n, and
   * - The test et holds for [[exp]]_n, and
   * - (if applicable) exp => ( n != vnr ).
   *
   * This function updates sz to be the term size of [[exp]]_n.
   *
   * If strict is false, then we also test whether the invariance test holds
   * independently of the entire value of vn.
   *
   * The argument var_count is used for tracking the variables that we introduce
   * to generalize the shape of vn. This map is passed to
   * TermDbSygus::getFreeVarInc. This argument should be used if we are
   * calling this function multiple times and the generalization should not
   * introduce variables that shadow the variables introduced on previous calls.
   */
  void getExplanationFor(Node n,
                         Node vn,
                         std::vector<Node>& exp,
                         SygusInvarianceTest& et,
                         Node vnr,
                         unsigned& sz);
  void getExplanationFor(Node n,
                         Node vn,
                         std::vector<Node>& exp,
                         SygusInvarianceTest& et,
                         Node vnr,
                         std::map<TypeNode, int>& var_count,
                         unsigned& sz);
  void getExplanationFor(Node n,
                         Node vn,
                         std::vector<Node>& exp,
                         SygusInvarianceTest& et,
                         bool strict = true);
  void getExplanationFor(Node n,
                         Node vn,
                         std::vector<Node>& exp,
                         SygusInvarianceTest& et,
                         std::map<TypeNode, int>& var_count,
                         bool strict = true);

 private:
  /** sygus term database associated with this utility */
  TermDbSygus* d_tdb;
  /** Helper function for getExplanationFor
   * var_count is the number of free variables we have introduced,
   *   per type, for the purposes of generalizing subterms of n.
   * vnr_exp stores the explanation, if one exists, for
   *   n != vnr.  It is only non-null if vnr is non-null.
   */
  void getExplanationFor(TermRecBuild& trb,
                         Node n,
                         Node vn,
                         std::vector<Node>& exp,
                         std::map<TypeNode, int>& var_count,
                         SygusInvarianceTest& et,
                         Node vnr,
                         Node& vnr_exp,
                         int& sz);
};

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

#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner, Gereon Kremer
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 explanations
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
19		#define CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
20
21		#include <vector>
22
23		#include "expr/node.h"
24
25		namespace cvc5 {
26		namespace theory {
27		namespace quantifiers {
28
29		class SygusInvarianceTest;
30		class TermDbSygus;
31
32		/** Recursive term builder
33		*
34		* This is a utility used to generate variants
35		* of a term n, where subterms of n can be replaced
36		* by others via calls to replaceChild(...).
37		*
38		* This class maintains a "context", which indicates
39		* a position in term n. Below, we call the subterm of
40		* the initial term n at this position the "active term".
41		*
42		*/
43	12750	class TermRecBuild
44		{
45		public:
46	12750	TermRecBuild() {}
47		/** set the initial term to n
48		*
49		* The context initially empty, that is,
50		* the active term is initially n.
51		*/
52		void init(Node n);
53
54		/** push the context
55		*
56		* This updates the context so that the
57		* active term is updated to curr[p], where
58		* curr is the previously active term.
59		*/
60		void push(unsigned p);
61
62		/** pop the context */
63		void pop();
64		/** indicates that the i^th child of the active
65		* term should be replaced by r in calls to build().
66		*/
67		void replaceChild(unsigned i, Node r);
68		/** get the i^th child of the active term */
69		Node getChild(unsigned i);
70		/** build the (modified) version of the term
71		* we initialized via the call to init().
72		*/
73		Node build(unsigned p = 0);
74
75		private:
76		/** stack of active terms */
77		std::vector<Node> d_term;
78		/** stack of children of active terms
79		* Notice that these may be modified with calls to replaceChild(...).
80		*/
81		std::vector<std::vector<Node> > d_children;
82		/** stack the kind of active terms */
83		std::vector<Kind> d_kind;
84		/** stack of whether the active terms had an operator */
85		std::vector<bool> d_has_op;
86		/** stack of positions that were pushed via calls to push(...) */
87		std::vector<unsigned> d_pos;
88		/** add term to the context stack */
89		void addTerm(Node n);
90		};
91
92		/*The SygusExplain utility
93		*
94		* This class is used to produce explanations for refinement lemmas
95		* in the counterexample-guided inductive synthesis (CEGIS) loop.
96		*
97		* When given an invariance test T traverses the AST of a given term,
98		* uses TermRecBuild to replace various subterms by fresh variables and
99		* recheck whether the invariant, as specified by T still holds.
100		* If it does, then we may exclude the explanation for that subterm.
101		*
102		* For example, say we have that the current value of
103		* (datatype) sygus term n is:
104		* (if (gt x 0) 0 0)
105		* where if, gt, x, 0 are datatype constructors.
106		* The explanation returned by getExplanationForEquality
107		* below for n and the above term is:
108		* { ((_ is if) n), ((_ is geq) n.0),
109		* ((_ is x) n.0.0), ((_ is 0) n.0.1),
110		* ((_ is 0) n.1), ((_ is 0) n.2) }
111		*
112		* This class can also return more precise
113		* explanations based on a property that holds for
114		* variants of n. For instance,
115		* say we find that n's builtin analog rewrites to 0:
116		* ite( x>0, 0, 0 ) ----> 0
117		* and we would like to find the minimal explanation for
118		* why the builtin analog of n rewrites to 0.
119		* We use the invariance test EquivSygusInvarianceTest
120		* (see sygus_invariance.h) for doing this.
121		* Using the SygusExplain::getExplanationFor method below,
122		* this will invoke the invariant test to check, e.g.
123		* ite( x>0, 0, y1 ) ----> 0 ? fail
124		* ite( x>0, y2, 0 ) ----> 0 ? fail
125		* ite( y3, 0, 0 ) ----> 0 ? success
126		* where y1, y2, y3 are fresh variables.
127		* Hence the explanation for the condition x>0 is irrelevant.
128		* This gives us the explanation:
129		* { ((_ is if) n), ((_ is 0) n.1), ((_ is 0) n.2) }
130		* indicating that all terms of the form:
131		* (if _ 0 0) have a builtin equivalent that rewrites to 0.
132		*
133		* For details, see Reynolds et al SYNT 2017.
134		*
135		* Below, we let [[exp]]_n denote the term induced by
136		* the explanation exp for n.
137		* For example:
138		* exp = { ((_ is plus) n), ((_ is y) n.1) }
139		* is such that:
140		* [[exp]]_n = (plus w y)
141		* where w is a fresh variable.
142		*/
143		class SygusExplain
144		{
145		public:
146	1422	SygusExplain(TermDbSygus* tdb) : d_tdb(tdb) {}
147	1420	~SygusExplain() {}
148		/** get explanation for equality
149		*
150		* This function constructs an explanation, stored in exp, such that:
151		* - All formulas in exp are of the form ((_ is C) ns), where ns
152		* is a chain of selectors applied to n, and
153		* - exp => ( n = vn )
154		*/
155		void getExplanationForEquality(Node n, Node vn, std::vector<Node>& exp);
156		/** returns the conjunction of exp computed in the above function */
157		Node getExplanationForEquality(Node n, Node vn);
158
159		/** get explanation for equality
160		*
161		* This is identical to the above function except that we
162		* take an additional argument cexc, which says which
163		* children of vn should be excluded from the explanation.
164		*
165		* For example, if vn = plus( plus( x, x ), y ) and cexc is { 0 -> true },
166		* then the following is appended to exp :
167		* { ((_ is plus) n), ((_ is y) n.1) }
168		* where notice that the 0^th argument of vn is excluded.
169		*/
170		void getExplanationForEquality(Node n,
171		Node vn,
172		std::vector<Node>& exp,
173		std::map<unsigned, bool>& cexc);
174		/** returns the conjunction of exp computed in the above function */
175		Node getExplanationForEquality(Node n,
176		Node vn,
177		std::map<unsigned, bool>& cexc);
178
179		/** get explanation for
180		*
181		* This function constructs an explanation, stored in exp, such that:
182		* - All formulas in exp are of the form ((_ is C) ns), where ns
183		* is a chain of selectors applied to n, and
184		* - The test et holds for [[exp]]_n, and
185		* - (if applicable) exp => ( n != vnr ).
186		*
187		* This function updates sz to be the term size of [[exp]]_n.
188		*
189		* If strict is false, then we also test whether the invariance test holds
190		* independently of the entire value of vn.
191		*
192		* The argument var_count is used for tracking the variables that we introduce
193		* to generalize the shape of vn. This map is passed to
194		* TermDbSygus::getFreeVarInc. This argument should be used if we are
195		* calling this function multiple times and the generalization should not
196		* introduce variables that shadow the variables introduced on previous calls.
197		*/
198		void getExplanationFor(Node n,
199		Node vn,
200		std::vector<Node>& exp,
201		SygusInvarianceTest& et,
202		Node vnr,
203		unsigned& sz);
204		void getExplanationFor(Node n,
205		Node vn,
206		std::vector<Node>& exp,
207		SygusInvarianceTest& et,
208		Node vnr,
209		std::map<TypeNode, int>& var_count,
210		unsigned& sz);
211		void getExplanationFor(Node n,
212		Node vn,
213		std::vector<Node>& exp,
214		SygusInvarianceTest& et,
215		bool strict = true);
216		void getExplanationFor(Node n,
217		Node vn,
218		std::vector<Node>& exp,
219		SygusInvarianceTest& et,
220		std::map<TypeNode, int>& var_count,
221		bool strict = true);
222
223		private:
224		/** sygus term database associated with this utility */
225		TermDbSygus* d_tdb;
226		/** Helper function for getExplanationFor
227		* var_count is the number of free variables we have introduced,
228		* per type, for the purposes of generalizing subterms of n.
229		* vnr_exp stores the explanation, if one exists, for
230		* n != vnr. It is only non-null if vnr is non-null.
231		*/
232		void getExplanationFor(TermRecBuild& trb,
233		Node n,
234		Node vn,
235		std::vector<Node>& exp,
236		std::map<TypeNode, int>& var_count,
237		SygusInvarianceTest& et,
238		Node vnr,
239		Node& vnr_exp,
240		int& sz);
241		};
242
243		} // namespace quantifiers
244		} // namespace theory
245		} // namespace cvc5
246
247		#endif /* CVC5__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */