#include "util/sexpr.h"
#include "util/datatype.h"
#include "util/proof.h"
-#include "util/model.h"
+#include "util/util_model.h"
namespace CVC4 {
#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"
#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"
// 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];
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
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;
#include "theory/type_enumerator.h"
#include "expr/type_node.h"
#include "expr/kind.h"
+#include "theory/rewriter.h"
namespace CVC4 {
namespace theory {
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 */
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);
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;
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;
}
-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;
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;
}
#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"
else {
te = (*it).second;
}
- Assert(!te->isFinished());
+ if (te->isFinished()) {
+ return Node();
+ }
iterator itSet = d_typeSet.find(t);
std::set<Node>* s;
}
Node n = **te;
while (s->find(n) != s->end()) {
- Assert(!te->isFinished());
+ if (te->isFinished()) {
+ return Node();
+ }
++(*te);
n = **te;
}
/** 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(){}
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
+++ /dev/null
-/********************* */
-/*! \file model.cpp
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 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 Model class
- **/
-
-#include "util/model.h"
-#include "expr/command.h"
-#include "smt/smt_engine_scope.h"
-#include "smt/command_list.h"
-
-#include <vector>
-
-using namespace std;
-
-namespace CVC4 {
-
-Model::Model() :
- d_smt(*smt::currentSmtEngine()) {
-}
-
-size_t Model::getNumCommands() const {
- return d_smt.d_modelCommands->size();
-}
-
-const Command* Model::getCommand(size_t i) const {
- return (*d_smt.d_modelCommands)[i];
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* */
-/*! \file model.h
- ** \verbatim
- ** Original author: ajreynol
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 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 Model class
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__MODEL_H
-#define __CVC4__MODEL_H
-
-#include <iostream>
-#include <vector>
-
-#include "expr/expr.h"
-#include "util/cardinality.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC Command;
-class CVC4_PUBLIC SmtEngine;
-
-class CVC4_PUBLIC Model {
-private:
- /** The SmtEngine we're associated to */
- const SmtEngine& d_smt;
-public:
- /** construct the base class */
- Model();
- /** virtual destructor */
- virtual ~Model() { }
- /** get number of commands to report */
- size_t getNumCommands() const;
- /** get command */
- const Command* getCommand(size_t i) const;
-public:
- /** get value for expression */
- virtual Expr getValue(Expr expr) = 0;
- /** get cardinality for sort */
- virtual Cardinality getCardinality(Type t) = 0;
- /** write the model to a stream */
- virtual void toStream(std::ostream& out) = 0;
-};/* class Model */
-
-class ModelBuilder
-{
-public:
- ModelBuilder(){}
- virtual ~ModelBuilder(){}
- virtual void buildModel( Model* m, bool fullModel ) = 0;
-};/* class ModelBuilder */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__MODEL_H */
--- /dev/null
+/********************* */
+/*! \file model.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 Model class
+ **/
+
+#include "util/util_model.h"
+#include "expr/command.h"
+#include "smt/smt_engine_scope.h"
+#include "smt/command_list.h"
+
+#include <vector>
+
+using namespace std;
+
+namespace CVC4 {
+
+Model::Model() :
+ d_smt(*smt::currentSmtEngine()) {
+}
+
+size_t Model::getNumCommands() const {
+ return d_smt.d_modelCommands->size();
+}
+
+const Command* Model::getCommand(size_t i) const {
+ return (*d_smt.d_modelCommands)[i];
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file model.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 Model class
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__MODEL_H
+#define __CVC4__MODEL_H
+
+#include <iostream>
+#include <vector>
+
+#include "expr/expr.h"
+#include "util/cardinality.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC Command;
+class CVC4_PUBLIC SmtEngine;
+
+class CVC4_PUBLIC Model {
+private:
+ /** The SmtEngine we're associated to */
+ const SmtEngine& d_smt;
+public:
+ /** construct the base class */
+ Model();
+ /** virtual destructor */
+ virtual ~Model() { }
+ /** get number of commands to report */
+ size_t getNumCommands() const;
+ /** get command */
+ const Command* getCommand(size_t i) const;
+public:
+ /** get value for expression */
+ virtual Expr getValue(Expr expr) = 0;
+ /** get cardinality for sort */
+ virtual Cardinality getCardinality(Type t) = 0;
+ /** write the model to a stream */
+ virtual void toStream(std::ostream& out) = 0;
+};/* class Model */
+
+class ModelBuilder
+{
+public:
+ ModelBuilder(){}
+ virtual ~ModelBuilder(){}
+ virtual void buildModel( Model* m, bool fullModel ) = 0;
+};/* class ModelBuilder */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__MODEL_H */
projects / cvc5.git / commitdiff