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, NULL);
  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     Node gt0 = d_nm->mkNode(NOT, leq0);
 154     Node gt1 = d_nm->mkNode(NOT, leq1);
 155
 156     fakeTheoryEnginePreprocess(leq0);
 157     fakeTheoryEnginePreprocess(leq1);
 158     fakeTheoryEnginePreprocess(geq1);
 159
 160     d_arith->assertFact(lt1);
 161
 162
 163     d_arith->check(d_level);
 164     d_arith->propagate(d_level);
 165
 166     Node gt1ThenGt0  = NodeBuilder<2>(IMPLIES) << gt1 << gt0;
 167     Node geq1ThenGt0  = NodeBuilder<2>(IMPLIES) << geq1 << gt0;
 168     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
 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), gt1ThenGt0);
 174
 175     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 176     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0);
 177
 178     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
 179     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1);
 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     Node gt0 = d_nm->mkNode(NOT, leq0);
 193     Node gt1 = d_nm->mkNode(NOT, leq1);
 194
 195     fakeTheoryEnginePreprocess(leq0);
 196     fakeTheoryEnginePreprocess(leq1);
 197     fakeTheoryEnginePreprocess(geq1);
 198
 199     d_arith->assertFact(leq0);
 200
 201
 202     d_arith->check(d_level);
 203
 204     Node gt1ThenGt0  = NodeBuilder<2>(IMPLIES) << gt1 << gt0;
 205     Node geq1ThenGt0  = NodeBuilder<2>(IMPLIES) << geq1 << gt0;
 206     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
 207
 208     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 209
 210     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
 211     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0);
 212
 213     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 214     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0);
 215
 216     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
 217     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1);
 218   }
 219   void testTPLeq1() {
 220     Node x = d_nm->mkVar(*d_realType);
 221     Node c0 = d_nm->mkConst<Rational>(d_zero);
 222     Node c1 = d_nm->mkConst<Rational>(d_one);
 223
 224     Node leq0 = d_nm->mkNode(LEQ, x, c0);
 225     Node leq1 = d_nm->mkNode(LEQ, x, c1);
 226     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 227     Node lt1 = d_nm->mkNode(NOT, geq1);
 228     Node gt0 = d_nm->mkNode(NOT, leq0);
 229     Node gt1 = d_nm->mkNode(NOT, leq1);
 230
 231     fakeTheoryEnginePreprocess(leq0);
 232     fakeTheoryEnginePreprocess(leq1);
 233     fakeTheoryEnginePreprocess(geq1);
 234
 235     d_arith->assertFact(leq1);
 236
 237
 238     d_arith->check(d_level);
 239     d_arith->propagate(d_level);
 240
 241     Node gt1ThenGt0  = NodeBuilder<2>(IMPLIES) << gt1 << gt0;
 242     Node geq1ThenGt0  = NodeBuilder<2>(IMPLIES) << geq1 << gt0;
 243     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
 244
 245     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 246
 247     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
 248     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt1ThenGt0);
 249
 250     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 251     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq1ThenGt0);
 252
 253     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
 254     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1ThenLeq1);
 255   }
 256 };