dc1b47bdef1d5364b9c087b0994715a5f1fda18d
1 /********************* */
4 ** Original author: cconway
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): none
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 ** \brief Definitions of SMT2 constants.
16 ** Definitions of SMT2 constants.
19 #include "expr/type.h"
20 #include "parser/parser.h"
21 #include "parser/smt/smt.h"
22 #include "parser/smt2/smt2.h"
27 Smt2::Smt2(ExprManager
* exprManager
, Input
* input
, bool strictMode
, bool parseOnly
) :
28 Parser(exprManager
,input
,strictMode
,parseOnly
),
30 if( !strictModeEnabled() ) {
31 addTheory(Smt2::THEORY_CORE
);
35 void Smt2::addArithmeticOperators() {
36 addOperator(kind::PLUS
);
37 addOperator(kind::MINUS
);
38 addOperator(kind::UMINUS
);
39 addOperator(kind::MULT
);
40 addOperator(kind::DIVISION
);
41 addOperator(kind::LT
);
42 addOperator(kind::LEQ
);
43 addOperator(kind::GT
);
44 addOperator(kind::GEQ
);
47 void Smt2::addTheory(Theory theory
) {
50 defineType("Bool", getExprManager()->booleanType());
51 defineVar("true", getExprManager()->mkConst(true));
52 defineVar("false", getExprManager()->mkConst(false));
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 // FIXME: should define a paramterized type 'Array' with 2 arguments
67 addOperator(kind::SELECT
);
68 addOperator(kind::STORE
);
71 case THEORY_REALS_INTS
:
72 defineType("Real", getExprManager()->realType());
73 // falling-through on purpose, to add Ints part of RealsInts
76 defineType("Int", getExprManager()->integerType());
77 addArithmeticOperators();
81 defineType("Real", getExprManager()->realType());
82 addArithmeticOperators();
85 case THEORY_BITVECTORS
:
93 bool Smt2::logicIsSet() {
97 void Smt2::setLogic(const std::string
& name
) {
99 d_logic
= Smt::toLogic(name
);
101 // Core theory belongs to every logic
102 addTheory(THEORY_CORE
);
106 /* No extra symbols necessary */
110 addTheory(THEORY_ARRAYS
);
116 addTheory(THEORY_INTS
);
122 addTheory(THEORY_REALS
);
126 addOperator(kind::APPLY_UF
);
131 case Smt::QF_UFNIA
:// nonstandard logic
132 addTheory(THEORY_INTS
);
133 addOperator(kind::APPLY_UF
);
138 addTheory(THEORY_REALS
);
139 addOperator(kind::APPLY_UF
);
142 case Smt::QF_UFLIRA
:// nonstandard logic
143 case Smt::QF_UFNIRA
:// nonstandard logic
144 addOperator(kind::APPLY_UF
);
145 addTheory(THEORY_INTS
);
146 addTheory(THEORY_REALS
);
150 addTheory(THEORY_BITVECTORS
);
154 addTheory(THEORY_ARRAYS
);
155 addTheory(THEORY_BITVECTORS
);
159 addOperator(kind::APPLY_UF
);
160 addTheory(THEORY_BITVECTORS
);
164 addOperator(kind::APPLY_UF
);
165 addTheory(THEORY_ARRAYS
);
166 addTheory(THEORY_BITVECTORS
);
170 addTheory(THEORY_ARRAYS
);
171 addOperator(kind::APPLY_UF
);
172 addTheory(THEORY_INTS
);
175 case Smt::QF_AUFLIRA
:
176 addTheory(THEORY_ARRAYS
);
177 addOperator(kind::APPLY_UF
);
178 addTheory(THEORY_INTS
);
179 addTheory(THEORY_REALS
);
192 void Smt2::setInfo(const std::string
& flag
, const SExpr
& sexpr
) {
196 void Smt2::setOption(const std::string
& flag
, const SExpr
& sexpr
) {
200 }/* CVC4::parser namespace */
201 }/* CVC4 namespace */