src/theory/quantifiers/theory_quantifiers.cpp

   1 /*********************                                                        */
   2 /*! \file theory_quantifiers.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Andrew Reynolds
   6  ** Minor contributors (to current version): Dejan Jovanovic
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  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) :
  37   Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
  38   d_masterEqualityEngine(0)
  39 {
  40   d_numInstantiations = 0;
  41   d_baseDecLevel = -1;
  42   out.handleUserAttribute( "axiom", this );
  43   out.handleUserAttribute( "conjecture", this );
  44   out.handleUserAttribute( "fun-def", this );
  45   out.handleUserAttribute( "sygus", this );
  46   out.handleUserAttribute( "synthesis", this );
  47   out.handleUserAttribute( "quant-inst-max-level", this );
  48   out.handleUserAttribute( "rr-priority", this );
  49 }
  50
  51 TheoryQuantifiers::~TheoryQuantifiers() {
  52 }
  53
  54 void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  55   d_masterEqualityEngine = eq;
  56 }
  57
  58 void TheoryQuantifiers::addSharedTerm(TNode t) {
  59   Debug("quantifiers-other") << "TheoryQuantifiers::addSharedTerm(): "
  60                      << t << endl;
  61 }
  62
  63
  64 void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) {
  65   Debug("quantifiers-other") << "TheoryQuantifiers::notifyEq(): "
  66                      << lhs << " = " << rhs << endl;
  67
  68 }
  69
  70 void TheoryQuantifiers::preRegisterTerm(TNode n) {
  71   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
  72   if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){
  73     getQuantifiersEngine()->registerQuantifier( n );
  74   }
  75 }
  76
  77
  78 void TheoryQuantifiers::presolve() {
  79   Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << endl;
  80 }
  81
  82 Node TheoryQuantifiers::getValue(TNode n) {
  83   //NodeManager* nodeManager = NodeManager::currentNM();
  84   switch(n.getKind()) {
  85   case FORALL:
  86   case EXISTS:
  87     bool value;
  88     if( d_valuation.hasSatValue( n, value ) ){
  89       return NodeManager::currentNM()->mkConst(value);
  90     }else{
  91       return NodeManager::currentNM()->mkConst(false);  //FIX_THIS?
  92     }
  93     break;
  94   default:
  95     Unhandled(n.getKind());
  96   }
  97 }
  98
  99 void TheoryQuantifiers::computeCareGraph() {
 100   //do nothing
 101 }
 102
 103 void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) {
 104   if(fullModel) {
 105     for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
 106       if((*i).assertion.getKind() == kind::NOT) {
 107         Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
 108         m->assertPredicate((*i).assertion[0], false);
 109       } else {
 110         Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
 111         m->assertPredicate(*i, true);
 112       }
 113     }
 114   }
 115 }
 116
 117 void TheoryQuantifiers::check(Effort e) {
 118   if (done() && !fullEffort(e)) {
 119     return;
 120   }
 121
 122   TimerStat::CodeTimer checkTimer(d_checkTime);
 123
 124   Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
 125   while(!done()) {
 126     Node assertion = get();
 127     Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
 128     switch(assertion.getKind()) {
 129     case kind::FORALL:
 130       assertUniversal( assertion );
 131       break;
 132     case kind::INST_CLOSURE:
 133       getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
 134       if( !options::lteRestrictInstClosure() ){
 135         getQuantifiersEngine()->getMasterEqualityEngine()->addTerm( assertion[0] );
 136       }
 137       break;
 138     case kind::EQUAL:
 139       //do nothing
 140       break;
 141     case kind::NOT:
 142       {
 143         switch( assertion[0].getKind()) {
 144         case kind::FORALL:
 145           assertExistential( assertion );
 146           break;
 147         case kind::EQUAL:
 148           //do nothing
 149           break;
 150         case kind::INST_CLOSURE:
 151         default:
 152           Unhandled(assertion[0].getKind());
 153           break;
 154         }
 155       }
 156       break;
 157     default:
 158       Unhandled(assertion.getKind());
 159       break;
 160     }
 161   }
 162   // call the quantifiers engine to check
 163   getQuantifiersEngine()->check( e );
 164 }
 165
 166 void TheoryQuantifiers::propagate(Effort level){
 167   //getQuantifiersEngine()->propagate( level );
 168 }
 169
 170 Node TheoryQuantifiers::getNextDecisionRequest(){
 171   return getQuantifiersEngine()->getNextDecisionRequest();
 172 }
 173
 174 void TheoryQuantifiers::assertUniversal( Node n ){
 175   Assert( n.getKind()==FORALL );
 176   if( options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){
 177     getQuantifiersEngine()->assertQuantifier( n, true );
 178   }
 179 }
 180
 181 void TheoryQuantifiers::assertExistential( Node n ){
 182   Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
 183   if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){
 184     getQuantifiersEngine()->assertQuantifier( n[0], false );
 185   }
 186 }
 187
 188 bool TheoryQuantifiers::flipDecision(){
 189   //Debug("quantifiers-flip") << "No instantiation given, flip decision, level = " << d_valuation.getDecisionLevel() << std::endl;
 190   //for( int i=1; i<=(int)d_valuation.getDecisionLevel(); i++ ){
 191   //  Debug("quantifiers-flip") << "   " << d_valuation.getDecision( i ) << std::endl;
 192   //}
 193   //if( d_valuation.getDecisionLevel()>0 ){
 194   //  double r = double(rand())/double(RAND_MAX);
 195   //  unsigned decisionLevel = (unsigned)(r*d_valuation.getDecisionLevel());
 196   //  d_out->flipDecision( decisionLevel );
 197   //  return true;
 198   //}else{
 199   //  return false;
 200   //}
 201   return false;
 202 }
 203
 204 void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
 205   QuantifiersAttributes::setUserAttribute( attr, n, node_values, str_value );
 206 }