1 /********************* */
4 ** Original author: cconway
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** Definitions of SMT constants.
17 #include <ext/hash_map>
19 using namespace __gnu_cxx
;
22 #include "expr/type.h"
23 #include "expr/command.h"
24 #include "parser/parser.h"
25 #include "parser/smt/smt.h"
30 std::hash_map
<const std::string
, Smt::Logic
, CVC4::StringHashFunction
> Smt::newLogicMap() {
31 std::hash_map
<const std::string
, Smt::Logic
, CVC4::StringHashFunction
> logicMap
;
32 logicMap
["QF_AX"] = QF_AX
;
33 logicMap
["QF_BV"] = QF_BV
;
34 logicMap
["QF_IDL"] = QF_IDL
;
35 logicMap
["QF_LIA"] = QF_LIA
;
36 logicMap
["QF_LRA"] = QF_LRA
;
37 logicMap
["QF_NIA"] = QF_NIA
;
38 logicMap
["QF_NRA"] = QF_NRA
;
39 logicMap
["QF_RDL"] = QF_RDL
;
40 logicMap
["QF_SAT"] = QF_SAT
;
41 logicMap
["QF_UF"] = QF_UF
;
42 logicMap
["QF_UFIDL"] = QF_UFIDL
;
43 logicMap
["QF_UFBV"] = QF_UFBV
;
44 logicMap
["QF_UFLRA"] = QF_UFLRA
;
45 logicMap
["QF_UFLIA"] = QF_UFLIA
;
46 logicMap
["QF_UFLIRA"] = QF_UFLIRA
;
47 logicMap
["QF_UFNIA"] = QF_UFNIA
;
48 logicMap
["QF_UFNIRA"] = QF_UFNIRA
;
49 logicMap
["QF_UFNRA"] = QF_UFNRA
;
50 logicMap
["QF_ABV"] = QF_ABV
;
51 logicMap
["QF_AUFBV"] = QF_AUFBV
;
52 logicMap
["QF_AUFBVLIA"] = QF_AUFBVLIA
;
53 logicMap
["QF_AUFBVLRA"] = QF_AUFBVLRA
;
54 logicMap
["QF_UFNIRA"] = QF_UFNIRA
;
55 logicMap
["QF_AUFLIA"] = QF_AUFLIA
;
56 logicMap
["QF_AUFLIRA"] = QF_AUFLIRA
;
57 logicMap
["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED
;
58 logicMap
["ALL_SUPPORTED"] = ALL_SUPPORTED
;
62 Smt::Logic
Smt::toLogic(const std::string
& name
) {
63 static std::hash_map
<const std::string
, Smt::Logic
, CVC4::StringHashFunction
> logicMap
= newLogicMap();
64 return logicMap
[name
];
67 Smt::Smt(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
68 Parser(exprManager
,input
,strictMode
,parseOnly
),
71 // Boolean symbols are always defined
72 addOperator(kind::AND
);
73 addOperator(kind::EQUAL
);
74 addOperator(kind::IFF
);
75 addOperator(kind::IMPLIES
);
76 addOperator(kind::ITE
);
77 addOperator(kind::NOT
);
78 addOperator(kind::OR
);
79 addOperator(kind::XOR
);
83 void Smt::addArithmeticOperators() {
84 addOperator(kind::PLUS
);
85 addOperator(kind::MINUS
);
86 addOperator(kind::UMINUS
);
87 addOperator(kind::MULT
);
88 addOperator(kind::LT
);
89 addOperator(kind::LEQ
);
90 addOperator(kind::GT
);
91 addOperator(kind::GEQ
);
94 void Smt::addTheory(Theory theory
) {
97 case THEORY_ARRAYS_EX
: {
98 Type indexType
= mkSort("Index");
99 Type elementType
= mkSort("Element");
100 DeclarationSequence
* seq
= new DeclarationSequence();
101 seq
->addCommand(new DeclareTypeCommand("Index", 0, indexType
));
102 seq
->addCommand(new DeclareTypeCommand("Element", 0, elementType
));
105 defineType("Array", getExprManager()->mkArrayType(indexType
, elementType
));
107 addOperator(kind::SELECT
);
108 addOperator(kind::STORE
);
112 case THEORY_INT_ARRAYS_EX
: {
113 defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
115 addOperator(kind::SELECT
);
116 addOperator(kind::STORE
);
121 Type sort
= mkSort("U");
122 preemptCommand(new DeclareTypeCommand("U", 0, sort
));
126 case THEORY_REALS_INTS
:
127 defineType("Real", getExprManager()->realType());
128 // falling-through on purpose, to add Ints part of RealsInts
131 defineType("Int", getExprManager()->integerType());
132 addArithmeticOperators();
136 defineType("Real", getExprManager()->realType());
137 addArithmeticOperators();
140 case THEORY_BITVECTORS
:
148 bool Smt::logicIsSet() {
152 inline void Smt::addUf() {
153 addTheory(Smt::THEORY_EMPTY
);
154 addOperator(kind::APPLY_UF
);
157 void Smt::setLogic(const std::string
& name
) {
159 d_logic
= toLogic(name
);
163 addTheory(THEORY_ARRAYS_EX
);
169 addTheory(THEORY_INTS
);
175 addTheory(THEORY_REALS
);
179 /* no extra symbols needed */
184 case QF_UFNIA
:// nonstandard logic
185 addTheory(THEORY_INTS
);
191 addTheory(THEORY_REALS
);
195 case QF_UFLIRA
:// nonstandard logic
196 case QF_UFNIRA
:// nonstandard logic
197 addTheory(THEORY_INTS
);
198 addTheory(THEORY_REALS
);
207 addTheory(THEORY_BITVECTORS
);
211 addTheory(THEORY_ARRAYS_EX
);
212 addTheory(THEORY_BITVECTORS
);
217 addTheory(THEORY_BITVECTORS
);
222 addTheory(THEORY_ARRAYS_EX
);
223 addTheory(THEORY_BITVECTORS
);
228 addTheory(THEORY_ARRAYS_EX
);
229 addTheory(THEORY_BITVECTORS
);
230 addTheory(THEORY_INTS
);
235 addTheory(THEORY_ARRAYS_EX
);
236 addTheory(THEORY_BITVECTORS
);
237 addTheory(THEORY_REALS
);
241 addTheory(THEORY_INT_ARRAYS_EX
);
243 addTheory(THEORY_INTS
);
247 addTheory(THEORY_ARRAYS_EX
);
249 addTheory(THEORY_INTS
);
250 addTheory(THEORY_REALS
);
255 case QF_ALL_SUPPORTED
:
256 addTheory(THEORY_ARRAYS_EX
);
258 addTheory(THEORY_INTS
);
259 addTheory(THEORY_REALS
);
260 addTheory(THEORY_BITVECTORS
);
273 }/* CVC4::parser namespace */
274 }/* CVC4 namespace */