Merged master branch in

.project

@@ -5,16 +5,6 @@
 	<projects>
 	</projects>
 	<buildSpec>
-		<buildCommand>
-			<name>org.eclipse.ui.externaltools.ExternalToolBuilder</name>
-			<triggers>full,incremental,</triggers>
-			<arguments>
-				<dictionary>
-					<key>LaunchConfigHandle</key>
-					<value>&lt;project&gt;/.externalToolBuilders/cmake.launch</value>
-				</dictionary>
-			</arguments>
-		</buildCommand>
 		<buildCommand>
 			<name>org.eclipse.cdt.managedbuilder.core.genmakebuilder</name>
 			<triggers>clean,full,incremental,</triggers>

.travis.yml

@@ -3,7 +3,7 @@ language: cpp
 notifications:
   slack: sriformalmethods:wSnZggI8D3mxI5uqDsElZbV2
 
-sudo: false
+sudo: true
 
 compiler:
   # - clang (Disabling until boost and clang play well)
@@ -20,6 +20,7 @@ env:
 
 addons:
   apt:
+    update: true
     sources:
       - boost-latest
     packages:
@@ -32,10 +33,6 @@ addons:
       - default-jre
       - gperf
 
-cache:
-  directories:
-    - $HOME/yices2
-
 install:
   - bash contrib/install_yices2.sh
   - if [[ $ENABLE_COVERAGE == ON ]]; then 
@@ -44,7 +41,7 @@ install:
 
 script:
   - cd build
-  - cmake -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} -DENABLE_COVERAGE=${ENABLE_COVERAGE} -DYICES2_HOME=$HOME/yices2 ..
+  - cmake -DCMAKE_BUILD_TYPE=${CMAKE_BUILD_TYPE} -DENABLE_COVERAGE=${ENABLE_COVERAGE} ..
   - make 
   - make check
 

CMakeLists.txt

@@ -35,7 +35,7 @@ endif (CMAKE_SIZEOF_VOID_P EQUAL 8)
 
 # Find the GMP number library
 if (SALLY_STATIC_BUILD)
-	find_library(GMP_LIBRARY libgmp.a gmp)
+  find_library(GMP_LIBRARY libgmp.a gmp)
 else()
   find_library(GMP_LIBRARY gmp)
 endif()
@@ -45,12 +45,22 @@ else()
   message(FATAL_ERROR "Could not the GMP number library (sudo apt-get install libgmp-dev)")
 endif()
 
-# Find Yices
-SET(YICES2_HOME CACHE STRING "Yices2 installation directory")
-find_package(Yices2 2.3.0)
-if (YICES2_FOUND)
-  add_definitions(-DWITH_YICES2)
-  include_directories(${YICES2_INCLUDE_DIR}) 
+# Find LibPoly
+SET(LIBPOLY_HOME CACHE STRING "LibPoly installation directory")
+find_package(LibPoly 0.1.5)
+if (LIBPOLY_FOUND)
+  add_definitions(-DWITH_LIBPOLY)
+  include_directories(${LIBPOLY_INCLUDE_DIR})
+endif()
+
+# Find Yices if LibPoly is there
+if (LIBPOLY_FOUND)
+  SET(YICES2_HOME CACHE STRING "Yices2 installation directory")
+  find_package(Yices2 2.6.0)
+  if (YICES2_FOUND)
+    add_definitions(-DWITH_YICES2)
+    include_directories(${YICES2_INCLUDE_DIR}) 
+  endif()
 endif()
 
 # Find MathSAT5

README.md

@@ -20,7 +20,7 @@ sudo apt-get install libgmp-dev
 sudo apt-get install libboost-program-options-dev libboost-iostreams-dev libboost-test-dev libboost-thread-dev libboost-system-dev
 sudo apt-get install default-jre
 ```
-In addition, Sally needs an SMT solver for reasoning about the systems. It currently supports [Yices2](http://yices.csl.sri.com/) and [MathSAT5](http://mathsat.fbk.eu/), and for best results we recommend using both of them. 
+In addition, Sally needs an SMT solver for reasoning about the systems. It currently supports [Yices2](http://yices.csl.sri.com/), [MathSAT5](http://mathsat.fbk.eu/), and [Z3](https://github.com/Z3Prover/z3). For best results we recommend using at least Yices2 and MathSAT5. 
 
 ## How to Compile
 
@@ -42,7 +42,8 @@ cmake .. -DMATHSAT5_HOME=$MD
 make
 make check
 ```
