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-2020 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 "expr/proof_node_manager.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/quantifiers_rewriter.h"
  27 #include "theory/quantifiers/term_database.h"
  28 #include "theory/quantifiers/term_util.h"
  29 #include "theory/quantifiers_engine.h"
  30 #include "theory/valuation.h"
  31
  32 using namespace std;
  33 using namespace CVC4;
  34 using namespace CVC4::kind;
  35 using namespace CVC4::context;
  36 using namespace CVC4::theory;
  37 using namespace CVC4::theory::quantifiers;
  38
  39 TheoryQuantifiers::TheoryQuantifiers(Context* c,
  40                                      context::UserContext* u,
  41                                      OutputChannel& out,
  42                                      Valuation valuation,
  43                                      const LogicInfo& logicInfo,
  44                                      ProofNodeManager* pnm)
  45     : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm)
  46 {
  47   out.handleUserAttribute( "fun-def", this );
  48   out.handleUserAttribute( "sygus", this );
  49   out.handleUserAttribute("quant-name", this);
  50   out.handleUserAttribute("sygus-synth-grammar", this);
  51   out.handleUserAttribute( "sygus-synth-fun-var-list", this );
  52   out.handleUserAttribute( "quant-inst-max-level", this );
  53   out.handleUserAttribute( "quant-elim", this );
  54   out.handleUserAttribute( "quant-elim-partial", this );
  55
  56   ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
  57   if (pc != nullptr)
  58   {
  59     // add the proof rules
  60     d_qChecker.registerTo(pc);
  61   }
  62 }
  63
  64 TheoryQuantifiers::~TheoryQuantifiers() {
  65 }
  66
  67 void TheoryQuantifiers::finishInit()
  68 {
  69   // quantifiers are not evaluated in getModelValue
  70   TheoryModel* tm = d_valuation.getModel();
  71   Assert(tm != nullptr);
  72   tm->setUnevaluatedKind(EXISTS);
  73   tm->setUnevaluatedKind(FORALL);
  74   // witness is used in several instantiation strategies
  75   tm->setUnevaluatedKind(WITNESS);
  76 }
  77
  78 void TheoryQuantifiers::preRegisterTerm(TNode n) {
  79   if (n.getKind() != FORALL)
  80   {
  81     return;
  82   }
  83   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
  84   // Preregister the quantified formula.
  85   // This initializes the modules used for handling n in this user context.
  86   getQuantifiersEngine()->preRegisterQuantifier(n);
  87   Debug("quantifiers-prereg")
  88       << "TheoryQuantifiers::preRegisterTerm() done " << n << endl;
  89 }
  90
  91
  92 void TheoryQuantifiers::presolve() {
  93   Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << endl;
  94   if( getQuantifiersEngine() ){
  95     getQuantifiersEngine()->presolve();
  96   }
  97 }
  98
  99 void TheoryQuantifiers::ppNotifyAssertions(
 100     const std::vector<Node>& assertions) {
 101   Trace("quantifiers-presolve")
 102       << "TheoryQuantifiers::ppNotifyAssertions" << std::endl;
 103   if (getQuantifiersEngine()) {
 104     getQuantifiersEngine()->ppNotifyAssertions(assertions);
 105   }
 106 }
 107
 108 bool TheoryQuantifiers::collectModelInfo(TheoryModel* m)
 109 {
 110   for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) {
 111     if ((*i).d_assertion.getKind() == kind::NOT)
 112     {
 113       Debug("quantifiers::collectModelInfo")
 114           << "got quant FALSE: " << (*i).d_assertion[0] << endl;
 115       if (!m->assertPredicate((*i).d_assertion[0], false))
 116       {
 117         return false;
 118       }
 119     }
 120     else
 121     {
 122       Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl;
 123       if (!m->assertPredicate(*i, true))
 124       {
 125         return false;
 126       }
 127     }
 128   }
 129   return true;
 130 }
 131
 132 void TheoryQuantifiers::check(Effort e) {
 133   if (done() && !fullEffort(e)) {
 134     return;
 135   }
 136
 137   TimerStat::CodeTimer checkTimer(d_checkTime);
 138
 139   Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl;
 140   while(!done()) {
 141     Node assertion = get();
 142     Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl;
 143     switch(assertion.getKind()) {
 144     case kind::FORALL:
 145       getQuantifiersEngine()->assertQuantifier(assertion, true);
 146       break;
 147     case kind::INST_CLOSURE:
 148       getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true );
 149       if( !options::lteRestrictInstClosure() ){
 150         getQuantifiersEngine()->getMasterEqualityEngine()->addTerm( assertion[0] );
 151       }
 152       break;
 153     case kind::EQUAL:
 154       //do nothing
 155       break;
 156     case kind::NOT:
 157       {
 158         switch( assertion[0].getKind()) {
 159         case kind::FORALL:
 160           getQuantifiersEngine()->assertQuantifier(assertion[0], false);
 161           break;
 162         case kind::EQUAL:
 163           //do nothing
 164           break;
 165         case kind::INST_CLOSURE:
 166         default: Unhandled() << assertion[0].getKind(); break;
 167         }
 168       }
 169       break;
 170       default: Unhandled() << assertion.getKind(); break;
 171     }
 172   }
 173   // call the quantifiers engine to check
 174   getQuantifiersEngine()->check( e );
 175 }
 176
 177 void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){
 178   QuantAttributes::setUserAttribute( attr, n, node_values, str_value );
 179 }