From e24352317b31bfcc9e3be53909e152cfdcd72a28 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 30 Mar 2010 04:59:16 +0000
Subject: Highlights of this commit are:

* add NodeManagerWhite unit test

* change kind::APPLY to kind::APPLY_UF

* better APPLY handling: operators are no longer considered children

* more efficient pool lookup; the NodeValue doesn't have to be as fully constructed for the lookup to proceed

* extend DSL for kind declarations
  + new "theory" command declares a theory and its header.  theory_def.h no longer required.
  + arity enforced on operators
  + constant mapping, hashing, equality

* CONSTANT metakinds supported (via Node::getConst<T>(), for example, Node::getConst<CVC4::Rational>() gets a Rational out of a Node (assuming it is of CONST_RATIONAL kind)

* added CONST_RATIONAL and CONST_INTEGER kinds

* builtin operators (AND, OR, PLUS, etc..) returned by Node::getOperator() are now CONSTANT metakind and are created by NodeManager

* Pretty-printing of Nodes now has a depth limit settable by a stream manipulator (e.g. "cout << Node::setdepth(5) << m << endl;" prints DAG rooted at m to a depth of 5)

* getters added to Node, TNode, NodeValue, etc., for operators and metakinds

* build-time generators for kind.h, metakind.h, and theoryof_table.h headers now have a simpler design and flag errors better, and the templates (kind_template.h etc.) are easier to understand.

* DISTINCT is now a kind, and the SMT parser now passes through DISTINCT nodes instead of blowing them up into ANDs.  Until theory rewriting is online, though, DISTINCTs are directly blown up into conjunctions in TheoryEngine::rewrite().

* add gmpxx detection and inclusion

* better Asserts throughout, some documentation, cleanup
---
 src/parser/antlr_parser.cpp |  4 ++--
 src/parser/cvc/cvc_parser.g |  2 +-
 src/parser/smt/smt_parser.g | 18 ++++++++----------
 3 files changed, 11 insertions(+), 13 deletions(-)

(limited to 'src/parser')

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index d20e59db3..98fde0556 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -241,7 +241,7 @@ unsigned int AntlrParser::minArity(Kind kind) {
   case OR:
     return 1;
 
-  case APPLY:
+  case APPLY_UF:
   case EQUAL:
   case IFF:
   case IMPLIES:
@@ -278,7 +278,7 @@ unsigned int AntlrParser::maxArity(Kind kind) {
     return 3;
 
   case AND:
-  case APPLY:
+  case APPLY_UF:
   case PLUS:
   case OR:
     return UINT_MAX;
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 55ae0ff73..acf0394d0 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -323,7 +323,7 @@ term returns [CVC4::Expr t]
 
     LPAREN formulaList[args] RPAREN
     // TODO: check arity
-    { t = mkExpr(CVC4::kind::APPLY, args); }
+    { t = mkExpr(CVC4::kind::APPLY_UF, args); }
 
   | /* if-then-else */
     t = iteTerm
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index 4f93caa87..b876e1649 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -126,19 +126,17 @@ annotatedFormula returns [CVC4::Expr formula]
   : /* a built-in operator application */
     LPAREN kind = builtinOp annotatedFormulas[args] RPAREN
     { checkArity(kind, args.size());
-      formula = mkExpr(kind,args); }
+      if((kind == kind::AND || kind == kind::OR) && args.size() == 1) {
+        formula = args[0];
+      } else {
+        formula = mkExpr(kind, args);
+      }
+    }
 
   | /* a "distinct" expr */
     /* TODO: Should there be a DISTINCT kind in the Expr package? */
     LPAREN DISTINCT annotatedFormulas[args] RPAREN
-    { std::vector<Expr> diseqs;
-      for(unsigned i = 0; i < args.size(); ++i) {
-        for(unsigned j = i+1; j < args.size(); ++j) {
-          diseqs.push_back(mkExpr(CVC4::kind::NOT,
-                                  mkExpr(CVC4::kind::EQUAL,args[i],args[j])));
-        }
-      }
-      formula = mkExpr(CVC4::kind::AND, diseqs); }
+    { formula = mkExpr(CVC4::kind::DISTINCT, args); }
 
   | /* An ite expression */
     LPAREN (ITE | IF_THEN_ELSE)
@@ -164,7 +162,7 @@ annotatedFormula returns [CVC4::Expr formula]
     { args.push_back(f); }
     annotatedFormulas[args] RPAREN
     // TODO: check arity
-    { formula = mkExpr(CVC4::kind::APPLY,args); }
+    { formula = mkExpr(CVC4::kind::APPLY_UF, args); }
 
   | /* a variable */
     { std::string name; }
-- 
cgit v1.2.3