src/theory/quantifiers/quant_module.h

   1 /*********************                                                        */
   2 /*! \file quant_module.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-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.\endverbatim
  11  **
  12  ** \brief quantifier module
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__QUANT_MODULE_H
  18 #define CVC4__THEORY__QUANT_MODULE_H
  19
  20 #include <iostream>
  21 #include <map>
  22 #include <vector>
  23
  24 #include "theory/quantifiers/quantifiers_inference_manager.h"
  25 #include "theory/quantifiers/quantifiers_registry.h"
  26 #include "theory/quantifiers/quantifiers_state.h"
  27 #include "theory/theory.h"
  28 #include "theory/uf/equality_engine.h"
  29
  30 namespace CVC4 {
  31 namespace theory {
  32
  33 class QuantifiersEngine;
  34
  35 namespace quantifiers {
  36 class TermDb;
  37 }  // namespace quantifiers
  38
  39 /** QuantifiersModule class
  40  *
  41  * This is the virtual class for defining subsolvers of the quantifiers theory.
  42  * It has a similar interface to a Theory object.
  43  */
  44 class QuantifiersModule
  45 {
  46  public:
  47   /** effort levels for quantifiers modules check */
  48   enum QEffort
  49   {
  50     // conflict effort, for conflict-based instantiation
  51     QEFFORT_CONFLICT,
  52     // standard effort, for heuristic instantiation
  53     QEFFORT_STANDARD,
  54     // model effort, for model-based instantiation
  55     QEFFORT_MODEL,
  56     // last call effort, for last resort techniques
  57     QEFFORT_LAST_CALL,
  58     // none
  59     QEFFORT_NONE,
  60   };
  61
  62  public:
  63   QuantifiersModule(quantifiers::QuantifiersState& qs,
  64                     quantifiers::QuantifiersInferenceManager& qim,
  65                     quantifiers::QuantifiersRegistry& qr,
  66                     QuantifiersEngine* qe);
  67   virtual ~QuantifiersModule() {}
  68   /** Presolve.
  69    *
  70    * Called at the beginning of check-sat call.
  71    */
  72   virtual void presolve() {}
  73   /** Needs check.
  74    *
  75    * Returns true if this module wishes a call to be made
  76    * to check(e) during QuantifiersEngine::check(e).
  77    */
  78   virtual bool needsCheck(Theory::Effort e)
  79   {
  80     return e >= Theory::EFFORT_LAST_CALL;
  81   }
  82   /** Needs model.
  83    *
  84    * Whether this module needs a model built during a
  85    * call to QuantifiersEngine::check(e)
  86    * It returns one of QEFFORT_* from quantifiers_engine.h,
  87    * which specifies the quantifiers effort in which it requires the model to
  88    * be built.
  89    */
  90   virtual QEffort needsModel(Theory::Effort e);
  91   /** Reset.
  92    *
  93    * Called at the beginning of QuantifiersEngine::check(e).
  94    */
  95   virtual void reset_round(Theory::Effort e) {}
  96   /** Check.
  97    *
  98    *   Called during QuantifiersEngine::check(e) depending
  99    *   if needsCheck(e) returns true.
 100    */
 101   virtual void check(Theory::Effort e, QEffort quant_e) = 0;
 102   /** Check complete?
 103    *
 104    * Returns false if the module's reasoning was globally incomplete
 105    * (e.g. "sat" must be replaced with "incomplete").
 106    *
 107    * This is called just before the quantifiers engine will return
 108    * with no lemmas added during a LAST_CALL effort check.
 109    */
 110   virtual bool checkComplete() { return true; }
 111   /** Check was complete for quantified formula q
 112    *
 113    * If for each quantified formula q, some module returns true for
 114    * checkCompleteFor( q ),
 115    * and no lemmas are added by the quantifiers theory, then we may answer
 116    * "sat", unless
 117    * we are incomplete for other reasons.
 118    */
 119   virtual bool checkCompleteFor(Node q) { return false; }
 120   /** Check ownership
 121    *
 122    * Called once for new quantified formulas that are registered by the
 123    * quantifiers theory. The primary purpose of this function is to establish
 124    * if this module is the owner of quantified formula q.
 125    */
 126   virtual void checkOwnership(Node q) {}
 127   /** Register quantifier
 128    *
 129    * Called once for new quantified formulas q that are pre-registered by the
 130    * quantifiers theory, after internal ownership of quantified formulas is
 131    * finalized. This does context-independent initialization of this module
 132    * for quantified formula q.
 133    */
 134   virtual void registerQuantifier(Node q) {}
 135   /** Pre-register quantifier
 136    *
 137    * Called once for new quantified formulas that are
 138    * pre-registered by the quantifiers theory, after
 139    * internal ownership of quantified formulas is finalized.
 140    */
 141   virtual void preRegisterQuantifier(Node q) {}
 142   /** Assert node.
 143    *
 144    * Called when a quantified formula q is asserted to the quantifiers theory
 145    */
 146   virtual void assertNode(Node q) {}
 147   /** Identify this module (for debugging, dynamic configuration, etc..) */
 148   virtual std::string identify() const = 0;
 149   //----------------------------general queries
 150   /** get currently used the equality engine */
 151   eq::EqualityEngine* getEqualityEngine() const;
 152   /** are n1 and n2 equal in the current used equality engine? */
 153   bool areEqual(TNode n1, TNode n2) const;
 154   /** are n1 and n2 disequal in the current used equality engine? */
 155   bool areDisequal(TNode n1, TNode n2) const;
 156   /** get the representative of n in the current used equality engine */
 157   TNode getRepresentative(TNode n) const;
 158   /** get quantifiers engine that owns this module */
 159   QuantifiersEngine* getQuantifiersEngine() const;
 160   /** get currently used term database */
 161   quantifiers::TermDb* getTermDatabase() const;
 162   /** get the quantifiers state */
 163   quantifiers::QuantifiersState& getState();
 164   /** get the quantifiers inference manager */
 165   quantifiers::QuantifiersInferenceManager& getInferenceManager();
 166   /** get the quantifiers registry */
 167   quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
 168   //----------------------------end general queries
 169  protected:
 170   /** pointer to the quantifiers engine that owns this module */
 171   QuantifiersEngine* d_quantEngine;
 172   /** The state of the quantifiers engine */
 173   quantifiers::QuantifiersState& d_qstate;
 174   /** The quantifiers inference manager */
 175   quantifiers::QuantifiersInferenceManager& d_qim;
 176   /** The quantifiers registry */
 177   quantifiers::QuantifiersRegistry& d_qreg;
 178 }; /* class QuantifiersModule */
 179
 180 }  // namespace theory
 181 }  // namespace CVC4
 182
 183 #endif /* CVC4__THEORY__QUANT_UTIL_H */