Apron Prototyp und kleines Beispiel

src/org/sosy_lab/java_smt/solvers/apron/ApronBooleanFormulaManager.java

@@ -0,0 +1,80 @@
+/*
+ *  JavaSMT is an API wrapper for a collection of SMT solvers.
+ *  This file is part of JavaSMT.
+ *
+ *  Copyright (C) 2007-2016  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.apron;
+
+import org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+
+public class ApronBooleanFormulaManager extends AbstractBooleanFormulaManager {
+  protected ApronBooleanFormulaManager(FormulaCreator pCreator) {
+    super(pCreator);
+  }
+
+  @Override
+  protected Object makeVariableImpl(String pVar) {
+    return null;
+  }
+
+  @Override
+  protected Object makeBooleanImpl(boolean value) {
+    return null;
+  }
+
+  @Override
+  protected Object not(Object pParam1) {
+    return null;
+  }
+
+  @Override
+  protected Object and(Object pParam1, Object pParam2) {
+    return null;
+  }
+
+  @Override
+  protected Object or(Object pParam1, Object pParam2) {
+    return null;
+  }
+
+  @Override
+  protected Object xor(Object pParam1, Object pParam2) {
+    return null;
+  }
+
+  @Override
+  protected Object equivalence(Object bits1, Object bits2) {
+    return null;
+  }
+
+  @Override
+  protected boolean isTrue(Object bits) {
+    return false;
+  }
+
+  @Override
+  protected boolean isFalse(Object bits) {
+    return false;
+  }
+
+  @Override
+  protected Object ifThenElse(Object cond, Object f1, Object f2) {
+    return null;
+  }
+}

src/org/sosy_lab/java_smt/solvers/apron/ApronExamples.java

@@ -0,0 +1,75 @@
+/*
+ *  JavaSMT is an API wrapper for a collection of SMT solvers.
+ *  This file is part of JavaSMT.
+ *
+ *  Copyright (C) 2007-2016  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.apron;
+
+import java.util.Arrays;
+import apron.*;
+import org.junit.AssumptionViolatedException;
+import org.sosy_lab.common.NativeLibraries;
+
+/**
+ * Simple examples about the Apron Library. Inspired by
+ * <a href="https://github.com/antoinemine/apron/blob/master/examples/example1.c">...</a>
+ */
+public class ApronExamples
+{
+  private static void testBox(Manager pManager) throws ApronException {
+    String[] intVars = {"x"};
+    String[] realVars = {};
+
+    Environment environment = new Environment(intVars, realVars);
+    //x <= 2 and x >= -3
+
+    //x <= 2 --> -x+2 >= 0
+    Lincons1 cons1 = new Lincons1(environment);
+    cons1.setCoeff("x",new MpqScalar(-1));
+    cons1.setCst(new MpqScalar(+2));
+    cons1.setKind(Lincons1.SUPEQ);
+    //x >= 3 --> x-3 >= 0
+    Lincons1 cons2 = new Lincons1(environment);
+    cons2.setCoeff("x",new MpqScalar(1));
+    cons2.setCst(new MpqScalar(-3));
+    cons2.setKind(Lincons1.SUPEQ);
+
+    Lincons1[] constraints = {cons1, cons2};
+    Abstract1 abstract1 = new Abstract1(pManager, constraints);
+    //is x = 1 satisfiable?
+    Lincons1 cons3 = new Lincons1(environment);
+    cons3.setCoeff("x",new MpqScalar(1));
+    cons3.setCst(new MpqScalar(-1));
+    cons3.setKind(Lincons1.EQ);
+    System.out.println("Constraint is satisfiable: "+abstract1.satisfy(pManager, cons3));
+
+    //always unsat example, 1 = 0
+    Lincons1 cons4 = new Lincons1(environment);
+    cons4.setCoeff("x", new MpqScalar(0));
+    cons4.setCst(new MpqScalar(1));
+    cons4.setKind(Lincons1.EQ);
+    Abstract1 abstract2 = new Abstract1(pManager, new Lincons1[]{cons4});
+    System.out.println("Abstract-Obj. is Bottom: "+abstract2.isBottom(pManager));
+  }
+
+  public static void main(String[] args) throws ApronException {
+    Manager manager = new Box();
+    testBox(manager);
+  }
+}
+

