src/theory/quantifiers/instantiator_default.cpp

   1 /*********************                                                        */
   2 /*! \file instantiator_default.cpp
   3  ** \verbatim
   4  ** Original author: ajreynol
   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, 2011  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 instantiator_default class
  15  **/
  16
  17 #include "theory/quantifiers/instantiator_default.h"
  18 #include "theory/theory_engine.h"
  19
  20 using namespace std;
  21 using namespace CVC4;
  22 using namespace CVC4::kind;
  23 using namespace CVC4::context;
  24 using namespace CVC4::theory;
  25
  26 InstantiatorDefault::InstantiatorDefault(context::Context* c, QuantifiersEngine* ie, Theory* th) :
  27   Instantiator( c, ie, th ) {
  28 }
  29
  30 void InstantiatorDefault::assertNode( Node assertion ){
  31 }
  32
  33 void InstantiatorDefault::processResetInstantiationRound( Theory::Effort effort ){
  34 }
  35
  36 int InstantiatorDefault::process( Node f, Theory::Effort effort, int e ){
  37   /*
  38   if( e < 4 ){
  39     return InstStrategy::STATUS_UNFINISHED;
  40   }else if( e == 4 ){
  41     Debug("quant-default") << "Process " << f << " : " << std::endl;
  42     InstMatch m;
  43     for( int j=0; j<(int)d_quantEngine->getNumInstantiationConstants( f ); j++ ){
  44       Node i = d_quantEngine->getInstantiationConstant( f, j );
  45       Debug("quant-default") << "Getting value for " << i << std::endl;
  46       if( d_quantEngine->getTheoryEngine()->theoryOf( i )==getTheory() ){    //if it belongs to this theory
  47         Node val = d_th->getValue( i );
  48         Debug("quant-default") << "Default Instantiate for " << d_th->getId() << ", setting " << i << " = " << val << std::endl;
  49         m.set( i, val);
  50       }
  51     }
  52     d_quantEngine->addInstantiation( f, m );
  53   }
  54   */
  55   return InstStrategy::STATUS_UNKNOWN;
  56 }