From: Dejan Jovanović Date: Wed, 3 Feb 2010 19:50:44 +0000 (+0000) Subject: simple ITE parsing X-Git-Tag: cvc5-1.0.0~9302 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e0fc2cbe091097d95dbe6dd2eb9b6416b75be279;p=cvc5.git simple ITE parsing --- diff --git a/src/expr/expr.h b/src/expr/expr.h index 8d0d4f347..0bbdcd09a 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -132,10 +132,10 @@ public: /** * Very basic pretty printer for Expr. * This is equivalent to calling e.getNode().printAst(...) - * @param o output stream to print to. + * @param out output stream to print to. * @param indent number of spaces to indent the formula by. */ - void printAst(std::ostream & o, int indent = 0) const; + void printAst(std::ostream & out, int indent = 0) const; private: diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 0212b4fdd..78c4f9186 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -128,7 +128,7 @@ void Node::printAst(ostream & o, int ind) const{ if(getKind() == VARIABLE){ o << ' ' << getId(); - }else if(getNumChildren() > 1){ + }else if(getNumChildren() >= 1){ for(Node::iterator child = begin(); child != end(); ++child){ (*child).printAst(o, ind+1); } diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index dbaebf5a5..01235bf88 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -63,17 +63,21 @@ Expr AntlrParser::mkExpr(Kind kind, const Expr& child) { return d_exprManager->mkExpr(kind, child); } -Expr AntlrParser::mkExpr(Kind kind, const Expr& child_1, - const Expr& child_2) { +Expr AntlrParser::mkExpr(Kind kind, const Expr& child_1, const Expr& child_2) { return d_exprManager->mkExpr(kind, child_1, child_2); } +Expr AntlrParser::mkExpr(Kind kind, const Expr& child_1, const Expr& child_2, + const Expr& child_3) { + return d_exprManager->mkExpr(kind, child_1, child_2, child_3); +} + Expr AntlrParser::mkExpr(Kind kind, const std::vector& children) { return d_exprManager->mkExpr(kind, children); } -void AntlrParser::newPredicate(std::string name, - const std::vector< std::string>& sorts) { +void AntlrParser::newPredicate(std::string name, + const std::vector& sorts) { if(sorts.size() == 0) { d_varSymbolTable.bindName(name, d_exprManager->mkVar()); } else { @@ -81,8 +85,8 @@ void AntlrParser::newPredicate(std::string name, } } -void AntlrParser::newPredicates(const std::vector& names, - const std::vector< std::string>& sorts) { +void AntlrParser::newPredicates(const std::vector& names, + const std::vector& sorts) { for(unsigned i = 0; i < names.size(); ++i) { newPredicate(names[i], sorts); } diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 3025d44da..ae84318c8 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -99,7 +99,8 @@ protected: /** * Renames the antlr semantic expression to a given message. */ - void rethrow(antlr::SemanticException& e, std::string msg) throw (antlr::SemanticException); + void rethrow(antlr::SemanticException& e, std::string msg) + throw (antlr::SemanticException); /** * Returns a variable, given a name and a type. @@ -150,16 +151,30 @@ protected: * Creates a new unary CVC4 expression using the expression manager. * @param kind the kind of the expression * @param child the child + * @return the new unary expression */ Expr mkExpr(Kind kind, const Expr& child); /** * Creates a new binary CVC4 expression using the expression manager. * @param kind the kind of the expression - * @param children the children of the expression + * @param child1 the first child + * @param child2 the second child + * @return the new binary expression */ Expr mkExpr(Kind kind, const Expr& child_1, const Expr& child_2); + /** + * Creates a new ternary CVC4 expression using the expression manager. + * @param kind the kind of the expression + * @param child_1 the first child + * @param child_2 the second child + * @param child_3 + * @return the new ternary expression + */ + Expr mkExpr(Kind kind, const Expr& child_1, const Expr& child_2, + const Expr& child_3); + /** * Creates a new CVC4 expression using the expression manager. * @param kind the kind of the expression @@ -173,16 +188,15 @@ protected: * @param name the name of the predicate * @param sorts the sorts */ - void newPredicate(std::string name, - const std::vector& sorts); + void newPredicate(std::string name, const std::vector& sorts); /** * Creates new predicates over the given sorts. Each predicate * will have arity sorts.size(). * @param p_names the names of the predicates */ - void newPredicates(const std::vector& names, - const std::vector& sorts); + void newPredicates(const std::vector& names, const std::vector< + std::string>& sorts); /** * Returns the precedence rank of the kind. diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 1cbdbd067..474c38c96 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -211,10 +211,25 @@ boolIffFormula returns [CVC4::Expr iffFormula] */ primaryBoolFormula returns [CVC4::Expr formula] : formula = boolAtom + | formula = iteFormula | NOT formula = primaryBoolFormula { formula = mkExpr(CVC4::NOT, formula); } | LPAREN formula = boolFormula RPAREN ; +/** + * Parses an ITE boolean formula. + */ +iteFormula returns [CVC4::Expr formula] +{ + Expr iteCondition, iteThen, iteElse; +} + : IF iteCondition = boolFormula + THEN iteThen = boolFormula + ELSE iteElse = boolFormula + ENDIF + { formula = mkExpr(CVC4::ITE, iteCondition, iteThen, iteElse); } + ; + /** * Parses the Boolean atoms (variables and predicates). * @return the expression representing the atom. diff --git a/src/util/command.cpp b/src/util/command.cpp index 334180967..06545a0a0 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -110,7 +110,9 @@ void CheckSatCommand::toStream(ostream& out) const { } void QueryCommand::toStream(ostream& out) const { - out << "Query(" << d_expr << ")"; + out << "Query("; + d_expr.printAst(out, 2); + out << ")"; } void CommandSequence::toStream(ostream& out) const { diff --git a/test/regress/logops.cvc b/test/regress/logops.cvc index 663a659f3..35e080992 100644 --- a/test/regress/logops.cvc +++ b/test/regress/logops.cvc @@ -2,11 +2,13 @@ a, b, c: BOOLEAN; -QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); +%% QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); -QUERY (IF c THEN a ELSE b ENDIF) <=> (c AND a) OR (NOT c AND b); +%% QUERY NOT c AND b; -QUERY (a => b) <=> (NOT a OR b); +QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); -QUERY TRUE XOR FALSE; +%% QUERY (a => b) <=> (NOT a OR b); + +%% QUERY TRUE XOR FALSE;