# expression (no |, no \<, ...).
Debug_tags.tmp Trace_tags.tmp:
$(AM_V_GEN)\
- grep '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \
+ grep -h '\<$(@:_tags.tmp=)\(\.isOn\)* *( *\".*\" *)' \
`find @srcdir@/../ -name "*.cpp" -o -name "*.h" -o -name "*.cc" -o -name "*.g"` | \
sed 's/\/\/.*//;s/^$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=)\(\.isOn\)* *( *\"\([^"]*\)\".*/\2/' | LC_ALL=C sort | uniq >"$@"
}
return out;
}
+ if(in.getType().isArray()) {
+ // convert in to in'
+ // e.g. in : (Array Int Bool)
+ // for in' : (Array Int (_ BitVec 1))
+ // then subs in |=> \array_lambda ( \lambda (x:Int) . [convert (read a' x) x]
+ Assert(as.isArray());
+ Assert(as.getArrayIndexType() == in.getType().getArrayIndexType());
+ Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType());
+ Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType());
+ Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x);
+ Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x);
+ Node selprime = rewriteAs(sel, as.getArrayConstituentType());
+ Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime);
+ Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam);
+ Assert(out.getType() == as);
+ return out;
+ }
if(in.getType().isParametricDatatype() &&
in.getType().isInstantiatedDatatype()) {
// We have something here like (Pair Bool Bool)---need to dig inside
case kind::EXISTS: {
Debug("bt") << "looking at quantifier -> " << top << endl;
set<TNode> ourVars;
+ set<TNode> output;
for(TNode::iterator i = top[0].begin(); i != top[0].end(); ++i) {
if((*i).getType().isBoolean()) {
ourVars.insert(*i);
+ } else if(convertType((*i).getType(), false) != (*i).getType()) {
+ output.insert(*i);
}
}
- if(ourVars.empty()) {
+ if(ourVars.empty() && output.empty()) {
// Simple case, quantifier doesn't quantify over Boolean vars,
// no special handling needed for quantifier. Fall through.
Debug("bt") << "- quantifier simple case (1), no Boolean vars bound" << endl;
} else {
- set<TNode> output;
hash_set< pair<TNode, bool>, PairHashFunction<TNode, bool, TNodeHashFunction, BoolHashFunction> > alreadySeen;
collectVarsInTermContext(top[1], ourVars, output, true, alreadySeen);
if(output.empty()) {
// We have Boolean vars appearing in term context. Convert their
// types in the quantifier.
for(set<TNode>::const_iterator i = output.begin(); i != output.end(); ++i) {
- Node newVar = nm->mkBoundVar((*i).toString(), nm->mkBitVectorType(1));
+ Node newVar = nm->mkBoundVar((*i).toString(), convertType((*i).getType(), false));
Assert(quantBoolVars.find(*i) == quantBoolVars.end(), "bad quantifier: shares a bound var with another quantifier (don't do that!)");
quantBoolVars[*i] = newVar;
}
n = d_private->d_iteRemover.replace(n);
Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n << endl;
+ // Apply our model value substitutions (again), as things may have been simplified.
+ Debug("boolean-terms") << "applying subses to " << n << endl;
+ n = substitutions.apply(n);
+ Debug("boolean-terms") << "++ got " << n << endl;
+ Notice() << "SmtEngine::checkModel(): -- re-substitutes to " << n << endl;
+
// As a last-ditch effort, ask model to simplify it.
// Presently, this is only an issue for quantifiers, which can have a value
// but don't show up in our substitution map above.
# used internally by array theory
operator ARR_TABLE_FUN 4 "array table function (internal-only symbol)"
+# used internally for substitutions in models (e.g. the Boolean terms converter)
+# The (single) argument is a lambda(x:T):U. Type of the array lambda is
+# Array T of U. Thus ARRAY_LAMBDA LAMBDA(x:INT) . (read a x) is the same array
+# as a. ARRAY_LAMBDA LAMBDA(x:INT) . (read a (- x 1)) is the same array as
+# as a shifted over one.
+operator ARRAY_LAMBDA 1 "array lambda (internal-only symbol)"
+
typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule
typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule
typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
+typerule ARRAY_LAMBDA ::CVC4::theory::arrays::ArrayLambdaTypeRule
# store operations that are ordered (by index) over a store-all are constant
construle STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
}
};/* struct ArrayTableFunTypeRule */
+struct ArrayLambdaTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::ARRAY_LAMBDA);
+ TypeNode lamType = n[0].getType(check);
+ if( check ) {
+ if(n[0].getKind() != kind::LAMBDA) {
+ throw TypeCheckingExceptionPrivate(n, "array lambda arg is non-lambda");
+ }
+ }
+ if(lamType.getNumChildren() != 2) {
+ throw TypeCheckingExceptionPrivate(n, "array lambda arg is not unary lambda");
+ }
+ return nodeManager->mkArrayType(lamType[0], lamType[1]);
+ }
+};/* struct ArrayLambdaTypeRule */
+
struct ArraysProperties {
inline static Cardinality computeCardinality(TypeNode type) {
Assert(type.getKind() == kind::ARRAY_TYPE);
arrayinuf_declare.smt2 \
boolean-terms-kernel1.smt2 \
boolean-terms-kernel2.smt2 \
+ boolean-terms-bug-array.smt2 \
chained-equality.smt2 \
ite2.smt2 \
ite3.smt2 \
--- /dev/null
+(set-logic AUFLIRA)
+
+(declare-fun f ((Array Int Bool)) Bool)
+(declare-fun y () (Array Int Bool))
+
+(assert (forall ((x (Array Int Bool))) (f y)))
+
+(check-sat)
projects / cvc5.git / commitdiff