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 #include "base/check.h"
  20 #include "expr/kind.h"
  21 #include "options/quantifiers_options.h"
  22 #include "theory/quantifiers/ematching/instantiation_engine.h"
  23 #include "theory/quantifiers/fmf/model_engine.h"
  24 #include "theory/quantifiers/quantifiers_attributes.h"
  25 #include "theory/quantifiers/quantifiers_rewriter.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).d_assertion.getKind() == kind::NOT)
 100     {
 101       Debug("quantifiers::collectModelInfo")
 102           << "got quant FALSE: " << (*i).d_assertion[0] << endl;
 103       if (!m->assertPredicate((*i).d_assertion[0], false))
 104       {
 105         return false;
 106       }
 107     }
 108     else
 109     {
 110       Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
 111       if (!m->assertPredicate(*i, true))
 112       {
 113         return false;
 114       }
 115     }
 116   }
 117   return true;
 118 }
 119
 120 void TheoryQuantifiers::check(Effort e) {
 121   if (done() && !fullEffort(e)) {
 122     return;
 123   }
 124
 125   TimerStat::CodeTimer checkTimer(d_checkTime);
 126
 127   Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
 128   while(!done()) {
 129     Node assertion = get();
 130     Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
 131     switch(assertion.getKind()) {
 132     case kind::FORALL:
 133       getQuantifiersEngine()->assertQuantifier(assertion, true);
 134       break;
 135     case kind::INST_CLOSURE:
 136       getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
 137       if( !options::lteRestrictInstClosure() ){
 138         getQuantifiersEngine()->getMasterEqualityEngine()->addTerm( assertion[0] );
 139       }
 140       break;
 141     case kind::EQUAL:
 142       //do nothing
 143       break;
 144     case kind::NOT:
 145       {
 146         switch( assertion[0].getKind()) {
 147         case kind::FORALL:
 148           getQuantifiersEngine()->assertQuantifier(assertion[0], false);
 149           break;
 150         case kind::EQUAL:
 151           //do nothing
 152           break;
 153         case kind::INST_CLOSURE:
 154         default: Unhandled() << assertion[0].getKind(); break;
 155         }
 156       }
 157       break;
 158       default: Unhandled() << assertion.getKind(); 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 }