From: Morgan Deters Date: Sat, 1 Dec 2012 14:36:14 +0000 (+0000) Subject: Fix the way abstract values are typed; fixes some compliance issues. X-Git-Tag: cvc5-1.0.0~7491 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ec29471e427bf25034a93c182b424730d439a90a;p=cvc5.git Fix the way abstract values are typed; fixes some compliance issues. Also support array-store-all for Boolean terms (related to abstract values, since that's the only way for the user to include an array-store-all in an assertion). (this commit was certified error- and warning-free by the test-and-commit script.) --- diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index e68873176..f6aa1920d 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1303,14 +1303,7 @@ inline void NodeBuilder::maybeCheckType(const TNode n) const kind::MetaKind mk = n.getMetaKind(); if( mk != kind::metakind::VARIABLE && mk != kind::metakind::CONSTANT ) { - try { - d_nm->getType(n, true); - } catch(UnknownTypeException&) { - // Ignore the error; this expression doesn't have a type, - // because it has an abstract value in it. If the user - // depends on the type of this expression, he should get an - // exception, but so far he's only constructed it. - } + d_nm->getType(n, true); } } } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index f040c7c72..59d23c6ea 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -86,7 +86,8 @@ NodeManager::NodeManager(context::Context* ctxt, d_attrManager(ctxt), d_exprManager(exprManager), d_nodeUnderDeletion(NULL), - d_inReclaimZombies(false) { + d_inReclaimZombies(false), + d_abstractValueCount(0) { init(); } @@ -99,7 +100,8 @@ NodeManager::NodeManager(context::Context* ctxt, d_attrManager(ctxt), d_exprManager(exprManager), d_nodeUnderDeletion(NULL), - d_inReclaimZombies(false) { + d_inReclaimZombies(false), + d_abstractValueCount(0) { init(); } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 2cda23f2d..e94795f0e 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -170,6 +170,14 @@ class NodeManager { */ std::hash_map d_tupleAndRecordTypes; + /** + * Keep a count of all abstract values produced by this NodeManager. + * Abstract values have a type attribute, so if multiple SmtEngines + * are attached to this NodeManager, we don't want their abstract + * values to overlap. + */ + unsigned d_abstractValueCount; + /** * Look up a NodeValue in the pool associated to this NodeManager. * The NodeValue argument need not be a "completely-constructed" @@ -455,6 +463,9 @@ public: /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); + /** Make a new abstract value with the given type. */ + Node mkAbstractValue(const TypeNode& type); + /** * Create a constant of type T. It will have the appropriate * CONST_* kind defined for T. @@ -1557,6 +1568,13 @@ inline Node NodeManager::mkInstConstant(const TypeNode& type) { return n; } +inline Node NodeManager::mkAbstractValue(const TypeNode& type) { + Node n = mkConst(AbstractValue(++d_abstractValueCount)); + n.setAttribute(TypeAttr(), type); + n.setAttribute(TypeCheckedAttr(), true); + return n; +} + template Node NodeManager::mkConst(const T& val) { return mkConstInternal(val); diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index dda9c7a3e..696622cfe 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -121,6 +121,33 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw } if(mk == kind::metakind::CONSTANT) { + if(k == kind::STORE_ALL) { + const ArrayStoreAll& asa = top.getConst(); + ArrayType arrType = asa.getType(); + TypeNode indexType = TypeNode::fromType(arrType.getIndexType()); + Type constituentType = arrType.getConstituentType(); + if(constituentType.isBoolean()) { + // we have store_all(true) or store_all(false) + // just turn it into store_all(1) or store_all(0) + Node newConst = nm->mkConst(BitVector(1u, asa.getExpr().getConst() ? 1u : 0u)); + if(indexType.isBoolean()) { + // change index type to BV(1) also + indexType = nm->mkBitVectorType(1); + } + ArrayStoreAll asaRepl(nm->mkArrayType(indexType, nm->mkBitVectorType(1)).toType(), newConst.toExpr()); + Node n = nm->mkConst(asaRepl); + Debug("boolean-terms") << " returning new store_all: " << n << std::endl; + return n; + } + if(indexType.isBoolean()) { + // must change index type to BV(1) + indexType = nm->mkBitVectorType(1); + ArrayStoreAll asaRepl(nm->mkArrayType(indexType, TypeNode::fromType(constituentType)).toType(), asa.getExpr()); + Node n = nm->mkConst(asaRepl); + Debug("boolean-terms") << " returning new store_all: " << n << std::endl; + return n; + } + } return top; } else if(mk == kind::metakind::VARIABLE) { TypeNode t = top.getType(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fb8b78759..c82b7ca2c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -495,7 +495,7 @@ public: Assert(options::abstractValues()); Node& val = d_abstractValues[n]; if(val.isNull()) { - val = d_smt.d_nodeManager->mkConst(AbstractValue(d_abstractValues.size())); + val = d_smt.d_nodeManager->mkAbstractValue(n.getType()); d_abstractValueMap.addSubstitution(val, n); } return val; diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 40f838623..baf498968 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -139,9 +139,9 @@ class AbstractValueTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { // An UnknownTypeException means that this node has no type. For now, - // only abstract values are like this. Assigning them a type in all - // cases is difficult, since then the parser and the SmtEngine must be - // more tightly coupled. + // only abstract values are like this---and then, only if they are created + // by the user and don't actually correspond to one that the SmtEngine gave + // them previously. throw UnknownTypeException(n); } };/* class AbstractValueTypeRule */