src/theory/incomplete_id.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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.
  11  * ****************************************************************************
  12  *
  13  * Incompleteness enumeration.
  14  */
  15
  16 #include "cvc5_private.h"
  17
  18 #ifndef CVC5__THEORY__INCOMPLETE_ID_H
  19 #define CVC5__THEORY__INCOMPLETE_ID_H
  20
  21 #include <iosfwd>
  22
  23 namespace cvc5 {
  24 namespace theory {
  25
  26 /**
  27  * Reasons for incompleteness in cvc5.
  28  */
  29 enum class IncompleteId
  30 {
  31   // the non-linear arithmetic solver was disabled
  32   ARITH_NL_DISABLED,
  33   // the non-linear arithmetic solver was incomplete
  34   ARITH_NL,
  35   // incomplete due to lack of a complete quantifiers strategy
  36   QUANTIFIERS,
  37   // we failed to verify the correctness of a candidate solution in SyGuS
  38   QUANTIFIERS_SYGUS_NO_VERIFY,
  39   // incomplete due to counterexample-guided instantiation not being complete
  40   QUANTIFIERS_CEGQI,
  41   // incomplete due to finite model finding not being complete
  42   QUANTIFIERS_FMF,
  43   // incomplete due to explicitly recorded instantiations
  44   QUANTIFIERS_RECORDED_INST,
  45   // incomplete due to limited number of allowed instantiation rounds
  46   QUANTIFIERS_MAX_INST_ROUNDS,
  47   // incomplete due to separation logic
  48   SEP,
  49   // relations were used in combination with set cardinality constraints
  50   SETS_RELS_CARD,
  51   // we skipped processing a looping word equation
  52   STRINGS_LOOP_SKIP,
  53   // we could not simplify a regular expression membership
  54   STRINGS_REGEXP_NO_SIMPLIFY,
  55   // incomplete due to sequence of a dynamic finite type (e.g. a type that
  56   // we know is finite, but its exact cardinality is not fixed. For example,
  57   // when finite model finding is enabled, uninterpreted sorts have a
  58   // cardinality that depends on their interpretation in the current model).
  59   SEQ_FINITE_DYNAMIC_CARDINALITY,
  60   // HO extensionality axiom was disabled
  61   UF_HO_EXT_DISABLED,
  62   // UF+cardinality solver was disabled
  63   UF_CARD_DISABLED,
  64   // UF+cardinality solver used in an incomplete mode
  65   UF_CARD_MODE,
  66
  67   //-------------------------------------- unknown
  68   UNKNOWN
  69 };
  70
  71 /**
  72  * Converts an incompleteness id to a string.
  73  *
  74  * @param i The incompleteness identifier
  75  * @return The name of the incompleteness identifier
  76  */
  77 const char* toString(IncompleteId i);
  78
  79 /**
  80  * Writes an incompleteness identifier to a stream.
  81  *
  82  * @param out The stream to write to
  83  * @param i The incompleteness identifier to write to the stream
  84  * @return The stream
  85  */
  86 std::ostream& operator<<(std::ostream& out, IncompleteId i);
  87
  88 }  // namespace theory
  89 }  // namespace cvc5
  90
  91 #endif /* CVC5__THEORY__INCOMPLETE_ID_H */