From 5b09650edeac065f816247b5f88571ea72e79c3f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 21 Nov 2014 10:48:17 +0100 Subject: [PATCH] Throw error when pattern is not list of terms. --- .../theory_quantifiers_type_rules.h | 6 +++++ .../quantifiers/stream-x2014-09-18-unsat.smt2 | 24 +++++++++---------- 2 files changed, 18 insertions(+), 12 deletions(-) diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index 5d86c29c0..e44712412 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -84,6 +84,12 @@ struct QuantifierInstPatternTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw(TypeCheckingExceptionPrivate) { Assert(n.getKind() == kind::INST_PATTERN ); + if( check ){ + TypeNode tn = n[0].getType(check); + if( tn.isFunction() ){ + throw TypeCheckingExceptionPrivate(n[0], "Pattern must be a list of fully-applied terms."); + } + } return nodeManager->instPatternType(); } };/* struct QuantifierInstPatternTypeRule */ diff --git a/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 index 5f20cb3b5..615d43fe8 100644 --- a/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 +++ b/test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2 @@ -112,18 +112,18 @@ (assert (! (= (smap$f id$e) id$b) :named a12)) (assert (! (= (smap$a id$) id$e) :named a13)) (assert (! (= (smap$b id$a) id$d) :named a14)) -(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern (fun_app$j id$b ?v0))) :named a15)) -(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern (fun_app$i id$c ?v0))) :named a16)) -(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern (fun_app$e id$d ?v0))) :named a17)) -(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern (fun_app$c id$e ?v0))) :named a18)) -(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern (fun_app$d id$ ?v0))) :named a19)) -(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern (fun_app$f id$a ?v0))) :named a20)) -(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern (fun_app$j id$b ?v0))) :named a21)) -(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern (fun_app$i id$c ?v0))) :named a22)) -(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern (fun_app$e id$d ?v0))) :named a23)) -(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern (fun_app$c id$e ?v0))) :named a24)) -(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern (fun_app$d id$ ?v0))) :named a25)) -(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern (fun_app$f id$a ?v0))) :named a26)) +(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern ((fun_app$j id$b ?v0)))) :named a15)) +(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern ((fun_app$i id$c ?v0)))) :named a16)) +(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern ((fun_app$e id$d ?v0)))) :named a17)) +(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern ((fun_app$c id$e ?v0)))) :named a18)) +(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern ((fun_app$d id$ ?v0)))) :named a19)) +(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern ((fun_app$f id$a ?v0)))) :named a20)) +(assert (! (forall ((?v0 B_stream_stream$)) (! (= (fun_app$j id$b ?v0) ?v0) :pattern ((fun_app$j id$b ?v0)))) :named a21)) +(assert (! (forall ((?v0 A_stream_stream$)) (! (= (fun_app$i id$c ?v0) ?v0) :pattern ((fun_app$i id$c ?v0)))) :named a22)) +(assert (! (forall ((?v0 A_stream$)) (! (= (fun_app$e id$d ?v0) ?v0) :pattern ((fun_app$e id$d ?v0)))) :named a23)) +(assert (! (forall ((?v0 B_stream$)) (! (= (fun_app$c id$e ?v0) ?v0) :pattern ((fun_app$c id$e ?v0)))) :named a24)) +(assert (! (forall ((?v0 B$)) (! (= (fun_app$d id$ ?v0) ?v0) :pattern ((fun_app$d id$ ?v0)))) :named a25)) +(assert (! (forall ((?v0 A$)) (! (= (fun_app$f id$a ?v0) ?v0) :pattern ((fun_app$f id$a ?v0)))) :named a26)) (assert (! (forall ((?v0 B_b_stream_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$ (smap$g ?v0 ?v1) ?v2) (fun_app$ ?v0 (snth$a ?v1 ?v2)))) :named a27)) (assert (! (forall ((?v0 B_a_stream_fun$) (?v1 B_stream$) (?v2 Nat$)) (= (snth$b (smap$h ?v0 ?v1) ?v2) (fun_app$k ?v0 (snth$a ?v1 ?v2)))) :named a28)) (assert (! (forall ((?v0 A_b_stream_fun$) (?v1 A_stream$) (?v2 Nat$)) (= (snth$ (smap$i ?v0 ?v1) ?v2) (fun_app$l ?v0 (snth$c ?v1 ?v2)))) :named a29)) -- 2.30.2