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)
--- /dev/null
+/********************* */
+/*! \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 <algorithm>
+#include <set>
+#include <vector>
+
+#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<TNode> v1(n1.begin(), n1.end());
+ std::vector<TNode> 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<TNode> elts)
+ {
+ std::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());
+
+ 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
+++ /dev/null
-/********************* */
-/*! \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 <algorithm>
-#include <set>
-#include <vector>
-
-#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<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_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 */
projects / cvc5.git / commitdiff