src/theory/quantifiers/theory_quantifiers.cpp

   1 /*********************                                                        */
   2 /*! \file theory_quantifiers.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andrew Reynolds, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Implementation of the theory of quantifiers
  13  **
  14  ** Implementation of the theory of quantifiers.
  15  **/
  16
  17 #include "theory/quantifiers/theory_quantifiers.h"
  18
  19
  20 #include "base/cvc4_assert.h"
  21 #include "expr/kind.h"
  22 #include "options/quantifiers_options.h"
  23 #include "theory/quantifiers/ematching/instantiation_engine.h"
  24 #include "theory/quantifiers/fmf/model_engine.h"
  25 #include "theory/quantifiers/quantifiers_attributes.h"
  26 #include "theory/quantifiers/term_database.h"
  27 #include "theory/quantifiers/term_util.h"
  28 #include "theory/quantifiers_engine.h"
  29 #include "theory/valuation.h"
  30
  31 using namespace std;
  32 using namespace CVC4;
  33 using namespace CVC4::kind;
  34 using namespace CVC4::context;
  35 using namespace CVC4::theory;
  36 using namespace CVC4::theory::quantifiers;
  37
  38 TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
  39     Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo)
  40 {
  41   d_numInstantiations = 0;
  42   d_baseDecLevel = -1;
  43   out.handleUserAttribute( "axiom", this );
  44   out.handleUserAttribute( "conjecture", this );
  45   out.handleUserAttribute( "fun-def", this );
  46   out.handleUserAttribute( "sygus", this );
  47   out.handleUserAttribute("quant-name", this);
  48   out.handleUserAttribute("sygus-synth-grammar", this);
  49   out.handleUserAttribute( "sygus-synth-fun-var-list", this );
  50   out.handleUserAttribute( "synthesis", this );
  51   out.handleUserAttribute( "quant-inst-max-level", this );
  52   out.handleUserAttribute( "rr-priority", this );
  53   out.handleUserAttribute( "quant-elim", this );
  54   out.handleUserAttribute( "quant-elim-partial", this );
  55 }
  56
  57 TheoryQuantifiers::~TheoryQuantifiers() {
  58 }
  59
  60 void TheoryQuantifiers::finishInit()
  61 {
  62   // quantifiers are not evaluated in getModelValue
  63   TheoryModel* tm = d_valuation.getModel();
  64   Assert(tm != nullptr);
  65   tm->setUnevaluatedKind(EXISTS);
  66   tm->setUnevaluatedKind(FORALL);
  67 }
  68
  69 void TheoryQuantifiers::preRegisterTerm(TNode n) {
  70   if (n.getKind() != FORALL)
  71   {
  72     return;
  73   }
  74   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
  75   if (options::cbqi() && !options::recurseCbqi()
  76       && TermUtil::hasInstConstAttr(n))
  77   {
  78     Debug("quantifiers-prereg")
  79         << "TheoryQuantifiers::preRegisterTerm() done, unused " << n << endl;
  80     return;
  81   }
  82   // Preregister the quantified formula.
  83   // This initializes the modules used for handling n in this user context.
  84   getQuantifiersEngine()->preRegisterQuantifier(n);
  85   Debug("quantifiers-prereg")
  86       << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
  87 }
  88
  89
  90 void TheoryQuantifiers::presolve() {
  91   Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << endl;
  92   if( getQuantifiersEngine() ){
  93     getQuantifiersEngine()->presolve();
  94   }
  95 }
  96
  97 void TheoryQuantifiers::ppNotifyAssertions(
  98     const std::vector<Node>& assertions) {
  99   Trace("quantifiers-presolve")
 100       << "TheoryQuantifiers::ppNotifyAssertions" << std::endl;
 101   if (getQuantifiersEngine()) {
 102     getQuantifiersEngine()->ppNotifyAssertions(assertions);
 103   }
 104 }
 105
 106 bool TheoryQuantifiers::collectModelInfo(TheoryModel* m)
 107 {
 108   for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
 109     if((*i).assertion.getKind() == kind::NOT) {
 110       Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
 111       if (!m->assertPredicate((*i).assertion[0], false))
 112       {
 113         return false;
 114       }
 115     } else {
 116       Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
 117       if (!m->assertPredicate(*i, true))
 118       {
 119         return false;
 120       }
 121     }
 122   }
 123   return true;
 124 }
 125
 126 void TheoryQuantifiers::check(Effort e) {
 127   if (done() && !fullEffort(e)) {
 128     return;
 129   }
 130
 131   TimerStat::CodeTimer checkTimer(d_checkTime);
 132
 133   Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
 134   while(!done()) {
 135     Node assertion = get();
 136     Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
 137     switch(assertion.getKind()) {
 138     case kind::FORALL:
 139       assertUniversal( assertion );
 140       break;
 141     case kind::INST_CLOSURE:
 142       getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
 143       if( !options::lteRestrictInstClosure() ){
 144         getQuantifiersEngine()->getMasterEqualityEngine()->addTerm( assertion[0] );
 145       }
 146       break;
 147     case kind::EQUAL:
 148       //do nothing
 149       break;
 150     case kind::NOT:
 151       {
 152         switch( assertion[0].getKind()) {
 153         case kind::FORALL:
 154           assertExistential( assertion );
 155           break;
 156         case kind::EQUAL:
 157           //do nothing
 158           break;
 159         case kind::INST_CLOSURE:
 160         default:
 161           Unhandled(assertion[0].getKind());
 162           break;
 163         }
 164       }
 165       break;
 166     default:
 167       Unhandled(assertion.getKind());
 168       break;
 169     }
 170   }
 171   // call the quantifiers engine to check
 172   getQuantifiersEngine()->check( e );
 173 }
 174
 175 Node TheoryQuantifiers::getNextDecisionRequest( unsigned& priority ){
 176   return getQuantifiersEngine()->getNextDecisionRequest( priority );
 177 }
 178
 179 void TheoryQuantifiers::assertUniversal( Node n ){
 180   Assert( n.getKind()==FORALL );
 181   if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){
 182     getQuantifiersEngine()->assertQuantifier( n, true );
 183   }
 184 }
 185
 186 void TheoryQuantifiers::assertExistential( Node n ){
 187   Assert( n.getKind()== NOT && n[0].getKind()==FORALL );
 188   if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n[0]) ){
 189     getQuantifiersEngine()->assertQuantifier( n[0], false );
 190   }
 191 }
 192
 193 void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
 194   QuantAttributes::setUserAttribute( attr, n, node_values, str_value );
 195 }