1 /********************* */
4 ** Original author: cconway
5 ** Major contributors: none
6 ** Minor contributors (to current version): mdeters, dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 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 "parser/parser.h"
23 #include "parser/smt/smt.h"
28 std::hash_map
<const std::string
, Smt::Logic
, CVC4::StringHashFunction
> Smt::newLogicMap() {
29 std::hash_map
<const std::string
, Smt::Logic
, CVC4::StringHashFunction
> logicMap
;
30 logicMap
["QF_AX"] = QF_AX
;
31 logicMap
["QF_BV"] = QF_BV
;
32 logicMap
["QF_IDL"] = QF_IDL
;
33 logicMap
["QF_LIA"] = QF_LIA
;
34 logicMap
["QF_LRA"] = QF_LRA
;
35 logicMap
["QF_NIA"] = QF_NIA
;
36 logicMap
["QF_RDL"] = QF_RDL
;
37 logicMap
["QF_SAT"] = QF_SAT
;
38 logicMap
["QF_UF"] = QF_UF
;
39 logicMap
["QF_UFIDL"] = QF_UFIDL
;
43 Smt::Logic
Smt::toLogic(const std::string
& name
) {
44 static std::hash_map
<const std::string
, Smt::Logic
, CVC4::StringHashFunction
> logicMap
= newLogicMap();
45 return logicMap
[name
];
48 Smt::Smt(ExprManager
* exprManager
, Input
* input
, bool strictMode
) :
49 Parser(exprManager
,input
,strictMode
),
52 // Boolean symbols are always defined
53 addOperator(kind::AND
);
54 addOperator(kind::EQUAL
);
55 addOperator(kind::IFF
);
56 addOperator(kind::IMPLIES
);
57 addOperator(kind::ITE
);
58 addOperator(kind::NOT
);
59 addOperator(kind::OR
);
60 addOperator(kind::XOR
);
64 void Smt::addArithmeticOperators() {
65 addOperator(kind::PLUS
);
66 addOperator(kind::MINUS
);
67 addOperator(kind::UMINUS
);
68 addOperator(kind::MULT
);
69 addOperator(kind::LT
);
70 addOperator(kind::LEQ
);
71 addOperator(kind::GT
);
72 addOperator(kind::GEQ
);
76 * Add theory symbols to the parser state.
78 * @param parser the CVC4 Parser object
79 * @param theory the theory to open (e.g., Core, Ints)
81 void Smt::addTheory(Theory theory
) {
84 case THEORY_ARRAYS_EX
: {
85 Type indexType
= mkSort("Index");
86 Type elementType
= mkSort("Element");
88 defineType("Array",getExprManager()->mkArrayType(indexType
,elementType
));
90 addOperator(kind::SELECT
);
91 addOperator(kind::STORE
);
99 case THEORY_REALS_INTS
:
100 defineType("Real", getExprManager()->realType());
101 // falling-through on purpose, to add Ints part of RealsInts
104 defineType("Int", getExprManager()->integerType());
105 addArithmeticOperators();
109 defineType("Real", getExprManager()->realType());
110 addArithmeticOperators();
113 case THEORY_BITVECTORS
:
121 bool Smt::logicIsSet() {
125 inline void Smt::addUf() {
126 addTheory(Smt::THEORY_EMPTY
);
127 addOperator(kind::APPLY_UF
);
131 * Sets the logic for the current benchmark. Declares any logic and theory symbols.
133 * @param parser the CVC4 Parser object
134 * @param name the name of the logic (e.g., QF_UF, AUFLIA)
136 void Smt::setLogic(const std::string
& name
) {
138 d_logic
= toLogic(name
);
142 addTheory(THEORY_ARRAYS_EX
);
148 addTheory(THEORY_INTS
);
153 addTheory(THEORY_REALS
);
157 /* no extra symbols needed */
162 addTheory(THEORY_INTS
);
168 addTheory(THEORY_REALS
);
177 addTheory(THEORY_BITVECTORS
);
191 }/* CVC4::parser namespace */
192 }/* CVC4 namespace */