-Of course, you can use both Yices2 and MathSAT by adding both options to 
+Similarly, to find Z3, you can set the Z3_HOME variable with cmake. Of course, 
+you can use, e.g., both Yices2 and MathSAT, by adding both options to 
 cmake as expected.
 
 To compile sally in debug mode then configure and build with
@@ -53,6 +54,11 @@ make
 make check
 ```
 
+In order to use the non-linear capabilities of Yices2 in Sally, the 
+version of Yices2 used mused be compiled with MCSAT enabled, and LibPoly 
+must be available. Similar to above, you can pass `-DLIBPOLY_HOME=$LPD` 
+to cmake if LibPoly is installed in a non-standard location. 
+
 ### Input Language
 
 Sally takes as input a simple description of transition systems based on the 
@@ -218,8 +224,8 @@ unknown
 
 * Checking the property with BMC with a bigger bound and showing any 
 counter-example traces
-> sally --engine bmc --bmc-max 20 --show-trace examples/example.mcmt
 ```bash
+> sally --engine bmc --bmc-max 20 --show-trace examples/example.mcmt
 unknown
 unknown
 unknown
@@ -259,3 +265,54 @@ valid
 invalid
 valid
 ```
+
+* Checking nonlinear properties with Yices2 
+
+By relying on Yices2 with support for MCSAT, you can use Sally to reason 
+about (polynomial) non-linear systems using BMC and k-induction. The
+following example models two systems computing sums `S1 = 1 + 2 + ... + n` and
+`S2 = 1^2 + 2^2 + ... + n^2`, and asks whether `S1 = n*(n+1)/2` and 
+`S2 = n*(n+1)*(2n+1)/6`. 
+
+```lisp
+;; Maintain Sum and n
+(define-state-type ST ((Sum Real) (n Real)))
+;; Initial states: Sum = 0, n = 0
+(define-states Init ST (and (= Sum 0) (= n 0)))
+
+;; Transition: Sum += n; n ++;
+(define-transition Trans1 ST (and 
+  (= next.Sum (+ state.Sum state.n))
+  (= next.n (+ state.n 1))
+))   
+
+;; Transition system: Sum = 1 + 2 + ... + (n-1)
+(define-transition-system T1 ST Init Trans1)
+;; Sum = n*(n-1)/2
+(query T1 (= Sum (/ (* n (- n 1)) 2)))
+
+;; Transition: Sum += n^2; n ++;
+(define-transition Trans2 ST (and 
+    (= next.Sum (+ state.Sum (* state.n state.n)))
+    (= next.n (+ state.n 1))
+))   
+
+;; Transition system: Sum = 1^2 + 2^2 + ... + (n-1)^2
+(define-transition-system T2 ST Init Trans2)
+;; Sum = n*(n-1)/2
+(query T2 (= Sum (/ (* n (- n 1) (- (* 2 n) 1)) 6)))
+
+```
+
+We can prove these two properties with Sally by using Yices2 with MCSAT 
+as follows
+
+```bash
+> sally --engine kind --yices2-mcsat ../examples/example-nra.mcmt
+valid
+valid
+```
+
+
+
+

cmake/FindLibPoly.cmake

@@ -0,0 +1,56 @@
+# - Try to find LibPoly
+# Once done this will define
+#  LIBPOLY_FOUND - System has LibPoly
+#  LIBPOLY_INCLUDE_DIRS - The LibPoly include directories
+#  LIBPOLY_LIBRARIES - The libraries needed to use LibPoly
+
+if (LIBPOLY_HOME)
+  find_path(LIBPOLY_INCLUDE_DIR poly/poly.h PATHS "${LIBPOLY_HOME}/include")
+else() 
+  find_path(LIBPOLY_INCLUDE_DIR poly/poly.h)
+endif()
+
+if (SALLY_STATIC_BUILD)
+  if (LIBPOLY_HOME)
+    find_library(LIBPOLY_LIBRARY libpoly.a poly PATHS "${LIBPOLY_HOME}/lib")
+  else() 
+    find_library(LIBPOLY_LIBRARY libpoly.a poly)
+  endif()
+else()
+  if (LIBPOLY_HOME)
+    find_library(LIBPOLY_LIBRARY poly PATHS "${LIBPOLY_HOME}/lib")
+  else() 
+    find_library(LIBPOLY_LIBRARY poly)
+  endif()
+endif()
+
+# If library found, check the version
+if (LIBPOLY_INCLUDE_DIR AND LibPoly_FIND_VERSION)
+
+  # Check version. It is in poly/version.h of the form 
+  # 
+  # #define LIBPOLY_VERSION 0.1.1
+
+  # Extract version lines from yices.h
+  file(STRINGS "${LIBPOLY_INCLUDE_DIR}/poly/version.h" LIBPOLY_H_VERSION REGEX "#define LIBPOLY_VERSION")
+  if("${LIBPOLY_H_VERSION}" MATCHES ".*#define LIBPOLY_VERSION[ ]+([0-9]+\\.[0-9]+\\.[0-9]+).*")
+    set(LIBPOLY_VERSION "${CMAKE_MATCH_1}")
+  endif()
+
+  # Compare the found version to asked for version
+  if ("${LIBPOLY_VERSION}" VERSION_LESS "${LibPoly_FIND_VERSION}")
+    unset(LIBPOLY_INCLUDE_DIR CACHE)
+    unset(LIBPOLY_LIBRARY CACHE)
+  elseif (LibPoly_FIND_VERSION_EXACT AND NOT "${LIBPOLY_VERSION}" VERSION_EQUAL "${LibPoly_FIND_VERSION}")
+    unset(LIBPOLY_INCLUDE_DIR CACHE)
+    unset(LIBPOLY_LIBRARY CACHE) 
+  endif()
+endif()
+
+set(LIBPOLY_LIBRARIES ${LIBPOLY_LIBRARY})
+set(LIBPOLY_INCLUDE_DIRS ${LIBPOLY_INCLUDE_DIR})
+
+include(FindPackageHandleStandardArgs)
+find_package_handle_standard_args(LibPoly DEFAULT_MSG LIBPOLY_LIBRARY LIBPOLY_INCLUDE_DIR)
+
+mark_as_advanced(LIBPOLY_INCLUDE_DIR LIBPOLY_LIBRARY)

cmake/FindZ3.cmake

@@ -19,7 +19,7 @@ endif()
 # If library found, check the version
 if (Z3_INCLUDE_DIR AND Z3_LIBRARY AND Z3_FIND_VERSION)
 
-	# Check version from char *msat_get_version(void)
+  # Check version from char *msat_get_version(void)
   file(WRITE "${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/src.cpp" "
     #include <stdio.h>
     #include \"z3.h\"
@@ -47,8 +47,8 @@ if (Z3_INCLUDE_DIR AND Z3_LIBRARY AND Z3_FIND_VERSION)
       VERSION_TEST_RUN_OUTPUT
   )
 
-	if (NOT VERSION_TEST_COMPILED)
-  	unset(Z3_INCLUDE_DIR CACHE)
+  if (NOT VERSION_TEST_COMPILED)
+    unset(Z3_INCLUDE_DIR CACHE)
     unset(Z3_LIBRARY CACHE)
   elseif (NOT ("${VERSION_TEST_EXITCODE}" EQUAL 0))
     unset(Z3_INCLUDE_DIR CACHE)
@@ -57,16 +57,16 @@ if (Z3_INCLUDE_DIR AND Z3_LIBRARY AND Z3_FIND_VERSION)
     # Output is of the form: major.minor.build_number.revision
     if("${VERSION_TEST_RUN_OUTPUT}" MATCHES "([0-9]*\\.[0-9]*\\.[0-9]*\\.[0-9]*)")
       set(Z3_VERSION "${CMAKE_MATCH_1}")
-  	  if ("${Z3_VERSION}" VERSION_LESS "${Z3_FIND_VERSION}")
-    	  unset(Z3_INCLUDE_DIR CACHE)
-    	  unset(Z3_LIBRARY CACHE)
-  	  elseif (Z3_FIND_VERSION_EXACT AND NOT "${Z3_VERSION}" VERSION_EQUAL "${Z3_FIND_VERSION}")
-    	  unset(Z3_INCLUDE_DIR CACHE)
-     	  unset(Z3_LIBRARY CACHE)
-  	  endif()
+      if ("${Z3_VERSION}" VERSION_LESS "${Z3_FIND_VERSION}")
+    	unset(Z3_INCLUDE_DIR CACHE)
+    	unset(Z3_LIBRARY CACHE)
+      elseif (Z3_FIND_VERSION_EXACT AND NOT "${Z3_VERSION}" VERSION_EQUAL "${Z3_FIND_VERSION}")
+    	unset(Z3_INCLUDE_DIR CACHE)
+     	unset(Z3_LIBRARY CACHE)
+      endif()
     else()
-   	  unset(Z3_INCLUDE_DIR CACHE)
-  	  unset(Z3_LIBRARY CACHE)
+      unset(Z3_INCLUDE_DIR CACHE)
+      unset(Z3_LIBRARY CACHE)
     endif()
   endif()
 endif()

contrib/install_yices2.sh

@@ -1,11 +1,21 @@
 #!/bin/bash
 set -e 
 
-# Check if the yices2 folder is empty
-if [ ! -d "$HOME/yices2/lib" ]; then
-  wget "http://yices.csl.sri.com/cgi-bin/yices2-newnewdownload.cgi?file=yices-2.3.1-src.tar.gz&accept=I+Agree" -O yices.tar.gz
-  tar xzvf yices.tar.gz
-  cd yices* && autoconf && ./configure --prefix=$HOME/yices2 && make MODE=release && make MODE=release install && cd ..
-else
-  echo 'Using cached directory.';
-fi
+# libpoly
+pushd .
+git clone https://github.com/SRI-CSL/libpoly.git
+cd libpoly/build
+cmake -DCMAKE_BUILD_TYPE=Release ..
+make
+sudo make install
+popd 
+
+# yices2
+pushd .
+git clone https://github.com/SRI-CSL/yices2.git
+cd yices2
+autoconf
+./configure --enable-mcsat 
+make 
+sudo make install
+popd 

examples/example-nra.mcmt

@@ -0,0 +1,30 @@
+;; Maintain Sum and n
+(define-state-type ST ((Sum Real) (n Real)))
+;; Initial states: Sum = 0, n = 0
+(define-states Init ST (and (= Sum 0) (= n 0)))
+
+;; Transition: Sum += n
+(define-transition Trans1 ST 
+  (and 
+    (= next.Sum (+ state.Sum state.n))
+    (= next.n (+ state.n 1))
+  )
+)   
+
+;; Transition system: Sum = 1 + 2 + ... + (n-1)
+(define-transition-system T1 ST Init Trans1)
+;; Sum = n*(n-1)/2
+(query T1 (= Sum (/ (* n (- n 1)) 2)))
+
+;; Transition: Sum += n^2
+(define-transition Trans2 ST 
+  (and 
+    (= next.Sum (+ state.Sum (* state.n state.n)))
+    (= next.n (+ state.n 1))
+  )
+)   
+
+;; Transition system: Sum = 1^2 + 2^2 + ... + (n-1)^2
+(define-transition-system T2 ST Init Trans2)
+;; Sum = n*(n-1)/2
+(query T2 (= Sum (/ (* n (- n 1) (- (* 2 n) 1)) 6)))

src/CMakeLists.txt

@@ -27,6 +27,9 @@ target_link_libraries(sally ${sally_LIBS})
 if (YICES2_FOUND)
   target_link_libraries(sally ${YICES2_LIBRARY})
 endif()
+if (LIBPOLY_FOUND)
+  target_link_libraries(sally ${LIBPOLY_LIBRARY})
+endif()
 if (MATHSAT5_FOUND)
   target_link_libraries(sally ${MATHSAT5_LIBRARY})
 endif()
@@ -59,7 +62,7 @@ foreach(FILE ${regressions})
     # Get the gold output
     file(READ "${FILE}.gold" GOLD_OUTPUT)
     # Set the output
-    set_tests_properties(${FILE} PROPERTIES PASS_REGULAR_EXPRESSION ${GOLD_OUTPUT})
+    set_tests_properties(${FILE} PROPERTIES PASS_REGULAR_EXPRESSION "${GOLD_OUTPUT}")
   endif()
 
 endforeach(FILE)