summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/quantifiers/first_order_model.cpp34
-rw-r--r--src/theory/quantifiers/first_order_model.h31
-rw-r--r--src/theory/quantifiers/fmf/first_order_model_fmc.cpp6
-rw-r--r--src/theory/quantifiers/fmf/first_order_model_fmc.h7
-rw-r--r--src/theory/quantifiers/fmf/full_model_check.cpp17
-rw-r--r--src/theory/quantifiers/fmf/full_model_check.h4
-rw-r--r--src/theory/quantifiers/fmf/model_builder.cpp6
-rw-r--r--src/theory/quantifiers/fmf/model_builder.h10
-rw-r--r--src/theory/quantifiers_engine.cpp21
-rw-r--r--src/theory/uf/theory_uf_model.cpp6
10 files changed, 80 insertions, 62 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 44c42b305..001c2f62a 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -20,8 +20,8 @@
#include "theory/quantifiers/quantifiers_attributes.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"
using namespace std;
using namespace CVC4::kind;
@@ -32,18 +32,33 @@ namespace CVC4 {
namespace theory {
namespace quantifiers {
-FirstOrderModel::FirstOrderModel(QuantifiersEngine* qe,
- QuantifiersState& qs,
+struct ModelBasisAttributeId
+{
+};
+using ModelBasisAttribute = expr::Attribute<ModelBasisAttributeId, bool>;
+// for APPLY_UF terms, 1 : term has direct child with model basis attribute,
+// 0 : term has no direct child with model basis attribute.
+struct ModelBasisArgAttributeId
+{
+};
+using ModelBasisArgAttribute = expr::Attribute<ModelBasisArgAttributeId, uint64_t>;
+
+FirstOrderModel::FirstOrderModel(QuantifiersState& qs,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
std::string name)
: TheoryModel(qs.getSatContext(), name, true),
- d_qe(qe),
+ d_qe(nullptr),
d_qreg(qr),
+ d_treg(tr),
d_forall_asserts(qs.getSatContext()),
d_forallRlvComputed(false)
{
}
+//!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
+void FirstOrderModel::finishInit(QuantifiersEngine* qe) { d_qe = qe; }
+
void FirstOrderModel::assertQuantifier( Node n ){
if( n.getKind()==FORALL ){
d_forall_asserts.push_back( n );
@@ -143,6 +158,11 @@ bool FirstOrderModel::initializeRepresentativesForType(TypeNode tn)
}
}
+bool FirstOrderModel::isModelBasis(TNode n)
+{
+ return n.getAttribute(ModelBasisAttribute());
+}
+
/** needs check */
bool FirstOrderModel::checkNeeded() {
return d_forall_asserts.size()>0;
@@ -237,13 +257,13 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
Node mbt;
if (tn.isClosedEnumerable())
{
- mbt = d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
+ mbt = d_treg.getTermEnumeration()->getEnumerateTerm(tn, 0);
}
else
{
if (options::fmfFreshDistConst())
{
- mbt = d_qe->getTermDatabase()->getOrMakeTypeFreshVariable(tn);
+ mbt = d_treg.getTermDatabase()->getOrMakeTypeFreshVariable(tn);
}
else
{
@@ -251,7 +271,7 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
// may produce an inconsistent model by choosing an arbitrary
// equivalence class for it. Hence, we require that it be an existing or
// fresh variable.
- mbt = d_qe->getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
+ mbt = d_treg.getTermDatabase()->getOrMakeTypeGroundTerm(tn, true);
}
}
ModelBasisAttribute mba;
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 484d7738a..c2660d933 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -27,22 +27,10 @@ namespace theory {
class QuantifiersEngine;
-struct ModelBasisAttributeId
-{
-};
-typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
-// for APPLY_UF terms, 1 : term has direct child with model basis attribute,
-// 0 : term has no direct child with model basis attribute.
-struct ModelBasisArgAttributeId
-{
-};
-typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t>
- ModelBasisArgAttribute;
-
namespace quantifiers {
-class TermDb;
class QuantifiersState;
+class TermRegistry;
class QuantifiersRegistry;
namespace fmcheck {
@@ -56,12 +44,15 @@ typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
class FirstOrderModel : public TheoryModel
{
public:
- FirstOrderModel(QuantifiersEngine* qe,
- QuantifiersState& qs,
+ FirstOrderModel(QuantifiersState& qs,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
std::string name);
- virtual fmcheck::FirstOrderModelFmc* asFirstOrderModelFmc() { return nullptr; }
+ //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
+ /** finish initialize */
+ void finishInit(QuantifiersEngine* qe);
+
/** assert quantifier */
void assertQuantifier( Node n );
/** get number of asserted quantifiers */
@@ -132,12 +123,18 @@ class FirstOrderModel : public TheoryModel
* has all representatives of type tn.
*/
bool initializeRepresentativesForType(TypeNode tn);
+ /**
+ * Has the term been marked as a model basis term?
+ */
+ static bool isModelBasis(TNode n);
protected:
- /** quant engine */
+ //!!!!!!!!!!!!!!!!!!!!!!! TODO (project #15): temporarily available
QuantifiersEngine* d_qe;
/** The quantifiers registry */
QuantifiersRegistry& d_qreg;
+ /** Reference to the term registry */
+ TermRegistry& d_treg;
/** list of quantifiers asserted in the current context */
context::CDList<Node> d_forall_asserts;
/**
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
index 5ce5eecfc..252261b9c 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.cpp
@@ -24,11 +24,11 @@ namespace theory {
namespace quantifiers {
namespace fmcheck {
-FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine* qe,
- QuantifiersState& qs,
+FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersState& qs,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
std::string name)
- : FirstOrderModel(qe, qs, qr, name)
+ : FirstOrderModel(qs, qr, tr, name)
{
}
diff --git a/src/theory/quantifiers/fmf/first_order_model_fmc.h b/src/theory/quantifiers/fmf/first_order_model_fmc.h
index 8f371a96b..d8ae054ad 100644
--- a/src/theory/quantifiers/fmf/first_order_model_fmc.h
+++ b/src/theory/quantifiers/fmf/first_order_model_fmc.h
@@ -38,17 +38,16 @@ class FirstOrderModelFmc : public FirstOrderModel
void processInitializeModelForTerm(Node n) override;
public:
- FirstOrderModelFmc(QuantifiersEngine* qe,
- QuantifiersState& qs,
+ FirstOrderModelFmc(QuantifiersState& qs,
QuantifiersRegistry& qr,
+ TermRegistry& tr,
std::string name);
~FirstOrderModelFmc() override;
- FirstOrderModelFmc* asFirstOrderModelFmc() override { return this; }
// initialize the model
void processInitialize(bool ispre) override;
Node getFunctionValue(Node op, const char* argPrefix);
- bool isStar(Node n);
+ static bool isStar(Node n);
Node getStar(TypeNode tn);
}; /* class FirstOrderModelFmc */
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index abcd5a794..be83f3b10 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -284,10 +284,9 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
}
}
-FullModelChecker::FullModelChecker(QuantifiersEngine* qe,
- QuantifiersState& qs,
+FullModelChecker::FullModelChecker(QuantifiersState& qs,
QuantifiersRegistry& qr)
- : QModelBuilder(qe, qs, qr)
+ : QModelBuilder(qs, qr)
{
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
@@ -298,8 +297,8 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
if( !preProcessBuildModelStd( m ) ){
return false;
}
-
- FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
+
+ FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m;
Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
d_preinitialized_eqc.clear();
d_preinitialized_types.clear();
@@ -346,7 +345,7 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){
// nothing to do if no functions
return true;
}
- FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
+ FirstOrderModelFmc* fm = (FirstOrderModelFmc*)m;
Trace("fmc") << "---Full Model Check reset() " << std::endl;
d_quant_models.clear();
d_rep_ids.clear();
@@ -573,11 +572,11 @@ void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {
}
void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
- FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel();
if( n.isNull() ){
Trace(tr) << "null";
}
- else if(fm->isStar(n) && dispStar) {
+ else if (FirstOrderModelFmc::isStar(n) && dispStar)
+ {
Trace(tr) << "*";
}
else
@@ -607,7 +606,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
{
return 0;
}
- FirstOrderModelFmc* fmfmc = fm->asFirstOrderModelFmc();
+ FirstOrderModelFmc* fmfmc = static_cast<FirstOrderModelFmc*>(fm);
if (effort == 0)
{
if (options::mbqiMode() == options::MbqiMode::NONE)
diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h
index b3c55ee7a..904a1b9a0 100644
--- a/src/theory/quantifiers/fmf/full_model_check.h
+++ b/src/theory/quantifiers/fmf/full_model_check.h
@@ -154,9 +154,7 @@ protected:
Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
public:
- FullModelChecker(QuantifiersEngine* qe,
- QuantifiersState& qs,
- QuantifiersRegistry& qr);
+ FullModelChecker(QuantifiersState& qs, QuantifiersRegistry& qr);
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 89e4fa29d..9aa687fbd 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -30,13 +30,11 @@ using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-QModelBuilder::QModelBuilder(QuantifiersEngine* qe,
- QuantifiersState& qs,
- QuantifiersRegistry& qr)
+QModelBuilder::QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr)
: TheoryEngineModelBuilder(),
- d_qe(qe),
d_addedLemmas(0),
d_triedLemmas(0),
+ d_qe(nullptr),
d_qstate(qs),
d_qreg(qr)
{
diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h
index 534226a7c..7ba7a66e2 100644
--- a/src/theory/quantifiers/fmf/model_builder.h
+++ b/src/theory/quantifiers/fmf/model_builder.h
@@ -32,8 +32,6 @@ class QuantifiersRegistry;
class QModelBuilder : public TheoryEngineModelBuilder
{
protected:
- //quantifiers engine
- QuantifiersEngine* d_qe;
// must call preProcessBuildModelStd
bool preProcessBuildModel(TheoryModel* m) override;
bool preProcessBuildModelStd(TheoryModel* m);
@@ -42,9 +40,9 @@ class QModelBuilder : public TheoryEngineModelBuilder
unsigned d_triedLemmas;
public:
- QModelBuilder(QuantifiersEngine* qe,
- QuantifiersState& qs,
- QuantifiersRegistry& qr);
+ QModelBuilder(QuantifiersState& qs, QuantifiersRegistry& qr);
+ //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
+ void finishInit(QuantifiersEngine* qe) { d_qe = qe; }
//do exhaustive instantiation
// 0 : failed, but resorting to true exhaustive instantiation may work
@@ -62,6 +60,8 @@ class QModelBuilder : public TheoryEngineModelBuilder
unsigned getNumTriedLemmas() { return d_triedLemmas; }
protected:
+ /** Pointer to quantifiers engine */
+ QuantifiersEngine* d_qe;
/** The quantifiers state object */
QuantifiersState& d_qstate;
/** Reference to the quantifiers registry */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 1784b976e..d6aaeed3f 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -72,7 +72,7 @@ QuantifiersEngine::QuantifiersEngine(
//---- utilities
// quantifiers registry must come before the other utilities
d_util.push_back(&d_qreg);
- d_util.push_back(d_treg.getTermDatabase());
+ d_util.push_back(tr.getTermDatabase());
d_util.push_back(d_instantiate.get());
@@ -93,19 +93,22 @@ QuantifiersEngine::QuantifiersEngine(
{
Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
d_model.reset(new quantifiers::fmcheck::FirstOrderModelFmc(
- this, qstate, qr, "FirstOrderModelFmc"));
- d_builder.reset(
- new quantifiers::fmcheck::FullModelChecker(this, qstate, qr));
+ qstate, qr, tr, "FirstOrderModelFmc"));
+ d_builder.reset(new quantifiers::fmcheck::FullModelChecker(qstate, qr));
}else{
Trace("quant-engine-debug") << "...make default model builder." << std::endl;
- d_model.reset(new quantifiers::FirstOrderModel(
- this, qstate, qr, "FirstOrderModel"));
- d_builder.reset(new quantifiers::QModelBuilder(this, qstate, qr));
+ d_model.reset(
+ new quantifiers::FirstOrderModel(qstate, qr, tr, "FirstOrderModel"));
+ d_builder.reset(new quantifiers::QModelBuilder(qstate, qr));
}
+ d_builder->finishInit(this);
}else{
- d_model.reset(new quantifiers::FirstOrderModel(
- this, qstate, d_qreg, "FirstOrderModel"));
+ d_model.reset(
+ new quantifiers::FirstOrderModel(qstate, qr, tr, "FirstOrderModel"));
}
+ //!!!!!!!!!!!!!!!!!!!!! temporary (project #15)
+ d_model->finishInit(this);
+ // initialize the equality query
d_eq_query.reset(
new quantifiers::EqualityQueryQuantifiersEngine(qstate, d_model.get()));
d_util.insert(d_util.begin(), d_eq_query.get());
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 393f1f705..abb0c2e6c 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -45,7 +45,11 @@ void UfModelTreeNode::setValue( TheoryModel* m, Node n, Node v, std::vector< int
if( argIndex<(int)indexOrder.size() ){
//take r = null when argument is the model basis
Node r;
- if( ground || ( !n.isNull() && !n[ indexOrder[argIndex] ].getAttribute(ModelBasisAttribute()) ) ){
+ if (ground
+ || (!n.isNull()
+ && !quantifiers::FirstOrderModel::isModelBasis(
+ n[indexOrder[argIndex]])))
+ {
r = m->getRepresentative( n[ indexOrder[argIndex] ] );
}
d_data[ r ].setValue( m, n, v, indexOrder, ground, argIndex+1 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback