Head

GCC Code Coverage Report

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