diff options
Diffstat (limited to 'src/parser/smt1/smt1.cpp')
-rw-r--r-- | src/parser/smt1/smt1.cpp | 336 |
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 */ |