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     d_arith->propagate(d_level);
 163
 164     Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
 165     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
 166     Node leq0ThenLt1  = NodeBuilder<2>(IMPLIES) << leq0 << lt1;
 167
 168     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 169
 170     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
 171     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1);
 172
 173     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 174     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1);
 175
 176     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
 177     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1);
 178   }
 179
 180
 181   void testTPLeq0() {
 182     Node x = d_nm->mkVar(*d_realType);
 183     Node c0 = d_nm->mkConst<Rational>(d_zero);
 184     Node c1 = d_nm->mkConst<Rational>(d_one);
 185
 186     Node leq0 = d_nm->mkNode(LEQ, x, c0);
 187     Node leq1 = d_nm->mkNode(LEQ, x, c1);
 188     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 189     Node lt1 = d_nm->mkNode(NOT, geq1);
 190
 191     fakeTheoryEnginePreprocess(leq0);
 192     fakeTheoryEnginePreprocess(leq1);
 193     fakeTheoryEnginePreprocess(geq1);
 194
 195     d_arith->assertFact(leq0);
 196
 197
 198     d_arith->check(d_level);
 199
 200     Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
 201     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
 202     Node leq0ThenLt1  = NodeBuilder<2>(IMPLIES) << leq0 << lt1;
 203
 204     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 205
 206     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
 207     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1);
 208
 209     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 210     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1);
 211
 212     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
 213     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1);
 214   }
 215   void testTPLeq1() {
 216     Node x = d_nm->mkVar(*d_realType);
 217     Node c0 = d_nm->mkConst<Rational>(d_zero);
 218     Node c1 = d_nm->mkConst<Rational>(d_one);
 219
 220     Node leq0 = d_nm->mkNode(LEQ, x, c0);
 221     Node leq1 = d_nm->mkNode(LEQ, x, c1);
 222     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 223     Node lt1 = d_nm->mkNode(NOT, geq1);
 224
 225     fakeTheoryEnginePreprocess(leq0);
 226     fakeTheoryEnginePreprocess(leq1);
 227     fakeTheoryEnginePreprocess(geq1);
 228
 229     d_arith->assertFact(leq1);
 230
 231
 232     d_arith->check(d_level);
 233     d_arith->propagate(d_level);
 234
 235     Node leq0ThenLeq1 = NodeBuilder<2>(IMPLIES) << leq0 << (leq1);
 236     Node lt1ThenLeq1  = NodeBuilder<2>(IMPLIES) << lt1 << leq1;
 237     Node leq0ThenLt1  = NodeBuilder<2>(IMPLIES) << leq0 << lt1;
 238
 239     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 240
 241     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
 242     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), leq0ThenLeq1);
 243
 244     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 245     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), lt1ThenLeq1);
 246
 247     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), LEMMA);
 248     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq0ThenLt1);
 249   }
 250 };