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