Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/quantifiers_rewriter.h	Lines:	1	1	100.0 %
Date:	2021-08-20	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Haniel Barbosa, Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * Rewriter for the theory of inductive quantifiers.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H

#include "proof/trust_node.h"
#include "theory/theory_rewriter.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

struct QAttributes;

/**
 * List of steps used by the quantifiers rewriter, details on these steps
 * can be found in the class below.
 */
enum RewriteStep
{
  /** Eliminate symbols (e.g. implies, xor) */
  COMPUTE_ELIM_SYMBOLS = 0,
  /** Miniscoping */
  COMPUTE_MINISCOPING,
  /** Aggressive miniscoping */
  COMPUTE_AGGRESSIVE_MINISCOPING,
  /** Apply the extended rewriter to quantified formula bodies */
  COMPUTE_EXT_REWRITE,
  /**
   * Term processing (e.g. simplifying terms based on ITE lifting,
   * eliminating extended arithmetic symbols).
   */
  COMPUTE_PROCESS_TERMS,
  /** Prenexing */
  COMPUTE_PRENEX,
  /** Variable elimination */
  COMPUTE_VAR_ELIMINATION,
  /** Conditional splitting */
  COMPUTE_COND_SPLIT,
  /** Placeholder for end of steps */
  COMPUTE_LAST
};
std::ostream& operator<<(std::ostream& out, RewriteStep s);

class QuantifiersRewriter : public TheoryRewriter
{
 public:
  static bool isLiteral( Node n );
  //-------------------------------------variable elimination utilities
  /** is variable elimination
   *
   * Returns true if v is not a subterm of s, and the type of s is a subtype of
   * the type of v.
   */
  static bool isVarElim(Node v, Node s);
  /** get variable elimination literal
   *
   * If n asserted with polarity pol is equivalent to an equality of the form
   * v = s for some v in args, where isVariableElim( v, s ) holds, then this
   * method removes v from args, adds v to vars, adds s to subs, and returns
   * true. Otherwise, it returns false.
   */
  static bool getVarElimLit(Node n,
                            bool pol,
                            std::vector<Node>& args,
                            std::vector<Node>& vars,
                            std::vector<Node>& subs);
  /**
   * Get variable eliminate for an equality based on theory-specific reasoning.
   */
  static Node getVarElimEq(Node lit, const std::vector<Node>& args, Node& var);
  /** variable eliminate for real equalities
   *
   * If this returns a non-null value ret, then var is updated to a member of
   * args, lit is equivalent to ( var = ret ).
   */
  static Node getVarElimEqReal(Node lit,
                               const std::vector<Node>& args,
                               Node& var);
  /** variable eliminate for bit-vector equalities
   *
   * If this returns a non-null value ret, then var is updated to a member of
   * args, lit is equivalent to ( var = ret ).
   */
  static Node getVarElimEqBv(Node lit,
                             const std::vector<Node>& args,
                             Node& var);
  /** variable eliminate for string equalities
   *
   * If this returns a non-null value ret, then var is updated to a member of
   * args, lit is equivalent to ( var = ret ).
   */
  static Node getVarElimEqString(Node lit,
                                 const std::vector<Node>& args,
                                 Node& var);
  /** get variable elimination
   *
   * If n asserted with polarity pol entails a literal lit that corresponds
   * to a variable elimination for some v via the above method, we return true.
   * In this case, we update args/vars/subs based on eliminating v.
   */
  static bool getVarElim(Node n,
                         bool pol,
                         std::vector<Node>& args,
                         std::vector<Node>& vars,
                         std::vector<Node>& subs);
  /** has variable elimination
   *
   * Returns true if n asserted with polarity pol entails a literal for
   * which variable elimination is possible.
   */
  static bool hasVarElim(Node n, bool pol, std::vector<Node>& args);
  /** compute variable elimination inequality
   *
   * This method eliminates variables from the body of quantified formula
   * "body" using (global) reasoning about inequalities. In particular, if there
   * exists a variable x that only occurs in body or annotation qa in literals
   * of the form x>=t with a fixed polarity P, then we may replace all such
   * literals with P. For example, note that:
   *   forall xy. x>y OR P(y) is equivalent to forall y. P(y).
   *
   * In the case that a variable x from args can be eliminated in this way,
   * we remove x from args, add x >= t1, ..., x >= tn to bounds, add false, ...,
   * false to subs, and return true.
   */
  static bool getVarElimIneq(Node body,
                             std::vector<Node>& args,
                             std::vector<Node>& bounds,
                             std::vector<Node>& subs,
                             QAttributes& qa);
  //-------------------------------------end variable elimination utilities
 private:
  static int getPurifyIdLit2(Node n, std::map<Node, int>& visited);
  static bool addCheckElimChild(std::vector<Node>& children,
                                Node c,
                                Kind k,
                                std::map<Node, bool>& lit_pol,
                                bool& childrenChanged);
  static void addNodeToOrBuilder(Node n, NodeBuilder& t);
  static void computeArgs(const std::vector<Node>& args,
                          std::map<Node, bool>& activeMap,
                          Node n,
                          std::map<Node, bool>& visited);
  static void computeArgVec(const std::vector<Node>& args,
                            std::vector<Node>& activeArgs,
                            Node n);
  static void computeArgVec2(const std::vector<Node>& args,
                             std::vector<Node>& activeArgs,
                             Node n,
                             Node ipl);
  static Node computeProcessTerms2(Node body,
                                   std::map<Node, Node>& cache,
                                   std::vector<Node>& new_vars,
                                   std::vector<Node>& new_conds);
  static void computeDtTesterIteSplit(
      Node n,
      std::map<Node, Node>& pcons,
      std::map<Node, std::map<int, Node> >& ncons,
      std::vector<Node>& conj);

