1 /********************* */
2 /*! \file shared_term_manager_black.h
4 ** Original author: barrett
5 ** Major contributors: none
6 ** Minor contributors (to current version): mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Black box testing of CVC4::SharedTermManager.
16 ** Black box testing of CVC4::SharedTermManager.
19 #include <cxxtest/TestSuite.h>
25 #include "theory/theory.h"
26 #include "theory/theory_engine.h"
27 #include "theory/theoryof_table.h"
28 #include "expr/node.h"
29 #include "expr/node_manager.h"
30 #include "expr/kind.h"
31 #include "context/context.h"
32 #include "util/rational.h"
33 #include "util/integer.h"
34 #include "util/options.h"
35 #include "util/Assert.h"
38 using namespace CVC4::theory
;
39 using namespace CVC4::expr
;
40 using namespace CVC4::context
;
41 using namespace CVC4::kind
;
46 * Test the SharedTermManager.
48 class SharedTermManagerBlack
: public CxxTest::TestSuite
{
52 NodeManagerScope
* d_scope
;
53 TheoryEngine
* d_theoryEngine
;
61 d_nm
= new NodeManager(d_ctxt
);
62 d_scope
= new NodeManagerScope(d_nm
);
64 d_theoryEngine
= new TheoryEngine(d_ctxt
, &d_options
);
68 d_theoryEngine
->shutdown();
69 delete d_theoryEngine
;
77 void testExplanation() {
78 // Example from Barcelogic paper
79 SharedTermManager
* stm
= d_theoryEngine
->getSharedTermManager();
81 Node x1
= d_nm
->mkVar("x1", d_nm
->integerType());
82 Node x2
= d_nm
->mkVar("x2", d_nm
->integerType());
83 Node x3
= d_nm
->mkVar("x3", d_nm
->integerType());
84 Node x4
= d_nm
->mkVar("x4", d_nm
->integerType());
85 Node x5
= d_nm
->mkVar("x5", d_nm
->integerType());
86 Node x6
= d_nm
->mkVar("x6", d_nm
->integerType());
87 Node x7
= d_nm
->mkVar("x7", d_nm
->integerType());
88 Node x8
= d_nm
->mkVar("x8", d_nm
->integerType());
89 Node x9
= d_nm
->mkVar("x9", d_nm
->integerType());
90 Node x10
= d_nm
->mkVar("x10", d_nm
->integerType());
91 Node x11
= d_nm
->mkVar("x11", d_nm
->integerType());
92 Node x12
= d_nm
->mkVar("x12", d_nm
->integerType());
93 Node x13
= d_nm
->mkVar("x13", d_nm
->integerType());
94 Node x14
= d_nm
->mkVar("x14", d_nm
->integerType());
96 Node a1
, a2
, a3
, a4
, a5
, a6
, a7
, a8
, a9
, a10
, a11
, a12
;
100 stm
->addEq(a1
= d_nm
->mkNode(EQUAL
, x1
, x8
));
101 stm
->addEq(a2
= d_nm
->mkNode(EQUAL
, x7
, x2
));
102 stm
->addEq(a3
= d_nm
->mkNode(EQUAL
, x3
, x13
));
103 stm
->addEq(a4
= d_nm
->mkNode(EQUAL
, x7
, x1
));
104 stm
->addEq(a5
= d_nm
->mkNode(EQUAL
, x6
, x7
));
105 stm
->addEq(a6
= d_nm
->mkNode(EQUAL
, x9
, x5
));
106 stm
->addEq(a7
= d_nm
->mkNode(EQUAL
, x9
, x3
));
107 stm
->addEq(a8
= d_nm
->mkNode(EQUAL
, x14
, x11
));
108 stm
->addEq(a9
= d_nm
->mkNode(EQUAL
, x10
, x4
));
109 stm
->addEq(a10
= d_nm
->mkNode(EQUAL
, x12
, x9
));
110 stm
->addEq(a11
= d_nm
->mkNode(EQUAL
, x4
, x11
));
111 stm
->addEq(a12
= d_nm
->mkNode(EQUAL
, x10
, x7
));
113 Node explanation
= stm
->explain(d_nm
->mkNode(EQUAL
, x1
, x4
));
115 TS_ASSERT(explanation
.getNumChildren() == 3);
117 Node e0
= explanation
[0];
118 Node e1
= explanation
[1];
119 Node e2
= explanation
[2];
121 TS_ASSERT(e0
== a4
&& e1
== a9
&& e2
== a12
);
123 TS_ASSERT(stm
->getRep(x8
) == stm
->getRep(x14
));
124 TS_ASSERT(stm
->getRep(x2
) != stm
->getRep(x12
));
128 TS_ASSERT(stm
->getRep(x8
) != stm
->getRep(x14
));
132 stm
->addEq(a1
= d_nm
->mkNode(EQUAL
, x1
, x8
));
133 stm
->addEq(a2
= d_nm
->mkNode(EQUAL
, x8
, x2
));
134 stm
->addEq(a3
= d_nm
->mkNode(EQUAL
, x2
, x3
));
136 explanation
= stm
->explain(d_nm
->mkNode(EQUAL
, x1
, x3
));
137 TS_ASSERT(explanation
.getNumChildren() == 3);
143 TS_ASSERT(e0
== a1
&& e1
== a2
&& e2
== a3
);
145 TS_ASSERT(stm
->getRep(x8
) == stm
->getRep(x2
));