1 
2 /*
3  * File SMTLIBLogic.hpp.
4  *
5  * This file is part of the source code of the software program
6  * Vampire. It is protected by applicable
7  * copyright laws.
8  *
9  * This source code is distributed under the licence found here
10  * https://vprover.github.io/license.html
11  * and in the source directory
12  *
13  * In summary, you are allowed to use Vampire for non-commercial
14  * purposes but not allowed to distribute, modify, copy, create derivatives,
15  * or use in competitions.
16  * For other uses of Vampire please contact developers for a different
17  * licence, which we will make an effort to provide.
18  */
19 #ifndef __SMTLIBLogic__
20 #define __SMTLIBLogic__
21 
22 namespace Shell {
23 
24 /**
25   * SMT-LIB logics
26   * QF (quantifier free) should be ground
27   * A - arrays
28   * (L/N)(I/R/both)A - linear/non-linear integer/real/both arithmetic
29   * BV - bit vector - we don't support
30   * (I/R)DL - difference logic - we don't treat specially (fragment of L(I/R)A)
31   * UF - uninterpreted function = first order we know and love
32   * DT - datatypes (term algebras)
33   */
34 enum SMTLIBLogic {
35   SMT_ALIA,
36   SMT_ALL,
37   SMT_AUFDTLIA,
38   SMT_AUFDTLIRA,
39   SMT_AUFDTNIRA,
40   SMT_AUFNIA,
41   SMT_AUFLIA,
42   SMT_AUFLIRA,
43   SMT_AUFNIRA,
44   SMT_BV,
45   SMT_LIA,
46   SMT_LRA,
47   SMT_NIA,
48   SMT_NRA,
49   SMT_QF_ABV,
50   SMT_QF_ALIA,
51   SMT_QF_ANIA,
52   SMT_QF_AUFBV,
53   SMT_QF_AUFLIA,
54   SMT_QF_AUFNIA,
55   SMT_QF_AX,
56   SMT_QF_BV,
57   SMT_QF_IDL,
58   SMT_QF_LIA,
59   SMT_QF_LIRA,
60   SMT_QF_LRA,
61   SMT_QF_NIA,
62   SMT_QF_NIRA,
63   SMT_QF_NRA,
64   SMT_QF_RDL,
65   SMT_QF_UF,
66   SMT_QF_UFBV,
67   SMT_QF_UFIDL,
68   SMT_QF_UFLIA,
69   SMT_QF_UFLRA,
70   SMT_QF_UFNIA,
71   SMT_QF_UFNRA,
72   SMT_UF,
73   SMT_UFBV,
74   SMT_UFDT,
75   SMT_UFDTLIA,
76   SMT_UFDTLIRA,
77   SMT_UFDTNIA,
78   SMT_UFDTNIRA,
79   SMT_UFIDL,
80   SMT_UFLIA,
81   SMT_UFLRA,
82   SMT_UFNIA,
83   SMT_UNDEFINED
84 };
85 
86 }
87 
88 #endif // __SMTLIBLogic__
89