1 /********************* */
3 ** Original author: cconway
5 ** Minor contributors (to current version): none
6 ** This file is part of the CVC4 prototype.
7 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
8 ** Courant Institute of Mathematical Sciences
10 ** See the file COPYING in the top-level source directory for licensing
13 ** Definitions of SMT constants.
16 #include <ext/hash_map>
18 using namespace __gnu_cxx
;
21 #include "parser/parser.h"
22 #include "parser/smt/smt.h"
27 std::hash_map
<const std::string
, Smt::Logic
, CVC4::StringHashFunction
> Smt::newLogicMap() {
28 std::hash_map
<const std::string
, Smt::Logic
, CVC4::StringHashFunction
> logicMap
;
29 logicMap
["QF_AX"] = QF_AX
;
30 logicMap
["QF_BV"] = QF_BV
;
31 logicMap
["QF_IDL"] = QF_IDL
;
32 logicMap
["QF_LIA"] = QF_LIA
;
33 logicMap
["QF_LRA"] = QF_LRA
;
34 logicMap
["QF_NIA"] = QF_NIA
;
35 logicMap
["QF_RDL"] = QF_RDL
;
36 logicMap
["QF_SAT"] = QF_SAT
;
37 logicMap
["QF_UF"] = QF_UF
;
38 logicMap
["QF_UFIDL"] = QF_UFIDL
;
42 Smt::Logic
Smt::toLogic(const std::string
& name
) {
43 static std::hash_map
<const std::string
, Smt::Logic
, CVC4::StringHashFunction
> logicMap
= newLogicMap();
44 return logicMap
[name
];
47 Smt::Smt(ExprManager
* exprManager
, Input
* input
, bool strictMode
) :
48 Parser(exprManager
,input
,strictMode
),
51 // Boolean symbols are always defined
52 addOperator(kind::AND
);
53 addOperator(kind::EQUAL
);
54 addOperator(kind::IFF
);
55 addOperator(kind::IMPLIES
);
56 addOperator(kind::ITE
);
57 addOperator(kind::NOT
);
58 addOperator(kind::OR
);
59 addOperator(kind::XOR
);
63 void Smt::addArithmeticOperators() {
64 addOperator(kind::PLUS
);
65 addOperator(kind::MINUS
);
66 addOperator(kind::UMINUS
);
67 addOperator(kind::MULT
);
68 addOperator(kind::LT
);
69 addOperator(kind::LEQ
);
70 addOperator(kind::GT
);
71 addOperator(kind::GEQ
);
75 * Add theory symbols to the parser state.
77 * @param parser the CVC4 Parser object
78 * @param theory the theory to open (e.g., Core, Ints)
80 void Smt::addTheory(Theory theory
) {
86 case THEORY_REALS_INTS
:
87 defineType("Real", getExprManager()->realType());
88 // falling-through on purpose, to add Ints part of RealsInts
91 defineType("Int", getExprManager()->integerType());
92 addArithmeticOperators();
96 defineType("Real", getExprManager()->realType());
97 addArithmeticOperators();
105 bool Smt::logicIsSet() {
110 * Sets the logic for the current benchmark. Declares any logic and theory symbols.
112 * @param parser the CVC4 Parser object
113 * @param name the name of the logic (e.g., QF_UF, AUFLIA)
115 void Smt::setLogic(const std::string
& name
) {
117 d_logic
= toLogic(name
);
123 addTheory(THEORY_INTS
);
128 addTheory(THEORY_REALS
);
132 /* no extra symbols needed */
136 addTheory(THEORY_INTS
);
137 // falling-through on purpose, to add UF part of UFIDL
140 addTheory(THEORY_EMPTY
);
141 addOperator(kind::APPLY_UF
);
155 }/* CVC4::parser namespace */
156 }/* CVC4 namespace */