Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
cduce
cduce
Commits
d82aa4fb
Commit
d82aa4fb
authored
Oct 05, 2007
by
Pietro Abate
Browse files
[r2005-05-07 20:13:53 by afrisch] Simplification
Original author: afrisch Date: 2005-05-07 20:13:54+00:00
parent
9c9b2bde
Changes
6
Hide whitespace changes
Inline
Side-by-side
Makefile.distrib
View file @
d82aa4fb
...
...
@@ -142,7 +142,8 @@ OBJECTS = \
driver/config.cmo
\
misc/stats.cmo
\
misc/serialize.cmo misc/custom.cmo
\
misc/state.cmo misc/pool.cmo misc/encodings.cmo misc/bool.cmo
\
misc/state.cmo misc/pool.cmo misc/encodings.cmo misc/myweak.cmo
\
misc/bool.cmo
\
misc/pretty.cmo misc/ns.cmo misc/inttbl.cmo misc/imap.cmo
\
misc/html.cmo
\
\
...
...
depend
View file @
d82aa4fb
...
...
@@ -14,8 +14,14 @@ misc/pool.cmx: misc/state.cmx misc/serialize.cmx misc/custom.cmx \
misc/pool.cmi
misc/encodings.cmo: misc/serialize.cmi misc/custom.cmo misc/encodings.cmi
misc/encodings.cmx: misc/serialize.cmx misc/custom.cmx misc/encodings.cmi
misc/bool.cmo: misc/serialize.cmi misc/custom.cmo misc/bool.cmi
misc/bool.cmx: misc/serialize.cmx misc/custom.cmx misc/bool.cmi
misc/myweak.cmo: misc/myweak.cmi
misc/myweak.cmx: misc/myweak.cmi
misc/memo.cmo: misc/memo.cmi
misc/memo.cmx: misc/memo.cmi
misc/bool.cmo: misc/serialize.cmi misc/myweak.cmi misc/memo.cmi \
misc/custom.cmo misc/bool.cmi
misc/bool.cmx: misc/serialize.cmx misc/myweak.cmx misc/memo.cmx \
misc/custom.cmx misc/bool.cmi
misc/pretty.cmo: misc/pretty.cmi
misc/pretty.cmx: misc/pretty.cmi
misc/ns.cmo: misc/state.cmi misc/serialize.cmi misc/pool.cmi \
...
...
@@ -115,9 +121,9 @@ typing/typed.cmo: types/types.cmi types/patterns.cmi misc/ns.cmi \
typing/typed.cmx: types/types.cmx types/patterns.cmx misc/ns.cmx \
parser/location.cmx types/ident.cmx
typing/typepat.cmo: types/types.cmi types/sequence.cmi types/patterns.cmi \
parser/location.cmi
types/ident.cmo types/chars.cmi typing/typepat.cmi
types/ident.cmo types/chars.cmi typing/typepat.cmi
typing/typepat.cmx: types/types.cmx types/sequence.cmx types/patterns.cmx \
parser/location.cmx
types/ident.cmx types/chars.cmx typing/typepat.cmi
types/ident.cmx types/chars.cmx typing/typepat.cmi
typing/typer.cmo: types/types.cmi typing/typepat.cmi typing/typed.cmo \
misc/serialize.cmi types/sequence.cmi types/patterns.cmi misc/ns.cmi \
parser/location.cmi types/ident.cmo misc/html.cmi types/externals.cmi \
...
...
@@ -173,14 +179,14 @@ schema/schema_parser.cmx: parser/url.cmx schema/schema_xml.cmx \
schema/schema_pcre.cmx schema/schema_common.cmx schema/schema_builtin.cmx \
misc/ns.cmx misc/encodings.cmx types/atoms.cmx schema/schema_parser.cmi
schema/schema_converter.cmo: runtime/value.cmi types/types.cmi \
typing/typer.cmi typ
es/sequence.cmi schema/schema_xml
.cmi \
schema/schema_validator.cmi schema/schema_types.cmi \
typing/typer.cmi typ
ing/typepat.cmi types/sequence
.cmi \
schema/schema_xml.cmi
schema/schema_validator.cmi schema/schema_types.cmi \
schema/schema_parser.cmi schema/schema_common.cmi \
schema/schema_builtin.cmi misc/ns.cmi types/ident.cmo misc/encodings.cmi \
types/builtin_defs.cmi types/atoms.cmi
schema/schema_converter.cmx: runtime/value.cmx types/types.cmx \
typing/typer.cmx typ
es/sequence.cmx schema/schema_xml
.cmx \
schema/schema_validator.cmx schema/schema_types.cmx \
typing/typer.cmx typ
ing/typepat.cmx types/sequence
.cmx \
schema/schema_xml.cmx
schema/schema_validator.cmx schema/schema_types.cmx \
schema/schema_parser.cmx schema/schema_common.cmx \
schema/schema_builtin.cmx misc/ns.cmx types/ident.cmx misc/encodings.cmx \
types/builtin_defs.cmx types/atoms.cmx
...
...
@@ -284,14 +290,6 @@ ocamliface/mlstub.cmx: types/types.cmx typing/typer.cmx types/sequence.cmx \
driver/librarian.cmx types/ident.cmx types/externals.cmx \
driver/config.cmx compile/compile.cmx types/builtin_defs.cmx \
types/atoms.cmx ocamliface/mlstub.cmi
parser/cduce_curl.cmo: parser/url.cmi driver/config.cmi
parser/cduce_curl.cmx: parser/url.cmx driver/config.cmx
runtime/cduce_pxp.cmo: parser/url.cmi schema/schema_xml.cmi \
parser/location.cmi runtime/load_xml.cmi driver/config.cmi \
runtime/cduce_pxp.cmi
runtime/cduce_pxp.cmx: parser/url.cmx schema/schema_xml.cmx \
parser/location.cmx runtime/load_xml.cmx driver/config.cmx \
runtime/cduce_pxp.cmi
runtime/cduce_expat.cmo: parser/url.cmi schema/schema_xml.cmi \
parser/location.cmi runtime/load_xml.cmi driver/config.cmi \
runtime/cduce_expat.cmi
...
...
@@ -380,6 +378,7 @@ runtime/value.cmi: types/types.cmi misc/ns.cmi compile/lambda.cmi \
parser/location.cmi: misc/html.cmi
parser/parser.cmi: parser/ast.cmo
types/externals.cmi: types/types.cmi
typing/typepat.cmi: types/types.cmi types/patterns.cmi types/ident.cmo
typing/typer.cmi: runtime/value.cmi types/types.cmi typing/typed.cmo \
misc/serialize.cmi types/patterns.cmi misc/ns.cmi parser/location.cmi \
types/ident.cmo parser/ast.cmo
...
...
misc/bool.ml
View file @
d82aa4fb
...
...
@@ -18,13 +18,17 @@ sig
->
cap
:
(
'
b
->
'
b
->
'
b
)
->
diff
:
(
'
b
->
'
b
->
'
b
)
->
atom
:
(
elem
->
'
b
)
->
t
->
'
b
(*
val print: string -> (Format.formatter -> elem -> unit) -> t ->
(Format.formatter -> unit) list
*)
val
trivially_disjoint
:
t
->
t
->
bool
end
module
MakeOld
(
X
:
Custom
.
T
)
=
module
type
MAKE
=
functor
(
X
:
Custom
.
T
)
->
S
with
type
elem
=
X
.
t
module
Make
(
X
:
Custom
.
T
)
=
struct
type
elem
=
X
.
t
type
t
=
...
...
@@ -94,8 +98,8 @@ struct
|
True
->
Format
.
fprintf
ppf
"+"
|
False
->
Format
.
fprintf
ppf
"-"
|
Split
(
_
,
x
,
p
,
i
,
n
)
->
Format
.
fprintf
ppf
"%
a
(@[%a,%a,%a@])"
X
.
dump
x
dump
p
dump
i
dump
n
Format
.
fprintf
ppf
"%
i
(@[%a,%a,%a@])"
(*
X.dump x
*)
(
X
.
hash
x
)
dump
p
dump
i
dump
n
let
rec
print
f
ppf
=
function
...
...
@@ -394,7 +398,12 @@ struct
end
module
Make
(
X
:
Custom
.
T
)
=
module
type
S'
=
sig
include
S
type
bdd
=
False
|
True
|
Br
of
elem
*
t
*
t
val
br
:
t
->
bdd
end
module
MakeBdd
(
X
:
Custom
.
T
)
=
struct
type
elem
=
X
.
t
type
t
=
...
...
@@ -414,7 +423,7 @@ struct
(* Internalization + detection of useless branching *)
let
max_id
=
ref
2
(* Must be >= 2 *)
module
W
=
W
eak
.
Make
(
module
W
=
Myw
eak
.
Make
(
struct
type
t
=
node
...
...
@@ -478,6 +487,21 @@ struct
else
memo_occ
.
(
h
)
<-
pred
i
;
r
let
rec
dump
ppf
=
function
|
One
->
Format
.
fprintf
ppf
"+"
|
Zero
->
Format
.
fprintf
ppf
"-"
|
Branch
(
x
,
p
,
n
,
id
,_
)
->
Format
.
fprintf
ppf
"%i:%a(@[%a,%a@])"
id
X
.
dump
x
dump
p
dump
n
(*
let cup x y =
let d = cup x y in
Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX+Z = %a@\n"
dump x dump y dump d;
d
*)
let
cap
x1
x2
=
neg
(
cup
(
neg
x1
)
(
neg
x2
))
...
...
@@ -488,12 +512,6 @@ struct
|
Branch
(
x
,
p
,
n
,_,_
)
->
f
x
;
iter
f
p
;
iter
f
n
|
_
->
()
let
rec
dump
ppf
=
function
|
One
->
Format
.
fprintf
ppf
"+"
|
Zero
->
Format
.
fprintf
ppf
"-"
|
Branch
(
x
,
p
,
n
,_,_
)
->
Format
.
fprintf
ppf
"%a(@[%a,%a@])"
X
.
dump
x
dump
p
dump
n
let
rec
print
f
ppf
=
function
...
...
@@ -569,4 +587,518 @@ struct
let
equal
x
y
=
x
==
y
let
hash
x
=
id
x
let
check
x
=
()
type
bdd
=
False
|
True
|
Br
of
elem
*
t
*
t
let
br
=
function
|
Zero
->
False
|
One
->
True
|
Branch
(
x
,
p
,
n
,_,_
)
->
Br
(
x
,
p
,
n
)
end
module
Simplify
(
M
:
MAKE
)(
X
:
Custom
.
T
)
=
struct
module
B
=
M
(
X
)
type
elem
=
X
.
t
type
f
=
{
vars
:
(
X
.
t
*
bool
)
list
;
(* toplevel vars and their polarity *)
subs
:
f
list
;
(* subformulas *)
allvars
:
(
X
.
t
*
int
*
int
)
list
;
(* # of pos,neg occurences *)
mutable
form
:
B
.
t
option
;
mutable
id
:
int
(* unique id for hash consing *)
}
type
t
=
f
let
tmpl
=
{
vars
=
[]
;
subs
=
[]
;
allvars
=
[]
;
form
=
None
;
id
=
0
}
let
print
px
=
let
allvars
ppf
f
=
List
.
iter
(
fun
(
x
,
p
,
n
)
->
Format
.
fprintf
ppf
"[%a:%i,%i]"
px
x
p
n
)
f
.
allvars
in
let
rec
aux
ppf
f
=
(* Format.fprintf ppf "{%i}" f.id; *)
(* (match f.form with Some _ -> Format.fprintf ppf "*" | _ -> ()); *)
(* allvars ppf f; *)
let
first
=
ref
true
in
let
sep
()
=
if
!
first
then
first
:=
false
else
Format
.
fprintf
ppf
"|"
in
List
.
iter
(
function
|
(
x
,
true
)
->
sep
()
;
Format
.
fprintf
ppf
"%a"
px
x
|
(
x
,
false
)
->
sep
()
;
Format
.
fprintf
ppf
"~%a"
px
x
)
f
.
vars
;
List
.
iter
(
fun
f
->
sep
()
;
Format
.
fprintf
ppf
"~(@[%a@])"
aux
f
)
f
.
subs
;
if
!
first
then
Format
.
fprintf
ppf
"."
in
fun
ppf
f
->
(*allvars ppf f; *)
aux
ppf
f
let
dump
=
print
(*X.dump*)
(
fun
ppf
i
->
Format
.
fprintf
ppf
"%i"
(
X
.
hash
i
))
let
rec
cup_vars
vars1
vars2
=
match
(
vars1
,
vars2
)
with
|
((
x1
,
p1
,
n1
)
as
z1
)
::
vars1'
,
((
x2
,
p2
,
n2
)
as
z2
)
::
vars2'
->
let
c
=
X
.
compare
x1
x2
in
if
c
=
0
then
(
x1
,
p1
+
p2
,
n1
+
n2
)
::
(
cup_vars
vars1'
vars2'
)
else
if
c
<
0
then
z1
::
(
cup_vars
vars1'
vars2
)
else
z2
::
(
cup_vars
vars1
vars2'
)
|
vars
,
[]
|
[]
,
vars
->
vars
let
occ
(
x1
,
x1v
)
=
if
x1v
then
(
x1
,
1
,
0
)
else
(
x1
,
0
,
1
)
let
rec
cup_vars'
vars1
vars2
=
match
(
vars1
,
vars2
)
with
|
(
x1
,
x1v
)
::
vars1'
,
(
x2
,
p2
,
n2
)
::
vars2'
->
let
c
=
X
.
compare
x1
x2
in
if
c
=
0
then
assert
false
(* x1::(cup_vars' vars1' vars2') *)
else
if
c
<
0
then
(
if
x1v
then
(
x1
,
1
,
0
)
else
(
x1
,
0
,
1
))
::
(
cup_vars'
vars1'
vars2
)
else
(
x2
,
n2
,
p2
)
::
(
cup_vars'
vars1
vars2'
)
|
vars
,
[]
->
List
.
map
occ
vars
|
[]
,
vars
->
List
.
map
(
fun
(
x
,
p
,
n
)
->
(
x
,
n
,
p
))
vars
let
compute_allvars
subs
vars
=
cup_vars'
vars
(
List
.
fold_left
(
fun
accu
f
->
cup_vars
accu
f
.
allvars
)
[]
subs
)
let
rec
cap_vars
vars1
vars2
=
match
(
vars1
,
vars2
)
with
|
((
x1
,
xv1
)
as
z1
)
::
vars1'
,
(
x2
,_,_
)
::
vars2'
->
let
c
=
X
.
compare
x1
x2
in
if
c
=
0
then
z1
::
(
cap_vars
vars1'
vars2'
)
else
if
c
<
0
then
cap_vars
vars1'
vars2
else
cap_vars
vars1
vars2'
|
_
->
[]
let
rec
csubs
s1
s2
=
match
s1
,
s2
with
|
f1
::
s1'
,
f2
::
s2'
->
if
f1
==
f2
then
f1
::
(
csubs
s1'
s2'
)
else
if
f1
.
id
<
f2
.
id
then
f1
::
(
csubs
s1'
s2
)
else
f2
::
(
csubs
s1
s2'
)
|
[]
,
[]
->
[]
|
s
,
[]
|
[]
,
s
->
s
let
print_vars
v
=
List
.
iter
(
fun
(
x
,
b
)
->
Printf
.
printf
"[%i:%b]"
(
X
.
hash
x
)
b
)
v
;
print_newline
()
module
H
=
struct
type
t
=
f
let
rec
hash_vars
accu
=
function
|
(
x
,
v
)
::
r
->
hash_vars
(
65537
*
accu
+
257
*
X
.
hash
x
+
(
if
v
then
1
else
0
))
r
|
[]
->
accu
let
rec
hash_subs
accu
=
function
|
f
::
r
->
hash_subs
(
257
*
accu
+
f
.
id
)
r
|
[]
->
accu
let
hash
f
=
hash_vars
(
hash_subs
1
f
.
subs
)
f
.
vars
(*
let rec equal_vars vars1 vars2 = vars1 == vars2 || match vars1,vars2 with
| (x1,xv1)::(x1',xv1')::vars1,(x2,xv2)::(x2',xv2')::vars2 ->
xv1 == xv2 && xv1' == xv2' && X.equal x1 x2 &&
X.equal x1' x2' && equal_vars vars1 vars2
| [(x1,xv1)],[(x2,xv2)] ->
xv1 == xv2 && X.equal x1 x2
| _ -> false *)
let
rec
equal_vars
vars1
vars2
=
vars1
==
vars2
||
match
vars1
,
vars2
with
|
(
x1
,
xv1
)
::
vars1
,
(
x2
,
xv2
)
::
vars2
->
xv1
==
xv2
&&
X
.
equal
x1
x2
&&
equal_vars
vars1
vars2
|
_
->
false
let
rec
equal_subs
s1
s2
=
s1
==
s2
||
match
s1
,
s2
with
|
f1
::
s1
,
f2
::
s2
->
f1
==
f2
&&
equal_subs
s1
s2
|
_
->
false
let
equal
f1
f2
=
(
f1
==
f2
)
||
((
f1
.
id
=
0
||
f2
.
id
=
0
)
&&
equal_vars
f1
.
vars
f2
.
vars
&&
equal_subs
f1
.
subs
f2
.
subs
)
end
module
W
=
Myweak
.
Make
(
H
)
let
mk
=
let
tbl
=
W
.
create
16387
in
let
id
=
ref
0
in
fun
f
->
if
(
f
.
id
!=
0
)
then
f
else
let
f
=
W
.
merge
tbl
f
in
if
(
f
.
id
=
0
)
then
f
.
id
<-
(
incr
id
;
!
id
);
f
let
empty
=
mk
{
tmpl
with
subs
=
[]
}
let
full
=
mk
{
tmpl
with
subs
=
[
empty
]
}
let
check
f
=
()
let
posvar
x
=
mk
{
tmpl
with
vars
=
[
x
,
true
];
allvars
=
[
x
,
1
,
0
]
}
let
negvar
x
=
mk
{
tmpl
with
vars
=
[
x
,
false
];
allvars
=
[
x
,
0
,
1
]
}
let
neg
=
function
|
{
vars
=
[
x
,
true
];
subs
=
[]
}
->
negvar
x
|
{
vars
=
[
x
,
false
];
subs
=
[]
}
->
posvar
x
|
{
vars
=
[]
;
subs
=
[
f
]
}
->
f
|
f
->
mk
{
tmpl
with
allvars
=
List
.
map
(
fun
(
x
,
p
,
n
)
->
(
x
,
n
,
p
))
f
.
allvars
;
subs
=
[
f
]
}
let
has_complement
f1
f2
=
List
.
memq
f2
f1
.
subs
let
is_complement
f1
f2
=
match
f1
with
|
{
vars
=
[]
;
subs
=
[
f
]
}
->
f
==
f2
|
_
->
match
f2
with
|
{
vars
=
[]
;
subs
=
[
f
]
}
->
f
==
f1
|
_
->
false
exception
One
type
memo
=
{
key1
:
int
array
;
key2
:
int
array
;
res
:
t
array
}
let
new_memo
n
=
{
key1
=
Array
.
create
n
(
-
1
);
key2
=
Array
.
create
n
(
-
1
);
res
=
Array
.
create
n
empty
}
let
memo_cup
=
new_memo
16383
let
memo_cap
=
new_memo
16383
let
filrat
tbl
=
let
o
=
ref
0
in
Array
.
iter
(
fun
i
->
if
i
>=
0
then
incr
o
)
tbl
.
key1
;
!
o
let
memo_bin
tbl
g
f1
f2
=
let
h
=
((
f1
.
id
+
1027
*
f2
.
id
)
land
max_int
)
mod
(
Array
.
length
tbl
.
res
)
in
if
(
tbl
.
key1
.
(
h
)
==
f1
.
id
)
&&
(
tbl
.
key2
.
(
h
)
==
f2
.
id
)
then
tbl
.
res
.
(
h
)
else
let
r
=
g
(
f1
,
f2
)
in
tbl
.
key1
.
(
h
)
<-
f1
.
id
;
tbl
.
key2
.
(
h
)
<-
f2
.
id
;
tbl
.
res
.
(
h
)
<-
r
;
r
let
rec
cvars
vars1
vars2
=
match
(
vars1
,
vars2
)
with
|
((
x1
,
xv1
)
as
z1
)
::
vars1'
,
((
x2
,
xv2
)
as
z2
)
::
vars2'
->
let
c
=
X
.
compare
x1
x2
in
if
c
=
0
then
if
xv1
==
xv2
then
z1
::
(
cvars
vars1'
vars2'
)
else
raise
One
else
if
c
<
0
then
z1
::
(
cvars
vars1'
vars2
)
else
z2
::
(
cvars
vars1
vars2'
)
|
vars
,
[]
|
[]
,
vars
->
vars
let
mk_vs
vars
subs
=
mk
{
tmpl
with
vars
=
vars
;
allvars
=
compute_allvars
subs
vars
;
subs
=
subs
}
let
rec
split_vars
vars1
vars2
=
match
vars1
,
vars2
with
|
((
x1
,
xv1
)
as
z1
)
::
vars1'
,
((
x2
,
xv2
)
as
z2
)
::
vars2'
->
let
c
=
X
.
compare
x1
x2
in
if
c
=
0
then
let
(
vars1
,
common
,
vars2
)
=
split_vars
vars1'
vars2'
in
if
xv1
==
xv2
then
(
vars1
,
z1
::
common
,
vars2
)
else
(
z1
::
vars1
,
common
,
z2
::
vars2
)
else
if
c
<
0
then
let
(
vars1
,
common
,
vars2
)
=
split_vars
vars1'
vars2
in
z1
::
vars1
,
common
,
vars2
else
let
(
vars1
,
common
,
vars2
)
=
split_vars
vars1
vars2'
in
vars1
,
common
,
z2
::
vars2
|
vars1
,
vars2
->
vars1
,
[]
,
vars2
let
rec
split_subs
s1
s2
=
match
s1
,
s2
with
|
f1
::
s1'
,
f2
::
s2'
->
if
f1
==
f2
then
let
(
s1
,
common
,
s2
)
=
split_subs
s1'
s2'
in
(
s1
,
f1
::
common
,
s2
)
else
if
f1
.
id
<
f2
.
id
then
let
(
s1
,
common
,
s2
)
=
split_subs
s1'
s2
in
f1
::
s1
,
common
,
s2
else
let
(
s1
,
common
,
s2
)
=
split_subs
s1
s2'
in
s1
,
common
,
f2
::
s2
|
s1
,
s2
->
s1
,
[]
,
s2
let
order_subs
subs
=
let
rec
clean
=
function
|
f1
::
(
f2
::_
as
z
)
->
if
f1
==
f2
then
clean
z
else
f1
::
(
clean
z
)
|
z
->
z
in
clean
(
List
.
sort
(
fun
f1
f2
->
f1
.
id
-
f2
.
id
)
subs
)
let
rec
remove_complement
f
c
=
let
rec
aux
=
function
|
c'
::
r
->
if
(
c
==
c'
)
then
r
else
c'
::
(
aux
r
)
|
_
->
assert
false
in
vars_subs
f
.
vars
(
aux
f
.
subs
)
and
simplify_subs
subs
=
(* TODO: avoid quadratic behavior by pre-detecting collisions in one pass *)
let
rec
aux
f1
=
function
|
[]
->
[
f1
]
|
f2
::
s
->
let
(
vars1
,
vars
,
vars2
)
=
split_vars
f1
.
vars
f2
.
vars
in
let
(
subs1
,
subs
,
subs2
)
=
split_subs
f1
.
subs
f2
.
subs
in
if
vars
=
[]
&&
subs
=
[]
then
if
has_complement
f2
f1
then
(
remove_complement
f2
f1
)
::
(
aux
f1
s
)
else
if
has_complement
f1
f2
then
f2
::
(
aux
(
remove_complement
f1
f2
)
s
)
else
f2
::
(
aux
f1
s
)
else
(
let
f1'
=
mk_vs
vars1
subs1
in
let
f2'
=
mk_vs
vars2
subs2
in
let
f
=
mk_vs
vars
subs
in
let
f'
=
cup
f
(
cap
f1'
f2'
)
in
(* Format.fprintf Format.std_formatter
"MERGE %a+%a==>%a@." dump f1 dump f2 dump f'; *)
if
f'
==
full
then
s
else
aux
f'
s
)
in
if
subs
=
[]
then
[]
else
let
subs
=
List
.
fold_left
(
fun
accu
f
->
aux
f
accu
)
[]
subs
in
order_subs
subs
and
vars_subs
vars
subs
=
let
subs
=
simplify_subs
subs
in
let
extra
=
ref
[]
in
let
rec
aux
=
function
|
[]
->
[]
|
{
vars
=
[
x
,
v
];
subs
=
[]
}
::
s
->
extra
:=
(
x
,
not
v
)
::!
extra
;
aux
s
|
f
::
s
->
f
::
(
aux
s
)
in
let
subs
=
aux
subs
in
let
rec
aux
=
function
|
((
x1
,
v1
)
as
z
)
::
((
x2
,
v2
)
::_
as
r
)
->
if
X
.
equal
x1
x2
then
if
v1
==
v2
then
aux
r
else
raise
One
else
z
::
(
aux
r
)
|
r
->
r
in
let
extra
=
aux
(
List
.
sort
(
fun
(
x1
,_
)
(
x2
,_
)
->
X
.
compare
x1
x2
)
!
extra
)
in
let
vars
=
cvars
vars
extra
and
subs
=
elim_subs_opt
(
List
.
map
(
fun
(
x
,
v
)
->
(
x
,
not
v
))
extra
)
subs
in
let
hoist
=
ref
[]
in
let
rec
aux
=
function
|
[]
->
[]
|
{
vars
=
[]
;
subs
=
[
f
]
}
::
s
->
hoist
:=
f
::
!
hoist
;
aux
s
|
f
::
s
->
f
::
(
aux
s
)
in
let
subs
=
aux
subs
in
let
f
=
mk_vs
vars
subs
in
List
.
fold_left
cup
f
!
hoist
and
elim_real
elv
f
=
let
vars
=
cap_vars
elv
f
.
allvars
in
if
vars
=
[]
then
f
else
(
let
el
=
ref
[]
in
let
rec
evars
vars1
vars2
=
match
(
vars1
,
vars2
)
with
|
((
x1
,
xv1
)
as
z1
)
::
vars1'
,
((
x2
,
xv2
)
as
z2
)
::
vars2'
->
let
c
=
X
.
compare
x1
x2
in
if
c
=
0
then
if
xv1
==
xv2
then
raise
One
else
evars
vars1'
vars2'
else
if
c
<
0
then
z1
::
(
evars
vars1'
vars2
)
else
(
el
:=
z2
::!
el
;
evars
vars1
vars2'
)
|
vars1
,
[]
->
el
:=
List
.
rev
!
el
;
vars1
|
[]
,
vars2
->
el
:=
List
.
rev_append
!
el
vars2
;
[]
in
try
let
vars
=
evars
f
.
vars
elv
in
let
subs
=
elim_subs_opt
!
el
f
.
subs
in
vars_subs
vars
subs
with
One
->
full
)
and
elim
elv
f
=
let
f'
=
elim_real
elv
f
in
(* print_string "elim vars="; print_vars elv;
Format.fprintf Format.std_formatter "<= %a@." dump f;
Format.fprintf Format.std_formatter "=> %a@." dump f'; *)
f'
and
elim_subs_opt
el
subs
=
if
el
=
[]
then
subs
else
order_subs
(
elim_subs
el
subs
)
and
elim_subs
vars
=
function
|
[]
->
[]
|
f
::
s
->
let
f
=
elim
vars
f
in
if
f
==
empty
then
raise
One
else
if
f
==
full
then
elim_subs
vars
s
else
f
::
(
elim_subs
vars
s
)
and
cup
f1
f2
=
if
(
f1
==
f2
)
then
f1
else
if
(
f1
==
empty
)
then
f2
else
if
(
f2
==
empty
)
then
f1
else
if
(
f1
==
full
)
||
(
f2
==
full
)
||
(
has_complement
f1
f2
)
||
(
has_complement
f2
f1
)
then
full
else
memo_bin
memo_cup
real_cup
f1
f2
and
real_cup
(
f1
,
f2
)
=
let
elim1
=
ref
[]
and
elim2
=
ref
[]
in
let
rec
cvars
vars1
vars2
=
match
(
vars1
,
vars2
)
with
|
((
x1
,
xv1
)
as
z1
)
::
vars1'
,
((
x2
,
xv2
)
as
z2
)
::
vars2'
->
let
c
=
X
.
compare
x1
x2
in
if
c
=
0
then
if
xv1
==
xv2
then
z1
::
(
cvars
vars1'
vars2'
)
else
raise
One
else
if
c
<
0
then
(
elim2
:=
(
x1
,
not
xv1
)
::!
elim2
;
z1
::
(
cvars
vars1'
vars2
))
else
(
elim1
:=
(
x2
,
not
xv2
)
::!
elim1
;
z2
::
(
cvars
vars1
vars2'
))
|
vars
,
[]
->
List
.
iter
(
fun
(
x
,
v
)
->
elim2
:=
(
x
,
not
v
)
::
!
elim2
)
vars
;
vars
|
[]
,
vars
->
List
.
iter
(
fun
(
x
,
v
)
->
elim1
:=
(
x
,
not
v
)
::
!
elim1
)
vars
;
vars
in
try
let
vars
=
cvars
f1
.
vars
f2
.
vars
in
let
elim1
=
cap_vars
(
List
.
rev
!
elim1
)
f1
.
allvars
in
let
subs1
=
elim_subs_opt
elim1
f1
.
subs
in
let
elim2
=
cap_vars
(
List
.
rev
!
elim2
)
f2
.
allvars
in
let
subs2
=
elim_subs_opt
elim2
f2
.
subs
in
let
subs
=
csubs
subs1
subs2
in
vars_subs
vars
subs
with
One
->
full
and
real_cap
(
f1
,
f2
)
=
let
(
vars1
,
vars
,
vars2
)
=
split_vars
f1
.
vars
f2
.
vars
in
let
(
subs1
,
subs
,
subs2
)
=
split_subs
f1
.
subs
f2
.
subs
in
if
vars
=
[]
&&
subs
=
[]
then
neg
(
cup
(
neg
f1
)
(
neg
f2
))
else
let
f1
=
mk_vs
vars1
subs1
in
let
f2
=
mk_vs
vars2
subs2
in
let
f
=
mk_vs
vars
subs
in
(* print_int (List.length vars); print_char ':';
print_int (List.length subs); print_char ' '; *)
cup
f
(
cap
f1
f2
)
and
cap
t1
t2
=
if
t1
==
t2
then
t1
else
if
t1
==
empty
||
t2
==
empty
then
empty
else
if
t1
==
full
then
t2
else
if
t2
==
full
then
t1
else
if
is_complement
t1
t2
then
empty
else
memo_bin
memo_cap
real_cap
t1
t2
let
rec
diff
t1
t2
=
if
t1
==
t2
then
empty
else
if
t2
==
empty
then
t1
else
if
t2
==
full
then
empty
else
if
is_complement
t1
t2
then
t1
else
real_diff
t1
t2
and
real_diff
f1
f2
=
(* Need only to compute vars1,subs1 *)
let
(
vars1
,
vars
,
vars2
)
=
split_vars
f1
.
vars
f2
.
vars
in
let
(
subs1
,
subs
,
subs2
)
=
split_subs
f1
.
subs
f2
.
subs
in
if
vars
=
[]
&&
subs
=
[]
then
neg
(
cup
(
neg
f1
)
f2
)
else
let
f1
=
mk_vs
vars1
subs1
in
(* print_int (List.length vars); print_char '!';
print_int (List.length subs); print_char ' '; *)
diff
f1
f2
let
find_max
f
l
=
let
aux
m
z
=
if
f
m
z
<
0
then
z
else
m
in
match
l
with
[]
->
raise
Not_found
|
m
::
z
->
List
.
fold_left
aux
m
z
let
simplify
f
=
try
let
(
x
,
p
,
n
)
=
find_max
(
fun
(
x1
,
p1
,
n1
)
(
x2
,
p2
,
n2
)
->
Pervasives
.
compare
(
p1
+
n1
)
(
p2
+
n2
))
f
.
allvars
in
(* Printf.printf "x=%i; p=%i,n=%i\n" (X.hash x) p n; *)
if
(
p
+
n
)
>
2
then
(
let
g
=
if
(
n
=
0
)
then
cup
(
elim
[
x
,
false
]
f
)
(
cap
(
posvar
x
)
(
elim
[
x
,
true
]
f
))
else
if
(
p
=
0
)
then
cup
(
elim
[
x
,
true
]
f
)
(
cap
(
negvar
x
)
(
elim
[
x
,
false
]
f
))
else
cup
(
cap
(
negvar
x
)
(
elim
[
x
,
false
]
f
))
(
cap
(
posvar
x
)
(
elim
[
x
,
true
]
f
))
in
Format
.
fprintf
Format
.
std_formatter
"Simplify %a ==> %a@."
dump
f
dump
g
;
g
)