Fixed bugs and rebuild the API

Author: refactormyself

.classpath

@@ -27,6 +27,6 @@
 		</attributes>
 	</classpathentry>
 	<classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER"/>
-	<classpathentry kind="lib" path="/home/lubuntu/SAHEED/gsoc/CODE/java-smt/lib/stpJavaAPI.jar"/>
+	<classpathentry kind="lib" path="lib/stpJavaAPI.jar"/>
 	<classpathentry kind="output" path="bin"/>
 </classpath>

lib/native/x86_64-linux/libstpJapi.so

@@ -19,7 +19,7 @@ PRJ_NAME=$(basename "$PRJ_DIR")
 
 # confirm expected directory structure 
 # MUST BE like java-smt/../../this_script.sh
-if [[ "$PRJ_NAME"!="java-smt" ]]
+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\
@@ -29,7 +29,7 @@ fi
 
 # set destination directory for final libraries
 JAR_LIB_DIR="${PRJ_DIR}/lib/"
-SO_LIB_DIR="${JAR_LIB_DIR}/native/x86_64-linux/
+SO_LIB_DIR="${JAR_LIB_DIR}/native/x86_64-linux/"
 
 
 # echo $FILE

native-library-files/stp_project/build_raw_to_java_api.sh

@@ -153,12 +153,12 @@ struct Type {};
 %nodefaultctor WholeCounterExample;
 struct WholeCounterExample {};
 
-
+/* 
 %inline%{
 
 // typedef void* VC;
 
-/* TODO: hanldle this in Java Code; Remove if confirmed. Envoronment configs
+// TODO: hanldle this in Java Code; Remove if confirmed. Envoronment configs
  struct Flags {
 	const char a;
 	const char c;
@@ -188,10 +188,11 @@ struct WholeCounterExample {};
 	.w = 'w',
 	.y = 'y'
 };
- */
 
 %}
+ */
 
+%inline%{
 
 /////////////////////////////////////////////////////////////////////////////
 /// API INITIALISATION AND CONFIG

native-library-files/stp_project/stpJ/StpJavaApi.i

@@ -84,25 +84,25 @@ public void testingSAT() {
     Expr x = StpJavaApi.vc_varExpr(stpContextVC, "x", StpJavaApi.vc_bvType(stpContextVC, width));
 
     // Create bitvector x + x
-    Expr xPlusx = StpJavaApi.vc_bvPlusExpr(stpContextVC, width, x, x);
+    Expr xPlusx = StpJavaApi.vc_bvPlusExpr(stpContextVC, width, x, x); // Non-Formla can't assert
 
     // Create bitvector constant 2
     Expr two = StpJavaApi.vc_bvConstExprFromInt(stpContextVC, width, 20);
 
     // Create bitvector 2*x
-    Expr xTimes2 = StpJavaApi.vc_bvMultExpr(stpContextVC, width, two, x);
+    Expr xTimes2 = StpJavaApi.vc_bvMultExpr(stpContextVC, width, two, x); // Non-Formla can't assert
 
     // Create bool expression x + x = 2*x
     Expr equality = StpJavaApi.vc_eqExpr(stpContextVC, xPlusx, xTimes2);
 
-    // StpJavaApi.vc_assertFormula(stpContextVC, StpJavaApi.vc_trueExpr(stpContextVC));
-    StpJavaApi.vc_assertFormula(stpContextVC, xTimes2);
+    StpJavaApi.vc_assertFormula(stpContextVC, StpJavaApi.vc_trueExpr(stpContextVC));
+    StpJavaApi.vc_assertFormula(stpContextVC, equality);
 
     // Print the assertions
     System.out.println("Assertions:\n");
     StpJavaApi.vc_printAsserts(stpContextVC, 0);
-    System.out.println("Query:\n");
-    StpJavaApi.vc_printQuery(stpContextVC);
+    // System.out.println("Query:\n");
+    // StpJavaApi.vc_printQuery(stpContextVC);
 
   }