* reviewed BooleanSimplification, added documentation & unit test

* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work

8 files changed, 348 insertions, 2 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 12e2bb347..323e61ca4 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -38,6 +38,7 @@ SMT2_TESTS = \
 
 # Regression tests for PL inputs
 CVC_TESTS = \
+	subranges.cvc \
 	boolean-prec.cvc \
 	hole6.cvc \
 	ite.cvc \
diff --git a/test/regress/regress0/subranges.cvc b/test/regress/regress0/subranges.cvc
new file mode 100644
index 000000000..d8351c7f1
--- /dev/null
+++ b/test/regress/regress0/subranges.cvc
@@ -0,0 +1,17 @@
+% COMMAND-LINE: --parse-only
+% EXPECT: 
+% EXIT: 0
+
+A : [0..0];
+B : [ -5 .. 8];
+C : [1..3];
+D : [1..2];
+E : [-100 ..-1];
+F : [-100 ..0];
+G : [-100 ..1];
+H : [-1 ..1];
+I : [0..10];
+J : [-10..-9];
+J : [-10..-10];
+
+QUERY TRUE;
diff --git a/test/regress/run_regression b/test/regress/run_regression
index a7a6630b9..8f2e385d7 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -114,12 +114,13 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then
     error "cannot determine status of \`$benchmark'"
   fi
 elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then
-  expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'`
+  expected_output=$(grep '^% EXPECT: ' "$benchmark")
   expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'`
   if [ -z "$expected_output" -a -z "$expected_error" ]; then
     error "cannot determine expected output of \`$benchmark': " \
           "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures"
   fi
+  expected_output=$(echo "$expected_output" | sed 's,^% EXPECT: ,,;s,\r,,')
   expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,;s,\r,,'`
   if [ -z "$expected_exit_status" ]; then
     error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture"
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 646ebf9bb..13d28f3bb 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -44,6 +44,8 @@ UNIT_TESTS = \
 	util/rational_white \
 	util/stats_black \
 	util/trans_closure_black \
