
19 jun 2021
   - h1 is now compiled using GimML instead of HimML.
     'regexp' no longer exists in GimML, and is replaced
     by a new regexp library ('re_make_nfa', 're_parse', and so on).
     Now made all changes necessary to use the new regexp library.
   - some regexps (coq_fun.ml, coq_auto.ml) were meant to match
     "^##false\\(([a-zA-Z0-9'_]*)\\)"; I assume the double hash sign
     was a mistake: replaced by  "^#false\\(([a-zA-Z0-9'_]*)\\)".
08 dec 2009
	- corrected a bug in clause.ml.
This manifested itself in the
Doc/butler-puzzle.p example (see Doc/h1.tex),
and was concerned with the handling
of fully defined predicate symbols.
	Bug corrected, but no example
known that runs through the new piece
of code (if this is executed, the log
file should print the sentence:
"Remove parent clause, which was resolved
 on predicates just realized to be fully defined.")
	The idea is as follows.  When
the last automaton clause in the queue
is dealt with that has head P(...), P
is marked fully defined, and all clauses
with some P(...) in the al part (in selfq;
not those in selxq, see bug of 23 nov 2009),
are resolved with it.
	I initially thought incorrectly that
this would be an invariant: no P would occur
in bodies of clauses (correction: in selfq)
when P is fully defined.  However, it may
happen that P becomes fully defined because
the last clause with head P(...) was erased,
typically because it was subsumed.  In this
case, one needs to resolve, using resolve_auto_def,
with all automaton and (unit clauses) with head
P(...).  This was added to the end of resolve(),
testing the new variable new_fully_defined_ok,
which keeps those predicates that became fully
defined because of the first case (i.e., the
last automaton clause with head P(...) was just
seen).

23 nov 2009
	- corrected a bug in clause.ml,
found by Sylvain Schmitz on 20 nov 2009.
In test1.p, we have the clause
	(1) p(f(X)) :- p(X)
and after a few steps the clause
	-p(X).
Moreover, p is fully defined.  So h1
computed all the resolvents with -p(X),
in particular the one with clause (1),
and generated -p(X) again, forever.
	This should have been detected
by ct_subsumed or ct_subsumed_try, but
the resolve_selxq_def function that deals
with fully defined predicate symbols takes
short-circuits.  (Instead of putting
-p(X) into the selxq table, then removing
it because it is subsumed, it never puts
it into the table, making the subsumption
test fail.)
	Anyway, resolution on fully defined
predicate symbols is only guaranteed to
terminate when the premise is replaced by
a smaller conclusion---what resolve_auto_def
does.  So resolve_selx_def was commented out,
and all its uses removed.

02 dec 2008
	- corrected a bug in check_disjoint_very_simple,
in model.ml.  The indices i and j were not guaranteed
to be from the set Ps of predicates actually occurring
in the clause.  Added '& Ps' twice to correct the problem.
	- corrected a misconception (not a bug) in
scc.ml.  I though the 'low' num of a node ended up being the
least dfsnum of its strongly connected component, but
this is wrong.  See counterexample in a comment at the
end of function scc, in scc.ml.
	As a consequence, I am now only returning
the dfsnum map (dfs), not the 'low' map.

13 nov 2008
	- corrected a bug in clause.ml.  Manifested
itself in very rare cases, namely by running
./h1 -all eke.p.  Corrected by adding the following
lines to ct_subsumed_simple:
	  | ct_subsumed_simple (CL (HVAR _, _, nil, ...)) =
	    false (* case of clauses P(X1) <= B2 (X2), B3(X3), ...
Problem was that a clause such as
	testable_current(X1) :- testable_current(crypt(X1,X2)), knows_current(X2)
	was sometimes subsumed [forward] before being
ever considered, since ct_subsumed_simple thought
it could be subsumed by the previous clause
	testable_current(X1) :- knows_current(X1)
This was not matched by the previous case on ct_subsumed_simple,
hence it fell through to the last case, which was only
meant for clauses with heads of the form q, or false.
	- corrected a bug in coq_auto.ml, which printed
both the clauses P(cons(X1,X2)) :- Q(X1) and
P(cons(X1,X2)) :- Q(X2) as though it were the first one
(on empty blocks, the counter i used to print X<i>
failed to get incremented).

11 feb 2008
	- corrected a bug in clause.ml.  Manifested
itself by raising SortSimplifyBBug in very rare cases.
Occurred any time I used a variable called 'doner'
to detected cycles in reachability-like algorithms.
The point is that we should fail, not when P is
already in !doner (this might be a loop, but also
a memoized result from some other path computation),
but when P is mapped to false by !doner; and then
we should add the result of the reachability test
after the computation is complete.

06 feb 2008
	- Corrected plenty of bugs in h1mc
(model.ml, coq_model.ml, pfcprintcoq.ml).
Mostly due to the fact that h1mc was largely
rewritten, and several bugs were introduced.

01 feb 2008
	- Corrected a bug in h1mc (coq_model.ml)
where we wanted to output a proof of C in history H,
and we had already proved C in some other history H',
a subset of H.  We need a helper lemma [comment is:
(* Already proved, with different history. *)].
	- Made epsdone and done_clauses mechanism
in model.ml more efficient.  Before, find_simple_inclusions
(testing simulations) used its own looping and memory
mechanism.  Then, work was redone to output new translations
to the MC_ format of already done SIJ_ proofs.
These are now memoized in j_of_ij_memo_r.

31 jan 2008
	- Now h1mc (both model.ml and coq_model.ml)
recognize that, when proving C from history H,
we may have proved C in some subset H' of H already.
Previously, h1mc required H'=H, for simplicity.
	Accordingly, semantics of MC_DONE changed
from "marks clauses that have already been proved, in the
same history" to "[...] or some smaller history already".

24 jan 2008
	- All coq tools can now output both Coq v7 and
v8 syntax.
	- In the MC_DEDUCE_POS case of pjustif_1,
a final dot was not added if !firstr was true, and
empty h andalso empty vars also.

22 jan 2008
	- TPTP format changed from 1.0 to 3.3.0
since last time.  Changed tptp.l and tptp.y so
that can parse both formats.  Changed other tools,
in particular tptpmorph, to output both formats.
Added -tptp option for this.  Conversion can be
done by 'tptpmorph -tptp 3.3.0 <file.p>' to 3.3.0 format,
by 'tptpmorph -tptp 1.0 <file.p>' in the reverse
direction.
	- 'conjecture' in input_clause (resp. cnf)
did not mean what I thought.  Should use 'axiom'
on every clause.

06 jan 2006
	- again corrected bug in reference counting
on pdef's: bad interaction with sort simplification,
where parent clause is not inserted (since it is
subsumed by conclusion), but rem_def was not called.

16 dec 2005
	- corrected bug in reference counting
on pdef's (in clause.ml; using check_pdef).

06 dec 2005
	- changed determinize.ml so that blocks
{P1, ...,Pn} are printed as __exactly_P1_and_..._and_Pn
instead of __inter_P1_and_..._and_Pn.  The former
means that we satisfy P1, ..., Pn but no other
predicate from the signature.  The latter means
that we satisfy P1, ..., Pn, and possibly others.
	This involved adding block_of_exact and
mk_detval in intersym.ml, and adding file exactsym.l.
	Modified pl2gastex so that it prints
__exactly_P1_and_..._and_Pn as {P1, ...,Pn}
(and __inter_P1_and_..._and_Pn as P1 \cap ... \cap Pn
as before)... recursively.

04 dec 2005
	- bumped version to 1.5.

03 dec 2005
	- changed slightly the way resolve_auto
and resolve_selx report whether the generated conclusion
subsumes its parent.  If the two clauses are renamings
one of the other, then this would generate c,
erase the previous c, re-generate c, erase the
previous one, etc., and loop.  (Forward subsumption
is OK, backward no.)

02 dec 2005
	- added -no-deep-abbrv option (not yet
documented).
	- replaced autoinfoq as map to sets of
lists of blocks by a map to 'blocks', which is
a tree-like (rather ZBDD-like) structure of atoms.
	Eases subsumption a lot.  Should do
the same for other shapes of clauses.

28 nov 2005
	- ct_subsumed_by_auto chooses between
two methods to detect whether a clause is subsumed
by some automaton clause.  One is to enumerate
all automata clauses with the same head (say
there are m of them), another is to enumerate
all subsets of the body of the argument clause
(if there are nBs atoms in this, there are 2^nBs
subsets to test).  Before, the second method
was chosen as soon as m>=5.  We now decide
to choose the second method whenever 2^nBs < m,
which is more natural.

27 nov 2005
	- added #false token to pl.l; we now
recognize heads of clauses of the form #false
and #false(<identifier>) in pl.y.  This affects
pl2tptp and plpurge.
	Problem is that the name of the clause
(<identifier>) is lost.  But at least this does
not produce satisfiable clause sets from unsatisfiable
ones.  (Or we should decide that #false(...) must
always be false in all models.)

22 nov 2005
	- added all_states to xmlauto.ml; only
definitions of predicates from all_preds \ all_states
are printed, not all from all_preds, otherwise
symbols in all_preds & all_states are defined twice
in the output set of clauses by auto2pl.
	- changed intersym.ml/mk_inter so that
intersections of just one state q really gets a fresh
name __inter_q, instead of inheriting the same name q.
(This makes the previous change [see above] moot,
since by definition all_preds & all_states will be
empty.)  The point is as follows.  
	Consider the file
__def_1(f(X1)) :- __def_3(X1).
__def_2(b).
__def_3(a).
eq(pair(X1,X2)) :- __def_2(X2), __def_1(X1).
sig(a).
sig(b).
sig(f(X)) :- sig(X).
	If we run this through pldet (new version),
we get the admittedly ugly, but correct:
__inter_____def__3(a).
__inter_eq(pair(X1,X2)) :- __inter_____def__1(X1), __inter_____def__2(X2).
__inter_____def__2(b).
__inter_sig(f(X1)) :- __inter_____def__2(X1).
__inter_sig(f(X1)) :- __inter_sig(X1).
__inter_sig(f(X1)) :- __inter_____def__1(X1).
__inter_____def__1(f(X1)) :- __inter_____def__3(X1).
% Definitions.
__def_2(X) :- __inter_____def__2(X).
__def_1(X) :- __inter_____def__1(X).
sig(X) :- __inter_____def__3(X).
sig(X) :- __inter_sig(X).
sig(X) :- __inter_____def__2(X).
sig(X) :- __inter_____def__1(X).
eq(X) :- __inter_eq(X).
__def_3(X) :- __inter_____def__3(X).
	Before, __inter_sig and sig were confused.
However, note that __inter_sig only recognizes
terms of the form f(...).  This is because __inter_sig
is meant to be the set of terms that satisfy
sig *and no other predicate*.  So this is not the
same as sig.
	- changed a #put stdout "P" into #put stdout P
in xmlauto.ml: before every %[def] output by auto2pl
was of the form "%[def] P(...)".

05 jun 2005
	- changed code in Makefile.in that used 'install -C';
now uses 'install'.  The -C option is obsolete, ignored on
some machines, and causes failure on Sun machines (mentioned
by Thomas Gawlitza).
09 jan 2005
	- corrected bug in pldet (determinize.ml, do_iter
inside determinize), where vl was used as tuple of values
instead of rev vl.  This made the arguments the other way
around in the generated deterministic automata.
	- changed the code of resolve_auto in clause.ml,
so as to try to resolve on literals with the fewest
matching automata clauses firsts (counting card !blkls).
This definitely does not work.  Times for Fabrice/alice_full1.p
went up from 22 min to 80 min, then back to about 40 min
after optimization.
	Also, auto_back_subsume seems to take a lot of
time, although almost no automaton clause is ever
back-subsumed.  (But beware: this back subsumption
is absolutely crucial.)
	- in resolve_auto now, when some of the generated
resolvents subsumes one of the non-automaton premises,
only this resolvent is wait_insert'ed, and none of
the other generated resolvents.  In other words,
resolve_auto implements resolution simplification,
not just resolution here.

06 jan 2005
	- changed all option names.
In h1 mainly:
	-p	-> -no-log
	+p	-> -log
	+p-out	-> -log-out
	-nondet	-> -alternation
	+nondet	-> -no-alternation
	-m	-> -no-model
	+m	-> -model
	-trace	-> -no-progress
	+trace	-> -progress
	-monadic-proxy	-> -standard-approx
	+monadic-proxy	-> -monadic-proxy
	-all	-> -first
	+all	-> -all
	-resolve	-> -no-resolve
	+resolve	-> -resolve
In h1, h1mc, pldet, h1logstrip:
	-v <n>	-> -v<n>
    Added -v, synonym of -v1
In h1, xmlauto (auto2pl):
	-trim	-> -no-trim
	+trim	-> -trim
In xmlauto (auto2pl):
	+defs	-> -defs
	-defs	-> -no-defs
	+trim	-> -purge
	-trim	-> -no-purge
In h1logstrip:
	-f	-> -no-false
	+f	-> -false
	-a	-> -no-auto
	+a	-> -auto
	-q	-> -no-ne
	+q	-> -ne
In h1mc:
	-axioms	-> -no-axioms
	+axioms	-> -axioms

02 jan 2005
	- changed prefix not_ in xmlauto to __not_;
	- changed seidl_from_gclause so that it creates
fresh predicates as __aux_<n>, as before, except it
is now guaranteed that these predicates are indeed new.
I.e., if the original clause set already contains
predicates of this form, none of the fresh predicates
will be equal to the original ones.  On the other hand,
seidl_from_gclause also memoizes names of fresh
predicates across clauses, which it did not do before.
01 jan 2005
	- added +nondet flag to h1, allowing one to
compute non-deterministic tree automata instead of
general alternating tree automata in model files.
31 dec 2004
	- corrected bug in pldet; determinize.ml/inter_auto
did not compute an intersection of sets of transitions,
but something larger.
24 dec 2004
	- Created pl2gastex utility.  Works better
than autodot, should replace it.
12 dec 2004
	- changed the name of 'monitor' to 'h1mon'.
	- added h1getlog to the list of programs
installed by make install.
06 apr 2004
	- had to revert partially from optimizations
on pldet, done on 01 apr 2004.  Transitions corresponding
to invisible function symbols were ignored; this seemed
to be in the spirit of ignoring %q<n> symbols, but
in fact removed the possibility of considering
auxiliary predicates __aux_45(X,Y,Z,T,U) for example
(as introduced by seidl_from_gclause); this is not
a problem, but this also removed important clauses
from problems using non-monadic predicates.

04 apr 2004
	- h1 and tptpmorph could not read clauses
output by pl2tptp.  The latter printed atoms of
the form p X instead of p(X), which h1 and tptpmorph
could not parse.  Now h1 and tptpmorph also parse
the forms p X and p f(t1,...,tn).
	- In h1, sometimes the same predicate symbol
(generated by seidl_from_clause using newP_aux)
was generated with different arities.  This was
because newP_aux was used inconsistently,
sometimes with a body as argument, sometimes
with a pair (body, head).  Now strict typing
is enforced.
	- the -trim option of h1 was simply ignored.
Repaired.

01 apr 2004
	- improved pldet massively.  Now clauses of
the form %q<n> (...) :- ... are simply ignored.  They
do not contribute anything useful, as they only describe
auxiliary states %q<n>, which are only used internally
by h1.  Also, transitions abutting on the sink state {}
are not produced at all.  So pldet now produces a possibly
incomplete deterministic automaton.

03 jan 2004
	- removed bug in resolve: we should never call
b_set (or any other function that does side-effects on
tables like selfq, selxq, autoinfoq, etc.) while iterating
on the tables.  This was innocuous when tables were just
references to (applicative) maps, because the iteration
just proceeded on the previous version of the table.  With
tables (using the (''a, 'b) table type), not so.  So
functions which want to backward subsume some clauses
should collect the clauses to backward subsume in some
set, then terminate the iteration, then backward subsume
all clauses in the set.  I knew this all along, but
must have forgotten that in some cases.
	- pathset environments used to be stored along
with clauses; they are now recomputed each time; this takes
a bit more time, but uses less space.  Moreover, the
handling of pathset environments (without recomputing them)
may have been less reliable, although I have never experienced
any bug related to this.

02 jan 2004
	- removed bug in resolve: when an automaton clause
was popped from waitq, and it was the last one with head P
(so that P would be declared fully defined), dec_pdef was
called on P only after all resolvents were generated.
	Now dec_pdef is called before all resolvents were
generated (as it should have been), so that resolution
is done to expand all definitions by their bodies.
(The selection function selects all negative atoms with
a fully defined predicate, if any; otherwise, all negative
atoms.  This is meant to replace all defined symbols
by their definitions eagerly.)
	- When running h1 on <whatever>.p, generates
<whatever>.model.pl, <whatever>.model.xml, <whatever>.log instead
of h1model.pl, h1model.xml, h1proof.log.

27 dec 2003
	- changed the architecture of h1 completely.
Now h1 itself only does resolution proof, and outputs
files h1model.pl (model in Prolog format), h1model.xml
(finite model in XML format), h1proof.log (symbolic
execution trace).
	h1trace can print proofs from file h1proof.log,
in unit resolution (aka, natural deduction) format;
recognized options are 'log' (can be input to h1trace
again), 'tree' (ASCII, meant to be readable in outline
mode under emacs), 'coq' (checkable by Coq).
	h1mc is the model-checking part, and takes
both h1model.pl and h1proof.log in argument.
	- bumped version to 1.4.

20 jul 2003
	- removed bug in ctnoq_run_subsumes, which tried
to iterate over some purported list of CT_NEXT nodes coming
after the current CT_ATOM.  This list was stored in the "next"
field of the CT_ATOM, and was maintained by ctt_merge.
Unfortunately, merging just concatenated this lists, even
when merging two CT_NEXT nodes (in which case there should
only be one element in the list, not the concatenation of
two one-element lists).  This causes exponential blowup in
the size of subsumption structures, and quite some complexity
explosion as soon as the set of clauses to resolve was a
bit too complicated.
	- changed seidl_from_clause a bit, so that not
only clauses of the form h <= body with a complex head
and a body of at least two literals gets abbreviated as
h <= A and A <= body, where A is some P(f(x1,...,xk)),
x1, ..., xk being the free variables common to h and body;
but also each literal A of the body that is of depth at least
1 is replaced by some literal P(f(x1,...,xk)), with
x1, ..., xk the free variables of A, plus a clause
P(f(x1,...,xk)) <= A.  Since we share this with respect
to A (modulo renaming in the last case), this allows the
resolver to share some computations.

19 jul 2003
	- added minlen, maxlen, minmaxd, maxmaxd to CT_ATOM
constructor in subsumption structures.  This gets me roughly
a factor of 3 in speed on time ./h1 Fabrice/essai7.p.

17 jul 2003
	- added -auto <.pl filename> option to h1;

14 jul 2003
	- changed name of xmlauto to auto2pl, which is closer
to what it does.
	- changed linauto so that transitions are names d<m>_<n>,
where m is the number of the current cycle and n is between 0 and base-1.

13 jul 2003
	- Added -complete option to xmlauto; now also checks whether
input automaton is deterministic, and fails otherwise.
	- Added +defs and -defs options to xmlauto.
	- Created linauto, a solver of unquantified Presburger formulas,
version 1.0:
"
Usage: linauto <flags>* filename.
  Version 1.0 - Jul 13, 2003, Copyright (C) Jean Goubault-Larrecq;
     see file COPYRIGHT.
  linauto comes with ABSOLUTELY NO WARRANTY; see file COPYING, sections 11, 12.
  This is free software, and you are welcome to redistribute it
  under certain conditions; see TERMS AND CONDITIONS in file COPYING.
    Use '-' instead of filename to read from stdin.
  Flags are:
    -h prints this help.
    -base <n> produces an automaton in base <n> (n>=2); default: 2.
    -var <name> declares variable <name> (only needed if <name> is not
           free in system of equations given in <filename>);
    -prefix <name> builds state names as <name>1, <name>2, ... default: q.
    -epsilon <name> uses <name> for the empty word; default: epsilon.
    -final <name> uses <name> as final predicate name; default: final.
    -cycle <name> builds intermediate predicates <name>0, ..., <name>k-1,
           where k is number of variables; each state satisfies
           exactly one of these, and transitions go from a state satisfying
           <name>i to <name>i-1 (mod k);   default: __cycle_.
"

	- Bumped h1 version to 1.2.

11 jul 2003
	- Corrected bug in auto.ml/auto_simple_inclusions/detect,
which iterated over all P => Pfmap instead of computing Pfmap as
?auto P.  This only made the block inclusion test less precise
than it could be.
	- Created xmlauto, version 1.0;
"
Usage: xmlauto <flags>* filename.
  Version 1.0 - Jul 11, 2003, Copyright (C) Jean Goubault-Larrecq;
     see file COPYRIGHT.
  xmlauto comes with ABSOLUTELY NO WARRANTY; see file COPYING, sections 11, 12.
  This is free software, and you are welcome to redistribute it
  under certain conditions; see TERMS AND CONDITIONS in file COPYING.
    Use '-' instead of filename to read from stdin.
  Flags are:
    -h prints this help.
    -prefix <name> prepends <name> to state names.
    -negate <name> adds clauses to define a predicate not_<name>
            recognizing the complement of <name>;
            <name> should be the name of a predicate, as found
            in the <definitions> section of the input file.
       Several -negate <name> flags may be given, to define several
       negated predicates at once
    +trim (only useful in conjunction with -negate) outputs only
          the part of the input automaton that is useful to build
          the negations of predicates given in -negate flags.
        Default: -trim.
"
	- Created tptpmorph, version 1.0;
"
Usage: tptpmorph <flags>* filename.
  Version 1.0 - Jul 11, 2003, Copyright (C) Jean Goubault-Larrecq;
     see file COPYRIGHT.
  tptpmorph comes with ABSOLUTELY NO WARRANTY; see file COPYING, sections 11, 12.
  This is free software, and you are welcome to redistribute it
  under certain conditions; see TERMS AND CONDITIONS in file COPYING.
    Use '-' instead of filename to read from stdin.
  Flags are:
    -h prints this help.
    -rewrite "f(X1,...,Xn)=t" where t is a term.
       Several -rewrite flags may be given, with distinct f's.
    -status <name>: uses <name> as second argument of 'input_clause'
                    (default: 'conjecture').
"
	- Bumped h1 version to 1.1.

10 jul 2003
	- Created this file.
	- Created h1 version 1.0:
"
Usage: h1 <flags>* filename.
  Version 1.0 - Jul 10, 2003, Copyright (C) Jean Goubault-Larrecq;
     see file COPYRIGHT.
  h1 comes with ABSOLUTELY NO WARRANTY; see file COPYING, sections 11, 12.
  This is free software, and you are welcome to redistribute it
  under certain conditions; see TERMS AND CONDITIONS in file COPYING.
    Use '-' instead of filename to read from stdin.
  Flags are:
    -h prints this help.
    -v 0 runs silently, -v 1 prints clauses as they are derived or checked,
       -v 2 prints detailed information about current computation.
    -check-h1 <n>: if n=0, do not check whether input clauses are in class H1;
                   if n=1, emits warnings for non-H1 clauses (default);
                   if n>=2, checks and fails on non-H1 clauses.
    +all finds all contradictions,
        -all stops on first contradiction (default).
    +cp outputs Coq proofs of all found contradictions in 'h1cp.v'.
        Default: -cp.
    +cm outputs model as an automaton in Coq format, and proofs that this model
        satisfies the initial clause set, in 'h1cm.v'.
        Default: -cm.
    +m outputs model as sets of Horn clauses, in file 'h1model.pl'.
        Default: -m.
    +xm outputs model as complete deterministic automaton (a.k.a., finite
        first-order structure), in XML format, in file 'h1model.xml'.
        Default -xm.
    +dm outputs model as complete deterministic automaton, in dot format,
        in file 'h1dm.dot'.  This is unusable except for very small automata,
        and is provided for pedagogical reasons.
        Default: -dm.
"
	- Created pl2tptp version 1.0:
"
  Version 1.0 - Jul 10, 2003, Copyright (C) Jean Goubault-Larrecq;
     see file COPYRIGHT.
  pl2tptp comes with ABSOLUTELY NO WARRANTY; see file COPYING, sections 11, 12.
  This is free software, and you are welcome to redistribute it
  under certain conditions; see TERMS AND CONDITIONS in file COPYING.
    Use '-' instead of filename to read from stdin.
  Flags are:
    -h prints this help.
    -prefix <name>: uses <name> as prefix to generate names of clauses
                    (default: 'clause').
    -status <name>: uses <name> as second argument of 'input_clause'
                    (default: 'conjecture').
"
