1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 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.
11 * ****************************************************************************
13 * Incompleteness enumeration.
16 #include "cvc5_private.h"
18 #ifndef CVC5__THEORY__INCOMPLETE_ID_H
19 #define CVC5__THEORY__INCOMPLETE_ID_H
27 * Reasons for incompleteness in cvc5.
29 enum class IncompleteId
31 // the non-linear arithmetic solver was disabled
33 // the non-linear arithmetic solver was incomplete
35 // incomplete due to lack of a complete quantifiers strategy
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
41 // incomplete due to finite model finding not being complete
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
49 // relations were used in combination with set cardinality constraints
51 // we skipped processing a looping word equation
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
62 // UF+cardinality solver was disabled
64 // UF+cardinality solver used in an incomplete mode
67 //-------------------------------------- unknown
72 * Converts an incompleteness id to a string.
74 * @param i The incompleteness identifier
75 * @return The name of the incompleteness identifier
77 const char* toString(IncompleteId i
);
80 * Writes an incompleteness identifier to a stream.
82 * @param out The stream to write to
83 * @param i The incompleteness identifier to write to the stream
86 std::ostream
& operator<<(std::ostream
& out
, IncompleteId i
);
91 #endif /* CVC5__THEORY__INCOMPLETE_ID_H */