summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/command.h2
-rw-r--r--src/printer/printer.h2
-rw-r--r--src/smt/smt_engine.h2
-rw-r--r--src/theory/arrays/theory_arrays.cpp14
-rw-r--r--src/theory/arrays/theory_arrays_rewriter.h4
-rw-r--r--src/theory/arrays/type_enumerator.h80
-rw-r--r--src/theory/bv/theory_bv.cpp2
-rw-r--r--src/theory/model.cpp18
-rw-r--r--src/theory/model.h12
-rw-r--r--src/util/Makefile.am4
-rw-r--r--src/util/util_model.cpp (renamed from src/util/model.cpp)2
-rw-r--r--src/util/util_model.h (renamed from src/util/model.h)0
12 files changed, 119 insertions, 23 deletions
diff --git a/src/expr/command.h b/src/expr/command.h
index e120deed6..6f5b0bd4c 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -37,7 +37,7 @@
#include "util/sexpr.h"
#include "util/datatype.h"
#include "util/proof.h"
-#include "util/model.h"
+#include "util/util_model.h"
namespace CVC4 {
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 778c21f1f..48b76d15a 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -23,7 +23,7 @@
#include "util/language.h"
#include "util/sexpr.h"
-#include "util/model.h"
+#include "util/util_model.h"
#include "expr/node.h"
#include "expr/command.h"
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 096708f53..f30a98935 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -29,7 +29,7 @@
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "util/proof.h"
-#include "util/model.h"
+#include "util/util_model.h"
#include "smt/modal_exception.h"
#include "util/hash.h"
#include "options/options.h"
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 63b61995a..b4cc8e5f7 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -565,11 +565,17 @@ void TheoryArrays::computeCareGraph()
// If arrays are known to be disequal, or cannot become equal, we can continue
Assert(d_mayEqualEqualityEngine.hasTerm(r1[0]) && d_mayEqualEqualityEngine.hasTerm(r2[0]));
if (r1[0].getType() != r2[0].getType() ||
- (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) ||
d_equalityEngine.areDisequal(r1[0], r2[0], false)) {
Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
continue;
}
+ else if (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) {
+ if (r2.getType().getCardinality().isInfinite()) {
+ continue;
+ }
+ // TODO: add a disequality split for these two arrays
+ continue;
+ }
}
TNode x = r1[1];
@@ -678,11 +684,17 @@ void TheoryArrays::collectModelInfo( TheoryModel* m, bool fullModel ){
if (it == defValues.end()) {
TypeNode valueType = n.getType().getArrayConstituentType();
rep = defaultValuesSet.nextTypeEnum(valueType);
+ if (rep.isNull()) {
+ Assert(defaultValuesSet.getSet(valueType)->begin() != defaultValuesSet.getSet(valueType)->end());
+ rep = *(defaultValuesSet.getSet(valueType)->begin());
+ }
+ Trace("arrays-models") << "New default value = " << rep << endl;
defValues[mayRep] = rep;
}
else {
rep = (*it).second;
}
+
// Build the STORE_ALL term with the default value
rep = nm->mkConst(ArrayStoreAll(n.getType().toType(), rep.toExpr()));
// For each read, require that the rep stores the right value
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index d120f8feb..0f46ffe7c 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -358,6 +358,10 @@ public:
Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl;
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
}
+ else if (node[0].isConst() && node[1].isConst()) {
+ Trace("arrays-postrewrite") << "Arrays::postRewrite returning false" << std::endl;
+ return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
+ }
if (node[0] > node[1]) {
Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << newNode << std::endl;
diff --git a/src/theory/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index f6d871c48..c6b73b9f6 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -24,6 +24,7 @@
#include "theory/type_enumerator.h"
#include "expr/type_node.h"
#include "expr/kind.h"
+#include "theory/rewriter.h"
namespace CVC4 {
namespace theory {
@@ -31,27 +32,94 @@ namespace arrays {
class ArrayEnumerator : public TypeEnumeratorBase<ArrayEnumerator> {
TypeEnumerator d_index;
- TypeEnumerator d_constituent;
+ TypeNode d_constituentType;
+ NodeManager* d_nm;
+ std::vector<Node> d_indexVec;
+ std::vector<TypeEnumerator*> d_constituentVec;
+ bool d_finished;
+ Node d_arrayConst;
public:
ArrayEnumerator(TypeNode type) throw(AssertionException) :
TypeEnumeratorBase<ArrayEnumerator>(type),
- d_index(TypeEnumerator(type.getArrayIndexType())),
- d_constituent(TypeEnumerator(type.getArrayConstituentType())) {
+ d_index(type.getArrayIndexType()),
+ d_constituentType(type.getArrayConstituentType()),
+ d_nm(NodeManager::currentNM()),
+ d_finished(false)
+ {
+ d_indexVec.push_back(*d_index);
+ d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+ d_arrayConst = d_nm->mkConst(ArrayStoreAll(type.toType(), (*(*d_constituentVec.back())).toExpr()));
+ }
+
+ ~ArrayEnumerator() {
+ while (!d_constituentVec.empty()) {
+ delete d_constituentVec.back();
+ d_constituentVec.pop_back();
+ }
}
Node operator*() throw(NoMoreValuesException) {
- return Node::null();
- //return NodeManager::currentNM()->mkConst(Array(d_size, d_bits));
+ if (d_finished) {
+ throw NoMoreValuesException(getType());
+ }
+ Node n = d_arrayConst;
+ for (unsigned i = 0; i < d_indexVec.size(); ++i) {
+ n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i])));
+ }
+ Trace("array-type-enum") << "operator * prerewrite: " << n << std::endl;
+ n = Rewriter::rewrite(n);
+ Trace("array-type-enum") << "operator * returning: " << n << std::endl;
+ return n;
}
ArrayEnumerator& operator++() throw() {
+ Trace("array-type-enum") << "operator++ called, **this = " << **this << std::endl;
+
+ if (d_finished) {
+ Trace("array-type-enum") << "operator++ finished!" << std::endl;
+ return *this;
+ }
+ while (!d_constituentVec.empty()) {
+ ++(*d_constituentVec.back());
+ if (d_constituentVec.back()->isFinished()) {
+ delete d_constituentVec.back();
+ d_constituentVec.pop_back();
+ }
+ else {
+ break;
+ }
+ }
+
+ if (d_constituentVec.empty()) {
+ ++d_index;
+ if (d_index.isFinished()) {
+ Trace("array-type-enum") << "operator++ finished!" << std::endl;
+ d_finished = true;
+ return *this;
+ }
+ d_indexVec.push_back(*d_index);
+ d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+ ++(*d_constituentVec.back());
+ if (d_constituentVec.back()->isFinished()) {
+ Trace("array-type-enum") << "operator++ finished!" << std::endl;
+ d_finished = true;
+ return *this;
+ }
+ }
+
+ while (d_constituentVec.size() < d_indexVec.size()) {
+ d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+ }
+
+ Trace("array-type-enum") << "operator++ returning, **this = " << **this << std::endl;
return *this;
}
bool isFinished() throw() {
- Unimplemented();
+ Trace("array-type-enum") << "isFinished returning: " << d_finished << std::endl;
+ return d_finished;
}
};/* class ArrayEnumerator */
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 51e09ee5a..1c5b08546 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -127,7 +127,7 @@ void TheoryBV::check(Effort e)
void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
Assert(!inConflict());
- Assert (fullModel); // can only query full model
+ // Assert (fullModel); // can only query full model
d_equalitySolver.collectModelInfo(m);
d_bitblastSolver.collectModelInfo(m);
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index 4a3ddc9ca..d4b71c9e2 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -486,7 +486,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
eq::EqClassIterator eqc_i = eq::EqClassIterator(*i2, &tm->d_equalityEngine);
for ( ; !eqc_i.isFinished(); ++eqc_i) {
Node n = *eqc_i;
- Node normalized = normalize(tm, n, constantReps);
+ Node normalized = normalize(tm, n, constantReps, true);
if (normalized.isConst()) {
typeConstSet.add(t, normalized);
constantReps[*i2] = normalized;
@@ -529,7 +529,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
for (i = repSet.begin(); i != repSet.end(); ) {
Assert(assertedReps.find(*i) != assertedReps.end());
Node rep = assertedReps[*i];
- Node normalized = normalize(tm, rep, constantReps);
+ Node normalized = normalize(tm, rep, constantReps, false);
Trace("model-builder") << " Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
if (normalized.isConst()) {
changed = true;
@@ -602,9 +602,8 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
}
-Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps)
+Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps, bool evalOnly)
{
- Trace("tembn") << "Normalize " << r << std::endl;
std::map<Node, Node>::iterator itMap = constantReps.find(r);
if (itMap != constantReps.end()) {
return (*itMap).second;
@@ -625,8 +624,17 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node
if (!ri.isConst()) {
if (m->d_equalityEngine.hasTerm(ri)) {
ri = m->d_equalityEngine.getRepresentative(ri);
+ itMap = constantReps.find(ri);
+ if (itMap != constantReps.end()) {
+ ri = (*itMap).second;
+ }
+ else if (evalOnly) {
+ ri = normalize(m, r[i], constantReps, evalOnly);
+ }
+ }
+ else {
+ ri = normalize(m, ri, constantReps, evalOnly);
}
- ri = normalize(m, ri, constantReps);
if (!ri.isConst()) {
childrenConst = false;
}
diff --git a/src/theory/model.h b/src/theory/model.h
index 90cd1e35a..0a846a3c6 100644
--- a/src/theory/model.h
+++ b/src/theory/model.h
@@ -19,7 +19,7 @@
#ifndef __CVC4__THEORY_MODEL_H
#define __CVC4__THEORY_MODEL_H
-#include "util/model.h"
+#include "util/util_model.h"
#include "theory/uf/equality_engine.h"
#include "theory/rep_set.h"
#include "theory/substitutions.h"
@@ -193,7 +193,9 @@ private:
else {
te = (*it).second;
}
- Assert(!te->isFinished());
+ if (te->isFinished()) {
+ return Node();
+ }
iterator itSet = d_typeSet.find(t);
std::set<Node>* s;
@@ -206,7 +208,9 @@ private:
}
Node n = **te;
while (s->find(n) != s->end()) {
- Assert(!te->isFinished());
+ if (te->isFinished()) {
+ return Node();
+ }
++(*te);
n = **te;
}
@@ -254,7 +258,7 @@ protected:
/** choose representative for unconstrained equivalence class */
virtual Node chooseRepresentative(TheoryModel* m, Node eqc, bool fullModel);
/** normalize representative */
- Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps);
+ Node normalize(TheoryModel* m, TNode r, std::map<Node, Node>& constantReps, bool evalOnly);
public:
TheoryEngineModelBuilder(TheoryEngine* te);
virtual ~TheoryEngineModelBuilder(){}
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 6c3104760..a4462d824 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -81,8 +81,8 @@ libutil_la_SOURCES = \
uninterpreted_constant.cpp \
array_store_all.h \
array_store_all.cpp \
- model.h \
- model.cpp
+ util_model.h \
+ util_model.cpp
libutil_la_LIBADD = \
@builddir@/libutilcudd.la
diff --git a/src/util/model.cpp b/src/util/util_model.cpp
index 8b0e956cf..6dfe2c566 100644
--- a/src/util/model.cpp
+++ b/src/util/util_model.cpp
@@ -14,7 +14,7 @@
** \brief implementation of Model class
**/
-#include "util/model.h"
+#include "util/util_model.h"
#include "expr/command.h"
#include "smt/smt_engine_scope.h"
#include "smt/command_list.h"
diff --git a/src/util/model.h b/src/util/util_model.h
index 97010dd45..97010dd45 100644
--- a/src/util/model.h
+++ b/src/util/util_model.h
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback