summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/quantifiers/instantiate.cpp30
-rw-r--r--src/theory/quantifiers/instantiate.h19
-rw-r--r--src/theory/quantifiers/quantifiers_inference_manager.cpp24
-rw-r--r--src/theory/quantifiers/quantifiers_inference_manager.h18
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp45
-rw-r--r--src/theory/quantifiers/theory_quantifiers.h2
-rw-r--r--src/theory/quantifiers_engine.cpp27
-rw-r--r--src/theory/quantifiers_engine.h4
8 files changed, 101 insertions, 68 deletions
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index be6101b81..fd74e17e8 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -29,6 +29,7 @@
#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"
@@ -40,17 +41,18 @@ namespace CVC4 {
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)
@@ -79,7 +81,6 @@ bool Instantiate::reset(Theory::Effort e)
}
d_recorded_inst.clear();
}
- d_term_db = d_qe->getTermDatabase();
return true;
}
@@ -111,7 +112,6 @@ bool Instantiate::addInstantiation(Node q,
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++)
@@ -131,7 +131,7 @@ bool Instantiate::addInstantiation(Node q,
{
// 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())
@@ -188,6 +188,7 @@ bool Instantiate::addInstantiation(Node q,
#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
@@ -210,7 +211,7 @@ bool Instantiate::addInstantiation(Node q,
{
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);
@@ -223,7 +224,7 @@ bool Instantiate::addInstantiation(Node q,
{
for (Node& t : terms)
{
- if (!d_term_db->isTermEligibleForInstantiation(t, q))
+ if (!tdb->isTermEligibleForInstantiation(t, q))
{
return false;
}
@@ -408,6 +409,7 @@ bool Instantiate::addInstantiationExpFail(Node q,
// 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];
@@ -441,7 +443,7 @@ bool Instantiate::addInstantiationExpFail(Node 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
@@ -615,9 +617,9 @@ Node Instantiate::getTermForType(TypeNode tn)
{
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)
@@ -704,7 +706,7 @@ void Instantiate::debugPrint(std::ostream& out)
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;
}
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index abdee69ef..8e556b648 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -32,15 +32,13 @@ namespace CVC4 {
class LazyCDProof;
namespace theory {
-
-class QuantifiersEngine;
-
namespace quantifiers {
-class TermDb;
+class TermRegistry;
class QuantifiersState;
class QuantifiersInferenceManager;
class QuantifiersRegistry;
+class FirstOrderModel;
/** Instantiation rewriter
*
@@ -95,10 +93,11 @@ class Instantiate : public QuantifiersUtil
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();
@@ -311,18 +310,18 @@ class Instantiate : public QuantifiersUtil
*/
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;
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index 8469720c4..9a82265f9 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -14,18 +14,38 @@
#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();
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.h b/src/theory/quantifiers/quantifiers_inference_manager.h
index 76b7d0982..aa7fc1b6a 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.h
+++ b/src/theory/quantifiers/quantifiers_inference_manager.h
@@ -24,6 +24,11 @@ namespace CVC4 {
namespace theory {
namespace quantifiers {
+class Instantiate;
+class Skolemize;
+class QuantifiersRegistry;
+class TermRegistry;
+class FirstOrderModel;
/**
* The quantifiers inference manager.
*/
@@ -32,12 +37,25 @@ class QuantifiersInferenceManager : public InferenceManagerBuffered
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
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 5bcc80eb0..092689b5f 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -41,15 +41,9 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
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 );
@@ -62,10 +56,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
// 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")
@@ -73,18 +63,11 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
// 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
{
@@ -92,13 +75,27 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c,
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.
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 9714ec718..2371b00ce 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -94,7 +94,7 @@ class TheoryQuantifiers : public Theory {
/** 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 */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 68962de72..9ca8226bc 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -62,9 +62,6 @@ QuantifiersEngine::QuantifiersEngine(
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())
{
@@ -73,7 +70,7 @@ QuantifiersEngine::QuantifiersEngine(
// 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() {}
@@ -125,6 +122,9 @@ quantifiers::FirstOrderModel* QuantifiersEngine::getModel() const
{
return d_model;
}
+
+/// !!!!!!!!!!!!!! temporary (project #15)
+
quantifiers::TermDb* QuantifiersEngine::getTermDatabase() const
{
return d_treg.getTermDatabase();
@@ -139,16 +139,17 @@ quantifiers::TermEnumeration* QuantifiersEngine::getTermEnumeration() const
}
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;
@@ -468,7 +469,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
{
Options& sopts = smt::currentSmtEngine()->getOptions();
std::ostream& out = *sopts.getOut();
- d_instantiate->debugPrint(out);
+ d_qim.getInstantiate()->debugPrint(out);
}
}
if( Trace.isOn("quant-engine") ){
@@ -491,7 +492,7 @@ void QuantifiersEngine::check( Theory::Effort e ){
d_qim.setIncomplete();
}
//output debug stats
- d_instantiate->debugPrintModel();
+ d_qim.getInstantiate()->debugPrintModel();
}
}
@@ -611,7 +612,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){
}
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"))
@@ -645,11 +646,11 @@ void QuantifiersEngine::markRelevant( Node q ) {
}
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 ) {
@@ -663,13 +664,13 @@ 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()
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 4d3029ca9..b6562caa7 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -237,10 +237,6 @@ public:
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback