fix for most cases

CMakeLists.txt

@@ -1,5 +1,5 @@
 cmake_minimum_required (VERSION 2.8)
-set(Nv 2)
+set(Nv 3)
 add_definitions(-D__SELECTIVE_SAMPLING_ENABLED)
 project(zilu CXX)
 set(PRECISION 3)
@@ -74,7 +74,7 @@ configure_file(config.h.in ../include/config.h)
 # add include dir and source dir into project
 include_directories (include)
 aux_source_directory(src DIR_SRCS)
-add_executable(09 /home/lijiaying/Research/zilu/test/09.cpp ${DIR_SRCS})
-target_link_libraries(09 ${Z3_LIBRARY})
-target_link_libraries(09 ${GSL_LIBRARIES})
-target_link_libraries(09 gsl gslcblas m)
+add_executable(24 /home/lijiaying/Research/zilu/test/24.cpp ${DIR_SRCS})
+target_link_libraries(24 ${Z3_LIBRARY})
+target_link_libraries(24 ${GSL_LIBRARIES})
+target_link_libraries(24 gsl gslcblas m)

benchmark/47.cfg

@@ -1,7 +1,6 @@
 names= x y
 precondition= x<y
 loopcondition= x<y
-loop= if (x < 0) x = x + 7; else x = x + 10;
-if (y < 0) y = y - 10; else y = y + 3;
+loop= if (x < 0) x = x + 7; else x = x + 10; if (y < 0) y = y - 10; else y = y + 3;
 postcondition= x >= y && x <= y + 16
 learners=linear

benchmark/50.cfg

@@ -1,7 +1,6 @@
 names= xa ya
 precondition=xa + ya > 0
 loopcondition=xa > 0
-loop=xa--; 
-ya++;
+loop=xa--; ya++;
 postcondition=ya >= 0
 learners=linear

benchmark/51.cfg

@@ -3,9 +3,6 @@ precondition=(x>=0) && (x<=50)
 beforeloop=
 beforeloopinit=
 loopcondition=
-loop= if (x>50) x++;
-		if (x == 0) {
-			x ++;
-		} else x--;
+loop= if (x>50) x++; if (x == 0) { x ++; } else x--;
 postcondition=(x>=0) && (x<=50)
 learners=poly

benchmark/README.md

@@ -0,0 +1,27 @@
+# precision problem
+In our invariant generation approach, we apply learning algorithm to produce a classifier which will be round off into integer coefficients.
+This round off operation depends much on the precision we could bear.
+By default, the precidion is set to 2, which means if there are two coefficents a, and b, and a > 100*b, b will be rounded off to 0.
+This default setting works for most cases. But for the following cases, you need to specify a new precision value in order to learn an invariant. Otherwise, the learning iteration will continue until reaching the upbound or running overtime.
+
+| benchmark | precision |
+| --------- |:---------:|
+| 08.cfg    |  1        |
+| 15.cfg    |  1        |
+| 16.cfg    |  2        |may take many times
+| 20.cfg    |  1        |
+| 21.cfg    |  ?        |-
+| 22.cfg    |  1        |may take many times
+| 23.cfg    |  3        |
+| 24.cfg    |  1        |failed to reproduce the result for now
+| 29.cfg    |  3        |
+| 34.cfg    |  1        |
+| 40.cfg    |  1        |
+| 41.cfg    |  1        |question_mark as positive
+| 42.cfg    |  1        |take many times
+| 43.cfg    |  3        |
+| 44.cfg    |  ?        |-
+| 45.cfg    |  ?        |-
+| 46.cfg    |  ?        |-
+| 52.cfg    |  3        |
+| 53.cfg    |  1        |

config.h.in

@@ -62,8 +62,8 @@
  *		   This should be set in /CMakeLists.txt file
  *		   You'd better set this value in a scope [1, 12] 
  */
-//#define PRECISION 1
-#define PRECISION 2
+#define PRECISION 1
+//#define PRECISION 2
 //#define PRECISION 3
 
 /** @brief The pointer to test program, DO NOT assign directly

disj/benchmark/44.cfg

@@ -0,0 +1,12 @@
+names= x y
+precondition= x<y
+loopcondition= x<y
+loop=
+branchcondition=(x<0 && y<0)
+branch=x=x+7; y=y-10;
+branchcondition=(x<0 && y>=0)
+branch=x=x+7; y=y+3;
+branchcondition=
+branch=x=x+10; y=y+3;
+postcondition= x >= y && x <= y + 16
+learners=linear disjunctive

disj/benchmark/45.cfg

@@ -0,0 +1,9 @@
+names= x y
+precondition= y>0 || x>0
+loopcondition=
+branchcondition=x>0
+branch=x++;
+branchcondition=
+branch=y++;
+postcondition=x>0 || y>0
+learners=linear disjunctive

disj/benchmark/46.cfg

@@ -0,0 +1,12 @@
+names= x y z
+precondition= y>0 || x>0 || z>0
+loopcondition=
+#loop=if (x>0) x++; else x--; x=-1 * x;
+branchcondition=x>0
+branch=x++;
+branchcondition=y>0
+branch=y++;
+branchcondition=
+branch=z++;
+postcondition=x>0 || y>0 || z>0
+learners=linear disjunctive

disj/cfg/21.cfg

@@ -0,0 +1,12 @@
+names= x y
+precondition= y>0 || x>0
+loopcondition=1
+realloopcondition=x+y<=2
+branchcondition=x+y>-2
+branch=break;
+branchcondition=x>0
+branch=x++;
+branchcondition=
+branch=y++;
+postcondition=x>0 || y>0
+learners=conj disjunctive

disj/cfg/44.cfg

@@ -0,0 +1,12 @@
+names= x y
+precondition= x<y
+loopcondition= x<y
+loop=
+branchcondition=(x<0 && y<0)
+branch=x=x+7; y=y-10;
+branchcondition=(x<0 && y>=0)
+branch=x=x+7; y=y+3;
+branchcondition=
+branch=x=x+10; y=y+3;
+postcondition= x >= y && x <= y + 16
+learners=linear disjunctive

disj/cfg/45.cfg

@@ -0,0 +1,9 @@
+names= x y
+precondition= y>0 || x>0
+loopcondition=
+branchcondition=x>0
+branch=x++;
+branchcondition=
+branch=y++;
+postcondition=x>0 || y>0
+learners=linear disjunctive

disj/cfg/46.cfg

@@ -0,0 +1,12 @@
+names= x y z
+precondition= y>0 || x>0 || z>0
+loopcondition=
+#loop=if (x>0) x++; else x--; x=-1 * x;
+branchcondition=x>0
+branch=x++;
+branchcondition=y>0
+branch=y++;
+branchcondition=
+branch=z++;
+postcondition=x>0 || y>0 || z>0
+learners=linear disjunctive

disj/cfg/f2.cfg

@@ -0,0 +1,6 @@
+names= x y
+precondition=x + y >= 0
+loopcondition=y > 0
+loop=x++; y--;
+postcondition=x >= 0
+learners=linear

disj/cfg/fig1b.cfg

@@ -0,0 +1,12 @@
+names= x y
+precondition= y>0 || x>0
+loopcondition=1
+realloopcondition=x+y<=2
+branchcondition=x+y>-2
+branch=break;
+branchcondition=x>0
+branch=x++;
+branchcondition=
+branch=y++;
+postcondition=x>0 || y>0
+learners=conj disjunctive

disj/cfg/pldi08_fig1.cfg

@@ -0,0 +1,11 @@
+names=x y
+precondition=x < 0
+loopcondition=1
+realloopcondition=x<0
+loop=
+branchcondition=x>=0
+branch=break;
+branchcondition=
+branch=x=x+y; y++;
+postcondition=y>=0
+learners=linear disjunctive

disj/cfg/zilu_disj1.cfg

@@ -0,0 +1,12 @@
+names= x y
+precondition= x<y
+loopcondition= x<y
+loop=
+branchcondition=(x<0 && y<0)
+branch=x=x+7; y=y-10;
+branchcondition=(x<0 && y>=0)
+branch=x=x+7; y=y+3;
+branchcondition=
+branch=x=x+10; y=y+3;
+postcondition= x >= y && x <= y + 16
+learners=linear disjunctive

disj/cfg/zilu_disj2.cfg

@@ -0,0 +1,9 @@
+names= x y
+precondition= y>0 || x>0
+loopcondition=
+branchcondition=x>0
+branch=x++;
+branchcondition=
+branch=y++;
+postcondition=x>0 || y>0
+learners=linear disjunctive

disj/cfg/zilu_disj3.cfg

@@ -0,0 +1,12 @@
+names= x y z
+precondition= y>0 || x>0 || z>0
+loopcondition=
+#loop=if (x>0) x++; else x--; x=-1 * x;
+branchcondition=x>0
+branch=x++;
+branchcondition=y>0
+branch=y++;
+branchcondition=
+branch=z++;
+postcondition=x>0 || y>0 || z>0
+learners=linear disjunctive

disj/cmake/FindGSL.cmake

@@ -0,0 +1,27 @@
+# - Try to find GSL
+# Once done, this will define
+#
+#  GSL_FOUND - system has GSL
+#  GSL_INCLUDE_DIRS - the GSL include directories
+#  GSL_LIBRARIES - link these to use GSL
+
+include(LibFindMacros)
+
+# Include dir
+find_path(GSL_INCLUDE_DIR
+  NAMES gsl/gsl_sf.h
+  PATHS ${GSL_PKGCONF_INCLUDE_DIRS}
+)
+
+# Finally the library itself
+find_library(GSL_LIBRARY
+  NAMES gsl 
+  PATHS ${GSL_PKGCONF_LIBRARY_DIRS}
+)
+
+# Set the include dir variables and the libraries and let libfind_process do the rest.
+# NOTE: Singular variables for this library, plural for libraries this this lib depends on.
+set(GSL_PROCESS_INCLUDES GSL_INCLUDE_DIR GSL_INCLUDE_DIRS)
+set(GSL_PROCESS_LIBS GSL_LIBRARY GSL_LIBRARIES)
+libfind_process(GSL)
+

disj/cmake/FindZ3.cmake

@@ -0,0 +1,32 @@
+# - Try to find Z3
+# Once done, this will define
+#
+#  Z3_FOUND - system has Z3
+#  Z3_INCLUDE_DIRS - the Z3 include directories
+#  Z3_LIBRARIES - link these to use Z3
+
+include(LibFindMacros)
+
+# Dependencies
+# libfind_package(Z3 z3)
+
+# Use pkg-config to get hints about paths
+# libfind_pkg_check_modules(Z3_PKGCONF z3)
+
+# Include dir
+find_path(Z3_INCLUDE_DIR
+  NAMES z3.h
+  PATHS ${Z3_PKGCONF_INCLUDE_DIRS}
+)
+
+# Finally the library itself
+find_library(Z3_LIBRARY
+  NAMES z3
+  PATHS ${Z3_PKGCONF_LIBRARY_DIRS}
+)
+
+# Set the include dir variables and the libraries and let libfind_process do the rest.
+# NOTE: Singular variables for this library, plural for libraries this this lib depends on.
+set(Z3_INCLUDES Z3_INCLUDE_DIR Z3_INCLUDE_DIRS)
+set(Z3_LIBS Z3_LIBRARY Z3_LIBRARIES)
+libfind_process(Z3)

disj/cmake/FindZ3.cmake.old

@@ -0,0 +1,31 @@
+set(Z3_ROOT "/usr/local" CACHE PATH "Root of Z3 distribution.")
+find_path(Z3_INCLUDE_DIR NAMES z3.h z3++.h PATHS ${Z3_ROOT}/include NO_DEFAULT_PATH)
+#find_path(Z3_INCLUDE_DIR NAMES z3.h z3++.h PATH ${Z3_ROOT}/include /usr/local/include)
+find_library(Z3_LIBRARY NAMES z3 PATHS ${Z3_ROOT}/lib NO_DEFAULT_PATH)
+#find_library(Z3_LIBRARY NAMES z3 PATH ${Z3_ROOT}/lib /usr/local/lib)
+
+#find_path(Z3_INCLUDE_DIR NAMES z3.h z3++.h PATHS ${Z3_ROOT}/include NO_DEFAULT_PATH)
+mark_as_advanced(Z3_EXECUTABLE Z3_INCLUDE_DIR Z3_LIBRARY)
+find_program (Z3_EXECUTABLE
+	NAMES z3 PATHS ${Z3_ROOT} PATH_SUFFIXES bin 
+	DOC "z3 command line executable" NO_DEFAULT_PATH)
+	#DOC "z3 command line executable" /usr/local/bin)
+mark_as_advanced(Z3_EXECUTABLE)
+
+if (Z3_EXECUTABLE)
+	execute_process (COMMAND ${Z3_EXECUTABLE} -version
+		OUTPUT_VARIABLE z3_version
+		ERROR_QUIET
+		OUTPUT_STRIP_TRAILING_WHITESPACE)
+	if (z3_version MATCHES "^Z3 version [0-9]")
+		string (REPLACE "Z3 version " "" Z3_VERSION_STRING ${z3_version})
+	endif()
+endif()
+mark_as_advanced(Z3_VERSION_STRING)
+
+include (FindPackageHandleStandardArgs)
+find_package_handle_standard_args(Z3
+	REQUIRED_VARS Z3_LIBRARY Z3_INCLUDE_DIR Z3_EXECUTABLE
+	VERSION_VAR Z3_VERSION_STRING)
+#include_directories(${Z3_INCLUDE_DIR})
+#endif(UNIX)