before rebuilding the API binding (for many reasons)

Author: refactormyself

src/org/sosy_lab/java_smt/SolverContextFactory.java

@@ -54,6 +54,7 @@
 import org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5SolverContext;
 import org.sosy_lab.java_smt.solvers.princess.PrincessSolverContext;
 import org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolSolverContext;
+import org.sosy_lab.java_smt.solvers.stp.StpSolverContext;
 
 /**
  * Factory class for loading and generating solver contexts. Generates a {@link SolverContext}
@@ -68,7 +69,8 @@ public enum Solvers {
     MATHSAT5,
     SMTINTERPOL,
     Z3,
-    PRINCESS
+    PRINCESS,
+    STP
   }
 
   @Option(secure = true, description = "Export solver queries in SmtLib format into a file.")
@@ -214,6 +216,8 @@ private SolverContext generateContext0(Solvers solverToCreate)
       case PRINCESS:
         return PrincessSolverContext.create(
             config, shutdownNotifier, logfile, (int) randomSeed, nonLinearArithmetic);
+      case STP:
+        return StpSolverContext.create(config, logger, shutdownNotifier, logfile, randomSeed);
 
       default:
         throw new AssertionError("no solver selected");

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

@@ -0,0 +1,32 @@
+/*
+ *  JavaSMT is an API wrapper for a collection of SMT solvers.
+ *  This file is part of JavaSMT.
+ *
+ *  Copyright (C) 2007-2019  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package org.sosy_lab.java_smt.native_api.stp;
+//TODO REBUILD STP API Binding change package name = ~.solver.stp and class name = StpJavaApi
+
+public class Testing extends VC {
+
+  protected Testing(long pArg0, boolean pArg1) {
+    super(pArg0, pArg1);
+
+    Type t = new Type(pArg0, pArg1);
+  }
+
+}
+

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

@@ -0,0 +1,4 @@
+/**
+ * 
+ */
+package org.sosy_lab.java_smt.native_api.stp;

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

@@ -0,0 +1,104 @@
+/*
+ *  JavaSMT is an API wrapper for a collection of SMT solvers.
+ *  This file is part of JavaSMT.
+ *
+ *  Copyright (C) 2007-2019  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.stp;
+
+import java.util.Collection;
+import java.util.List;
+import java.util.Optional;
+import java.util.Set;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Model;
+import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.SolverException;
+import org.sosy_lab.java_smt.basicimpl.AbstractProver;
+
+class StpAbstractProver<T> extends AbstractProver<T> {
+
+  protected StpAbstractProver(Set<ProverOptions> pOptions) {
+    super(pOptions);
+    // TODO Auto-generated constructor stub
+  }
+
+  @Override
+  public void pop() {
+    // TODO Auto-generated method stub
+
+  }
+
+  @Override
+  public @Nullable T addConstraint(BooleanFormula pConstraint) throws InterruptedException {
+    // TODO Auto-generated method stub
+    return null;
+  }
+
+  @Override
+  public void push() {
+    // TODO Auto-generated method stub
+
+  }
+
+  @Override
+  public boolean isUnsat() throws SolverException, InterruptedException {
+    // TODO Auto-generated method stub
+    return false;
+  }
+
+  @Override
+  public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
+      throws SolverException, InterruptedException {
+    // TODO Auto-generated method stub
+    return false;
+  }
+
+  @Override
+  public Model getModel() throws SolverException {
+    // TODO Auto-generated method stub
+    return null;
+  }
+
+  @Override
+  public List<BooleanFormula> getUnsatCore() {
+    // TODO Auto-generated method stub
+    return null;
+  }
+
+  @Override
+  public Optional<List<BooleanFormula>>
+      unsatCoreOverAssumptions(Collection<BooleanFormula> pAssumptions)
+          throws SolverException, InterruptedException {
+    // TODO Auto-generated method stub
+    return null;
+  }
+
+  @Override
+  public void close() {
+    // TODO Auto-generated method stub
+
+  }
+
+  @Override
+  public <R> R allSat(AllSatCallback<R> pCallback, List<BooleanFormula> pImportant)
+      throws InterruptedException, SolverException {
+    // TODO Auto-generated method stub
+    return null;
+  }
+
+}

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

@@ -0,0 +1,60 @@
+/*
+ *  JavaSMT is an API wrapper for a collection of SMT solvers.
+ *  This file is part of JavaSMT.
+ *
+ *  Copyright (C) 2007-2019  Dirk Beyer
+ *  All rights reserved.
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package org.sosy_lab.java_smt.solvers.stp;
+
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaType;
+import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+
+class StpArrayFormulaManager
+    extends AbstractArrayFormulaManager<Long, Long, Long, Long> {
+
+  public StpArrayFormulaManager(FormulaCreator<Long, Long, Long, Long> pFormulaCreator) {
+    super(pFormulaCreator);
+    // TODO Auto-generated constructor stub
+  }
+
+  @Override
+  protected Long select(Long pArray, Long pIndex) {
+    // TODO Auto-generated method stub
+    return null;
+  }
+
+  @Override
+  protected Long store(Long pArray, Long pIndex, Long pValue) {
+    // TODO Auto-generated method stub
+    return null;
+  }
+
+  @Override
+  protected <TI extends Formula, TE extends Formula> Long
+      internalMakeArray(String pName, FormulaType<TI> pIndexType, FormulaType<TE> pElementType) {
+    // TODO Auto-generated method stub
+    return null;
+  }
+
+  @Override
+  protected Long equivalence(Long pArray1, Long pArray2) {
+    // TODO Auto-generated method stub
+    return null;
+  }
+
+}