/********************* */
/*! \file smt2.cpp
** \verbatim
- ** Original author: cconway
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
+ ** Original author: Christopher L. Conway
+ ** Major contributors: Kshitij Bansal, Morgan Deters
+ ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett, Tianyi Liang
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
#include "parser/parser.h"
#include "parser/smt1/smt1.h"
#include "parser/smt2/smt2.h"
+#include "parser/antlr_input.h"
+
+// ANTLR defines these, which is really bad!
+#undef true
+#undef false
namespace CVC4 {
namespace parser {
Smt2::Smt2(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
Parser(exprManager,input,strictMode,parseOnly),
d_logicSet(false) {
+ d_unsatCoreNames.push(std::map<Expr, std::string>());
if( !strictModeEnabled() ) {
addTheory(Smt2::THEORY_CORE);
}
}
void Smt2::addArithmeticOperators() {
- addOperator(kind::PLUS);
- addOperator(kind::MINUS);
- addOperator(kind::UMINUS);
- addOperator(kind::MULT);
- addOperator(kind::DIVISION);
- addOperator(kind::LT);
- addOperator(kind::LEQ);
- addOperator(kind::GT);
- addOperator(kind::GEQ);
+ 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);
}
void Smt2::addBitvectorOperators() {
- addOperator(kind::BITVECTOR_CONCAT);
- addOperator(kind::BITVECTOR_AND);
- addOperator(kind::BITVECTOR_OR);
- addOperator(kind::BITVECTOR_XOR);
- addOperator(kind::BITVECTOR_NOT);
- addOperator(kind::BITVECTOR_NAND);
- addOperator(kind::BITVECTOR_NOR);
- addOperator(kind::BITVECTOR_XNOR);
- addOperator(kind::BITVECTOR_COMP);
- addOperator(kind::BITVECTOR_MULT);
- addOperator(kind::BITVECTOR_PLUS);
- addOperator(kind::BITVECTOR_SUB);
- addOperator(kind::BITVECTOR_NEG);
- addOperator(kind::BITVECTOR_UDIV);
- addOperator(kind::BITVECTOR_UREM);
- addOperator(kind::BITVECTOR_SDIV);
- addOperator(kind::BITVECTOR_SREM);
- addOperator(kind::BITVECTOR_SMOD);
- addOperator(kind::BITVECTOR_SHL);
- addOperator(kind::BITVECTOR_LSHR);
- addOperator(kind::BITVECTOR_ASHR);
- addOperator(kind::BITVECTOR_ULT);
- addOperator(kind::BITVECTOR_ULE);
- addOperator(kind::BITVECTOR_UGT);
- addOperator(kind::BITVECTOR_UGE);
- addOperator(kind::BITVECTOR_SLT);
- addOperator(kind::BITVECTOR_SLE);
- addOperator(kind::BITVECTOR_SGT);
- addOperator(kind::BITVECTOR_SGE);
- addOperator(kind::BITVECTOR_BITOF);
- addOperator(kind::BITVECTOR_EXTRACT);
- addOperator(kind::BITVECTOR_REPEAT);
- addOperator(kind::BITVECTOR_ZERO_EXTEND);
- addOperator(kind::BITVECTOR_SIGN_EXTEND);
- addOperator(kind::BITVECTOR_ROTATE_LEFT);
- addOperator(kind::BITVECTOR_ROTATE_RIGHT);
+ Parser::addOperator(kind::BITVECTOR_CONCAT);
+ Parser::addOperator(kind::BITVECTOR_AND);
+ Parser::addOperator(kind::BITVECTOR_OR);
+ Parser::addOperator(kind::BITVECTOR_XOR);
+ Parser::addOperator(kind::BITVECTOR_NOT);
+ Parser::addOperator(kind::BITVECTOR_NAND);
+ Parser::addOperator(kind::BITVECTOR_NOR);
+ Parser::addOperator(kind::BITVECTOR_XNOR);
+ Parser::addOperator(kind::BITVECTOR_COMP);
+ Parser::addOperator(kind::BITVECTOR_MULT);
+ Parser::addOperator(kind::BITVECTOR_PLUS);
+ Parser::addOperator(kind::BITVECTOR_SUB);
+ Parser::addOperator(kind::BITVECTOR_NEG);
+ Parser::addOperator(kind::BITVECTOR_UDIV);
+ Parser::addOperator(kind::BITVECTOR_UREM);
+ Parser::addOperator(kind::BITVECTOR_SDIV);
+ Parser::addOperator(kind::BITVECTOR_SREM);
+ Parser::addOperator(kind::BITVECTOR_SMOD);
+ Parser::addOperator(kind::BITVECTOR_SHL);
+ Parser::addOperator(kind::BITVECTOR_LSHR);
+ Parser::addOperator(kind::BITVECTOR_ASHR);
+ Parser::addOperator(kind::BITVECTOR_ULT);
+ Parser::addOperator(kind::BITVECTOR_ULE);
+ Parser::addOperator(kind::BITVECTOR_UGT);
+ Parser::addOperator(kind::BITVECTOR_UGE);
+ Parser::addOperator(kind::BITVECTOR_SLT);
+ Parser::addOperator(kind::BITVECTOR_SLE);
+ Parser::addOperator(kind::BITVECTOR_SGT);
+ Parser::addOperator(kind::BITVECTOR_SGE);
+ Parser::addOperator(kind::BITVECTOR_BITOF);
+ Parser::addOperator(kind::BITVECTOR_EXTRACT);
+ Parser::addOperator(kind::BITVECTOR_REPEAT);
+ Parser::addOperator(kind::BITVECTOR_ZERO_EXTEND);
+ Parser::addOperator(kind::BITVECTOR_SIGN_EXTEND);
+ Parser::addOperator(kind::BITVECTOR_ROTATE_LEFT);
+ Parser::addOperator(kind::BITVECTOR_ROTATE_RIGHT);
+
+ Parser::addOperator(kind::INT_TO_BITVECTOR);
+ Parser::addOperator(kind::BITVECTOR_TO_NAT);
+}
+
+void Smt2::addStringOperators() {
+ Parser::addOperator(kind::STRING_CONCAT);
+ Parser::addOperator(kind::STRING_LENGTH);
}
void Smt2::addTheory(Theory theory) {
switch(theory) {
+ case THEORY_ARRAYS:
+ Parser::addOperator(kind::SELECT);
+ Parser::addOperator(kind::STORE);
+ break;
+
+ case THEORY_BITVECTORS:
+ addBitvectorOperators();
+ break;
+
case THEORY_CORE:
defineType("Bool", getExprManager()->booleanType());
defineVar("true", getExprManager()->mkConst(true));
defineVar("false", getExprManager()->mkConst(false));
- addOperator(kind::AND);
- addOperator(kind::DISTINCT);
- addOperator(kind::EQUAL);
- addOperator(kind::IFF);
- addOperator(kind::IMPLIES);
- addOperator(kind::ITE);
- addOperator(kind::NOT);
- addOperator(kind::OR);
- addOperator(kind::XOR);
- break;
-
- case THEORY_ARRAYS:
- addOperator(kind::SELECT);
- addOperator(kind::STORE);
+ Parser::addOperator(kind::AND);
+ Parser::addOperator(kind::DISTINCT);
+ 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:
defineType("Real", getExprManager()->realType());
- // falling-through on purpose, to add Ints part of RealsInts
-
+ Parser::addOperator(kind::DIVISION);
+ Parser::addOperator(kind::TO_INTEGER);
+ Parser::addOperator(kind::IS_INTEGER);
+ Parser::addOperator(kind::TO_REAL);
+ // falling through on purpose, to add Ints part of Reals_Ints
case THEORY_INTS:
defineType("Int", getExprManager()->integerType());
addArithmeticOperators();
+ Parser::addOperator(kind::INTS_DIVISION);
+ Parser::addOperator(kind::INTS_MODULUS);
+ Parser::addOperator(kind::ABS);
+ Parser::addOperator(kind::DIVISIBLE);
break;
case THEORY_REALS:
defineType("Real", getExprManager()->realType());
addArithmeticOperators();
+ Parser::addOperator(kind::DIVISION);
break;
- case THEORY_BITVECTORS:
- addBitvectorOperators();
+ case THEORY_QUANTIFIERS:
break;
- case THEORY_QUANTIFIERS:
+ case THEORY_SETS:
+ addOperator(kind::UNION, "union");
+ addOperator(kind::INTERSECTION, "intersection");
+ addOperator(kind::SETMINUS, "setminus");
+ addOperator(kind::SUBSET, "subset");
+ addOperator(kind::MEMBER, "member");
+ addOperator(kind::SINGLETON, "singleton");
+ addOperator(kind::INSERT, "insert");
+ break;
+
+ case THEORY_DATATYPES:
+ Parser::addOperator(kind::APPLY_CONSTRUCTOR);
+ Parser::addOperator(kind::APPLY_TESTER);
+ Parser::addOperator(kind::APPLY_SELECTOR);
+ Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
+ break;
+
+ case THEORY_STRINGS:
+ defineType("String", getExprManager()->stringType());
+ addStringOperators();
+ break;
+
+ case THEORY_UF:
+ Parser::addOperator(kind::APPLY_UF);
break;
default:
}
}
+void Smt2::addOperator(Kind kind, const std::string& name) {
+ Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
+ << std::endl;
+ Parser::addOperator(kind);
+ operatorKindMap[name] = kind;
+}
+
+Kind Smt2::getOperatorKind(const std::string& name) const {
+ // precondition: isOperatorEnabled(name)
+ return operatorKindMap.find(name)->second;
+}
+
+bool Smt2::isOperatorEnabled(const std::string& name) const {
+ return operatorKindMap.find(name) != operatorKindMap.end();
+}
+
+bool Smt2::isTheoryEnabled(Theory theory) const {
+ switch(theory) {
+ case THEORY_ARRAYS:
+ return d_logic.isTheoryEnabled(theory::THEORY_ARRAY);
+ case THEORY_BITVECTORS:
+ return d_logic.isTheoryEnabled(theory::THEORY_BV);
+ case THEORY_CORE:
+ return true;
+ case THEORY_DATATYPES:
+ return d_logic.isTheoryEnabled(theory::THEORY_DATATYPES);
+ case THEORY_INTS:
+ return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
+ d_logic.areIntegersUsed() && ( !d_logic.areRealsUsed() );
+ case THEORY_REALS:
+ return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
+ ( !d_logic.areIntegersUsed() ) && d_logic.areRealsUsed();
+ case THEORY_REALS_INTS:
+ return d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
+ d_logic.areIntegersUsed() && d_logic.areRealsUsed();
+ case THEORY_QUANTIFIERS:
+ return d_logic.isQuantified();
+ case THEORY_SETS:
+ return d_logic.isTheoryEnabled(theory::THEORY_SETS);
+ case THEORY_STRINGS:
+ return d_logic.isTheoryEnabled(theory::THEORY_STRINGS);
+ case THEORY_UF:
+ return d_logic.isTheoryEnabled(theory::THEORY_UF);
+ default:
+ std::stringstream ss;
+ ss << "internal error: unsupported theory " << theory;
+ throw ParserException(ss.str());
+ }
+}
+
bool Smt2::logicIsSet() {
return d_logicSet;
}
void Smt2::setLogic(const std::string& name) {
d_logicSet = true;
- d_logic = Smt1::toLogic(name);
+ if(logicIsForced()) {
+ d_logic = getForcedLogic();
+ } else {
+ d_logic = name;
+ }
// Core theory belongs to every logic
addTheory(THEORY_CORE);
- switch(d_logic) {
- case Smt1::QF_SAT:
- /* No extra symbols necessary */
- break;
-
- case Smt1::QF_AX:
- addTheory(THEORY_ARRAYS);
- break;
-
- case Smt1::QF_IDL:
- case Smt1::QF_LIA:
- case Smt1::QF_NIA:
- addTheory(THEORY_INTS);
- break;
-
- case Smt1::QF_RDL:
- case Smt1::QF_LRA:
- case Smt1::QF_NRA:
- addTheory(THEORY_REALS);
- break;
-
- case Smt1::QF_UF:
- addOperator(kind::APPLY_UF);
- break;
-
- case Smt1::QF_UFIDL:
- case Smt1::QF_UFLIA:
- case Smt1::QF_UFNIA:// nonstandard logic
- addTheory(THEORY_INTS);
- addOperator(kind::APPLY_UF);
- break;
-
- case Smt1::QF_UFLRA:
- case Smt1::QF_UFNRA:
- addTheory(THEORY_REALS);
- addOperator(kind::APPLY_UF);
- break;
-
- case Smt1::QF_UFLIRA:// nonstandard logic
- case Smt1::QF_UFNIRA:// nonstandard logic
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_INTS);
- addTheory(THEORY_REALS);
- break;
-
- case Smt1::QF_BV:
- addTheory(THEORY_BITVECTORS);
- break;
-
- case Smt1::QF_ABV:
- addTheory(THEORY_ARRAYS);
- addTheory(THEORY_BITVECTORS);
- break;
-
- case Smt1::QF_UFBV:
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_BITVECTORS);
- break;
+ if(d_logic.isTheoryEnabled(theory::THEORY_UF)) {
+ addTheory(THEORY_UF);
+ }
- case Smt1::QF_AUFBV:
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_ARRAYS);
- addTheory(THEORY_BITVECTORS);
- break;
+ if(d_logic.isTheoryEnabled(theory::THEORY_ARITH)) {
+ if(d_logic.areIntegersUsed()) {
+ if(d_logic.areRealsUsed()) {
+ addTheory(THEORY_REALS_INTS);
+ } else {
+ addTheory(THEORY_INTS);
+ }
+ } else if(d_logic.areRealsUsed()) {
+ addTheory(THEORY_REALS);
+ }
+ }
- case Smt1::QF_AUFBVLIA:
- addOperator(kind::APPLY_UF);
+ if(d_logic.isTheoryEnabled(theory::THEORY_ARRAY)) {
addTheory(THEORY_ARRAYS);
- addTheory(THEORY_BITVECTORS);
- addTheory(THEORY_INTS);
- break;
+ }
- case Smt1::QF_AUFBVLRA:
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_ARRAYS);
+ if(d_logic.isTheoryEnabled(theory::THEORY_BV)) {
addTheory(THEORY_BITVECTORS);
- addTheory(THEORY_REALS);
- break;
+ }
- case Smt1::QF_AUFLIA:
- addTheory(THEORY_ARRAYS);
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_INTS);
- break;
+ if(d_logic.isTheoryEnabled(theory::THEORY_DATATYPES)) {
+ addTheory(THEORY_DATATYPES);
+ }
- case Smt1::QF_AUFLIRA:
- addTheory(THEORY_ARRAYS);
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_INTS);
- addTheory(THEORY_REALS);
- break;
+ if(d_logic.isTheoryEnabled(theory::THEORY_SETS)) {
+ addTheory(THEORY_SETS);
+ }
- case Smt1::ALL_SUPPORTED:
- addTheory(THEORY_QUANTIFIERS);
- /* fall through */
- case Smt1::QF_ALL_SUPPORTED:
- addTheory(THEORY_ARRAYS);
- addOperator(kind::APPLY_UF);
- addTheory(THEORY_INTS);
- addTheory(THEORY_REALS);
- addTheory(THEORY_BITVECTORS);
- break;
+ if(d_logic.isTheoryEnabled(theory::THEORY_STRINGS)) {
+ addTheory(THEORY_STRINGS);
+ }
- case Smt1::AUFLIA:
- case Smt1::AUFLIRA:
- case Smt1::AUFNIRA:
- case Smt1::LRA:
- case Smt1::UFNIA:
- case Smt1::UFNIRA:
- case Smt1::UFLRA:
- if(d_logic != Smt1::AUFLIA && d_logic != Smt1::UFNIA) {
- addTheory(THEORY_REALS);
- }
- if(d_logic != Smt1::LRA) {
- addOperator(kind::APPLY_UF);
- if(d_logic != Smt1::UFLRA) {
- addTheory(THEORY_INTS);
- if(d_logic != Smt1::UFNIA && d_logic != Smt1::UFNIRA) {
- addTheory(THEORY_ARRAYS);
- }
- }
- }
+ if(d_logic.isQuantified()) {
addTheory(THEORY_QUANTIFIERS);
- break;
}
}/* Smt2::setLogic() */
setLogic("ALL_SUPPORTED");
- preemptCommand(new SetBenchmarkLogicCommand("ALL_SUPPORTED"));
+ Command* c = new SetBenchmarkLogicCommand("ALL_SUPPORTED");
+ c->setMuted(true);
+ preemptCommand(c);
}
}
}
+/* The include are managed in the lexer but called in the parser */
+// Inspired by http://www.antlr3.org/api/C/interop.html
+
+static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
+ Debug("parser") << "Including " << filename << std::endl;
+ // Create a new input stream and take advantage of built in stream stacking
+ // in C target runtime.
+ //
+ pANTLR3_INPUT_STREAM in;
+#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
+ in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
+#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
+ in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
+#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
+ if( in == NULL ) {
+ Debug("parser") << "Can't open " << filename << std::endl;
+ return false;
+ }
+ // Same thing as the predefined PUSHSTREAM(in);
+ lexer->pushCharStream(lexer, in);
+ // restart it
+ //lexer->rec->state->tokenStartCharIndex = -10;
+ //lexer->emit(lexer);
+
+ // Note that the input stream is not closed when it EOFs, I don't bother
+ // to do it here, but it is up to you to track streams created like this
+ // and destroy them when the whole parse session is complete. Remember that you
+ // don't want to do this until all tokens have been manipulated all the way through
+ // your tree parsers etc as the token does not store the text it just refers
+ // back to the input stream and trying to get the text for it will abort if you
+ // close the input stream too early.
+
+ //TODO what said before
+ return true;
+}
+
+void Smt2::includeFile(const std::string& filename) {
+ // security for online version
+ if(!canIncludeFile()) {
+ parseError("include-file feature was disabled for this run.");
+ }
+
+ // Get the lexer
+ AntlrInput* ai = static_cast<AntlrInput*>(getInput());
+ pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
+ // get the name of the current stream "Does it work inside an include?"
+ const std::string inputName = ai->getInputStreamName();
+
+ // Find the directory of the current input file
+ std::string path;
+ size_t pos = inputName.rfind('/');
+ if(pos != std::string::npos) {
+ path = std::string(inputName, 0, pos + 1);
+ }
+ path.append(filename);
+ if(!newInputStream(path, lexer)) {
+ parseError("Couldn't open include file `" + path + "'");
+ }
+}
+
}/* CVC4::parser namespace */
}/* CVC4 namespace */
projects / cvc5.git / blobdiff