Adding STP solver @GSoC 2019

.classpath

@@ -21,11 +21,12 @@
 	<classpathentry kind="lib" path="lib/java/test/truth-java8-extension.jar" sourcepath="lib/java-contrib/truth-java8-extension-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/runtime/checker-qual.jar" sourcepath="lib/java-contrib/checker-qual-sources.jar"/>
 	<classpathentry kind="lib" path="lib/java/test/diffutils.jar"/>
-	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-1.8"/>
 	<classpathentry kind="src" path=".apt-generated">
 		<attributes>
 			<attribute name="optional" value="true"/>
 		</attributes>
 	</classpathentry>
+	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
+	<classpathentry kind="lib" path="lib/stpJavaAPI.jar"/>
 	<classpathentry kind="output" path="bin"/>
 </classpath>

.gitignore

@@ -1,3 +1,8 @@
+/native-library-files/stp_project/stp
+/native-library-files/stp_project/stpJ/build
+/native-library-files/stp_project/stpJ/files
+/native-library-files/stp_project/stpJ/install_include
+
 .idea/workspace.xml
 .factorypath
 

.settings/org.eclipse.jdt.core.prefs

@@ -133,6 +133,7 @@ org.eclipse.jdt.core.compiler.problem.unusedTypeParameter=warning
 org.eclipse.jdt.core.compiler.problem.unusedWarningToken=ignore
 org.eclipse.jdt.core.compiler.problem.varargsArgumentNeedCast=warning
 org.eclipse.jdt.core.compiler.processAnnotations=enabled
+org.eclipse.jdt.core.compiler.release=disabled
 org.eclipse.jdt.core.compiler.source=1.8
 org.eclipse.jdt.core.formatter.align_fields_grouping_blank_lines=2147483647
 org.eclipse.jdt.core.formatter.align_type_members_on_columns=false
@@ -223,11 +224,9 @@ org.eclipse.jdt.core.formatter.indent_statements_compare_to_body=true
 org.eclipse.jdt.core.formatter.indent_switchstatements_compare_to_cases=true
 org.eclipse.jdt.core.formatter.indent_switchstatements_compare_to_switch=true
 org.eclipse.jdt.core.formatter.indentation.size=4
-org.eclipse.jdt.core.formatter.insert_new_line_after_annotation=insert
 org.eclipse.jdt.core.formatter.insert_new_line_after_annotation_on_enum_constant=insert
 org.eclipse.jdt.core.formatter.insert_new_line_after_annotation_on_field=insert
 org.eclipse.jdt.core.formatter.insert_new_line_after_annotation_on_local_variable=insert
-org.eclipse.jdt.core.formatter.insert_new_line_after_annotation_on_member=insert
 org.eclipse.jdt.core.formatter.insert_new_line_after_annotation_on_method=insert
 org.eclipse.jdt.core.formatter.insert_new_line_after_annotation_on_package=insert
 org.eclipse.jdt.core.formatter.insert_new_line_after_annotation_on_parameter=do not insert

build.xml

@@ -39,6 +39,9 @@
     <path id="classpath">
         <pathelement location="${class.dir}"/>
         <fileset dir="${ivy.lib.dir}" includes="runtime/*.jar test/*.jar build/annotations.jar build/auto-value-annotations.jar build/error_prone_annotations.jar"/>
+    	<fileset dir="lib">
+    	    <include name="**/*.jar" />
+    	</fileset>
     </path>
 
     <!-- Needs to include all annotation processors and error-prone -->

native-library-files/stp_project/.vscode/c_cpp_properties.json

@@ -0,0 +1,17 @@
+{
+    "configurations": [
+        {
+            "name": "Linux",
+            "includePath": [
+                "${workspaceFolder}/**"
+            ],
+            "defines": [],
+            "compilerPath": "/usr/bin/gcc",
+            "cStandard": "c11",
+            "cppStandard": "c++17",
+            "intelliSenseMode": "clang-x64",
+            "compileCommands": "${workspaceFolder}/stp/build/compile_commands.json"
+        }
+    ],
+    "version": 4
+}