+	util/boolean_simplification_black \
+	util/subrange_bound_white \
 	main/interactive_shell_black
 
 export VERBOSE = 1
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index 3b1e96084..e37c197ab 100644
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -46,7 +46,7 @@ private:
       worklist.pop_back();
       if( current.getKind() == kind ) {
         for( unsigned int i = 0; i < current.getNumChildren(); ++i ) {
-          worklist.push_back( current.getChild(i) );
+          worklist.push_back( current[i] );
         }
       } else {
         childrenFound++;
diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index 632db2b91..53050eece 100644
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -27,6 +27,7 @@
 #include "parser/parser_builder.h"
 #include "parser/smt2/smt2.h"
 #include "expr/command.h"
+#include "util/options.h"
 #include "util/output.h"
 #include "util/language.h"
 
@@ -40,6 +41,8 @@ class ParserBlack {
   ExprManager *d_exprManager;
 
 protected:
+  Options d_options;
+
   /* Set up declaration context for expr inputs */
   virtual void setupContext(Parser& parser) {
     /* a, b, c: BOOLEAN */
@@ -69,6 +72,7 @@ protected:
         Parser *parser =
           ParserBuilder(d_exprManager,"test")
             .withStringInput(goodInput)
+            .withOptions(d_options)
             .withInputLanguage(d_lang)
             .build();
         TS_ASSERT( !parser->done() );
@@ -96,6 +100,7 @@ protected:
     Parser *parser =
       ParserBuilder(d_exprManager,"test")
         .withStringInput(badInput)
+        .withOptions(d_options)
         .withInputLanguage(d_lang)
         .withStrictMode(strictMode)
         .build();
@@ -118,6 +123,7 @@ protected:
         Parser *parser =
           ParserBuilder(d_exprManager,"test")
             .withStringInput(goodExpr)
+            .withOptions(d_options)
             .withInputLanguage(d_lang)
             .build();
 
@@ -155,6 +161,7 @@ protected:
       Parser *parser =
         ParserBuilder(d_exprManager,"test")
           .withStringInput(badExpr)
+          .withOptions(d_options)
           .withInputLanguage(d_lang)
           .withStrictMode(strictMode)
           .build();
@@ -177,6 +184,7 @@ protected:
 
   void setUp() {
     d_exprManager = new ExprManager;
+    d_options.parseOnly = true;
   }
 
   void tearDown() {
@@ -217,6 +225,14 @@ public:
     tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment");
     tryGoodInput("a : BOOLEAN; a: BOOLEAN;"); // double decl, but compatible
     tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible
+    tryGoodInput("a : TYPE; a : INT;"); // ok, sort and variable symbol spaces distinct
+    tryGoodInput("a : TYPE; a : INT; b : a;"); // ok except a is both INT and sort `a'
+    tryGoodInput("a : [0..0]; b : [-5..5]; c : [-1..1]; d : [ _ .._];"); // subranges
+    tryGoodInput("a : [ _..1]; b : [_.. 0]; c :[_..-1];");
+    tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;");
+    tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) END;");
+    tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
+    tryGoodInput("DATATYPE trex = Foo | Bar END; DATATYPE tree = node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
   }
 
   void testBadCvc4Inputs() {
@@ -232,6 +248,14 @@ public:
     tryBadInput("A : TYPE; A: TYPE;"); // types can't be double-declared
     tryBadInput("a : INT; a: INT = 5;"); // can't define after decl
     tryBadInput("a : INT = 5; a: BOOLEAN;"); // decl w/ incompatible type
+    tryBadInput("a : TYPE; a : INT; a : a;"); // ok except a is both INT and sort `a'
+    tryBadInput("a : [1..-1];"); // bad subrange
+    tryBadInput("a : [0. .0];"); // bad subrange
+    tryBadInput("a : [..0];"); // bad subrange
+    tryBadInput("a : [0.0];"); // bad subrange
+    tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | cons(car:INT,cdr:list) END;");
+    tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil END;");
+    tryBadInput("DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;");
   }
 
   void testGoodCvc4Exprs() {
diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h
new file mode 100644
index 000000000..8dafd202e
--- /dev/null
+++ b/test/unit/util/boolean_simplification_black.h
@@ -0,0 +1,224 @@
+/*********************                                                        */
+/*! \file boolean_simplification_black.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** 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
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::BooleanSimplification
+ **
+ ** Black box testing of CVC4::BooleanSimplification.
+ **/
+
+#include "context/context.h"
+#include "util/language.h"
+#include "expr/node.h"
+#include "expr/kind.h"
+#include "expr/node_manager.h"
+#include "util/boolean_simplification.h"
+
+#include <algorithm>
+#include <vector>
+#include <set>
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace std;
+
+class BooleanSimplificationBlack : public CxxTest::TestSuite {
+
+  Context* d_context;
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
+
+  Node a, b, c, d, e, f, g, h;
+  Node fa, fb, fc, ga, ha, hc, ffb, fhc, hfc, gfb;
+  Node ac, ffbd, efhc, dfa;
+
+  // assert equality up to commuting children
+  void ASSERT_NODES_EQUAL(TNode n1, TNode n2) {
+    cout << "ASSERTING: " << n1 << endl
+         << "        ~= " << n2 << endl;
+    TS_ASSERT_EQUALS( n1.getKind(), n2.getKind() );
+    TS_ASSERT_EQUALS( n1.getNumChildren(), n2.getNumChildren() );
+    vector<TNode> v1(n1.begin(), n1.end());
+    vector<TNode> v2(n2.begin(), n2.end());
+    sort(v1.begin(), v1.end());
+    sort(v2.begin(), v2.end());
+    TS_ASSERT_EQUALS( v1, v2 );
+  }
+
+  // assert that node's children have same elements as the set
+  // (so no duplicates); also n is asserted to have kind k
+  void ASSERT_NODE_EQUALS_SET(TNode n, Kind k, set<TNode> elts) {
+    vector<TNode> v(n.begin(), n.end());
+
+    // BooleanSimplification implementation sorts its output nodes, BUT
+    // that's an implementation detail, not part of the contract, so we
+    // should be robust to it here; this is a black-box test!
+    sort(v.begin(), v.end());
+
+    TS_ASSERT_EQUALS( n.getKind(), k );
+    TS_ASSERT_EQUALS( elts.size(), n.getNumChildren() );
+    TS_ASSERT( equal(n.begin(), n.end(), elts.begin()) );
+  }
+
+public:
+
+  void setUp() {
+    d_context = new Context();
+    d_nm = new NodeManager(d_context, NULL);
+    d_scope = new NodeManagerScope(d_nm);
+
+    a = d_nm->mkVar("a", d_nm->booleanType());
+    b = d_nm->mkVar("b", d_nm->booleanType());
+    c = d_nm->mkVar("c", d_nm->booleanType());
+    d = d_nm->mkVar("d", d_nm->booleanType());
+    e = d_nm->mkVar("e", d_nm->booleanType());
+    f = d_nm->mkVar("f", d_nm->mkFunctionType(d_nm->booleanType(),
+                                              d_nm->booleanType()));
+    g = d_nm->mkVar("g", d_nm->mkFunctionType(d_nm->booleanType(),
+                                              d_nm->booleanType()));
+    h = d_nm->mkVar("h", d_nm->mkFunctionType(d_nm->booleanType(),
+                                              d_nm->booleanType()));
+    fa = d_nm->mkNode(kind::APPLY_UF, f, a);
+    fb = d_nm->mkNode(kind::APPLY_UF, f, b);
+    fc = d_nm->mkNode(kind::APPLY_UF, f, c);
+    ga = d_nm->mkNode(kind::APPLY_UF, g, a);
+    ha = d_nm->mkNode(kind::APPLY_UF, h, a);
+    hc = d_nm->mkNode(kind::APPLY_UF, h, c);
+    ffb = d_nm->mkNode(kind::APPLY_UF, f, fb);
+    fhc = d_nm->mkNode(kind::APPLY_UF, f, hc);
+    hfc = d_nm->mkNode(kind::APPLY_UF, h, fc);
+    gfb = d_nm->mkNode(kind::APPLY_UF, g, fb);
+
+    ac = d_nm->mkNode(kind::IFF, a, c);
+    ffbd = d_nm->mkNode(kind::IFF, ffb, d);
+    efhc = d_nm->mkNode(kind::IFF, e, fhc);
+    dfa = d_nm->mkNode(kind::IFF, d, fa);
+
+    // this test is designed for >= 10 removal threshold
+    TS_ASSERT_LESS_THAN_EQUALS(10u,
+      BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD);
+
+    cout << Expr::setdepth(-1)
+         << Expr::setlanguage(language::output::LANG_CVC4);
+  }
+
+  void tearDown() {
+    a = b = c = d = e = f = g = h = Node();
+    fa = fb = fc = ga = ha = hc = ffb = fhc = hfc = gfb = Node();
+    ac = ffbd = efhc = dfa = Node();
+
+    delete d_scope;
+    delete d_nm;
+    delete d_context;
+  }
+
+  void testNegate() {
+    Node in, out;
+
+    in = d_nm->mkNode(kind::NOT, a);
+    out = a;
+    ASSERT_NODES_EQUAL( out, BooleanSimplification::negate(in) );
+    ASSERT_NODES_EQUAL( in, BooleanSimplification::negate(out) );
+
+    in = fa.andNode(ac).notNode().notNode().notNode().notNode();
+    out = fa.andNode(ac).notNode();
+    ASSERT_NODES_EQUAL( out, BooleanSimplification::negate(in) );
+
+#ifdef CVC4_ASSERTIONS
+    in = Node();
+    TS_ASSERT_THROWS( BooleanSimplification::negate(in), IllegalArgumentException );
+#endif /* CVC4_ASSERTIONS */
+  }
+
+  void testRemoveDuplicates() {
+  }
+
+  void testPushBackAssociativeCommute() {
+  }
+
+  void testSimplifyClause() {
+    Node in, out;
+
+    in = a.orNode(b);
+    out = in;
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyClause(in));
+
+    in = d_nm->mkNode(kind::OR, a, d.andNode(b));
+    out = in;
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyClause(in));
+
+    in = d_nm->mkNode(kind::OR, a, d.orNode(b));
+    out = d_nm->mkNode(kind::OR, a, d, b);
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyClause(in));
+
+    in = d_nm->mkNode(kind::OR, fa, ga.orNode(c).notNode(), hfc, ac, d.andNode(b));
+    out = NodeBuilder<>(kind::OR) << fa << ga.orNode(c).notNode() << hfc << ac << d.andNode(b);
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyClause(in));
+
+    in = d_nm->mkNode(kind::OR, fa, ga.andNode(c).notNode(), hfc, ac, d.andNode(b));
+    out = NodeBuilder<>(kind::OR) << fa << ga.notNode() << c.notNode() << hfc << ac << d.andNode(b);
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyClause(in));
+
+#ifdef CVC4_ASSERTIONS
+    in = d_nm->mkNode(kind::AND, a, b);
+    TS_ASSERT_THROWS( BooleanSimplification::simplifyClause(in), IllegalArgumentException );
+#endif /* CVC4_ASSERTIONS */
+  }
+
+  void testSimplifyHorn() {
+    Node in, out;
+
+    in = a.impNode(b);
+    out = a.notNode().orNode(b);
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyHornClause(in));
+
+    in = a.notNode().impNode(ac.andNode(b));
+    out = d_nm->mkNode(kind::OR, a, ac.andNode(b));
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyHornClause(in));
+
+    in = a.andNode(b).impNode(d_nm->mkNode(kind::AND, fa, ga.orNode(c).notNode(), hfc.orNode(ac), d.andNode(b)));
+    out = d_nm->mkNode(kind::OR, a.notNode(), b.notNode(), d_nm->mkNode(kind::AND, fa, ga.orNode(c).notNode(), hfc.orNode(ac), d.andNode(b)));
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyHornClause(in));
+
+    in = a.andNode(b).impNode(d_nm->mkNode(kind::OR, fa, ga.orNode(c).notNode(), hfc.orNode(ac), d.andNode(b).notNode()));
+    out = NodeBuilder<>(kind::OR) << a.notNode() << b.notNode() << fa << ga.orNode(c).notNode() << hfc << ac << d.notNode();
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyHornClause(in));
+
+#ifdef CVC4_ASSERTIONS
+    in = d_nm->mkNode(kind::OR, a, b);
+    TS_ASSERT_THROWS( BooleanSimplification::simplifyHornClause(in), IllegalArgumentException );
+#endif /* CVC4_ASSERTIONS */
+  }
+
+  void testSimplifyConflict() {
+    Node in, out;
+
+    in = a.andNode(b);
+    out = in;
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyConflict(in));
+
+    in = d_nm->mkNode(kind::AND, a, d.andNode(b));
+    out = d_nm->mkNode(kind::AND, a, d, b);
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyConflict(in));
+
+    in = d_nm->mkNode(kind::AND, fa, ga.orNode(c).notNode(), fa, hfc.orNode(ac), d.andNode(b));
+    out = NodeBuilder<>(kind::AND) << fa << ga.notNode() << c.notNode() << hfc.orNode(ac) << d << b;
+    ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyConflict(in));
+
+#ifdef CVC4_ASSERTIONS
+    in = d_nm->mkNode(kind::OR, a, b);
+    TS_ASSERT_THROWS( BooleanSimplification::simplifyConflict(in), IllegalArgumentException );
+#endif /* CVC4_ASSERTIONS */
+  }
+
+};/* class BooleanSimplificationBlack */
+
diff --git a/test/unit/util/subrange_bound_white.h b/test/unit/util/subrange_bound_white.h
new file mode 100644
index 000000000..a41f75af9
--- /dev/null
+++ b/test/unit/util/subrange_bound_white.h
@@ -0,0 +1,77 @@
+/*********************                                                        */
+/*! \file subrange_bound_white.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** 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
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief White box testing of CVC4::SubrangeBound
+ **
+ ** White box testing of CVC4::SubrangeBound.
+ **/
+
+#include "util/subrange_bound.h"
+#include "util/integer.h"
+
+#include <string>
+#include <sstream>
+
+using namespace CVC4;
+using namespace std;
+
+class SubrangeBoundWhite : public CxxTest::TestSuite {
+  stringstream ss;
+
+public:
+
+  void testInfinite() {
+    SubrangeBound b;
+    TS_ASSERT( ! b.hasBound() );
+    TS_ASSERT_THROWS( b.getBound(), IllegalArgumentException );
+    ss.str(""); ss << b;
+    TS_ASSERT_EQUALS( ss.str(), "_" );
+  }
+
+  void testZero() {
+    SubrangeBound b1(0), b2(string("0")), b3(Integer("1"));
+    TS_ASSERT( b1.hasBound() && b2.hasBound() && b3.hasBound() );
+    TS_ASSERT( b1.getBound() == 0 && b2.getBound() == 0 && b3.getBound() == 1 );
+    TS_ASSERT( b1 == b2 ); TS_ASSERT( b2 == b1 );
+    TS_ASSERT( !(b1 == b3) ); TS_ASSERT( !(b3 == b1) );
+    TS_ASSERT( !(b2 == b3) ); TS_ASSERT( !(b3 == b2) );
+    TS_ASSERT( !(b1 != b2) ); TS_ASSERT( !(b2 != b1) );
+    TS_ASSERT( b1 != b3 ); TS_ASSERT( b3 != b1 );
+    TS_ASSERT( b2 != b3 ); TS_ASSERT( b3 != b2 );
+    ss.str(""); ss << b1;
+    TS_ASSERT( ss.str() == "0" );
+    ss.str(""); ss << b2;
+    TS_ASSERT( ss.str() == "0" );
+    ss.str(""); ss << b3;
+    TS_ASSERT( ss.str() == "1" );
+  }
+
+  void testOne() {
+    SubrangeBound b(string("1"));
+    TS_ASSERT( b.hasBound() );
+    TS_ASSERT( b.getBound() == 1 );
+    ss.str(""); ss << b;
+    TS_ASSERT( ss.str() == "1" );
+  }
+
+  void testMinusOne() {
+  }
+
+  void testLarge() {
+  }
+
+  void testSmall() {
+  }
+
+};/* class SubrangeBoundWhite */
+