From 7237456b4e2e5a119feacf98f52ec9e55d7a62a5 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 6 Apr 2012 22:06:52 +0000 Subject: [PATCH] * Fix ITEs and functions in CVC language printer. * Permit "BOOL = BOOL" in CVC language parser (auto-replaced with IFF internally, except in strict mode). * SExpr atoms now can be string-, integer-, or rational-valued. * SmtEngine::setInfo(":status", ...) now properly dumps a SetBenchmarkStatusCommand rather than a SetInfoCommand. * Some dumping fixes (resolves bug 313) --- src/expr/command.h | 2 +- src/parser/cvc/Cvc.g | 29 ++++---- src/parser/smt/Smt.g | 1 + src/parser/smt2/Smt2.g | 4 +- src/printer/cvc/cvc_printer.cpp | 40 +++++++++-- src/printer/smt/smt_printer.cpp | 2 +- src/printer/smt2/smt2_printer.cpp | 31 ++++++++- src/smt/smt_engine.cpp | 10 ++- src/util/sexpr.h | 110 +++++++++++++++++++++++++++--- 9 files changed, 193 insertions(+), 36 deletions(-) diff --git a/src/expr/command.h b/src/expr/command.h index 6bb6fba3d..a6f22fe20 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -57,7 +57,7 @@ enum BenchmarkStatus { SMT_UNSATISFIABLE, /** The status of the benchmark is unknown */ SMT_UNKNOWN -}; +};/* enum BenchmarkStatus */ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) throw() CVC4_PUBLIC; diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 657a2fe2c..411a0aea1 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -351,7 +351,7 @@ unsigned findPivot(const std::vector& operators, return pivot; }/* findPivot() */ -Expr createPrecedenceTree(ExprManager* em, +Expr createPrecedenceTree(Parser* parser, ExprManager* em, const std::vector& expressions, const std::vector& operators, unsigned startIndex, unsigned stopIndex) { @@ -368,17 +368,20 @@ Expr createPrecedenceTree(ExprManager* em, //Debug("prec") << "pivot[" << startIndex << "," << stopIndex - 1 << "] at " << pivot << std::endl; bool negate; Kind k = getOperatorKind(operators[pivot], negate); - Expr lhs = createPrecedenceTree(em, expressions, operators, startIndex, pivot); - Expr rhs = createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex); + Expr lhs = createPrecedenceTree(parser, em, expressions, operators, startIndex, pivot); + Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex); if(k == kind::EQUAL && lhs.getType().isBoolean()) { - WarningOnce() << "Warning: converting BOOL = BOOL to BOOL <=> BOOL" << std::endl; - k = kind::IFF; + if(parser->strictModeEnabled()) { + WarningOnce() << "Warning: in strict parsing mode, will not convert BOOL = BOOL to BOOL <=> BOOL" << std::endl; + } else { + k = kind::IFF; + } } Expr e = em->mkExpr(k, lhs, rhs); return negate ? em->mkExpr(kind::NOT, e) : e; }/* createPrecedenceTree() recursive variant */ -Expr createPrecedenceTree(ExprManager* em, +Expr createPrecedenceTree(Parser* parser, ExprManager* em, const std::vector& expressions, const std::vector& operators) { if(Debug.isOn("prec") && operators.size() > 1) { @@ -391,7 +394,7 @@ Expr createPrecedenceTree(ExprManager* em, Debug("prec") << std::endl; } - Expr e = createPrecedenceTree(em, expressions, operators, 0, expressions.size() - 1); + Expr e = createPrecedenceTree(parser, em, expressions, operators, 0, expressions.size() - 1); if(Debug.isOn("prec") && operators.size() > 1) { Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST); Debug("prec") << "=> " << e << std::endl; @@ -749,9 +752,9 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr] CVC4::Rational r; } : INTEGER_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); } + { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } | DECIMAL_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); } + { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } | HEX_LITERAL { sexpr = SExpr(AntlrInput::tokenText($HEX_LITERAL)); } | BINARY_LITERAL @@ -1197,7 +1200,7 @@ formula[CVC4::Expr& f] expressions.push_back(f); } i=morecomparisons[expressions,operators]? - { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } + { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); } ) ; @@ -1321,7 +1324,7 @@ comparison[CVC4::Expr& f] : term[f] { expressions.push_back(f); } ( comparisonBinop[op] term[f] { operators.push_back(op); expressions.push_back(f); } )* - { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } + { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); } ; comparisonBinop[unsigned& op] @@ -1345,7 +1348,7 @@ term[CVC4::Expr& f] } : storeTerm[f] { expressions.push_back(f); } ( arithmeticBinop[op] storeTerm[f] { operators.push_back(op); expressions.push_back(f); } )* - { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } + { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); } ; arithmeticBinop[unsigned& op] @@ -1500,7 +1503,7 @@ bvBinaryOpTerm[CVC4::Expr& f] } : bvNegTerm[f] { expressions.push_back(f); } ( bvBinop[op] bvNegTerm[f] { operators.push_back(op); expressions.push_back(f); } )* - { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } + { f = createPrecedenceTree(PARSER_STATE, EXPR_MANAGER, expressions, operators); } ; bvBinop[unsigned& op] @init { diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 53a05a9a4..5a80083b3 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -536,6 +536,7 @@ annotation[CVC4::Command*& smt_command] { std::string value = AntlrInput::tokenText($USER_VALUE); Assert(*value.begin() == '{'); Assert(*value.rbegin() == '}'); + // trim whitespace value.erase(value.begin(), value.begin() + 1); value.erase(value.begin(), std::find_if(value.begin(), value.end(), std::not1(std::ptr_fun(std::isspace)))); value.erase(value.end() - 1); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 926ce1718..d478bd843 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -405,9 +405,9 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr] std::string s; } : INTEGER_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); } + { sexpr = SExpr(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } | DECIMAL_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); } + { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); } | str[s] { sexpr = SExpr(s); } | SYMBOL diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 04690f500..a3d15f822 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -173,6 +173,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo toStream(out, n[1], depth, types, true); out << " ELSE "; toStream(out, n[2], depth, types, true); + out << " ENDIF"; return; break; case kind::TUPLE_TYPE: @@ -237,18 +238,18 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo if (n.getNumChildren() > 2) { out << '('; } - for (unsigned i = 0; i < n.getNumChildren(); ++ i) { - if (i > 0) { + for (unsigned i = 1; i < n.getNumChildren(); ++i) { + if (i > 1) { out << ", "; } - toStream(out, n[i], depth, types, false); + toStream(out, n[i - 1], depth, types, false); } if (n.getNumChildren() > 2) { out << ')'; } } out << " -> "; - toStream(out, n[n.getNumChildren()-1], depth, types, false); + toStream(out, n[n.getNumChildren() - 1], depth, types, false); return; break; @@ -630,6 +631,29 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw }/* CvcPrinter::toStream(CommandStatus*) */ +static void toStream(std::ostream& out, const SExpr& sexpr) throw() { + if(sexpr.isInteger()) { + out << sexpr.getIntegerValue(); + } else if(sexpr.isRational()) { + out << sexpr.getRationalValue(); + } else if(sexpr.isString()) { + string s = sexpr.getValue(); + // escape backslash and quote + for(string::iterator i = s.begin(); i != s.end(); ++i) { + if(*i == '"') { + s.replace(i, i + 1, "\\\""); + ++i; + } else if(*i == '\\') { + s.replace(i, i + 1, "\\\\"); + ++i; + } + } + out << "\"" << s << "\""; + } else { + out << sexpr; + } +} + static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "ASSERT " << c->getExpr() << ";"; } @@ -756,7 +780,9 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw } static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { - out << "% (set-info " << c->getFlag() << " " << c->getSExpr() << ")"; + out << "% (set-info " << c->getFlag() << " "; + toStream(out, c->getSExpr()); + out << ")"; } static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { @@ -764,7 +790,9 @@ static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { } static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { - out << "% (set-option " << c->getFlag() << " " << c->getSExpr() << ")"; + out << "% (set-option " << c->getFlag() << " "; + toStream(out, c->getSExpr()); + out << ")"; } static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index 2ac514988..e6490de63 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -45,7 +45,7 @@ void SmtPrinter::toStream(std::ostream& out, const Command* c, void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { s->toStream(out, language::output::LANG_SMTLIB_V2); -} +}/* SmtPrinter::toStream() */ }/* CVC4::printer::smt namespace */ }/* CVC4::printer namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 691e96ed7..218654a19 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -427,6 +427,29 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, }/* Smt2Printer::toStream(Command*) */ +static void toStream(std::ostream& out, const SExpr& sexpr) throw() { + if(sexpr.isInteger()) { + out << sexpr.getIntegerValue(); + } else if(sexpr.isRational()) { + out << sexpr.getRationalValue(); + } else if(sexpr.isString()) { + string s = sexpr.getValue(); + // escape backslash and quote + for(size_t i = 0; i < s.length(); ++i) { + if(s[i] == '"') { + s.replace(i, 1, "\\\""); + ++i; + } else if(s[i] == '\\') { + s.replace(i, 1, "\\\\"); + ++i; + } + } + out << "\"" << s << "\""; + } else { + out << sexpr; + } +} + template static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); @@ -576,7 +599,9 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw } static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { - out << "(set-info " << c->getFlag() << " " << c->getSExpr() << ")"; + out << "(set-info " << c->getFlag() << " "; + toStream(out, c->getSExpr()); + out << ")"; } static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { @@ -584,7 +609,9 @@ static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { } static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { - out << "(set-option " << c->getFlag() << " " << c->getSExpr() << ")"; + out << "(set-option " << c->getFlag() << " "; + toStream(out, c->getSExpr()); + out << ")"; } static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 57a8c2f23..2b6eb3915 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -383,7 +383,15 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value) throw(BadOptionException, ModalException) { Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; if(Dump.isOn("benchmark")) { - Dump("benchmark") << SetInfoCommand(key, value); + if(key == ":status") { + std::string s = value.getValue(); + BenchmarkStatus status = + (s == "sat") ? SMT_SATISFIABLE : + ((s == "unsat") ? SMT_UNSATISFIABLE : SMT_UNKNOWN); + Dump("benchmark") << SetBenchmarkStatusCommand(status); + } else { + Dump("benchmark") << SetInfoCommand(key, value); + } } // Check for CVC4-specific info keys (prefixed with "cvc4-" or "cvc4_") diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 63ce23874..005d9411d 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -34,8 +34,18 @@ namespace CVC4 { */ class CVC4_PUBLIC SExpr { - /** Flag telling us if this is an atom or a list. */ - bool d_isAtom; + enum { + SEXPR_STRING, + SEXPR_INTEGER, + SEXPR_RATIONAL, + SEXPR_NOT_ATOM + } d_atomType; + + /** The value of an atomic integer-valued S-expression. */ + Integer d_integerValue; + + /** The value of an atomic rational-valued S-expression. */ + Rational d_rationalValue; /** The value of an atomic S-expression. */ std::string d_stringValue; @@ -45,46 +55,126 @@ class CVC4_PUBLIC SExpr { public: SExpr() : - d_isAtom(true) { + d_atomType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(const Integer& value) : + d_atomType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(const Rational& value) : + d_atomType(SEXPR_RATIONAL), + d_integerValue(0), + d_rationalValue(value), + d_stringValue(""), + d_children() { } SExpr(const std::string& value) : - d_isAtom(true), - d_stringValue(value) { + d_atomType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children() { } SExpr(const std::vector children) : - d_isAtom(false), + d_atomType(SEXPR_NOT_ATOM), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), d_children(children) { } /** Is this S-expression an atom? */ bool isAtom() const; + /** Is this S-expression an integer? */ + bool isInteger() const; + + /** Is this S-expression a rational? */ + bool isRational() const; + + /** Is this S-expression a string? */ + bool isString() const; + /** * Get the string value of this S-expression. This will cause an * error if this S-expression is not an atom. */ const std::string getValue() const; + /** + * Get the integer value of this S-expression. This will cause an + * error if this S-expression is not an integer. + */ + const Integer& getIntegerValue() const; + + /** + * Get the rational value of this S-expression. This will cause an + * error if this S-expression is not a rational. + */ + const Rational& getRationalValue() const; + /** * Get the children of this S-expression. This will cause an error * if this S-expression is not a list. */ const std::vector getChildren() const; -}; + +};/* class SExpr */ inline bool SExpr::isAtom() const { - return d_isAtom; + return d_atomType != SEXPR_NOT_ATOM; +} + +inline bool SExpr::isInteger() const { + return d_atomType == SEXPR_INTEGER; +} + +inline bool SExpr::isRational() const { + return d_atomType == SEXPR_RATIONAL; +} + +inline bool SExpr::isString() const { + return d_atomType == SEXPR_STRING; } inline const std::string SExpr::getValue() const { - AlwaysAssert( d_isAtom ); + AlwaysAssert( isAtom() ); + switch(d_atomType) { + case SEXPR_INTEGER: + return d_integerValue.toString(); + case SEXPR_RATIONAL: + return d_rationalValue.toString(); + case SEXPR_STRING: + return d_stringValue; + default: + Unhandled(d_atomType); + } return d_stringValue; } +inline const Integer& SExpr::getIntegerValue() const { + AlwaysAssert( isInteger() ); + return d_integerValue; +} + +inline const Rational& SExpr::getRationalValue() const { + AlwaysAssert( isRational() ); + return d_rationalValue; +} + inline const std::vector SExpr::getChildren() const { - AlwaysAssert( !d_isAtom ); + AlwaysAssert( !isAtom() ); return d_children; } -- 2.30.2