  //-------------------------------------variable elimination
  /** compute variable elimination
   *
   * This computes variable elimination rewrites for a body of a quantified
   * formula with bound variables args. This method updates args to args' and
   * returns a node body' such that (forall args. body) is equivalent to
   * (forall args'. body'). An example of a variable elimination rewrite is:
   *   forall xy. x != a V P( x,y ) ---> forall y. P( a, y )
   */
  static Node computeVarElimination(Node body,
                                    std::vector<Node>& args,
                                    QAttributes& qa);
  //-------------------------------------end variable elimination
  //-------------------------------------conditional splitting
  /** compute conditional splitting
   *
   * This computes conditional splitting rewrites for a body of a quantified
   * formula with bound variables args. It returns a body' that is equivalent
   * to body. We split body into a conjunction if variable elimination can
   * occur in one of the conjuncts. Examples of this are:
   *   ite( x=a, P(x), Q(x) ) ----> ( x!=a V P(x) ) ^ ( x=a V Q(x) )
   *   (x=a) = P(x) ----> ( x!=a V P(x) ) ^ ( x=a V ~P(x) )
   *   ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
   * where in each case, x can be eliminated in the first conjunct.
   */
  static Node computeCondSplit(Node body,
                               const std::vector<Node>& args,
                               QAttributes& qa);
  //-------------------------------------end conditional splitting
  //------------------------------------- process terms
  /** compute process terms
   *
   * This takes as input a quantified formula q with attributes qa whose
   * body is body.
   *
   * This rewrite eliminates problematic terms from the bodies of
   * quantified formulas, which includes performing:
   * - Certain cases of ITE lifting,
   * - Elimination of extended arithmetic functions like to_int/is_int/div/mod,
   * - Elimination of select over store.
   *
   * It may introduce new variables V into new_vars and new conditions C into
   * new_conds. It returns a node retBody such that q of the form
   *   forall X. body
   * is equivalent to:
   *   forall X, V. ( C => retBody )
   */
  static Node computeProcessTerms(Node body,
                                  std::vector<Node>& new_vars,
                                  std::vector<Node>& new_conds,
                                  Node q,
                                  QAttributes& qa);
  //------------------------------------- end process terms
  //------------------------------------- extended rewrite
  /** compute extended rewrite
   *
   * This returns the result of applying the extended rewriter on the body
   * of quantified formula q.
   */
  static Node computeExtendedRewrite(Node q);
  //------------------------------------- end extended rewrite
 public:
  static Node computeElimSymbols( Node body );
  /**
   * Compute miniscoping in quantified formula q with attributes in qa.
   */
  static Node computeMiniscoping(Node q, QAttributes& qa);
  static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
  /**
   * This function removes top-level quantifiers from subformulas of body
   * appearing with overall polarity pol. It adds quantified variables that
   * appear in positive polarity positions into args, and those at negative
   * polarity positions in nargs.
   *
   * If prenexAgg is true, we ensure that all top-level quantifiers are
   * eliminated from subformulas. This means that we must expand ITE and
   * Boolean equalities to ensure that quantifiers are at fixed polarities.
   *
   * For example, calling this function on:
   *   (or (forall ((x Int)) (P x z)) (not (forall ((y Int)) (Q y z))))
   * would return:
   *   (or (P x z) (not (Q y z)))
   * and add {x} to args, and {y} to nargs.
   */
  static Node computePrenex(Node q,
                            Node body,
                            std::unordered_set<Node>& args,
                            std::unordered_set<Node>& nargs,
                            bool pol,
                            bool prenexAgg);
  /**
   * Apply prenexing aggressively. Returns the prenex normal form of n.
   */
  static Node computePrenexAgg(Node n, std::map<Node, Node>& visited);
  static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
private:
 static Node computeOperation(Node f,
                              RewriteStep computeOption,
                              QAttributes& qa);

public:
 RewriteResponse preRewrite(TNode in) override;
 RewriteResponse postRewrite(TNode in) override;

private:
  /** options */
 static bool doOperation(Node f, RewriteStep computeOption, QAttributes& qa);

private:
  static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
public:
  static bool isPrenexNormalForm( Node n );
  /** preprocess
   *
   * This returns the result of applying simple quantifiers-specific
   * preprocessing to n, including but not limited to:
   * - rewrite rule elimination,
   * - pre-skolemization,
   * - aggressive prenexing.
   * The argument isInst is set to true if n is an instance of a previously
   * registered quantified formula. If this flag is true, we do not apply
   * certain steps like pre-skolemization since we know they will have no
   * effect.
   *
   * The result is wrapped in a trust node of kind TrustNodeKind::REWRITE.
   */
  static TrustNode preprocess(Node n, bool isInst = false);
  static Node mkForAll(const std::vector<Node>& args,
                       Node body,
                       QAttributes& qa);
  static Node mkForall(const std::vector<Node>& args,
                       Node body,
                       bool marked = false);
  static Node mkForall(const std::vector<Node>& args,
                       Node body,
                       std::vector<Node>& iplc,
                       bool marked = false);
}; /* class QuantifiersRewriter */

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

