UNSAT problem

31 views
Skip to first unread message

Pat

unread,
Aug 12, 2013, 12:10:10 PM8/12/13
to hampi...@googlegroups.com

I am wondering why something like this returns unsat in hampi

var v : 10 .. 150;

//Target: xmlns= $$http://www.java2s.com$$;
cfg Books :=  "<Books>" SEQUENCE0 "</Books>" ;
cfg SEQUENCE0 := Book ;
cfg Book := (Booke)+ ;
cfg Booke :=  "<Book" BookAttributes ">" SEQUENCE1 "</Book>" ;
cfg SEQUENCE1 := Title Author Date ISBN Publisher ;
cfg Title :=  "<Title>" string "</Title>" ;
cfg Author := (Authore)+ ;
cfg Authore :=  "<Author>" string "</Author>" ;
cfg Date :=  "<Date>" string "</Date>" ;
cfg ISBN :=  "<ISBN>" string "</ISBN>" ;
cfg Publisher :=  "<Publisher>" string "</Publisher>" ;
cfg BookAttributes :=  Category InStock Reviewer;
cfg Category := " Category =" SIMPLE0;
cfg SIMPLE0 :=  "autobiography" | "non-fiction" | "fiction";
cfg InStock :=  | " InStock =" boolean;
cfg Reviewer :=  | " Reviewer =" string;

cfg string := ( CHAR )* ;
cfg boolean := "true" | "false" ;
cfg CHAR := ['!'-'~'];

assert v in Books;

Any help is appreciated.
Reply all
Reply to author
Forward
0 new messages