test/unit/theory/theory_arith_white.h

   1 /*********************                                                        */
   2 /*! \file theory_arith_white.h
   3  ** \verbatim
   4  ** Original author: taking
   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 [[ Add one-line brief description here ]]
  15  **
  16  ** [[ Add lengthier description here ]]
  17  ** \todo document this file
  18  **/
  19
  20
  21 #include <cxxtest/TestSuite.h>
  22
  23 #include "theory/theory.h"
  24 #include "theory/arith/theory_arith.h"
  25 #include "expr/node.h"
  26 #include "expr/node_manager.h"
  27 #include "context/context.h"
  28 #include "util/rational.h"
  29
  30 #include "theory/theory_test_utils.h"
  31
  32 #include <vector>
  33
  34 using namespace CVC4;
  35 using namespace CVC4::theory;
  36 using namespace CVC4::theory::arith;
  37 using namespace CVC4::expr;
  38 using namespace CVC4::context;
  39 using namespace CVC4::kind;
  40
  41 using namespace std;
  42
  43 class TheoryArithWhite : public CxxTest::TestSuite {
  44
  45   Context* d_ctxt;
  46   NodeManager* d_nm;
  47   NodeManagerScope* d_scope;
  48
  49   TestOutputChannel d_outputChannel;
  50   Theory::Effort d_level;
  51
  52   TheoryArith* d_arith;
  53
  54   TypeNode* d_booleanType;
  55   TypeNode* d_realType;
  56
  57   const Rational d_zero;
  58   const Rational d_one;
  59
  60   std::set<Node>* preregistered;
  61
  62   bool debug;
  63
  64 public:
  65
  66   TheoryArithWhite() : d_level(Theory::FULL_EFFORT), d_zero(0), d_one(1), debug(false) {}
  67
  68   void fakeTheoryEnginePreprocess(TNode inp){
  69     Node rewrite = inp; //FIXME this needs to enforce that inp is fully rewritten already!
  70
  71     if(debug) cout << rewrite << inp << endl;
  72
  73     std::list<Node> toPreregister;
  74
  75     toPreregister.push_back(rewrite);
  76     for(std::list<Node>::iterator i = toPreregister.begin(); i != toPreregister.end(); ++i){
  77       Node n = *i;
  78       preregistered->insert(n);
  79
  80       for(Node::iterator citer = n.begin(); citer != n.end(); ++citer){
  81         Node c = *citer;
  82         if(preregistered->find(c) == preregistered->end()){
  83           toPreregister.push_back(c);
  84         }
  85       }
  86     }
  87     for(std::list<Node>::reverse_iterator i = toPreregister.rbegin(); i != toPreregister.rend(); ++i){
  88       Node n = *i;
  89       if(debug) cout << n.getId() << " "<< n << endl;
  90       d_arith->preRegisterTerm(n);
  91     }
  92   }
  93
  94   void setUp() {
  95     d_ctxt = new Context;
  96     d_nm = new NodeManager(d_ctxt);
  97     d_scope = new NodeManagerScope(d_nm);
  98     d_outputChannel.clear();
  99     d_arith = new TheoryArith(0, d_ctxt, d_outputChannel);
 100
 101     preregistered = new std::set<Node>();
 102
 103     d_booleanType = new TypeNode(d_nm->booleanType());
 104     d_realType = new TypeNode(d_nm->realType());
 105
 106   }
 107
 108   void tearDown() {
 109     delete d_realType;
 110     delete d_booleanType;
 111
 112     delete preregistered;
 113
 114     delete d_arith;
 115     d_outputChannel.clear();
 116     delete d_scope;
 117     delete d_nm;
 118     delete d_ctxt;
 119   }
 120
 121   void testAssert() {
 122     Node x = d_nm->mkVar(*d_realType);
 123     Node c = d_nm->mkConst<Rational>(d_zero);
 124
 125     Node leq = d_nm->mkNode(LEQ, x, c);
 126     fakeTheoryEnginePreprocess(leq);
 127
 128     d_arith->assertFact(leq);
 129
 130     d_arith->check(d_level);
 131
 132     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
 133   }
 134
 135   Node simulateSplit(TNode l, TNode r){
 136     Node eq = d_nm->mkNode(EQUAL, l, r);
 137     Node lt = d_nm->mkNode(LT, l, r);
 138     Node gt = d_nm->mkNode(GT, l, r);
 139
 140     Node dis = d_nm->mkNode(OR, eq, lt, gt);
 141     return dis;
 142   }
 143
 144   void testBasicConflict() {
 145     Node x = d_nm->mkVar(*d_realType);
 146     Node c = d_nm->mkConst<Rational>(d_zero);
 147
 148     Node eq = d_nm->mkNode(EQUAL, x, c);
 149     Node lt = d_nm->mkNode(NOT, d_nm->mkNode(GEQ, x, c));
 150     Node expectedDisjunct = simulateSplit(x,c);
 151
 152     fakeTheoryEnginePreprocess(eq);
 153     fakeTheoryEnginePreprocess(lt);
 154
 155     d_arith->assertFact(eq);
 156     d_arith->assertFact(lt);
 157
 158
 159     d_arith->check(d_level);
 160
 161     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
 162     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), expectedDisjunct);
 163     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), AUG_LEMMA);
 164
 165     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), CONFLICT);
 166
 167     Node expectedClonflict = d_nm->mkNode(AND, eq, lt);
 168
 169     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedClonflict);
 170   }
 171
 172   void testBasicPropagate() {
 173     Node x = d_nm->mkVar(*d_realType);
 174     Node c = d_nm->mkConst<Rational>(d_zero);
 175
 176     Node eq = d_nm->mkNode(EQUAL, x, c);
 177     Node lt = d_nm->mkNode(NOT, d_nm->mkNode(GEQ, x, c));
 178     Node expectedDisjunct = simulateSplit(x,c);
 179
 180     fakeTheoryEnginePreprocess(eq);
 181     fakeTheoryEnginePreprocess(lt);
 182
 183     d_arith->assertFact(eq);
 184
 185
 186     d_arith->check(d_level);
 187     d_arith->propagate(d_level);
 188
 189     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
 190     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), AUG_LEMMA);
 191
 192
 193     Node expectedProp = d_nm->mkNode(GEQ, x, c);
 194     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE);
 195     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedProp);
 196
 197   }
 198   void testTPLt1() {
 199     Node x = d_nm->mkVar(*d_realType);
 200     Node c0 = d_nm->mkConst<Rational>(d_zero);
 201     Node c1 = d_nm->mkConst<Rational>(d_one);
 202
 203     Node leq0 = d_nm->mkNode(LEQ, x, c0);
 204     Node leq1 = d_nm->mkNode(LEQ, x, c1);
 205     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 206     Node lt1 = d_nm->mkNode(NOT, geq1);
 207
 208     fakeTheoryEnginePreprocess(leq0);
 209     fakeTheoryEnginePreprocess(leq1);
 210     fakeTheoryEnginePreprocess(geq1);
 211
 212     d_arith->assertFact(lt1);
 213
 214
 215     d_arith->check(d_level);
 216     d_arith->propagate(d_level);
 217
 218 #ifdef CVC4_ASSERTIONS
 219     TS_ASSERT_THROWS(  d_arith->explain(leq0, d_level), AssertionException );
 220     TS_ASSERT_THROWS(  d_arith->explain(lt1, d_level), AssertionException );
 221 #endif
 222     d_arith->explain(leq1, d_level);
 223
 224     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
 225     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPAGATE);
 226     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), EXPLANATION);
 227     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq1);
 228     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1);
 229   }
 230
 231
 232   void testTPLeq0() {
 233     Node x = d_nm->mkVar(*d_realType);
 234     Node c0 = d_nm->mkConst<Rational>(d_zero);
 235     Node c1 = d_nm->mkConst<Rational>(d_one);
 236
 237     Node leq0 = d_nm->mkNode(LEQ, x, c0);
 238     Node leq1 = d_nm->mkNode(LEQ, x, c1);
 239     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 240     Node lt1 = d_nm->mkNode(NOT, geq1);
 241
 242     fakeTheoryEnginePreprocess(leq0);
 243     fakeTheoryEnginePreprocess(leq1);
 244     fakeTheoryEnginePreprocess(geq1);
 245
 246     d_arith->assertFact(leq0);
 247
 248
 249     d_arith->check(d_level);
 250     d_arith->propagate(d_level);
 251
 252
 253     d_arith->explain(lt1, d_level);
 254 #ifdef CVC4_ASSERTIONS
 255     TS_ASSERT_THROWS(  d_arith->explain(leq0, d_level), AssertionException );
 256 #endif
 257     d_arith->explain(leq1, d_level);
 258
 259     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u);
 260     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), PROPAGATE);
 261     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE);
 262     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), EXPLANATION);
 263     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), EXPLANATION);
 264
 265     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1);
 266     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq1);
 267
 268
 269     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0);
 270     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(3), leq0);
 271   }
 272   void testTPLeq1() {
 273     Node x = d_nm->mkVar(*d_realType);
 274     Node c0 = d_nm->mkConst<Rational>(d_zero);
 275     Node c1 = d_nm->mkConst<Rational>(d_one);
 276
 277     Node leq0 = d_nm->mkNode(LEQ, x, c0);
 278     Node leq1 = d_nm->mkNode(LEQ, x, c1);
 279     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 280     Node lt1 = d_nm->mkNode(NOT, geq1);
 281
 282     fakeTheoryEnginePreprocess(leq0);
 283     fakeTheoryEnginePreprocess(leq1);
 284     fakeTheoryEnginePreprocess(geq1);
 285
 286     d_arith->assertFact(leq1);
 287
 288
 289     d_arith->check(d_level);
 290     d_arith->propagate(d_level);
 291
 292 #ifdef CVC4_ASSERTIONS
 293     TS_ASSERT_THROWS(  d_arith->explain(leq0, d_level), AssertionException );
 294     TS_ASSERT_THROWS(  d_arith->explain(leq1, d_level), AssertionException );
 295     TS_ASSERT_THROWS(  d_arith->explain(lt1, d_level), AssertionException );
 296 #endif
 297
 298     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
 299   }
 300 };