#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Haniel Barbosa, Morgan Deters
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		* Rewriter for the theory of inductive quantifiers.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
19		#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
20
21		#include "proof/trust_node.h"
22		#include "theory/theory_rewriter.h"
23
24		namespace cvc5 {
25		namespace theory {
26		namespace quantifiers {
27
28		struct QAttributes;
29
30		/**
31		* List of steps used by the quantifiers rewriter, details on these steps
32		* can be found in the class below.
33		*/
34		enum RewriteStep
35		{
36		/** Eliminate symbols (e.g. implies, xor) */
37		COMPUTE_ELIM_SYMBOLS = 0,
38		/** Miniscoping */
39		COMPUTE_MINISCOPING,
40		/** Aggressive miniscoping */
41		COMPUTE_AGGRESSIVE_MINISCOPING,
42		/** Apply the extended rewriter to quantified formula bodies */
43		COMPUTE_EXT_REWRITE,
44		/**
45		* Term processing (e.g. simplifying terms based on ITE lifting,
46		* eliminating extended arithmetic symbols).
47		*/
48		COMPUTE_PROCESS_TERMS,
49		/** Prenexing */
50		COMPUTE_PRENEX,
51		/** Variable elimination */
52		COMPUTE_VAR_ELIMINATION,
53		/** Conditional splitting */
54		COMPUTE_COND_SPLIT,
55		/** Placeholder for end of steps */
56		COMPUTE_LAST
57		};
58		std::ostream& operator<<(std::ostream& out, RewriteStep s);
59
60	19712	class QuantifiersRewriter : public TheoryRewriter
61		{
62		public:
63		static bool isLiteral( Node n );
64		//-------------------------------------variable elimination utilities
65		/** is variable elimination
66		*
67		* Returns true if v is not a subterm of s, and the type of s is a subtype of
68		* the type of v.
69		*/
70		static bool isVarElim(Node v, Node s);
71		/** get variable elimination literal
72		*
73		* If n asserted with polarity pol is equivalent to an equality of the form
74		* v = s for some v in args, where isVariableElim( v, s ) holds, then this
75		* method removes v from args, adds v to vars, adds s to subs, and returns
76		* true. Otherwise, it returns false.
77		*/
78		static bool getVarElimLit(Node n,
79		bool pol,
80		std::vector<Node>& args,
81		std::vector<Node>& vars,
82		std::vector<Node>& subs);
83		/**
84		* Get variable eliminate for an equality based on theory-specific reasoning.
85		*/
86		static Node getVarElimEq(Node lit, const std::vector<Node>& args, Node& var);
87		/** variable eliminate for real equalities
88		*
89		* If this returns a non-null value ret, then var is updated to a member of
90		* args, lit is equivalent to ( var = ret ).
91		*/
92		static Node getVarElimEqReal(Node lit,
93		const std::vector<Node>& args,
94		Node& var);
95		/** variable eliminate for bit-vector equalities
96		*
97		* If this returns a non-null value ret, then var is updated to a member of
98		* args, lit is equivalent to ( var = ret ).
99		*/
100		static Node getVarElimEqBv(Node lit,
101		const std::vector<Node>& args,
102		Node& var);
103		/** variable eliminate for string equalities
104		*
105		* If this returns a non-null value ret, then var is updated to a member of
106		* args, lit is equivalent to ( var = ret ).
107		*/
108		static Node getVarElimEqString(Node lit,
109		const std::vector<Node>& args,
110		Node& var);
111		/** get variable elimination
112		*
113		* If n asserted with polarity pol entails a literal lit that corresponds
114		* to a variable elimination for some v via the above method, we return true.
115		* In this case, we update args/vars/subs based on eliminating v.
116		*/
117		static bool getVarElim(Node n,
118		bool pol,
119		std::vector<Node>& args,
120		std::vector<Node>& vars,
121		std::vector<Node>& subs);
122		/** has variable elimination
123		*
124		* Returns true if n asserted with polarity pol entails a literal for
125		* which variable elimination is possible.
126		*/
127		static bool hasVarElim(Node n, bool pol, std::vector<Node>& args);
128		/** compute variable elimination inequality
129		*
130		* This method eliminates variables from the body of quantified formula
131		* "body" using (global) reasoning about inequalities. In particular, if there
132		* exists a variable x that only occurs in body or annotation qa in literals
133		* of the form x>=t with a fixed polarity P, then we may replace all such
134		* literals with P. For example, note that:
135		* forall xy. x>y OR P(y) is equivalent to forall y. P(y).
136		*
137		* In the case that a variable x from args can be eliminated in this way,
138		* we remove x from args, add x >= t1, ..., x >= tn to bounds, add false, ...,
139		* false to subs, and return true.
140		*/
141		static bool getVarElimIneq(Node body,
142		std::vector<Node>& args,
143		std::vector<Node>& bounds,
144		std::vector<Node>& subs,
145		QAttributes& qa);
146		//-------------------------------------end variable elimination utilities
147		private:
148		static int getPurifyIdLit2(Node n, std::map<Node, int>& visited);
149		static bool addCheckElimChild(std::vector<Node>& children,
150		Node c,
151		Kind k,
152		std::map<Node, bool>& lit_pol,
153		bool& childrenChanged);
154		static void addNodeToOrBuilder(Node n, NodeBuilder& t);
155		static void computeArgs(const std::vector<Node>& args,
156		std::map<Node, bool>& activeMap,
157		Node n,
158		std::map<Node, bool>& visited);
159		static void computeArgVec(const std::vector<Node>& args,
160		std::vector<Node>& activeArgs,
161		Node n);
162		static void computeArgVec2(const std::vector<Node>& args,
163		std::vector<Node>& activeArgs,
164		Node n,
165		Node ipl);
166		static Node computeProcessTerms2(Node body,
167		std::map<Node, Node>& cache,
168		std::vector<Node>& new_vars,
169		std::vector<Node>& new_conds);
170		static void computeDtTesterIteSplit(
171		Node n,
172		std::map<Node, Node>& pcons,
173		std::map<Node, std::map<int, Node> >& ncons,
174		std::vector<Node>& conj);
175
176		//-------------------------------------variable elimination
177		/** compute variable elimination
178		*
179		* This computes variable elimination rewrites for a body of a quantified
180		* formula with bound variables args. This method updates args to args' and
181		* returns a node body' such that (forall args. body) is equivalent to
182		* (forall args'. body'). An example of a variable elimination rewrite is:
183		* forall xy. x != a V P( x,y ) ---> forall y. P( a, y )
184		*/
185		static Node computeVarElimination(Node body,
186		std::vector<Node>& args,
187		QAttributes& qa);
188		//-------------------------------------end variable elimination
189		//-------------------------------------conditional splitting
190		/** compute conditional splitting
191		*
192		* This computes conditional splitting rewrites for a body of a quantified
193		* formula with bound variables args. It returns a body' that is equivalent
194		* to body. We split body into a conjunction if variable elimination can
195		* occur in one of the conjuncts. Examples of this are:
196		* ite( x=a, P(x), Q(x) ) ----> ( x!=a V P(x) ) ^ ( x=a V Q(x) )
197		* (x=a) = P(x) ----> ( x!=a V P(x) ) ^ ( x=a V ~P(x) )
198		* ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
199		* where in each case, x can be eliminated in the first conjunct.
200		*/
201		static Node computeCondSplit(Node body,
202		const std::vector<Node>& args,
203		QAttributes& qa);
204		//-------------------------------------end conditional splitting
205		//------------------------------------- process terms
206		/** compute process terms
207		*
208		* This takes as input a quantified formula q with attributes qa whose
209		* body is body.
210		*
211		* This rewrite eliminates problematic terms from the bodies of
212		* quantified formulas, which includes performing:
213		* - Certain cases of ITE lifting,
214		* - Elimination of extended arithmetic functions like to_int/is_int/div/mod,
215		* - Elimination of select over store.
216		*
217		* It may introduce new variables V into new_vars and new conditions C into
218		* new_conds. It returns a node retBody such that q of the form
219		* forall X. body
220		* is equivalent to:
221		* forall X, V. ( C => retBody )
222		*/
223		static Node computeProcessTerms(Node body,
224		std::vector<Node>& new_vars,
225		std::vector<Node>& new_conds,
226		Node q,
227		QAttributes& qa);
228		//------------------------------------- end process terms
229		//------------------------------------- extended rewrite
230		/** compute extended rewrite
231		*
232		* This returns the result of applying the extended rewriter on the body
233		* of quantified formula q.
234		*/
235		static Node computeExtendedRewrite(Node q);
236		//------------------------------------- end extended rewrite
237		public:
238		static Node computeElimSymbols( Node body );
239		/**
240		* Compute miniscoping in quantified formula q with attributes in qa.
241		*/
242		static Node computeMiniscoping(Node q, QAttributes& qa);
243		static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
244		/**
245		* This function removes top-level quantifiers from subformulas of body
246		* appearing with overall polarity pol. It adds quantified variables that
247		* appear in positive polarity positions into args, and those at negative
248		* polarity positions in nargs.
249		*
250		* If prenexAgg is true, we ensure that all top-level quantifiers are
251		* eliminated from subformulas. This means that we must expand ITE and
252		* Boolean equalities to ensure that quantifiers are at fixed polarities.
253		*
254		* For example, calling this function on:
255		* (or (forall ((x Int)) (P x z)) (not (forall ((y Int)) (Q y z))))
256		* would return:
257		* (or (P x z) (not (Q y z)))
258		* and add {x} to args, and {y} to nargs.
259		*/
260		static Node computePrenex(Node q,
261		Node body,
262		std::unordered_set<Node>& args,
263		std::unordered_set<Node>& nargs,
264		bool pol,
265		bool prenexAgg);
266		/**
267		* Apply prenexing aggressively. Returns the prenex normal form of n.
268		*/
269		static Node computePrenexAgg(Node n, std::map<Node, Node>& visited);
270		static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
271		private:
272		static Node computeOperation(Node f,
273		RewriteStep computeOption,
274		QAttributes& qa);
275
276		public:
277		RewriteResponse preRewrite(TNode in) override;
278		RewriteResponse postRewrite(TNode in) override;
279
280		private:
281		/** options */
282		static bool doOperation(Node f, RewriteStep computeOption, QAttributes& qa);
283
284		private:
285		static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
286		public:
287		static bool isPrenexNormalForm( Node n );
288		/** preprocess
289		*
290		* This returns the result of applying simple quantifiers-specific
291		* preprocessing to n, including but not limited to:
292		* - rewrite rule elimination,
293		* - pre-skolemization,
294		* - aggressive prenexing.
295		* The argument isInst is set to true if n is an instance of a previously
296		* registered quantified formula. If this flag is true, we do not apply
297		* certain steps like pre-skolemization since we know they will have no
298		* effect.
299		*
300		* The result is wrapped in a trust node of kind TrustNodeKind::REWRITE.
301		*/
302		static TrustNode preprocess(Node n, bool isInst = false);
303		static Node mkForAll(const std::vector<Node>& args,
304		Node body,
305		QAttributes& qa);
306		static Node mkForall(const std::vector<Node>& args,
307		Node body,
308		bool marked = false);
309		static Node mkForall(const std::vector<Node>& args,
310		Node body,
311		std::vector<Node>& iplc,
312		bool marked = false);
313		}; /* class QuantifiersRewriter */
314
315		} // namespace quantifiers
316		} // namespace theory
317		} // namespace cvc5
318
319		#endif /* CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */