Merge branch 'master' into inc-extension

samples/AMPL/CT2.mod

@@ -0,0 +1,58 @@
+param num_beams;                  # number of beams
+
+param num_rows >= 1, integer;     # number of rows
+param num_cols >= 1, integer;     # number of columns 
+
+set BEAMS   := 1 .. num_beams;    # set of beams
+
+set ROWS    := 1 .. num_rows;	  # set of rows
+set COLUMNS := 1 .. num_cols;	  # set of columns
+
+# values for entries of each beam
+param beam_values {BEAMS, ROWS, COLUMNS} >= 0; 
+
+# values of tumor
+param tumor_values {ROWS, COLUMNS} >= 0; 
+
+# values of critical area
+param critical_values {ROWS, COLUMNS} >= 0; 
+
+# critical maximum dosage requirement
+param critical_max;
+
+# tumor minimum dosage requirement
+param tumor_min;
+
+# dosage scalar of each beam
+var X {i in BEAMS} >= 0;
+
+
+# define the tumor area which includes the locations where tumor exists
+set tumor_area := {k in ROWS, h in COLUMNS: tumor_values[k,h] > 0};
+
+# define critical area 
+set critical_area := {k in ROWS, h in COLUMNS: critical_values[k,h] > 0};
+
+var S {(k,h) in tumor_area} >= 0;
+var T {(k,h) in critical_area} >= 0;
+
+# maximize total dosage in tumor area
+maximize total_tumor_dosage: sum {i in BEAMS} sum {(k,h) in tumor_area} X[i] * beam_values[i,k,h];
+
+# minimize total dosage in critical area
+minimize total_critical_dosage: sum {i in BEAMS} sum {(k,h) in critical_area} X[i] * beam_values[i,k,h];
+
+# minimize total tumor slack
+minimize total_tumor_slack: sum {(k,h) in tumor_area} S[k,h];
+
+# minimize total critical area slack
+minimize total_critical_slack: sum {(k,h) in critical_area} T[k,h];
+
+# total dosage at each tumor location [k,h] should be >= min tumor dosage with slack variable
+subject to tumor_limit {(k,h) in tumor_area} : sum {i in BEAMS} X[i] * beam_values[i,k,h] == tumor_min - S[k,h];
+
+# total dosage at each critical location [k,h] should be = max critical dosage with slack variable
+subject to critical_limit {(k,h) in critical_area} : sum {i in BEAMS} X[i] * beam_values[i,k,h] == critical_max + T[k,h];
+
+
+

samples/Linux Kernel Module/bcm4334x.mod

@@ -0,0 +1,2 @@
+/data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/bcm4334x.ko
+/data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_pno.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_common.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_ip.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_custom_gpio.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_linux.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_linux_sched.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_cfg80211.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_linux_wq.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/aiutils.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/bcmevent.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/bcmutils.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/bcmwifi_channels.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/hndpmu.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/linux_osl.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/sbutils.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/siutils.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/wl_android.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/wl_cfg80211.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/wl_cfgp2p.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/wl_cfg_btcoex.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/wldev_common.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/wl_linux_mon.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_linux_platdev.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/bcmsdh.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/bcmsdh_linux.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/bcmsdh_sdmmc.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/bcmsdh_sdmmc_linux.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_cdc.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_wlfc.o /data/israel/edison/poky/meta-edison/recipes-kernel/bcm43340/driver_bcm43x/dhd_sdio.o

samples/Linux Kernel Module/mbcache.mod

@@ -0,0 +1,2 @@
+fs/mbcache.ko
+fs/mbcache.o

samples/Linux Kernel Module/md5.mod

@@ -0,0 +1,2 @@
+crypto/md5.ko
+crypto/md5.o

samples/Modula-2/HuffChan.mod

