Head

GCC Code Coverage Report

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


/******************************************************************************
 * Top contributors (to current version):
 *   Yoni Zohar, 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 detecting quantifier macro definitions.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MACROS_H
#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MACROS_H

#include <map>
#include <vector>
#include "expr/node.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class QuantifiersRegistry;

/**
 * A utility for inferring macros from quantified formulas. This can be seen as
 * a method for putting quantified formulas in solved form, e.g.
 *   forall x. P(x) ---> P = (lambda x. true)
 */
class QuantifiersMacros
{
 public:
  QuantifiersMacros(QuantifiersRegistry& qr);
  ~QuantifiersMacros() {}
  /**
   * Called on quantified formulas lit of the form
   *   forall x1 ... xn. n = ndef
   * where n is of the form U(x1...xn). Returns an equality of the form
   *   U = lambda x1 ... xn. ndef
   * if this is a legal macro definition for U, and the null node otherwise.
   *
   * @param lit The body of the quantified formula
   * @param reqGround Whether we require the macro definition to be ground,
   * i.e. does not contain quantified formulas as subterms.
   * @return If a macro can be inferred, an equality of the form
   * (op = lambda x1 ... xn. def)), or the null node otherwise.
   */
  Node solve(Node lit, bool reqGround = false);

 private:
  /**
   * Return true n is an APPLY_UF with pairwise unique BOUND_VARIABLE as
   * children.
   */
  bool isBoundVarApplyUf(Node n);
  /**
   * Returns true if n contains op, or if n contains a quantified formula
   * as a subterm and reqGround is true.
   */
  bool containsBadOp(Node n, Node op, bool reqGround);
  /**
   * Return true if n preserves trigger variables in quantified formula q, that
   * is, triggers can be inferred containing all variables in q in term n.
   */
  bool preservesTriggerVariables(Node q, Node n);
  /**
   * From n, get a list of possible subterms of n that could be the head of a
   * macro definition.
   */
  void getMacroCandidates(Node n,
                          std::vector<Node>& candidates,
                          std::map<Node, bool>& visited);
  /**
   * Solve n in literal lit, return n' such that n = n' is equivalent to lit
   * if possible, or null otherwise.
   */
  Node solveInEquality(Node n, Node lit);
  /**
   * Called when we have inferred a quantified formula is of the form
   *   forall x1 ... xn. n = ndef
   * where n is of the form U(x1...xn).
   */
  Node solveEq(Node n, Node ndef);
  /**
   * Returns the macro fdef, which originated from lit. This method is for
   * debugging.
   */
  Node returnMacro(Node fdef, Node lit) const;
  /** Reference to the quantifiers registry */
  QuantifiersRegistry& d_qreg;
};

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

#endif /*CVC5__THEORY__QUANTIFIERS__QUANTIFIER_MACROS_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Yoni Zohar, 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 detecting quantifier macro definitions.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MACROS_H
19		#define CVC5__THEORY__QUANTIFIERS__QUANTIFIERS_MACROS_H
20
21		#include <map>
22		#include <vector>
23		#include "expr/node.h"
24
25		namespace cvc5 {
26		namespace theory {
27		namespace quantifiers {
28
29		class QuantifiersRegistry;
30
31		/**
32		* A utility for inferring macros from quantified formulas. This can be seen as
33		* a method for putting quantified formulas in solved form, e.g.
34		* forall x. P(x) ---> P = (lambda x. true)
35		*/
36		class QuantifiersMacros
37		{
38		public:
39		QuantifiersMacros(QuantifiersRegistry& qr);
40	22	~QuantifiersMacros() {}
41		/**
42		* Called on quantified formulas lit of the form
43		* forall x1 ... xn. n = ndef
44		* where n is of the form U(x1...xn). Returns an equality of the form
45		* U = lambda x1 ... xn. ndef
46		* if this is a legal macro definition for U, and the null node otherwise.
47		*
48		* @param lit The body of the quantified formula
49		* @param reqGround Whether we require the macro definition to be ground,
50		* i.e. does not contain quantified formulas as subterms.
51		* @return If a macro can be inferred, an equality of the form
52		* (op = lambda x1 ... xn. def)), or the null node otherwise.
53		*/
54		Node solve(Node lit, bool reqGround = false);
55
56		private:
57		/**
58		* Return true n is an APPLY_UF with pairwise unique BOUND_VARIABLE as
59		* children.
60		*/
61		bool isBoundVarApplyUf(Node n);
62		/**
63		* Returns true if n contains op, or if n contains a quantified formula
64		* as a subterm and reqGround is true.
65		*/
66		bool containsBadOp(Node n, Node op, bool reqGround);
67		/**
68		* Return true if n preserves trigger variables in quantified formula q, that
69		* is, triggers can be inferred containing all variables in q in term n.
70		*/
71		bool preservesTriggerVariables(Node q, Node n);
72		/**
73		* From n, get a list of possible subterms of n that could be the head of a
74		* macro definition.
75		*/
76		void getMacroCandidates(Node n,
77		std::vector<Node>& candidates,
78		std::map<Node, bool>& visited);
79		/**
80		* Solve n in literal lit, return n' such that n = n' is equivalent to lit
81		* if possible, or null otherwise.
82		*/
83		Node solveInEquality(Node n, Node lit);
84		/**
85		* Called when we have inferred a quantified formula is of the form
86		* forall x1 ... xn. n = ndef
87		* where n is of the form U(x1...xn).
88		*/
89		Node solveEq(Node n, Node ndef);
90		/**
91		* Returns the macro fdef, which originated from lit. This method is for
92		* debugging.
93		*/
94		Node returnMacro(Node fdef, Node lit) const;
95		/** Reference to the quantifiers registry */
96		QuantifiersRegistry& d_qreg;
97		};
98
99		} // namespace quantifiers
100		} // namespace theory
101		} // namespace cvc5
102
103		#endif /CVC5__THEORY__QUANTIFIERS__QUANTIFIER_MACROS_H /