test/unit/theory/theory_arith_white.h

   1 /*********************                                                        */
   2 /*! \file theory_arith_white.h
   3  ** \verbatim
   4  ** Original author: Tim King
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): Dejan Jovanovic
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18
  19 #include <cxxtest/TestSuite.h>
  20
  21 #include "theory/theory.h"
  22 #include "theory/theory_engine.h"
  23 #include "theory/arith/theory_arith.h"
  24 #include "theory/quantifiers_engine.h"
  25 #include "expr/node.h"
  26 #include "expr/node_manager.h"
  27 #include "context/context.h"
  28 #include "util/rational.h"
  29 #include "smt/smt_engine.h"
  30 #include "smt/smt_engine_scope.h"
  31
  32 #include "theory/theory_test_utils.h"
  33
  34 #include <vector>
  35
  36 using namespace CVC4;
  37 using namespace CVC4::theory;
  38 using namespace CVC4::theory::arith;
  39 using namespace CVC4::expr;
  40 using namespace CVC4::context;
  41 using namespace CVC4::kind;
  42 using namespace CVC4::smt;
  43
  44 using namespace std;
  45
  46 class TheoryArithWhite : public CxxTest::TestSuite {
  47
  48   Context* d_ctxt;
  49   UserContext* d_uctxt;
  50   ExprManager* d_em;
  51   NodeManager* d_nm;
  52   SmtScope* d_scope;
  53   SmtEngine* d_smt;
  54
  55   TestOutputChannel d_outputChannel;
  56   LogicInfo d_logicInfo;
  57   Theory::Effort d_level;
  58
  59   TheoryArith* d_arith;
  60
  61   TypeNode* d_booleanType;
  62   TypeNode* d_realType;
  63   TypeNode* d_intType;
  64
  65   const Rational d_zero;
  66   const Rational d_one;
  67
  68   std::set<Node>* preregistered;
  69
  70   bool debug;
  71
  72 public:
  73
  74   TheoryArithWhite() : d_level(Theory::EFFORT_FULL), d_zero(0), d_one(1), debug(false) {}
  75
  76   void fakeTheoryEnginePreprocess(TNode inp){
  77     Node rewrite = inp; //FIXME this needs to enforce that inp is fully rewritten already!
  78
  79     if(debug) cout << rewrite << inp << endl;
  80
  81     std::list<Node> toPreregister;
  82
  83     toPreregister.push_back(rewrite);
  84     for(std::list<Node>::iterator i = toPreregister.begin(); i != toPreregister.end(); ++i){
  85       Node n = *i;
  86       preregistered->insert(n);
  87
  88       for(Node::iterator citer = n.begin(); citer != n.end(); ++citer){
  89         Node c = *citer;
  90         if(preregistered->find(c) == preregistered->end()){
  91           toPreregister.push_back(c);
  92         }
  93       }
  94     }
  95     for(std::list<Node>::reverse_iterator i = toPreregister.rbegin(); i != toPreregister.rend(); ++i){
  96       Node n = *i;
  97       if(debug) cout << n.getId() << " "<< n << endl;
  98       d_arith->preRegisterTerm(n);
  99     }
 100   }
 101
 102   void setUp() {
 103     d_em = new ExprManager();
 104     d_nm = NodeManager::fromExprManager(d_em);
 105     d_smt = new SmtEngine(d_em);
 106     d_ctxt = d_smt->d_context;
 107     d_uctxt = d_smt->d_userContext;
 108     d_scope = new SmtScope(d_smt);
 109     d_outputChannel.clear();
 110     d_logicInfo.lock();
 111
 112     // guard against duplicate statistics assertion errors
 113     delete d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH];
 114     delete d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH];
 115     d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH] = NULL;
 116     d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH] = NULL;
 117
 118     d_arith = new TheoryArith(d_ctxt, d_uctxt, d_outputChannel, Valuation(NULL), d_logicInfo, d_smt->d_theoryEngine->d_quantEngine);
 119
 120     preregistered = new std::set<Node>();
 121
 122     d_booleanType = new TypeNode(d_nm->booleanType());
 123     d_realType = new TypeNode(d_nm->realType());
 124     d_intType = new TypeNode(d_nm->integerType());
 125
 126   }
 127
 128   void tearDown() {
 129     delete d_intType;
 130     delete d_realType;
 131     delete d_booleanType;
 132
 133     delete preregistered;
 134
 135     delete d_arith;
 136     d_outputChannel.clear();
 137     delete d_scope;
 138     delete d_smt;
 139     delete d_em;
 140   }
 141
 142   void testAssert() {
 143     Node x = d_nm->mkVar(*d_realType);
 144     Node c = d_nm->mkConst<Rational>(d_zero);
 145
 146     Node gt = d_nm->mkNode(GT, x, c);
 147     Node leq = gt.notNode();
 148     fakeTheoryEnginePreprocess(leq);
 149
 150     d_arith->assertFact(leq, true);
 151
 152     d_arith->check(d_level);
 153
 154     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 0u);
 155   }
 156
 157   Node simulateSplit(TNode l, TNode r){
 158     Node eq = d_nm->mkNode(EQUAL, l, r);
 159     Node lt = d_nm->mkNode(LT, l, r);
 160     Node gt = d_nm->mkNode(GT, l, r);
 161
 162     Node dis = d_nm->mkNode(OR, eq, lt, gt);
 163     return dis;
 164   }
 165
 166   void testTPLt1() {
 167     Node x = d_nm->mkVar(*d_realType);
 168     Node c0 = d_nm->mkConst<Rational>(d_zero);
 169     Node c1 = d_nm->mkConst<Rational>(d_one);
 170
 171     Node gt0 = d_nm->mkNode(GT, x, c0);
 172     Node gt1 = d_nm->mkNode(GT, x, c1);
 173     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 174     Node leq0 = gt0.notNode();
 175     Node leq1 = gt1.notNode();
 176     Node lt1 = geq1.notNode();
 177
 178     fakeTheoryEnginePreprocess(leq0);
 179     fakeTheoryEnginePreprocess(leq1);
 180     fakeTheoryEnginePreprocess(geq1);
 181
 182     d_arith->presolve();
 183     d_arith->assertFact(lt1, true);
 184     d_arith->check(d_level);
 185     d_arith->propagate(d_level);
 186
 187
 188     Node gt0Orlt1  = NodeBuilder<2>(OR) << gt0 << lt1;
 189     Node geq0OrLeq1  = NodeBuilder<2>(OR) << geq1 << leq1;
 190
 191     cout << d_outputChannel.getIthNode(0) << endl << endl;
 192     cout << d_outputChannel.getIthNode(1) << endl << endl;
 193     cout << d_outputChannel.getIthNode(2) << endl << endl;
 194
 195     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 3u);
 196
 197     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
 198     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
 199
 200     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 201     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
 202
 203     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE);
 204     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), leq1);
 205   }
 206
 207
 208   void testTPLeq0() {
 209     Node x = d_nm->mkVar(*d_realType);
 210     Node c0 = d_nm->mkConst<Rational>(d_zero);
 211     Node c1 = d_nm->mkConst<Rational>(d_one);
 212
 213     Node gt0 = d_nm->mkNode(GT, x, c0);
 214     Node gt1 = d_nm->mkNode(GT, x, c1);
 215     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 216     Node leq0 = gt0.notNode();
 217     Node leq1 = gt1.notNode();
 218     Node lt1 = geq1.notNode();
 219
 220     fakeTheoryEnginePreprocess(leq0);
 221     fakeTheoryEnginePreprocess(leq1);
 222     fakeTheoryEnginePreprocess(geq1);
 223
 224     d_arith->presolve();
 225     d_arith->assertFact(leq0, true);
 226     d_arith->check(d_level);
 227     d_arith->propagate(d_level);
 228
 229     Node gt0Orlt1  = NodeBuilder<2>(OR) << gt0 << lt1;
 230     Node geq0OrLeq1  = NodeBuilder<2>(OR) << geq1 << leq1;
 231
 232     cout << d_outputChannel.getIthNode(0) << endl;
 233     cout << d_outputChannel.getIthNode(1) << endl;
 234     cout << d_outputChannel.getIthNode(2) << endl;
 235     cout << d_outputChannel.getIthNode(3) << endl;
 236
 237     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 4u);
 238
 239     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
 240     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
 241
 242     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 243     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
 244
 245     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(2), PROPAGATE);
 246     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(2), lt1 );
 247
 248     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(3), PROPAGATE);
 249     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(3), leq1);
 250   }
 251
 252   void testTPLeq1() {
 253     Node x = d_nm->mkVar(*d_realType);
 254     Node c0 = d_nm->mkConst<Rational>(d_zero);
 255     Node c1 = d_nm->mkConst<Rational>(d_one);
 256
 257     Node gt0 = d_nm->mkNode(GT, x, c0);
 258     Node gt1 = d_nm->mkNode(GT, x, c1);
 259     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 260     Node leq0 = gt0.notNode();
 261     Node leq1 = gt1.notNode();
 262     Node lt1 = geq1.notNode();
 263
 264     fakeTheoryEnginePreprocess(leq0);
 265     fakeTheoryEnginePreprocess(leq1);
 266     fakeTheoryEnginePreprocess(geq1);
 267
 268     d_arith->presolve();
 269     d_arith->assertFact(leq1, true);
 270     d_arith->check(d_level);
 271     d_arith->propagate(d_level);
 272
 273     Node gt0Orlt1  = NodeBuilder<2>(OR) << gt0 << lt1;
 274     Node geq0OrLeq1  = NodeBuilder<2>(OR) << geq1 << leq1;
 275
 276     cout << d_outputChannel.getIthNode(0) << endl;
 277     cout << d_outputChannel.getIthNode(1) << endl;
 278
 279     TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
 280
 281     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), LEMMA);
 282     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), gt0Orlt1);
 283
 284     TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), LEMMA);
 285     TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), geq0OrLeq1);
 286   }
 287
 288   void testIntNormalForm() {
 289     Node x = d_nm->mkVar(*d_intType);
 290     Node c0 = d_nm->mkConst<Rational>(d_zero);
 291     Node c1 = d_nm->mkConst<Rational>(d_one);
 292     Node c2 = d_nm->mkConst<Rational>(Rational(2));
 293
 294
 295     Node geq0 = d_nm->mkNode(GEQ, x, c0);
 296     Node geq1 = d_nm->mkNode(GEQ, x, c1);
 297     Node geq2 = d_nm->mkNode(GEQ, x, c2);
 298
 299     TS_ASSERT_EQUALS(Rewriter::rewrite(geq0), geq0);
 300     TS_ASSERT_EQUALS(Rewriter::rewrite(geq1), geq1);
 301
 302     Node gt0 = d_nm->mkNode(GT, x, c0);
 303     Node gt1 = d_nm->mkNode(GT, x, c1);
 304
 305     TS_ASSERT_EQUALS(Rewriter::rewrite(gt0), Rewriter::rewrite(geq1));
 306     TS_ASSERT_EQUALS(Rewriter::rewrite(gt1), Rewriter::rewrite(geq2));
 307
 308     Node lt0 = d_nm->mkNode(LT, x, c0);
 309     Node lt1 = d_nm->mkNode(LT, x, c1);
 310
 311     TS_ASSERT_EQUALS(Rewriter::rewrite(lt0), Rewriter::rewrite(geq0.notNode()));
 312     TS_ASSERT_EQUALS(Rewriter::rewrite(lt1), Rewriter::rewrite(geq1.notNode()));
 313
 314     Node leq0 = d_nm->mkNode(LEQ, x, c0);
 315     Node leq1 = d_nm->mkNode(LEQ, x, c1);
 316
 317     TS_ASSERT_EQUALS(Rewriter::rewrite(leq0), Rewriter::rewrite(geq1.notNode()));
 318     TS_ASSERT_EQUALS(Rewriter::rewrite(leq1), Rewriter::rewrite(geq2.notNode()));
 319   }
 320 };