native-library-files/stp_project/.vscode/settings.json

@@ -0,0 +1,55 @@
+{
+    "files.associations": {
+        "cstdlib": "cpp",
+        "extstpswigapi.h": "c",
+        "cassert": "cpp",
+        "iostream": "cpp",
+        "cctype": "cpp",
+        "clocale": "cpp",
+        "cmath": "cpp",
+        "cstdarg": "cpp",
+        "cstddef": "cpp",
+        "cstdio": "cpp",
+        "cstring": "cpp",
+        "ctime": "cpp",
+        "cwchar": "cpp",
+        "cwctype": "cpp",
+        "array": "cpp",
+        "atomic": "cpp",
+        "*.tcc": "cpp",
+        "cstdint": "cpp",
+        "deque": "cpp",
+        "list": "cpp",
+        "unordered_map": "cpp",
+        "unordered_set": "cpp",
+        "vector": "cpp",
+        "exception": "cpp",
+        "algorithm": "cpp",
+        "functional": "cpp",
+        "iterator": "cpp",
+        "map": "cpp",
+        "memory": "cpp",
+        "memory_resource": "cpp",
+        "numeric": "cpp",
+        "random": "cpp",
+        "set": "cpp",
+        "string": "cpp",
+        "system_error": "cpp",
+        "tuple": "cpp",
+        "type_traits": "cpp",
+        "utility": "cpp",
+        "fstream": "cpp",
+        "initializer_list": "cpp",
+        "iomanip": "cpp",
+        "iosfwd": "cpp",
+        "istream": "cpp",
+        "limits": "cpp",
+        "new": "cpp",
+        "ostream": "cpp",
+        "sstream": "cpp",
+        "stdexcept": "cpp",
+        "streambuf": "cpp",
+        "cinttypes": "cpp",
+        "typeinfo": "cpp"
+    }
+}

native-library-files/stp_project/Readme.md

@@ -0,0 +1,41 @@
+
+# README: Scripts and Directory Structure
+
+## ./stp
+
+This contains STP source code, cloned from its Github repo. This folder is created by a script that clones the repo.
+
+## ./stp_extend
+
+In order to extend the STP api, it was necessary to directly modify some source files. This folder contains these source files : *c_interface.h*, *ext_c_interface.cpp* and *CMakeLists.txt*. These files should be modified directly in these folder since the build script will be copying them to replace the one in STP source. **Please edit the source for extending STP inside this folder**
+
+## ./stpJ
+
+Contains the folders and files necessary to build the Java Binding for STP. There is an attempt to extend the interface at the level of Java Binding the sources for this is in folders */stpJ/include/* and */stpJ/src/*.
+
+The raw STP library (before binding) is installed inside the folder */stpJ/install_include/*, Cmake should locate it there. 
+
+*/stpJ/build/* contains build files for the Java binding. The resulting object files are copied to their appropriate java-smt's library folders.
+
+*/stpJ/StpJavaApi.i* is the SWIG interface used to generate an interface for the Java Binding.
+
+## ./install_prereq.sh and ./dependencies
+
+STP requires some dependencies, *./install_prereq.sh* calls a script inside *./dependencies/* which installs them. It also clones cryptominisat into this folder and build it before installing it.
+
+## ./clean_up.sh
+
+This removes build files for the binding and also the source files for cryptominisat.
+
+## ./clean_and_build_stp.sh
+
+This removes build files for the Java binding, then copies the STP extension files to replace corresponding files in the STP source. It then builds the raw STP.
+
+## ./clean_clone_build_stp.sh
+
+This removes all build files for raw STP and the Java binding. It also removes the STP source and reclones it for it Github repo. Then copies the STP extension files to replace corresponding files in the STP source. It then builds the raw STP.
+
+## ./build_raw_to_java_api.sh
+
+This is the script that builds the Java Binding for STP. It clones the STP source from Githib if not found otherwise it asks if you want to rebuild the raw STP, if 'y' it calls */clean_and_build_stp.sh* before going ahead to build the Java Binding.
+

native-library-files/stp_project/build_raw_to_java_api.sh

@@ -0,0 +1,76 @@
+#!/usr/bin/etc/ bash
+
+set -e
+set -u
+
+# Gets the normal STP library, if not found it is cloned and built.
+# Afterwards, using SWIG we define a new API and generate its JNI bindings
+# The new API is rebuild as a shared library and the JNI Java classes generated
+# The resulting .so library and the binding classes (compile to a .jar) 
+# are copied into appropriate folder in java-smt.
+
+
+STP_LIB=./stp/build/lib/libstp.so
+
+
+PRJ_DIR="${PWD%/*/*}"
+PRJ_NAME=$(basename "$PRJ_DIR")
+
+
+# confirm expected directory structure 
+# MUST BE like java-smt/../../this_script.sh
+if [[ "$PRJ_NAME" != "java-smt" ]]
+ then
+	echo "this script is not place in the proper directory" >&2
+	echo "this script expects to reside in somewhere like\
+	 .../java-smt/dir_1/dir_2/build_raw_to_java_api.sh" >&2 
+	exit 1
+fi
+
+# set destination directory for final libraries
+JAR_LIB_DIR="${PRJ_DIR}/lib/"
+SO_LIB_DIR="${JAR_LIB_DIR}/native/x86_64-linux/"
+
+
+# echo $FILE
+echo ---
+if [! -f "$STP_LIB" ]
+ then
+	echo "I can't find the STP library file. I am making a new one ..."
+    sh clean_clone_build_stp.sh
+else 
+ echo -n "To rebuild stp press 'y' "
+ read re_bld
+ if [ "$re_bld" != "${re_bld#[Yy]}" ] ;then
+	sh clean_and_build_stp.sh
+ fi
+
+fi
+
+cd ./stpJ
+[ ! -f ./build ] && mkdir ./build || rm -rf ./build/* ||:
+
+cd ./build
+
+echo "Now building the JAVA API for STP ..."
+
+cmake .. #-DCMAKE_BUILD_TYPE=Debug
+cmake --build . 
+
+echo
+echo "BUILD SUCCESSFUL"
+echo
+
+ls
+
+# copy API - jar and - so into javasmt
+echo
+echo "copying library files into JavaSMT (old files are overwritten) ... ..."
+
+# cp ./stpJavaAPI.jar /home/lubuntu/SAHEED/gsoc/CODE/java-smt/lib/
+# cp ./libstpJapi.so /home/lubuntu/SAHEED/gsoc/CODE/java-smt/lib/native/x86_64-linux/
+
+cp ./stpJavaAPI.jar $JAR_LIB_DIR
+cp ./libstpJapi.so $SO_LIB_DIR
+
+echo "SUCCESS"

native-library-files/stp_project/clean_and_build_stp.sh

@@ -0,0 +1,39 @@
+#/usr/bin/env/ bash
+
+# This removes raw STP buld files and rebuild it
+# 
+set -e
+
+DESTN_DIR=$PWD/stpJ/install_include
+
+[ ! -f "$DESTN_DIR" ] && mkdir -p "$DESTN_DIR" || rm -rf "$DESTN_DIR"/* ||:
+
+[ -d "./stp/build" ] && rm -rf ./stp/build ||:
+[ -d "./build" ] && rm -rf ./build ||:
+
+echo "Raw STP Build files removed "
+
+echo "Now copying necessary files to expend STP"
+STP_HEADER=$PWD/stp/include/stp/
+yes | cp -f $PWD/stp_extend/c_interface.h $STP_HEADER
+STP_INTERFACE_SRC=$PWD/stp/lib/Interface/
+yes | cp -f $PWD/stp_extend/ext_c_interface.cpp $STP_INTERFACE_SRC
+yes | cp -f $PWD/stp_extend/CMakeLists.txt $STP_INTERFACE_SRC
+
+cd stp
+mkdir ./build;cd ./build
+echo
+echo "Now rebuilding building STP ... "
+
+
+cmake ..
+make
+
+echo "Installing STP into $DESTN_DIR"
+make DESTDIR=$DESTN_DIR install
+
+echo "... ... STP BUILD SUCCESSFULL"
+ls 
+echo
+
+# cd ../../

native-library-files/stp_project/clean_clone_build_stp.sh

@@ -0,0 +1,42 @@
+#/usr/bin/env/ bash
+
+# This removes any existing STP repositories and build files
+# and clones a new repo and build STP
+# 
+set -e
+
+DESTN_DIR=$PWD/stpJ/install_include
+
+[ ! -f "$DESTN_DIR" ] && mkdir -p "$DESTN_DIR" || rm -rf "$DESTN_DIR"/* ||:
+
+[ -d "./stp" ] && rm -rf ./stp ||:
+[ -d "./build" ] && rm -rf ./build ||:
+
+echo "Build files removed and STP repo deleted."
+echo "Now cloning stp ..."
+
+git clone https://github.com/stp/stp.git
+
+echo "Now copying necessary files to expend STP"
+STP_HEADER=$PWD/stp/include/stp/
+yes | cp -f $PWD/stp_extend/c_interface.h $STP_HEADER
+STP_INTERFACE_SRC=$PWD/stp/lib/Interface/
+yes | cp -f $PWD/stp_extend/ext_c_interface.cpp $STP_INTERFACE_SRC
+yes | cp -f $PWD/stp_extend/CMakeLists.txt $STP_INTERFACE_SRC
+
+cd stp
+mkdir ./build;cd ./build
+echo
+echo "Now building STP ... "
+
+cmake ..
+make
+
+echo "Installing STP into $DESTN_DIR"
+make DESTDIR=$DESTN_DIR install
+
+echo "... ... STP BUILD SUCCESSFULL"
+ls 
+echo
+
+# cd ../../

native-library-files/stp_project/clean_up.sh

@@ -0,0 +1,23 @@
+#/usr/bin/env/ bash
+
+# Clean up the build files for StpJavaApi
+# cryptominisat repo is also removed
+
+set -e
+
+# remove STP repo
+#[ -d "./stp" ] && rm -rf ./stp ||:
+
+
+# the built STP library should have been copied out 
+[ -d "./stpJ/build" ] && rm -rf ./stpJ/build ||:
+
+DESTN_DIR=$PWD/stpJ/install_include
+[ ! -f "$DESTN_DIR" ] && rm -rf "$DESTN_DIR"/* ||:
+
+#remove cryptominisat repo
+[ -d "./dependencies/cryptominisat" ] && rm -rf ./dependencies/cryptominisat ||:
+
+# java builds
+
+echo "Build files and cloned repos removed."

native-library-files/stp_project/dependencies/install_depends.sh

@@ -0,0 +1,15 @@
+#!/usr/etc/ bash
+
+set -e
+# prerequisite for building STP
+#  boost, flex, bison and minisat
+sudo apt-get install cmake bison flex libboost-all-dev python perl minisat
+
+# CryptoMiniSat 
+git clone https://github.com/msoos/cryptominisat
+cd cryptominisat
+mkdir build && cd build
+cmake ..
+make
+sudo make install
+sudo ldconfig

native-library-files/stp_project/install_prereq.sh

@@ -0,0 +1,7 @@
+#!/usr/etc/ bash
+
+# installs dependencies for building the STP library
+set -e
+
+cd ./dependencies
+sh install_depends.sh