After this PR, utilities for instantiation are available from the quantifiers inference manager instead of quantifiers engine. This means that the majority of the dependencies on quantifiers engine will (finally) start being cleaned up after this PR.
#include "theory/quantifiers/quantifiers_rewriter.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/term_enumeration.h"
+#include "theory/quantifiers/term_registry.h"
#include "theory/quantifiers/term_util.h"
#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
namespace theory {
namespace quantifiers {
-Instantiate::Instantiate(QuantifiersEngine* qe,
- QuantifiersState& qs,
+Instantiate::Instantiate(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
+ FirstOrderModel* m,
ProofNodeManager* pnm)
- : d_qe(qe),
- d_qstate(qs),
+ : d_qstate(qs),
d_qim(qim),
d_qreg(qr),
+ d_treg(tr),
+ d_model(m),
d_pnm(pnm),
- d_term_db(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();
return true;
}
d_qim.safePoint(ResourceManager::Resource::QuantifierStep);
Assert(!d_qstate.isInConflict());
Assert(terms.size() == q[0].getNumChildren());
- Assert(d_term_db != nullptr);
Trace("inst-add-debug") << "For quantified formula " << q
<< ", add instantiation: " << std::endl;
for (unsigned i = 0, size = terms.size(); i < size; i++)
{
// pick the best possible representative for instantiation, based on past
// use and simplicity of term
- terms[i] = d_qe->getModel()->getInternalRepresentative(terms[i], q, i);
+ terms[i] = d_model->getInternalRepresentative(terms[i], q, i);
}
Trace("inst-add-debug") << " -> " << terms[i] << std::endl;
if (terms[i].isNull())
#endif
}
+ TermDb* tdb = d_treg.getTermDatabase();
// Note we check for entailment before checking for term vector duplication.
// Although checking for term vector duplication is a faster check, it is
// included automatically with recordInstantiationInternal, hence we prefer
{
subs[q[0][i]] = terms[i];
}
- if (d_term_db->isEntailed(q[1], subs, false, true))
+ if (tdb->isEntailed(q[1], subs, false, true))
{
Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
++(d_statistics.d_inst_duplicate_ent);
{
for (Node& t : terms)
{
- if (!d_term_db->isTermEligibleForInstantiation(t, q))
+ if (!tdb->isTermEligibleForInstantiation(t, q))
{
return false;
}
// will never succeed with 1 variable
return false;
}
+ TermDb* tdb = d_treg.getTermDatabase();
Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl;
// set up information for below
std::vector<Node>& vars = d_qreg.d_vars[q];
if (options::instNoEntail())
{
Trace("inst-exp-fail") << " check entailment" << std::endl;
- success = d_term_db->isEntailed(q[1], subs, false, true);
+ success = tdb->isEntailed(q[1], subs, false, true);
Trace("inst-exp-fail") << " entailed: " << success << std::endl;
}
// check whether the instantiation rewrites to the same thing
{
if (tn.isClosedEnumerable())
{
- return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
+ return d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0);
}
- return d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn);
+ return d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn);
}
void Instantiate::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
for (std::pair<const Node, uint32_t>& i : d_temp_inst_debug)
{
Node name;
- if (!d_qe->getNameForQuant(i.first, name, req))
+ if (!d_qreg.getNameForQuant(i.first, name, req))
{
continue;
}
class LazyCDProof;
namespace theory {
-
-class QuantifiersEngine;
-
namespace quantifiers {
-class TermDb;
+class TermRegistry;
class QuantifiersState;
class QuantifiersInferenceManager;
class QuantifiersRegistry;
+class FirstOrderModel;
/** Instantiation rewriter
*
typedef context::CDHashMap<Node, uint32_t, NodeHashFunction> NodeUIntMap;
public:
- Instantiate(QuantifiersEngine* qe,
- QuantifiersState& qs,
+ Instantiate(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
+ FirstOrderModel* m,
ProofNodeManager* pnm = nullptr);
~Instantiate();
*/
static Node ensureType(Node n, TypeNode tn);
- /** pointer to the quantifiers engine */
- QuantifiersEngine* d_qe;
/** Reference to the quantifiers state */
QuantifiersState& d_qstate;
/** Reference to the quantifiers inference manager */
QuantifiersInferenceManager& d_qim;
/** The quantifiers registry */
QuantifiersRegistry& d_qreg;
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
+ /** Pointer to the model */
+ FirstOrderModel* d_model;
/** pointer to the proof node manager */
ProofNodeManager* d_pnm;
- /** cache of term database for quantifiers engine */
- TermDb* d_term_db;
/** instantiation rewriter classes */
std::vector<InstantiationRewriter*> d_instRewrite;
#include "theory/quantifiers/quantifiers_inference_manager.h"
+#include "theory/quantifiers/instantiate.h"
+#include "theory/quantifiers/skolemize.h"
+
namespace CVC4 {
namespace theory {
namespace quantifiers {
QuantifiersInferenceManager::QuantifiersInferenceManager(
- Theory& t, QuantifiersState& state, ProofNodeManager* pnm)
- : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers")
+ Theory& t,
+ QuantifiersState& state,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr,
+ FirstOrderModel* m,
+ ProofNodeManager* pnm)
+ : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"),
+ d_instantiate(new Instantiate(state, *this, qr, tr, m, pnm)),
+ d_skolemize(new Skolemize(state, pnm))
{
}
QuantifiersInferenceManager::~QuantifiersInferenceManager() {}
+Instantiate* QuantifiersInferenceManager::getInstantiate()
+{
+ return d_instantiate.get();
+}
+
+Skolemize* QuantifiersInferenceManager::getSkolemize()
+{
+ return d_skolemize.get();
+}
+
void QuantifiersInferenceManager::doPending()
{
doPendingLemmas();
namespace theory {
namespace quantifiers {
+class Instantiate;
+class Skolemize;
+class QuantifiersRegistry;
+class TermRegistry;
+class FirstOrderModel;
/**
* The quantifiers inference manager.
*/
public:
QuantifiersInferenceManager(Theory& t,
QuantifiersState& state,
+ QuantifiersRegistry& qr,
+ TermRegistry& tr,
+ FirstOrderModel* m,
ProofNodeManager* pnm);
~QuantifiersInferenceManager();
+ /** get instantiate utility */
+ Instantiate* getInstantiate();
+ /** get skolemize utility */
+ Skolemize* getSkolemize();
/**
* Do all pending lemmas, then do all pending phase requirements.
*/
void doPending();
+
+ private:
+ /** instantiate utility */
+ std::unique_ptr<Instantiate> d_instantiate;
+ /** skolemize utility */
+ std::unique_ptr<Skolemize> d_skolemize;
};
} // namespace quantifiers
d_qstate(c, u, valuation, logicInfo),
d_qreg(),
d_treg(d_qstate, d_qreg),
- d_qim(*this, d_qstate, pnm)
+ d_qim(nullptr),
+ d_qengine(nullptr)
{
- // 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);
-
out.handleUserAttribute( "fun-def", this );
out.handleUserAttribute("qid", this);
out.handleUserAttribute( "quant-inst-max-level", this );
// add the proof rules
d_qChecker.registerTo(pc);
}
- // 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;
Trace("quant-engine-debug") << "Initialize quantifiers engine." << std::endl;
Trace("quant-engine-debug")
// Finite model finding requires specialized ways of building the model.
// We require constructing the model here, since it is required for
// initializing the CombinationEngine and the rest of quantifiers engine.
- if (options::finiteModelFind() || options::fmfBound())
+ if ((options::finiteModelFind() || options::fmfBound())
+ && QuantifiersModules::useFmcModel())
{
- if (QuantifiersModules::useFmcModel())
- {
- d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
- d_qstate, d_qreg, d_treg, "FirstOrderModelFmc"));
- }
- else
- {
- d_qmodel.reset(new quantifiers::FirstOrderModel(
- d_qstate, d_qreg, d_treg, "FirstOrderModel"));
- }
+ d_qmodel.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
+ d_qstate, d_qreg, d_treg, "FirstOrderModelFmc"));
}
else
{
d_qstate, d_qreg, d_treg, "FirstOrderModel"));
}
+ d_qim.reset(new QuantifiersInferenceManager(
+ *this, d_qstate, d_qreg, d_treg, d_qmodel.get(), pnm));
+
+ // 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.get());
+
// construct the quantifiers engine
d_qengine.reset(new QuantifiersEngine(
- d_qstate, d_qreg, d_treg, d_qim, d_qmodel.get(), pnm));
+ d_qstate, d_qreg, d_treg, *d_qim.get(), d_qmodel.get(), pnm));
//!!!!!!!!!!!!!! temporary (project #15)
d_qmodel->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.get();
// 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.
/** The term registry */
TermRegistry d_treg;
/** The quantifiers inference manager */
- QuantifiersInferenceManager d_qim;
+ std::unique_ptr<QuantifiersInferenceManager> d_qim;
/** The quantifiers engine, which lives here */
std::unique_ptr<QuantifiersEngine> d_qengine;
};/* class TheoryQuantifiers */
d_treg(tr),
d_tr_trie(new inst::TriggerTrie),
d_model(qm),
- d_instantiate(
- new quantifiers::Instantiate(this, qstate, qim, d_qreg, pnm)),
- d_skolemize(new quantifiers::Skolemize(d_qstate, d_pnm)),
d_quants_prereg(qstate.getUserContext()),
d_quants_red(qstate.getUserContext())
{
// quantifiers registry must come before the remaining utilities
d_util.push_back(&d_qreg);
d_util.push_back(tr.getTermDatabase());
- d_util.push_back(d_instantiate.get());
+ d_util.push_back(qim.getInstantiate());
}
QuantifiersEngine::~QuantifiersEngine() {}
{
return d_model;
}
+
+/// !!!!!!!!!!!!!! temporary (project #15)
+
quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
{
return d_treg.getTermDatabase();
}
quantifiers::Instantiate* QuantifiersEngine::getInstantiate() const
{
- return d_instantiate.get();
+ return d_qim.getInstantiate();
}
quantifiers::Skolemize* QuantifiersEngine::getSkolemize() const
{
- return d_skolemize.get();
+ return d_qim.getSkolemize();
}
inst::TriggerTrie* QuantifiersEngine::getTriggerDatabase() const
{
return d_tr_trie.get();
}
+/// !!!!!!!!!!!!!!
void QuantifiersEngine::presolve() {
Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
{
Options& sopts = smt::currentSmtEngine()->getOptions();
std::ostream& out = *sopts.getOut();
- d_instantiate->debugPrint(out);
+ d_qim.getInstantiate()->debugPrint(out);
}
}
if( Trace.isOn("quant-engine") ){
d_qim.setIncomplete();
}
//output debug stats
- d_instantiate->debugPrintModel();
+ d_qim.getInstantiate()->debugPrintModel();
}
}
}
if( !pol ){
// do skolemization
- TrustNode lem = d_skolemize->process(f);
+ TrustNode lem = d_qim.getSkolemize()->process(f);
if (!lem.isNull())
{
if (Trace.isOn("quantifiers-sk-debug"))
}
void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
- d_instantiate->getInstantiationTermVectors(q, tvecs);
+ d_qim.getInstantiate()->getInstantiationTermVectors(q, tvecs);
}
void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
- d_instantiate->getInstantiationTermVectors(insts);
+ d_qim.getInstantiate()->getInstantiationTermVectors(insts);
}
void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
void QuantifiersEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
{
- d_instantiate->getInstantiatedQuantifiedFormulas(qs);
+ d_qim.getInstantiate()->getInstantiatedQuantifiedFormulas(qs);
}
void QuantifiersEngine::getSkolemTermVectors(
std::map<Node, std::vector<Node> >& sks) const
{
- d_skolemize->getSkolemTermVectors(sks);
+ d_qim.getSkolemize()->getSkolemTermVectors(sks);
}
QuantifiersEngine::Statistics::Statistics()
std::unique_ptr<inst::TriggerTrie> d_tr_trie;
/** extended model object */
quantifiers::FirstOrderModel* d_model;
- /** instantiate utility */
- std::unique_ptr<quantifiers::Instantiate> d_instantiate;
- /** skolemize utility */
- std::unique_ptr<quantifiers::Skolemize> d_skolemize;
//------------- end quantifiers utilities
/**
* The modules utility, which contains all of the quantifiers modules.
projects / cvc5.git / commitdiff