src/theory/quantifiers/quant_util.h

   1 /*********************                                                        */
   2 /*! \file quant_util.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 util
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__QUANT_UTIL_H
  18 #define CVC4__THEORY__QUANT_UTIL_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   class TermUtil;
  38 }
  39
  40 /** QuantifiersModule class
  41 *
  42 * This is the virtual class for defining subsolvers of the quantifiers theory.
  43 * It has a similar interface to a Theory object.
  44 */
  45 class QuantifiersModule {
  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 ) { return e>=Theory::EFFORT_LAST_CALL; }
  79   /** Needs model.
  80    *
  81    * Whether this module needs a model built during a
  82    * call to QuantifiersEngine::check(e)
  83    * It returns one of QEFFORT_* from quantifiers_engine.h,
  84    * which specifies the quantifiers effort in which it requires the model to
  85    * be built.
  86    */
  87   virtual QEffort needsModel(Theory::Effort e);
  88   /** Reset.
  89    *
  90    * Called at the beginning of QuantifiersEngine::check(e).
  91    */
  92   virtual void reset_round( Theory::Effort e ){}
  93   /** Check.
  94    *
  95    *   Called during QuantifiersEngine::check(e) depending
  96    *   if needsCheck(e) returns true.
  97    */
  98   virtual void check(Theory::Effort e, QEffort quant_e) = 0;
  99   /** Check complete?
 100    *
 101    * Returns false if the module's reasoning was globally incomplete
 102    * (e.g. "sat" must be replaced with "incomplete").
 103    *
 104    * This is called just before the quantifiers engine will return
 105    * with no lemmas added during a LAST_CALL effort check.
 106    */
 107   virtual bool checkComplete() { return true; }
 108   /** Check was complete for quantified formula q
 109    *
 110    * If for each quantified formula q, some module returns true for
 111    * checkCompleteFor( q ),
 112    * and no lemmas are added by the quantifiers theory, then we may answer
 113    * "sat", unless
 114    * we are incomplete for other reasons.
 115    */
 116   virtual bool checkCompleteFor( Node q ) { return false; }
 117   /** Check ownership
 118    *
 119    * Called once for new quantified formulas that are registered by the
 120    * quantifiers theory. The primary purpose of this function is to establish
 121    * if this module is the owner of quantified formula q.
 122    */
 123   virtual void checkOwnership(Node q) {}
 124   /** Register quantifier
 125    *
 126    * Called once for new quantified formulas q that are pre-registered by the
 127    * quantifiers theory, after internal ownership of quantified formulas is
 128    * finalized. This does context-independent initialization of this module
 129    * for quantified formula q.
 130    */
 131   virtual void registerQuantifier(Node q) {}
 132   /** Pre-register quantifier
 133    *
 134    * Called once for new quantified formulas that are
 135    * pre-registered by the quantifiers theory, after
 136    * internal ownership of quantified formulas is finalized.
 137    */
 138   virtual void preRegisterQuantifier(Node q) {}
 139   /** Assert node.
 140    *
 141    * Called when a quantified formula q is asserted to the quantifiers theory
 142    */
 143   virtual void assertNode(Node q) {}
 144   /** Identify this module (for debugging, dynamic configuration, etc..) */
 145   virtual std::string identify() const = 0;
 146   //----------------------------general queries
 147   /** get currently used the equality engine */
 148   eq::EqualityEngine* getEqualityEngine() const;
 149   /** are n1 and n2 equal in the current used equality engine? */
 150   bool areEqual(TNode n1, TNode n2) const;
 151   /** are n1 and n2 disequal in the current used equality engine? */
 152   bool areDisequal(TNode n1, TNode n2) const;
 153   /** get the representative of n in the current used equality engine */
 154   TNode getRepresentative(TNode n) const;
 155   /** get quantifiers engine that owns this module */
 156   QuantifiersEngine* getQuantifiersEngine() const;
 157   /** get currently used term database */
 158   quantifiers::TermDb* getTermDatabase() const;
 159   /** get currently used term utility object */
 160   quantifiers::TermUtil* getTermUtil() const;
 161   /** get the quantifiers state */
 162   quantifiers::QuantifiersState& getState();
 163   /** get the quantifiers inference manager */
 164   quantifiers::QuantifiersInferenceManager& getInferenceManager();
 165   //----------------------------end general queries
 166  protected:
 167   /** pointer to the quantifiers engine that owns this module */
 168   QuantifiersEngine* d_quantEngine;
 169   /** The state of the quantifiers engine */
 170   quantifiers::QuantifiersState& d_qstate;
 171   /** The quantifiers inference manager */
 172   quantifiers::QuantifiersInferenceManager& d_qim;
 173   /** The quantifiers registry */
 174   quantifiers::QuantifiersRegistry& d_qreg;
 175 };/* class QuantifiersModule */
 176
 177 /** Quantifiers utility
 178 *
 179 * This is a lightweight version of a quantifiers module that does not implement
 180 * methods
 181 * for checking satisfiability.
 182 */
 183 class QuantifiersUtil {
 184 public:
 185   QuantifiersUtil(){}
 186   virtual ~QuantifiersUtil(){}
 187   /* reset
 188    * Called at the beginning of an instantiation round
 189    * Returns false if the reset failed. When reset fails, the utility should
 190    * have added a lemma via a call to d_qim.addPendingLemma.
 191    */
 192   virtual bool reset( Theory::Effort e ) = 0;
 193   /* Called for new quantifiers */
 194   virtual void registerQuantifier(Node q) = 0;
 195   /** Identify this module (for debugging, dynamic configuration, etc..) */
 196   virtual std::string identify() const = 0;
 197   /** Check complete?
 198    *
 199    * Returns false if the utility's reasoning was globally incomplete
 200    * (e.g. "sat" must be replaced with "incomplete").
 201    */
 202   virtual bool checkComplete() { return true; }
 203 };
 204
 205 class QuantPhaseReq
 206 {
 207 private:
 208   /** helper functions compute phase requirements */
 209   void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs );
 210 public:
 211   QuantPhaseReq(){}
 212   QuantPhaseReq( Node n, bool computeEq = false );
 213   ~QuantPhaseReq(){}
 214   void initialize( Node n, bool computeEq );
 215   /** is phase required */
 216   bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); }
 217   /** get phase requirement */
 218   bool getPhaseReq( Node lit ) { return d_phase_reqs.find( lit )==d_phase_reqs.end() ? false : d_phase_reqs[ lit ]; }
 219   /** phase requirements for each quantifier for each instantiation literal */
 220   std::map< Node, bool > d_phase_reqs;
 221   std::map< Node, bool > d_phase_reqs_equality;
 222   std::map< Node, Node > d_phase_reqs_equality_term;
 223
 224   static void getPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
 225   static void getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol );
 226 };
 227
 228 /** Types of bounds that can be inferred for quantified formulas */
 229 enum BoundVarType
 230 {
 231   // a variable has a finite bound because it has finite cardinality
 232   BOUND_FINITE,
 233   // a variable has a finite bound because it is in an integer range, e.g.
 234   //   forall x. u <= x <= l => P(x)
 235   BOUND_INT_RANGE,
 236   // a variable has a finite bound because it is a member of a set, e.g.
 237   //   forall x. x in S => P(x)
 238   BOUND_SET_MEMBER,
 239   // a variable has a finite bound because only a fixed set of terms are
 240   // relevant for it in the domain of the quantified formula, e.g.
 241   //   forall x. ( x = t1 OR ... OR x = tn ) => P(x)
 242   BOUND_FIXED_SET,
 243   // a bound has not been inferred for the variable
 244   BOUND_NONE
 245 };
 246 }
 247 }
 248
 249 #endif /* CVC4__THEORY__QUANT_UTIL_H */