diff --git a/CMakeLists.txt b/CMakeLists.txt index e52aa7c..04db93f 100644 --- a/CMakeLists.txt +++ b/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) diff --git a/benchmark/47.cfg b/benchmark/47.cfg index 28eb8c9..6f39ba5 100644 --- a/benchmark/47.cfg +++ b/benchmark/47.cfg @@ -1,7 +1,6 @@ names= x y precondition= x= y && x <= y + 16 learners=linear diff --git a/benchmark/50.cfg b/benchmark/50.cfg index 5aebebc..f42d878 100644 --- a/benchmark/50.cfg +++ b/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 diff --git a/benchmark/51.cfg b/benchmark/51.cfg index b86ff61..fe7d815 100644 --- a/benchmark/51.cfg +++ b/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 diff --git a/benchmark/README.md b/benchmark/README.md new file mode 100644 index 0000000..0c0d02c --- /dev/null +++ b/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 | diff --git a/config.h.in b/config.h.in index 7d6d569..408d50c 100644 --- a/config.h.in +++ b/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 diff --git a/disj/benchmark/44.cfg b/disj/benchmark/44.cfg new file mode 100644 index 0000000..e28343e --- /dev/null +++ b/disj/benchmark/44.cfg @@ -0,0 +1,12 @@ +names= x y +precondition= x=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 diff --git a/disj/benchmark/45.cfg b/disj/benchmark/45.cfg new file mode 100644 index 0000000..cfb5891 --- /dev/null +++ b/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 diff --git a/disj/benchmark/46.cfg b/disj/benchmark/46.cfg new file mode 100644 index 0000000..81c4326 --- /dev/null +++ b/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 diff --git a/disj/cfg/21.cfg b/disj/cfg/21.cfg new file mode 100644 index 0000000..fdf2bd0 --- /dev/null +++ b/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 diff --git a/disj/cfg/44.cfg b/disj/cfg/44.cfg new file mode 100644 index 0000000..e28343e --- /dev/null +++ b/disj/cfg/44.cfg @@ -0,0 +1,12 @@ +names= x y +precondition= x=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 diff --git a/disj/cfg/45.cfg b/disj/cfg/45.cfg new file mode 100644 index 0000000..cfb5891 --- /dev/null +++ b/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 diff --git a/disj/cfg/46.cfg b/disj/cfg/46.cfg new file mode 100644 index 0000000..81c4326 --- /dev/null +++ b/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 diff --git a/disj/cfg/f2.cfg b/disj/cfg/f2.cfg new file mode 100644 index 0000000..c36eb30 --- /dev/null +++ b/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 diff --git a/disj/cfg/fig1b.cfg b/disj/cfg/fig1b.cfg new file mode 100644 index 0000000..fdf2bd0 --- /dev/null +++ b/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 diff --git a/disj/cfg/pldi08_fig1.cfg b/disj/cfg/pldi08_fig1.cfg new file mode 100644 index 0000000..126a431 --- /dev/null +++ b/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 diff --git a/disj/cfg/zilu_disj1.cfg b/disj/cfg/zilu_disj1.cfg new file mode 100644 index 0000000..e28343e --- /dev/null +++ b/disj/cfg/zilu_disj1.cfg @@ -0,0 +1,12 @@ +names= x y +precondition= x=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 diff --git a/disj/cfg/zilu_disj2.cfg b/disj/cfg/zilu_disj2.cfg new file mode 100644 index 0000000..cfb5891 --- /dev/null +++ b/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 diff --git a/disj/cfg/zilu_disj3.cfg b/disj/cfg/zilu_disj3.cfg new file mode 100644 index 0000000..81c4326 --- /dev/null +++ b/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 diff --git a/disj/cmake/FindGSL.cmake b/disj/cmake/FindGSL.cmake new file mode 100644 index 0000000..ecc96c1 --- /dev/null +++ b/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) + diff --git a/disj/cmake/FindZ3.cmake b/disj/cmake/FindZ3.cmake new file mode 100644 index 0000000..36d43c9 --- /dev/null +++ b/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) diff --git a/disj/cmake/FindZ3.cmake.old b/disj/cmake/FindZ3.cmake.old new file mode 100644 index 0000000..b8fe657 --- /dev/null +++ b/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) diff --git a/disj/cmake/LibFindMacros.cmake b/disj/cmake/LibFindMacros.cmake new file mode 100644 index 0000000..20e3433 --- /dev/null +++ b/disj/cmake/LibFindMacros.cmake @@ -0,0 +1,98 @@ +# Works the same as find_package, but forwards the "REQUIRED" and "QUIET" arguments +# used for the current package. For this to work, the first parameter must be the +# prefix of the current package, then the prefix of the new package etc, which are +# passed to find_package. +macro (libfind_package PREFIX) + set (LIBFIND_PACKAGE_ARGS ${ARGN}) + if (${PREFIX}_FIND_QUIETLY) + set (LIBFIND_PACKAGE_ARGS ${LIBFIND_PACKAGE_ARGS} QUIET) + endif (${PREFIX}_FIND_QUIETLY) + if (${PREFIX}_FIND_REQUIRED) + set (LIBFIND_PACKAGE_ARGS ${LIBFIND_PACKAGE_ARGS} REQUIRED) + endif (${PREFIX}_FIND_REQUIRED) + find_package(${LIBFIND_PACKAGE_ARGS}) +endmacro (libfind_package) + +# CMake developers made the UsePkgConfig system deprecated in the same release (2.6) +# where they added pkg_check_modules. Consequently I need to support both in my scripts +# to avoid those deprecated warnings. Here's a helper that does just that. +# Works identically to pkg_check_modules, except that no checks are needed prior to use. +macro (libfind_pkg_check_modules PREFIX PKGNAME) + if (${CMAKE_MAJOR_VERSION} EQUAL 2 AND ${CMAKE_MINOR_VERSION} EQUAL 4) + include(UsePkgConfig) + pkgconfig(${PKGNAME} ${PREFIX}_INCLUDE_DIRS ${PREFIX}_LIBRARY_DIRS ${PREFIX}_LDFLAGS ${PREFIX}_CFLAGS) + else (${CMAKE_MAJOR_VERSION} EQUAL 2 AND ${CMAKE_MINOR_VERSION} EQUAL 4) + find_package(PkgConfig) + if (PKG_CONFIG_FOUND) + pkg_check_modules(${PREFIX} ${PKGNAME}) + endif (PKG_CONFIG_FOUND) + endif (${CMAKE_MAJOR_VERSION} EQUAL 2 AND ${CMAKE_MINOR_VERSION} EQUAL 4) +endmacro (libfind_pkg_check_modules) + +# Do the final processing once the paths have been detected. +# If include dirs are needed, ${PREFIX}_PROCESS_INCLUDES should be set to contain +# all the variables, each of which contain one include directory. +# Ditto for ${PREFIX}_PROCESS_LIBS and library files. +# Will set ${PREFIX}_FOUND, ${PREFIX}_INCLUDE_DIRS and ${PREFIX}_LIBRARIES. +# Also handles errors in case library detection was required, etc. +macro (libfind_process PREFIX) + # Skip processing if already processed during this run + if (NOT ${PREFIX}_FOUND) + # Start with the assumption that the library was found + set (${PREFIX}_FOUND TRUE) + + # Process all includes and set _FOUND to false if any are missing + foreach (i ${${PREFIX}_PROCESS_INCLUDES}) + if (${i}) + set (${PREFIX}_INCLUDE_DIRS ${${PREFIX}_INCLUDE_DIRS} ${${i}}) + mark_as_advanced(${i}) + else (${i}) + set (${PREFIX}_FOUND FALSE) + endif (${i}) + endforeach (i) + + # Process all libraries and set _FOUND to false if any are missing + foreach (i ${${PREFIX}_PROCESS_LIBS}) + if (${i}) + set (${PREFIX}_LIBRARIES ${${PREFIX}_LIBRARIES} ${${i}}) + mark_as_advanced(${i}) + else (${i}) + set (${PREFIX}_FOUND FALSE) + endif (${i}) + endforeach (i) + + # Print message and/or exit on fatal error + if (${PREFIX}_FOUND) + if (NOT ${PREFIX}_FIND_QUIETLY) + message (STATUS "Found ${PREFIX} ${${PREFIX}_VERSION}") + endif (NOT ${PREFIX}_FIND_QUIETLY) + else (${PREFIX}_FOUND) + if (${PREFIX}_FIND_REQUIRED) + foreach (i ${${PREFIX}_PROCESS_INCLUDES} ${${PREFIX}_PROCESS_LIBS}) + message("${i}=${${i}}") + endforeach (i) + message (FATAL_ERROR "Required library ${PREFIX} NOT FOUND.\nInstall the library (dev version) and try again. If the library is already installed, use ccmake to set the missing variables manually.") + endif (${PREFIX}_FIND_REQUIRED) + endif (${PREFIX}_FOUND) + endif (NOT ${PREFIX}_FOUND) +endmacro (libfind_process) + +macro(libfind_library PREFIX basename) + set(TMP "") + if(MSVC80) + set(TMP -vc80) + endif(MSVC80) + if(MSVC90) + set(TMP -vc90) + endif(MSVC90) + set(${PREFIX}_LIBNAMES ${basename}${TMP}) + if(${ARGC} GREATER 2) + set(${PREFIX}_LIBNAMES ${basename}${TMP}-${ARGV2}) + string(REGEX REPLACE "\\." "_" TMP ${${PREFIX}_LIBNAMES}) + set(${PREFIX}_LIBNAMES ${${PREFIX}_LIBNAMES} ${TMP}) + endif(${ARGC} GREATER 2) + find_library(${PREFIX}_LIBRARY + NAMES ${${PREFIX}_LIBNAMES} + PATHS ${${PREFIX}_PKGCONF_LIBRARY_DIRS} + ) +endmacro(libfind_library) diff --git a/disj/include/config.h b/disj/include/config.h index ab8033d..25b7570 100644 --- a/disj/include/config.h +++ b/disj/include/config.h @@ -20,10 +20,10 @@ * If it is not set correctly, you may come across a runtime error */ #define Nv 2 -#define Nb 1 -#define Project "04" -#define ProjectHome "/home/lijiaying/Research/GitHub/zilu/disj" -//#define Project #04 +#define Nb 3 +#define Project "44" +#define ProjectHome "/home/lijiaying/Research/zilu/disj" +//#define Project #44 /*#define Cv(i) do {int return_num##i = 1;\ for (int tempi = 0; tempi < i; i++) return_num##i *= (Nv + i);\ diff --git a/disj/include/svm.h b/disj/include/svm.h index 9b98665..e26f335 100644 --- a/disj/include/svm.h +++ b/disj/include/svm.h @@ -181,9 +181,9 @@ class SVM : public MLalgo return -1; } - //std::cout << "---------------------------------------->>>>>>\n"; - //std::cout << problem; - //problem.print_Negatives(); + std::cout << "---------------------------------------->>>>>>\n"; + std::cout << problem; + problem.print_Negatives(); int res = 0; if (kernel == 0) { res = trainLinear(); diff --git a/disj/parser/parser b/disj/parser/parser index ac2c274..57894e2 100755 Binary files a/disj/parser/parser and b/disj/parser/parser differ diff --git a/disj/parser/tokens.l b/disj/parser/tokens.l index 9d6f759..7063a14 100644 --- a/disj/parser/tokens.l +++ b/disj/parser/tokens.l @@ -36,7 +36,7 @@ static int n_learners = 0; "afterloop=" { BEGIN STRSTART; yylval.tag = ALOOP; return TAG; } "invariant=" { BEGIN STRSTART; yylval.tag = INVR; /*printf("encounter INVARIANT.\n");*/ return TAG; } [^\n]*\n { yytext[yyleng-1] = '\0'; - /*printf("\t[%d]->%s\n", yylval.tag, yytext);*/ + /*printf("\t[%d]->%s\n", yylval.tag, yytext);*/ yylval.pstr = new std::string(yytext); BEGIN INITIAL; return STRING; diff --git a/disj/scripts/build.sh b/disj/scripts/build.sh index 72fc96d..56d18fd 100755 --- a/disj/scripts/build.sh +++ b/disj/scripts/build.sh @@ -96,7 +96,8 @@ cat ../cmake.in >> $cmakefile echo "add_executable("$prefix" "$path_cpp" \${DIR_SRCS} \${HEADER})" >> $cmakefile echo "target_link_libraries("$prefix" \${Z3_LIBRARY})" >> $cmakefile echo "target_link_libraries("$prefix" \${GSL_LIBRARIES})" >> $cmakefile -echo "target_link_libraries("$target" gsl gslcblas m)" >> $cmakefile +echo "target_link_libraries("$prefix" gsl gslcblas m)" >> $cmakefile +#echo "target_link_libraries("$target" gsl gslcblas m)" >> $cmakefile echo -e $green$bold"[DONE]"$normal diff --git a/disj/test/zilu_disj1.cpp b/disj/test/zilu_disj1.cpp index c0b1ca5..3fb2a00 100644 --- a/disj/test/zilu_disj1.cpp +++ b/disj/test/zilu_disj1.cpp @@ -30,8 +30,8 @@ int loopFunction(int _reserved_input_[]) { } int main(int argc, char** argv) { - Context context("/home/lijiaying/Research/GitHub/disZILU/tmp/zilu_disj1.var", loopFunction, "loopFunction", NULL); + Context context("/home/lijiaying/Research/zilu/disj/tmp/zilu_disj1.var", loopFunction, "loopFunction", NULL); context.addLearner("linear"); - return context.learn("/home/lijiaying/Research/GitHub/disZILU/tmp/zilu_disj1.cnt", "/home/lijiaying/Research/GitHub/disZILU/tmp/zilu_disj1.inv", "/home/lijiaying/Research/GitHub/disZILU/test/zilu_disj1.pc"); + return context.learn("/home/lijiaying/Research/zilu/disj/tmp/zilu_disj1.cnt", "/home/lijiaying/Research/zilu/disj/tmp/zilu_disj1.inv", "/home/lijiaying/Research/zilu/disj/test/zilu_disj1.pc"); } diff --git a/include/config.h b/include/config.h index 8e1671b..081e925 100644 --- a/include/config.h +++ b/include/config.h @@ -20,7 +20,7 @@ * This should be set in /CMakeLists.txt file * If it is not set correctly, you may come across a runtime error */ -#define Nv 2 +#define Nv 3 /*#define Cv(i) do {int return_num##i = 1;\ for (int tempi = 0; tempi < i; i++) return_num##i *= (Nv + i);\ @@ -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 diff --git a/test/11.cpp b/test/11.cpp index 7e534ea..41a0497 100644 --- a/test/11.cpp +++ b/test/11.cpp @@ -4,21 +4,19 @@ using namespace std; using namespace iif; int loopFunction(int _reserved_input_[]) { - int i = _reserved_input_[0]; - int j = _reserved_input_[1]; - int x = _reserved_input_[2]; + int x = _reserved_input_[0]; + int n = _reserved_input_[1]; - iif_assume(j==0&&i==0&&x>=0); + iif_assume(x==0 && n>0); - while(i0)); - while(xy){ - y++; - } + while(j>0 && n>0) { + recordi(j, k, n); + j--; + k--; } - recordi(n, x, y); + recordi(j, k, n); - iif_assert(y==n); + iif_assert( (k == 0)); return 0; } @@ -28,8 +26,8 @@ int loopFunction(int _reserved_input_[]) { int main(int argc, char** argv) { iifround = atoi(argv[1]); initseed = atoi(argv[2]); - iifContext context("/home/lijiaying/Research/GitHub/zilu/tmp/19.var", loopFunction, "loopFunction", "/home/lijiaying/Research/GitHub/zilu/tmp/19.ds"); + iifContext context("/home/lijiaying/Research/zilu/tmp/19.var", loopFunction, "loopFunction", "/home/lijiaying/Research/zilu/tmp/19.ds"); context.addLearner("conjunctive"); - return context.learn("/home/lijiaying/Research/GitHub/zilu/tmp/19.cnt", "/home/lijiaying/Research/GitHub/zilu/tmp/19"); + return context.learn("/home/lijiaying/Research/zilu/tmp/19.cnt", "/home/lijiaying/Research/zilu/tmp/19"); } diff --git a/test/20.cpp b/test/20.cpp index cbddaf6..ac38832 100644 --- a/test/20.cpp +++ b/test/20.cpp @@ -4,27 +4,21 @@ using namespace std; using namespace iif; int loopFunction(int _reserved_input_[]) { - int x = _reserved_input_[0]; - int y = _reserved_input_[1]; - int k = _reserved_input_[2]; + int i = _reserved_input_[0]; + int n = _reserved_input_[1]; + int sum = _reserved_input_[2]; - iif_assume((x+y)== k); + iif_assume(i==0 && n>=0 && n<=100 && sum==0); - while(rand()%2) { - recordi(x, y, k); - if(rand()%2){ - x++; - y--; - } - else{ - y++; - x--; - } + while(i=0); return 0; } @@ -32,8 +26,8 @@ int loopFunction(int _reserved_input_[]) { int main(int argc, char** argv) { iifround = atoi(argv[1]); initseed = atoi(argv[2]); - iifContext context("/home/lijiaying/Research/GitHub/zilu/tmp/20.var", loopFunction, "loopFunction", "/home/lijiaying/Research/GitHub/zilu/tmp/20.ds"); + iifContext context("/home/lijiaying/Research/zilu/tmp/20.var", loopFunction, "loopFunction", "/home/lijiaying/Research/zilu/tmp/20.ds"); context.addLearner("conjunctive"); - return context.learn("/home/lijiaying/Research/GitHub/zilu/tmp/20.cnt", "/home/lijiaying/Research/GitHub/zilu/tmp/20"); + return context.learn("/home/lijiaying/Research/zilu/tmp/20.cnt", "/home/lijiaying/Research/zilu/tmp/20"); } diff --git a/test/23.cpp b/test/23.cpp index 29598e8..0b47b91 100644 --- a/test/23.cpp +++ b/test/23.cpp @@ -5,20 +5,19 @@ using namespace iif; int loopFunction(int _reserved_input_[]) { int i = _reserved_input_[0]; - int n = _reserved_input_[1]; - int sum = _reserved_input_[2]; + int j = _reserved_input_[1]; - iif_assume( n>=0&&i==0&&sum==0); + iif_assume(i==0 && j==0); - while( i=0); + iif_assert(j==200); return 0; } @@ -26,8 +25,8 @@ int loopFunction(int _reserved_input_[]) { int main(int argc, char** argv) { iifround = atoi(argv[1]); initseed = atoi(argv[2]); - iifContext context("/home/lijiaying/Research/GitHub/zilu/tmp/23.var", loopFunction, "loopFunction", "/home/lijiaying/Research/GitHub/zilu/tmp/23.ds"); + iifContext context("/home/lijiaying/Research/zilu/tmp/23.var", loopFunction, "loopFunction", "/home/lijiaying/Research/zilu/tmp/23.ds"); context.addLearner("conjunctive"); - return context.learn("/home/lijiaying/Research/GitHub/zilu/tmp/23.cnt", "/home/lijiaying/Research/GitHub/zilu/tmp/23"); + return context.learn("/home/lijiaying/Research/zilu/tmp/23.cnt", "/home/lijiaying/Research/zilu/tmp/23"); } diff --git a/test/28.cpp b/test/28.cpp index 5c8e42b..020502b 100644 --- a/test/28.cpp +++ b/test/28.cpp @@ -4,21 +4,25 @@ using namespace std; using namespace iif; int loopFunction(int _reserved_input_[]) { - int x = _reserved_input_[0]; - int y = _reserved_input_[1]; + int i = _reserved_input_[0]; + int j = _reserved_input_[1]; - iif_assume( x == y && y >=0); + if (i < 0) i = -i; if (j < 0) j = -j; if (i == 0) i = 1; if (j == 0) j = 1; + iif_assume( i * i < j * j); - while(x!=0) { - recordi(x, y); - x--; - y--; - if (x<0 || y<0) break; + while( i < j) { + recordi(i, j); + j = j - i; + if (j < i) { + j = j + i; + i = j - i; + j = j - i; + } } - recordi(x, y); + recordi(i, j); - iif_assert(y==0); + iif_assert(j == i); return 0; } @@ -26,8 +30,8 @@ int loopFunction(int _reserved_input_[]) { int main(int argc, char** argv) { iifround = atoi(argv[1]); initseed = atoi(argv[2]); - iifContext context("/home/lijiaying/Research/GitHub/zilu/tmp/28.var", loopFunction, "loopFunction", "/home/lijiaying/Research/GitHub/zilu/tmp/28.ds"); - context.addLearner("conjunctive"); - return context.learn("/home/lijiaying/Research/GitHub/zilu/tmp/28.cnt", "/home/lijiaying/Research/GitHub/zilu/tmp/28"); + iifContext context("/home/lijiaying/Research/zilu/tmp/28.var", loopFunction, "loopFunction", "/home/lijiaying/Research/zilu/tmp/28.ds"); + context.addLearner("linear"); + return context.learn("/home/lijiaying/Research/zilu/tmp/28.cnt", "/home/lijiaying/Research/zilu/tmp/28"); } diff --git a/test/30.cpp b/test/30.cpp index f4bdfce..eb9fb0a 100644 --- a/test/30.cpp +++ b/test/30.cpp @@ -4,20 +4,20 @@ using namespace std; using namespace iif; int loopFunction(int _reserved_input_[]) { - int i = _reserved_input_[0]; - int c = _reserved_input_[1]; + int x = _reserved_input_[0]; + int y = _reserved_input_[1]; - iif_assume( i>=0&&c>=i); + iif_assume( y == x); - while(i<40) { - recordi(i, c); - c=c+i; - i++; + while(rand()%2) { + recordi(x, y); + x++; + y++; } - recordi(i, c); + recordi(x, y); - iif_assert(c>=0); + iif_assert(x == y); return 0; } @@ -25,8 +25,8 @@ int loopFunction(int _reserved_input_[]) { int main(int argc, char** argv) { iifround = atoi(argv[1]); initseed = atoi(argv[2]); - iifContext context("/home/lijiaying/Research/GitHub/zilu/tmp/30.var", loopFunction, "loopFunction", "/home/lijiaying/Research/GitHub/zilu/tmp/30.ds"); + iifContext context("/home/lijiaying/Research/zilu/tmp/30.var", loopFunction, "loopFunction", "/home/lijiaying/Research/zilu/tmp/30.ds"); context.addLearner("conjunctive"); - return context.learn("/home/lijiaying/Research/GitHub/zilu/tmp/30.cnt", "/home/lijiaying/Research/GitHub/zilu/tmp/30"); + return context.learn("/home/lijiaying/Research/zilu/tmp/30.cnt", "/home/lijiaying/Research/zilu/tmp/30"); } diff --git a/test/35.cpp b/test/35.cpp index d300aab..798be74 100644 --- a/test/35.cpp +++ b/test/35.cpp @@ -23,8 +23,8 @@ int loopFunction(int _reserved_input_[]) { int main(int argc, char** argv) { iifround = atoi(argv[1]); initseed = atoi(argv[2]); - iifContext context("/home/lijiaying/Research/GitHub/zilu/tmp/35.var", loopFunction, "loopFunction", "/home/lijiaying/Research/GitHub/zilu/tmp/35.ds"); + iifContext context("/home/lijiaying/Research/zilu/tmp/35.var", loopFunction, "loopFunction", "/home/lijiaying/Research/zilu/tmp/35.ds"); context.addLearner("linear"); - return context.learn("/home/lijiaying/Research/GitHub/zilu/tmp/35.cnt", "/home/lijiaying/Research/GitHub/zilu/tmp/35"); + return context.learn("/home/lijiaying/Research/zilu/tmp/35.cnt", "/home/lijiaying/Research/zilu/tmp/35"); } diff --git a/test/41.cpp b/test/41.cpp index 58dd540..1d5602f 100644 --- a/test/41.cpp +++ b/test/41.cpp @@ -27,8 +27,8 @@ int loopFunction(int _reserved_input_[]) { int main(int argc, char** argv) { iifround = atoi(argv[1]); initseed = atoi(argv[2]); - iifContext context("/home/lijiaying/Research/GitHub/zilu/tmp/41.var", loopFunction, "loopFunction", "/home/lijiaying/Research/GitHub/zilu/tmp/41.ds"); + iifContext context("/home/lijiaying/Research/zilu/tmp/41.var", loopFunction, "loopFunction", "/home/lijiaying/Research/zilu/tmp/41.ds"); context.addLearner("conjunctive"); - return context.learn("/home/lijiaying/Research/GitHub/zilu/tmp/41.cnt", "/home/lijiaying/Research/GitHub/zilu/tmp/41"); + return context.learn("/home/lijiaying/Research/zilu/tmp/41.cnt", "/home/lijiaying/Research/zilu/tmp/41"); } diff --git a/test/43.cpp b/test/43.cpp index dd0783d..3e9d514 100644 --- a/test/43.cpp +++ b/test/43.cpp @@ -6,20 +6,18 @@ using namespace iif; int loopFunction(int _reserved_input_[]) { int x = _reserved_input_[0]; int y = _reserved_input_[1]; - int t = _reserved_input_[2]; - iif_assume(t==y); + iif_assume( x < 100 && y < 100); - while(rand()%2) { - recordi(x, y, t); - if(x>0){ - y=y+x; - } + while( x < 100 && y < 100 ) { + recordi(x, y); + x=x+1; + y=y+1; } - recordi(x, y, t); + recordi(x, y); - iif_assert(y>=t); + iif_assert( x == 100 || y == 100); return 0; } @@ -27,8 +25,8 @@ int loopFunction(int _reserved_input_[]) { int main(int argc, char** argv) { iifround = atoi(argv[1]); initseed = atoi(argv[2]); - iifContext context("/home/lijiaying/Research/GitHub/zilu/tmp/43.var", loopFunction, "loopFunction", "/home/lijiaying/Research/GitHub/zilu/tmp/43.ds"); + iifContext context("/home/lijiaying/Research/zilu/tmp/43.var", loopFunction, "loopFunction", "/home/lijiaying/Research/zilu/tmp/43.ds"); context.addLearner("conjunctive"); - return context.learn("/home/lijiaying/Research/GitHub/zilu/tmp/43.cnt", "/home/lijiaying/Research/GitHub/zilu/tmp/43"); + return context.learn("/home/lijiaying/Research/zilu/tmp/43.cnt", "/home/lijiaying/Research/zilu/tmp/43"); }