X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Ftheory%2Fquantifiers%2Ftheory_quantifiers.cpp;h=c3c3fe7b65300a627bf7d84498fcd2bea4c2dc67;hb=05a53a2ac405bcd18a84024247145f161809c3b0;hp=86fc057ea33ea3b3503642fb8fc9fc1319023b3c;hpb=2ba8bb701ce289ba60afec01b653b0930cc59298;p=cvc5.git diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 86fc057ea..c3c3fe7b6 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file theory_quantifiers.cpp ** \verbatim - ** Original author: Morgan Deters - ** Major contributors: Andrew Reynolds - ** Minor contributors (to current version): Dejan Jovanovic + ** Top contributors (to current version): + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + ** in the top-level source directory and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief Implementation of the theory of quantifiers ** @@ -16,175 +16,172 @@ #include "theory/quantifiers/theory_quantifiers.h" - -#include "base/cvc4_assert.h" -#include "expr/kind.h" +#include "expr/proof_node_manager.h" #include "options/quantifiers_options.h" -#include "theory/quantifiers/instantiation_engine.h" -#include "theory/quantifiers/model_engine.h" -#include "theory/quantifiers/quantifiers_attributes.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/quantifiers_modules.h" +#include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/valuation.h" -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - -TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : - Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo), - d_masterEqualityEngine(0) +using namespace cvc5::kind; +using namespace cvc5::context; + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +TheoryQuantifiers::TheoryQuantifiers(Context* c, + context::UserContext* u, + OutputChannel& out, + Valuation valuation, + const LogicInfo& logicInfo, + ProofNodeManager* pnm) + : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, pnm), + d_qstate(c, u, valuation, logicInfo), + d_qreg(), + d_treg(d_qstate, d_qreg), + d_qim(*this, d_qstate, d_qreg, d_treg, pnm), + d_qengine(nullptr) { - d_numInstantiations = 0; - d_baseDecLevel = -1; - out.handleUserAttribute( "axiom", this ); - out.handleUserAttribute( "conjecture", this ); out.handleUserAttribute( "fun-def", this ); - out.handleUserAttribute( "sygus", this ); - out.handleUserAttribute( "synthesis", this ); + out.handleUserAttribute("qid", this); out.handleUserAttribute( "quant-inst-max-level", this ); - out.handleUserAttribute( "rr-priority", this ); -} + out.handleUserAttribute( "quant-elim", this ); + out.handleUserAttribute( "quant-elim-partial", this ); + + ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr; + if (pc != nullptr) + { + // add the proof rules + d_qChecker.registerTo(pc); + } -TheoryQuantifiers::~TheoryQuantifiers() { + // Finish initializing the term registry by hooking it up to the inference + // manager. This is required due to a cyclic dependency between the term + // database and the instantiate module. Term database needs inference manager + // since it sends out lemmas when term indexing is inconsistent, instantiate + // needs term database for entailment checks. + d_treg.finishInit(&d_qim); + + // construct the quantifiers engine + d_qengine.reset(new QuantifiersEngine(d_qstate, d_qreg, d_treg, d_qim, pnm)); + + //!!!!!!!!!!!!!! temporary (project #15) + d_treg.getModel()->finishInit(d_qengine.get()); + + // indicate we are using the quantifiers theory state object + d_theoryState = &d_qstate; + // use the inference manager as the official inference manager + d_inferManager = &d_qim; + // Set the pointer to the quantifiers engine, which this theory owns. This + // pointer will be retreived by TheoryEngine and set to all theories + // post-construction. + d_quantEngine = d_qengine.get(); } -void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) { - d_masterEqualityEngine = eq; +TheoryQuantifiers::~TheoryQuantifiers() { } -void TheoryQuantifiers::addSharedTerm(TNode t) { - Debug("quantifiers-other") << "TheoryQuantifiers::addSharedTerm(): " - << t << endl; +TheoryRewriter* TheoryQuantifiers::getTheoryRewriter() { return &d_rewriter; } +void TheoryQuantifiers::finishInit() +{ + // quantifiers are not evaluated in getModelValue + d_valuation.setUnevaluatedKind(EXISTS); + d_valuation.setUnevaluatedKind(FORALL); + // witness is used in several instantiation strategies + d_valuation.setUnevaluatedKind(WITNESS); } - -void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) { - Debug("quantifiers-other") << "TheoryQuantifiers::notifyEq(): " - << lhs << " = " << rhs << endl; - +bool TheoryQuantifiers::needsEqualityEngine(EeSetupInfo& esi) +{ + // use the master equality engine + esi.d_useMaster = true; + return true; } -void TheoryQuantifiers::preRegisterTerm(TNode n) { - Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl; - if( n.getKind()==FORALL && !TermDb::hasInstConstAttr(n) ){ - getQuantifiersEngine()->registerQuantifier( n ); +void TheoryQuantifiers::preRegisterTerm(TNode n) +{ + if (n.getKind() != FORALL) + { + return; } + Debug("quantifiers-prereg") + << "TheoryQuantifiers::preRegisterTerm() " << n << std::endl; + // Preregister the quantified formula. + // This initializes the modules used for handling n in this user context. + getQuantifiersEngine()->preRegisterQuantifier(n); + Debug("quantifiers-prereg") + << "TheoryQuantifiers::preRegisterTerm() done " << n << std::endl; } void TheoryQuantifiers::presolve() { - Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << endl; + Debug("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << std::endl; if( getQuantifiersEngine() ){ getQuantifiersEngine()->presolve(); } } -Node TheoryQuantifiers::getValue(TNode n) { - //NodeManager* nodeManager = NodeManager::currentNM(); - switch(n.getKind()) { - case FORALL: - case EXISTS: - bool value; - if( d_valuation.hasSatValue( n, value ) ){ - return NodeManager::currentNM()->mkConst(value); - }else{ - return NodeManager::currentNM()->mkConst(false); //FIX_THIS? - } - break; - default: - Unhandled(n.getKind()); +void TheoryQuantifiers::ppNotifyAssertions( + const std::vector& assertions) { + Trace("quantifiers-presolve") + << "TheoryQuantifiers::ppNotifyAssertions" << std::endl; + if (getQuantifiersEngine()) { + getQuantifiersEngine()->ppNotifyAssertions(assertions); } } -void TheoryQuantifiers::computeCareGraph() { - //do nothing -} - -void TheoryQuantifiers::collectModelInfo(TheoryModel* m, bool fullModel) { - if(fullModel) { - for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { - if((*i).assertion.getKind() == kind::NOT) { - Debug("quantifiers::collectModelInfo") << "got quant FALSE: " << (*i).assertion[0] << endl; - m->assertPredicate((*i).assertion[0], false); - } else { - Debug("quantifiers::collectModelInfo") << "got quant TRUE : " << *i << endl; - m->assertPredicate(*i, true); +bool TheoryQuantifiers::collectModelValues(TheoryModel* m, + const std::set& termSet) +{ + for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { + if ((*i).d_assertion.getKind() == NOT) + { + Debug("quantifiers::collectModelInfo") + << "got quant FALSE: " << (*i).d_assertion[0] << std::endl; + if (!m->assertPredicate((*i).d_assertion[0], false)) + { + return false; } } - } -} - -void TheoryQuantifiers::check(Effort e) { - if (done() && !fullEffort(e)) { - return; - } - - TimerStat::CodeTimer checkTimer(d_checkTime); - - Trace("quantifiers-check") << "quantifiers::check(" << e << ")" << std::endl; - while(!done()) { - Node assertion = get(); - Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl; - switch(assertion.getKind()) { - case kind::FORALL: - assertUniversal( assertion ); - break; - case kind::INST_CLOSURE: - getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true ); - if( !options::lteRestrictInstClosure() ){ - getQuantifiersEngine()->getMasterEqualityEngine()->addTerm( assertion[0] ); - } - break; - case kind::EQUAL: - //do nothing - break; - case kind::NOT: + else + { + Debug("quantifiers::collectModelInfo") + << "got quant TRUE : " << *i << std::endl; + if (!m->assertPredicate(*i, true)) { - switch( assertion[0].getKind()) { - case kind::FORALL: - assertExistential( assertion ); - break; - case kind::EQUAL: - //do nothing - break; - case kind::INST_CLOSURE: - default: - Unhandled(assertion[0].getKind()); - break; - } + return false; } - break; - default: - Unhandled(assertion.getKind()); - break; } } - // call the quantifiers engine to check - getQuantifiersEngine()->check( e ); + return true; } -Node TheoryQuantifiers::getNextDecisionRequest(){ - return getQuantifiersEngine()->getNextDecisionRequest(); +void TheoryQuantifiers::postCheck(Effort level) +{ + // call the quantifiers engine to check + getQuantifiersEngine()->check(level); } -void TheoryQuantifiers::assertUniversal( Node n ){ - Assert( n.getKind()==FORALL ); - if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n) ){ - getQuantifiersEngine()->assertQuantifier( n, true ); +bool TheoryQuantifiers::preNotifyFact( + TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal) +{ + Kind k = atom.getKind(); + if (k == FORALL) + { + getQuantifiersEngine()->assertQuantifier(atom, polarity); } -} - -void TheoryQuantifiers::assertExistential( Node n ){ - Assert( n.getKind()== NOT && n[0].getKind()==FORALL ); - if( !options::cbqi() || options::recurseCbqi() || !TermDb::hasInstConstAttr(n[0]) ){ - getQuantifiersEngine()->assertQuantifier( n[0], false ); + else + { + Unhandled() << "Unexpected fact " << fact; } + // don't use equality engine, always return true + return true; } void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector node_values, std::string str_value){ - QuantifiersAttributes::setUserAttribute( attr, n, node_values, str_value ); + QuantAttributes::setUserAttribute( attr, n, node_values, str_value ); } + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5