diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
commit | 57b8c4c8581d2d3ffcf3d3a1bb228271cb4d074a (patch) | |
tree | 1c1781cc83118e4bbd2ad6939b16734c30a69f1a /test/unit/util | |
parent | 673d0e86b91094a58433c3ca71591fb0a0c60f84 (diff) |
* 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
Diffstat (limited to 'test/unit/util')
-rw-r--r-- | test/unit/util/boolean_simplification_black.h | 224 | ||||
-rw-r--r-- | test/unit/util/subrange_bound_white.h | 77 |
2 files changed, 301 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 */ + 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 */ + |