#define DECLARATION_SCOPE_H_
#include "expr.h"
+#include "util/hash.h"
#include <ext/hash_map>
} //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 {
};
}
}
+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;
#define __CVC4__PARSER__PARSER_STATE_H
#include <string>
+#include <set>
#include "input.h"
#include "parser_exception.h"
/** 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);
*
* @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.
*/
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
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);
libparsersmt2_la_SOURCES = \
Smt2.g \
+ smt2.h \
+ smt2.cpp \
smt2_input.h \
smt2_input.cpp \
$(ANTLR_STUFF)
#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"
#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: ???
-}
-
}
/**
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
}
: 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
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);
}
}
| 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);
}
: sortName[name,CHECK_NONE]
{ t = PARSER_STATE->getSort(name); }
- | BOOL_TOK
- { t = EXPR_MANAGER->booleanType(); }
;
/**
// Base SMT-LIB tokens
ASSERT_TOK : 'assert';
-BOOL_TOK : 'Bool';
//CATEGORY_TOK : ':category';
CHECKSAT_TOK : 'check-sat';
//DIFFICULTY_TOK : ':difficulty';
;
/**
- * 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+
;
--- /dev/null
+/********************* */
+/** 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 */
--- /dev/null
+/********************* */
+/** 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 */
decision_engine.cpp \
decision_engine.h \
exception.h \
+ hash.h \
model.h \
options.h \
output.cpp \
--- /dev/null
+/*
+ * 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_ */
projects / cvc5.git / commitdiff