Skip to content

Commit e23b5e9

Browse files
refactormyselfrefactormyself
committed
Update the new API and fixed reference errors
1 parent fdb4dfc commit e23b5e9

File tree

9 files changed

+1370
-71
lines changed

9 files changed

+1370
-71
lines changed

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

+1,317
Large diffs are not rendered by default.

‎src/org/sosy_lab/java_smt/native_api/stp/Testing.java

+3-1
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,14 @@
2020
package org.sosy_lab.java_smt.native_api.stp;
2121
//TODO REBUILD STP API Binding change package name = ~.solver.stp and class name = StpJavaApi
2222

23+
import org.sosy_lab.java_smt.solvers.stp.VC;
24+
2325
public class Testing extends VC {
2426

2527
protected Testing(long pArg0, boolean pArg1) {
2628
super(pArg0, pArg1);
2729

28-
Type t = new Type(pArg0, pArg1);
30+
// Type t = new Type(pArg0, pArg1);
2931
}
3032

3133
}

‎src/org/sosy_lab/java_smt/solvers/stp/StpExpr.java

-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@
1919
*/
2020
package org.sosy_lab.java_smt.solvers.stp;
2121

22-
import org.sosy_lab.java_smt.native_api.stp.Expr;
2322

2423
class StpExpr extends Expr {
2524

‎src/org/sosy_lab/java_smt/solvers/stp/StpFormulaCreator.java

+25-35
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,6 @@
2525
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
2626
import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
2727
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
28-
import org.sosy_lab.java_smt.native_api.stp.VC;
29-
import org.sosy_lab.java_smt.native_api.stp.stpJapi;
3028

3129
//extends FormulaCreator<TFormulaInfo, TType, TEnv, TFuncDecl> {
3230
public class StpFormulaCreator extends FormulaCreator<Long, Long, Long, Long> {
@@ -41,7 +39,7 @@ public class StpFormulaCreator extends FormulaCreator<Long, Long, Long, Long> {
4139
// }
4240
//
4341
// protected StpFormulaCreator(Long pEnv) {
44-
// super(pEnv, stpJapi.vc_boolType(vc), null, null);
42+
// super(pEnv, StpJavaApi.vc_boolType(vc), null, null);
4543
//
4644
// }
4745

@@ -52,14 +50,14 @@ public class StpFormulaCreator extends FormulaCreator<Long, Long, Long, Long> {
5250
private final VC vc;
5351

5452
protected StpFormulaCreator(VC vc) {
55-
super(StpVC.getVCptr(vc), StpType.getTypePtr(stpJapi.vc_boolType(vc)), null, null);
53+
super(StpVC.getVCptr(vc), Type.getCPtr(StpJavaApi.vc_boolType(vc)), null, null);
5654
this.vc = vc;
5755
}
5856

5957

6058
@Override
6159
public Long getBitvectorType(int pBitwidth) {
62-
return StpType.getTypePtr(stpJapi.vc_bvType(vc, pBitwidth));
60+
return Type.getCPtr(StpJavaApi.vc_bvType(vc, pBitwidth));
6361
}
6462

6563
@Override
@@ -69,50 +67,42 @@ public Long getFloatingPointType(FloatingPointType pType) {
6967

7068
@Override
7169
public Long getArrayType(Long pIndexType, Long pElementType) {
72-
return StpType.getTypePtr(
73-
stpJapi.vc_arrayType(vc, StpType.getType(pIndexType), StpType.getType(pElementType)));
70+
return Type.getCPtr(
71+
StpJavaApi.vc_arrayType(vc, new Type(pIndexType, true), new Type(pElementType, true)));
7472
}
7573

7674
@Override
7775
public Long makeVariable(Long pType, String pVarName) {
7876
String alphaNum_ = "^[a-zA-Z0-9_]*$";
7977
assert (pVarName
8078
.matches(alphaNum_)) : "A valid Variable Name can only contain Alphanumeric and underscore";
81-
return StpExpr.getExprPtr(stpJapi.vc_varExpr(vc, pVarName, StpType.getType(pType)));
79+
return Expr.getCPtr(StpJavaApi.vc_varExpr(vc, pVarName, new Type(pType, true)));
8280
}
8381

8482
@Override
8583
public FormulaType<?> getFormulaType(Long pFormula) {
86-
// TODO Auto-generated method stub
84+
System.out.println("I came here.");
85+
// long type = msat_term_get_type(pFormula);
86+
// return getFormulaTypeFromTermType(type);
8787
return null;
8888
}
89-
//
90-
//
91-
// private FormulaType<?> getFormulaTypeFromTermType(Long type) {
92-
// long env = getEnv();
93-
// if (msat_is_bool_type(env, type)) {
94-
// return FormulaType.BooleanType;
95-
// } else if (msat_is_integer_type(env, type)) {
96-
// return FormulaType.IntegerType;
97-
// } else if (msat_is_rational_type(env, type)) {
98-
// return FormulaType.RationalType;
99-
// } else if (msat_is_bv_type(env, type)) {
100-
// return FormulaType.getBitvectorTypeWithSize(msat_get_bv_type_size(env, type));
101-
// } else if (msat_is_fp_type(env, type)) {
102-
// return FormulaType.getFloatingPointType(
103-
// msat_get_fp_type_exp_width(env, type), msat_get_fp_type_mant_width(env, type));
104-
// } else if (msat_is_fp_roundingmode_type(env, type)) {
105-
// return FormulaType.FloatingPointRoundingModeType;
106-
// } else if (msat_is_array_type(env, type)) {
107-
// long indexType = msat_get_array_index_type(env, type);
108-
// long elementType = msat_get_array_element_type(env, type);
109-
// return FormulaType.getArrayType(
110-
// getFormulaTypeFromTermType(indexType), getFormulaTypeFromTermType(elementType));
111-
// }
112-
// throw new IllegalArgumentException("Unknown formula type " + msat_type_repr(type));
113-
// }
114-
//
11589

90+
/*
91+
* private FormulaType<?> getFormulaTypeFromTermType(Long type) { // long env = getEnv(); if
92+
* (msat_is_bool_type(env, type)) { return FormulaType.BooleanType; } else if
93+
* (msat_is_integer_type(env, type)) { return FormulaType.IntegerType; } else if
94+
* (msat_is_rational_type(env, type)) { return FormulaType.RationalType; } else if
95+
* (msat_is_bv_type(env, type)) { return
96+
* FormulaType.getBitvectorTypeWithSize(msat_get_bv_type_size(env, type)); } else if
97+
* (msat_is_fp_type(env, type)) { return FormulaType.getFloatingPointType(
98+
* msat_get_fp_type_exp_width(env, type), msat_get_fp_type_mant_width(env, type)); } else if
99+
* (msat_is_fp_roundingmode_type(env, type)) { return FormulaType.FloatingPointRoundingModeType; }
100+
* else if (msat_is_array_type(env, type)) { long indexType = msat_get_array_index_type(env,
101+
* type); long elementType = msat_get_array_element_type(env, type); return
102+
* FormulaType.getArrayType( getFormulaTypeFromTermType(indexType),
103+
* getFormulaTypeFromTermType(elementType)); } throw new
104+
* IllegalArgumentException("Unknown formula type " + msat_type_repr(type)); }
105+
*/
116106
@Override
117107
public <R> R visit(FormulaVisitor<R> pVisitor, Formula pFormula, Long pF) {
118108
// TODO Auto-generated method stub

‎src/org/sosy_lab/java_smt/solvers/stp/StpNativeApi.java

+4-4
Original file line numberDiff line numberDiff line change
@@ -21,13 +21,13 @@
2121

2222
//import org.sosy_lab.java_smt.solvers.stp.
2323
//import org.sosy_lab.java_smt.native_api.stp.Type;
24-
import org.sosy_lab.java_smt.native_api.stp.VC;
25-
import org.sosy_lab.java_smt.native_api.stp.stpJapi;
2624

2725
public class StpNativeApi {
2826

27+
private static StpJavaApi StpJavaApi;
28+
2929
static String getStpVersion() {
30-
return stpJapi.get_git_version_tag();
30+
return org.sosy_lab.java_smt.solvers.stp.StpJavaApi.get_git_version_tag();
3131
}
3232

3333

@@ -43,7 +43,7 @@ static long getStpBoolType(StpSolverContext context) throws Exception {
4343
// the address of the boolType for that context
4444
VC vc = null;
4545
// Type type = stpJapi.vc_boolType(vc);
46-
return StpType.getTypePtr(stpJapi.vc_boolType(vc));
46+
return StpType.getTypePtr(org.sosy_lab.java_smt.solvers.stp.StpJavaApi.vc_boolType(vc));
4747
}
4848

4949
}

‎src/org/sosy_lab/java_smt/solvers/stp/StpNativeApiTest.java

+18-22
Original file line numberDiff line numberDiff line change
@@ -23,10 +23,6 @@
2323
import org.junit.BeforeClass;
2424
import org.junit.Test;
2525
import org.sosy_lab.common.NativeLibraries;
26-
import org.sosy_lab.java_smt.native_api.stp.Expr;
27-
import org.sosy_lab.java_smt.native_api.stp.VC;
28-
import org.sosy_lab.java_smt.native_api.stp.ifaceflag_t;
29-
import org.sosy_lab.java_smt.native_api.stp.stpJapi;
3026

3127
public class StpNativeApiTest {
3228

@@ -41,24 +37,24 @@ public static void loadOpensmt2Library() {
4137

4238
@Test
4339
public void testStpGitVersion() throws Exception {
44-
String version_sha = stpJapi.get_git_version_sha();
40+
String version_sha = StpJavaApi.get_git_version_sha();
4541
System.out.println("\nSHA of this STP version is :");
4642
System.out.println(version_sha);
4743

48-
String version_tag = stpJapi.get_git_version_tag();
44+
String version_tag = StpJavaApi.get_git_version_tag();
4945
System.out.println("\nThis STP version is :");
5046
System.out.println(version_tag);
5147

5248
}
5349

5450
@Test
5551
public void testStpCompilationEnvironment() throws Exception {
56-
String compile_env = stpJapi.get_compilation_env();
52+
String compile_env = StpJavaApi.get_compilation_env();
5753
System.out.println("\nCompilation Environment of this STP version is :");
5854

5955
System.out.println(compile_env);
6056

61-
// stpJapi.
57+
// StpJavaApi.
6258
ifaceflag_t x = ifaceflag_t.EXPRDELETE;
6359

6460
}
@@ -68,27 +64,27 @@ public void testStpSampleFromRepo() throws Exception {
6864

6965
int width = 8;
7066

71-
VC handle = stpJapi.vc_createValidityChecker();
67+
VC handle = StpJavaApi.vc_createValidityChecker();
7268

7369
// Register a callback for errors
74-
// stpJapi.vc_registerErrorHandler(errorHandler);
70+
// StpJavaApi.vc_registerErrorHandler(errorHandler);
7571

7672
// Create variable "x"
77-
Expr x = stpJapi.vc_varExpr(handle, "x", stpJapi.vc_bvType(handle, width));
73+
Expr x = StpJavaApi.vc_varExpr(handle, "x", StpJavaApi.vc_bvType(handle, width));
7874

7975
// Create bitvector x + x
80-
Expr xPlusx = stpJapi.vc_bvPlusExpr(handle, width, x, x);
76+
Expr xPlusx = StpJavaApi.vc_bvPlusExpr(handle, width, x, x);
8177

8278
// Create bitvector constant 2
83-
Expr two = stpJapi.vc_bvConstExprFromInt(handle, width, 2);
79+
Expr two = StpJavaApi.vc_bvConstExprFromInt(handle, width, 2);
8480

8581
// Create bitvector 2*x
86-
Expr xTimes2 = stpJapi.vc_bvMultExpr(handle, width, two, x);
82+
Expr xTimes2 = StpJavaApi.vc_bvMultExpr(handle, width, two, x);
8783

8884
// Create bool expression x + x = 2*x
89-
Expr equality = stpJapi.vc_eqExpr(handle, xPlusx, xTimes2);
85+
Expr equality = StpJavaApi.vc_eqExpr(handle, xPlusx, xTimes2);
9086

91-
stpJapi.vc_assertFormula(handle, stpJapi.vc_trueExpr(handle));
87+
StpJavaApi.vc_assertFormula(handle, StpJavaApi.vc_trueExpr(handle));
9288

9389
// We are asking STP: ∀ x. true → ( x + x = 2*x )
9490
// This should be VALID.
@@ -99,11 +95,11 @@ public void testStpSampleFromRepo() throws Exception {
9995
// This should be INVALID.
10096
System.out.println("######Second Query\n");
10197
// Create bool expression x + x = 2
102-
Expr badEquality = stpJapi.vc_eqExpr(handle, xPlusx, two);
98+
Expr badEquality = StpJavaApi.vc_eqExpr(handle, xPlusx, two);
10399
handleQuery(handle, badEquality);
104100

105101
// Clean up
106-
stpJapi.vc_Destroy(handle);
102+
StpJavaApi.vc_Destroy(handle);
107103

108104
}
109105

@@ -118,18 +114,18 @@ void errorHandler(String err_msg) throws Exception {
118114
void handleQuery(VC handle, Expr queryExpr) {
119115
// Print the assertions
120116
System.out.println("Assertions:\n");
121-
stpJapi.vc_printAsserts(handle, 0);
117+
StpJavaApi.vc_printAsserts(handle, 0);
122118

123-
int result = stpJapi.vc_query(handle, queryExpr);
119+
int result = StpJavaApi.vc_query(handle, queryExpr);
124120
System.out.println("Query:\n");
125-
stpJapi.vc_printQuery(handle);
121+
StpJavaApi.vc_printQuery(handle);
126122
switch (result) {
127123
case 0:
128124
System.out.println("Query is INVALID\n");
129125

130126
// print counter example
131127
System.out.println("Counter example:\n");
132-
stpJapi.vc_printCounterExample(handle);
128+
StpJavaApi.vc_printCounterExample(handle);
133129
break;
134130

135131
case 1:

‎src/org/sosy_lab/java_smt/solvers/stp/StpSolverContext.java

+2-4
Original file line numberDiff line numberDiff line change
@@ -33,8 +33,6 @@
3333
import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
3434
import org.sosy_lab.java_smt.api.ProverEnvironment;
3535
import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
36-
import org.sosy_lab.java_smt.native_api.stp.VC;
37-
import org.sosy_lab.java_smt.native_api.stp.stpJapi;
3836

3937
public final class StpSolverContext extends AbstractSolverContext {
4038

@@ -75,7 +73,7 @@ public static StpSolverContext create(
7573
StpEnvironment environ = // TODO: I got this wrong
7674
new StpEnvironment(config, logger, shutdownNotifier, stpLogfile, randomSeed);
7775

78-
vcStpContext = stpJapi.vc_createValidityChecker(); // this is the 'env'
76+
vcStpContext = StpJavaApi.vc_createValidityChecker(); // this is the 'env'
7977

8078
// use the 'environment' to create a FormulaCreator object
8179
// StpFormulaCreator formulaCreator = new StpFormulaCreator(environ);//vcStpContext
@@ -109,7 +107,7 @@ public void close() {
109107
logger.log(Level.FINER, "Freeing STP environment resources");
110108
// stpJapi.vc_Destroy(formulaCreator.getEnv()); //TODO: use this and make vcStpContext
111109
// non-static
112-
stpJapi.vc_Destroy(vcStpContext);
110+
StpJavaApi.vc_Destroy(vcStpContext);
113111
}
114112

115113
@Override

‎src/org/sosy_lab/java_smt/solvers/stp/StpType.java

+1-2
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,8 @@
1919
*/
2020
package org.sosy_lab.java_smt.solvers.stp;
2121

22-
import org.sosy_lab.java_smt.native_api.stp.Type;
2322

24-
class StpType extends org.sosy_lab.java_smt.native_api.stp.Type {
23+
class StpType extends Type {
2524

2625
protected StpType(long cPtr, boolean cMemoryOwn) {
2726
super(cPtr, cMemoryOwn);

‎src/org/sosy_lab/java_smt/solvers/stp/StpVC.java

-2
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,6 @@
1919
*/
2020
package org.sosy_lab.java_smt.solvers.stp;
2121

22-
import org.sosy_lab.java_smt.native_api.stp.VC;
23-
2422
/**
2523
* Validity Checker (VC) is Context in STP
2624
*/

0 commit comments

Comments
 (0)