more cleaning up

README

-Trying to clean the slate.

WISHLIST

-Do Add here what you would love FunCheck to be able to do
-------------------------------------------------------
-VK: support maps Map[A,B] for ground types A,B (no polymorphism)
-VK: add bitvectors, including multiplication of int32 variables
-
-PS: support multiple top-level objects
-PS: support tuples (including natively in Z3)
-PS: implement @induct tactic, completely, not just for one arg
-PS: construct models for sets properly (also in interpreter)
-PS: support maps natively
-
-PS: use different levels of summaries (eg. just contract, part of contract
-that's public, then finally body) in unrollings, trying to minimize the
-branching at first
-
-Wishes granted so far
----------------------
-
-PS: create a wishlist
-PS: rewrite pattern-matching translator to use if-then-else
-VK: add IsValid class to allow for writing just "holds" in place of ensuring(_ == true)
-PS: generate VCs for preconditions
-PS: generate VCs for pattern-matching
-PS: use 'private' accessor to indicate what's part of the interface
-PS: use a theory plugin to instantiate/unroll function bodies
-PS: instantiate/unroll function bodies in a fair way, to guarantee termination

funcheck-laraserver

-#!/bin/bash
-FUNCHECKCLASSPATH="/localhome/liftweb/funcheck/project/boot/scala-2.8.1/lib/scala-library.jar:/localhome/liftweb/funcheck/project/boot/scala-2.8.1/lib/scala-compiler.jar:/localhome/liftweb/funcheck/bin/purescala/purescala-definitions_2.8.1-1.0.jar:/localhome/liftweb/funcheck/bin/funcheck/funcheck-plugin_2.8.1-1.0.jar:/localhome/liftweb/funcheck/lib/z3.jar"
-
-for f in "/localhome/liftweb/funcheck/bin/multisets-lib/multiset-placeholder-library_2.8.1-1.0.jar" "/localhome/liftweb/funcheck/bin/multisets/multiset-solver_2.8.1-1.0.jar" "/localhome/liftweb/funcheck/bin/orderedsets/ordered-sets-solver_2.8.1-1.0.jar" "/localhome/liftweb/funcheck/bin/setconstraints/type-inference-with-set-constraints_2.8.1-1.0.jar"; do
-  if [ -e ${f} ]
-  then
-    FUNCHECKCLASSPATH=${FUNCHECKCLASSPATH}:${f}
-  fi
-done
-
-SCALACCLASSPATH="/localhome/liftweb/funcheck/bin/multisets-lib/multiset-placeholder-library_2.8.1-1.0.jar:/localhome/liftweb/funcheck/bin/funcheck/funcheck-plugin_2.8.1-1.0.jar:/localhome/liftweb/funcheck/bin/purescala/purescala-definitions_2.8.1-1.0.jar"
-
-LD_LIBRARY_PATH=/localhome/liftweb/libstdc++:/localhome/liftweb/z3/z3-2.19/lib \
-scala -classpath ${FUNCHECKCLASSPATH}:${SCALACCLASSPATH} \
-funcheck.Main -cp /localhome/liftweb/funcheck/bin/funcheck/funcheck-plugin_2.8.1-1.0.jar $@