diff options
Diffstat (limited to 'test/unit')
-rw-r--r-- | test/unit/Makefile.am | 2 | ||||
-rw-r--r-- | test/unit/expr/expr_manager_public.h | 2 | ||||
-rw-r--r-- | test/unit/parser/parser_black.h | 24 | ||||
-rw-r--r-- | test/unit/util/boolean_simplification_black.h | 224 | ||||
-rw-r--r-- | test/unit/util/subrange_bound_white.h | 77 |
5 files changed, 328 insertions, 1 deletions
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 */ + |