/********************* */
/*! \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
**
#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<Node>& 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<Node>& 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> 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
projects / cvc5.git / blobdiff