// This file is part of the Wyone automated theorem prover.
//
// Wyone is free software; you can redistribute it and/or modify 
// it under the terms of the GNU General Public License as published 
// by the Free Software Foundation; either version 3 of the License, 
// or (at your option) any later version.
//
// Wyone is distributed in the hope that it will be useful, but 
// WITHOUT ANY WARRANTY; without even the implied warranty of 
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See 
// the GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public 
// License along with Wyone. If not, see <http://www.gnu.org/licenses/>
//
// Copyright 2010, David James Pearce. 

package wyone.testing;

import static org.junit.Assert.assertTrue;
import static wyone.Main.checkUnsat;
import static wyone.Main.checkSat;

import org.junit.Test;

public class BoundedListQuantifiers {
	
	@Test
	public void Unsat_1() {
		assertTrue(checkUnsat("[int] xs; xs==[0,1,2] && all [ i : xs | xs[i] > 0 ]"));
	}
	
	@Test
	public void Unsat_5() {
		assertTrue(checkUnsat("[int] xs; int i; xs[i]==0 && all [ j : xs | xs[j] > 0 ]"));
	}
	
	@Test
	public void Unsat_6() {
		assertTrue(checkUnsat("[int] xs; some [ i : xs | xs[i] == 0 ] && all [ j : xs | xs[j] > 0 ]"));
	}
	
	@Test
	public void Unsat_7() {
		assertTrue(checkUnsat("int x,i; [int] xs; x == xs[i]" + 
				" && all [ j : xs | xs[j] > 0 ] && x >= 0 && x < 1"));
	}
	
	
	@Test
	public void Sat_1() {
		assertTrue(checkSat("[int] xs; xs==[1,2] && all [ i : xs | xs[i] > 0 ]"));
	}
}

@@ -1513,16 +1513,385 @@
 %09%7D%0D%0A%09%0D%0A%09
+@Test%0D%0A%09public void Unsat_8() %7B%0D%0A%09%09assertTrue(checkUnsat(%22%5Bint%5D left, right, result; %22 + %0D%0A%09%09%09%09%22some %5Bx : result %7C 0 %3E result%5Bx%5D%5D && left==%5B1.0,2.0,3.0%5D  && right==%5B5.0,6.0,7.0%5D%22 + %0D%0A%09%09%09%09%22&& %7Cresult%7C==(%7Cleft%7C+%7Cright%7C) %22 + %0D%0A%09%09%09%09%22&& (all %5B$3 : result %7C (right%5B($3-%7Cleft%7C)%5D==result%5B$3%5D %7C%7C 0 %3E ($3-%7Cleft%7C)) && (0 %3C= ($3-%7Cleft%7C) %7C%7C left%5B$3%5D==result%5B$3%5D)%5D)%22));%0D%0A%09%09%09%09%09%09%0D%0A%09%7D%0D%0A
 %0D%0A%09@Test

Working on list append test failure.