diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index 4857c85527..9d56bfe86d 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -1,15 +1,4 @@
<?xml version="1.0" encoding="UTF-8"?>
-
-<!--
-This file is part of JavaSMT,
-an API wrapper for a collection of SMT solvers:
-https://github.com/sosy-lab/java-smt
-
-SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
<module type="JAVA_MODULE" version="4">
<component name="NewModuleRootManager">
<output url="file://$MODULE_DIR$/bin" />
@@ -313,210 +302,15 @@ SPDX-License-Identifier: Apache-2.0
<SOURCES />
</library>
</orderEntry>
+ <orderEntry type="module-library">
+ <library>
+ <CLASSES />
+ <JAVADOC />
+ <SOURCES>
+ <root url="jar://$USER_HOME$/Bachelorarbeit/apron/japron/apron.jar!/" />
+ </SOURCES>
+ </library>
+ </orderEntry>
+ <orderEntry type="library" name="apron" level="application" />
</component>
- <component name="org.twodividedbyzero.idea.findbugs">
- <option name="_basePreferences">
- <map>
- <entry key="property.analysisEffortLevel" value="default" />
- <entry key="property.analyzeAfterAutoMake" value="false" />
- <entry key="property.analyzeAfterCompile" value="false" />
- <entry key="property.annotationGutterIconEnabled" value="true" />
- <entry key="property.annotationSuppressWarningsClass" value="edu.umd.cs.findbugs.annotations.SuppressFBWarnings" />
- <entry key="property.annotationTextRangeMarkupEnabled" value="true" />
- <entry key="property.exportAsHtml" value="true" />
- <entry key="property.exportAsXml" value="true" />
- <entry key="property.exportBaseDir" value="" />
- <entry key="property.exportCreateArchiveDir" value="false" />
- <entry key="property.exportOpenBrowser" value="true" />
- <entry key="property.minPriorityToReport" value="Medium" />
- <entry key="property.runAnalysisInBackground" value="false" />
- <entry key="property.showHiddenDetectors" value="false" />
- <entry key="property.toolWindowToFront" value="true" />
- </map>
- </option>
- <option name="_detectors">
- <map>
- <entry key="AppendingToAnObjectOutputStream" value="true" />
- <entry key="AtomicityProblem" value="true" />
- <entry key="BadAppletConstructor" value="false" />
- <entry key="BadResultSetAccess" value="true" />
- <entry key="BadSyntaxForRegularExpression" value="true" />
- <entry key="BadUseOfReturnValue" value="true" />
- <entry key="BadlyOverriddenAdapter" value="true" />
- <entry key="BooleanReturnNull" value="true" />
- <entry key="BuildInterproceduralCallGraph" value="false" />
- <entry key="BuildObligationPolicyDatabase" value="true" />
- <entry key="BuildStringPassthruGraph" value="true" />
- <entry key="CallToUnsupportedMethod" value="false" />
- <entry key="CalledMethods" value="true" />
- <entry key="CheckCalls" value="false" />
- <entry key="CheckExpectedWarnings" value="false" />
- <entry key="CheckImmutableAnnotation" value="true" />
- <entry key="CheckRelaxingNullnessAnnotation" value="true" />
- <entry key="CheckTypeQualifiers" value="true" />
- <entry key="CloneIdiom" value="true" />
- <entry key="ComparatorIdiom" value="true" />
- <entry key="ConfusedInheritance" value="true" />
- <entry key="ConfusionBetweenInheritedAndOuterMethod" value="true" />
- <entry key="CovariantArrayAssignment" value="false" />
- <entry key="CrossSiteScripting" value="true" />
- <entry key="DefaultEncodingDetector" value="true" />
- <entry key="DoInsideDoPrivileged" value="true" />
- <entry key="DontCatchIllegalMonitorStateException" value="true" />
- <entry key="DontIgnoreResultOfPutIfAbsent" value="true" />
- <entry key="DontUseEnum" value="true" />
- <entry key="DroppedException" value="true" />
- <entry key="DumbMethodInvocations" value="true" />
- <entry key="DumbMethods" value="true" />
- <entry key="DuplicateBranches" value="true" />
- <entry key="EmptyZipFileEntry" value="false" />
- <entry key="EqualsOperandShouldHaveClassCompatibleWithThis" value="true" />
- <entry key="ExplicitSerialization" value="true" />
- <entry key="FieldItemSummary" value="true" />
- <entry key="FinalizerNullsFields" value="true" />
- <entry key="FindBadCast2" value="true" />
- <entry key="FindBadForLoop" value="true" />
- <entry key="FindBugsSummaryStats" value="true" />
- <entry key="FindCircularDependencies" value="false" />
- <entry key="FindComparatorProblems" value="true" />
- <entry key="FindDeadLocalStores" value="true" />
- <entry key="FindDoubleCheck" value="true" />
- <entry key="FindEmptySynchronizedBlock" value="true" />
- <entry key="FindFieldSelfAssignment" value="true" />
- <entry key="FindFinalizeInvocations" value="true" />
- <entry key="FindFloatEquality" value="true" />
- <entry key="FindFloatMath" value="false" />
- <entry key="FindHEmismatch" value="true" />
- <entry key="FindInconsistentSync2" value="true" />
- <entry key="FindJSR166LockMonitorenter" value="true" />
- <entry key="FindLocalSelfAssignment2" value="true" />
- <entry key="FindMaskedFields" value="true" />
- <entry key="FindMismatchedWaitOrNotify" value="true" />
- <entry key="FindNakedNotify" value="true" />
- <entry key="FindNoSideEffectMethods" value="true" />
- <entry key="FindNonSerializableStoreIntoSession" value="false" />
- <entry key="FindNonSerializableValuePassedToWriteObject" value="false" />
- <entry key="FindNonShortCircuit" value="true" />
- <entry key="FindNullDeref" value="true" />
- <entry key="FindNullDerefsInvolvingNonShortCircuitEvaluation" value="true" />
- <entry key="FindOpenStream" value="true" />
- <entry key="FindPuzzlers" value="true" />
- <entry key="FindRefComparison" value="true" />
- <entry key="FindReturnRef" value="true" />
- <entry key="FindRoughConstants" value="true" />
- <entry key="FindRunInvocations" value="true" />
- <entry key="FindSelfComparison" value="true" />
- <entry key="FindSelfComparison2" value="true" />
- <entry key="FindSleepWithLockHeld" value="true" />
- <entry key="FindSpinLoop" value="true" />
- <entry key="FindSqlInjection" value="true" />
- <entry key="FindTwoLockWait" value="true" />
- <entry key="FindUncalledPrivateMethods" value="true" />
- <entry key="FindUnconditionalWait" value="true" />
- <entry key="FindUninitializedGet" value="true" />
- <entry key="FindUnrelatedTypesInGenericContainer" value="true" />
- <entry key="FindUnreleasedLock" value="true" />
- <entry key="FindUnsatisfiedObligation" value="true" />
- <entry key="FindUnsyncGet" value="true" />
- <entry key="FindUseOfNonSerializableValue" value="true" />
- <entry key="FindUselessControlFlow" value="true" />
- <entry key="FindUselessObjects" value="true" />
- <entry key="FormatStringChecker" value="true" />
- <entry key="FunctionsThatMightBeMistakenForProcedures" value="true" />
- <entry key="HugeSharedStringConstants" value="true" />
- <entry key="IDivResultCastToDouble" value="true" />
- <entry key="IncompatMask" value="true" />
- <entry key="InconsistentAnnotations" value="true" />
- <entry key="InefficientIndexOf" value="false" />
- <entry key="InefficientInitializationInsideLoop" value="false" />
- <entry key="InefficientMemberAccess" value="false" />
- <entry key="InefficientToArray" value="false" />
- <entry key="InfiniteLoop" value="true" />
- <entry key="InfiniteRecursiveLoop" value="true" />
- <entry key="InheritanceUnsafeGetResource" value="true" />
- <entry key="InitializationChain" value="true" />
- <entry key="InitializeNonnullFieldsInConstructor" value="true" />
- <entry key="InstantiateStaticClass" value="true" />
- <entry key="IntCast2LongAsInstant" value="true" />
- <entry key="InvalidJUnitTest" value="true" />
- <entry key="IteratorIdioms" value="true" />
- <entry key="LazyInit" value="true" />
- <entry key="LoadOfKnownNullValue" value="true" />
- <entry key="LostLoggerDueToWeakReference" value="true" />
- <entry key="MethodReturnCheck" value="true" />
- <entry key="Methods" value="true" />
- <entry key="MultithreadedInstanceAccess" value="true" />
- <entry key="MutableEnum" value="true" />
- <entry key="MutableLock" value="true" />
- <entry key="MutableStaticFields" value="true" />
- <entry key="Naming" value="true" />
- <entry key="Noise" value="false" />
- <entry key="NoiseNullDeref" value="false" />
- <entry key="NoteAnnotationRetention" value="true" />
- <entry key="NoteCheckReturnValueAnnotations" value="true" />
- <entry key="NoteDirectlyRelevantTypeQualifiers" value="true" />
- <entry key="NoteJCIPAnnotation" value="true" />
- <entry key="NoteNonNullAnnotations" value="false" />
- <entry key="NoteNonnullReturnValues" value="false" />
- <entry key="NoteSuppressedWarnings" value="true" />
- <entry key="NoteUnconditionalParamDerefs" value="true" />
- <entry key="NumberConstructor" value="true" />
- <entry key="OptionalReturnNull" value="true" />
- <entry key="OverridingEqualsNotSymmetrical" value="true" />
- <entry key="PreferZeroLengthArrays" value="true" />
- <entry key="PublicSemaphores" value="false" />
- <entry key="QuestionableBooleanAssignment" value="true" />
- <entry key="ReadOfInstanceFieldInMethodInvokedByConstructorInSuperclass" value="true" />
- <entry key="ReadReturnShouldBeChecked" value="true" />
- <entry key="RedundantConditions" value="true" />
- <entry key="RedundantInterfaces" value="true" />
- <entry key="ReflectiveClasses" value="true" />
- <entry key="RepeatedConditionals" value="true" />
- <entry key="ResolveAllReferences" value="false" />
- <entry key="RuntimeExceptionCapture" value="true" />
- <entry key="SerializableIdiom" value="true" />
- <entry key="StartInConstructor" value="true" />
- <entry key="StaticCalendarDetector" value="true" />
- <entry key="StringConcatenation" value="true" />
- <entry key="SuperfluousInstanceOf" value="true" />
- <entry key="SuspiciousThreadInterrupted" value="true" />
- <entry key="SwitchFallthrough" value="true" />
- <entry key="SynchronizationOnSharedBuiltinConstant" value="true" />
- <entry key="SynchronizeAndNullCheckField" value="true" />
- <entry key="SynchronizeOnClassLiteralNotGetClass" value="true" />
- <entry key="SynchronizingOnContentsOfFieldToProtectField" value="true" />
- <entry key="TestASM" value="false" />
- <entry key="TestDataflowAnalysis" value="false" />
- <entry key="TestingGround" value="false" />
- <entry key="TestingGround2" value="false" />
- <entry key="TrainFieldStoreTypes" value="true" />
- <entry key="TrainLongInstantfParams" value="true" />
- <entry key="TrainNonNullAnnotations" value="true" />
- <entry key="TrainUnconditionalDerefParams" value="true" />
- <entry key="URLProblems" value="true" />
- <entry key="UncallableMethodOfAnonymousClass" value="true" />
- <entry key="UnnecessaryMath" value="true" />
- <entry key="UnreadFields" value="true" />
- <entry key="UselessSubclassMethod" value="false" />
- <entry key="VarArgsProblems" value="true" />
- <entry key="VolatileUsage" value="true" />
- <entry key="WaitInLoop" value="true" />
- <entry key="WrongMapIterator" value="true" />
- <entry key="XMLFactoryBypass" value="true" />
- </map>
- </option>
- <option name="_reportCategories">
- <map>
- <entry key="BAD_PRACTICE" value="true" />
- <entry key="CORRECTNESS" value="true" />
- <entry key="EXPERIMENTAL" value="true" />
- <entry key="I18N" value="true" />
- <entry key="MALICIOUS_CODE" value="true" />
- <entry key="MT_CORRECTNESS" value="true" />
- <entry key="PERFORMANCE" value="true" />
- <entry key="SECURITY" value="true" />
- <entry key="STYLE" value="true" />
- </map>
- </option>
- </component>
-</module>
+</module>
\ No newline at end of file
diff --git a/.idea/ant.xml b/.idea/ant.xml
index 3e3b7e7277..52ce37416f 100644
--- a/.idea/ant.xml
+++ b/.idea/ant.xml
@@ -1,19 +1,8 @@
<?xml version="1.0" encoding="UTF-8"?>
-
-<!--
-This file is part of JavaSMT,
-an API wrapper for a collection of SMT solvers:
-https://github.com/sosy-lab/java-smt
-
-SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
<project version="4">
<component name="AntConfiguration">
<buildFile url="file://$PROJECT_DIR$/build.xml">
<executeOn event="beforeCompilation" target="build-dependencies" />
</buildFile>
</component>
-</project>
+</project>
\ No newline at end of file
diff --git a/.idea/codeStyles/Project.xml b/.idea/codeStyles/Project.xml
new file mode 100644
index 0000000000..2e6e4da19a
--- /dev/null
+++ b/.idea/codeStyles/Project.xml
@@ -0,0 +1,185 @@
+<component name="ProjectCodeStyleConfiguration">
+ <code_scheme name="Project" version="173">
+ <option name="OTHER_INDENT_OPTIONS">
+ <value>
+ <option name="INDENT_SIZE" value="2" />
+ <option name="CONTINUATION_INDENT_SIZE" value="4" />
+ <option name="TAB_SIZE" value="8" />
+ </value>
+ </option>
+ <option name="LINE_SEPARATOR" value=" " />
+ <option name="PARAMETER_NAME_PREFIX" value="" />
+ <option name="INSERT_INNER_CLASS_IMPORTS" value="false" />
+ <option name="CLASS_COUNT_TO_USE_IMPORT_ON_DEMAND" value="5" />
+ <option name="NAMES_COUNT_TO_USE_IMPORT_ON_DEMAND" value="3" />
+ <option name="PACKAGES_TO_USE_IMPORT_ON_DEMAND">
+ <value>
+ <package name="java.awt" withSubpackages="false" static="false" />
+ <package name="javax.swing" withSubpackages="false" static="false" />
+ </value>
+ </option>
+ <option name="IMPORT_LAYOUT_TABLE">
+ <value>
+ <package name="" withSubpackages="true" static="false" />
+ <emptyLine />
+ <package name="javax" withSubpackages="true" static="false" />
+ <package name="java" withSubpackages="true" static="false" />
+ <emptyLine />
+ <package name="" withSubpackages="true" static="true" />
+ </value>
+ </option>
+ <option name="RIGHT_MARGIN" value="100" />
+ <option name="WRAP_WHEN_TYPING_REACHES_RIGHT_MARGIN" value="true" />
+ <option name="KEEP_BLANK_LINES_IN_CODE" value="2" />
+ <option name="KEEP_CONTROL_STATEMENT_IN_ONE_LINE" value="false" />
+ <option name="BLANK_LINES_AFTER_CLASS_HEADER" value="1" />
+ <option name="ALIGN_MULTILINE_PARAMETERS_IN_CALLS" value="true" />
+ <option name="ALIGN_MULTILINE_BINARY_OPERATION" value="true" />
+ <option name="ALIGN_MULTILINE_ASSIGNMENT" value="true" />
+ <option name="ALIGN_MULTILINE_TERNARY_OPERATION" value="true" />
+ <option name="ALIGN_MULTILINE_THROWS_LIST" value="true" />
+ <option name="ALIGN_MULTILINE_EXTENDS_LIST" value="true" />
+ <option name="ALIGN_MULTILINE_PARENTHESIZED_EXPRESSION" value="true" />
+ <option name="ALIGN_MULTILINE_ARRAY_INITIALIZER_EXPRESSION" value="true" />
+ <option name="CALL_PARAMETERS_WRAP" value="1" />
+ <option name="METHOD_PARAMETERS_WRAP" value="1" />
+ <option name="EXTENDS_LIST_WRAP" value="1" />
+ <option name="THROWS_LIST_WRAP" value="1" />
+ <option name="EXTENDS_KEYWORD_WRAP" value="1" />
+ <option name="THROWS_KEYWORD_WRAP" value="1" />
+ <option name="METHOD_CALL_CHAIN_WRAP" value="1" />
+ <option name="BINARY_OPERATION_WRAP" value="1" />
+ <option name="BINARY_OPERATION_SIGN_ON_NEXT_LINE" value="true" />
+ <option name="TERNARY_OPERATION_WRAP" value="1" />
+ <option name="TERNARY_OPERATION_SIGNS_ON_NEXT_LINE" value="true" />
+ <option name="FOR_STATEMENT_WRAP" value="1" />
+ <option name="ARRAY_INITIALIZER_WRAP" value="1" />
+ <option name="ASSIGNMENT_WRAP" value="5" />
+ <option name="WRAP_COMMENTS" value="true" />
+ <option name="IF_BRACE_FORCE" value="3" />
+ <option name="DOWHILE_BRACE_FORCE" value="3" />
+ <option name="WHILE_BRACE_FORCE" value="3" />
+ <option name="FOR_BRACE_FORCE" value="3" />
+ <JavaCodeStyleSettings>
+ <option name="PARAMETER_NAME_PREFIX" value="p" />
+ <option name="INSERT_INNER_CLASS_IMPORTS" value="true" />
+ <option name="CLASS_COUNT_TO_USE_IMPORT_ON_DEMAND" value="99" />
+ <option name="NAMES_COUNT_TO_USE_IMPORT_ON_DEMAND" value="99" />
+ <option name="PACKAGES_TO_USE_IMPORT_ON_DEMAND">
+ <value />
+ </option>
+ <option name="IMPORT_LAYOUT_TABLE">
+ <value>
+ <package name="" withSubpackages="true" static="true" />
+ <emptyLine />
+ <package name="" withSubpackages="true" static="false" />
+ </value>
+ </option>
+ </JavaCodeStyleSettings>
+ <ADDITIONAL_INDENT_OPTIONS fileType="haml">
+ <option name="INDENT_SIZE" value="2" />
+ </ADDITIONAL_INDENT_OPTIONS>
+ <ADDITIONAL_INDENT_OPTIONS fileType="java">
+ <option name="INDENT_SIZE" value="2" />
+ <option name="CONTINUATION_INDENT_SIZE" value="4" />
+ <option name="TAB_SIZE" value="8" />
+ </ADDITIONAL_INDENT_OPTIONS>
+ <ADDITIONAL_INDENT_OPTIONS fileType="js">
+ <option name="CONTINUATION_INDENT_SIZE" value="4" />
+ </ADDITIONAL_INDENT_OPTIONS>
+ <ADDITIONAL_INDENT_OPTIONS fileType="sass">
+ <option name="INDENT_SIZE" value="2" />
+ </ADDITIONAL_INDENT_OPTIONS>
+ <ADDITIONAL_INDENT_OPTIONS fileType="yml">
+ <option name="INDENT_SIZE" value="2" />
+ </ADDITIONAL_INDENT_OPTIONS>
+ <codeStyleSettings language="ECMA Script Level 4">
+ <option name="KEEP_CONTROL_STATEMENT_IN_ONE_LINE" value="false" />
+ <option name="KEEP_BLANK_LINES_IN_CODE" value="1" />
+ <option name="BLANK_LINES_AFTER_CLASS_HEADER" value="1" />
+ <option name="ALIGN_MULTILINE_PARAMETERS_IN_CALLS" value="true" />
+ <option name="ALIGN_MULTILINE_BINARY_OPERATION" value="true" />
+ <option name="ALIGN_MULTILINE_ASSIGNMENT" value="true" />
+ <option name="ALIGN_MULTILINE_TERNARY_OPERATION" value="true" />
+ <option name="ALIGN_MULTILINE_THROWS_LIST" value="true" />
+ <option name="ALIGN_MULTILINE_EXTENDS_LIST" value="true" />
+ <option name="ALIGN_MULTILINE_PARENTHESIZED_EXPRESSION" value="true" />
+ <option name="ALIGN_MULTILINE_ARRAY_INITIALIZER_EXPRESSION" value="true" />
+ <option name="CALL_PARAMETERS_WRAP" value="1" />
+ <option name="METHOD_PARAMETERS_WRAP" value="1" />
+ <option name="EXTENDS_LIST_WRAP" value="1" />
+ <option name="THROWS_LIST_WRAP" value="1" />
+ <option name="EXTENDS_KEYWORD_WRAP" value="1" />
+ <option name="THROWS_KEYWORD_WRAP" value="1" />
+ <option name="METHOD_CALL_CHAIN_WRAP" value="1" />
+ <option name="BINARY_OPERATION_WRAP" value="1" />
+ <option name="BINARY_OPERATION_SIGN_ON_NEXT_LINE" value="true" />
+ <option name="TERNARY_OPERATION_WRAP" value="1" />
+ <option name="TERNARY_OPERATION_SIGNS_ON_NEXT_LINE" value="true" />
+ <option name="FOR_STATEMENT_WRAP" value="1" />
+ <option name="ARRAY_INITIALIZER_WRAP" value="1" />
+ <option name="ASSIGNMENT_WRAP" value="5" />
+ <option name="WRAP_COMMENTS" value="true" />
+ <option name="IF_BRACE_FORCE" value="3" />
+ <option name="DOWHILE_BRACE_FORCE" value="3" />
+ <option name="WHILE_BRACE_FORCE" value="3" />
+ <option name="FOR_BRACE_FORCE" value="3" />
+ <option name="PARENT_SETTINGS_INSTALLED" value="true" />
+ </codeStyleSettings>
+ <codeStyleSettings language="JAVA">
+ <option name="ALIGN_MULTILINE_TERNARY_OPERATION" value="true" />
+ <option name="ALIGN_MULTILINE_THROWS_LIST" value="true" />
+ <option name="ALIGN_MULTILINE_EXTENDS_LIST" value="true" />
+ <option name="CALL_PARAMETERS_WRAP" value="1" />
+ <option name="METHOD_PARAMETERS_WRAP" value="5" />
+ <option name="METHOD_PARAMETERS_LPAREN_ON_NEXT_LINE" value="true" />
+ <option name="EXTENDS_LIST_WRAP" value="1" />
+ <option name="THROWS_LIST_WRAP" value="1" />
+ <option name="EXTENDS_KEYWORD_WRAP" value="1" />
+ <option name="THROWS_KEYWORD_WRAP" value="1" />
+ <option name="METHOD_CALL_CHAIN_WRAP" value="1" />
+ <option name="BINARY_OPERATION_WRAP" value="1" />
+ <option name="BINARY_OPERATION_SIGN_ON_NEXT_LINE" value="true" />
+ <option name="TERNARY_OPERATION_WRAP" value="1" />
+ <option name="TERNARY_OPERATION_SIGNS_ON_NEXT_LINE" value="true" />
+ <option name="FOR_STATEMENT_WRAP" value="1" />
+ <option name="ASSIGNMENT_WRAP" value="1" />
+ <option name="ASSERT_STATEMENT_WRAP" value="1" />
+ <option name="ASSERT_STATEMENT_COLON_ON_NEXT_LINE" value="true" />
+ <option name="IF_BRACE_FORCE" value="3" />
+ <option name="DOWHILE_BRACE_FORCE" value="3" />
+ <option name="WHILE_BRACE_FORCE" value="3" />
+ <option name="FOR_BRACE_FORCE" value="3" />
+ <option name="VARIABLE_ANNOTATION_WRAP" value="2" />
+ <option name="ENUM_CONSTANTS_WRAP" value="2" />
+ <indentOptions>
+ <option name="INDENT_SIZE" value="2" />
+ <option name="CONTINUATION_INDENT_SIZE" value="4" />
+ <option name="TAB_SIZE" value="8" />
+ </indentOptions>
+ </codeStyleSettings>
+ <codeStyleSettings language="JavaScript">
+ <option name="KEEP_BLANK_LINES_IN_CODE" value="1" />
+ <option name="ALIGN_MULTILINE_PARAMETERS_IN_CALLS" value="true" />
+ <option name="ALIGN_MULTILINE_BINARY_OPERATION" value="true" />
+ <option name="ALIGN_MULTILINE_TERNARY_OPERATION" value="true" />
+ <option name="ALIGN_MULTILINE_ARRAY_INITIALIZER_EXPRESSION" value="true" />
+ <option name="CALL_PARAMETERS_WRAP" value="1" />
+ <option name="METHOD_PARAMETERS_WRAP" value="1" />
+ <option name="METHOD_CALL_CHAIN_WRAP" value="1" />
+ <option name="BINARY_OPERATION_WRAP" value="1" />
+ <option name="BINARY_OPERATION_SIGN_ON_NEXT_LINE" value="true" />
+ <option name="TERNARY_OPERATION_WRAP" value="1" />
+ <option name="TERNARY_OPERATION_SIGNS_ON_NEXT_LINE" value="true" />
+ <option name="FOR_STATEMENT_WRAP" value="1" />
+ <option name="ARRAY_INITIALIZER_WRAP" value="1" />
+ <option name="ASSIGNMENT_WRAP" value="5" />
+ <option name="WRAP_COMMENTS" value="true" />
+ <option name="IF_BRACE_FORCE" value="3" />
+ <option name="DOWHILE_BRACE_FORCE" value="3" />
+ <option name="WHILE_BRACE_FORCE" value="3" />
+ <option name="FOR_BRACE_FORCE" value="3" />
+ <option name="PARENT_SETTINGS_INSTALLED" value="true" />
+ </codeStyleSettings>
+ </code_scheme>
+</component>
\ No newline at end of file
diff --git a/.idea/codeStyles/codeStyleConfig.xml b/.idea/codeStyles/codeStyleConfig.xml
new file mode 100644
index 0000000000..79ee123c2b
--- /dev/null
+++ b/.idea/codeStyles/codeStyleConfig.xml
@@ -0,0 +1,5 @@
+<component name="ProjectCodeStyleConfiguration">
+ <state>
+ <option name="USE_PER_PROJECT_SETTINGS" value="true" />
+ </state>
+</component>
\ No newline at end of file
diff --git a/.idea/modules.xml b/.idea/modules.xml
index e70e3fe729..a13a73c19b 100644
--- a/.idea/modules.xml
+++ b/.idea/modules.xml
@@ -1,19 +1,8 @@
<?xml version="1.0" encoding="UTF-8"?>
-
-<!--
-This file is part of JavaSMT,
-an API wrapper for a collection of SMT solvers:
-https://github.com/sosy-lab/java-smt
-
-SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
<project version="4">
<component name="ProjectModuleManager">
<modules>
<module fileurl="file://$PROJECT_DIR$/.idea/JavaSMT.iml" filepath="$PROJECT_DIR$/.idea/JavaSMT.iml" />
</modules>
</component>
-</project>
+</project>
\ No newline at end of file
diff --git a/src/org/sosy_lab/java_smt/SolverContextFactory.java b/src/org/sosy_lab/java_smt/SolverContextFactory.java
index 500beb11cf..4edb6ff4d3 100644
--- a/src/org/sosy_lab/java_smt/SolverContextFactory.java
+++ b/src/org/sosy_lab/java_smt/SolverContextFactory.java
@@ -29,6 +29,7 @@
import org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext;
import org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext;
import org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext;
+import org.sosy_lab.java_smt.solvers.apron.ApronSolverContext;
import org.sosy_lab.java_smt.solvers.boolector.BoolectorSolverContext;
import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext;
import org.sosy_lab.java_smt.solvers.cvc5.CVC5SolverContext;
@@ -55,7 +56,8 @@ public enum Solvers {
BOOLECTOR,
CVC4,
CVC5,
- YICES2
+ YICES2,
+ APRON
}
@Option(secure = true, description = "Export solver queries in SmtLib format into a file.")
@@ -282,6 +284,9 @@ private SolverContext generateContext0(Solvers solverToCreate)
case BOOLECTOR:
return BoolectorSolverContext.create(config, shutdownNotifier, logfile, randomSeed, loader);
+ case APRON:
+ return ApronSolverContext.create();
+
default:
throw new AssertionError("no solver selected");
}
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronBooleanFormulaManager.java
index 2c294e7e62..26d4589e27 100644
--- a/src/org/sosy_lab/java_smt/solvers/apron/ApronBooleanFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronBooleanFormulaManager.java
@@ -24,8 +24,11 @@
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
public class ApronBooleanFormulaManager extends AbstractBooleanFormulaManager {
- protected ApronBooleanFormulaManager(FormulaCreator pCreator) {
+
+ private ApronFormulaCreator formulaCreator;
+ protected ApronBooleanFormulaManager(ApronFormulaCreator pCreator) {
super(pCreator);
+ this.formulaCreator = pCreator;
}
@Override
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronExamples.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronExamples.java
index bfece0e87b..07c681eea2 100644
--- a/src/org/sosy_lab/java_smt/solvers/apron/ApronExamples.java
+++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronExamples.java
@@ -37,20 +37,20 @@ private static void testBox(Manager pManager) throws ApronException {
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
+ //x >= - 3 --> x+3 >= 0
Lincons1 cons2 = new Lincons1(environment);
cons2.setCoeff("x",new MpqScalar(1));
- cons2.setCst(new MpqScalar(-3));
+ cons2.setCst(new MpqScalar(+3));
cons2.setKind(Lincons1.SUPEQ);
+ Abstract1 abstract1 = new Abstract1(pManager, new Lincons1[]{cons1,cons2});
- Lincons1[] constraints = {cons1, cons2};
- Abstract1 abstract1 = new Abstract1(pManager, constraints);
+ System.out.println("Variable has to be in: "+abstract1.getBound(pManager, "x"));
+ System.out.println(abstract1.toString(pManager));
//is x = 1 satisfiable?
Lincons1 cons3 = new Lincons1(environment);
cons3.setCoeff("x",new MpqScalar(1));
@@ -68,7 +68,7 @@ private static void testBox(Manager pManager) throws ApronException {
}
public static void main(String[] args) throws ApronException {
- Manager manager = new Box();
+ Manager manager = new Polka(false);
testBox(manager);
}
}
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaCreator.java
index 182a893218..13a2a0e5f9 100644
--- a/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaCreator.java
+++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaCreator.java
@@ -20,6 +20,9 @@
package org.sosy_lab.java_smt.solvers.apron;
+import apron.Environment;
+import apron.Var;
+import com.google.common.base.Preconditions;
import java.util.List;
import javax.annotation.Nullable;
import org.sosy_lab.java_smt.api.Formula;
@@ -27,60 +30,105 @@
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;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.Type;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulas;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronBooleanType;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronIntegerType;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronRationalType;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulas.ApronVar;
-public class ApronFormulaCreator extends FormulaCreator {
+public class ApronFormulaCreator extends FormulaCreator<ApronFormulas, ApronFormulaType,Environment,Long> {
+
+ private Environment environment;
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);
+ Environment pO,
+ ApronBooleanType boolType,
+ @Nullable ApronIntegerType pIntegerType,
+ @Nullable ApronRationalType pRationalType,
+ @Nullable Long stringType,
+ @Nullable Long regexType) {
+ super(pO, boolType, pIntegerType, pRationalType, null, null);
+ this.environment = pO;
+
+ }
+
+ public Environment getEnvironment(){
+ return this.environment;
}
@Override
- public Object getBitvectorType(int bitwidth) {
+ public ApronFormulaType getBitvectorType(int bitwidth) {
return null;
}
@Override
- public Object getFloatingPointType(FloatingPointType type) {
+ public ApronFormulaType getFloatingPointType(FloatingPointType type) {
return null;
}
@Override
- public Object getArrayType(Object indexType, Object elementType) {
+ public ApronFormulaType getArrayType(ApronFormulaType indexType, ApronFormulaType elementType) {
return null;
}
@Override
- public Object makeVariable(Object pO, String varName) {
- return null;
+ public ApronFormulas makeVariable(ApronFormulaType pApronFormulaType, String varName) {
+ Preconditions.checkArgument(!environment.hasVar(varName),"Variablename already exists!");
+ Preconditions.checkArgument(
+ (pApronFormulaType.getType().equals(Type.INTEGER) || pApronFormulaType.getType().equals(Type.RATIONAL)),
+ "Only Integer or rational variables allowed1");
+ if(pApronFormulaType.getType().equals(Type.INTEGER)){
+ String[] intvars = new String[]{varName};
+ this.environment.add(intvars,new String[]{});
+ return new ApronVar();
+ }else {
+ String[] realvars = new String[]{varName};
+ this.environment.add(new String[]{}, realvars);
+ return new ApronVar();
+ }
}
@Override
- public FormulaType<?> getFormulaType(Object formula) {
+ public FormulaType<ApronFormulas> getFormulaType(ApronFormulas formula) {
+ //TODO
+ switch (formula.getFormulaType()){
+ case VAR:
+ //...
+ case TERM:
+ //...
+ case COEFF:
+ //...
+ case CONSTRAINT:
+ //...
+ case EXPRESSION:
+ //...
+ default:
+ //....
+ }
return null;
}
@Override
- public Object callFunctionImpl(Object declaration, List args) {
+ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, ApronFormulas f) {
return null;
}
@Override
- public Object declareUFImpl(String pName, Object pReturnType, List pArgTypes) {
+ public ApronFormulas callFunctionImpl(Long declaration, List<ApronFormulas> args) {
return null;
}
@Override
- protected Object getBooleanVarDeclarationImpl(Object pO) {
+ public Long declareUFImpl(
+ String pName,
+ ApronFormulaType pReturnType,
+ List<ApronFormulaType> pArgTypes) {
return null;
}
@Override
- public Object visit(FormulaVisitor visitor, Formula formula, Object f) {
+ protected Long getBooleanVarDeclarationImpl(ApronFormulas pApronFormula) {
return null;
}
}
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaManager.java
index 6b116a0f95..d60fed1ea2 100644
--- a/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaManager.java
@@ -20,6 +20,7 @@
package org.sosy_lab.java_smt.solvers.apron;
+import apron.Environment;
import java.util.Map;
import org.checkerframework.checker.nullness.qual.Nullable;
import org.sosy_lab.common.Appender;
@@ -39,15 +40,15 @@
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>{
+public class ApronFormulaManager extends AbstractFormulaManager <Long, Long, Environment, Long>{
/**
* Builds a solver from the given theory implementations.
*
* @param pFormulaCreator
* @param functionManager
* @param booleanManager
- * @param pIntegerManager
- * @param pRationalManager
+ * @param pIntegerFormulaManager
+ * @param pRationalFormulaManager
* @param bitvectorManager
* @param floatingPointManager
* @param quantifiedManager
@@ -57,11 +58,11 @@ public class ApronFormulaManager extends AbstractFormulaManager <Long, Long, Lon
* @param enumManager
*/
protected ApronFormulaManager(
- FormulaCreator pFormulaCreator,
- AbstractUFManager functionManager,
- AbstractBooleanFormulaManager booleanManager,
- @Nullable IntegerFormulaManager pIntegerManager,
- @Nullable RationalFormulaManager pRationalManager,
+ ApronFormulaCreator pFormulaCreator,
+ ApronUFManager functionManager,
+ ApronBooleanFormulaManager booleanManager,
+ ApronIntegerFormulaManager pIntegerFormulaManager,
+ ApronRationalFormulaManager pRationalFormulaManager,
@Nullable AbstractBitvectorFormulaManager bitvectorManager,
@Nullable AbstractFloatingPointFormulaManager floatingPointManager,
@Nullable AbstractQuantifiedFormulaManager quantifiedManager,
@@ -69,7 +70,8 @@ protected ApronFormulaManager(
@Nullable AbstractSLFormulaManager slManager,
@Nullable AbstractStringFormulaManager strManager,
@Nullable AbstractEnumerationFormulaManager enumManager) {
- super(pFormulaCreator, functionManager, booleanManager, pIntegerManager, pRationalManager,
+ super(pFormulaCreator, functionManager, booleanManager, pIntegerFormulaManager,
+ pRationalFormulaManager,
bitvectorManager, floatingPointManager, quantifiedManager, arrayManager, slManager,
strManager, enumManager);
}
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronIntegerFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronIntegerFormulaManager.java
index 0d380209c6..807927a7c1 100644
--- a/src/org/sosy_lab/java_smt/solvers/apron/ApronIntegerFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronIntegerFormulaManager.java
@@ -20,6 +20,7 @@
package org.sosy_lab.java_smt.solvers.apron;
+import apron.Environment;
import java.math.BigDecimal;
import java.math.BigInteger;
import java.util.List;
@@ -28,130 +29,96 @@
import org.sosy_lab.java_smt.api.IntegerFormulaManager;
import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula;
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulas;
public class ApronIntegerFormulaManager extends ApronNumeralFormulaManager<IntegerFormula, IntegerFormula>
implements IntegerFormulaManager {
+
protected ApronIntegerFormulaManager(
- FormulaCreator pCreator,
+ FormulaCreator<ApronFormulas, ApronFormulaType, Environment, Long> pCreator,
NonLinearArithmetic pNonLinearArithmetic) {
super(pCreator, pNonLinearArithmetic);
}
@Override
- public BooleanFormula modularCongruence(
- IntegerFormula number1,
- IntegerFormula number2,
- BigInteger n) {
- return null;
- }
-
- @Override
- public BooleanFormula modularCongruence(IntegerFormula number1, IntegerFormula number2, long n) {
- return null;
+ protected boolean isNumeral(ApronFormulas val) {
+ return false;
}
@Override
- public IntegerFormula modulo(IntegerFormula numerator, IntegerFormula denumerator) {
+ protected ApronFormulas makeNumberImpl(long i) {
return null;
}
@Override
- public IntegerFormula makeNumber(long number) {
+ protected ApronFormulas makeNumberImpl(BigInteger i) {
return null;
}
@Override
- public IntegerFormula makeNumber(BigInteger number) {
+ protected ApronFormulas makeNumberImpl(String i) {
return null;
}
@Override
- public IntegerFormula makeNumber(double number) {
+ protected ApronFormulas makeNumberImpl(double pNumber) {
return null;
}
@Override
- public IntegerFormula makeNumber(BigDecimal number) {
+ protected ApronFormulas makeNumberImpl(BigDecimal pNumber) {
return null;
}
@Override
- public IntegerFormula makeNumber(String pI) {
+ protected ApronFormulas makeVariableImpl(String i) {
return null;
}
@Override
- public IntegerFormula makeNumber(Rational pRational) {
+ protected ApronFormulas negate(ApronFormulas pParam1) {
return null;
}
@Override
- public IntegerFormula makeVariable(String pVar) {
+ protected ApronFormulas add(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public IntegerFormula negate(IntegerFormula number) {
+ protected ApronFormulas subtract(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public IntegerFormula add(IntegerFormula number1, IntegerFormula number2) {
+ protected ApronFormulas equal(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public IntegerFormula sum(List operands) {
+ protected ApronFormulas distinctImpl(List<ApronFormulas> pNumbers) {
return null;
}
@Override
- public IntegerFormula subtract(IntegerFormula number1, IntegerFormula number2) {
+ protected ApronFormulas greaterThan(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public IntegerFormula divide(IntegerFormula numerator, IntegerFormula denumerator) {
+ protected ApronFormulas greaterOrEquals(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public IntegerFormula multiply(IntegerFormula number1, IntegerFormula number2) {
+ protected ApronFormulas lessThan(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public BooleanFormula equal(IntegerFormula number1, IntegerFormula number2) {
+ protected ApronFormulas lessOrEquals(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
- @Override
- public BooleanFormula distinct(List pNumbers) {
- return null;
- }
-
- @Override
- public BooleanFormula greaterThan(IntegerFormula number1, IntegerFormula number2) {
- return null;
- }
-
- @Override
- public BooleanFormula greaterOrEquals(IntegerFormula number1, IntegerFormula number2) {
- return null;
- }
-
- @Override
- public BooleanFormula lessThan(IntegerFormula number1, IntegerFormula number2) {
- return null;
- }
-
- @Override
- public BooleanFormula lessOrEquals(IntegerFormula number1, IntegerFormula number2) {
- return null;
- }
-
- @Override
- public IntegerFormula floor(IntegerFormula formula) {
- return null;
- }
}
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronModel.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronModel.java
new file mode 100644
index 0000000000..96878c180d
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronModel.java
@@ -0,0 +1,46 @@
+/*
+ * 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 com.google.common.collect.ImmutableList;
+import javax.annotation.Nullable;
+import org.sosy_lab.java_smt.basicimpl.AbstractModel;
+import org.sosy_lab.java_smt.basicimpl.AbstractProver;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+
+public class ApronModel extends AbstractModel {
+ protected ApronModel(
+ AbstractProver prover,
+ FormulaCreator creator) {
+ super(prover, creator);
+ }
+
+ @Override
+ public ImmutableList<ValueAssignment> asList() {
+ return null;
+ }
+
+ @Nullable
+ @Override
+ protected Object evalImpl(Object formula) {
+ return null;
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronNumeralFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronNumeralFormulaManager.java
index a5a84cddf8..e1215b7107 100644
--- a/src/org/sosy_lab/java_smt/solvers/apron/ApronNumeralFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronNumeralFormulaManager.java
@@ -20,6 +20,7 @@
package org.sosy_lab.java_smt.solvers.apron;
+import apron.Environment;
import java.math.BigDecimal;
import java.math.BigInteger;
import java.util.List;
@@ -27,99 +28,16 @@
import org.sosy_lab.java_smt.api.NumeralFormula;
import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager;
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulas;
-public class ApronNumeralFormulaManager<
+abstract class ApronNumeralFormulaManager <
ParamFormulaType extends NumeralFormula, ResultFormulaType extends NumeralFormula>
extends AbstractNumeralFormulaManager<
- Long, Long, Long, ParamFormulaType, ResultFormulaType, Long> {
+ ApronFormulas, ApronFormulaType, Environment, ParamFormulaType, ResultFormulaType, Long>{
protected ApronNumeralFormulaManager(
- FormulaCreator<Long, Long, Long, Long> pCreator,
+ FormulaCreator<ApronFormulas, ApronFormulaType, Environment, Long> pCreator,
NonLinearArithmetic pNonLinearArithmetic) {
super(pCreator, pNonLinearArithmetic);
}
-
- @Override
- public FormulaType<ResultFormulaType> getFormulaType() {
- return null;
- }
-
- @Override
- protected boolean isNumeral(Long val) {
- return false;
- }
-
- @Override
- protected Long makeNumberImpl(long i) {
- return null;
- }
-
- @Override
- protected Long makeNumberImpl(BigInteger i) {
- return null;
- }
-
- @Override
- protected Long makeNumberImpl(String i) {
- return null;
- }
-
- @Override
- protected Long makeNumberImpl(double pNumber) {
- return null;
- }
-
- @Override
- protected Long makeNumberImpl(BigDecimal pNumber) {
- return null;
- }
-
- @Override
- protected Long makeVariableImpl(String i) {
- return null;
- }
-
- @Override
- protected Long negate(Long pParam1) {
- return null;
- }
-
- @Override
- protected Long add(Long pParam1, Long pParam2) {
- return null;
- }
-
- @Override
- protected Long subtract(Long pParam1, Long pParam2) {
- return null;
- }
-
- @Override
- protected Long equal(Long pParam1, Long pParam2) {
- return null;
- }
-
- @Override
- protected Long distinctImpl(List<Long> pNumbers) {
- return null;
- }
-
- @Override
- protected Long greaterThan(Long pParam1, Long pParam2) {
- return null;
- }
-
- @Override
- protected Long greaterOrEquals(Long pParam1, Long pParam2) {
- return null;
- }
-
- @Override
- protected Long lessThan(Long pParam1, Long pParam2) {
- return null;
- }
-
- @Override
- protected Long lessOrEquals(Long pParam1, Long pParam2) {
- return null;
- }
}
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronRationalFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronRationalFormulaManager.java
index c342e67b3f..bfc6f334f9 100644
--- a/src/org/sosy_lab/java_smt/solvers/apron/ApronRationalFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronRationalFormulaManager.java
@@ -20,6 +20,7 @@
package org.sosy_lab.java_smt.solvers.apron;
+import apron.Environment;
import java.math.BigDecimal;
import java.math.BigInteger;
import java.util.List;
@@ -30,112 +31,95 @@
import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula;
import org.sosy_lab.java_smt.api.RationalFormulaManager;
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulas;
public class ApronRationalFormulaManager extends ApronNumeralFormulaManager<NumeralFormula,
RationalFormula> implements RationalFormulaManager {
+
protected ApronRationalFormulaManager(
- FormulaCreator<Long, Long, Long, Long> pCreator,
+ FormulaCreator<ApronFormulas, ApronFormulaType, Environment, Long> pCreator,
NonLinearArithmetic pNonLinearArithmetic) {
super(pCreator, pNonLinearArithmetic);
}
@Override
- public RationalFormula makeNumber(long number) {
- return null;
- }
-
- @Override
- public RationalFormula makeNumber(BigInteger number) {
- return null;
- }
-
- @Override
- public RationalFormula makeNumber(double number) {
- return null;
- }
-
- @Override
- public RationalFormula makeNumber(BigDecimal number) {
- return null;
- }
-
- @Override
- public RationalFormula makeNumber(String pI) {
- return null;
+ protected boolean isNumeral(ApronFormulas val) {
+ return false;
}
@Override
- public RationalFormula makeNumber(Rational pRational) {
+ protected ApronFormulas makeNumberImpl(long i) {
return null;
}
@Override
- public RationalFormula makeVariable(String pVar) {
+ protected ApronFormulas makeNumberImpl(BigInteger i) {
return null;
}
@Override
- public RationalFormula negate(NumeralFormula number) {
+ protected ApronFormulas makeNumberImpl(String i) {
return null;
}
@Override
- public RationalFormula add(NumeralFormula number1, NumeralFormula number2) {
+ protected ApronFormulas makeNumberImpl(double pNumber) {
return null;
}
@Override
- public RationalFormula sum(List operands) {
+ protected ApronFormulas makeNumberImpl(BigDecimal pNumber) {
return null;
}
@Override
- public RationalFormula subtract(NumeralFormula number1, NumeralFormula number2) {
+ protected ApronFormulas makeVariableImpl(String i) {
return null;
}
@Override
- public RationalFormula divide(NumeralFormula numerator, NumeralFormula denumerator) {
+ protected ApronFormulas negate(ApronFormulas pParam1) {
return null;
}
@Override
- public RationalFormula multiply(NumeralFormula number1, NumeralFormula number2) {
+ protected ApronFormulas add(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public BooleanFormula equal(NumeralFormula number1, NumeralFormula number2) {
+ protected ApronFormulas subtract(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public BooleanFormula distinct(List pNumbers) {
+ protected ApronFormulas equal(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public BooleanFormula greaterThan(NumeralFormula number1, NumeralFormula number2) {
+ protected ApronFormulas distinctImpl(List<ApronFormulas> pNumbers) {
return null;
}
@Override
- public BooleanFormula greaterOrEquals(NumeralFormula number1, NumeralFormula number2) {
+ protected ApronFormulas greaterThan(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public BooleanFormula lessThan(NumeralFormula number1, NumeralFormula number2) {
+ protected ApronFormulas greaterOrEquals(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public BooleanFormula lessOrEquals(NumeralFormula number1, NumeralFormula number2) {
+ protected ApronFormulas lessThan(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
@Override
- public IntegerFormula floor(NumeralFormula formula) {
+ protected ApronFormulas lessOrEquals(ApronFormulas pParam1, ApronFormulas pParam2) {
return null;
}
}
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronSolverContext.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronSolverContext.java
index bc2c5008d6..7e399adac9 100644
--- a/src/org/sosy_lab/java_smt/solvers/apron/ApronSolverContext.java
+++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronSolverContext.java
@@ -20,37 +20,94 @@
package org.sosy_lab.java_smt.solvers.apron;
+import apron.ApronException;
+import apron.Box;
+import apron.Environment;
+import apron.Manager;
+import com.microsoft.z3.Native;
import java.util.Set;
+import org.sosy_lab.common.ShutdownNotifier;
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
import org.sosy_lab.java_smt.api.FormulaManager;
import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
import org.sosy_lab.java_smt.api.OptimizationProverEnvironment;
import org.sosy_lab.java_smt.api.ProverEnvironment;
+import org.sosy_lab.java_smt.basicimpl.AbstractNumeralFormulaManager.NonLinearArithmetic;
import org.sosy_lab.java_smt.basicimpl.AbstractSolverContext;
+import org.sosy_lab.java_smt.solvers.apron.types.ApronFormulaType.ApronBooleanType;
public class ApronSolverContext extends AbstractSolverContext {
- protected ApronSolverContext(FormulaManager fmgr) {
+
+ private Manager manager;
+ private final ApronFormulaCreator formulaCreator;
+ protected ShutdownNotifier shutdownNotifier;
+ protected ApronSolverContext(ApronFormulaManager fmgr,
+ Manager pManager,
+ ApronFormulaCreator pFormulaCreator,
+ ShutdownNotifier pShutdownNotifier) {
super(fmgr);
+ this.manager = pManager;
+ this.formulaCreator = pFormulaCreator;
+ this.shutdownNotifier = pShutdownNotifier;
+ }
+
+ public static synchronized ApronSolverContext create(NonLinearArithmetic pNonLinearArithmetic,
+ ShutdownNotifier pShutdownNotifier){
+
+ Environment env = new Environment();
+ Manager manager = new Box();
+ ApronBooleanType booleanType = new ApronBooleanType();
+ ApronFormulaCreator formulaCreator = new ApronFormulaCreator(env, booleanType, null,null,null,null);
+ ApronUFManager ufManager = new ApronUFManager(formulaCreator);
+ ApronBooleanFormulaManager booleanFormulaManager =
+ new ApronBooleanFormulaManager(formulaCreator);
+ ApronIntegerFormulaManager integerFormulaManager =
+ new ApronIntegerFormulaManager(formulaCreator, pNonLinearArithmetic);
+ ApronRationalFormulaManager rationalFormulaManager =
+ new ApronRationalFormulaManager(formulaCreator, pNonLinearArithmetic);
+ ApronFormulaManager fmgr = new ApronFormulaManager(formulaCreator, ufManager,
+ booleanFormulaManager,integerFormulaManager,rationalFormulaManager,null,null,null,null,
+ null,null,null);
+ return new ApronSolverContext(fmgr, manager, formulaCreator, pShutdownNotifier);
}
+ public Manager getManager(){
+ return this.manager;
+ }
+
+ public ApronFormulaCreator getFormulaCreator(){
+ return this.formulaCreator;
+ }
@Override
public String getVersion() {
- return null;
+ return this.manager.getVersion();
}
@Override
public Solvers getSolverName() {
- return null;
+ return Solvers.APRON;
}
@Override
public void close() {
-
+ //TODO
}
@Override
protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> options) {
- return null;
+ return newApronProverEnvironment(options);
+ }
+
+ private ProverEnvironment newApronProverEnvironment(Set<ProverOptions> pProverOptions){
+ try{
+ ApronBooleanFormulaManager booleanFormulaManager =
+ new ApronBooleanFormulaManager(this.formulaCreator);
+ return new ApronTheoremProver(pProverOptions,booleanFormulaManager,this.shutdownNotifier,this);
+ } catch(ApronException pApronException){
+ System.out.println(pApronException.toString());
+ System.exit(0);
+ return null;
+ }
}
@Override
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/ApronTheoremProver.java b/src/org/sosy_lab/java_smt/solvers/apron/ApronTheoremProver.java
index 4427755eb5..ff01731aa3 100644
--- a/src/org/sosy_lab/java_smt/solvers/apron/ApronTheoremProver.java
+++ b/src/org/sosy_lab/java_smt/solvers/apron/ApronTheoremProver.java
@@ -20,11 +20,14 @@
package org.sosy_lab.java_smt.solvers.apron;
+import apron.Abstract1;
+import apron.ApronException;
import java.util.Collection;
import java.util.List;
import java.util.Optional;
import java.util.Set;
import javax.annotation.Nullable;
+import org.checkerframework.checker.units.qual.A;
import org.sosy_lab.common.ShutdownNotifier;
import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.BooleanFormulaManager;
@@ -33,13 +36,21 @@
import org.sosy_lab.java_smt.api.ProverEnvironment;
import org.sosy_lab.java_smt.api.SolverException;
import org.sosy_lab.java_smt.basicimpl.AbstractProverWithAllSat;
+import org.sosy_lab.java_smt.utils.SolverUtils;
public class ApronTheoremProver extends AbstractProverWithAllSat<Void> implements ProverEnvironment {
+
+ private Abstract1 abstract1;
+ private ApronSolverContext solverContext;
protected ApronTheoremProver(
Set pSet,
BooleanFormulaManager pBmgr,
- ShutdownNotifier pShutdownNotifier) {
+ ShutdownNotifier pShutdownNotifier,
+ ApronSolverContext pApronSolverContext) throws ApronException {
super(pSet, pBmgr, pShutdownNotifier);
+ this.solverContext = pApronSolverContext;
+ this.abstract1 = new Abstract1(pApronSolverContext.getManager(),
+ pApronSolverContext.getFormulaCreator().getEnvironment());
}
@Override
@@ -64,10 +75,19 @@ public int size() {
}
@Override
- public boolean isUnsat() throws SolverException, InterruptedException {
- return false;
+ public boolean isUnsat() throws SolverException, InterruptedException{
+ return isUnsatApron();
}
+ private boolean isUnsatApron(){
+ try {
+ return abstract1.isBottom(solverContext.getManager());
+ } catch (ApronException pApronException){
+ System.out.println(pApronException.toString());
+ System.exit(0);
+ return false;
+ }
+ }
@Override
public Model getModel() throws SolverException {
return null;
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/types/ApronFormulaType.java b/src/org/sosy_lab/java_smt/solvers/apron/types/ApronFormulaType.java
new file mode 100644
index 0000000000..dfaa98537d
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/apron/types/ApronFormulaType.java
@@ -0,0 +1,62 @@
+/*
+ * 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.types;
+
+import org.sosy_lab.java_smt.solvers.apron.ApronIntegerFormulaManager;
+
+public interface ApronFormulaType {
+
+ enum Type{
+ BOOLEAN,
+ INTEGER,
+ RATIONAL
+ }
+
+ Type getType();
+ class ApronIntegerType implements ApronFormulaType{
+
+ public ApronIntegerType(){}
+ @Override
+ public Type getType(){
+ return Type.INTEGER;
+ }
+
+ }
+
+ class ApronRationalType implements ApronFormulaType{
+
+ public ApronRationalType(){}
+ @Override
+ public Type getType(){
+ return Type.RATIONAL;
+ }
+ }
+
+ class ApronBooleanType implements ApronFormulaType{
+
+ public ApronBooleanType(){
+ }
+ @Override
+ public Type getType(){
+ return Type.BOOLEAN;
+ }
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/apron/types/ApronFormulas.java b/src/org/sosy_lab/java_smt/solvers/apron/types/ApronFormulas.java
new file mode 100644
index 0000000000..e66ce46010
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/apron/types/ApronFormulas.java
@@ -0,0 +1,94 @@
+/*
+ * 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.types;
+
+import apron.Coeff;
+import apron.Linexpr1;
+import apron.Linterm1;
+import org.sosy_lab.java_smt.api.Formula;
+
+public interface ApronFormulas extends Formula {
+
+ enum ApronFormulaType {
+ VAR,
+ COEFF,
+ TERM,
+ EXPRESSION,
+ CONSTRAINT
+ }
+
+ ApronFormulaType getFormulaType();
+
+ class ApronVar implements ApronFormulas {
+
+ public ApronVar(){}
+ @Override
+ public ApronFormulaType getFormulaType() {
+ return ApronFormulaType.VAR;
+ }
+ }
+
+ class ApronCoeff implements ApronFormulas {
+
+ public ApronCoeff(){}
+ @Override
+ public ApronFormulaType getFormulaType() {
+ return ApronFormulaType.COEFF;
+ }
+ }
+
+ class ApronTerm implements ApronFormulas {
+ private Linterm1 linterm1;
+
+ public ApronTerm(String pVar,Coeff pCoeff){
+ this.linterm1 = new Linterm1(pVar,pCoeff);
+ }
+
+ @Override
+ public ApronFormulaType getFormulaType() {
+ return ApronFormulaType.TERM;
+ }
+ }
+
+ class ApronExpr implements ApronFormulas {
+ private Linexpr1 linexpr1;
+
+ public ApronExpr(){
+
+ }
+
+ @Override
+ public ApronFormulaType getFormulaType() {
+ return ApronFormulaType.EXPRESSION;
+ }
+ }
+
+ class ApronCons implements ApronFormulas {
+ public ApronCons(){
+
+ }
+
+ @Override
+ public ApronFormulaType getFormulaType() {
+ return ApronFormulaType.CONSTRAINT;
+ }
+ }
+}