c042c39926e7adefcd6beeefe5003a647e71ead4
1 /********************* */
4 ** Original author: Christopher L. Conway
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): Clark Barrett
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Definitions of SMT2 constants.
14 ** Definitions of SMT2 constants.
17 #include "expr/type.h"
18 #include "expr/command.h"
19 #include "parser/parser.h"
20 #include "parser/smt1/smt1.h"
21 #include "parser/smt2/smt2.h"
26 Smt2::Smt2(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
27 Parser(exprManager
,input
,strictMode
,parseOnly
),
29 if( !strictModeEnabled() ) {
30 addTheory(Smt2::THEORY_CORE
);
34 void Smt2::addArithmeticOperators() {
35 addOperator(kind::PLUS
);
36 addOperator(kind::MINUS
);
37 addOperator(kind::UMINUS
);
38 addOperator(kind::MULT
);
39 addOperator(kind::LT
);
40 addOperator(kind::LEQ
);
41 addOperator(kind::GT
);
42 addOperator(kind::GEQ
);
45 void Smt2::addBitvectorOperators() {
46 addOperator(kind::BITVECTOR_CONCAT
);
47 addOperator(kind::BITVECTOR_AND
);
48 addOperator(kind::BITVECTOR_OR
);
49 addOperator(kind::BITVECTOR_XOR
);
50 addOperator(kind::BITVECTOR_NOT
);
51 addOperator(kind::BITVECTOR_NAND
);
52 addOperator(kind::BITVECTOR_NOR
);
53 addOperator(kind::BITVECTOR_XNOR
);
54 addOperator(kind::BITVECTOR_COMP
);
55 addOperator(kind::BITVECTOR_MULT
);
56 addOperator(kind::BITVECTOR_PLUS
);
57 addOperator(kind::BITVECTOR_SUB
);
58 addOperator(kind::BITVECTOR_NEG
);
59 addOperator(kind::BITVECTOR_UDIV
);
60 addOperator(kind::BITVECTOR_UREM
);
61 addOperator(kind::BITVECTOR_SDIV
);
62 addOperator(kind::BITVECTOR_SREM
);
63 addOperator(kind::BITVECTOR_SMOD
);
64 addOperator(kind::BITVECTOR_SHL
);
65 addOperator(kind::BITVECTOR_LSHR
);
66 addOperator(kind::BITVECTOR_ASHR
);
67 addOperator(kind::BITVECTOR_ULT
);
68 addOperator(kind::BITVECTOR_ULE
);
69 addOperator(kind::BITVECTOR_UGT
);
70 addOperator(kind::BITVECTOR_UGE
);
71 addOperator(kind::BITVECTOR_SLT
);
72 addOperator(kind::BITVECTOR_SLE
);
73 addOperator(kind::BITVECTOR_SGT
);
74 addOperator(kind::BITVECTOR_SGE
);
75 addOperator(kind::BITVECTOR_BITOF
);
76 addOperator(kind::BITVECTOR_EXTRACT
);
77 addOperator(kind::BITVECTOR_REPEAT
);
78 addOperator(kind::BITVECTOR_ZERO_EXTEND
);
79 addOperator(kind::BITVECTOR_SIGN_EXTEND
);
80 addOperator(kind::BITVECTOR_ROTATE_LEFT
);
81 addOperator(kind::BITVECTOR_ROTATE_RIGHT
);
84 void Smt2::addTheory(Theory theory
) {
87 defineType("Bool", getExprManager()->booleanType());
88 defineVar("true", getExprManager()->mkConst(true));
89 defineVar("false", getExprManager()->mkConst(false));
90 addOperator(kind::AND
);
91 addOperator(kind::DISTINCT
);
92 addOperator(kind::EQUAL
);
93 addOperator(kind::IFF
);
94 addOperator(kind::IMPLIES
);
95 addOperator(kind::ITE
);
96 addOperator(kind::NOT
);
97 addOperator(kind::OR
);
98 addOperator(kind::XOR
);
102 addOperator(kind::SELECT
);
103 addOperator(kind::STORE
);
106 case THEORY_REALS_INTS
:
107 defineType("Real", getExprManager()->realType());
108 addOperator(kind::DIVISION
);
109 // falling through on purpose, to add Ints part of Reals_Ints
112 defineType("Int", getExprManager()->integerType());
113 addArithmeticOperators();
114 addOperator(kind::INTS_DIVISION
);
115 addOperator(kind::INTS_MODULUS
);
119 defineType("Real", getExprManager()->realType());
120 addArithmeticOperators();
121 addOperator(kind::DIVISION
);
124 case THEORY_BITVECTORS
:
125 addBitvectorOperators();
128 case THEORY_QUANTIFIERS
:
132 std::stringstream ss
;
133 ss
<< "internal error: unsupported theory " << theory
;
134 throw ParserException(ss
.str());
138 bool Smt2::logicIsSet() {
142 void Smt2::setLogic(const std::string
& name
) {
146 // Core theory belongs to every logic
147 addTheory(THEORY_CORE
);
149 if(d_logic
.isTheoryEnabled(theory::THEORY_UF
)) {
150 addOperator(kind::APPLY_UF
);
153 if(d_logic
.isTheoryEnabled(theory::THEORY_ARITH
)) {
154 if(d_logic
.areIntegersUsed()) {
155 addTheory(THEORY_INTS
);
158 if(d_logic
.areRealsUsed()) {
159 addTheory(THEORY_REALS
);
163 if(d_logic
.isTheoryEnabled(theory::THEORY_ARRAY
)) {
164 addTheory(THEORY_ARRAYS
);
167 if(d_logic
.isTheoryEnabled(theory::THEORY_BV
)) {
168 addTheory(THEORY_BITVECTORS
);
171 if(d_logic
.isQuantified()) {
172 addTheory(THEORY_QUANTIFIERS
);
174 }/* Smt2::setLogic() */
176 void Smt2::setInfo(const std::string
& flag
, const SExpr
& sexpr
) {
180 void Smt2::setOption(const std::string
& flag
, const SExpr
& sexpr
) {
184 void Smt2::checkThatLogicIsSet() {
185 if( ! logicIsSet() ) {
186 if( strictModeEnabled() ) {
187 parseError("set-logic must appear before this point.");
189 warning("No set-logic command was given before this point.");
190 warning("CVC4 will assume the non-standard ALL_SUPPORTED logic.");
191 warning("Consider setting a stricter logic for (likely) better performance.");
192 warning("To suppress this warning in the future use (set-logic ALL_SUPPORTED).");
194 setLogic("ALL_SUPPORTED");
196 Command
* c
= new SetBenchmarkLogicCommand("ALL_SUPPORTED");
203 }/* CVC4::parser namespace */
204 }/* CVC4 namespace */