summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/Makefile.am2
-rw-r--r--src/smt/boolean_terms.cpp25
-rw-r--r--src/smt/smt_engine.cpp6
-rw-r--r--src/theory/arrays/kinds8
-rw-r--r--src/theory/arrays/theory_arrays_type_rules.h17
-rw-r--r--test/regress/regress0/Makefile.am1
-rw-r--r--test/regress/regress0/boolean-terms-bug-array.smt28
7 files changed, 63 insertions, 4 deletions
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 018f66ca8..2be82469e 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -169,7 +169,7 @@ endif
# 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 >"$@"
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index df5499c86..89f35bf05 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -164,6 +164,23 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
}
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
@@ -725,17 +742,19 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
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()) {
@@ -747,7 +766,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
// 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;
}
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7c5f98253..105ab9749 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3840,6 +3840,12 @@ void SmtEngine::checkModel(bool hardFailure) {
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.
diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 0bc973de9..c18492a58 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -41,10 +41,18 @@ constant STORE_ALL \
# 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
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 6cb31e51a..70e1c1a5b 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -178,6 +178,23 @@ struct ArrayTableFunTypeRule {
}
};/* 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);
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index d65fd20c5..cc691f8d2 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -49,6 +49,7 @@ SMT2_TESTS = \
arrayinuf_declare.smt2 \
boolean-terms-kernel1.smt2 \
boolean-terms-kernel2.smt2 \
+ boolean-terms-bug-array.smt2 \
chained-equality.smt2 \
ite2.smt2 \
ite3.smt2 \
diff --git a/test/regress/regress0/boolean-terms-bug-array.smt2 b/test/regress/regress0/boolean-terms-bug-array.smt2
new file mode 100644
index 000000000..781a19ff5
--- /dev/null
+++ b/test/regress/regress0/boolean-terms-bug-array.smt2
@@ -0,0 +1,8 @@
+(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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback