From 930601b40c68d959e66abc71da6ff3296860952e Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Thu, 4 Oct 2012 17:45:56 +0000 Subject: [PATCH] Implemented array type enumerator, more fixes for models --- src/expr/command.h | 2 +- src/printer/printer.h | 2 +- src/smt/smt_engine.h | 2 +- src/theory/arrays/theory_arrays.cpp | 14 +++- src/theory/arrays/theory_arrays_rewriter.h | 4 ++ src/theory/arrays/type_enumerator.h | 80 ++++++++++++++++++++-- src/theory/bv/theory_bv.cpp | 2 +- src/theory/model.cpp | 18 +++-- src/theory/model.h | 12 ++-- src/util/Makefile.am | 4 +- src/util/{model.cpp => util_model.cpp} | 2 +- src/util/{model.h => util_model.h} | 0 12 files changed, 119 insertions(+), 23 deletions(-) rename src/util/{model.cpp => util_model.cpp} (97%) rename src/util/{model.h => util_model.h} (100%) 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 { TypeEnumerator d_index; - TypeEnumerator d_constituent; + TypeNode d_constituentType; + NodeManager* d_nm; + std::vector d_indexVec; + std::vector d_constituentVec; + bool d_finished; + Node d_arrayConst; public: ArrayEnumerator(TypeNode type) throw(AssertionException) : TypeEnumeratorBase(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::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* 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& constantReps); + Node normalize(TheoryModel* m, TNode r, std::map& 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 similarity index 97% rename from src/util/model.cpp rename to 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 similarity index 100% rename from src/util/model.h rename to src/util/util_model.h -- 2.30.2