From: Aina Niemetz Date: Mon, 1 Mar 2021 12:44:11 +0000 (-0800) Subject: google test: util: Migrate boolean_simplification_black. (#6014) X-Git-Tag: cvc5-1.0.0~2188 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=28fd445f012a154e872bbc2feaa69391b37e2301;p=cvc5.git google test: util: Migrate boolean_simplification_black. (#6014) --- diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index ab7bf25f5..4d644acfe 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -15,7 +15,7 @@ cvc4_add_unit_test_white(array_store_all_white util) cvc4_add_unit_test_white(assert_white util) cvc4_add_unit_test_black(binary_heap_black util) cvc4_add_cxx_unit_test_black(bitvector_black util) -cvc4_add_cxx_unit_test_black(boolean_simplification_black util) +cvc4_add_unit_test_black(boolean_simplification_black util) cvc4_add_unit_test_black(cardinality_black util) cvc4_add_unit_test_white(check_white util) cvc4_add_cxx_unit_test_black(configuration_black util) diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp new file mode 100644 index 000000000..23cfe3e0f --- /dev/null +++ b/test/unit/util/boolean_simplification_black.cpp @@ -0,0 +1,251 @@ +/********************* */ +/*! \file boolean_simplification_black.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz, Morgan Deters, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. 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 +#include +#include + +#include "expr/expr_iomanip.h" +#include "expr/kind.h" +#include "expr/node.h" +#include "options/language.h" +#include "options/set_language.h" +#include "smt_util/boolean_simplification.h" +#include "test_node.h" + +namespace CVC4 { +namespace test { + +class TestUtilBlackBooleanSimplification : public TestNode +{ + protected: + void SetUp() override + { + TestNode::SetUp(); + + d_a = d_nodeManager->mkSkolem("a", d_nodeManager->booleanType()); + d_b = d_nodeManager->mkSkolem("b", d_nodeManager->booleanType()); + d_c = d_nodeManager->mkSkolem("c", d_nodeManager->booleanType()); + d_d = d_nodeManager->mkSkolem("d", d_nodeManager->booleanType()); + d_e = d_nodeManager->mkSkolem("e", d_nodeManager->booleanType()); + d_f = d_nodeManager->mkSkolem( + "f", + d_nodeManager->mkFunctionType(d_nodeManager->booleanType(), + d_nodeManager->booleanType())); + d_g = d_nodeManager->mkSkolem( + "g", + d_nodeManager->mkFunctionType(d_nodeManager->booleanType(), + d_nodeManager->booleanType())); + d_h = d_nodeManager->mkSkolem( + "h", + d_nodeManager->mkFunctionType(d_nodeManager->booleanType(), + d_nodeManager->booleanType())); + d_fa = d_nodeManager->mkNode(kind::APPLY_UF, d_f, d_a); + d_fb = d_nodeManager->mkNode(kind::APPLY_UF, d_f, d_b); + d_fc = d_nodeManager->mkNode(kind::APPLY_UF, d_f, d_c); + d_ga = d_nodeManager->mkNode(kind::APPLY_UF, d_g, d_a); + d_ha = d_nodeManager->mkNode(kind::APPLY_UF, d_h, d_a); + d_hc = d_nodeManager->mkNode(kind::APPLY_UF, d_h, d_c); + d_ffb = d_nodeManager->mkNode(kind::APPLY_UF, d_f, d_fb); + d_fhc = d_nodeManager->mkNode(kind::APPLY_UF, d_f, d_hc); + d_hfc = d_nodeManager->mkNode(kind::APPLY_UF, d_h, d_fc); + d_gfb = d_nodeManager->mkNode(kind::APPLY_UF, d_g, d_fb); + + d_ac = d_nodeManager->mkNode(kind::EQUAL, d_a, d_c); + d_ffbd = d_nodeManager->mkNode(kind::EQUAL, d_ffb, d_d); + d_efhc = d_nodeManager->mkNode(kind::EQUAL, d_e, d_fhc); + d_dfa = d_nodeManager->mkNode(kind::EQUAL, d_d, d_fa); + + // this test is designed for >= 10 removal threshold + Assert(BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD >= 10); + + std::cout << expr::ExprSetDepth(-1) + << language::SetLanguage(language::output::LANG_CVC4); + } + + // assert equality up to commuting children + void test_nodes_equal(TNode n1, TNode n2) + { + std::cout << "ASSERTING: " << n1 << std::endl + << " ~= " << n2 << std::endl; + ASSERT_EQ(n1.getKind(), n2.getKind()); + ASSERT_EQ(n1.getNumChildren(), n2.getNumChildren()); + std::vector v1(n1.begin(), n1.end()); + std::vector v2(n2.begin(), n2.end()); + sort(v1.begin(), v1.end()); + sort(v2.begin(), v2.end()); + ASSERT_EQ(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 test_node_equals_set(TNode n, Kind k, std::set elts) + { + std::vector 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()); + + ASSERT_EQ(n.getKind(), k); + ASSERT_EQ(elts.size(), n.getNumChildren()); + ASSERT_TRUE(equal(n.begin(), n.end(), elts.begin())); + } + + Node d_a, d_b, d_c, d_d, d_e, d_f, d_g, d_h; + Node d_fa, d_fb, d_fc, d_ga, d_ha, d_hc, d_ffb, d_fhc, d_hfc, d_gfb; + Node d_ac, d_ffbd, d_efhc, d_dfa; +}; + +TEST_F(TestUtilBlackBooleanSimplification, negate) +{ + Node in, out; + + in = d_nodeManager->mkNode(kind::NOT, d_a); + out = d_a; + test_nodes_equal(out, BooleanSimplification::negate(in)); + test_nodes_equal(in, BooleanSimplification::negate(out)); + + in = d_fa.andNode(d_ac).notNode().notNode().notNode().notNode(); + out = d_fa.andNode(d_ac).notNode(); + test_nodes_equal(out, BooleanSimplification::negate(in)); + +#ifdef CVC4_ASSERTIONS + in = Node(); + ASSERT_THROW(BooleanSimplification::negate(in), AssertArgumentException); +#endif +} + +TEST_F(TestUtilBlackBooleanSimplification, simplifyClause) +{ + Node in, out; + + in = d_a.orNode(d_b); + out = in; + test_nodes_equal(out, BooleanSimplification::simplifyClause(in)); + + in = d_nodeManager->mkNode(kind::OR, d_a, d_d.andNode(d_b)); + out = in; + test_nodes_equal(out, BooleanSimplification::simplifyClause(in)); + + in = d_nodeManager->mkNode(kind::OR, d_a, d_d.orNode(d_b)); + out = d_nodeManager->mkNode(kind::OR, d_a, d_d, d_b); + test_nodes_equal(out, BooleanSimplification::simplifyClause(in)); + + in = d_nodeManager->mkNode(kind::OR, + d_fa, + d_ga.orNode(d_c).notNode(), + d_hfc, + d_ac, + d_d.andNode(d_b)); + out = NodeBuilder<>(kind::OR) << d_fa << d_ga.orNode(d_c).notNode() << d_hfc + << d_ac << d_d.andNode(d_b); + test_nodes_equal(out, BooleanSimplification::simplifyClause(in)); + + in = d_nodeManager->mkNode(kind::OR, + d_fa, + d_ga.andNode(d_c).notNode(), + d_hfc, + d_ac, + d_d.andNode(d_b)); + out = NodeBuilder<>(kind::OR) << d_fa << d_ga.notNode() << d_c.notNode() + << d_hfc << d_ac << d_d.andNode(d_b); + test_nodes_equal(out, BooleanSimplification::simplifyClause(in)); + +#ifdef CVC4_ASSERTIONS + in = d_nodeManager->mkNode(kind::AND, d_a, d_b); + ASSERT_THROW(BooleanSimplification::simplifyClause(in), + AssertArgumentException); +#endif +} + +TEST_F(TestUtilBlackBooleanSimplification, simplifyHornClause) +{ + Node in, out; + + in = d_a.impNode(d_b); + out = d_a.notNode().orNode(d_b); + test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in)); + + in = d_a.notNode().impNode(d_ac.andNode(d_b)); + out = d_nodeManager->mkNode(kind::OR, d_a, d_ac.andNode(d_b)); + test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in)); + + in = + d_a.andNode(d_b).impNode(d_nodeManager->mkNode(kind::AND, + d_fa, + d_ga.orNode(d_c).notNode(), + d_hfc.orNode(d_ac), + d_d.andNode(d_b))); + out = d_nodeManager->mkNode(kind::OR, + d_a.notNode(), + d_b.notNode(), + d_nodeManager->mkNode(kind::AND, + d_fa, + d_ga.orNode(d_c).notNode(), + d_hfc.orNode(d_ac), + d_d.andNode(d_b))); + test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in)); + + in = d_a.andNode(d_b).impNode( + d_nodeManager->mkNode(kind::OR, + d_fa, + d_ga.orNode(d_c).notNode(), + d_hfc.orNode(d_ac), + d_d.andNode(d_b).notNode())); + out = NodeBuilder<>(kind::OR) + << d_a.notNode() << d_b.notNode() << d_fa << d_ga.orNode(d_c).notNode() + << d_hfc << d_ac << d_d.notNode(); + test_nodes_equal(out, BooleanSimplification::simplifyHornClause(in)); + +#ifdef CVC4_ASSERTIONS + in = d_nodeManager->mkNode(kind::OR, d_a, d_b); + ASSERT_THROW(BooleanSimplification::simplifyHornClause(in), + AssertArgumentException); +#endif +} + +TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict) +{ + Node in, out; + + in = d_a.andNode(d_b); + out = in; + test_nodes_equal(out, BooleanSimplification::simplifyConflict(in)); + + in = d_nodeManager->mkNode(kind::AND, d_a, d_d.andNode(d_b)); + out = d_nodeManager->mkNode(kind::AND, d_a, d_d, d_b); + test_nodes_equal(out, BooleanSimplification::simplifyConflict(in)); + + in = d_nodeManager->mkNode(kind::AND, + d_fa, + d_ga.orNode(d_c).notNode(), + d_fa, + d_hfc.orNode(d_ac), + d_d.andNode(d_b)); + out = NodeBuilder<>(kind::AND) << d_fa << d_ga.notNode() << d_c.notNode() + << d_hfc.orNode(d_ac) << d_d << d_b; + test_nodes_equal(out, BooleanSimplification::simplifyConflict(in)); + +#ifdef CVC4_ASSERTIONS + in = d_nodeManager->mkNode(kind::OR, d_a, d_b); + ASSERT_THROW(BooleanSimplification::simplifyConflict(in), + AssertArgumentException); +#endif +} +} // namespace test +} // namespace CVC4 diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h deleted file mode 100644 index bb1c58581..000000000 --- a/test/unit/util/boolean_simplification_black.h +++ /dev/null @@ -1,222 +0,0 @@ -/********************* */ -/*! \file boolean_simplification_black.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS - ** in the top-level source directory and their institutional affiliations. - ** All rights reserved. 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 -#include -#include - -#include "expr/expr_iomanip.h" -#include "expr/kind.h" -#include "expr/node.h" -#include "expr/node_manager.h" -#include "options/language.h" -#include "options/set_language.h" -#include "smt_util/boolean_simplification.h" - -using namespace CVC4; -using namespace std; - -class BooleanSimplificationBlack : public CxxTest::TestSuite { - - 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 v1(n1.begin(), n1.end()); - vector 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 elts) { - vector 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_nm = new NodeManager(NULL); - d_scope = new NodeManagerScope(d_nm); - - a = d_nm->mkSkolem("a", d_nm->booleanType()); - b = d_nm->mkSkolem("b", d_nm->booleanType()); - c = d_nm->mkSkolem("c", d_nm->booleanType()); - d = d_nm->mkSkolem("d", d_nm->booleanType()); - e = d_nm->mkSkolem("e", d_nm->booleanType()); - f = d_nm->mkSkolem("f", d_nm->mkFunctionType(d_nm->booleanType(), - d_nm->booleanType())); - g = d_nm->mkSkolem("g", d_nm->mkFunctionType(d_nm->booleanType(), - d_nm->booleanType())); - h = d_nm->mkSkolem("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::EQUAL, a, c); - ffbd = d_nm->mkNode(kind::EQUAL, ffb, d); - efhc = d_nm->mkNode(kind::EQUAL, e, fhc); - dfa = d_nm->mkNode(kind::EQUAL, d, fa); - - // this test is designed for >= 10 removal threshold - TS_ASSERT_LESS_THAN_EQUALS(10u, - BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD); - - cout << expr::ExprSetDepth(-1) - << language::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; - } - - 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), - AssertArgumentException&); -#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), - AssertArgumentException&); -#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), - AssertArgumentException&); -#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), - AssertArgumentException&); -#endif /* CVC4_ASSERTIONS */ - } - -};/* class BooleanSimplificationBlack */