ade887b23ec0e0bb7c0c92bf67df59b364927c11
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_UFNIRA"] = QF_UFNIRA
;
53 logicMap
["QF_AUFLIA"] = QF_AUFLIA
;
54 logicMap
["QF_AUFLIRA"] = QF_AUFLIRA
;
58 Smt::Logic
Smt::toLogic(const std::string
& name
) {
59 static std::hash_map
<const std::string
, Smt::Logic
, CVC4::StringHashFunction
> logicMap
= newLogicMap();
60 return logicMap
[name
];
63 Smt::Smt(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
64 Parser(exprManager
,input
,strictMode
,parseOnly
),
67 // Boolean symbols are always defined
68 addOperator(kind::AND
);
69 addOperator(kind::EQUAL
);
70 addOperator(kind::IFF
);
71 addOperator(kind::IMPLIES
);
72 addOperator(kind::ITE
);
73 addOperator(kind::NOT
);
74 addOperator(kind::OR
);
75 addOperator(kind::XOR
);
79 void Smt::addArithmeticOperators() {
80 addOperator(kind::PLUS
);
81 addOperator(kind::MINUS
);
82 addOperator(kind::UMINUS
);
83 addOperator(kind::MULT
);
84 addOperator(kind::LT
);
85 addOperator(kind::LEQ
);
86 addOperator(kind::GT
);
87 addOperator(kind::GEQ
);
90 void Smt::addTheory(Theory theory
) {
93 case THEORY_ARRAYS_EX
: {
94 Type indexType
= mkSort("Index");
95 Type elementType
= mkSort("Element");
96 DeclarationSequence
* seq
= new DeclarationSequence();
97 seq
->addCommand(new DeclareTypeCommand("Index", 0, indexType
));
98 seq
->addCommand(new DeclareTypeCommand("Element", 0, elementType
));
101 defineType("Array", getExprManager()->mkArrayType(indexType
, elementType
));
103 addOperator(kind::SELECT
);
104 addOperator(kind::STORE
);
108 case THEORY_INT_ARRAYS_EX
: {
109 defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
111 addOperator(kind::SELECT
);
112 addOperator(kind::STORE
);
117 Type sort
= mkSort("U");
118 preemptCommand(new DeclareTypeCommand("U", 0, sort
));
122 case THEORY_REALS_INTS
:
123 defineType("Real", getExprManager()->realType());
124 // falling-through on purpose, to add Ints part of RealsInts
127 defineType("Int", getExprManager()->integerType());
128 addArithmeticOperators();
132 defineType("Real", getExprManager()->realType());
133 addArithmeticOperators();
136 case THEORY_BITVECTORS
:
144 bool Smt::logicIsSet() {
148 inline void Smt::addUf() {
149 addTheory(Smt::THEORY_EMPTY
);
150 addOperator(kind::APPLY_UF
);
153 void Smt::setLogic(const std::string
& name
) {
155 d_logic
= toLogic(name
);
159 addTheory(THEORY_ARRAYS_EX
);
165 addTheory(THEORY_INTS
);
171 addTheory(THEORY_REALS
);
175 /* no extra symbols needed */
180 case QF_UFNIA
:// nonstandard logic
181 addTheory(THEORY_INTS
);
187 addTheory(THEORY_REALS
);
191 case QF_UFLIRA
:// nonstandard logic
192 case QF_UFNIRA
:// nonstandard logic
193 addTheory(THEORY_INTS
);
194 addTheory(THEORY_REALS
);
203 addTheory(THEORY_BITVECTORS
);
207 addTheory(THEORY_ARRAYS_EX
);
208 addTheory(THEORY_BITVECTORS
);
213 addTheory(THEORY_BITVECTORS
);
218 addTheory(THEORY_ARRAYS_EX
);
219 addTheory(THEORY_BITVECTORS
);
223 addTheory(THEORY_INT_ARRAYS_EX
);
225 addTheory(THEORY_INTS
);
229 addTheory(THEORY_ARRAYS_EX
);
231 addTheory(THEORY_INTS
);
232 addTheory(THEORY_REALS
);
245 }/* CVC4::parser namespace */
246 }/* CVC4 namespace */