No commit message

We can now prove insert in BinarySearchTree.scala, yeah !

The combination Unifier + OrderedBAPA
can now prove the postconditions of
createRoot / dumbInsert / dumbInsertWithOrder
in BinarySearchTree.scala :)

 1. Reduced irksome debug 'warnings' from the code.
 2. Changed (C != {}) to ( |C| > 0 )
 3. Removed duplicated cardinality constraints

Also added a small 'ordered' part to the post condition of dumbInsert. Makes the execution time jump from a few milliseconds to a whooping 12+ minutes.

Fixed a bug which created different Fresh Variables Collxx for the same \alpha(txx). Unification seems to be working.

Fixed the bug caught by Robin in his own code for searchAndReplace, which we were using. :-\

dumbInsert and createRoot in BinarySearchTree seem to be verified correctly.

Added handling of case expressions after substitution to Leaf() terms (which do not contain any variables).

1. Fixed a variable naming bug in orderedsets.Main, used id.uniqueName instead of id.name
2. Added a dumbInsert example in BinarySearchTree.scala (which bypasses the ifExpr problem, in function insert)
3. Added formula relaxation in ExprToASTConverter, in orderedsets

Added an example with min and max, inlined the partial evaluation of catamorphisms, and added parsing of ResultVariable() in orderedsets.Main

The unifier now translates terms (internal representation) back to expressions (pure Scala) and returns the substitution table.

It performs:
 - DNF transformation
 - Separating ADT formulas from non-ADT formulas (purifying terms as needed)
 - Unification on ADT part
 - returns either VALID or UNKNOWN (sound, but incomplete)

No commit message

No commit message