1 /********************* */
2 /*! \file instantiator_default.cpp
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
14 ** \brief Implementation of instantiator_default class
17 #include "theory/quantifiers/instantiator_default.h"
18 #include "theory/theory_engine.h"
22 using namespace CVC4::kind
;
23 using namespace CVC4::context
;
24 using namespace CVC4::theory
;
26 InstantiatorDefault::InstantiatorDefault(context::Context
* c
, QuantifiersEngine
* ie
, Theory
* th
) :
27 Instantiator( c
, ie
, th
) {
30 void InstantiatorDefault::assertNode( Node assertion
){
33 void InstantiatorDefault::processResetInstantiationRound( Theory::Effort effort
){
36 int InstantiatorDefault::process( Node f
, Theory::Effort effort
, int e
){
39 return InstStrategy::STATUS_UNFINISHED;
41 Debug("quant-default") << "Process " << f << " : " << std::endl;
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;
52 d_quantEngine->addInstantiation( f, m );
55 return InstStrategy::STATUS_UNKNOWN
;