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 | |
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')
-rw-r--r-- | test/regress/regress0/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/subranges.cvc | 17 | ||||
-rwxr-xr-x | test/regress/run_regression | 3 | ||||
-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 |
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 */ + |