src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaCreator.java

@@ -0,0 +1,86 @@
+/*
+ *  JavaSMT is an API wrapper for a collection of SMT solvers.
+ *  This file is part of JavaSMT.
+ *
+ *  Copyright (C) 2007-2016  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.apron;
+
+import java.util.List;
+import javax.annotation.Nullable;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaType;
+import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+
+public class ApronFormulaCreator extends FormulaCreator {
+  protected ApronFormulaCreator(
+      Object pO,
+      Object boolType,
+      @Nullable Object pIntegerType,
+      @Nullable Object pRationalType,
+      @Nullable Object stringType,
+      @Nullable Object regexType) {
+    super(pO, boolType, pIntegerType, pRationalType, stringType, regexType);
+  }
+
+  @Override
+  public Object getBitvectorType(int bitwidth) {
+    return null;
+  }
+
+  @Override
+  public Object getFloatingPointType(FloatingPointType type) {
+    return null;
+  }
+
+  @Override
+  public Object getArrayType(Object indexType, Object elementType) {
+    return null;
+  }
+
+  @Override
+  public Object makeVariable(Object pO, String varName) {
+    return null;
+  }
+
+  @Override
+  public FormulaType<?> getFormulaType(Object formula) {
+    return null;
+  }
+
+  @Override
+  public Object callFunctionImpl(Object declaration, List args) {
+    return null;
+  }
+
+  @Override
+  public Object declareUFImpl(String pName, Object pReturnType, List pArgTypes) {
+    return null;
+  }
+
+  @Override
+  protected Object getBooleanVarDeclarationImpl(Object pO) {
+    return null;
+  }
+
+  @Override
+  public Object visit(FormulaVisitor visitor, Formula formula, Object f) {
+    return null;
+  }
+}

src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaManager.java

@@ -0,0 +1,92 @@
+/*
+ *  JavaSMT is an API wrapper for a collection of SMT solvers.
+ *  This file is part of JavaSMT.
+ *
+ *  Copyright (C) 2007-2016  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.apron;
+
+import java.util.Map;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.Appender;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.IntegerFormulaManager;
+import org.sosy_lab.java_smt.api.RationalFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractUFManager;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+
+public class ApronFormulaManager extends AbstractFormulaManager <Long, Long, Long, Long>{
+  /**
+   * Builds a solver from the given theory implementations.
+   *
+   * @param pFormulaCreator
+   * @param functionManager
+   * @param booleanManager
+   * @param pIntegerManager
+   * @param pRationalManager
+   * @param bitvectorManager
+   * @param floatingPointManager
+   * @param quantifiedManager
+   * @param arrayManager
+   * @param slManager
+   * @param strManager
+   * @param enumManager
+   */
+  protected ApronFormulaManager(
+      FormulaCreator pFormulaCreator,
+      AbstractUFManager functionManager,
+      AbstractBooleanFormulaManager booleanManager,
+      @Nullable IntegerFormulaManager pIntegerManager,
+      @Nullable RationalFormulaManager pRationalManager,
+      @Nullable AbstractBitvectorFormulaManager bitvectorManager,
+      @Nullable AbstractFloatingPointFormulaManager floatingPointManager,
+      @Nullable AbstractQuantifiedFormulaManager quantifiedManager,
+      @Nullable AbstractArrayFormulaManager arrayManager,
+      @Nullable AbstractSLFormulaManager slManager,
+      @Nullable AbstractStringFormulaManager strManager,
+      @Nullable AbstractEnumerationFormulaManager enumManager) {
+    super(pFormulaCreator, functionManager, booleanManager, pIntegerManager, pRationalManager,
+        bitvectorManager, floatingPointManager, quantifiedManager, arrayManager, slManager,
+        strManager, enumManager);
+  }
+
+  @Override
+  public BooleanFormula parse(String s) throws IllegalArgumentException {
+    return null;
+  }
+
+  @Override
+  public <T extends Formula > T substitute(T f,
+                                         Map<? extends Formula, ? extends Formula> fromToMapping) {
+    return null;
+  }
+
+  @Override
+  public Appender dumpFormula(Long t) {
+    return null;
+  }
+}