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_RDL"] = QF_RDL
;
39 logicMap
["QF_SAT"] = QF_SAT
;
40 logicMap
["QF_UF"] = QF_UF
;
41 logicMap
["QF_UFIDL"] = QF_UFIDL
;
42 logicMap
["QF_UFLRA"] = QF_UFLRA
;
43 logicMap
["QF_UFLIA"] = QF_UFLIA
;
44 logicMap
["QF_UFLIRA"] = QF_UFLIRA
;
45 logicMap
["QF_UFNIA"] = QF_UFNIA
;
46 logicMap
["QF_UFNIRA"] = QF_UFNIRA
;
47 logicMap
["QF_AUFLIA"] = QF_AUFLIA
;
48 logicMap
["QF_AUFLIRA"] = QF_AUFLIRA
;
52 Smt::Logic
Smt::toLogic(const std::string
& name
) {
53 static std::hash_map
<const std::string
, Smt::Logic
, CVC4::StringHashFunction
> logicMap
= newLogicMap();
54 return logicMap
[name
];
57 Smt::Smt(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
58 Parser(exprManager
,input
,strictMode
,parseOnly
),
61 // Boolean symbols are always defined
62 addOperator(kind::AND
);
63 addOperator(kind::EQUAL
);
64 addOperator(kind::IFF
);
65 addOperator(kind::IMPLIES
);
66 addOperator(kind::ITE
);
67 addOperator(kind::NOT
);
68 addOperator(kind::OR
);
69 addOperator(kind::XOR
);
73 void Smt::addArithmeticOperators() {
74 addOperator(kind::PLUS
);
75 addOperator(kind::MINUS
);
76 addOperator(kind::UMINUS
);
77 addOperator(kind::MULT
);
78 addOperator(kind::LT
);
79 addOperator(kind::LEQ
);
80 addOperator(kind::GT
);
81 addOperator(kind::GEQ
);
84 void Smt::addTheory(Theory theory
) {
87 case THEORY_ARRAYS_EX
: {
88 Type indexType
= mkSort("Index");
89 Type elementType
= mkSort("Element");
90 DeclarationSequence
* seq
= new DeclarationSequence();
91 seq
->addCommand(new DeclareTypeCommand("Index", 0, indexType
));
92 seq
->addCommand(new DeclareTypeCommand("Element", 0, elementType
));
95 defineType("Array", getExprManager()->mkArrayType(indexType
,elementType
));
97 addOperator(kind::SELECT
);
98 addOperator(kind::STORE
);
103 Type sort
= mkSort("U");
104 preemptCommand(new DeclareTypeCommand("U", 0, sort
));
108 case THEORY_REALS_INTS
:
109 defineType("Real", getExprManager()->realType());
110 // falling-through on purpose, to add Ints part of RealsInts
113 defineType("Int", getExprManager()->integerType());
114 addArithmeticOperators();
118 defineType("Real", getExprManager()->realType());
119 addArithmeticOperators();
122 case THEORY_BITVECTORS
:
130 bool Smt::logicIsSet() {
134 inline void Smt::addUf() {
135 addTheory(Smt::THEORY_EMPTY
);
136 addOperator(kind::APPLY_UF
);
139 void Smt::setLogic(const std::string
& name
) {
141 d_logic
= toLogic(name
);
145 addTheory(THEORY_ARRAYS_EX
);
151 addTheory(THEORY_INTS
);
156 addTheory(THEORY_REALS
);
160 /* no extra symbols needed */
165 case QF_UFNIA
:// nonstandard logic
166 addTheory(THEORY_INTS
);
172 addTheory(THEORY_REALS
);
176 case QF_UFLIRA
:// nonstandard logic
177 case QF_UFNIRA
:// nonstandard logic
178 addTheory(THEORY_INTS
);
179 addTheory(THEORY_REALS
);
188 addTheory(THEORY_BITVECTORS
);
192 addTheory(THEORY_ARRAYS_EX
);
194 addTheory(THEORY_INTS
);
198 addTheory(THEORY_ARRAYS_EX
);
200 addTheory(THEORY_INTS
);
201 addTheory(THEORY_REALS
);
214 }/* CVC4::parser namespace */
215 }/* CVC4 namespace */