src/theory/quantifiers/theory_quantifiers.cpp

   1 /*********************                                                        */
   2 /*! \file theory_quantifiers.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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   out.handleUserAttribute( "axiom", this );
  42   out.handleUserAttribute( "conjecture", this );
  43   out.handleUserAttribute( "fun-def", this );
  44   out.handleUserAttribute( "sygus", this );
  45   out.handleUserAttribute("quant-name", this);
  46   out.handleUserAttribute("sygus-synth-grammar", this);
  47   out.handleUserAttribute( "sygus-synth-fun-var-list", this );
  48   out.handleUserAttribute( "quant-inst-max-level", this );
  49   out.handleUserAttribute( "rr-priority", this );
  50   out.handleUserAttribute( "quant-elim", this );
  51   out.handleUserAttribute( "quant-elim-partial", this );
  52 }
  53
  54 TheoryQuantifiers::~TheoryQuantifiers() {
  55 }
  56
  57 void TheoryQuantifiers::finishInit()
  58 {
  59   // quantifiers are not evaluated in getModelValue
  60   TheoryModel* tm = d_valuation.getModel();
  61   Assert(tm != nullptr);
  62   tm->setUnevaluatedKind(EXISTS);
  63   tm->setUnevaluatedKind(FORALL);
  64 }
  65
  66 void TheoryQuantifiers::preRegisterTerm(TNode n) {
  67   if (n.getKind() != FORALL)
  68   {
  69     return;
  70   }
  71   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
  72   // Preregister the quantified formula.
  73   // This initializes the modules used for handling n in this user context.
  74   getQuantifiersEngine()->preRegisterQuantifier(n);
  75   Debug("quantifiers-prereg")
  76       << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
  77 }
  78
  79
  80 void TheoryQuantifiers::presolve() {
  81   Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << endl;
  82   if( getQuantifiersEngine() ){
  83     getQuantifiersEngine()->presolve();
  84   }
  85 }
  86
  87 void TheoryQuantifiers::ppNotifyAssertions(
  88     const std::vector<Node>& assertions) {
  89   Trace("quantifiers-presolve")
  90       << "TheoryQuantifiers::ppNotifyAssertions" << std::endl;
  91   if (getQuantifiersEngine()) {
  92     getQuantifiersEngine()->ppNotifyAssertions(assertions);
  93   }
  94 }
  95
  96 bool TheoryQuantifiers::collectModelInfo(TheoryModel* m)
  97 {
  98   for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
  99     if((*i).assertion.getKind() == kind::NOT) {
 100       Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl;
 101       if (!m->assertPredicate((*i).assertion[0], false))
 102       {
 103         return false;
 104       }
 105     } else {
 106       Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
 107       if (!m->assertPredicate(*i, true))
 108       {
 109         return false;
 110       }
 111     }
 112   }
 113   return true;
 114 }
 115
 116 void TheoryQuantifiers::check(Effort e) {
 117   if (done() && !fullEffort(e)) {
 118     return;
 119   }
 120
 121   TimerStat::CodeTimer checkTimer(d_checkTime);
 122
 123   Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
 124   while(!done()) {
 125     Node assertion = get();
 126     Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
 127     switch(assertion.getKind()) {
 128     case kind::FORALL:
 129       getQuantifiersEngine()->assertQuantifier(assertion, true);
 130       break;
 131     case kind::INST_CLOSURE:
 132       getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
 133       if( !options::lteRestrictInstClosure() ){
 134         getQuantifiersEngine()->getMasterEqualityEngine()->addTerm( assertion[0] );
 135       }
 136       break;
 137     case kind::EQUAL:
 138       //do nothing
 139       break;
 140     case kind::NOT:
 141       {
 142         switch( assertion[0].getKind()) {
 143         case kind::FORALL:
 144           getQuantifiersEngine()->assertQuantifier(assertion[0], false);
 145           break;
 146         case kind::EQUAL:
 147           //do nothing
 148           break;
 149         case kind::INST_CLOSURE:
 150         default:
 151           Unhandled(assertion[0].getKind());
 152           break;
 153         }
 154       }
 155       break;
 156     default:
 157       Unhandled(assertion.getKind());
 158       break;
 159     }
 160   }
 161   // call the quantifiers engine to check
 162   getQuantifiersEngine()->check( e );
 163 }
 164
 165 void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
 166   QuantAttributes::setUserAttribute( attr, n, node_values, str_value );
 167 }