test/unit/theory/shared_term_manager_black.h

   1 /*********************                                                        */
   2 /*! \file shared_term_manager_black.h
   3  ** \verbatim
   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
  13  **
  14  ** \brief Black box testing of CVC4::SharedTermManager.
  15  **
  16  ** Black box testing of CVC4::SharedTermManager.
  17  **/
  18
  19 #include <cxxtest/TestSuite.h>
  20
  21 #include <iostream>
  22 #include <string>
  23 #include <deque>
  24
  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"
  36
  37 using namespace CVC4;
  38 using namespace CVC4::theory;
  39 using namespace CVC4::expr;
  40 using namespace CVC4::context;
  41 using namespace CVC4::kind;
  42
  43 using namespace std;
  44
  45 /**
  46  * Test the SharedTermManager.
  47  */
  48 class SharedTermManagerBlack : public CxxTest::TestSuite {
  49   Context* d_ctxt;
  50
  51   NodeManager* d_nm;
  52   NodeManagerScope* d_scope;
  53   TheoryEngine* d_theoryEngine;
  54   Options d_options;
  55
  56 public:
  57
  58   void setUp() {
  59     d_ctxt = new Context;
  60
  61     d_nm = new NodeManager(d_ctxt);
  62     d_scope = new NodeManagerScope(d_nm);
  63
  64     d_theoryEngine = new TheoryEngine(d_ctxt, &d_options);
  65   }
  66
  67   void tearDown() {
  68     d_theoryEngine->shutdown();
  69     delete d_theoryEngine;
  70
  71     delete d_scope;
  72     delete d_nm;
  73
  74     delete d_ctxt;
  75   }
  76
  77   void testExplanation() {
  78     // Example from Barcelogic paper
  79     SharedTermManager* stm = d_theoryEngine->getSharedTermManager();
  80
  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());
  95
  96     Node a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12;
  97
  98     d_ctxt->push();
  99
 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));
 112
 113     Node explanation = stm->explain(d_nm->mkNode(EQUAL, x1, x4));
 114
 115     TS_ASSERT(explanation.getNumChildren() == 3);
 116
 117     Node e0 = explanation[0];
 118     Node e1 = explanation[1];
 119     Node e2 = explanation[2];
 120
 121     TS_ASSERT(e0 == a4 && e1 == a9 && e2 == a12);
 122
 123     TS_ASSERT(stm->getRep(x8) == stm->getRep(x14));
 124     TS_ASSERT(stm->getRep(x2) != stm->getRep(x12));
 125
 126     d_ctxt->pop();
 127
 128     TS_ASSERT(stm->getRep(x8) != stm->getRep(x14));
 129
 130     d_ctxt->push();
 131
 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));
 135
 136     explanation = stm->explain(d_nm->mkNode(EQUAL, x1, x3));
 137     TS_ASSERT(explanation.getNumChildren() == 3);
 138
 139     e0 = explanation[0];
 140     e1 = explanation[1];
 141     e2 = explanation[2];
 142
 143     TS_ASSERT(e0 == a1 && e1 == a2 && e2 == a3);
 144
 145     TS_ASSERT(stm->getRep(x8) == stm->getRep(x2));
 146
 147     d_ctxt->pop();
 148   }
 149
 150 };