summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr.h4
-rw-r--r--src/expr/node.cpp2
-rw-r--r--src/parser/antlr_parser.cpp16
-rw-r--r--src/parser/antlr_parser.h26
-rw-r--r--src/parser/cvc/cvc_parser.g15
-rw-r--r--src/util/command.cpp4
-rw-r--r--test/regress/logops.cvc10
7 files changed, 57 insertions, 20 deletions
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<Expr>& 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<std::string>& 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<std::string>& names,
- const std::vector< std::string>& sorts) {
+void AntlrParser::newPredicates(const std::vector<std::string>& names,
+ const std::vector<std::string>& 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,17 +151,31 @@ 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
* @param children the children 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<std::string>& sorts);
+ void newPredicate(std::string name, const std::vector<std::string>& 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<std::string>& names,
- const std::vector<std::string>& sorts);
+ void newPredicates(const std::vector<std::string>& 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,11 +211,26 @@ 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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback