Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.
Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.
theory/quantifiers/quant_split.h
theory/quantifiers/quant_util.cpp
theory/quantifiers/quant_util.h
+ theory/quantifiers/quant_module.cpp
+ theory/quantifiers/quant_module.h
theory/quantifiers/quantifiers_attributes.cpp
theory/quantifiers/quantifiers_attributes.h
theory/quantifiers/quantifiers_inference_manager.cpp
#include "smt/smt_engine_scope.h"
#include "theory/arith/arith_msum.h"
#include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/quantifiers_registry.h"
#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
{
Node icn = d_preprocContext->getTheoryEngine()
->getQuantifiersEngine()
- ->getTermUtil()
- ->substituteBoundVariablesToInstConstants(n, q);
+ ->getQuantifiersRegistry()
+ .substituteBoundVariablesToInstConstants(n, q);
Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
std::vector< Node > var;
quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var);
//add cbqi lemma
//get the counterexample literal
Node ceLit = getCounterexampleLiteral(q);
- Node ceBody = d_quantEngine->getTermUtil()->getInstConstantBody( q );
+ Node ceBody = d_qreg.getInstConstantBody(q);
if( !ceBody.isNull() ){
//add counterexample lemma
Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
// must register with the instantiator
// must explicitly remove ITEs so that we record dependencies
std::vector<Node> ce_vars;
- TermUtil* tutil = d_quantEngine->getTermUtil();
- for (unsigned i = 0, nics = tutil->getNumInstantiationConstants(q); i < nics;
+ for (size_t i = 0, nics = d_qreg.getNumInstantiationConstants(q); i < nics;
i++)
{
- ce_vars.push_back(tutil->getInstantiationConstant(q, i));
+ ce_vars.push_back(d_qreg.getInstantiationConstant(q, i));
}
// send the lemma
- d_quantEngine->getOutputChannel().lemma(lem);
+ d_qim.lemma(lem, InferenceId::UNKNOWN);
// get the preprocessed form of the lemma we just sent
std::vector<Node> skolems;
std::vector<Node> skAsserts;
- Node ppLem = d_quantEngine->getValuation().getPreprocessedTerm(
- lem, skAsserts, skolems);
+ Node ppLem =
+ d_qstate.getValuation().getPreprocessedTerm(lem, skAsserts, skolems);
std::vector<Node> lemp{ppLem};
lemp.insert(lemp.end(), skAsserts.begin(), skAsserts.end());
ppLem = NodeManager::currentNM()->mkAnd(lemp);
#include "theory/quantifiers/cegqi/nested_qe.h"
#include "theory/quantifiers/cegqi/vts_term_cache.h"
#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
#include "util/statistics_registry.h"
namespace CVC4 {
#include "context/cdhashmap.h"
#include "expr/node_trie.h"
#include "expr/term_canonize.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
#include "theory/type_enumerator.h"
namespace CVC4 {
#include "theory/quantifiers/ematching/ho_trigger.h"
#include "theory/quantifiers/instantiate.h"
#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/uf/theory_uf_rewriter.h"
#include "util/hash.h"
HigherOrderTrigger::HigherOrderTrigger(
QuantifiersEngine* qe,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
Node q,
std::vector<Node>& nodes,
std::map<Node, std::vector<Node> >& ho_apps)
- : Trigger(qe, qim, q, nodes), d_ho_var_apps(ho_apps)
+ : Trigger(qe, qim, qr, q, nodes), d_ho_var_apps(ho_apps)
{
NodeManager* nm = NodeManager::currentNM();
// process the higher-order variable applications
// get substitution corresponding to m
std::vector<TNode> vars;
std::vector<TNode> subs;
- quantifiers::TermUtil* tutil = d_quantEngine->getTermUtil();
for (unsigned i = 0, size = d_quant[0].getNumChildren(); i < size; i++)
{
subs.push_back(m.d_vals[i]);
- vars.push_back(tutil->getInstantiationConstant(d_quant, i));
+ vars.push_back(d_qreg.getInstantiationConstant(d_quant, i));
}
Trace("ho-unif-debug") << "Run higher-order unification..." << std::endl;
private:
HigherOrderTrigger(QuantifiersEngine* qe,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
Node q,
std::vector<Node>& nodes,
std::map<Node, std::vector<Node> >& ho_apps);
if (trieIndex < iio->d_order.size())
{
size_t curr_index = iio->d_order[trieIndex];
- // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant,
- // curr_index );
Node n = m.get(curr_index);
if (n.isNull())
{
InstStrategy::InstStrategy(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : d_quantEngine(qe), d_qstate(qs), d_qim(qim)
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
{
}
InstStrategy::~InstStrategy() {}
class QuantifiersState;
class QuantifiersInferenceManager;
+class QuantifiersRegistry;
/** A status response to process */
enum class InstStrategyStatus
public:
InstStrategy(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
virtual ~InstStrategy();
/** presolve */
virtual void presolve();
QuantifiersState& d_qstate;
/** The quantifiers inference manager object */
QuantifiersInferenceManager& d_qim;
+ /** The quantifiers registry */
+ QuantifiersRegistry& d_qreg;
}; /* class InstStrategy */
} // namespace quantifiers
QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantRelevance* qr)
- : InstStrategy(qe, qs, qim), d_quant_rel(qr)
+ QuantifiersRegistry& qr,
+ QuantRelevance* qrlv)
+ : InstStrategy(qe, qs, qim, qr), d_quant_rel(qrlv)
{
//how to select trigger terms
d_tr_strategy = options::triggerSelMode();
{
tr = Trigger::mkTrigger(d_quantEngine,
d_qim,
+ d_qreg,
f,
patTerms[0],
false,
// will possibly want to get an old trigger
tr = Trigger::mkTrigger(d_quantEngine,
d_qim,
+ d_qreg,
f,
patTerms,
false,
d_single_trigger_gen[patTerms[index]] = true;
Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
d_qim,
+ d_qreg,
f,
patTerms[index],
false,
bool ntrivTriggers = options::relationalTriggers();
std::vector<Node> patTermsF;
std::map<Node, inst::TriggerTermInfo> tinfo;
- TermUtil* tu = d_quantEngine->getTermUtil();
NodeManager* nm = NodeManager::currentNM();
// well-defined function: can assume LHS is only pattern
if (options::quantFunWellDefined())
Node hd = QuantAttributes::getFunDefHead(f);
if (!hd.isNull())
{
- hd = tu->substituteBoundVariablesToInstConstants(hd, f);
+ hd = d_qreg.substituteBoundVariablesToInstConstants(hd, f);
patTermsF.push_back(hd);
tinfo[hd].init(f, hd);
}
// otherwise, use algorithm for collecting pattern terms
if (patTermsF.empty())
{
- Node bd = tu->getInstConstantBody(f);
+ Node bd = d_qreg.getInstConstantBody(f);
PatternTermSelector pts(f, d_tr_strategy, d_user_no_gen[f], true);
pts.collect(bd, patTermsF, tinfo);
if (ntrivTriggers)
std::vector<Node> vcs[2];
for (size_t i = 0, nchild = f[0].getNumChildren(); i < nchild; i++)
{
- Node ic = tu->getInstantiationConstant(f, i);
+ Node ic = d_qreg.getInstantiationConstant(f, i);
vcs[vcMap.find(ic) == vcMap.end() ? 0 : 1].push_back(f[0][i]);
}
for (size_t i = 0; i < 2; i++)
NodeManager* nm = NodeManager::currentNM();
// partial trigger : generate implication to mark user pattern
Node pat =
- d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables(
- tr->getInstPattern(), q);
+ d_qreg.substituteInstConstantsToBoundVariables(tr->getInstPattern(), q);
Node ipl = nm->mkNode(INST_PATTERN_LIST, pat);
Node qq = nm->mkNode(FORALL,
d_vc_partition[1][q],
InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
- QuantRelevance* qr);
+ QuantifiersRegistry& qr,
+ QuantRelevance* qrlv);
~InstStrategyAutoGenTriggers() {}
/** get auto-generated trigger */
InstStrategyUserPatterns::InstStrategyUserPatterns(
QuantifiersEngine* ie,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim)
- : InstStrategy(ie, qs, qim)
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr)
+ : InstStrategy(ie, qs, qim, qr)
{
}
InstStrategyUserPatterns::~InstStrategyUserPatterns() {}
std::vector<std::vector<Node> >& ugw = d_user_gen_wait[q];
for (size_t i = 0, usize = ugw.size(); i < usize; i++)
{
- Trigger* t = Trigger::mkTrigger(
- d_quantEngine, d_qim, q, ugw[i], true, Trigger::TR_RETURN_NULL);
+ Trigger* t = Trigger::mkTrigger(d_quantEngine,
+ d_qim,
+ d_qreg,
+ q,
+ ugw[i],
+ true,
+ Trigger::TR_RETURN_NULL);
if (t)
{
d_user_gen[q].push_back(t);
return;
}
Trigger* t = Trigger::mkTrigger(
- d_quantEngine, d_qim, q, nodes, true, Trigger::TR_MAKE_NEW);
+ d_quantEngine, d_qim, d_qreg, q, nodes, true, Trigger::TR_MAKE_NEW);
if (t)
{
d_user_gen[q].push_back(t);
public:
InstStrategyUserPatterns(QuantifiersEngine* qe,
QuantifiersState& qs,
- QuantifiersInferenceManager& qim);
+ QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr);
~InstStrategyUserPatterns();
/** add pattern */
void addUserPattern(Node q, Node pat);
// user-provided patterns
if (options::userPatternsQuant() != options::UserPatMode::IGNORE)
{
- d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim));
+ d_isup.reset(new InstStrategyUserPatterns(d_quantEngine, qs, qim, qr));
d_instStrategies.push_back(d_isup.get());
}
// auto-generated patterns
d_i_ag.reset(new InstStrategyAutoGenTriggers(
- d_quantEngine, qs, qim, d_quant_rel.get()));
+ d_quantEngine, qs, qim, qr, d_quant_rel.get()));
d_instStrategies.push_back(d_i_ag.get());
}
}
// take into account user patterns
if (q.getNumChildren() == 3)
{
- Node subsPat =
- d_quantEngine->getTermUtil()->substituteBoundVariablesToInstConstants(
- q[2], q);
+ Node subsPat = d_qreg.substituteBoundVariablesToInstConstants(q[2], q);
// add patterns
for (const Node& p : subsPat)
{
#include <vector>
#include "theory/quantifiers/ematching/inst_strategy.h"
+#include "theory/quantifiers/quant_module.h"
#include "theory/quantifiers/quant_relevance.h"
-#include "theory/quantifiers/quant_util.h"
namespace CVC4 {
namespace theory {
/** trigger class constructor */
Trigger::Trigger(QuantifiersEngine* qe,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
Node q,
std::vector<Node>& nodes)
- : d_quantEngine(qe), d_qim(qim), d_quant(q)
+ : d_quantEngine(qe), d_qim(qim), d_qreg(qr), d_quant(q)
{
// We must ensure that the ground subterms of the trigger have been
// preprocessed.
Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
Node f,
std::vector<Node>& nodes,
bool keepAll,
Trigger* t;
if (!ho_apps.empty())
{
- t = new HigherOrderTrigger(qe, qim, f, trNodes, ho_apps);
+ t = new HigherOrderTrigger(qe, qim, qr, f, trNodes, ho_apps);
}
else
{
- t = new Trigger(qe, qim, f, trNodes);
+ t = new Trigger(qe, qim, qr, f, trNodes);
}
qe->getTriggerDatabase()->addTrigger( trNodes, t );
Trigger* Trigger::mkTrigger(QuantifiersEngine* qe,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
Node f,
Node n,
bool keepAll,
{
std::vector< Node > nodes;
nodes.push_back( n );
- return mkTrigger(qe, qim, f, nodes, keepAll, trOption, useNVars);
+ return mkTrigger(qe, qim, qr, f, nodes, keepAll, trOption, useNVars);
}
int Trigger::getActiveScore() {
namespace quantifiers {
class QuantifiersInferenceManager;
+class QuantifiersRegistry;
}
namespace inst {
};
static Trigger* mkTrigger(QuantifiersEngine* qe,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
Node q,
std::vector<Node>& nodes,
bool keepAll = true,
/** single trigger version that calls the above function */
static Trigger* mkTrigger(QuantifiersEngine* qe,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
Node q,
Node n,
bool keepAll = true,
/** trigger constructor, intentionally protected (use Trigger::mkTrigger). */
Trigger(QuantifiersEngine* ie,
quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
Node q,
std::vector<Node>& nodes);
/** add an instantiation (called by InstMatchGenerator)
QuantifiersEngine* d_quantEngine;
/** Reference to the quantifiers inference manager */
quantifiers::QuantifiersInferenceManager& d_qim;
+ /** The quantifiers registry */
+ quantifiers::QuantifiersRegistry& d_qreg;
/** The quantified formula this trigger is for. */
Node d_quant;
/** match generator
#include "theory/quantifiers/term_util.h"
#include "theory/rewriter.h"
#include "theory/strings/sequences_rewriter.h"
+#include "theory/theory.h"
using namespace CVC4::kind;
using namespace std;
FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersRegistry& qr,
std::string name)
: TheoryModel(qs.getSatContext(), name, true),
d_qe(qe),
+ d_qreg(qr),
d_forall_asserts(qs.getSatContext()),
d_forallRlvComputed(false)
{
d_model_basis_terms[q].push_back(getModelBasisTerm(q[0][j].getType()));
}
}
- Node gn = d_qe->getTermUtil()->substituteInstConstants(
- n, q, d_model_basis_terms[q]);
+ Node gn = d_qreg.substituteInstConstants(n, q, d_model_basis_terms[q]);
return gn;
}
FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersRegistry& qr,
std::string name)
- : FirstOrderModel(qe, qs, name)
+ : FirstOrderModel(qe, qs, qr, name)
{
}
#include "context/cdlist.h"
#include "expr/attribute.h"
-#include "theory/quantifiers/quantifiers_state.h"
#include "theory/theory_model.h"
#include "theory/uf/theory_uf_model.h"
namespace quantifiers {
class TermDb;
+class QuantifiersState;
+class QuantifiersRegistry;
namespace fmcheck {
class FirstOrderModelFmc;
public:
FirstOrderModel(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersRegistry& qr,
std::string name);
virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
protected:
/** quant engine */
QuantifiersEngine* d_qe;
+ /** The quantifiers registry */
+ QuantifiersRegistry& d_qreg;
/** list of quantifiers asserted in the current context */
context::CDList<Node> d_forall_asserts;
/**
public:
FirstOrderModelFmc(QuantifiersEngine* qe,
QuantifiersState& qs,
+ QuantifiersRegistry& qr,
std::string name);
~FirstOrderModelFmc() override;
FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
{
for (const Node& v : it->second)
{
- indices.push_back(d_quantEngine->getTermUtil()->getVariableNum(q, v));
+ indices.push_back(TermUtil::getVariableNum(q, v));
}
}
}
#ifndef CVC4__BOUNDED_INTEGERS_H
#define CVC4__BOUNDED_INTEGERS_H
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
#include "context/cdhashmap.h"
#include "context/context.h"
#include "theory/quantifiers/quant_rep_bound_ext.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
using namespace std;
if( Trace.isOn("fmf-exh-inst-debug") ){
Trace("fmf-exh-inst-debug") << " Instantiation Constants: ";
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- Trace("fmf-exh-inst-debug") << d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ) << " ";
+ Trace("fmf-exh-inst-debug")
+ << d_qreg.getInstantiationConstant(f, i) << " ";
}
Trace("fmf-exh-inst-debug") << std::endl;
}
#define CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H
#include "theory/quantifiers/fmf/model_builder.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
#include "theory/theory_model.h"
namespace CVC4 {
#include "theory/quantifiers/inst_match.h"
#include "theory/quantifiers/instantiate.h"
-#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers_engine.h"
#include "context/context.h"
#include "context/context_mm.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
#include "theory/quantifiers/relevant_domain.h"
namespace CVC4 {
Instantiate::Instantiate(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
ProofNodeManager* pnm)
: d_qe(qe),
d_qstate(qs),
d_qim(qim),
+ d_qreg(qr),
d_pnm(pnm),
d_term_db(nullptr),
- d_term_util(nullptr),
d_total_inst_debug(qs.getUserContext()),
d_c_inst_match_trie_dom(qs.getUserContext()),
d_pfInst(pnm ? new CDProof(pnm) : nullptr)
d_recorded_inst.clear();
}
d_term_db = d_qe->getTermDatabase();
- d_term_util = d_qe->getTermUtil();
return true;
}
Assert(!d_qstate.isInConflict());
Assert(terms.size() == q[0].getNumChildren());
Assert(d_term_db != nullptr);
- Assert(d_term_util != nullptr);
Trace("inst-add-debug") << "For quantified formula " << q
<< ", add instantiation: " << std::endl;
for (unsigned i = 0, size = terms.size(); i < size; i++)
<< terms[i] << std::endl;
bad_inst = true;
}
- else if (expr::hasSubterm(terms[i], d_term_util->d_inst_constants[q]))
+ else if (expr::hasSubterm(terms[i], d_qreg.d_inst_constants[q]))
{
Trace("inst") << "***& inst contains inst constants : " << terms[i]
<< std::endl;
// construct the instantiation
Trace("inst-add-debug") << "Constructing instantiation..." << std::endl;
- Assert(d_term_util->d_vars[q].size() == terms.size());
+ Assert(d_qreg.d_vars[q].size() == terms.size());
// get the instantiation
- Node body =
- getInstantiation(q, d_term_util->d_vars[q], terms, doVts, pfTmp.get());
+ Node body = getInstantiation(q, d_qreg.d_vars[q], terms, doVts, pfTmp.get());
Node orig_body = body;
// now preprocess, storing the trust node for the rewrite
TrustNode tpBody = quantifiers::QuantifiersRewriter::preprocess(body, true);
Node Instantiate::getInstantiation(Node q, InstMatch& m, bool doVts)
{
- Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end());
+ Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
Assert(m.d_vals.size() == q[0].getNumChildren());
- return getInstantiation(q, d_term_util->d_vars[q], m.d_vals, doVts);
+ return getInstantiation(q, d_qreg.d_vars[q], m.d_vals, doVts);
}
Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts)
{
- Assert(d_term_util->d_vars.find(q) != d_term_util->d_vars.end());
- return getInstantiation(q, d_term_util->d_vars[q], terms, doVts);
+ Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
+ return getInstantiation(q, d_qreg.d_vars[q], terms, doVts);
}
bool Instantiate::recordInstantiationInternal(Node q,
namespace quantifiers {
class TermDb;
-class TermUtil;
+class QuantifiersState;
+class QuantifiersInferenceManager;
+class QuantifiersRegistry;
/** Instantiation rewriter
*
Instantiate(QuantifiersEngine* qe,
QuantifiersState& qs,
QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
ProofNodeManager* pnm = nullptr);
~Instantiate();
QuantifiersState& d_qstate;
/** Reference to the quantifiers inference manager */
QuantifiersInferenceManager& d_qim;
+ /** The quantifiers registry */
+ QuantifiersRegistry& d_qreg;
/** pointer to the proof node manager */
ProofNodeManager* d_pnm;
/** cache of term database for quantifiers engine */
TermDb* d_term_db;
- /** cache of term util for quantifiers engine */
- TermUtil* d_term_util;
/** instantiation rewriter classes */
std::vector<InstantiationRewriter*> d_instRewrite;
//check constraints
for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
//apply substitution to the tconstraint
- Node cons =
- p->getTermUtil()->substituteBoundVariables(it->first, d_q, terms);
+ Node cons = p->getQuantifiersRegistry().substituteBoundVariables(
+ it->first, d_q, terms);
cons = it->second ? cons : cons.negate();
if (!entailmentTest(p, cons, p->atConflictEffort())) {
return true;
#include "context/cdhashmap.h"
#include "context/cdlist.h"
#include "expr/node_trie.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
namespace CVC4 {
namespace theory {
--- /dev/null
+/********************* */
+/*! \file quant_module.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 quantifier module
+ **/
+
+#include "theory/quantifiers/quant_module.h"
+#include "theory/quantifiers/inst_match.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+
+QuantifiersModule::QuantifiersModule(
+ quantifiers::QuantifiersState& qs,
+ quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
+ QuantifiersEngine* qe)
+ : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
+{
+}
+
+QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
+{
+ return QEFFORT_NONE;
+}
+
+eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const
+{
+ return d_qstate.getEqualityEngine();
+}
+
+bool QuantifiersModule::areEqual(TNode n1, TNode n2) const
+{
+ return d_qstate.areEqual(n1, n2);
+}
+
+bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const
+{
+ return d_qstate.areDisequal(n1, n2);
+}
+
+TNode QuantifiersModule::getRepresentative(TNode n) const
+{
+ return d_qstate.getRepresentative(n);
+}
+
+QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const
+{
+ return d_quantEngine;
+}
+
+quantifiers::TermDb* QuantifiersModule::getTermDatabase() const
+{
+ return d_quantEngine->getTermDatabase();
+}
+
+quantifiers::TermUtil* QuantifiersModule::getTermUtil() const
+{
+ return d_quantEngine->getTermUtil();
+}
+
+quantifiers::QuantifiersState& QuantifiersModule::getState()
+{
+ return d_qstate;
+}
+
+quantifiers::QuantifiersInferenceManager&
+QuantifiersModule::getInferenceManager()
+{
+ return d_qim;
+}
+
+quantifiers::QuantifiersRegistry& QuantifiersModule::getQuantifiersRegistry()
+{
+ return d_qreg;
+}
+
+} // namespace theory
+} /* namespace CVC4 */
--- /dev/null
+/********************* */
+/*! \file quant_module.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Andrew Reynolds, Morgan Deters, Mathias Preiner
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 quantifier module
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANT_MODULE_H
+#define CVC4__THEORY__QUANT_MODULE_H
+
+#include <iostream>
+#include <map>
+#include <vector>
+
+#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/quantifiers_registry.h"
+#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+class QuantifiersEngine;
+
+namespace quantifiers {
+class TermDb;
+class TermUtil;
+} // namespace quantifiers
+
+/** QuantifiersModule class
+ *
+ * This is the virtual class for defining subsolvers of the quantifiers theory.
+ * It has a similar interface to a Theory object.
+ */
+class QuantifiersModule
+{
+ public:
+ /** effort levels for quantifiers modules check */
+ enum QEffort
+ {
+ // conflict effort, for conflict-based instantiation
+ QEFFORT_CONFLICT,
+ // standard effort, for heuristic instantiation
+ QEFFORT_STANDARD,
+ // model effort, for model-based instantiation
+ QEFFORT_MODEL,
+ // last call effort, for last resort techniques
+ QEFFORT_LAST_CALL,
+ // none
+ QEFFORT_NONE,
+ };
+
+ public:
+ QuantifiersModule(quantifiers::QuantifiersState& qs,
+ quantifiers::QuantifiersInferenceManager& qim,
+ quantifiers::QuantifiersRegistry& qr,
+ QuantifiersEngine* qe);
+ virtual ~QuantifiersModule() {}
+ /** Presolve.
+ *
+ * Called at the beginning of check-sat call.
+ */
+ virtual void presolve() {}
+ /** Needs check.
+ *
+ * Returns true if this module wishes a call to be made
+ * to check(e) during QuantifiersEngine::check(e).
+ */
+ virtual bool needsCheck(Theory::Effort e)
+ {
+ return e >= Theory::EFFORT_LAST_CALL;
+ }
+ /** Needs model.
+ *
+ * Whether this module needs a model built during a
+ * call to QuantifiersEngine::check(e)
+ * It returns one of QEFFORT_* from quantifiers_engine.h,
+ * which specifies the quantifiers effort in which it requires the model to
+ * be built.
+ */
+ virtual QEffort needsModel(Theory::Effort e);
+ /** Reset.
+ *
+ * Called at the beginning of QuantifiersEngine::check(e).
+ */
+ virtual void reset_round(Theory::Effort e) {}
+ /** Check.
+ *
+ * Called during QuantifiersEngine::check(e) depending
+ * if needsCheck(e) returns true.
+ */
+ virtual void check(Theory::Effort e, QEffort quant_e) = 0;
+ /** Check complete?
+ *
+ * Returns false if the module's reasoning was globally incomplete
+ * (e.g. "sat" must be replaced with "incomplete").
+ *
+ * This is called just before the quantifiers engine will return
+ * with no lemmas added during a LAST_CALL effort check.
+ */
+ virtual bool checkComplete() { return true; }
+ /** Check was complete for quantified formula q
+ *
+ * If for each quantified formula q, some module returns true for
+ * checkCompleteFor( q ),
+ * and no lemmas are added by the quantifiers theory, then we may answer
+ * "sat", unless
+ * we are incomplete for other reasons.
+ */
+ virtual bool checkCompleteFor(Node q) { return false; }
+ /** Check ownership
+ *
+ * Called once for new quantified formulas that are registered by the
+ * quantifiers theory. The primary purpose of this function is to establish
+ * if this module is the owner of quantified formula q.
+ */
+ virtual void checkOwnership(Node q) {}
+ /** Register quantifier
+ *
+ * Called once for new quantified formulas q that are pre-registered by the
+ * quantifiers theory, after internal ownership of quantified formulas is
+ * finalized. This does context-independent initialization of this module
+ * for quantified formula q.
+ */
+ virtual void registerQuantifier(Node q) {}
+ /** Pre-register quantifier
+ *
+ * Called once for new quantified formulas that are
+ * pre-registered by the quantifiers theory, after
+ * internal ownership of quantified formulas is finalized.
+ */
+ virtual void preRegisterQuantifier(Node q) {}
+ /** Assert node.
+ *
+ * Called when a quantified formula q is asserted to the quantifiers theory
+ */
+ virtual void assertNode(Node q) {}
+ /** Identify this module (for debugging, dynamic configuration, etc..) */
+ virtual std::string identify() const = 0;
+ //----------------------------general queries
+ /** get currently used the equality engine */
+ eq::EqualityEngine* getEqualityEngine() const;
+ /** are n1 and n2 equal in the current used equality engine? */
+ bool areEqual(TNode n1, TNode n2) const;
+ /** are n1 and n2 disequal in the current used equality engine? */
+ bool areDisequal(TNode n1, TNode n2) const;
+ /** get the representative of n in the current used equality engine */
+ TNode getRepresentative(TNode n) const;
+ /** get quantifiers engine that owns this module */
+ QuantifiersEngine* getQuantifiersEngine() const;
+ /** get currently used term database */
+ quantifiers::TermDb* getTermDatabase() const;
+ /** get currently used term utility object */
+ quantifiers::TermUtil* getTermUtil() const;
+ /** get the quantifiers state */
+ quantifiers::QuantifiersState& getState();
+ /** get the quantifiers inference manager */
+ quantifiers::QuantifiersInferenceManager& getInferenceManager();
+ /** get the quantifiers registry */
+ quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
+ //----------------------------end general queries
+ protected:
+ /** pointer to the quantifiers engine that owns this module */
+ QuantifiersEngine* d_quantEngine;
+ /** The state of the quantifiers engine */
+ quantifiers::QuantifiersState& d_qstate;
+ /** The quantifiers inference manager */
+ quantifiers::QuantifiersInferenceManager& d_qim;
+ /** The quantifiers registry */
+ quantifiers::QuantifiersRegistry& d_qreg;
+}; /* class QuantifiersModule */
+
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANT_UTIL_H */
#define CVC4__THEORY__QUANT_SPLIT_H
#include "context/cdo.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
namespace CVC4 {
namespace theory {
**/
#include "theory/quantifiers/quant_util.h"
-#include "theory/quantifiers/inst_match.h"
-#include "theory/quantifiers/term_database.h"
+
#include "theory/quantifiers/term_util.h"
-#include "theory/quantifiers_engine.h"
using namespace CVC4::kind;
namespace CVC4 {
namespace theory {
-QuantifiersModule::QuantifiersModule(
- quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::QuantifiersRegistry& qr,
- QuantifiersEngine* qe)
- : d_quantEngine(qe), d_qstate(qs), d_qim(qim), d_qreg(qr)
-{
-}
-
-QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e)
-{
- return QEFFORT_NONE;
-}
-
-eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const
-{
- return d_qstate.getEqualityEngine();
-}
-
-bool QuantifiersModule::areEqual(TNode n1, TNode n2) const
-{
- return d_qstate.areEqual(n1, n2);
-}
-
-bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const
-{
- return d_qstate.areDisequal(n1, n2);
-}
-
-TNode QuantifiersModule::getRepresentative(TNode n) const
-{
- return d_qstate.getRepresentative(n);
-}
-
-QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const
-{
- return d_quantEngine;
-}
-
-quantifiers::TermDb* QuantifiersModule::getTermDatabase() const
-{
- return d_quantEngine->getTermDatabase();
-}
-
-quantifiers::TermUtil* QuantifiersModule::getTermUtil() const
-{
- return d_quantEngine->getTermUtil();
-}
-
-quantifiers::QuantifiersState& QuantifiersModule::getState()
-{
- return d_qstate;
-}
-
-quantifiers::QuantifiersInferenceManager&
-QuantifiersModule::getInferenceManager()
-{
- return d_qim;
-}
-
QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){
initialize( n, computeEq );
}
#include <map>
#include <vector>
-#include "theory/quantifiers/quantifiers_inference_manager.h"
-#include "theory/quantifiers/quantifiers_registry.h"
-#include "theory/quantifiers/quantifiers_state.h"
+#include "expr/node.h"
#include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
namespace CVC4 {
namespace theory {
-class QuantifiersEngine;
-
-namespace quantifiers {
- class TermDb;
- class TermUtil;
-}
-
-/** QuantifiersModule class
-*
-* This is the virtual class for defining subsolvers of the quantifiers theory.
-* It has a similar interface to a Theory object.
-*/
-class QuantifiersModule {
- public:
- /** effort levels for quantifiers modules check */
- enum QEffort
- {
- // conflict effort, for conflict-based instantiation
- QEFFORT_CONFLICT,
- // standard effort, for heuristic instantiation
- QEFFORT_STANDARD,
- // model effort, for model-based instantiation
- QEFFORT_MODEL,
- // last call effort, for last resort techniques
- QEFFORT_LAST_CALL,
- // none
- QEFFORT_NONE,
- };
-
- public:
- QuantifiersModule(quantifiers::QuantifiersState& qs,
- quantifiers::QuantifiersInferenceManager& qim,
- quantifiers::QuantifiersRegistry& qr,
- QuantifiersEngine* qe);
- virtual ~QuantifiersModule(){}
- /** Presolve.
- *
- * Called at the beginning of check-sat call.
- */
- virtual void presolve() {}
- /** Needs check.
- *
- * Returns true if this module wishes a call to be made
- * to check(e) during QuantifiersEngine::check(e).
- */
- virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
- /** Needs model.
- *
- * Whether this module needs a model built during a
- * call to QuantifiersEngine::check(e)
- * It returns one of QEFFORT_* from quantifiers_engine.h,
- * which specifies the quantifiers effort in which it requires the model to
- * be built.
- */
- virtual QEffort needsModel(Theory::Effort e);
- /** Reset.
- *
- * Called at the beginning of QuantifiersEngine::check(e).
- */
- virtual void reset_round( Theory::Effort e ){}
- /** Check.
- *
- * Called during QuantifiersEngine::check(e) depending
- * if needsCheck(e) returns true.
- */
- virtual void check(Theory::Effort e, QEffort quant_e) = 0;
- /** Check complete?
- *
- * Returns false if the module's reasoning was globally incomplete
- * (e.g. "sat" must be replaced with "incomplete").
- *
- * This is called just before the quantifiers engine will return
- * with no lemmas added during a LAST_CALL effort check.
- */
- virtual bool checkComplete() { return true; }
- /** Check was complete for quantified formula q
- *
- * If for each quantified formula q, some module returns true for
- * checkCompleteFor( q ),
- * and no lemmas are added by the quantifiers theory, then we may answer
- * "sat", unless
- * we are incomplete for other reasons.
- */
- virtual bool checkCompleteFor( Node q ) { return false; }
- /** Check ownership
- *
- * Called once for new quantified formulas that are registered by the
- * quantifiers theory. The primary purpose of this function is to establish
- * if this module is the owner of quantified formula q.
- */
- virtual void checkOwnership(Node q) {}
- /** Register quantifier
- *
- * Called once for new quantified formulas q that are pre-registered by the
- * quantifiers theory, after internal ownership of quantified formulas is
- * finalized. This does context-independent initialization of this module
- * for quantified formula q.
- */
- virtual void registerQuantifier(Node q) {}
- /** Pre-register quantifier
- *
- * Called once for new quantified formulas that are
- * pre-registered by the quantifiers theory, after
- * internal ownership of quantified formulas is finalized.
- */
- virtual void preRegisterQuantifier(Node q) {}
- /** Assert node.
- *
- * Called when a quantified formula q is asserted to the quantifiers theory
- */
- virtual void assertNode(Node q) {}
- /** Identify this module (for debugging, dynamic configuration, etc..) */
- virtual std::string identify() const = 0;
- //----------------------------general queries
- /** get currently used the equality engine */
- eq::EqualityEngine* getEqualityEngine() const;
- /** are n1 and n2 equal in the current used equality engine? */
- bool areEqual(TNode n1, TNode n2) const;
- /** are n1 and n2 disequal in the current used equality engine? */
- bool areDisequal(TNode n1, TNode n2) const;
- /** get the representative of n in the current used equality engine */
- TNode getRepresentative(TNode n) const;
- /** get quantifiers engine that owns this module */
- QuantifiersEngine* getQuantifiersEngine() const;
- /** get currently used term database */
- quantifiers::TermDb* getTermDatabase() const;
- /** get currently used term utility object */
- quantifiers::TermUtil* getTermUtil() const;
- /** get the quantifiers state */
- quantifiers::QuantifiersState& getState();
- /** get the quantifiers inference manager */
- quantifiers::QuantifiersInferenceManager& getInferenceManager();
- //----------------------------end general queries
- protected:
- /** pointer to the quantifiers engine that owns this module */
- QuantifiersEngine* d_quantEngine;
- /** The state of the quantifiers engine */
- quantifiers::QuantifiersState& d_qstate;
- /** The quantifiers inference manager */
- quantifiers::QuantifiersInferenceManager& d_qim;
- /** The quantifiers registry */
- quantifiers::QuantifiersRegistry& d_qreg;
-};/* class QuantifiersModule */
-
/** Quantifiers utility
-*
-* This is a lightweight version of a quantifiers module that does not implement
-* methods
-* for checking satisfiability.
-*/
+ *
+ * This is a lightweight version of a quantifiers module that does not implement
+ * methods for checking satisfiability.
+ */
class QuantifiersUtil {
public:
QuantifiersUtil(){}
// full saturation : instantiate from relevant domain, then arbitrary terms
if (options::fullSaturateQuant() || options::fullSaturateInterleave())
{
- d_rel_dom.reset(new RelevantDomain(qe));
+ d_rel_dom.reset(new RelevantDomain(qe, qr));
d_fs.reset(new InstStrategyEnum(qe, qs, qim, qr, d_rel_dom.get()));
modules.push_back(d_fs.get());
}
#include "theory/quantifiers/quantifiers_registry.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
+#include "theory/quantifiers/term_util.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
+void QuantifiersRegistry::registerQuantifier(Node q)
+{
+ if (d_inst_constants.find(q) != d_inst_constants.end())
+ {
+ return;
+ }
+ NodeManager* nm = NodeManager::currentNM();
+ Debug("quantifiers-engine")
+ << "Instantiation constants for " << q << " : " << std::endl;
+ for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
+ {
+ d_vars[q].push_back(q[0][i]);
+ // make instantiation constants
+ Node ic = nm->mkInstConstant(q[0][i].getType());
+ d_inst_constants_map[ic] = q;
+ d_inst_constants[q].push_back(ic);
+ Debug("quantifiers-engine") << " " << ic << std::endl;
+ // set the var number attribute
+ InstVarNumAttribute ivna;
+ ic.setAttribute(ivna, i);
+ InstConstantAttribute ica;
+ ic.setAttribute(ica, q);
+ }
+}
+
+bool QuantifiersRegistry::reset(Theory::Effort e) { return true; }
+
+std::string QuantifiersRegistry::identify() const
+{
+ return "QuantifiersRegistry";
+}
+
QuantifiersModule* QuantifiersRegistry::getOwner(Node q) const
{
std::map<Node, QuantifiersModule*>::const_iterator it = d_owner.find(q);
return mo == m || mo == nullptr;
}
+Node QuantifiersRegistry::getInstantiationConstant(Node q, size_t i) const
+{
+ std::map<Node, std::vector<Node> >::const_iterator it =
+ d_inst_constants.find(q);
+ if (it != d_inst_constants.end())
+ {
+ return it->second[i];
+ }
+ return Node::null();
+}
+
+size_t QuantifiersRegistry::getNumInstantiationConstants(Node q) const
+{
+ std::map<Node, std::vector<Node> >::const_iterator it =
+ d_inst_constants.find(q);
+ if (it != d_inst_constants.end())
+ {
+ return it->second.size();
+ }
+ return 0;
+}
+
+Node QuantifiersRegistry::getInstConstantBody(Node q)
+{
+ std::map<Node, Node>::const_iterator it = d_inst_const_body.find(q);
+ if (it == d_inst_const_body.end())
+ {
+ Node n = substituteBoundVariablesToInstConstants(q[1], q);
+ d_inst_const_body[q] = n;
+ return n;
+ }
+ return it->second;
+}
+
+Node QuantifiersRegistry::substituteBoundVariablesToInstConstants(Node n,
+ Node q)
+{
+ registerQuantifier(q);
+ return n.substitute(d_vars[q].begin(),
+ d_vars[q].end(),
+ d_inst_constants[q].begin(),
+ d_inst_constants[q].end());
+}
+
+Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n,
+ Node q)
+{
+ registerQuantifier(q);
+ return n.substitute(d_inst_constants[q].begin(),
+ d_inst_constants[q].end(),
+ d_vars[q].begin(),
+ d_vars[q].end());
+}
+
+Node QuantifiersRegistry::substituteBoundVariables(Node n,
+ Node q,
+ std::vector<Node>& terms)
+{
+ registerQuantifier(q);
+ Assert(d_vars[q].size() == terms.size());
+ return n.substitute(
+ d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end());
+}
+
+Node QuantifiersRegistry::substituteInstConstants(Node n,
+ Node q,
+ std::vector<Node>& terms)
+{
+ registerQuantifier(q);
+ Assert(d_inst_constants[q].size() == terms.size());
+ return n.substitute(d_inst_constants[q].begin(),
+ d_inst_constants[q].end(),
+ terms.begin(),
+ terms.end());
+}
+
} // namespace quantifiers
} // namespace theory
} // namespace CVC4
#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
#include "expr/node.h"
+#include "theory/quantifiers/quant_util.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
+class Instantiate;
+
/**
* The quantifiers registry, which manages basic information about which
- * quantifiers modules have ownership of quantified formulas.
+ * quantifiers modules have ownership of quantified formulas, and manages
+ * the allocation of instantiation constants per quantified formula.
*/
-class QuantifiersRegistry
+class QuantifiersRegistry : public QuantifiersUtil
{
+ friend class Instantiate;
+
public:
QuantifiersRegistry() {}
~QuantifiersRegistry() {}
+ /**
+ * Register quantifier, which allocates the instantiation constants for q.
+ */
+ void registerQuantifier(Node q) override;
+ /** reset */
+ bool reset(Theory::Effort e) override;
+ /** identify */
+ std::string identify() const override;
+ //----------------------------- ownership
/** get the owner of quantified formula q */
QuantifiersModule* getOwner(Node q) const;
/**
* Return true if module q has no owner registered or if its registered owner is m.
*/
bool hasOwnership(Node q, QuantifiersModule* m) const;
-
+ //----------------------------- end ownership
+ //----------------------------- instantiation constants
+ /** get the i^th instantiation constant of q */
+ Node getInstantiationConstant(Node q, size_t i) const;
+ /** get number of instantiation constants for q */
+ size_t getNumInstantiationConstants(Node q) const;
+ /** get the ce body q[e/x] */
+ Node getInstConstantBody(Node q);
+ /** returns node n with bound vars of q replaced by instantiation constants of
+ q node n : is the future pattern node q : is the quantifier containing
+ which bind the variable return a pattern where the variable are replaced by
+ variable for instantiation.
+ */
+ Node substituteBoundVariablesToInstConstants(Node n, Node q);
+ /** substitute { instantiation constants of q -> bound variables of q } in n
+ */
+ Node substituteInstConstantsToBoundVariables(Node n, Node q);
+ /** substitute { variables of q -> terms } in n */
+ Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms);
+ /** substitute { instantiation constants of q -> terms } in n */
+ Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms);
+ //----------------------------- end instantiation constants
private:
/**
* Maps quantified formulas to the module that owns them, if any module has
* precendence.
*/
std::map<Node, int32_t> d_owner_priority;
+ /** map from universal quantifiers to the list of variables */
+ std::map<Node, std::vector<Node> > d_vars;
+ /** map from universal quantifiers to their inst constant body */
+ std::map<Node, Node> d_inst_const_body;
+ /** instantiation constants to universal quantifiers */
+ std::map<Node, Node> d_inst_constants_map;
+ /** map from universal quantifiers to the list of instantiation constants */
+ std::map<Node, std::vector<Node> > d_inst_constants;
};
} // namespace quantifiers
}
}
-
-
-RelevantDomain::RelevantDomain( QuantifiersEngine* qe ) : d_qe( qe ){
- d_is_computed = false;
+RelevantDomain::RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr)
+ : d_qe(qe), d_qreg(qr)
+{
+ d_is_computed = false;
}
RelevantDomain::~RelevantDomain() {
FirstOrderModel* fm = d_qe->getModel();
for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node q = fm->getAssertedQuantifier( i );
- Node icf = d_qe->getTermUtil()->getInstConstantBody( q );
+ Node icf = d_qreg.getInstConstantBody(q);
Trace("rel-dom-debug") << "compute relevant domain for " << icf << std::endl;
computeRelevantDomain( q, icf, true, true );
}
void RelevantDomain::computeRelevantDomainOpCh( RDomain * rf, Node n ) {
if( n.getKind()==INST_CONSTANT ){
- Node q = d_qe->getTermUtil()->getInstConstAttr( n );
+ Node q = TermUtil::getInstConstAttr(n);
//merge the RDomains
unsigned id = n.getAttribute(InstVarNumAttribute());
Assert(q[0][id].getType() == n.getType());
Trace("rel-dom-debug") << n << " is variable # " << id << " for " << q;
- Trace("rel-dom-debug") << " with body : " << d_qe->getTermUtil()->getInstConstantBody( q ) << std::endl;
+ Trace("rel-dom-debug") << " with body : " << d_qreg.getInstConstantBody(q)
+ << std::endl;
RDomain * rq = getRDomain( q, id );
if( rf!=rq ){
rq->merge( rf );
d_rel_dom_lit[hasPol][pol][n].d_merge = false;
int varCount = 0;
int varCh = -1;
- TermUtil* tu = d_qe->getTermUtil();
for( unsigned i=0; i<n.getNumChildren(); i++ ){
if( n[i].getKind()==INST_CONSTANT ){
// must get the quantified formula this belongs to, which may be
// different from q
- Node qi = tu->getInstConstAttr(n[i]);
+ Node qi = TermUtil::getInstConstAttr(n[i]);
unsigned id = n[i].getAttribute(InstVarNumAttribute());
d_rel_dom_lit[hasPol][pol][n].d_rd[i] = getRDomain(qi, id, false);
varCount++;
bool hasNonVar = false;
for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
if (!it->first.isNull() && it->first.getKind() == INST_CONSTANT
- && tu->getInstConstAttr(it->first) == q)
+ && TermUtil::getInstConstAttr(it->first) == q)
{
if( var.isNull() ){
var = it->first;
namespace theory {
namespace quantifiers {
+class QuantifiersRegistry;
+
/** Relevant Domain
*
* This class computes the relevant domain of
class RelevantDomain : public QuantifiersUtil
{
public:
- RelevantDomain(QuantifiersEngine* qe);
+ RelevantDomain(QuantifiersEngine* qe, QuantifiersRegistry& qr);
virtual ~RelevantDomain();
/** Reset. */
bool reset(Theory::Effort e) override;
std::map< RDomain *, int > d_ri_map;
/** Quantifiers engine associated with this utility. */
QuantifiersEngine* d_qe;
+ /** The quantifiers registry */
+ QuantifiersRegistry& d_qreg;
/** have we computed the relevant domain on this full effort check? */
bool d_is_computed;
/** relevant domain literal
#include "expr/node_algorithm.h"
#include "theory/quantifiers/term_util.h"
+#include "theory/rewriter.h"
using namespace CVC4;
using namespace CVC4::kind;
#include "context/cdhashmap.h"
#include "expr/node.h"
#include "expr/type_node.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/eager_proof_generator.h"
#include "theory/trust_node.h"
namespace CVC4 {
class DTypeConstructor;
namespace theory {
+
+class QuantifiersEngine;
+
namespace quantifiers {
+class QuantifiersState;
+
/** Skolemization utility
*
* This class constructs Skolemization lemmas.
#define CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H
#include "context/cdhashmap.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
#include "theory/quantifiers/sygus/sygus_qe_preproc.h"
#include "theory/quantifiers/sygus/sygus_stats.h"
#include "theory/quantifiers/sygus/synth_conjecture.h"
#include <unordered_set>
#include "context/cdhashset.h"
-#include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/quant_module.h"
namespace CVC4 {
namespace theory {
TermDb::TermDb(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
QuantifiersEngine* qe)
: d_quantEngine(qe),
d_qstate(qs),
d_qim(qim),
+ d_qreg(qr),
d_termsContext(),
d_termsContextUse(options::termDbCd() ? qs.getSatContext()
: &d_termsContext),
}
void TermDb::registerQuantifier( Node q ) {
- Assert(q[0].getNumChildren()
- == d_quantEngine->getTermUtil()->getNumInstantiationConstants(q));
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- Node ic = d_quantEngine->getTermUtil()->getInstantiationConstant( q, i );
+ Assert(q[0].getNumChildren() == d_qreg.getNumInstantiationConstants(q));
+ for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
+ {
+ Node ic = d_qreg.getInstantiationConstant(q, i);
setTermInactive( ic );
}
}
{
if (ret.getKind() == EQUAL || ret.getKind() == GEQ)
{
- TheoryEngine* te = d_quantEngine->getTheoryEngine();
+ Valuation& val = d_qstate.getValuation();
for (unsigned j = 0; j < 2; j++)
{
- std::pair<bool, Node> et = te->entailmentCheck(
+ std::pair<bool, Node> et = val.entailmentCheck(
options::TheoryOfMode::THEORY_OF_TYPE_BASED,
j == 0 ? ret : ret.negate());
if (et.first)
namespace quantifiers {
-class ConjectureGenerator;
-class TermGenEnv;
+class QuantifiersState;
+class QuantifiersInferenceManager;
+class QuantifiersRegistry;
/** Context-dependent list of nodes */
class DbList
public:
TermDb(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
+ QuantifiersRegistry& qr,
QuantifiersEngine* qe);
~TermDb();
/** presolve (called once per user check-sat) */
QuantifiersState& d_qstate;
/** The quantifiers inference manager */
QuantifiersInferenceManager& d_qim;
+ /** The quantifiers registry */
+ QuantifiersRegistry& d_qreg;
/** A context for the data structures below, when not context-dependent */
context::Context d_termsContext;
/** The context we are using for the data structures below */
}
-void TermUtil::registerQuantifier( Node q ){
- if( d_inst_constants.find( q )==d_inst_constants.end() ){
- Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl;
- for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
- d_vars[q].push_back( q[0][i] );
- d_var_num[q][q[0][i]] = i;
- //make instantiation constants
- Node ic = NodeManager::currentNM()->mkInstConstant( q[0][i].getType() );
- d_inst_constants_map[ic] = q;
- d_inst_constants[ q ].push_back( ic );
- Debug("quantifiers-engine") << " " << ic << std::endl;
- //set the var number attribute
- InstVarNumAttribute ivna;
- ic.setAttribute( ivna, i );
- InstConstantAttribute ica;
- ic.setAttribute( ica, q );
- }
- }
+size_t TermUtil::getVariableNum(Node q, Node v)
+{
+ Node::iterator it = std::find(q[0].begin(), q[0].end(), v);
+ Assert(it != q[0].end());
+ return it - q[0].begin();
}
Node TermUtil::getRemoveQuantifiers2( Node n, std::map< Node, Node >& visited ) {
return getRemoveQuantifiers(q);
}
-/** get the i^th instantiation constant of q */
-Node TermUtil::getInstantiationConstant( Node q, int i ) const {
- std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
- if( it!=d_inst_constants.end() ){
- return it->second[i];
- }else{
- return Node::null();
- }
-}
-
-/** get number of instantiation constants for q */
-unsigned TermUtil::getNumInstantiationConstants( Node q ) const {
- std::map< Node, std::vector< Node > >::const_iterator it = d_inst_constants.find( q );
- if( it!=d_inst_constants.end() ){
- return it->second.size();
- }else{
- return 0;
- }
-}
-
-Node TermUtil::getInstConstantBody( Node q ){
- std::map< Node, Node >::iterator it = d_inst_const_body.find( q );
- if( it==d_inst_const_body.end() ){
- Node n = substituteBoundVariablesToInstConstants(q[1], q);
- d_inst_const_body[ q ] = n;
- return n;
- }else{
- return it->second;
- }
-}
-
-Node TermUtil::substituteBoundVariablesToInstConstants(Node n, Node q)
-{
- registerQuantifier( q );
- return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() );
-}
-
-Node TermUtil::substituteInstConstantsToBoundVariables(Node n, Node q)
-{
- registerQuantifier( q );
- return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() );
-}
-
-Node TermUtil::substituteBoundVariables(Node n,
- Node q,
- std::vector<Node>& terms)
-{
- registerQuantifier(q);
- Assert(d_vars[q].size() == terms.size());
- return n.substitute( d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end() );
-}
-
-Node TermUtil::substituteInstConstants(Node n, Node q, std::vector<Node>& terms)
-{
- registerQuantifier(q);
- Assert(d_inst_constants[q].size() == terms.size());
- return n.substitute(d_inst_constants[q].begin(),
- d_inst_constants[q].end(),
- terms.begin(),
- terms.end());
-}
-
void TermUtil::computeInstConstContains(Node n, std::vector<Node>& ics)
{
computeVarContainsInternal(n, INST_CONSTANT, ics);
#include <unordered_set>
#include "expr/attribute.h"
-#include "theory/quantifiers/quant_util.h"
#include "theory/type_enumerator.h"
namespace CVC4 {
namespace quantifiers {
class TermDatabase;
-class Instantiate;
// TODO : #1216 split this class, most of the functions in this class should be dispersed to where they are used.
-class TermUtil : public QuantifiersUtil
+class TermUtil
{
- // TODO : remove these
- friend class ::CVC4::theory::QuantifiersEngine;
- friend class Instantiate;
-
public:
TermUtil();
~TermUtil();
Node d_zero;
Node d_one;
- /** reset */
- bool reset(Theory::Effort e) override { return true; }
- /** register quantifier */
- void registerQuantifier(Node q) override;
- /** identify */
- std::string identify() const override { return "TermUtil"; }
// for inst constant
- private:
- /** map from universal quantifiers to the list of variables */
- std::map< Node, std::vector< Node > > d_vars;
- std::map< Node, std::map< Node, unsigned > > d_var_num;
- /** map from universal quantifiers to their inst constant body */
- std::map< Node, Node > d_inst_const_body;
- /** instantiation constants to universal quantifiers */
- std::map< Node, Node > d_inst_constants_map;
-public:
- /** map from universal quantifiers to the list of instantiation constants */
- std::map< Node, std::vector< Node > > d_inst_constants;
- /** get variable number */
- unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; }
- /** get the i^th instantiation constant of q */
- Node getInstantiationConstant( Node q, int i ) const;
- /** get number of instantiation constants for q */
- unsigned getNumInstantiationConstants( Node q ) const;
- /** get the ce body q[e/x] */
- Node getInstConstantBody( Node q );
- /** returns node n with bound vars of q replaced by instantiation constants of q
- node n : is the future pattern
- node q : is the quantifier containing which bind the variable
- return a pattern where the variable are replaced by variable for
- instantiation.
- */
- Node substituteBoundVariablesToInstConstants(Node n, Node q);
- /** substitute { instantiation constants of q -> bound variables of q } in n
- */
- Node substituteInstConstantsToBoundVariables(Node n, Node q);
- /** substitute { variables of q -> terms } in n */
- Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms);
- /** substitute { instantiation constants of q -> terms } in n */
- Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms);
+ public:
+ /** Get the index of BOUND_VARIABLE v in quantifier q */
+ static size_t getVariableNum(Node q, Node v);
static Node getInstConstAttr( Node n );
static bool hasInstConstAttr( Node n );
d_model(nullptr),
d_builder(nullptr),
d_term_util(new quantifiers::TermUtil),
- d_term_db(new quantifiers::TermDb(qstate, qim, this)),
+ d_term_db(new quantifiers::TermDb(qstate, qim, d_qreg, this)),
d_eq_query(nullptr),
d_sygus_tdb(nullptr),
d_quant_attr(new quantifiers::QuantAttributes),
- d_instantiate(new quantifiers::Instantiate(this, qstate, qim, pnm)),
+ d_instantiate(
+ new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
d_skolemize(new quantifiers::Skolemize(this, qstate, pnm)),
d_term_enum(new quantifiers::TermEnumeration),
d_quants_prereg(qstate.getUserContext()),
d_presolve_cache(qstate.getUserContext())
{
//---- utilities
- // term util must come before the other utilities
- d_util.push_back(d_term_util.get());
+ // quantifiers registry must come before the other utilities
+ d_util.push_back(&d_qreg);
d_util.push_back(d_term_db.get());
if (options::sygus() || options::sygusInst())
{
Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
- this, qstate, "FirstOrderModelFmc"));
+ this, qstate, d_qreg, "FirstOrderModelFmc"));
d_builder.reset(new quantifiers::fmcheck::FullModelChecker(this, qstate));
}else{
Trace("quant-engine-debug") << "...make default model builder." << std::endl;
- d_model.reset(
- new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
+ d_model.reset(new quantifiers::FirstOrderModel(
+ this, qstate, d_qreg, "FirstOrderModel"));
d_builder.reset(new quantifiers::QModelBuilder(this, qstate));
}
}else{
- d_model.reset(
- new quantifiers::FirstOrderModel(this, qstate, "FirstOrderModel"));
+ d_model.reset(new quantifiers::FirstOrderModel(
+ this, qstate, d_qreg, "FirstOrderModel"));
}
d_eq_query.reset(new quantifiers::EqualityQueryQuantifiersEngine(
qstate, d_term_db.get(), d_model.get()));
{
return d_qim;
}
+
+quantifiers::QuantifiersRegistry& QuantifiersEngine::getQuantifiersRegistry()
+{
+ return d_qreg;
+}
+
quantifiers::QModelBuilder* QuantifiersEngine::getModelBuilder() const
{
return d_builder.get();
{
mdl->assertNode(f);
}
- addTermToDatabase(d_term_util->getInstConstantBody(f), true);
+ addTermToDatabase(d_qreg.getInstConstantBody(f), true);
}
void QuantifiersEngine::addTermToDatabase(Node n, bool withinQuant)
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/fmf/model_builder.h"
#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/quant_module.h"
#include "theory/quantifiers/quant_util.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/quantifiers_inference_manager.h"
quantifiers::QuantifiersState& getState();
/** The quantifiers inference manager */
quantifiers::QuantifiersInferenceManager& getInferenceManager();
+ /** The quantifiers registry */
+ quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
//---------------------- end external interface
//---------------------- utilities
/** get the model builder */
projects / cvc5.git / commitdiff