@@ -0,0 +1,329 @@
+IMPLEMENTATION MODULE HuffChan;
+
+(*
+ This module shows how to redefine standard IO file functions. It provides
+ functions for reading and writing packed files opened in Raw mode.
+*)
+
+IMPORT IOChan, IOLink, ChanConsts, IOConsts, SYSTEM, Strings;
+FROM Storage IMPORT ALLOCATE, DEALLOCATE;
+
+CONST
+  rbldFrq = 512;	(* means: every 512 bytes rebuild table *)
+
+TYPE
+  charTap  = POINTER TO ARRAY [0..MAX(INTEGER)-1] OF CHAR;
+  smbTp = POINTER TO smbT;
+
+  smbT = RECORD			(* Huffman's tree *)
+    ch			: CHAR;
+    n			: CARDINAL; (* frequncy of char ch *)
+    left,right,next	: smbTp;
+  END;
+
+  tblT = RECORD		(* bit sequence for code *)
+    vl		: CARDINAL;	(* bit sequence *)
+    cnt		: INTEGER;	(* it length *)
+  END;
+
+  lclDataT = RECORD	(* channel's local data *)
+    tRoot 	: smbTp;
+    htbl	: ARRAY [0..255] OF tblT;     (* code -> bit sequence table *)
+    ftbl  	: ARRAY [0..255] OF CARDINAL; (* frequncey table *)
+    wBf,rb1,rb2	: CARDINAL;
+    wbc,rbc,smc	: INTEGER;
+    chid	: IOChan.ChanId;
+  END;
+  lclDataTp = POINTER TO lclDataT;
+  charp     = POINTER TO CHAR;
+
+VAR
+  did	: IOLink.DeviceId;
+  ldt	: lclDataTp;
+
+
+PROCEDURE Shf(a:CARDINAL; b : INTEGER) : CARDINAL; (* shl a,b (or shr) *)
+BEGIN
+  RETURN SYSTEM.CAST(CARDINAL,SYSTEM.SHIFT(SYSTEM.CAST(BITSET,a),b));
+END Shf;
+
+PROCEDURE wrDword(a:CARDINAL);	(* write 4 bytes to file *)
+BEGIN
+  IOChan.RawWrite(ldt^.chid,SYSTEM.ADR(a),4);
+END wrDword;
+
+PROCEDURE rdDword() : CARDINAL;  (* read 4 bytes from file *)
+VAR
+  a,z : CARDINAL;
+BEGIN
+  a:=0;
+  IOChan.RawRead(ldt^.chid,SYSTEM.ADR(a),4,z);
+  RETURN a;
+END rdDword;
+
+PROCEDURE wrSmb(ch : CHAR);	(* write bit sequence for code ch *)
+VAR
+  v,h : CARDINAL;
+  b,c : INTEGER;
+BEGIN
+  WITH ldt^ DO
+    v:=htbl[ORD(ch)].vl;
+    c:=htbl[ORD(ch)].cnt;
+    IF c+wbc<=32 THEN
+      wBf:=Shf(wBf,c);
+      wBf:=wBf+v;
+      wbc:=wbc+c;
+      IF wbc=32 THEN
+	wrDword(wBf);
+	wBf:=0; wbc:=0;
+      END;
+      RETURN;
+    END;
+    b:=c+wbc-32;
+    h:=Shf(v,-b);
+    wBf:=Shf(wBf,32-wbc)+h;
+    wrDword(wBf);
+    wBf:=v-Shf(h,b);
+    wbc:=b;
+  END;
+END wrSmb;
+
+PROCEDURE flush();	(* write data in buffer *)
+BEGIN
+  WITH ldt^ DO
+    wBf:=Shf(wBf,32-wbc);
+    wrDword(wBf);
+  END;
+END flush;
+
+PROCEDURE getSym() : CHAR; (* find code for first bit sequence in buffer *)
+VAR
+  t,i : CARDINAL;
+  b   : INTEGER;
+BEGIN
+  WITH ldt^ DO
+    IF rbc<=32 THEN
+      rb2:=rdDword();
+      t:=Shf(rb2,-rbc);
+      IF rbc=32 THEN t:=0; END;
+      rb1:=rb1+t;
+      rb2:=Shf(rb2,32-rbc);
+      IF rbc=0 THEN rb2:=0; END;
+      rbc:=rbc+32;
+    END;
+    FOR i:=0 TO 255 DO
+      t:=Shf(rb1,htbl[i].cnt-32);
+      IF t=htbl[i].vl THEN
+	rb1:=Shf(rb1,htbl[i].cnt);
+	b:=32-htbl[i].cnt;
+	t:=Shf(rb2,-b);
+	rb1:=rb1+t;
+	rb2:=Shf(rb2,32-b);
+	rbc:=rbc+b-32;
+	RETURN CHR(i);
+      END;
+    END;
+  END;
+END getSym;
+
+PROCEDURE Insert(s : smbTp); (* insert new character in Huffman's tree *)
+VAR
+  cr : smbTp;
+BEGIN
+  WITH ldt^ DO
+    IF tRoot=NIL THEN
+      cr:=tRoot;
+      tRoot:=s;
+      s^.next:=cr;
+      RETURN;
+    ELSIF tRoot^.n<=s^.n THEN
+      cr:=tRoot;
+      tRoot:=s;
+      s^.next:=cr;
+      RETURN;
+    END;
+    cr:=tRoot;
+    WHILE (cr^.next<>NIL) & (cr^.next^.n>s^.n) DO
+      cr:=cr^.next;
+    END;
+    s^.next:=cr^.next;
+    cr^.next:=s;
+  END;
+END Insert;
+
+PROCEDURE BuildTree(); (* build Huffman's tree *)
+VAR
+  cr,ocr,ncr : smbTp;
+BEGIN
+  WITH ldt^ DO
+    LOOP
+      ocr:=NIL; cr:=tRoot;
+      WHILE cr^.next^.next<>NIL  DO
+	ocr:=cr; cr:=cr^.next;
+      END;
+      NEW(ncr);
+      ncr^.n:=cr^.n+cr^.next^.n;
+      ncr^.left:=cr;
+      ncr^.right:=cr^.next;
+      IF ocr<>NIL THEN
+	ocr^.next:=NIL;
+	Insert(ncr);
+      ELSE
+	tRoot:=NIL;
+	Insert(ncr);
+	EXIT;
+      END;
+    END;
+  END;
+END BuildTree;
+
+PROCEDURE BuildTable(cr: smbTp; vl,n: CARDINAL); (* build table: code -> bit sequence *)
+BEGIN
+  WITH ldt^ DO
+    IF cr^.left=NIL THEN
+      htbl[ORD(cr^.ch)].vl:=vl;
+      htbl[ORD(cr^.ch)].cnt:=n;
+      DISPOSE(cr);
+      RETURN;
+    END;
+    vl:=vl*2;
+    BuildTable(cr^.left,vl,n+1);
+    BuildTable(cr^.right,vl+1,n+1);
+    DISPOSE(cr);
+  END;
+END BuildTable;
+
+PROCEDURE clcTab(); (* build code/bitseq. table from frequency table *)
+VAR
+  i : CARDINAL;
+  s : smbTp;
+BEGIN
+  WITH ldt^ DO
+    tRoot:=NIL;
+    FOR i:=0 TO 255 DO
+      NEW(s);
+      s^.ch:=CHR(i);
+      s^.n:=ftbl[i];
+      s^.left:=NIL; s^.right:=NIL; s^.next:=NIL;
+      Insert(s);
+    END;
+    BuildTree();
+    BuildTable(tRoot,0,0);
+  END;
+END clcTab;
+
+PROCEDURE iniHuf();
+VAR
+  i : CARDINAL;
+BEGIN
+  WITH ldt^ DO
+    FOR i:=0 TO 255 DO
+      ftbl[i]:=1;
+    END;
+    wBf:=0; wbc:=0; rb1:=0; rb2:=0; rbc:=0;
+    smc:=0;
+    clcTab();
+  END;
+END iniHuf;
+
+
+PROCEDURE RawWrite(x: IOLink.DeviceTablePtr; buf: SYSTEM.ADDRESS;
+		len: CARDINAL);
+VAR
+  i	: CARDINAL;
+  ch	: CHAR;
+  cht	: charTap;
+BEGIN
+  IF len = 0 THEN RETURN; END;
+  ldt:=SYSTEM.CAST(lclDataTp,x^.cd);
+  cht:=SYSTEM.CAST(charTap,buf);
+  WITH ldt^ DO
+    FOR i:=0 TO len-1 DO
+      ch:=cht^[i];
+      wrSmb(ch);
+      IF ch = 377C THEN wrSmb(ch); END;
+      ftbl[ORD(ch)]:=ftbl[ORD(ch)]+1; smc:=smc+1;
+      IF smc=rbldFrq THEN
+	clcTab();
+	smc:=0;
+      END;
+    END;
+  END;
+  x^.result:=IOChan.ReadResult(ldt^.chid);
+END RawWrite;
+
+PROCEDURE RawRead(x: IOLink.DeviceTablePtr; buf: SYSTEM.ADDRESS;
+		blen: CARDINAL; VAR len: CARDINAL);
+VAR
+  i	: CARDINAL;
+  cht	: charTap;
+  ch	: CHAR;
+BEGIN
+  ldt:=SYSTEM.CAST(lclDataTp,x^.cd);
+  cht:=SYSTEM.CAST(charTap,buf);
+  IF (blen=0) OR (x^.result<>IOConsts.allRight) THEN len:=0; RETURN; END;
+  WITH ldt^ DO
+    FOR i:=0 TO blen-1 DO
+      ch:=getSym();
+      IF ch = 377C THEN
+	ch:=getSym();
+	IF ch = 0C THEN
+	  x^.result:=IOConsts.endOfInput;
+	  len:=i; cht^[i]:=0C;
+	  RETURN;
+	END;
+      END;
+      cht^[i]:=ch;
+      ftbl[ORD(ch)]:=ftbl[ORD(ch)]+1; smc:=smc+1;
+      IF smc=rbldFrq THEN
+	clcTab();
+	smc:=0;
+      END;
+    END;
+    len:=blen;
+  END;
+END RawRead;
+
+PROCEDURE CreateAlias(VAR cid: ChanId; io: ChanId; VAR res: OpenResults);
+VAR
+  x	: IOLink.DeviceTablePtr;
+BEGIN
+  IOLink.MakeChan(did,cid);
+  IF cid = IOChan.InvalidChan() THEN
+    res:=ChanConsts.outOfChans
+  ELSE
+    NEW(ldt);
+    IF ldt=NIL THEN
+      IOLink.UnMakeChan(did,cid);
+      res:=ChanConsts.outOfChans;
+      RETURN;
+    END;
+    x:=IOLink.DeviceTablePtrValue(cid,did,IOChan.notAvailable,"");
+    ldt^.chid:=io;
+    x^.cd:=ldt;
+    x^.doRawWrite:=RawWrite;
+    x^.doRawRead:=RawRead;
+    res:=ChanConsts.opened;
+    iniHuf();
+    x^.result:=IOConsts.allRight;
+  END;
+END CreateAlias;
+
+PROCEDURE DeleteAlias(VAR cid: ChanId);
+VAR
+  x	: IOLink.DeviceTablePtr;
+BEGIN
+  x:=IOLink.DeviceTablePtrValue(cid,did,IOChan.notAvailable,"");
+  ldt:=x^.cd;
+  IF ldt^.rbc=0 THEN
+    wrSmb(377C);
+    wrSmb(0C);
+    flush();
+  END;
+  DISPOSE(ldt);
+  IOLink.UnMakeChan(did,cid);
+END DeleteAlias;
+
+BEGIN
+  IOLink.AllocateDeviceId(did);
+END HuffChan.

samples/PHP/root.php

@@ -0,0 +1,6 @@
+<?php
+  ////////////////////////////////////
+  // I am not Isabelle ROOT         //
+  ////////////////////////////////////
+
+?>

samples/Perl/strict.t

@@ -1,4 +1,5 @@
 use Test::Base;
+use Test::More;
 
 __DATA__
 === Strict Test

samples/Perl6/test.p6

@@ -73,26 +73,6 @@ Here's some POD!  Wooo
 
 say('this is not!');
 
-=table
-    Of role things
-
-say('not in your table');
-#= A single line declarator "block" (with a keyword like role)
-#| Another single line declarator "block" (with a keyword like role)
-#={
-    A declarator block (with a keyword like role)
-  }
-#|{
-    Another declarator block (with a keyword like role)
-  }
-#= { A single line declarator "block" with a brace (with a keyword like role)
-#=«
-    More declarator blocks! (with a keyword like role)
-  »
-#|«
-    More declarator blocks! (with a keyword like role)
-  »
-
 say 'Moar code!';
 
 my $don't = 16;

samples/SMT/bignum_lia1.smt2

@@ -0,0 +1,20 @@
+(set-logic QF_LIA)
+(set-info :source | SMT-COMP'06 organizers |)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status unsat)
+(set-info :notes |This benchmark is designed to check if the DP supports bignumbers.|)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(declare-fun x4 () Int)
+(declare-fun x5 () Int)
+(declare-fun x6 () Int)
+(assert (and (or (>= x1 1000) (>= x1 1002)) 
+             (or (>= x2 (* 1230 x1)) (>= x2 (* 1003 x1))) 
+			 (or (>= x3 (* 1310 x2)) (>= x3 (* 1999 x2)))
+			 (or (>= x4 (* 4000 x3)) (>= x4 (* 8000 x3))) 
+			 (or (<= x5 (* (- 4000) x4)) (<= x5 (* (- 8000) x4)))
+			 (or (>= x6 (* (- 3) x5)) (>= x6 (* (- 2) x5))) (< x6 0)))
+(check-sat)
+(exit)

samples/SMT/list4.smt2

@@ -0,0 +1,20 @@
+(set-logic AUFLIRA)
+(set-info :source | Buggy list theorem |)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-sort List 0)
+(declare-fun cons (Real List) List)
+(declare-fun nil () List)
+(declare-fun car (List) Real)
+(declare-fun cdr (List) List)
+(declare-fun len (List) Int)
+(assert (forall ((?x Real) (?y List)) (= (car (cons ?x ?y)) ?x)))
+(assert (forall ((?x Real) (?y List)) (= (cdr (cons ?x ?y)) ?y)))
+(assert (= (len nil) 0))
+(assert (forall ((?x Real) (?y List)) (= (len (cons ?x ?y)) (+ (len ?y) 1))))
+(declare-fun append (List List) List)
+(assert (forall ((?x Real) (?y1 List) (?y2 List)) (= (append (cons ?x ?y1) ?y2) (cons ?x (append ?y1 ?y2)))))
+(assert (not (forall ((?x Real) (?y List)) (= (append (cons ?x nil) ?y) (cons ?x ?y)))))
+(check-sat)
+(exit)

samples/SMT/queen10-1.smt2

@@ -0,0 +1,123 @@
+(set-logic QF_IDL)
+(set-info :source |
+Queens benchmarks generated by Hyondeuk Kim in SMT-LIB format.
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun x0 () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(declare-fun x4 () Int)
+(declare-fun x5 () Int)
+(declare-fun x6 () Int)
+(declare-fun x7 () Int)
+(declare-fun x8 () Int)
+(declare-fun x9 () Int)
+(declare-fun x10 () Int)
+(assert 
+  (let 
+    ((?v_0 (- x0 x10)) 
+     (?v_1 (- x1 x10)) 
+     (?v_2 (- x2 x10))
+     (?v_3 (- x3 x10))
+     (?v_4 (- x4 x10))
+     (?v_5 (- x5 x10))
+     (?v_6 (- x6 x10))
+     (?v_7 (- x7 x10))
+     (?v_8 (- x8 x10)) 
+     (?v_9 (- x9 x10)) 
+     (?v_10 (- x0 x1))
+     (?v_11 (- x0 x2))
+     (?v_12 (- x0 x3)) 
+     (?v_13 (- x0 x4))
+     (?v_14 (- x0 x5))
+     (?v_15 (- x0 x6))
+     (?v_16 (- x0 x7))
+     (?v_17 (- x0 x8))
+     (?v_18 (- x0 x9))
+     (?v_19 (- x1 x2))
+     (?v_20 (- x1 x3))
+     (?v_21 (- x1 x4))
+     (?v_22 (- x1 x5))
+     (?v_23 (- x1 x6))
+     (?v_24 (- x1 x7)) 
+     (?v_25 (- x1 x8)) 
+     (?v_26 (- x1 x9))
+     (?v_27 (- x2 x3)) 
+     (?v_28 (- x2 x4))
+     (?v_29 (- x2 x5))
+     (?v_30 (- x2 x6))
+     (?v_31 (- x2 x7))
+     (?v_32 (- x2 x8))
+     (?v_33 (- x2 x9))
+     (?v_34 (- x3 x4))
+     (?v_35 (- x3 x5))
+     (?v_36 (- x3 x6))
+     (?v_37 (- x3 x7))
+     (?v_38 (- x3 x8))
+     (?v_39 (- x3 x9))
+     (?v_40 (- x4 x5))
+     (?v_41 (- x4 x6))
+     (?v_42 (- x4 x7))
+     (?v_43 (- x4 x8))
+     (?v_44 (- x4 x9))
+     (?v_45 (- x5 x6))
+     (?v_46 (- x5 x7))
+     (?v_47 (- x5 x8)) 
+     (?v_48 (- x5 x9))
+     (?v_49 (- x6 x7))
+     (?v_50 (- x6 x8))
+     (?v_51 (- x6 x9))
+     (?v_52 (- x7 x8))
+     (?v_53 (- x7 x9)) 
+     (?v_54 (- x8 x9))) 
+  (and (<= ?v_0 9) (>= ?v_0 0) (<= ?v_1 9) (>= ?v_1 0) (<= ?v_2 9) (>= ?v_2 0) 
+       (<= ?v_3 9) (>= ?v_3 0) (<= ?v_4 9) (>= ?v_4 0) (<= ?v_5 9) (>= ?v_5 0) 
+       (<= ?v_6 9) (>= ?v_6 0) (<= ?v_7 9) (>= ?v_7 0) (<= ?v_8 9) (>= ?v_8 0) 
+       (<= ?v_9 9) (>= ?v_9 0)
+       (not (= x0 x1)) (not (= x0 x2)) (not (= x0 x3)) (not (= x0 x4))
+       (not (= x0 x5)) (not (= x0 x6)) (not (= x0 x7)) (not (= x0 x8)) 
+       (not (= x0 x9)) (not (= x1 x2)) (not (= x1 x3)) (not (= x1 x4)) 
+       (not (= x1 x5)) (not (= x1 x6)) (not (= x1 x7)) (not (= x1 x8)) 
+       (not (= x1 x9)) (not (= x2 x3)) (not (= x2 x4)) (not (= x2 x5)) 
+       (not (= x2 x6)) (not (= x2 x7)) (not (= x2 x8)) (not (= x2 x9))
+       (not (= x3 x4)) (not (= x3 x5)) (not (= x3 x6)) (not (= x3 x7)) 
+       (not (= x3 x8)) (not (= x3 x9)) (not (= x4 x5)) (not (= x4 x6)) 
+       (not (= x4 x7)) (not (= x4 x8)) (not (= x4 x9)) (not (= x5 x6)) 
+       (not (= x5 x7)) (not (= x5 x8)) (not (= x5 x9)) (not (= x6 x7)) 
+       (not (= x6 x8)) (not (= x6 x9)) (not (= x7 x8)) (not (= x7 x9)) 
+       (not (= x8 x9)) 
+       (not (= ?v_10 1)) (not (= ?v_10 (- 1))) (not (= ?v_11 2)) 
+       (not (= ?v_11 (- 2))) (not (= ?v_12 3)) (not (= ?v_12 (- 3))) 
+       (not (= ?v_13 4)) (not (= ?v_13 (- 4))) (not (= ?v_14 5)) 
+       (not (= ?v_14 (- 5))) (not (= ?v_15 6)) (not (= ?v_15 (- 6)))
+       (not (= ?v_16 7)) (not (= ?v_16 (- 7))) (not (= ?v_17 8)) 
+       (not (= ?v_17 (- 8))) (not (= ?v_18 9)) (not (= ?v_18 (- 9))) 
+       (not (= ?v_19 1)) (not (= ?v_19 (- 1))) (not (= ?v_20 2)) 
+       (not (= ?v_20 (- 2))) (not (= ?v_21 3)) (not (= ?v_21 (- 3))) 
+       (not (= ?v_22 4)) (not (= ?v_22 (- 4))) (not (= ?v_23 5)) 
+       (not (= ?v_23 (- 5))) (not (= ?v_24 6)) (not (= ?v_24 (- 6))) 
+       (not (= ?v_25 7)) (not (= ?v_25 (- 7))) (not (= ?v_26 8)) 
+       (not (= ?v_26 (- 8))) (not (= ?v_27 1)) (not (= ?v_27 (- 1))) 
+       (not (= ?v_28 2)) (not (= ?v_28 (- 2))) (not (= ?v_29 3)) 
+       (not (= ?v_29 (- 3))) (not (= ?v_30 4)) (not (= ?v_30 (- 4))) 
+       (not (= ?v_31 5)) (not (= ?v_31 (- 5))) (not (= ?v_32 6))
+       (not (= ?v_32 (- 6))) (not (= ?v_33 7)) (not (= ?v_33 (- 7))) 
+       (not (= ?v_34 1)) (not (= ?v_34 (- 1))) (not (= ?v_35 2)) 
+       (not (= ?v_35 (- 2))) (not (= ?v_36 3)) (not (= ?v_36 (- 3)))
+       (not (= ?v_37 4)) (not (= ?v_37 (- 4))) (not (= ?v_38 5)) 
+       (not (= ?v_38 (- 5))) (not (= ?v_39 6)) (not (= ?v_39 (- 6))) 
+       (not (= ?v_40 1)) (not (= ?v_40 (- 1))) (not (= ?v_41 2)) 
+       (not (= ?v_41 (- 2))) (not (= ?v_42 3)) (not (= ?v_42 (- 3)))
+       (not (= ?v_43 4)) (not (= ?v_43 (- 4))) (not (= ?v_44 5))
+       (not (= ?v_44 (- 5))) (not (= ?v_45 1)) (not (= ?v_45 (- 1))) 
+       (not (= ?v_46 2)) (not (= ?v_46 (- 2))) (not (= ?v_47 3)) 
+       (not (= ?v_47 (- 3))) (not (= ?v_48 4)) (not (= ?v_48 (- 4))) 
+       (not (= ?v_49 1)) (not (= ?v_49 (- 1))) (not (= ?v_50 2)) 
+       (not (= ?v_50 (- 2))) (not (= ?v_51 3)) (not (= ?v_51 (- 3))) 
+       (not (= ?v_52 1)) (not (= ?v_52 (- 1))) (not (= ?v_53 2)) 
+       (not (= ?v_53 (- 2))) (not (= ?v_54 1)) (not (= ?v_54 (- 1))))))
+(check-sat)
+(exit)

samples/XML/xhtml-struct-1.mod

@@ -0,0 +1,125 @@
+<!-- ...................................................................... -->
+<!-- XHTML Structure Module  .............................................. -->
+<!-- file: xhtml-struct-1.mod
+
+     This is XHTML, a reformulation of HTML as a modular XML application.
+     Copyright 1998-2000 W3C (MIT, INRIA, Keio), All Rights Reserved.
+     Revision: $Id: xhtml-struct-1.mod,v 1.1.1.1 2006/01/09 19:23:30 rcrews Exp $ SMI
+
+     This DTD module is identified by the PUBLIC and SYSTEM identifiers:
+
+       PUBLIC "-//W3C//ELEMENTS XHTML Document Structure 1.0//EN"
+       SYSTEM "http://www.w3.org/TR/xhtml-modulatization/DTD/xhtml-struct-1.mod"
+
+     Revisions:
+     (none)
+     ....................................................................... -->
+
+<!-- Document Structure
+
+        title, head, body, html
+
+     The Structure Module defines the major structural elements and 
+     their attributes.
+
+     Note that the content model of the head element type is redeclared 
+     when the Base Module is included in the DTD.
+
+     The parameter entity containing the XML namespace URI value used 
+     for XHTML is '%XHTML.xmlns;', defined in the Qualified Names module.
+-->
+
+<!-- title: Document Title ............................. -->
+
+<!-- The title element is not considered part of the flow of text.
+     It should be displayed, for example as the page header or
+     window title. Exactly one title is required per document.
+-->
+
+<!ENTITY % title.element  "INCLUDE" >
+<![%title.element;[
+<!ENTITY % title.content  "( #PCDATA )" >
+<!ENTITY % title.qname  "title" >
+<!ELEMENT %title.qname;  %title.content; >
+<!-- end of title.element -->]]>
+
+<!ENTITY % title.attlist  "INCLUDE" >
+<![%title.attlist;[
+<!ATTLIST %title.qname;
+      %XHTML.xmlns.attrib; 
+      %I18n.attrib;
+>
+<!-- end of title.attlist -->]]>
+
+<!-- head: Document Head ............................... -->
+
+<!ENTITY % head.element  "INCLUDE" >
+<![%head.element;[
+<!ENTITY % head.content
+    "( %HeadOpts.mix;, %title.qname;, %HeadOpts.mix; )"
+>
+<!ENTITY % head.qname  "head" >
+<!ELEMENT %head.qname;  %head.content; >
+<!-- end of head.element -->]]>
+
+<!ENTITY % head.attlist  "INCLUDE" >
+<![%head.attlist;[
+<!-- reserved for future use with document profiles
+-->
+<!ENTITY % profile.attrib
+     "profile      %URI.datatype;           '%XHTML.profile;'"
+>
+
+<!ATTLIST %head.qname;
+      %XHTML.xmlns.attrib; 
+      %I18n.attrib;
+      %profile.attrib;
+>
+<!-- end of head.attlist -->]]>
+
+<!-- body: Document Body ............................... -->
+
+<!ENTITY % body.element  "INCLUDE" >
+<![%body.element;[
+<!ENTITY % body.content
+     "( %Block.mix; )+"
+>
+<!ENTITY % body.qname  "body" >
+<!ELEMENT %body.qname;  %body.content; >
+<!-- end of body.element -->]]>
+
+<!ENTITY % body.attlist  "INCLUDE" >
+<![%body.attlist;[
+<!ATTLIST %body.qname;
+      %Common.attrib;
+>
+<!-- end of body.attlist -->]]>
+
+<!-- html: XHTML Document Element ...................... -->
+
+<!ENTITY % html.element  "INCLUDE" >
+<![%html.element;[
+<!ENTITY % html.content  "( %head.qname;, %body.qname; )" >
+<!ENTITY % html.qname  "html" >
+<!ELEMENT %html.qname;  %html.content; >
+<!-- end of html.element -->]]>
+
+<!ENTITY % html.attlist  "INCLUDE" >
+<![%html.attlist;[
+<!-- version attribute value defined in driver
+-->
+<!ENTITY % XHTML.version.attrib
+     "version      %FPI.datatype;           #FIXED '%XHTML.version;'"
+>
+
+<!-- see the Qualified Names module for information 
+     on how to extend XHTML using XML namespaces 
+-->
+<!ATTLIST %html.qname;
+      %XHTML.xmlns.attrib; 
+      %XHTML.version.attrib;
+      %I18n.attrib;
+>
+<!-- end of html.attlist -->]]>
+
+<!-- end of xhtml-struct-1.mod -->