Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/single_inv_partition.h	Lines:	7	7	100.0 %
Date:	2021-08-17	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/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,
                       std::vector<Node>& terms,
                       std::vector<Node>& subs);

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