* 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

1 files changed, 224 insertions, 0 deletions

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 */
+