From: Christopher L. Conway Date: Fri, 4 Jun 2010 17:15:13 +0000 (+0000) Subject: Missing files in last commit X-Git-Tag: cvc5-1.0.0~9000 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=febba49895125f4f3489e7dff283a000ae9965b3;p=cvc5.git Missing files in last commit --- diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp new file mode 100644 index 000000000..606fc5418 --- /dev/null +++ b/src/parser/smt/smt.cpp @@ -0,0 +1,151 @@ +/********************* */ +/** smt.h + ** Original author: cconway + ** Major contributors: + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Definitions of SMT constants. + **/ + +#include +namespace std { +using namespace __gnu_cxx; +} + +#include "parser/parser.h" +#include "parser/smt/smt.h" + +namespace CVC4 { +namespace parser { + +std::hash_map Smt::newLogicMap() { + std::hash_map logicMap; + 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_RDL"] = QF_RDL; + logicMap["QF_UF"] = QF_UF; + logicMap["QF_UFIDL"] = QF_UFIDL; + return logicMap; +} + +Smt::Logic Smt::toLogic(const std::string& name) { + static std::hash_map logicMap = newLogicMap(); + return logicMap[name]; +} + +Smt::Smt(ExprManager* exprManager, Input* input, bool strictMode) : + Parser(exprManager,input,strictMode), + d_logicSet(false) { + + // Boolean symbols are always defined + addOperator(kind::AND); + addOperator(kind::EQUAL); + addOperator(kind::IFF); + addOperator(kind::IMPLIES); + addOperator(kind::ITE); + addOperator(kind::NOT); + addOperator(kind::OR); + addOperator(kind::XOR); + +} + +void Smt::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); +} + +/** + * Add theory symbols to the parser state. + * + * @param parser the CVC4 Parser object + * @param theory the theory to open (e.g., Core, Ints) + */ +void Smt::addTheory(Theory theory) { + switch(theory) { + case THEORY_EMPTY: + mkSort("U"); + 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; + + default: + Unhandled(theory); + } +} + +bool Smt::logicIsSet() { + return d_logicSet; +} + +/** + * Sets the logic for the current benchmark. Declares any logic and theory symbols. + * + * @param parser the CVC4 Parser object + * @param name the name of the logic (e.g., QF_UF, AUFLIA) + */ +void Smt::setLogic(const std::string& name) { + d_logicSet = true; + d_logic = toLogic(name); + + switch(d_logic) { + case QF_IDL: + case QF_LIA: + case QF_NIA: + addTheory(THEORY_INTS); + break; + + case QF_LRA: + case QF_RDL: + addTheory(THEORY_REALS); + break; + + case QF_UFIDL: + addTheory(THEORY_INTS); + // falling-through on purpose, to add UF part of UFIDL + + case QF_UF: + addTheory(THEORY_EMPTY); + addOperator(kind::APPLY_UF); + break; + + case AUFLIA: + case AUFLIRA: + case AUFNIRA: + case QF_AUFBV: + case QF_AUFLIA: + case QF_AX: + case QF_BV: + Unhandled(name); + } +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h new file mode 100644 index 000000000..fa20382ff --- /dev/null +++ b/src/parser/smt/smt.h @@ -0,0 +1,108 @@ +/********************* */ +/** smt.h + ** Original author: cconway + ** Major contributors: + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Definitions of SMT constants. + **/ + +#include "cvc4parser_private.h" + +#ifndef __CVC4__PARSER__SMT_H +#define __CVC4__PARSER__SMT_H + +#include +namespace std { using namespace __gnu_cxx; } + +#include "util/hash.h" +#include "parser/parser.h" + +namespace CVC4 { + +class SExpr; + +namespace parser { + +class Smt : public Parser { + friend class ParserBuilder; + +public: + enum Logic { + AUFLIA, + AUFLIRA, + AUFNIRA, + QF_AUFBV, + QF_AUFLIA, + QF_AX, + QF_BV, + QF_IDL, + QF_LIA, + QF_LRA, + QF_NIA, + QF_RDL, + QF_UF, + QF_UFIDL + }; + + enum Theory { + THEORY_ARRAYS, + THEORY_ARRAYS_EX, + THEORY_BITVECTORS, + THEORY_BITVECTORS_32, + THEORY_BITVECTORS_ARRAYS_EX, + THEORY_EMPTY, + THEORY_INTS, + THEORY_INT_ARRAYS, + THEORY_INT_ARRAYS_EX, + THEORY_INT_INT_REAL_ARRAY_ARRAYS_EX, + THEORY_REALS, + THEORY_REALS_INTS, + }; + +private: + bool d_logicSet; + Logic d_logic; + +protected: + Smt(ExprManager* exprManager, Input* input, bool strictMode = false); + +public: + /** + * Add theory symbols to the parser state. + * + * @param parser the CVC4 Parser object + * @param theory the theory to open (e.g., Core, Ints) + */ + void + addTheory(Theory theory); + + bool + logicIsSet(); + + /** + * Sets the logic for the current benchmark. Declares any logic and theory symbols. + * + * @param parser the CVC4 Parser object + * @param name the name of the logic (e.g., QF_UF, AUFLIA) + */ + void + setLogic(const std::string& name); + + static Logic toLogic(const std::string& name); + +private: + + void addArithmeticOperators(); + static std::hash_map newLogicMap(); +}; +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PARSER__SMT_INPUT_H */