test/unit/theory/theory_black.h

   1 /*********************                                                        */
   2 /*! \file theory_black.h
   3  ** \verbatim
   4  ** Original author: taking
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): cconway, dejan
   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::theory::Theory.
  15  **
  16  ** Black box testing of CVC4::theory::Theory.
  17  **/
  18
  19 #include <cxxtest/TestSuite.h>
  20
  21 #include "theory/theory.h"
  22 #include "expr/node.h"
  23 #include "expr/node_manager.h"
  24 #include "context/context.h"
  25
  26 #include <vector>
  27
  28 using namespace CVC4;
  29 using namespace CVC4::theory;
  30 using namespace CVC4::expr;
  31 using namespace CVC4::context;
  32
  33 using namespace std;
  34
  35 /**
  36  * Very basic OutputChannel for testing simple Theory Behaviour.
  37  * Stores a call sequence for the output channel
  38  */
  39 enum OutputChannelCallType{CONFLICT, PROPAGATE, LEMMA, EXPLANATION};
  40 class TestOutputChannel : public OutputChannel {
  41 private:
  42   void push(OutputChannelCallType call, TNode n) {
  43     d_callHistory.push_back(make_pair(call, n));
  44   }
  45
  46 public:
  47   vector< pair<OutputChannelCallType, Node> > d_callHistory;
  48
  49   TestOutputChannel() {}
  50
  51   ~TestOutputChannel() {}
  52
  53   void safePoint() throw(Interrupted, AssertionException) {}
  54
  55   void conflict(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
  56     push(CONFLICT, n);
  57   }
  58
  59   void propagate(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
  60     push(PROPAGATE, n);
  61   }
  62
  63   void lemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){
  64     push(LEMMA, n);
  65   }
  66   void augmentingLemma(TNode n, bool safe = false) throw(Interrupted, AssertionException){
  67     Unreachable();
  68   }
  69
  70   void explanation(TNode n, bool safe = false) throw(Interrupted, AssertionException) {
  71     push(EXPLANATION, n);
  72   }
  73
  74   void clear() {
  75     d_callHistory.clear();
  76   }
  77
  78   Node getIthNode(int i) {
  79     Node tmp = (d_callHistory[i]).second;
  80     return tmp;
  81   }
  82
  83   OutputChannelCallType getIthCallType(int i) {
  84     return (d_callHistory[i]).first;
  85   }
  86
  87   unsigned getNumCalls() {
  88     return d_callHistory.size();
  89   }
  90 };
  91
  92 class DummyTheory : public Theory {
  93 public:
  94   set<Node> d_registered;
  95   vector<Node> d_getSequence;
  96
  97   DummyTheory(Context* ctxt, OutputChannel& out) :
  98     Theory(0, ctxt, out) {
  99   }
 100
 101   void registerTerm(TNode n) {
 102     // check that we registerTerm() a term only once
 103     TS_ASSERT(d_registered.find(n) == d_registered.end());
 104
 105     for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
 106       // check that registerTerm() is called in reverse topological order
 107       TS_ASSERT(d_registered.find(*i) != d_registered.end());
 108     }
 109
 110     d_registered.insert(n);
 111   }
 112
 113   Node getWrapper() {
 114     Node n = get();
 115     d_getSequence.push_back(n);
 116     return n;
 117   }
 118
 119   bool doneWrapper() {
 120     return done();
 121   }
 122
 123   void check(Effort e) {
 124     while(!done()) {
 125       getWrapper();
 126     }
 127   }
 128
 129   void preRegisterTerm(TNode n) {}
 130   void propagate(Effort level) {}
 131   void explain(TNode n, Effort level) {}
 132   string identify() const { return "DummyTheory"; }
 133 };
 134
 135 class TheoryBlack : public CxxTest::TestSuite {
 136
 137   Context* d_ctxt;
 138   NodeManager* d_nm;
 139   NodeManagerScope* d_scope;
 140
 141   TestOutputChannel d_outputChannel;
 142
 143   DummyTheory* d_dummy;
 144
 145   Node atom0;
 146   Node atom1;
 147
 148 public:
 149
 150   void setUp() {
 151     d_ctxt = new Context;
 152     d_nm = new NodeManager(d_ctxt);
 153     d_scope = new NodeManagerScope(d_nm);
 154     d_dummy = new DummyTheory(d_ctxt, d_outputChannel);
 155     d_outputChannel.clear();
 156     atom0 = d_nm->mkConst(true);
 157     atom1 = d_nm->mkConst(false);
 158   }
 159
 160   void tearDown() {
 161     atom1 = Node::null();
 162     atom0 = Node::null();
 163     delete d_dummy;
 164     delete d_scope;
 165     delete d_nm;
 166     delete d_ctxt;
 167   }
 168
 169   void testEffort(){
 170     Theory::Effort m = Theory::MIN_EFFORT;
 171     Theory::Effort q = Theory::QUICK_CHECK;
 172     Theory::Effort s = Theory::STANDARD;
 173     Theory::Effort f = Theory::FULL_EFFORT;
 174
 175     TS_ASSERT( Theory::minEffortOnly(m));
 176     TS_ASSERT(!Theory::minEffortOnly(q));
 177     TS_ASSERT(!Theory::minEffortOnly(s));
 178     TS_ASSERT(!Theory::minEffortOnly(f));
 179
 180     TS_ASSERT(!Theory::quickCheckOnly(m));
 181     TS_ASSERT( Theory::quickCheckOnly(q));
 182     TS_ASSERT(!Theory::quickCheckOnly(s));
 183     TS_ASSERT(!Theory::quickCheckOnly(f));
 184
 185     TS_ASSERT(!Theory::standardEffortOnly(m));
 186     TS_ASSERT(!Theory::standardEffortOnly(q));
 187     TS_ASSERT( Theory::standardEffortOnly(s));
 188     TS_ASSERT(!Theory::standardEffortOnly(f));
 189
 190     TS_ASSERT(!Theory::fullEffort(m));
 191     TS_ASSERT(!Theory::fullEffort(q));
 192     TS_ASSERT(!Theory::fullEffort(s));
 193     TS_ASSERT( Theory::fullEffort(f));
 194
 195     TS_ASSERT(!Theory::quickCheckOrMore(m));
 196     TS_ASSERT( Theory::quickCheckOrMore(q));
 197     TS_ASSERT( Theory::quickCheckOrMore(s));
 198     TS_ASSERT( Theory::quickCheckOrMore(f));
 199
 200     TS_ASSERT(!Theory::standardEffortOrMore(m));
 201     TS_ASSERT(!Theory::standardEffortOrMore(q));
 202     TS_ASSERT( Theory::standardEffortOrMore(s));
 203     TS_ASSERT( Theory::standardEffortOrMore(f));
 204   }
 205
 206   void testDone() {
 207     TS_ASSERT(d_dummy->doneWrapper());
 208
 209     d_dummy->assertFact(atom0);
 210     d_dummy->assertFact(atom1);
 211
 212     TS_ASSERT(!d_dummy->doneWrapper());
 213
 214     d_dummy->check(Theory::FULL_EFFORT);
 215
 216     TS_ASSERT(d_dummy->doneWrapper());
 217   }
 218
 219   // FIXME: move this to theory_engine test?
 220 //   void testRegisterTerm() {
 221 //     TS_ASSERT(d_dummy->doneWrapper());
 222
 223 //     TypeNode typeX = d_nm->booleanType();
 224 //     TypeNode typeF = d_nm->mkFunctionType(typeX, typeX);
 225
 226 //     Node x = d_nm->mkVar("x",typeX);
 227 //     Node f = d_nm->mkVar("f",typeF);
 228 //     Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
 229 //     Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
 230 //     Node f_x_eq_x = f_x.eqNode(x);
 231 //     Node x_eq_f_f_x = x.eqNode(f_f_x);
 232
 233 //     d_dummy->assertFact(f_x_eq_x);
 234 //     d_dummy->assertFact(x_eq_f_f_x);
 235
 236 //     Node got = d_dummy->getWrapper();
 237
 238 //     TS_ASSERT_EQUALS(got, f_x_eq_x);
 239
 240 //     TS_ASSERT_EQUALS(5u, d_dummy->d_registered.size());
 241 //     TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end());
 242 //     TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end());
 243 //     TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end());
 244 //     TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end());
 245 //     TS_ASSERT(d_dummy->d_registered.find(d_nm->operatorOf(kind::EQUAL)) != d_dummy->d_registered.end());
 246 //     TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end());
 247 //     TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end());
 248
 249 //     TS_ASSERT(!d_dummy->doneWrapper());
 250
 251 //     got = d_dummy->getWrapper();
 252
 253 //     TS_ASSERT_EQUALS(got, x_eq_f_f_x);
 254
 255 //     TS_ASSERT_EQUALS(7u, d_dummy->d_registered.size());
 256 //     TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end());
 257 //     TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end());
 258
 259 //     TS_ASSERT(d_dummy->doneWrapper());
 260 //   }
 261
 262   void testOutputChannelAccessors() {
 263     /* void setOutputChannel(OutputChannel& out)  */
 264     /* OutputChannel& getOutputChannel() */
 265
 266     TestOutputChannel theOtherChannel;
 267
 268     TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &d_outputChannel);
 269
 270     d_dummy->setOutputChannel(theOtherChannel);
 271
 272     TS_ASSERT_EQUALS(&(d_dummy->getOutputChannel()), &theOtherChannel);
 273
 274     const OutputChannel& oc = d_dummy->getOutputChannel();
 275
 276     TS_ASSERT_EQUALS(&oc, &theOtherChannel);
 277   }
 278 };