src/theory/arrays/theory_arrays.cpp

   1 /*********************                                                        */
   2 /*! \file theory_arrays.cpp
   3  ** \verbatim
   4  ** Original author: barrett
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   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 Implementation of the theory of arrays.
  15  **
  16  ** Implementation of the theory of arrays.
  17  **/
  18
  19
  20 #include "theory/arrays/theory_arrays.h"
  21 #include "expr/kind.h"
  22
  23
  24 using namespace std;
  25 using namespace CVC4;
  26 using namespace CVC4::kind;
  27 using namespace CVC4::context;
  28 using namespace CVC4::theory;
  29 using namespace CVC4::theory::arrays;
  30
  31
  32 TheoryArrays::TheoryArrays(int id, Context* c, OutputChannel& out) :
  33   Theory(id, c, out)
  34 {
  35 }
  36
  37
  38 TheoryArrays::~TheoryArrays() {
  39 }
  40
  41
  42 void TheoryArrays::addSharedTerm(TNode t) {
  43   Debug("arrays") << "TheoryArrays::addSharedTerm(): "
  44                   << t << endl;
  45 }
  46
  47
  48 void TheoryArrays::notifyEq(TNode lhs, TNode rhs) {
  49   Debug("arrays") << "TheoryArrays::notifyEq(): "
  50                   << lhs << " = " << rhs << endl;
  51 }
  52
  53
  54 void TheoryArrays::check(Effort e) {
  55   while(!done()) {
  56     Node assertion = get();
  57     Debug("arrays") << "TheoryArrays::check(): " << assertion << endl;
  58   }
  59   Debug("arrays") << "TheoryArrays::check(): done" << endl;
  60 }