summaryrefslogtreecommitdiff
path: root/src/parser/smt1/smt1.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smt1/smt1.cpp')
-rw-r--r--src/parser/smt1/smt1.cpp336
1 files changed, 0 insertions, 336 deletions
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
deleted file mode 100644
index 979880f8b..000000000
--- a/src/parser/smt1/smt1.cpp
+++ /dev/null
@@ -1,336 +0,0 @@
-/********************* */
-/*! \file smt1.cpp
- ** \verbatim
- ** Top contributors (to current version):
- ** Christopher L. Conway, Morgan Deters, Dejan Jovanovic
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved. See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** Definitions of SMT-LIB (v1) constants.
- **/
-
-#include "parser/smt1/smt1.h"
-
-#include "api/cvc4cpp.h"
-#include "expr/type.h"
-#include "parser/parser.h"
-#include "smt/command.h"
-
-namespace CVC4 {
-namespace parser {
-
-std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() {
- std::unordered_map<std::string, Smt1::Logic> logicMap;
- logicMap["AUFLIA"] = AUFLIA;
- logicMap["AUFLIRA"] = AUFLIRA;
- logicMap["AUFNIRA"] = AUFNIRA;
- logicMap["LRA"] = LRA;
- logicMap["QF_AX"] = QF_AX;
- logicMap["QF_BV"] = QF_BV;
- logicMap["QF_IDL"] = QF_IDL;
- logicMap["QF_LIA"] = QF_LIA;
- logicMap["QF_LRA"] = QF_LRA;
- logicMap["QF_NIA"] = QF_NIA;
- logicMap["QF_NRA"] = QF_NRA;
- logicMap["QF_RDL"] = QF_RDL;
- logicMap["QF_S"] = QF_S;
- logicMap["QF_SAT"] = QF_SAT;
- logicMap["QF_UF"] = QF_UF;
- logicMap["QF_UFIDL"] = QF_UFIDL;
- logicMap["QF_UFBV"] = QF_UFBV;
- logicMap["QF_UFLRA"] = QF_UFLRA;
- logicMap["QF_UFLIA"] = QF_UFLIA;
- logicMap["QF_UFLIRA"] = QF_UFLIRA;
- logicMap["QF_UFNIA"] = QF_UFNIA;
- logicMap["QF_UFNIRA"] = QF_UFNIRA;
- logicMap["QF_UFNRA"] = QF_UFNRA;
- logicMap["QF_ABV"] = QF_ABV;
- logicMap["QF_AUFBV"] = QF_AUFBV;
- logicMap["QF_AUFBVLIA"] = QF_AUFBVLIA;
- logicMap["QF_AUFBVLRA"] = QF_AUFBVLRA;
- logicMap["QF_UFNIRA"] = QF_UFNIRA;
- logicMap["QF_AUFLIA"] = QF_AUFLIA;
- logicMap["QF_AUFLIRA"] = QF_AUFLIRA;
- logicMap["SAT"] = SAT;
- logicMap["UFNIA"] = UFNIA;
- logicMap["UFNIRA"] = UFNIRA;
- logicMap["UFLRA"] = UFLRA;
- logicMap["QF_ALL_SUPPORTED"] = QF_ALL_SUPPORTED;
- logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
- logicMap["QF_ALL"] = QF_ALL_SUPPORTED;
- logicMap["ALL"] = ALL_SUPPORTED;
- logicMap["HORN"] = ALL_SUPPORTED;
- return logicMap;
-}
-
-Smt1::Logic Smt1::toLogic(const std::string& name) {
- static std::unordered_map<std::string, Smt1::Logic> logicMap = newLogicMap();
- return logicMap[name];
-}
-
-Smt1::Smt1(api::Solver* solver, Input* input, bool strictMode, bool parseOnly)
- : Parser(solver, input, strictMode, parseOnly), d_logic(UNSET)
-{
- // Boolean symbols are always defined
- addOperator(kind::AND);
- addOperator(kind::EQUAL);
- addOperator(kind::IMPLIES);
- addOperator(kind::ITE);
- addOperator(kind::NOT);
- addOperator(kind::OR);
- addOperator(kind::XOR);
-}
-
-void Smt1::addArithmeticOperators() {
- addOperator(kind::PLUS);
- addOperator(kind::MINUS);
- addOperator(kind::UMINUS);
- addOperator(kind::MULT);
- addOperator(kind::LT);
- addOperator(kind::LEQ);
- addOperator(kind::GT);
- addOperator(kind::GEQ);
-}
-
-void Smt1::addTheory(Theory theory) {
- switch(theory) {
- case THEORY_ARRAYS:
- case THEORY_ARRAYS_EX: {
- Type indexType = mkSort("Index");
- Type elementType = mkSort("Element");
- DeclarationSequence* seq = new DeclarationSequence();
- seq->addCommand(new DeclareTypeCommand("Index", 0, indexType));
- seq->addCommand(new DeclareTypeCommand("Element", 0, elementType));
- preemptCommand(seq);
-
- defineType("Array", getExprManager()->mkArrayType(indexType, elementType));
-
- addOperator(kind::SELECT);
- addOperator(kind::STORE);
- break;
- }
-
- case THEORY_BITVECTOR_ARRAYS_EX: {
- // We don't define the "Array" symbol in this case;
- // the parser creates the Array[m:n] types on the fly.
- addOperator(kind::SELECT);
- addOperator(kind::STORE);
- break;
- }
-
- case THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX: {
- defineType("Array1", getExprManager()->mkArrayType(getSort("Int"), getSort("Real")));
- defineType("Array2", getExprManager()->mkArrayType(getSort("Int"), getSort("Array1")));
- addOperator(kind::SELECT);
- addOperator(kind::STORE);
- break;
- }
-
- case THEORY_INT_ARRAYS:
- case THEORY_INT_ARRAYS_EX: {
- defineType("Array", getExprManager()->mkArrayType(getExprManager()->integerType(), getExprManager()->integerType()));
- addOperator(kind::SELECT);
- addOperator(kind::STORE);
- break;
- }
-
- case THEORY_EMPTY: {
- Type sort = mkSort("U");
- preemptCommand(new DeclareTypeCommand("U", 0, sort));
- break;
- }
-
- case THEORY_REALS_INTS:
- defineType("Real", getExprManager()->realType());
- // falling-through on purpose, to add Ints part of RealsInts
-
- case THEORY_INTS:
- defineType("Int", getExprManager()->integerType());
- addArithmeticOperators();
- break;
-
- case THEORY_REALS:
- defineType("Real", getExprManager()->realType());
- addArithmeticOperators();
- break;
-
- case THEORY_BITVECTORS:
- break;
-
- case THEORY_QUANTIFIERS:
- break;
-
- default:
- std::stringstream ss;
- ss << "internal error: unsupported theory " << theory;
- throw ParserException(ss.str());
- }
-}
-
-bool Smt1::logicIsSet() { return d_logic != UNSET; }
-
-void Smt1::setLogic(const std::string& name) {
- d_logic = toLogic(logicIsForced() ? getForcedLogic() : name);
-
- switch(d_logic) {
- case UNSET:
- throw ParserException("Logic cannot remain UNSET after being set.");
- break;
-
- case QF_S:
- throw ParserException(
- "Strings theory unsupported in SMT-LIBv1 front-end; try SMT-LIBv2.");
- break;
-
- case QF_AX:
- addTheory(THEORY_ARRAYS_EX);
- break;
-
- case QF_IDL:
- case QF_LIA:
- case QF_NIA:
- addTheory(THEORY_INTS);
- break;
-
- case QF_RDL:
- case QF_LRA:
- case QF_NRA:
- addTheory(THEORY_REALS);
- break;
-
- case QF_SAT:
- /* no extra symbols needed */
- break;
- case SAT:
- addTheory(THEORY_QUANTIFIERS);
- break;
-
- case QF_UFIDL:
- case QF_UFLIA:
- case QF_UFNIA: // nonstandard logic
- addTheory(THEORY_INTS);
- addOperator(kind::APPLY_UF);
- break;
-
- case QF_UFLRA:
- case QF_UFNRA:
- addTheory(THEORY_REALS);
- addOperator(kind::APPLY_UF);
- break;
-
- case QF_UFLIRA: // nonstandard logic
- case QF_UFNIRA: // nonstandard logic
- addTheory(THEORY_INTS);
- addTheory(THEORY_REALS);
- addOperator(kind::APPLY_UF);
- break;
-
- case QF_UF:
- addTheory(THEORY_EMPTY);
- addOperator(kind::APPLY_UF);
- break;
-
- case QF_BV:
- addTheory(THEORY_BITVECTORS);
- break;
-
- case QF_ABV: // nonstandard logic
- addTheory(THEORY_BITVECTOR_ARRAYS_EX);
- addTheory(THEORY_BITVECTORS);
- break;
-
- case QF_UFBV:
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_BITVECTORS);
- break;
-
- case QF_AUFBV:
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_BITVECTOR_ARRAYS_EX);
- addTheory(THEORY_BITVECTORS);
- break;
-
- case QF_AUFBVLIA: // nonstandard logic
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_ARRAYS_EX);
- addTheory(THEORY_BITVECTORS);
- addTheory(THEORY_INTS);
- break;
-
- case QF_AUFBVLRA: // nonstandard logic
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_ARRAYS_EX);
- addTheory(THEORY_BITVECTORS);
- addTheory(THEORY_REALS);
- break;
-
- case QF_AUFLIA:
- addTheory(THEORY_INT_ARRAYS_EX); // nonstandard logic
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_INTS);
- break;
-
- case QF_AUFLIRA: // nonstandard logic
- addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_INTS);
- addTheory(THEORY_REALS);
- break;
-
- case ALL_SUPPORTED: // nonstandard logic
- addTheory(THEORY_QUANTIFIERS);
- /* fall through */
- case QF_ALL_SUPPORTED: // nonstandard logic
- addTheory(THEORY_ARRAYS_EX);
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_INTS);
- addTheory(THEORY_REALS);
- addTheory(THEORY_BITVECTORS);
- break;
-
- case AUFLIA:
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_INTS);
- addTheory(THEORY_INT_ARRAYS_EX);
- addTheory(THEORY_QUANTIFIERS);
- break;
-
- case AUFLIRA:
- case AUFNIRA:
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_INTS);
- addTheory(THEORY_REALS);
- addTheory(THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX);
- addTheory(THEORY_QUANTIFIERS);
- break;
-
- case LRA:
- addTheory(THEORY_REALS);
- addTheory(THEORY_QUANTIFIERS);
- break;
-
- case UFNIA:
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_INTS);
- addTheory(THEORY_QUANTIFIERS);
- break;
- case UFNIRA:
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_INTS);
- addTheory(THEORY_REALS);
- addTheory(THEORY_QUANTIFIERS);
- break;
-
- case UFLRA:
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_REALS);
- addTheory(THEORY_QUANTIFIERS);
- break;
- }
-}/* Smt1::setLogic() */
-
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback