diff options
| -rw-r--r-- | src/expr/declaration_scope.h | 10 | ||||
| -rw-r--r-- | src/parser/parser.cpp | 11 | ||||
| -rw-r--r-- | src/parser/parser.h | 22 | ||||
| -rw-r--r-- | src/parser/smt2/Makefile.am | 2 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 46 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 121 | ||||
| -rw-r--r-- | src/parser/smt2/smt2.h | 85 | ||||
| -rw-r--r-- | src/util/Makefile.am | 1 | ||||
| -rw-r--r-- | src/util/hash.h | 24 |
9 files changed, 276 insertions, 46 deletions
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 7d0f2b787..e33aa25fa 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -15,6 +15,7 @@ #define DECLARATION_SCOPE_H_ #include "expr.h" +#include "util/hash.h" #include <ext/hash_map> @@ -31,15 +32,6 @@ class CDMap; } //namespace context -/** A basic hash function for std::string - * TODO: Does this belong somewhere else (like util/)? - */ -struct StringHashFunction { - size_t operator()(const std::string& str) const { - return __gnu_cxx::hash<const char*>()(str.c_str()); - } -}; - class CVC4_PUBLIC ScopeException : public Exception { }; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index b4bafc953..a1d6398f0 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -210,6 +210,17 @@ void Parser::checkArity(Kind kind, unsigned int numArgs) } } +void Parser::checkOperator(Kind kind, unsigned int numArgs) throw (ParserException) { + if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) { + parseError( "Operator is not defined in the current logic: " + kindToString(kind) ); + } + checkArity(kind,numArgs); +} + +void Parser::addOperator(Kind kind) { + d_logicOperators.insert(kind); +} + Command* Parser::nextCommand() throw(ParserException) { Debug("parser") << "nextCommand()" << std::endl; Command* cmd = NULL; diff --git a/src/parser/parser.h b/src/parser/parser.h index 25d7f2cd1..d87a97ec4 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -19,6 +19,7 @@ #define __CVC4__PARSER__PARSER_STATE_H #include <string> +#include <set> #include "input.h" #include "parser_exception.h" @@ -116,6 +117,9 @@ class CVC4_PUBLIC Parser { /** Are we parsing in strict mode? */ bool d_strictMode; + /** The set of operators available in the current logic. */ + std::set<Kind> d_logicOperators; + /** Lookup a symbol in the given namespace. */ Expr getSymbol(const std::string& var_name, SymbolType type); @@ -185,7 +189,7 @@ public: * * @param name the name of the logic (e.g., QF_UF, AUFLIA) */ - void setLogic(const std::string& name); +// void setLogic(const std::string& name); /** * Returns a variable, given a name and a type. @@ -234,6 +238,16 @@ public: */ void checkArity(Kind kind, unsigned int numArgs) throw (ParserException); + /** Check that <code>kind</code> is a legal operator in the current logic and + * that it can accept <code>numArgs</code> arguments. + * + * @param kind the built-in operator to check + * @param numArgs the number of actual arguments + * @throws ParserException if the parser mode is strict and the operator <code>kind</kind> + * has not been enabled + */ + void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException); + /** * Returns the type for the variable with the given name. * @param var_name the symbol to lookup @@ -266,6 +280,12 @@ public: const std::vector<Type> mkSorts(const std::vector<std::string>& names); + /** Add an operator to the current legal set. + * + * @param kind the built-in operator to add + */ + void addOperator(Kind kind); + /** Is the symbol bound to a boolean variable? */ bool isBoolean(const std::string& name); diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am index 6391919d6..d9082e0b6 100644 --- a/src/parser/smt2/Makefile.am +++ b/src/parser/smt2/Makefile.am @@ -24,6 +24,8 @@ ANTLR_STUFF = \ libparsersmt2_la_SOURCES = \ Smt2.g \ + smt2.h \ + smt2.cpp \ smt2_input.h \ smt2_input.cpp \ $(ANTLR_STUFF) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 268903bc7..94a9aa30b 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -77,6 +77,7 @@ namespace CVC4 { #include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" +#include "parser/smt2/smt2.h" #include "util/integer.h" #include "util/output.h" #include "util/rational.h" @@ -96,29 +97,6 @@ using namespace CVC4::parser; #undef MK_CONST #define MK_CONST EXPR_MANAGER->mkConst -/** - * Sets the logic for the current benchmark. Declares any logic symbols. - * - * @param parser the CVC4 Parser object - * @param name the name of the logic (e.g., QF_UF, AUFLIA) - */ -static void -setLogic(Parser *parser, const std::string& name) { - if( name == "QF_UF" ) { - parser->mkSort("U"); - } else if(name == "QF_LRA"){ - parser->defineType("Real", parser->getExprManager()->realType()); - } else{ - // NOTE: Theory types go here - Unhandled(name); - } -} - -static void -setInfo(Parser *parser, const std::string& flag, const SExpr& sexpr) { - // TODO: ??? -} - } /** @@ -154,11 +132,11 @@ command returns [CVC4::Command* cmd] SET_LOGIC_TOK SYMBOL { name = AntlrInput::tokenText($SYMBOL); Debug("parser") << "set logic: '" << name << "' " << std::endl; - setLogic(PARSER_STATE,name); + Smt2::setLogic(*PARSER_STATE,name); $cmd = new SetBenchmarkLogicCommand(name); } | SET_INFO_TOK KEYWORD symbolicExpr[sexpr] { name = AntlrInput::tokenText($KEYWORD); - setInfo(PARSER_STATE,name,sexpr); + Smt2::setInfo(*PARSER_STATE,name,sexpr); cmd = new SetInfoCommand(name,sexpr); } | /* sort declaration */ DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=INTEGER_LITERAL @@ -195,8 +173,8 @@ symbolicExpr[CVC4::SExpr& sexpr] } : INTEGER_LITERAL { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); } - | RATIONAL_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($RATIONAL_LITERAL)); } + | DECIMAL_LITERAL + { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); } | STRING_LITERAL { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); } | SYMBOL @@ -229,7 +207,7 @@ term[CVC4::Expr& expr] It just so happens expr should already by the only argument. */ Assert( expr == args[0] ); } else { - PARSER_STATE->checkArity(kind, args.size()); + PARSER_STATE->checkOperator(kind, args.size()); expr = MK_EXPR(kind, args); } } @@ -272,9 +250,9 @@ term[CVC4::Expr& expr] | FALSE_TOK { expr = MK_CONST(false); } | INTEGER_LITERAL { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } - | RATIONAL_LITERAL + | DECIMAL_LITERAL { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string - expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_LITERAL) ); } + expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } | HEX_LITERAL { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL,2); @@ -371,8 +349,6 @@ sortSymbol[CVC4::Type& t] } : sortName[name,CHECK_NONE] { t = PARSER_STATE->getSort(name); } - | BOOL_TOK - { t = EXPR_MANAGER->booleanType(); } ; /** @@ -394,7 +370,6 @@ symbol[std::string& id, // Base SMT-LIB tokens ASSERT_TOK : 'assert'; -BOOL_TOK : 'Bool'; //CATEGORY_TOK : ':category'; CHECKSAT_TOK : 'check-sat'; //DIFFICULTY_TOK : ':difficulty'; @@ -500,10 +475,9 @@ fragment NUMERAL ; /** - * Matches a rational constant from the input. This is a bit looser - * than what the standard allows, because it accepts leading zeroes. + * Matches a decimal constant from the input. */ -RATIONAL_LITERAL +DECIMAL_LITERAL : NUMERAL '.' DIGIT+ ; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp new file mode 100644 index 000000000..4d3062d81 --- /dev/null +++ b/src/parser/smt2/smt2.cpp @@ -0,0 +1,121 @@ +/********************* */ +/** smt2.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 SMT2 constants. + **/ + +#include <ext/hash_map> +namespace std { +using namespace __gnu_cxx; +} + +#include "parser/parser.h" +#include "parser/smt2/smt2.h" + +namespace CVC4 { +namespace parser { + +std::hash_map<const std::string, Smt2::Logic, CVC4::StringHashFunction> Smt2::newLogicMap() { + std::hash_map<const std::string, Smt2::Logic, CVC4::StringHashFunction> logicMap; + logicMap["QF_AX"] = QF_AX; + logicMap["QF_BV"] = QF_BV; + logicMap["QF_LIA"] = QF_LIA; + logicMap["QF_LRA"] = QF_LRA; + logicMap["QF_UF"] = QF_UF; + return logicMap; +} + +Smt2::Logic Smt2::toLogic(const std::string& name) { + static std::hash_map<const std::string, Smt2::Logic, CVC4::StringHashFunction> logicMap = newLogicMap(); + return logicMap[name]; +} + +void Smt2::addArithmeticOperators(Parser& parser) { + parser.addOperator(kind::PLUS); + parser.addOperator(kind::MINUS); + parser.addOperator(kind::UMINUS); + parser.addOperator(kind::MULT); + parser.addOperator(kind::LT); + parser.addOperator(kind::LEQ); + parser.addOperator(kind::GT); + parser.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 Smt2::addTheory(Parser& parser, Theory theory) { + switch(theory) { + case THEORY_CORE: + parser.defineType("Bool", parser.getExprManager()->booleanType()); + parser.addOperator(kind::AND); + parser.addOperator(kind::EQUAL); + parser.addOperator(kind::IFF); + parser.addOperator(kind::IMPLIES); + parser.addOperator(kind::ITE); + parser.addOperator(kind::NOT); + parser.addOperator(kind::OR); + parser.addOperator(kind::XOR); + break; + + case THEORY_REALS_INTS: + parser.defineType("Real", parser.getExprManager()->realType()); + // falling-through on purpose, to add Ints part of RealsInts + + case THEORY_INTS: + parser.defineType("Int", parser.getExprManager()->integerType()); + addArithmeticOperators(parser); + break; + + case THEORY_REALS: + parser.defineType("Real", parser.getExprManager()->realType()); + addArithmeticOperators(parser); + break; + + default: + Unhandled(theory); + } +} + +/** + * 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 Smt2::setLogic(Parser& parser, const std::string& name) { + // Core theory belongs to every logic + addTheory(parser, THEORY_CORE); + + switch(toLogic(name)) { + case QF_UF: + parser.addOperator(kind::APPLY_UF); + break; + + case QF_LRA: + addTheory(parser, THEORY_REALS); + break; + + default: + Unhandled(name); + } +} + +void Smt2::setInfo(Parser& parser, const std::string& flag, const SExpr& sexpr) { + // TODO: ??? +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h new file mode 100644 index 000000000..715d3199f --- /dev/null +++ b/src/parser/smt2/smt2.h @@ -0,0 +1,85 @@ +/********************* */ +/** smt2.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 SMT2 constants. + **/ + +#include "cvc4parser_private.h" + +#ifndef __CVC4__PARSER__SMT2_H +#define __CVC4__PARSER__SMT2_H + +#include <ext/hash_map> +namespace std { using namespace __gnu_cxx; } + +#include "util/hash.h" + +namespace CVC4 { + +class SExpr; + +namespace parser { + +class Parser; + +class Smt2 { + +public: + enum Logic { + QF_AX, + QF_BV, + QF_LIA, + QF_LRA, + QF_UF, + }; + + enum Theory { + THEORY_ARRAYS, + THEORY_BITVECTORS, + THEORY_CORE, + THEORY_INTS, + THEORY_REALS, + THEORY_REALS_INTS, + }; + + /** + * Add theory symbols to the parser state. + * + * @param parser the CVC4 Parser object + * @param theory the theory to open (e.g., Core, Ints) + */ + static void + addTheory(Parser& parser, Theory theory); + + /** + * 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) + */ + static void + setLogic(Parser& parser, const std::string& name); + + static void + setInfo(Parser& parser, const std::string& flag, const SExpr& sexpr); + + static Logic toLogic(const std::string& name); + +private: + + static void addArithmeticOperators(Parser& parser); + static std::hash_map<const std::string, Logic, CVC4::StringHashFunction> newLogicMap(); +}; +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__PARSER__SMT2_INPUT_H */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 7025c2952..8c9ddb5bb 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -14,6 +14,7 @@ libutil_la_SOURCES = \ decision_engine.cpp \ decision_engine.h \ exception.h \ + hash.h \ model.h \ options.h \ output.cpp \ diff --git a/src/util/hash.h b/src/util/hash.h new file mode 100644 index 000000000..c72fe47e8 --- /dev/null +++ b/src/util/hash.h @@ -0,0 +1,24 @@ +/* + * hash.h + * + * Created on: May 8, 2010 + * Author: chris + */ + +#ifndef __CVC4__HASH_H_ +#define __CVC4__HASH_H_ + +#include <ext/hash_map> +namespace std { using namespace __gnu_cxx; } + +namespace CVC4 { + +struct StringHashFunction { + size_t operator()(const std::string& str) const { + return std::hash<const char*>()(str.c_str()); + } +}; + +} + +#endif /* __CVC4__HASH_H_ */ |