src/theory/quantifiers/modes.h

   1 /*********************                                                        */
   2 /*! \file modes.h
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #ifndef __CVC4__THEORY__QUANTIFIERS__MODES_H
  21 #define __CVC4__THEORY__QUANTIFIERS__MODES_H
  22
  23 #include <iostream>
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace quantifiers {
  28
  29 typedef enum {
  30   /** Apply instantiation round before full effort (possibly at standard effort) */
  31   INST_WHEN_PRE_FULL,
  32   /** Apply instantiation round at full effort or above  */
  33   INST_WHEN_FULL,
  34   /** Apply instantiation round at full effort, after all other theories finish, or above  */
  35   INST_WHEN_FULL_DELAY,
  36   /** Apply instantiation round at full effort half the time, and last call always */
  37   INST_WHEN_FULL_LAST_CALL,
  38   /** Apply instantiation round at last call only */
  39   INST_WHEN_LAST_CALL,
  40 } InstWhenMode;
  41
  42 typedef enum {
  43   /** Do not consider polarity of patterns */
  44   LITERAL_MATCH_NONE,
  45   /** Consider polarity of boolean predicates only */
  46   LITERAL_MATCH_PREDICATE,
  47   /** Consider polarity of boolean predicates, as well as equalities */
  48   LITERAL_MATCH_EQUALITY,
  49 } LiteralMatchMode;
  50
  51 typedef enum {
  52   /** default, use all methods for axioms */
  53   AXIOM_INST_MODE_DEFAULT,
  54   /** only use heuristic methods for axioms, return unknown in the case no instantiations are produced */
  55   AXIOM_INST_MODE_TRUST,
  56   /** only use heuristic methods for axioms, resort to all methods when no instantiations are produced */
  57   AXIOM_INST_MODE_PRIORITY,
  58 } AxiomInstMode;
  59
  60 typedef enum {
  61   /** mbqi from CADE 24 paper */
  62   MBQI_GEN_EVAL,
  63   /** no mbqi */
  64   MBQI_NONE,
  65   /** implementation that mimics inst-gen */
  66   MBQI_INST_GEN,
  67   /** default, mbqi from Section 5.4.2 of AJR thesis */
  68   MBQI_FMC,
  69   /** mbqi with integer intervals */
  70   MBQI_FMC_INTERVAL,
  71   /** mbqi with interval abstraction of uninterpreted sorts */
  72   MBQI_INTERVAL,
  73   /** abstract mbqi algorithm */
  74   MBQI_ABS,
  75   /** mbqi trust (produce no instantiations) */
  76   MBQI_TRUST,
  77 } MbqiMode;
  78
  79 typedef enum {
  80   /** default, apply at full effort */
  81   QCF_WHEN_MODE_DEFAULT,
  82   /** apply at last call */
  83   QCF_WHEN_MODE_LAST_CALL,
  84   /** apply at standard effort */
  85   QCF_WHEN_MODE_STD,
  86   /** apply based on heuristics */
  87   QCF_WHEN_MODE_STD_H,
  88 } QcfWhenMode;
  89
  90 typedef enum {
  91   /** default, use qcf for conflicts only */
  92   QCF_CONFLICT_ONLY,
  93   /** use qcf for conflicts and propagations */
  94   QCF_PROP_EQ,
  95   /** use qcf for conflicts, propagations and heuristic instantiations */
  96   QCF_PARTIAL,
  97   /** use qcf for model checking */
  98   QCF_MC,
  99 } QcfMode;
 100
 101 typedef enum {
 102   /** default, use but do not trust */
 103   USER_PAT_MODE_DEFAULT,
 104   /** if patterns are supplied for a quantifier, use only those */
 105   USER_PAT_MODE_TRUST,
 106   /** ignore user patterns */
 107   USER_PAT_MODE_IGNORE,
 108 } UserPatMode;
 109
 110 }/* CVC4::theory::quantifiers namespace */
 111 }/* CVC4::theory namespace */
 112
 113 std::ostream& operator<<(std::ostream& out, theory::quantifiers::InstWhenMode mode) CVC4_PUBLIC;
 114
 115 }/* CVC4 namespace */
 116
 117 #endif /* __CVC4__THEORY__QUANTIFIERS__MODES_H */