Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/quantifiers/inst_strategy_enumerative.h	Lines:	3	3	100.0 %
Date:	2021-05-22	Branches:	1	2	50.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.
 * ****************************************************************************
 *
 * Enumerative instantiation.
 */

#include "cvc5_private.h"

#ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H
#define CVC5__INST_STRATEGY_ENUMERATIVE_H

#include "theory/quantifiers/quant_module.h"

namespace cvc5 {
namespace theory {
namespace quantifiers {

class RelevantDomain;

/** Enumerative instantiation
 *
 * This class implements enumerative instantiation described
 * in Reynolds et al., "Revisiting Enumerative Instantiation".
 *
 * It is an instance of QuantifiersModule, whose main
 * task is to make calls to QuantifiersEngine during
 * calls to QuantifiersModule::check(...).
 *
 * This class adds instantiations based on enumerating
 * well-typed terms that occur in the current context
 * based on a heuristically determined ordering on
 * tuples of terms. This ordering incorporates
 * reasoning about the relevant domain of quantified
 * formulas (see theory/quantifiers/relevant_domain.h).
 * We consider only ground terms that occur in the
 * context due to Theorem 1 of "Revisiting Enumerative
 * Instantiation". Notice this theorem holds only for theories
 * with compactness. For theories such as arithmetic,
 * this class may introduce "default" terms that are
 * used in instantiations, say 0 for arithmetic, even
 * when the term 0 does not occur in the context.
 *
 * This strategy is not enabled by default, and
 * is enabled by the option:
 *   --full-saturate-quant
 *
 * It is generally called with lower priority than
 * other instantiation strategies, although this
 * option interleaves it with other strategies
 * during quantifier effort level QEFFORT_STANDARD:
 *   --fs-interleave
 */
class InstStrategyEnum : public QuantifiersModule
{
 public:
  InstStrategyEnum(QuantifiersState& qs,
                   QuantifiersInferenceManager& qim,
                   QuantifiersRegistry& qr,
                   TermRegistry& tr,
                   RelevantDomain* rd);
  ~InstStrategyEnum() {}
  /** Presolve */
  void presolve() override;
  /** Needs check. */
  bool needsCheck(Theory::Effort e) override;
  /** Reset round. */
  void reset_round(Theory::Effort e) override;
  /** Check.
   * Adds instantiations for all currently asserted
   * quantified formulas via calls to process(...)
   */
  void check(Theory::Effort e, QEffort quant_e) override;
  /** Identify. */
  std::string identify() const override
  {
    return std::string("InstStrategyEnum");
  }

 private:
  /** Pointer to the relevant domain utility of quantifiers engine */
  RelevantDomain* d_rd;
  /** process quantified formula
   *
   * q is the quantified formula we are constructing instances for.
   * fullEffort is whether we are called at full effort.
   *
   * If this function returns true, then one instantiation
   * (determined by an enumeration) was added via a successful
   * call to QuantifiersEngine::addInstantiation(...).
   *
   * If fullEffort is true, then we may introduce a "default"
   * well-typed term *not* occurring in the current context.
   * This handles corner cases where there are no well-typed
   * ground terms in the current context to instantiate with.
   *
   * The flag isRd indicates whether we are trying relevant domain
   * instantiations. If this flag is false, we are trying arbitrary ground
   * term instantiations.
   */
  bool process(Node q, bool fullEffort, bool isRd);
  /**
   * A limit on the number of rounds to apply this strategy, where a value < 0
   * means no limit. This value is set to the value of fullSaturateLimit()
   * during presolve.
   */
  int32_t d_fullSaturateLimit;
}; /* class InstStrategyEnum */

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

#endif


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		* Enumerative instantiation.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__INST_STRATEGY_ENUMERATIVE_H
19		#define CVC5__INST_STRATEGY_ENUMERATIVE_H
20
21		#include "theory/quantifiers/quant_module.h"
22
23		namespace cvc5 {
24		namespace theory {
25		namespace quantifiers {
26
27		class RelevantDomain;
28
29		/** Enumerative instantiation
30		*
31		* This class implements enumerative instantiation described
32		* in Reynolds et al., "Revisiting Enumerative Instantiation".
33		*
34		* It is an instance of QuantifiersModule, whose main
35		* task is to make calls to QuantifiersEngine during
36		* calls to QuantifiersModule::check(...).
37		*
38		* This class adds instantiations based on enumerating
39		* well-typed terms that occur in the current context
40		* based on a heuristically determined ordering on
41		* tuples of terms. This ordering incorporates
42		* reasoning about the relevant domain of quantified
43		* formulas (see theory/quantifiers/relevant_domain.h).
44		* We consider only ground terms that occur in the
45		* context due to Theorem 1 of "Revisiting Enumerative
46		* Instantiation". Notice this theorem holds only for theories
47		* with compactness. For theories such as arithmetic,
48		* this class may introduce "default" terms that are
49		* used in instantiations, say 0 for arithmetic, even
50		* when the term 0 does not occur in the context.
51		*
52		* This strategy is not enabled by default, and
53		* is enabled by the option:
54		* --full-saturate-quant
55		*
56		* It is generally called with lower priority than
57		* other instantiation strategies, although this
58		* option interleaves it with other strategies
59		* during quantifier effort level QEFFORT_STANDARD:
60		* --fs-interleave
61		*/
62		class InstStrategyEnum : public QuantifiersModule
63		{
64		public:
65		InstStrategyEnum(QuantifiersState& qs,
66		QuantifiersInferenceManager& qim,
67		QuantifiersRegistry& qr,
68		TermRegistry& tr,
69		RelevantDomain* rd);
70	166	~InstStrategyEnum() {}
71		/** Presolve */
72		void presolve() override;
73		/** Needs check. */
74		bool needsCheck(Theory::Effort e) override;
75		/** Reset round. */
76		void reset_round(Theory::Effort e) override;
77		/** Check.
78		* Adds instantiations for all currently asserted
79		* quantified formulas via calls to process(...)
80		*/
81		void check(Theory::Effort e, QEffort quant_e) override;
82		/** Identify. */
83	13120	std::string identify() const override
84		{
85	13120	return std::string("InstStrategyEnum");
86		}
87
88		private:
89		/** Pointer to the relevant domain utility of quantifiers engine */
90		RelevantDomain* d_rd;
91		/** process quantified formula
92		*
93		* q is the quantified formula we are constructing instances for.
94		* fullEffort is whether we are called at full effort.
95		*
96		* If this function returns true, then one instantiation
97		* (determined by an enumeration) was added via a successful
98		* call to QuantifiersEngine::addInstantiation(...).
99		*
100		* If fullEffort is true, then we may introduce a "default"
101		* well-typed term not occurring in the current context.
102		* This handles corner cases where there are no well-typed
103		* ground terms in the current context to instantiate with.
104		*
105		* The flag isRd indicates whether we are trying relevant domain
106		* instantiations. If this flag is false, we are trying arbitrary ground
107		* term instantiations.
108		*/
109		bool process(Node q, bool fullEffort, bool isRd);
110		/**
111		* A limit on the number of rounds to apply this strategy, where a value < 0
112		* means no limit. This value is set to the value of fullSaturateLimit()
113		* during presolve.
114		*/
115		int32_t d_fullSaturateLimit;
116		}; /* class InstStrategyEnum */
117
118		} // namespace quantifiers
119		} // namespace theory
120		} // namespace cvc5
121
122		#endif