Fixing the bug when eating triggers the reduction of a match

Added problem failing because of order of step

Test --with-pac fails if unseparable+uncomplete

Allow comments (#) at the end of terms

Logging options to display measure of single terms in string_of_problem

Fixed bug in Scott.mk_match when no branches (Fixes problem 1 in solved)

Fixed bug in computing special k

Added exception Lambda, which may be caught when a conv becomes a lambda

Added very simple generator of tests with bombs/pacmans, run it with --with-pac

Fixed eta_compare in the case Lam vs. Bot

Removed special strategies in choose_step

Better error messages in parser

Check for absence of bombs and pacmans

Revert subst in branches of matches

Actually, it could be moved in susbt_in_problem,
hence doing it only once (on the deltas), instead
of replacing multiple times like now (useless).

Cleanup in w, added names, uncommented test for low special_k

Change to compute_special_k

Now the special_k taked into account the number or arguments (arity) of
terms. This solves problem "low special_k" in problems/w

Comments, fix indentation and

Renamed in critical_showstoppers: showstoppers -> inedible (I don't know why)

Simplified arity_of, precompute_edible_data, critical_showsteppers

Fixed computation of arity for top-level inerts

Simplified not-working example

Missing parenthesis fixed

Failing case found

Hack to reserve var 0 to purify it to BOM removed

String ==> Bytes to make recent ocaml compilers happy

Extracting solutions of 3-coloring problems

Added sample unsat problems found on the internet

subst does not replace anymore in branches of maches

It was unnecessary: a match cannot expand to a previous branch

Commented out problem, it is (still) failing because div occurs in conv

Printing now preserves the names of the original free variables

Fixed typo in problem

Improved parsing

- removed unused parse'
- fixed bug which was ignoring the first problems in some files

Improved pretty-printing

- Num does not use print_name anymore
- Original names of free variables are preserved
- bound variables' names start with x

Added problem wrongly backtracking

Forgot one "Z"

Code clean-up

Code clean-up

Important: added special variable "Z" for zero.

- Removed append_zero in Lambda4
- Now tests append "Z" at the end of ps'
- Manually appended "Z" at the end of all problems
- Removed tmp function in Lambda4, renamed to problem_of

Moved all problems in problems folder. Last ones in "w"

Encoding of SAT problems and 3-colorability of graphs

Fixes to parser

Added problems encoded from 3-colorability of graphs

Fixed "$" in parser

Command line arguments to ./a.out

For example:
 ./a.out problems/*
 ./a.out problems/p

Moved "o"-problems to problems/o

Fixed problems separator in parser: now it is $

A separable problem's label may start with '!', a not separable's with '?'

Added label to problem

Removed invalid problems

Failure in case of empty problem, to be fixed

Parser.from_file, and p* problems moved to problems/p

problems now contain a label and the names of the original free variables

First draft of Parser.problem_of_string

- problem_of_string should unify old Lambda4.problem_of and Parser.parse'
- Lambda4.problem_of was temporarily factored in problem_of_2
  and problem_of_String_tmp

Changed logic of entrypoint in Lambda4

- removed exception Fail
- added "check",which checks if we are in a subproblem
  of separation on which we know to be complete
- "solve" does not raise particular exceptions anymore,
  and the program raise failure only if there is some bug

Moved parse' from Num to Parser

Fixed: was using compare in place of eta_eq

in particular, eta_eq ignores arities of variables

there used to be cases of duplicate entries in PS (up to arities of variables)

Re-use Util.index_of

Code clean-up

Less casts and casts in the right place

Tidying up problems.ml

New failing problem, which shows that we need to change special_k

Added assert false

Fixed bug in eta_subterm

Remove FORCE option in Makefile

Fix: missing check to avoid stepping on vars of non positive arity

More problems

return type of simplify_match improved (no `Match in output)

Added safety check for step on n-th argument with n > 1

Avoid stepping on n if there is a div/number that would be turned into
a Lambda

Improved error messages

Failing problems commented out

New tests

Fix (??): some broken tests with Div = variable used to pass

Tentative commit: tactics dropped and clean-up

Fix: max_arity_tms was using wrong comparison

Fixed try in aux_conv + Added test in pure for divergence of conv

Fixes to printing

Added more problems with bombs, all working

Disabled some chars as variable names in the parser

Removed bomb variable

In Pure:
- Added constructor B to Pure.t
- Added rule corresponding to B (bottom) in Pure.mwhd
In Lambda4:
- Instantiating the bomb now actually uses subst_in_problem
- Two new exceptions: Bottom and Pacman
- Fixed subst_in_problem by making expand_match raise these two exceptions,
  which are caught when tolerated

Prettier-printing: string_of_problem outputs OCaml code

Added second problem with bombs and pacmans: it works!

Added new (passing) problem with a bomb (o1)

Towards `Bottom and `Pacman

1) Num updated to handle them
2) lambda4 compiles: safety conditions for projections hopefully
   implemented; strategy code not changed, therefore it will step over
   bombs and friends

New: simple backtracking with trail

auto_instantiate replaced by choose_step and first

Fixed if-then-else

Fix: nested `Lambda(false,_) were not handled correctly

-666 -> min_int

Fixed indentation and logging

instantiate takes an additional argument which is the number of the argument to the variable on which to step

clean removes *.o files

Removed old .ar files

Run tests with: make run

Fix: conv : x:min_int (.... y:1 ...)  y was not considered for stepping

When no other choice is available, step on any >0 variable that occurs in
a conv.

New problems n1, n2 used to debug the problem with dangerous variables fixed in the last commits

Bug fix: x (y z) where y was conv_dangerous did not make x so

Additional fix to last commit: args' where no longer checked for dangerous
variables. Fixed by passing three arguments to dangerous_invert_conv in
place of two.

Fix bug in dangerous_conv with arity of arguments of matches.
Next bug: variable replaced twice

The measure finally works on all problems in problems.ml!
Added in logs/fail.txt a fragment of a failing problem

Experimenting with a combined measure

Instantiate now uses a global initialSpecialK (ignoring the local one)
This fixes the bug in the previous commit, and makes the problem pass

Arity inherited only in the case (true, min_int)
Problem 25 fails because a fake variable becomes
critical step.

new_arity = old_arity + 1

Fixes to how arities are assigned and propagated
- added truelam to subst (useless, can be removed)
- TODO: to measure the problem, count the `fake` variables
        which are the ones with arity = min_int

Minor fixes

still stepping on negative variables