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