diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-23 17:00:56 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-23 17:00:56 -0500 |
| commit | fd29170106da3401dd183b479c84984a16ddcc41 (patch) | |
| tree | feed726bb7637261a80b46d8e42b7a5d2ae4ff15 /test | |
| parent | cf788e029054c1ee4a0399940422447ddefce878 (diff) | |
partially address bug 486: allow some model inspection of quantifiers
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/bug486.cvc | 25 |
2 files changed, 27 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 3b30a8d9e..d5b35594f 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -149,7 +149,8 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) \ simplification_bug4.smt2.expect \ - bug216.smt2.expect + bug216.smt2.expect \ + bug486.cvc if CVC4_BUILD_PROFILE_COMPETITION else diff --git a/test/regress/regress0/bug486.cvc b/test/regress/regress0/bug486.cvc new file mode 100644 index 000000000..6e8ee0018 --- /dev/null +++ b/test/regress/regress0/bug486.cvc @@ -0,0 +1,25 @@ +prin:TYPE; +form:TYPE; + +signed:(prin,form)->BOOLEAN; +says:(prin,form)->BOOLEAN; + +speaksfor:(prin,prin)->form; +signedE:BOOLEAN = FORALL(x:prin,y:form) : signed(x,y) => says(x,y); +saysE:BOOLEAN = FORALL(x,y:prin,z:form) : says(x,speaksfor(y,x)) AND says(y,z) => says(x,z); + +ASSERT(signedE); +ASSERT(saysE); + +julie:prin; +dave:prin; +alice:prin; +openfile:form; + +x2:BOOLEAN = signed(alice,openfile); +ASSERT(x2); +x3:BOOLEAN = signed(dave,speaksfor(alice,dave)); +ASSERT(x3); + +QUERY NOT says(dave,openfile); % this is invalid +QUERY says(dave,openfile); % this is valid |