1 /*********************                                                        */
2 /*! \file inst_strategy_enumerative.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Andrew Reynolds
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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.\endverbatim
11  **
12  ** \brief Enumerative instantiation
13  **/
14 
15 #include "cvc4_private.h"
16 
17 #ifndef __CVC4__INST_STRATEGY_ENUMERATIVE_H
18 #define __CVC4__INST_STRATEGY_ENUMERATIVE_H
19 
20 #include "context/context.h"
21 #include "context/context_mm.h"
22 #include "theory/quantifiers_engine.h"
23 
24 namespace CVC4 {
25 namespace theory {
26 namespace quantifiers {
27 
28 /** Enumerative instantiation
29  *
30  * This class implements enumerative instantiation described
31  * in Reynolds et al., "Revisiting Enumerative Instantiation".
32  *
33  * It is an instance of QuantifiersModule, whose main
34  * task is to make calls to QuantifiersEngine during
35  * calls to QuantifiersModule::check(...).
36  *
37  * This class adds instantiations based on enumerating
38  * well-typed terms that occur in the current context
39  * based on a heuristically determined ordering on
40  * tuples of terms. This ordering incorporates
41  * reasoning about the relevant domain of quantified
42  * formulas (see theory/quantifiers/relevant_domain.h).
43  * We consider only ground terms that occur in the
44  * context due to Theorem 1 of "Revisiting Enumerative
45  * Instantiation". Notice this theorem holds only for theories
46  * with compactness. For theories such as arithmetic,
47  * this class may introduce "default" terms that are
48  * used in instantiations, say 0 for arithmetic, even
49  * when the term 0 does not occur in the context.
50  *
51  * This strategy is not enabled by default, and
52  * is enabled by the option:
53  *   --full-saturate-quant
54  *
55  * It is generally called with lower priority than
56  * other instantiation strategies, although this
57  * option interleaves it with other strategies
58  * during quantifier effort level QEFFORT_STANDARD:
59  *   --fs-interleave
60  */
61 class InstStrategyEnum : public QuantifiersModule
62 {
63  public:
64   InstStrategyEnum(QuantifiersEngine* qe);
~InstStrategyEnum()65   ~InstStrategyEnum() {}
66   /** Needs check. */
67   bool needsCheck(Theory::Effort e) override;
68   /** Reset round. */
69   void reset_round(Theory::Effort e) override;
70   /** Check.
71    * Adds instantiations for all currently asserted
72    * quantified formulas via calls to process(...)
73    */
74   void check(Theory::Effort e, QEffort quant_e) override;
75   /** Identify. */
identify()76   std::string identify() const override
77   {
78     return std::string("InstStrategyEnum");
79   }
80 
81  private:
82   /** process quantified formula
83    *
84    * q is the quantified formula we are constructing instances for.
85    * fullEffort is whether we are called at full effort.
86    *
87    * If this function returns true, then one instantiation
88    * (determined by an enumeration) was added via a successful
89    * call to QuantifiersEngine::addInstantiation(...).
90    *
91    * If fullEffort is true, then we may introduce a "default"
92    * well-typed term *not* occurring in the current context.
93    * This handles corner cases where there are no well-typed
94    * ground terms in the current context to instantiate with.
95    */
96   bool process(Node q, bool fullEffort);
97 }; /* class InstStrategyEnum */
98 
99 } /* CVC4::theory::quantifiers namespace */
100 } /* CVC4::theory namespace */
101 } /* CVC4 namespace */
102 
103 #endif
104