src/theory/quantifiers/theory_quantifiers.cpp

   1 /*********************                                                        */
   2 /*! \file theory_quantifiers.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 the theory of quantifiers
  15  **
  16  ** Implementation of the theory of quantifiers.
  17  **/
  18
  19
  20 #include "theory/quantifiers/theory_quantifiers.h"
  21 #include "theory/valuation.h"
  22 #include "theory/quantifiers_engine.h"
  23 #include "theory/quantifiers/instantiation_engine.h"
  24 #include "theory/quantifiers/model_engine.h"
  25 #include "expr/kind.h"
  26 #include "util/Assert.h"
  27 #include "theory/quantifiers/theory_quantifiers_instantiator.h"
  28 #include "theory/quantifiers/options.h"
  29 #include "theory/quantifiers/term_database.h"
  30 #include "theory/quantifiers/quantifiers_attributes.h"
  31
  32 using namespace std;
  33 using namespace CVC4;
  34 using namespace CVC4::kind;
  35 using namespace CVC4::context;
  36 using namespace CVC4::theory;
  37 using namespace CVC4::theory::quantifiers;
  38
  39 TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
  40   Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, qe),
  41   d_numRestarts(0){
  42   d_numInstantiations = 0;
  43   d_baseDecLevel = -1;
  44   out.handleUserAttribute( "axiom", this );
  45   out.handleUserAttribute( "conjecture", this );
  46 }
  47
  48
  49 TheoryQuantifiers::~TheoryQuantifiers() {
  50 }
  51
  52 void TheoryQuantifiers::addSharedTerm(TNode t) {
  53   Debug("quantifiers-other") << "TheoryQuantifiers::addSharedTerm(): "
  54                      << t << endl;
  55 }
  56
  57
  58 void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) {
  59   Debug("quantifiers-other") << "TheoryQuantifiers::notifyEq(): "
  60                      << lhs << " = " << rhs << endl;
  61
  62 }
  63
  64 void TheoryQuantifiers::preRegisterTerm(TNode n) {
  65   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
  66   if( n.getKind()==FORALL && !n.hasAttribute(InstConstantAttribute()) ){
  67     getQuantifiersEngine()->registerQuantifier( n );
  68   }
  69 }
  70
  71
  72 void TheoryQuantifiers::presolve() {
  73   Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << endl;
  74 }
  75
  76 Node TheoryQuantifiers::getValue(TNode n) {
  77   //NodeManager* nodeManager = NodeManager::currentNM();
  78   switch(n.getKind()) {
  79   case FORALL:
  80   case EXISTS:
  81     bool value;
  82     if( d_valuation.hasSatValue( n, value ) ){
  83       return NodeManager::currentNM()->mkConst(value);
  84     }else{
  85       return NodeManager::currentNM()->mkConst(false);  //FIX_THIS?
  86     }
  87     break;
  88   default:
  89     Unhandled(n.getKind());
  90   }
  91 }
  92
  93 void TheoryQuantifiers::collectModelInfo( TheoryModel* m, bool fullModel ){
  94
  95 }
  96
  97 void TheoryQuantifiers::check(Effort e) {
  98   CodeTimer codeTimer(d_theoryTime);
  99
 100   Debug("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
 101   while(!done()) {
 102     Node assertion = get();
 103     Debug("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
 104     switch(assertion.getKind()) {
 105     case kind::FORALL:
 106       assertUniversal( assertion );
 107       break;
 108     case kind::NOT:
 109       {
 110         switch( assertion[0].getKind()) {
 111         case kind::FORALL:
 112           assertExistential( assertion );
 113           break;
 114         default:
 115           Unhandled(assertion[0].getKind());
 116           break;
 117         }
 118       }
 119       break;
 120     default:
 121       Unhandled(assertion.getKind());
 122       break;
 123     }
 124   }
 125   // call the quantifiers engine to check
 126   getQuantifiersEngine()->check( e );
 127 }
 128
 129 void TheoryQuantifiers::propagate(Effort level){
 130   //CodeTimer codeTimer(d_theoryTime);
 131   //getQuantifiersEngine()->propagate( level );
 132 }
 133
 134 Node TheoryQuantifiers::getNextDecisionRequest(){
 135   return getQuantifiersEngine()->getNextDecisionRequest();
 136 }
 137
 138 void TheoryQuantifiers::assertUniversal( Node n ){
 139   Assert( n.getKind()==FORALL );
 140   if( !n.hasAttribute(InstConstantAttribute()) ){
 141     getQuantifiersEngine()->registerQuantifier( n );
 142     getQuantifiersEngine()->assertNode( n );
 143   }
 144 }
 145
 146 void TheoryQuantifiers::assertExistential( Node n ){
 147   Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
 148   if( !n[0].hasAttribute(InstConstantAttribute()) ){
 149     if( d_skolemized.find( n )==d_skolemized.end() ){
 150       Node body = getQuantifiersEngine()->getTermDatabase()->getSkolemizedBody( n[0] );
 151       NodeBuilder<> nb(kind::OR);
 152       nb << n[0] << body.notNode();
 153       Node lem = nb;
 154       Debug("quantifiers-sk") << "Skolemize lemma : " << lem << std::endl;
 155       d_out->lemma( lem );
 156       d_skolemized[n] = true;
 157     }
 158   }
 159 }
 160
 161 bool TheoryQuantifiers::flipDecision(){
 162   //Debug("quantifiers-flip") << "No instantiation given, flip decision, level = " << d_valuation.getDecisionLevel() << std::endl;
 163   //for( int i=1; i<=(int)d_valuation.getDecisionLevel(); i++ ){
 164   //  Debug("quantifiers-flip") << "   " << d_valuation.getDecision( i ) << std::endl;
 165   //}
 166   //if( d_valuation.getDecisionLevel()>0 ){
 167   //  double r = double(rand())/double(RAND_MAX);
 168   //  unsigned decisionLevel = (unsigned)(r*d_valuation.getDecisionLevel());
 169   //  d_out->flipDecision( decisionLevel );
 170   //  return true;
 171   //}else{
 172   //  return false;
 173   //}
 174
 175   if( !d_out->flipDecision() ){
 176     return restart();
 177   }
 178   return true;
 179 }
 180
 181 bool TheoryQuantifiers::restart(){
 182   static const int restartLimit = 0;
 183   if( d_numRestarts==restartLimit ){
 184     Debug("quantifiers-flip") << "No more restarts." << std::endl;
 185     return false;
 186   }else{
 187     d_numRestarts++;
 188     Debug("quantifiers-flip") << "Do restart." << std::endl;
 189     return true;
 190   }
 191 }
 192
 193 void TheoryQuantifiers::setUserAttribute( std::string& attr, Node n ){
 194   QuantifiersAttributes::setUserAttribute( attr, n );
 195 }