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): barrett, 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(d_ctxt, d_outputChannel, Valuation(NULL));
 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 testTPLt1() {
 145     Node x = d_nm->mkVar(*d_realType);
 146     Node c0 = d_nm->mkConst<Rational>(d_zero);
 147     Node c1 = d_nm->mkConst<Rational>(d_one);
 148
 149     Node leq0 = d_nm->mkNode(LEQ, x, c0);
 150     Node leq1 = d_nm->mkNode(LEQ, x, c1);
 151     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 152     Node lt1 = d_nm->mkNode(NOT, geq1);
 153
 154     fakeTheoryEnginePreprocess(leq0);
 155     fakeTheoryEnginePreprocess(leq1);
 156     fakeTheoryEnginePreprocess(geq1);
 157
 158     d_arith->assertFact(lt1);
 159
 160
 161     d_arith->check(d_level);
 162     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
 163
 164     d_arith->propagate(d_level);
 165
 166     Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
 167     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
 168     Node leq0ThenLt1  = NodeBuilder<2>(IMPLIES) << leq0 << lt1;
 169
 170     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 171
 172     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
 173     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1);
 174
 175     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 176     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1);
 177
 178     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
 179     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1);
 180   }
 181
 182
 183   void testTPLeq0() {
 184     Node x = d_nm->mkVar(*d_realType);
 185     Node c0 = d_nm->mkConst<Rational>(d_zero);
 186     Node c1 = d_nm->mkConst<Rational>(d_one);
 187
 188     Node leq0 = d_nm->mkNode(LEQ, x, c0);
 189     Node leq1 = d_nm->mkNode(LEQ, x, c1);
 190     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 191     Node lt1 = d_nm->mkNode(NOT, geq1);
 192
 193     fakeTheoryEnginePreprocess(leq0);
 194     fakeTheoryEnginePreprocess(leq1);
 195     fakeTheoryEnginePreprocess(geq1);
 196
 197     d_arith->assertFact(leq0);
 198
 199
 200     d_arith->check(d_level);
 201     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
 202
 203     d_arith->propagate(d_level);
 204
 205     Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
 206     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
 207     Node leq0ThenLt1  = NodeBuilder<2>(IMPLIES) << leq0 << lt1;
 208
 209     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 210
 211     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
 212     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1);
 213
 214     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 215     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1);
 216
 217     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
 218     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1);
 219   }
 220   void testTPLeq1() {
 221     Node x = d_nm->mkVar(*d_realType);
 222     Node c0 = d_nm->mkConst<Rational>(d_zero);
 223     Node c1 = d_nm->mkConst<Rational>(d_one);
 224
 225     Node leq0 = d_nm->mkNode(LEQ, x, c0);
 226     Node leq1 = d_nm->mkNode(LEQ, x, c1);
 227     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 228     Node lt1 = d_nm->mkNode(NOT, geq1);
 229
 230     fakeTheoryEnginePreprocess(leq0);
 231     fakeTheoryEnginePreprocess(leq1);
 232     fakeTheoryEnginePreprocess(geq1);
 233
 234     d_arith->assertFact(leq1);
 235
 236
 237     d_arith->check(d_level);
 238     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
 239
 240     d_arith->propagate(d_level);
 241
 242     Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
 243     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
 244     Node leq0ThenLt1  = NodeBuilder<2>(IMPLIES) << leq0 << lt1;
 245
 246     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 247
 248     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
 249     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1);
 250
 251     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 252     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1);
 253
 254     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
 255     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1);
 256   }
 257
 258   void testConflict() {
 259     Node x = d_nm->mkVar(*d_realType);
 260     Node c0 = d_nm->mkConst<Rational>(d_zero);
 261     Node c1 = d_nm->mkConst<Rational>(d_one);
 262
 263     Node leq0 = d_nm->mkNode(LEQ, x, c0);
 264     Node leq1 = d_nm->mkNode(LEQ, x, c1);
 265     Node gt1 =  d_nm->mkNode(NOT, leq1);
 266
 267     fakeTheoryEnginePreprocess(leq0);
 268     fakeTheoryEnginePreprocess(leq1);
 269
 270     d_arith->assertFact(leq0);
 271     d_arith->assertFact(gt1);
 272
 273     d_arith->check(d_level);
 274
 275
 276     Node conf =  d_nm->mkNode(AND, leq0, gt1);
 277     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 1u);
 278
 279     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), CONFLICT);
 280     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), conf);
 281   }
 282 };