summaryrefslogtreecommitdiff
path: root/src/theory/arrays
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays')
-rw-r--r--src/theory/arrays/Makefile.am4
-rw-r--r--src/theory/arrays/kinds1
-rw-r--r--src/theory/arrays/theory_arrays.cpp9
-rw-r--r--src/theory/arrays/theory_arrays.h42
-rw-r--r--src/theory/arrays/theory_arrays_instantiator.cpp56
-rw-r--r--src/theory/arrays/theory_arrays_instantiator.h51
6 files changed, 149 insertions, 14 deletions
diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am
index 3dde70145..57c55d765 100644
--- a/src/theory/arrays/Makefile.am
+++ b/src/theory/arrays/Makefile.am
@@ -15,6 +15,8 @@ libarrays_la_SOURCES = \
array_info.h \
array_info.cpp \
static_fact_manager.h \
- static_fact_manager.cpp
+ static_fact_manager.cpp \
+ theory_arrays_instantiator.h \
+ theory_arrays_instantiator.cpp
EXTRA_DIST = kinds
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 06240a315..195a60035 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -6,6 +6,7 @@
theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h"
typechecker "theory/arrays/theory_arrays_type_rules.h"
+instantiator ::CVC4::theory::arrays::InstantiatorTheoryArrays "theory/arrays/theory_arrays_instantiator.h"
properties polite stable-infinite parametric
properties check propagate presolve
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 81661acd1..376a7e90f 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -23,6 +23,7 @@
#include <map>
#include "theory/rewriter.h"
#include "expr/command.h"
+#include "theory/arrays/theory_arrays_instantiator.h"
using namespace std;
@@ -45,8 +46,8 @@ const bool d_solveWrite2 = false;
const bool d_useNonLinearOpt = true;
const bool d_eagerIndexSplitting = true;
-TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
- Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo),
+TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
+ Theory(THEORY_ARRAY, c, u, out, valuation, logicInfo, qe),
d_numRow("theory::arrays::number of Row lemmas", 0),
d_numExt("theory::arrays::number of Ext lemmas", 0),
d_numProp("theory::arrays::number of propagations", 0),
@@ -218,7 +219,7 @@ Node TheoryArrays::ppRewrite(TNode term) {
}
Node r1 = nm->mkNode(kind::SELECT, e1, index_i);
- conc = (r1.getType() == nm->booleanType())?
+ conc = (r1.getType() == nm->booleanType())?
r1.iffNode(write_i[2]) : r1.eqNode(write_i[2]);
if (hyp.getNumChildren() != 0) {
if (hyp.getNumChildren() == 1) {
@@ -582,7 +583,6 @@ void TheoryArrays::computeCareGraph()
// Get representative trigger terms
TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_ARRAY);
TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_ARRAY);
-
EqualityStatus eqStatusDomain = d_valuation.getEqualityStatus(x_shared, y_shared);
switch (eqStatusDomain) {
case EQUALITY_TRUE_AND_PROPAGATED:
@@ -605,6 +605,7 @@ void TheoryArrays::computeCareGraph()
break;
}
+
// Otherwise, add this pair
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): adding to care-graph" << std::endl;
addCarePair(x_shared, y_shared);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 80fe692c0..1bf42a105 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -39,32 +39,32 @@ namespace arrays {
* Overview of decision procedure:
*
* Preliminary notation:
- * Stores(a) = {t | a ~ t and t = store( _ _ _ )}
+ * Stores(a) = {t | a ~ t and t = store( _ _ _ )}
* InStores(a) = {t | t = store (b _ _) and a ~ b }
* Indices(a) = {i | there exists a term b[i] such that a ~ b or store(b i v)}
* ~ represents the equivalence relation based on the asserted equalities in the
* current context.
- *
+ *
* The rules implemented are the following:
* store(b i v)
* Row1 -------------------
* store(b i v)[i] = v
- *
+ *
* store(b i v) a'[j]
* Row ---------------------- [ a' ~ store(b i v) or a' ~ b ]
* i = j OR a[j] = b[j]
- *
+ *
* a b same kind arrays
* Ext ------------------------ [ a!= b in current context, k new var]
* a = b OR a[k] != b[k]p
- *
- *
+ *
+ *
* The Row1 one rule is implemented implicitly as follows:
* - for each store(b i v) term add the following equality to the congruence
* closure store(b i v)[i] = v
* - if one of the literals in a conflict is of the form store(b i v)[i] = v
* remove it from the conflict
- *
+ *
* Because new store terms are not created, we need to check if we need to
* instantiate a new Row axiom in the following cases:
* 1. the congruence relation changes (i.e. two terms get merged)
@@ -77,7 +77,7 @@ namespace arrays {
* - this is implemented in the checkRowForIndex method which is called
* when preregistering a term of the form a[i].
* - as a consequence lemmas are instantiated even before full effort check
- *
+ *
* The Ext axiom is instantiated when a disequality is asserted during full effort
* check. Ext lemmas are stored in a cache to prevent instantiating essentially
* the same lemma multiple times.
@@ -122,7 +122,7 @@ class TheoryArrays : public Theory {
public:
- TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
+ TheoryArrays(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
~TheoryArrays();
std::string identify() const { return std::string("TheoryArrays"); }
@@ -133,6 +133,16 @@ class TheoryArrays : public Theory {
private:
+ // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used
+ class PPNotifyClass {
+ public:
+ bool notify(TNode propagation) { return true; }
+ void notify(TNode t1, TNode t2) { }
+ };
+
+ /** The notify class for d_ppEqualityEngine */
+ PPNotifyClass d_ppNotify;
+
/** Equaltity engine */
eq::EqualityEngine d_ppEqualityEngine;
@@ -181,6 +191,15 @@ class TheoryArrays : public Theory {
private:
+ class MayEqualNotifyClass {
+ public:
+ bool notify(TNode propagation) { return true; }
+ void notify(TNode t1, TNode t2) { }
+ };
+
+ /** The notify class for d_mayEqualEqualityEngine */
+ MayEqualNotifyClass d_mayEqualNotify;
+
/** Equaltity engine for determining if two arrays might be equal */
eq::EqualityEngine d_mayEqualEqualityEngine;
@@ -270,6 +289,11 @@ class TheoryArrays : public Theory {
Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
d_arrays.conflict(t1, t2);
}
+
+ void eqNotifyNewClass(TNode t) { }
+ void eqNotifyPreMerge(TNode t1, TNode t2) { }
+ void eqNotifyPostMerge(TNode t1, TNode t2) { }
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
};
/** The notify class for d_equalityEngine */
diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp
new file mode 100644
index 000000000..334d70eea
--- /dev/null
+++ b/src/theory/arrays/theory_arrays_instantiator.cpp
@@ -0,0 +1,56 @@
+/********************* */
+/*! \file theory_arrays_instantiator.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of theory_arrays_instantiator class
+ **/
+
+#include "theory/theory_engine.h"
+#include "theory/arrays/theory_arrays_instantiator.h"
+#include "theory/arrays/theory_arrays.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::arrays;
+
+InstantiatorTheoryArrays::InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th) :
+Instantiator( c, ie, th ){
+
+}
+
+void InstantiatorTheoryArrays::preRegisterTerm( Node t ){
+
+}
+
+void InstantiatorTheoryArrays::assertNode( Node assertion ){
+ Debug("quant-arrays-assert") << "InstantiatorTheoryArrays::assertNode: " << assertion << std::endl;
+ d_quantEngine->addTermToDatabase( assertion );
+ if( Options::current()->cbqi ){
+ if( assertion.hasAttribute(InstConstantAttribute()) ){
+ setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) );
+ }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){
+ setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) );
+ }
+ }
+}
+
+
+void InstantiatorTheoryArrays::processResetInstantiationRound( Theory::Effort effort ){
+
+}
+
+int InstantiatorTheoryArrays::process( Node f, Theory::Effort effort, int e, int limitInst ){
+ return InstStrategy::STATUS_SAT;
+}
diff --git a/src/theory/arrays/theory_arrays_instantiator.h b/src/theory/arrays/theory_arrays_instantiator.h
new file mode 100644
index 000000000..6a7c9c3ed
--- /dev/null
+++ b/src/theory/arrays/theory_arrays_instantiator.h
@@ -0,0 +1,51 @@
+/********************* */
+/*! \file theory_arrays_instantiator.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Instantiator for theory of arrays
+ **/
+
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__INSTANTIATOR_THEORY_ARRAYS_H
+#define __CVC4__INSTANTIATOR_THEORY_ARRAYS_H
+
+#include "theory/quantifiers_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arrays {
+
+class InstantiatorTheoryArrays : public Instantiator{
+ friend class QuantifiersEngine;
+protected:
+ /** reset instantiation round */
+ void processResetInstantiationRound( Theory::Effort effort );
+ /** process quantifier */
+ int process( Node f, Theory::Effort effort, int e, int limitInst = 0 );
+public:
+ InstantiatorTheoryArrays(context::Context* c, QuantifiersEngine* ie, Theory* th);
+ ~InstantiatorTheoryArrays() {}
+ /** Pre-register a term. */
+ void preRegisterTerm( Node t );
+ /** assertNode function, assertion is asserted to theory */
+ void assertNode( Node assertion );
+ /** identify */
+ std::string identify() const { return std::string("InstantiatorTheoryArrays"); }
+};/* class Instantiatior */
+
+}
+}
+}
+
+#endif \ No newline at end of file
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback