Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/single_inv_partition.h	Lines:	7	7	100.0 %
Date:	2021-09-29	Branches:	5	6	83.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * Utility for single invocation partitioning.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
#define CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H

#include <map>
#include <vector>

#include "expr/node.h"
#include "expr/subs.h"
#include "expr/type_node.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

/** single invocation partition
 *
 * This is a utility to group formulas into single invocation/non-single
 * invocation parts, relative to a set of "input functions".
 * It can be used when either the set of input functions is fixed,
 * or is unknown.
 *
 * (EX1) For example, if input functions are { f },
 * then the formula is ( f( x, y ) = g( y ) V f( x, y ) = b )
 * is single invocation since there is only one
 * unique application of f, that is, f( x, y ).
 * Notice that
 *   exists f. forall xy. f( x, y ) = g( y ) V f( x, y ) = b
 * is equivalent to:
 *   forall xy. exists z. z = g( y ) V z = b
 *
 * When handling multiple input functions, we only infer a formula
 * is single invocation if all (relevant) input functions have the
 * same argument types. An input function is relevant if it is
 * specified by the input in a call to init() or occurs in the
 * formula we are processing.
 *
 * Notice that this class may introduce auxiliary variables to
 * coerce a formula into being single invocation. For example,
 * see Example 5 of Reynolds et al. SYNT 2017.
 *
 */
class SingleInvocationPartition
{
 public:
  SingleInvocationPartition() : d_has_input_funcs(false) {}
  ~SingleInvocationPartition() {}
  /** initialize this partition for formula n, with input functions funcs
   *
   * This initializes this class to check whether formula n is single
   * invocation with respect to the input functions in funcs only.
   * Below, the "processed formula" is a formula generated by this
   * call that is equivalent to n (if this call is successful).
   *
   * This method returns true if all input functions have identical
   * argument types, and false otherwise. Notice that all
   * access functions below are only valid if this class is
   * successfully initialized.
   */
  bool init(std::vector<Node>& funcs, Node n);

  /** initialize this partition for formula n
   *
   * In contrast to the above method, this version assumes that
   * all uninterpreted functions are input functions. That is, this
   * method is equivalent to the above function with funcs containing
   * all uninterpreted functions occurring in n.
   */
  bool init(Node n);

  /** is the processed formula purely single invocation?
   *
   * A formula is purely single invocation if it is equivalent to:
   *   t[ f1( x ), ..., fn( x ), x ],
   * for some F, where f1...fn are the input functions.
   * Notice that the free variables of t are exactly x.
   */
  bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); }
  /** is the processed formula non-ground single invocation?
   *
   * A formula is non-ground single invocation if it is equivalent to:
   *   F[ f1( x ), ..., fn( x ), x, y ],
   * for some F, where f1...fn are the input functions.
   */
  bool isNonGroundSingleInvocation()
  {
    return d_conjuncts[3].size() == d_conjuncts[1].size();
  }

  /** Get the (portion of) the processed formula that is single invocation
   *
   * Notice this method returns the anti-skolemized version of the input
   * formula. In (EX1), this method returns:
   *   z = g( y ) V z = b
   * where z is the first-order variable for f (see
   * getFirstOrderVariableForFunction).
   */
  Node getSingleInvocation() { return getConjunct(0); }
  /** Get the (portion of) the processed formula that is not single invocation
   *
   * This formula and the above form a partition of the conjuncts of the
   * processed formula, that is:
   *   getSingleInvocation() * sigma ^ getNonSingleInvocation()
   * is equivalent to the processed formula, where sigma is a substitution of
   * the form:
   *   z_1 -> f_1( x ) .... z_n -> f_n( x )
   * where z_i are the first-order variables for input functions f_i
   * for all i=1,...,n, and x are the single invocation arguments of the input
   * formulas (see d_si_vars).
   */
  Node getNonSingleInvocation() { return getConjunct(1); }
  /** get full specification
   *
   * This returns getSingleInvocation() * sigma ^ getNonSingleInvocation(),
   * which is equivalent to the processed formula, where sigma is the
   * substitution described above.
   */
  Node getFullSpecification() { return getConjunct(2); }
  /** get first order variable for input function f
   *
   * This corresponds to the variable that we used when anti-skolemizing
   * function f. For example, in (EX1), if getSingleInvocation() returns:
   *   z = g( y ) V z = b
   * Then, getFirstOrderVariableForFunction(f) = z.
   */
  Node getFirstOrderVariableForFunction(Node f) const;

  /** get function for first order variable
   *
   * Opposite direction of above, where:
   *   getFunctionForFirstOrderVariable(z) = f.
   */
  Node getFunctionForFirstOrderVariable(Node v) const;

  /** get function invocation for
   *
   * Returns f( x ) where x are the single invocation arguments of the input
   * formulas (see d_si_vars). If f is not an input function, it returns null.
   */
  Node getFunctionInvocationFor(Node f) const;

  /** get single invocation variables, appends them to sivars */
  void getSingleInvocationVariables(std::vector<Node>& sivars) const;

  /** get all variables
   *
   * Appends all free variables of the processed formula to vars.
   */
  void getAllVariables(std::vector<Node>& vars) const;

  /** get function variables
   *
   * Appends all first-order variables corresponding to input functions to
   * fvars.
   */
  void getFunctionVariables(std::vector<Node>& fvars) const;

  /** get functions
   *
   * Gets all input functions. This has the same order as the list of
   * function variables above.
   */
  void getFunctions(std::vector<Node>& fs) const;

  /** print debugging information on Trace c */
  void debugPrint(const char* c);

 private:
  /** map from input functions to whether they have an anti-skolemizable type
   * An anti-skolemizable type is one of the form:
   *   ( T1, ..., Tn ) -> T
   * where Ti = d_arg_types[i] for i = 1,...,n.
   */
  std::map<Node, bool> d_funcs;

  /** map from functions to the invocation we inferred for them */
  std::map<Node, Node> d_func_inv;

  /** the list of first-order variables for functions
   * In (EX1), this is the list { z }.
   */
  std::vector<Node> d_func_vars;

  /** the arguments that we based the anti-skolemization on.
   * In (EX1), this is the list { x, y }.
   */
  std::vector<Node> d_si_vars;

  /** every free variable of conjuncts[2] */
  std::unordered_set<Node> d_all_vars;
  /** map from functions to first-order variables that anti-skolemized them */
  std::map<Node, Node> d_func_fo_var;
  /** map from first-order variables to the function it anti-skolemized */
  std::map<Node, Node> d_fo_var_to_func;

  /** The argument types for this single invocation partition.
   * These are the argument types of the input functions we are
   * processing, where notice that:
   *   d_si_vars[i].getType()==d_arg_types[i]
   */
  std::vector<TypeNode> d_arg_types;

  /** the list of conjuncts with various properties :
   * 0 : the single invocation conjuncts (stored in anti-skolemized form),
   * 1 : the non-single invocation conjuncts,
   * 2 : all conjuncts,
   * 3 : non-ground single invocation conjuncts.
   */
  std::vector<Node> d_conjuncts[4];

  /** did we initialize this class with input functions? */
  bool d_has_input_funcs;
  /** the input functions we initialized this class with */
  std::vector<Node> d_input_funcs;
  /** all input functions */
  std::vector<Node> d_all_funcs;
  /** skolem of the same type as input functions */
  std::vector<Node> d_input_func_sks;

  /** infer the argument types of uninterpreted function applications
   *
   * If this method returns true, then typs contains the list of types of
   * the arguments (in order) of all uninterpreted functions in n.
   * If this method returns false, then there exists (at least) two
   * uninterpreted functions in n whose argument types are not identical.
   */
  bool inferArgTypes(Node n,
                     std::vector<TypeNode>& typs,
                     std::map<Node, bool>& visited);

  /** is anti-skolemizable type
   *
   * This method returns true if f's argument types are equal to the
   * argument types we have fixed in this class (see d_arg_types).
   */
  bool isAntiSkolemizableType(Node f);

  /**
   * This is the entry point for initializing this class,
   * which is called by the public init(...) methods.
   *   funcs are the input functions (if any were explicitly provide),
   *   typs is the types of the arguments of funcs,
   *   n is the formula to process,
   *   has_funcs is whether input functions were explicitly provided.
   */
  bool init(std::vector<Node>& funcs,
            std::vector<TypeNode>& typs,
            Node n,
            bool has_funcs);

  /**
   * Collect the top-level conjuncts of the formula (equivalent to)
   * n or the negation of n if pol=false, and store them in conj.
   */
  bool collectConjuncts(Node n, bool pol, std::vector<Node>& conj);

  /** process conjunct n
   *
   * This function is called when n is a top-level conjunction in a
   * formula that is equivalent to the input formula given to this
   * class via init.
   *
   * args : stores the arguments (if any) that we have seen in an application
   *   of an application of an input function in this conjunct.
   * terms/subs : this stores a term substitution with entries of the form:
   *     f(args) -> z
   *   where z is the first-order variable for input function f.
   */
  bool processConjunct(Node n,
                       std::map<Node, bool>& visited,
                       std::vector<Node>& args,
                       Subs& sb);

  /** get the and node corresponding to d_conjuncts[index] */
  Node getConjunct(int index);
};

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

#endif /* CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Mathias Preiner
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		* Utility for single invocation partitioning.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
19		#define CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H
20
21		#include <map>
22		#include <vector>
23
24		#include "expr/node.h"
25		#include "expr/subs.h"
26		#include "expr/type_node.h"
27
28		namespace cvc5 {
29		namespace theory {
30		namespace quantifiers {
31
32		/** single invocation partition
33		*
34		* This is a utility to group formulas into single invocation/non-single
35		* invocation parts, relative to a set of "input functions".
36		* It can be used when either the set of input functions is fixed,
37		* or is unknown.
38		*
39		* (EX1) For example, if input functions are { f },
40		* then the formula is ( f( x, y ) = g( y ) V f( x, y ) = b )
41		* is single invocation since there is only one
42		* unique application of f, that is, f( x, y ).
43		* Notice that
44		* exists f. forall xy. f( x, y ) = g( y ) V f( x, y ) = b
45		* is equivalent to:
46		* forall xy. exists z. z = g( y ) V z = b
47		*
48		* When handling multiple input functions, we only infer a formula
49		* is single invocation if all (relevant) input functions have the
50		* same argument types. An input function is relevant if it is
51		* specified by the input in a call to init() or occurs in the
52		* formula we are processing.
53		*
54		* Notice that this class may introduce auxiliary variables to
55		* coerce a formula into being single invocation. For example,
56		* see Example 5 of Reynolds et al. SYNT 2017.
57		*
58		*/
59		class SingleInvocationPartition
60		{
61		public:
62	1198	SingleInvocationPartition() : d_has_input_funcs(false) {}
63	1196	~SingleInvocationPartition() {}
64		/** initialize this partition for formula n, with input functions funcs
65		*
66		* This initializes this class to check whether formula n is single
67		* invocation with respect to the input functions in funcs only.
68		* Below, the "processed formula" is a formula generated by this
69		* call that is equivalent to n (if this call is successful).
70		*
71		* This method returns true if all input functions have identical
72		* argument types, and false otherwise. Notice that all
73		* access functions below are only valid if this class is
74		* successfully initialized.
75		*/
76		bool init(std::vector<Node>& funcs, Node n);
77
78		/** initialize this partition for formula n
79		*
80		* In contrast to the above method, this version assumes that
81		* all uninterpreted functions are input functions. That is, this
82		* method is equivalent to the above function with funcs containing
83		* all uninterpreted functions occurring in n.
84		*/
85		bool init(Node n);
86
87		/** is the processed formula purely single invocation?
88		*
89		* A formula is purely single invocation if it is equivalent to:
90		* t[ f1( x ), ..., fn( x ), x ],
91		* for some F, where f1...fn are the input functions.
92		* Notice that the free variables of t are exactly x.
93		*/
94	314	bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); }
95		/** is the processed formula non-ground single invocation?
96		*
97		* A formula is non-ground single invocation if it is equivalent to:
98		* F[ f1( x ), ..., fn( x ), x, y ],
99		* for some F, where f1...fn are the input functions.
100		*/
101	2	bool isNonGroundSingleInvocation()
102		{
103	2	return d_conjuncts[3].size() == d_conjuncts[1].size();
104		}
105
106		/** Get the (portion of) the processed formula that is single invocation
107		*
108		* Notice this method returns the anti-skolemized version of the input
109		* formula. In (EX1), this method returns:
110		* z = g( y ) V z = b
111		* where z is the first-order variable for f (see
112		* getFirstOrderVariableForFunction).
113		*/
114	93	Node getSingleInvocation() { return getConjunct(0); }
115		/** Get the (portion of) the processed formula that is not single invocation
116		*
117		* This formula and the above form a partition of the conjuncts of the
118		* processed formula, that is:
119		* getSingleInvocation() * sigma ^ getNonSingleInvocation()
120		* is equivalent to the processed formula, where sigma is a substitution of
121		* the form:
122		* z_1 -> f_1( x ) .... z_n -> f_n( x )
123		* where z_i are the first-order variables for input functions f_i
124		* for all i=1,...,n, and x are the single invocation arguments of the input
125		* formulas (see d_si_vars).
126		*/
127		Node getNonSingleInvocation() { return getConjunct(1); }
128		/** get full specification
129		*
130		* This returns getSingleInvocation() * sigma ^ getNonSingleInvocation(),
131		* which is equivalent to the processed formula, where sigma is the
132		* substitution described above.
133		*/
134	2	Node getFullSpecification() { return getConjunct(2); }
135		/** get first order variable for input function f
136		*
137		* This corresponds to the variable that we used when anti-skolemizing
138		* function f. For example, in (EX1), if getSingleInvocation() returns:
139		* z = g( y ) V z = b
140		* Then, getFirstOrderVariableForFunction(f) = z.
141		*/
142		Node getFirstOrderVariableForFunction(Node f) const;
143
144		/** get function for first order variable
145		*
146		* Opposite direction of above, where:
147		* getFunctionForFirstOrderVariable(z) = f.
148		*/
149		Node getFunctionForFirstOrderVariable(Node v) const;
150
151		/** get function invocation for
152		*
153		* Returns f( x ) where x are the single invocation arguments of the input
154		* formulas (see d_si_vars). If f is not an input function, it returns null.
155		*/
156		Node getFunctionInvocationFor(Node f) const;
157
158		/** get single invocation variables, appends them to sivars */
159		void getSingleInvocationVariables(std::vector<Node>& sivars) const;
160
161		/** get all variables
162		*
163		* Appends all free variables of the processed formula to vars.
164		*/
165		void getAllVariables(std::vector<Node>& vars) const;
166
167		/** get function variables
168		*
169		* Appends all first-order variables corresponding to input functions to
170		* fvars.
171		*/
172		void getFunctionVariables(std::vector<Node>& fvars) const;
173
174		/** get functions
175		*
176		* Gets all input functions. This has the same order as the list of
177		* function variables above.
178		*/
179		void getFunctions(std::vector<Node>& fs) const;
180
181		/** print debugging information on Trace c */
182		void debugPrint(const char* c);
183
184		private:
185		/** map from input functions to whether they have an anti-skolemizable type
186		* An anti-skolemizable type is one of the form:
187		* ( T1, ..., Tn ) -> T
188		* where Ti = d_arg_types[i] for i = 1,...,n.
189		*/
190		std::map<Node, bool> d_funcs;
191
192		/** map from functions to the invocation we inferred for them */
193		std::map<Node, Node> d_func_inv;
194
195		/** the list of first-order variables for functions
196		* In (EX1), this is the list { z }.
197		*/
198		std::vector<Node> d_func_vars;
199
200		/** the arguments that we based the anti-skolemization on.
201		* In (EX1), this is the list { x, y }.
202		*/
203		std::vector<Node> d_si_vars;
204
205		/** every free variable of conjuncts[2] */
206		std::unordered_set<Node> d_all_vars;
207		/** map from functions to first-order variables that anti-skolemized them */
208		std::map<Node, Node> d_func_fo_var;
209		/** map from first-order variables to the function it anti-skolemized */
210		std::map<Node, Node> d_fo_var_to_func;
211
212		/** The argument types for this single invocation partition.
213		* These are the argument types of the input functions we are
214		* processing, where notice that:
215		* d_si_vars[i].getType()==d_arg_types[i]
216		*/
217		std::vector<TypeNode> d_arg_types;
218
219		/** the list of conjuncts with various properties :
220		* 0 : the single invocation conjuncts (stored in anti-skolemized form),
221		* 1 : the non-single invocation conjuncts,
222		* 2 : all conjuncts,
223		* 3 : non-ground single invocation conjuncts.
224		*/
225		std::vector<Node> d_conjuncts[4];
226
227		/** did we initialize this class with input functions? */
228		bool d_has_input_funcs;
229		/** the input functions we initialized this class with */
230		std::vector<Node> d_input_funcs;
231		/** all input functions */
232		std::vector<Node> d_all_funcs;
233		/** skolem of the same type as input functions */
234		std::vector<Node> d_input_func_sks;
235
236		/** infer the argument types of uninterpreted function applications
237		*
238		* If this method returns true, then typs contains the list of types of
239		* the arguments (in order) of all uninterpreted functions in n.
240		* If this method returns false, then there exists (at least) two
241		* uninterpreted functions in n whose argument types are not identical.
242		*/
243		bool inferArgTypes(Node n,
244		std::vector<TypeNode>& typs,
245		std::map<Node, bool>& visited);
246
247		/** is anti-skolemizable type
248		*
249		* This method returns true if f's argument types are equal to the
250		* argument types we have fixed in this class (see d_arg_types).
251		*/
252		bool isAntiSkolemizableType(Node f);
253
254		/**
255		* This is the entry point for initializing this class,
256		* which is called by the public init(...) methods.
257		* funcs are the input functions (if any were explicitly provide),
258		* typs is the types of the arguments of funcs,
259		* n is the formula to process,
260		* has_funcs is whether input functions were explicitly provided.
261		*/
262		bool init(std::vector<Node>& funcs,
263		std::vector<TypeNode>& typs,
264		Node n,
265		bool has_funcs);
266
267		/**
268		* Collect the top-level conjuncts of the formula (equivalent to)
269		* n or the negation of n if pol=false, and store them in conj.
270		*/
271		bool collectConjuncts(Node n, bool pol, std::vector<Node>& conj);
272
273		/** process conjunct n
274		*
275		* This function is called when n is a top-level conjunction in a
276		* formula that is equivalent to the input formula given to this
277		* class via init.
278		*
279		* args : stores the arguments (if any) that we have seen in an application
280		* of an application of an input function in this conjunct.
281		* terms/subs : this stores a term substitution with entries of the form:
282		* f(args) -> z
283		* where z is the first-order variable for input function f.
284		*/
285		bool processConjunct(Node n,
286		std::map<Node, bool>& visited,
287		std::vector<Node>& args,
288		Subs& sb);
289
290		/** get the and node corresponding to d_conjuncts[index] */
291		Node getConjunct(int index);
292		};
293
294		} // namespace quantifiers
295		} // namespace theory
296		} // namespace cvc5
297
298		#endif /* CVC5__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */