Skip to content

Commit c489a72

Browse files
DId few minor clean ups
unnecessary classes removed calling functions adjusted But now StpSolverTest gives a Segfault
1 parent 9dd07dc commit c489a72

10 files changed

+11
-168
lines changed

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

-34
This file was deleted.

src/org/sosy_lab/java_smt/native_api/stp/package-info.java

-4
This file was deleted.

src/org/sosy_lab/java_smt/solvers/stp/StpEnvironment.java

+3
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,9 @@
2626
import org.sosy_lab.common.log.LogManager;
2727

2828
/**
29+
* TODO use the class to settings or config OR BETTER DELETE IT
30+
*
31+
*
2932
* This class is the actual Wrapper around an STP "context" known over there as Validity Checker All
3033
* "context" related operations are handled here Flags, SAT solver settings, STP "environment"
3134
* variables are handled here

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

-37
This file was deleted.

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ public class StpFormulaCreator extends FormulaCreator<Long, Long, Long, Long> {
5050
private final VC vc;
5151

5252
protected StpFormulaCreator(VC vc) {
53-
super(StpVC.getVCptr(vc), Type.getCPtr(StpJavaApi.vc_boolType(vc)), null, null);
53+
super(VC.getCPtr(vc), Type.getCPtr(StpJavaApi.vc_boolType(vc)), null, null);
5454
this.vc = vc;
5555
}
5656

@@ -84,7 +84,7 @@ public Long makeVariable(Long pType, String pVarName) {
8484

8585
@Override
8686
public FormulaType<?> getFormulaType(Long pFormula) {
87-
// System.out.println("I came here.");
87+
8888
// long type = msat_term_get_type(pFormula);
8989
// return getFormulaTypeFromTermType(type);
9090
// return null;

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

+2-14
Original file line numberDiff line numberDiff line change
@@ -24,26 +24,14 @@
2424

2525
public class StpNativeApi {
2626

27-
private static StpJavaApi StpJavaApi;
28-
2927
static String getStpVersion() {
3028
return org.sosy_lab.java_smt.solvers.stp.StpJavaApi.get_git_version_tag();
3129
}
3230

3331

3432
static long getStpBoolType(StpSolverContext context) throws Exception {
35-
// ToDo: IMPLEMENT
36-
37-
// So everything needs to start with the SolverContext
38-
39-
// Create a SolverContext that will manage the life span of the VC object
40-
// ...
41-
// ...
42-
// In this method I want to get a VC object (i.e. a SolverContext) and return
43-
// the address of the boolType for that context
44-
VC vc = null;
45-
// Type type = stpJapi.vc_boolType(vc);
46-
return StpType.getTypePtr(org.sosy_lab.java_smt.solvers.stp.StpJavaApi.vc_boolType(vc));
33+
VC vc = context.getFormulaCreator().getVC();
34+
return Type.getCPtr(org.sosy_lab.java_smt.solvers.stp.StpJavaApi.vc_boolType(vc));
4735
}
4836

4937
}

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

+4-3
Original file line numberDiff line numberDiff line change
@@ -70,9 +70,6 @@ public static StpSolverContext create(
7070
}
7171

7272
//Create or setup the 'environment' with supplied parameters and other java-smt defaults
73-
StpEnvironment environ = // TODO: I got this wrong
74-
new StpEnvironment(config, logger, shutdownNotifier, stpLogfile, randomSeed);
75-
7673
vcStpContext = StpJavaApi.vc_createValidityChecker(); // this is the 'env'
7774

7875
// use the 'environment' to create a FormulaCreator object
@@ -98,6 +95,10 @@ public static StpSolverContext create(
9895
return new StpSolverContext(formulaMgr, formulaCreator, logger);
9996
}
10097

98+
public StpFormulaCreator getFormulaCreator() {
99+
return this.formulaCreator;
100+
}
101+
101102
@Override
102103
public String getVersion() {
103104
return StpNativeApi.getStpVersion();

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

-36
This file was deleted.

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

-38
This file was deleted.
File renamed without changes.

0 commit comments

Comments
 (0)