From: mudathirmahgoub Date: Fri, 22 Oct 2021 23:00:06 +0000 (-0500) Subject: Refactor java package name from cvc5 to io.github.cvc5.api (#7340) X-Git-Tag: cvc5-1.0.0~993 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=60c9b4980920e0f279085e4dd1ea2518b218074c;p=cvc5.git Refactor java package name from cvc5 to io.github.cvc5.api (#7340) This PR refactors java package name from cvc5 to io.github.cvc5.api. It also refactor the names of cpp and java files. --- diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt index 20a5d91a3..7c897a354 100644 --- a/docs/api/java/CMakeLists.txt +++ b/docs/api/java/CMakeLists.txt @@ -28,7 +28,7 @@ if(BUILD_BINDINGS_JAVA) add_custom_command( OUTPUT "${JAVADOC_INDEX_FILE}" COMMAND - ${Java_JAVADOC_EXECUTABLE} cvc5 + ${Java_JAVADOC_EXECUTABLE} io.github.cvc5.api -sourcepath ${CMAKE_SOURCE_DIR}/src/api/java/ -d ${JAVADOC_OUTPUT_DIR} -cp ${CMAKE_BINARY_DIR}/src/api/java/cvc5.jar diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index 181c16614..6209cf9dd 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -15,7 +15,7 @@ * */ -import cvc5.*; +import io.github.cvc5.api.*; import java.util.*; public class BitVectors diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java index 3e22604dd..07b9781d2 100644 --- a/examples/api/java/BitVectorsAndArrays.java +++ b/examples/api/java/BitVectorsAndArrays.java @@ -15,7 +15,7 @@ * */ -import cvc5.*; +import io.github.cvc5.api.*; import java.util.*; public class BitVectorsAndArrays diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index d25ea849e..66cd30b2b 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -17,7 +17,7 @@ * The model is displayed using getValue(). */ -import cvc5.*; +import io.github.cvc5.api.*; import java.util.Iterator; public class Combination diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java index b230affd5..85f878098 100644 --- a/examples/api/java/Datatypes.java +++ b/examples/api/java/Datatypes.java @@ -13,7 +13,7 @@ * An example of using inductive datatypes in cvc5. */ -import cvc5.*; +import io.github.cvc5.api.*; import java.util.Iterator; public class Datatypes diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java index bf87fc6be..2d62a7570 100644 --- a/examples/api/java/Exceptions.java +++ b/examples/api/java/Exceptions.java @@ -15,7 +15,7 @@ * A simple demonstration of catching CVC4 execptions via the Java API. */ -import cvc5.*; +import io.github.cvc5.api.*; public class Exceptions { diff --git a/examples/api/java/Extract.java b/examples/api/java/Extract.java index d86b7b1ef..0d8d6c2b2 100644 --- a/examples/api/java/Extract.java +++ b/examples/api/java/Extract.java @@ -15,7 +15,7 @@ * */ -import cvc5.*; +import io.github.cvc5.api.*; public class Extract { diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java index dda5bbcd0..88e24cbab 100644 --- a/examples/api/java/FloatingPointArith.java +++ b/examples/api/java/FloatingPointArith.java @@ -18,9 +18,9 @@ * an IEEE 754-2008 bit-vector to a floating-point number. */ -import static cvc5.Kind.*; +import static io.github.cvc5.api.Kind.*; -import cvc5.*; +import io.github.cvc5.api.*; public class FloatingPointArith { diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index 1013c0a9e..966bfb329 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -13,7 +13,7 @@ * A very simple CVC5 tutorial example. */ -import cvc5.*; +import io.github.cvc5.api.*; public class HelloWorld { diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index 0c728894a..2e67d526f 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -14,7 +14,7 @@ * the push pop of cvc5. This also gives an example option. */ -import cvc5.*; +import io.github.cvc5.api.*; public class LinearArith { public static void main(String args[]) throws CVC5ApiException diff --git a/examples/api/java/QuickStart.java b/examples/api/java/QuickStart.java index 4e1798d39..73bddb083 100644 --- a/examples/api/java/QuickStart.java +++ b/examples/api/java/QuickStart.java @@ -14,7 +14,7 @@ * */ -import cvc5.*; +import io.github.cvc5.api.*; import java.math.BigInteger; import java.util.ArrayList; import java.util.Arrays; diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java index cfcbb3b8e..f6454c812 100644 --- a/examples/api/java/Relations.java +++ b/examples/api/java/Relations.java @@ -13,9 +13,9 @@ * A simple demonstration of reasoning about relations with CVC4 via Java API. */ -import static cvc5.Kind.*; +import static io.github.cvc5.api.Kind.*; -import cvc5.*; +import io.github.cvc5.api.*; /* This file uses the API to make a sat call equivalent to the following benchmark: diff --git a/examples/api/java/Sequences.java b/examples/api/java/Sequences.java index 8d327fb2b..d1bb0440d 100644 --- a/examples/api/java/Sequences.java +++ b/examples/api/java/Sequences.java @@ -13,9 +13,9 @@ * A simple demonstration of reasoning about sequences with cvc5 via C++ API. */ -import static cvc5.Kind.*; +import static io.github.cvc5.api.Kind.*; -import cvc5.*; +import io.github.cvc5.api.*; public class Sequences { diff --git a/examples/api/java/Sets.java b/examples/api/java/Sets.java index 38f7d194d..602014c96 100644 --- a/examples/api/java/Sets.java +++ b/examples/api/java/Sets.java @@ -13,9 +13,9 @@ * A simple demonstration of reasoning about sets with cvc5. */ -import static cvc5.Kind.*; +import static io.github.cvc5.api.Kind.*; -import cvc5.*; +import io.github.cvc5.api.*; public class Sets { diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java index c5aad0558..e524eb3e3 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -13,9 +13,9 @@ * An example of accessing CVC4's statistics using the Java API. */ -import static cvc5.Kind.*; +import static io.github.cvc5.api.Kind.*; -import cvc5.*; +import io.github.cvc5.api.*; import java.util.List; import java.util.Map; @@ -26,7 +26,7 @@ public class Statistics Solver solver = getSolver(); // Get the statistics from the `Solver` and iterate over them. The // `Statistics` class implements the `Iterable>` interface. - cvc5.Statistics stats = solver.getStatistics(); + io.github.cvc5.api.Statistics stats = solver.getStatistics(); // short version System.out.println("Short version:"); System.out.println(stats); diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java index e023459fa..6cc152159 100644 --- a/examples/api/java/Strings.java +++ b/examples/api/java/Strings.java @@ -13,9 +13,9 @@ * A simple demonstration of reasoning about strings with cvc5 via C++ API. */ -import static cvc5.Kind.*; +import static io.github.cvc5.api.Kind.*; -import cvc5.*; +import io.github.cvc5.api.*; public class Strings { diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java index 1a53a0dd1..8b96dff50 100644 --- a/examples/api/java/SygusFun.java +++ b/examples/api/java/SygusFun.java @@ -48,9 +48,9 @@ * ) */ -import static cvc5.Kind.*; +import static io.github.cvc5.api.Kind.*; -import cvc5.*; +import io.github.cvc5.api.*; public class SygusFun { diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java index b39094ae5..fb079d49f 100644 --- a/examples/api/java/SygusGrammar.java +++ b/examples/api/java/SygusGrammar.java @@ -45,9 +45,9 @@ * ) */ -import static cvc5.Kind.*; +import static io.github.cvc5.api.Kind.*; -import cvc5.*; +import io.github.cvc5.api.*; public class SygusGrammar { diff --git a/examples/api/java/SygusInv.java b/examples/api/java/SygusInv.java index 47d6797ba..6c66c910b 100644 --- a/examples/api/java/SygusInv.java +++ b/examples/api/java/SygusInv.java @@ -36,9 +36,9 @@ * ) */ -import static cvc5.Kind.*; +import static io.github.cvc5.api.Kind.*; -import cvc5.*; +import io.github.cvc5.api.*; public class SygusInv { diff --git a/examples/api/java/Transcendentals.java b/examples/api/java/Transcendentals.java index 5e8c26820..026f9b826 100644 --- a/examples/api/java/Transcendentals.java +++ b/examples/api/java/Transcendentals.java @@ -13,9 +13,9 @@ * A simple demonstration of the transcendental extension. */ -import static cvc5.Kind.*; +import static io.github.cvc5.api.Kind.*; -import cvc5.*; +import io.github.cvc5.api.*; public class Transcendentals { diff --git a/examples/api/java/UnsatCores.java b/examples/api/java/UnsatCores.java index 2f83ddc9c..cefa90290 100644 --- a/examples/api/java/UnsatCores.java +++ b/examples/api/java/UnsatCores.java @@ -13,7 +13,7 @@ * An example of interacting with unsat cores using CVC4's Java API. */ -import cvc5.*; +import io.github.cvc5.api.*; import java.util.Arrays; public class UnsatCores diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index df35390ea..5f522f4d1 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -14,15 +14,15 @@ ## # create directories -file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/cvc5") +file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/io/github/cvc5/api") set(JNI_DIR "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/jni") file(MAKE_DIRECTORY ${JNI_DIR}) -# Generate cvc5/Kind.java +# Generate Kind.java configure_file(genkinds.py.in genkinds.py) set(JAVA_KIND_FILE - "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/cvc5/Kind.java" + "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/io/github/cvc5/api/Kind.java" ) add_custom_command( @@ -34,7 +34,7 @@ add_custom_command( "${PYTHON_EXECUTABLE}" "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" - --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/cvc5/Kind" + --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/src/api/java/io/github/cvc5/api/Kind" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" @@ -48,29 +48,29 @@ include(UseJava) # specify java source files set(JAVA_FILES - ${CMAKE_CURRENT_LIST_DIR}/cvc5/AbstractPointer.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiException.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiOptionException.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiRecoverableException.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Datatype.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/DatatypeConstructor.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/DatatypeConstructorDecl.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/DatatypeDecl.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/DatatypeSelector.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Grammar.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/IPointer.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Op.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/OptionInfo.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Pair.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Result.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/RoundingMode.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Solver.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Sort.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Stat.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Statistics.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Term.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Triplet.java - ${CMAKE_CURRENT_LIST_DIR}/cvc5/Utils.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/AbstractPointer.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/CVC5ApiException.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/CVC5ApiOptionException.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/CVC5ApiRecoverableException.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Datatype.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/DatatypeConstructor.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/DatatypeConstructorDecl.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/DatatypeDecl.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/DatatypeSelector.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Grammar.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/IPointer.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Op.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/OptionInfo.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Pair.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Result.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/RoundingMode.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Solver.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Sort.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Stat.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Statistics.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Term.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Triplet.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/api/Utils.java ${JAVA_KIND_FILE} ) @@ -110,21 +110,21 @@ message(STATUS "JAVA_INCLUDE_PATH2 : ${JAVA_INCLUDE_PATH2}") message(STATUS "JAVA_AWT_INCLUDE_PATH: ${JAVA_AWT_INCLUDE_PATH}") add_library(cvc5jni SHARED - jni/cvc5_Datatype.cpp - jni/cvc5_DatatypeConstructor.cpp - jni/cvc5_DatatypeConstructorDecl.cpp - jni/cvc5_DatatypeDecl.cpp - jni/cvc5_DatatypeSelector.cpp - jni/cvc5_Grammar.cpp - jni/cvc5_Op.cpp - jni/cvc5_OptionInfo.cpp - jni/cvc5_Result.cpp - jni/cvc5_Solver.cpp - jni/cvc5_Sort.cpp - jni/cvc5_Stat.cpp - jni/cvc5_Statistics.cpp - jni/cvc5_Term.cpp - jni/cvc5JavaApi.cpp) + jni/api_utilities.cpp + jni/datatype.cpp + jni/datatype_constructor.cpp + jni/datatype_constructor_decl.cpp + jni/datatype_decl.cpp + jni/datatype_selector.cpp + jni/grammar.cpp + jni/op.cpp + jni/option_info.cpp + jni/result.cpp + jni/solver.cpp + jni/sort.cpp + jni/stat.cpp + jni/statistics.cpp + jni/term.cpp) add_dependencies(cvc5jni generate-jni-headers) diff --git a/src/api/java/cvc5/AbstractPointer.java b/src/api/java/cvc5/AbstractPointer.java deleted file mode 100644 index 8006b67be..000000000 --- a/src/api/java/cvc5/AbstractPointer.java +++ /dev/null @@ -1,45 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -abstract class AbstractPointer implements IPointer -{ - protected final Solver solver; - protected final long pointer; - - public long getPointer() - { - return pointer; - } - - public Solver getSolver() - { - return solver; - } - - @Override public String toString() - { - return toString(pointer); - } - - abstract protected String toString(long pointer); - - AbstractPointer(Solver solver, long pointer) - { - this.solver = solver; - this.pointer = pointer; - } -} diff --git a/src/api/java/cvc5/CVC5ApiException.java b/src/api/java/cvc5/CVC5ApiException.java deleted file mode 100644 index 8b8b61198..000000000 --- a/src/api/java/cvc5/CVC5ApiException.java +++ /dev/null @@ -1,24 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -public class CVC5ApiException extends Exception -{ - public CVC5ApiException(String message) - { - super(message); - } -} diff --git a/src/api/java/cvc5/CVC5ApiOptionException.java b/src/api/java/cvc5/CVC5ApiOptionException.java deleted file mode 100644 index e792091e1..000000000 --- a/src/api/java/cvc5/CVC5ApiOptionException.java +++ /dev/null @@ -1,24 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Gereon Kremer, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -public class CVC5ApiOptionException extends CVC5ApiRecoverableException -{ - public CVC5ApiOptionException(String message) - { - super(message); - } -} diff --git a/src/api/java/cvc5/CVC5ApiRecoverableException.java b/src/api/java/cvc5/CVC5ApiRecoverableException.java deleted file mode 100644 index 035a79ab6..000000000 --- a/src/api/java/cvc5/CVC5ApiRecoverableException.java +++ /dev/null @@ -1,24 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -public class CVC5ApiRecoverableException extends CVC5ApiException -{ - public CVC5ApiRecoverableException(String message) - { - super(message); - } -} diff --git a/src/api/java/cvc5/Datatype.java b/src/api/java/cvc5/Datatype.java deleted file mode 100644 index 42e06286c..000000000 --- a/src/api/java/cvc5/Datatype.java +++ /dev/null @@ -1,233 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -import java.util.Iterator; -import java.util.NoSuchElementException; - -public class Datatype extends AbstractPointer implements Iterable -{ - // region construction and destruction - Datatype(Solver solver, long pointer) - { - super(solver, pointer); - } - - protected static native void deletePointer(long pointer); - - public long getPointer() - { - return pointer; - } - - @Override public void finalize() - { - deletePointer(pointer); - } - - // endregion - - /** - * Get the datatype constructor at a given index. - * @param idx the index of the datatype constructor to return - * @return the datatype constructor with the given index - */ - public DatatypeConstructor getConstructor(int idx) - { - long constructorPointer = getConstructor(pointer, idx); - return new DatatypeConstructor(solver, constructorPointer); - } - - private native long getConstructor(long pointer, int index); - - /** - * Get the datatype constructor with the given name. - * This is a linear search through the constructors, so in case of multiple, - * similarly-named constructors, the first is returned. - * @param name the name of the datatype constructor - * @return the datatype constructor with the given name - */ - public DatatypeConstructor getConstructor(String name) - { - long constructorPointer = getConstructor(pointer, name); - return new DatatypeConstructor(solver, constructorPointer); - } - - private native long getConstructor(long pointer, String name); - - /** - * Get a term representing the datatype constructor with the given name. - * This is a linear search through the constructors, so in case of multiple, - * similarly-named constructors, the - * first is returned. - */ - public Term getConstructorTerm(String name) - { - long termPointer = getConstructorTerm(pointer, name); - return new Term(solver, termPointer); - } - - private native long getConstructorTerm(long pointer, String name); - - /** - * Get the datatype constructor with the given name. - * This is a linear search through the constructors and their selectors, so - * in case of multiple, similarly-named selectors, the first is returned. - * @param name the name of the datatype selector - * @return the datatype selector with the given name - */ - public DatatypeSelector getSelector(String name) - { - long selectorPointer = getSelector(pointer, name); - return new DatatypeSelector(solver, selectorPointer); - } - - private native long getSelector(long pointer, String name); - - /** @return the name of this Datatype. */ - public String getName() - { - return getName(pointer); - } - - private native String getName(long pointer); - - /** @return the number of constructors for this Datatype. */ - public int getNumConstructors() - { - return getNumConstructors(pointer); - } - - private native int getNumConstructors(long pointer); - - /** @return true if this datatype is parametric */ - public boolean isParametric() - { - return isParametric(pointer); - } - - private native boolean isParametric(long pointer); - - /** @return true if this datatype corresponds to a co-datatype */ - public boolean isCodatatype() - { - return isCodatatype(pointer); - } - - private native boolean isCodatatype(long pointer); - - /** @return true if this datatype corresponds to a tuple */ - public boolean isTuple() - { - return isTuple(pointer); - } - - private native boolean isTuple(long pointer); - - /** @return true if this datatype corresponds to a record */ - public boolean isRecord() - { - return isRecord(pointer); - } - - private native boolean isRecord(long pointer); - - /** @return true if this datatype is finite */ - public boolean isFinite() - { - return isFinite(pointer); - } - - private native boolean isFinite(long pointer); - - /** - * Is this datatype well-founded? If this datatype is not a codatatype, - * this returns false if there are no values of this datatype that are of - * finite size. - * - * @return true if this datatype is well-founded - */ - public boolean isWellFounded() - { - return isWellFounded(pointer); - } - - private native boolean isWellFounded(long pointer); - - /** - * Does this datatype have nested recursion? This method returns false if a - * value of this datatype includes a subterm of its type that is nested - * beneath a non-datatype type constructor. For example, a datatype - * T containing a constructor having a selector with range type (Set T) has - * nested recursion. - * - * @return true if this datatype has nested recursion - */ - public boolean hasNestedRecursion() - { - return hasNestedRecursion(pointer); - } - - private native boolean hasNestedRecursion(long pointer); - - /** - * @return true if this Datatype is a null object - */ - public boolean isNull() - { - return isNull(pointer); - } - - private native boolean isNull(long pointer); - - /** - * @return a string representation of this datatype - */ - protected native String toString(long pointer); - - public class ConstIterator implements Iterator - { - private int currentIndex; - private int size; - - public ConstIterator() - { - currentIndex = -1; - size = getNumConstructors(); - } - - @Override public boolean hasNext() - { - return currentIndex < size - 1; - } - - @Override public DatatypeConstructor next() - { - if (currentIndex >= size - 1) - { - throw new NoSuchElementException(); - } - currentIndex++; - - return getConstructor(currentIndex); - } - } - - @Override public Iterator iterator() - { - return new ConstIterator(); - } -} diff --git a/src/api/java/cvc5/DatatypeConstructor.java b/src/api/java/cvc5/DatatypeConstructor.java deleted file mode 100644 index 7c0ee21d5..000000000 --- a/src/api/java/cvc5/DatatypeConstructor.java +++ /dev/null @@ -1,197 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -import java.util.Iterator; -import java.util.NoSuchElementException; - -public class DatatypeConstructor extends AbstractPointer implements Iterable -{ - // region construction and destruction - DatatypeConstructor(Solver solver, long pointer) - { - super(solver, pointer); - } - - protected static native void deletePointer(long pointer); - - public long getPointer() - { - return pointer; - } - - @Override public void finalize() - { - deletePointer(pointer); - } - - // endregion - - /** @return the name of this Datatype constructor. */ - public String getName() - { - return getName(pointer); - } - - private native String getName(long pointer); - - /** - * Get the constructor operator of this datatype constructor. - * @return the constructor term - */ - public Term getConstructorTerm() - { - long termPointer = getConstructorTerm(pointer); - return new Term(solver, termPointer); - } - - private native long getConstructorTerm(long pointer); - - /** - * Get the constructor operator of this datatype constructor whose return - * type is retSort. This method is intended to be used on constructors of - * parametric datatypes and can be seen as returning the constructor - * term that has been explicitly cast to the given sort. - * - * This method is required for constructors of parametric datatypes whose - * return type cannot be determined by type inference. For example, given: - * (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T)))))) - * The type of nil terms need to be provided by the user. In SMT version 2.6, - * this is done via the syntax for qualified identifiers: - * (as nil (List Int)) - * This method is equivalent of applying the above, where this - * DatatypeConstructor is the one corresponding to nil, and retSort is - * (List Int). - * - * Furthermore note that the returned constructor term t is an operator, - * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above - * (nullary) application of nil. - * - * @param retSort the desired return sort of the constructor - * @return the constructor term - */ - public Term getSpecializedConstructorTerm(Sort retSort) - { - long termPointer = getSpecializedConstructorTerm(pointer, retSort.getPointer()); - return new Term(solver, termPointer); - } - - private native long getSpecializedConstructorTerm(long pointer, long retSortPointer); - - /** - * Get the tester operator of this datatype constructor. - * @return the tester operator - */ - public Term getTesterTerm() - { - long termPointer = getTesterTerm(pointer); - return new Term(solver, termPointer); - } - private native long getTesterTerm(long pointer); - - /** - * @return the number of selectors (so far) of this Datatype constructor. - */ - public int getNumSelectors() - { - return getNumSelectors(pointer); - } - private native int getNumSelectors(long pointer); - - /** @return the i^th DatatypeSelector. */ - public DatatypeSelector getSelector(int index) - { - long selectorPointer = getSelector(pointer, index); - return new DatatypeSelector(solver, selectorPointer); - } - private native long getSelector(long pointer, int index); - - /** - * Get the datatype selector with the given name. - * This is a linear search through the selectors, so in case of - * multiple, similarly-named selectors, the first is returned. - * @param name the name of the datatype selector - * @return the first datatype selector with the given name - */ - public DatatypeSelector getSelector(String name) - { - long selectorPointer = getSelector(pointer, name); - return new DatatypeSelector(solver, selectorPointer); - } - private native long getSelector(long pointer, String name); - - /** - * Get the term representation of the datatype selector with the given name. - * This is a linear search through the arguments, so in case of multiple, - * similarly-named arguments, the selector for the first is returned. - * @param name the name of the datatype selector - * @return a term representing the datatype selector with the given name - */ - public Term getSelectorTerm(String name) - { - long termPointer = getSelectorTerm(pointer, name); - return new Term(solver, termPointer); - } - private native long getSelectorTerm(long pointer, String name); - - /** - * @return true if this DatatypeConstructor is a null object - */ - public boolean isNull() - { - return isNull(pointer); - } - - private native boolean isNull(long pointer); - - /** - * @return a string representation of this datatype constructor - */ - protected native String toString(long pointer); - - public class ConstIterator implements Iterator - { - private int currentIndex; - private int size; - - public ConstIterator() - { - currentIndex = -1; - size = getNumSelectors(); - } - - @Override public boolean hasNext() - { - return currentIndex < size - 1; - } - - @Override public DatatypeSelector next() - { - if (currentIndex >= size - 1) - { - throw new NoSuchElementException(); - } - currentIndex++; - - return getSelector(currentIndex); - } - } - - @Override public Iterator iterator() - { - return new ConstIterator(); - } -} diff --git a/src/api/java/cvc5/DatatypeConstructorDecl.java b/src/api/java/cvc5/DatatypeConstructorDecl.java deleted file mode 100644 index 9769aa2fb..000000000 --- a/src/api/java/cvc5/DatatypeConstructorDecl.java +++ /dev/null @@ -1,77 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -public class DatatypeConstructorDecl extends AbstractPointer -{ - // region construction and destruction - DatatypeConstructorDecl(Solver solver, long pointer) - { - super(solver, pointer); - } - - protected static native void deletePointer(long pointer); - - public long getPointer() - { - return pointer; - } - - @Override public void finalize() - { - deletePointer(pointer); - } - - // endregion - - /** - * Add datatype selector declaration. - * @param name the name of the datatype selector declaration to add - * @param sort the range sort of the datatype selector declaration to add - */ - public void addSelector(String name, Sort sort) - { - addSelector(pointer, name, sort.getPointer()); - } - - private native void addSelector(long pointer, String name, long sortPointer); - - /** - * Add datatype selector declaration whose range type is the datatype itself. - * @param name the name of the datatype selector declaration to add - */ - public void addSelectorSelf(String name) - { - addSelectorSelf(pointer, name); - } - - private native void addSelectorSelf(long pointer, String name); - - /** - * @return true if this DatatypeConstructorDecl is a null declaration. - */ - public boolean isNull() - { - return isNull(pointer); - } - - private native boolean isNull(long pointer); - - /** - * @return a string representation of this datatype constructor declaration - */ - protected native String toString(long pointer); -} diff --git a/src/api/java/cvc5/DatatypeDecl.java b/src/api/java/cvc5/DatatypeDecl.java deleted file mode 100644 index fa78c68ac..000000000 --- a/src/api/java/cvc5/DatatypeDecl.java +++ /dev/null @@ -1,88 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -public class DatatypeDecl extends AbstractPointer -{ - // region construction and destruction - DatatypeDecl(Solver solver, long pointer) - { - super(solver, pointer); - } - - protected static native void deletePointer(long pointer); - - public long getPointer() - { - return pointer; - } - - @Override public void finalize() - { - deletePointer(pointer); - } - - // endregion - /** - * Add datatype constructor declaration. - * @param ctor the datatype constructor declaration to add - */ - public void addConstructor(DatatypeConstructorDecl ctor) - { - addConstructor(pointer, ctor.getPointer()); - } - - private native void addConstructor(long pointer, long declPointer); - - /** Get the number of constructors (so far) for this Datatype declaration. */ - int getNumConstructors() - { - return getNumConstructors(pointer); - } - - private native int getNumConstructors(long pointer); - - /** Is this Datatype declaration parametric? */ - public boolean isParametric() - { - return isParametric(pointer); - } - - private native boolean isParametric(long pointer); - - /** - * @return true if this DatatypeDecl is a null object - */ - public boolean isNull() - { - return isNull(pointer); - } - - private native boolean isNull(long pointer); - - /** - * @return a string representation of this datatype declaration - */ - protected native String toString(long pointer); - - /** @return the name of this datatype declaration. */ - public String getName() - { - return getName(pointer); - } - - private native String getName(long pointer); -} diff --git a/src/api/java/cvc5/DatatypeSelector.java b/src/api/java/cvc5/DatatypeSelector.java deleted file mode 100644 index 014c35de0..000000000 --- a/src/api/java/cvc5/DatatypeSelector.java +++ /dev/null @@ -1,95 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -public class DatatypeSelector extends AbstractPointer -{ - // region construction and destruction - DatatypeSelector(Solver solver, long pointer) - { - super(solver, pointer); - } - - protected static native void deletePointer(long pointer); - - public long getPointer() - { - return pointer; - } - - @Override public void finalize() - { - deletePointer(pointer); - } - - // endregion - - /** @return the name of this Datatype selector. */ - String getName() - { - return getName(pointer); - } - - private native String getName(long pointer); - - /** - * Get the selector operator of this datatype selector. - * @return the selector term - */ - public Term getSelectorTerm() - { - long termPointer = getSelectorTerm(pointer); - return new Term(solver, termPointer); - } - - private native long getSelectorTerm(long pointer); - - /** - * Get the upater operator of this datatype selector. - * @return the updater term - */ - public Term getUpdaterTerm() - { - long termPointer = getUpdaterTerm(pointer); - return new Term(solver, termPointer); - } - - private native long getUpdaterTerm(long pointer); - - /** @return the range sort of this selector. */ - Sort getRangeSort() - { - long sortPointer = getRangeSort(pointer); - return new Sort(solver, sortPointer); - } - - private native long getRangeSort(long pointer); - - /** - * @return true if this DatatypeSelector is a null object - */ - public boolean isNull() - { - return isNull(pointer); - } - - private native boolean isNull(long pointer); - - /** - * @return a string representation of this datatype selector - */ - protected native String toString(long pointer); -} diff --git a/src/api/java/cvc5/Grammar.java b/src/api/java/cvc5/Grammar.java deleted file mode 100644 index b9240a621..000000000 --- a/src/api/java/cvc5/Grammar.java +++ /dev/null @@ -1,99 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -public class Grammar extends AbstractPointer -{ - // region construction and destruction - Grammar(Solver solver, long pointer) - { - super(solver, pointer); - } - - public Grammar(Grammar grammar) - { - super(grammar.solver, copyGrammar(grammar.pointer)); - } - - private static native long copyGrammar(long pointer); - - protected static native void deletePointer(long pointer); - - public long getPointer() - { - return pointer; - } - - @Override public void finalize() - { - deletePointer(pointer); - } - - // endregion - - /** - * Add \p rule to the set of rules corresponding to \p ntSymbol. - * @param ntSymbol the non-terminal to which the rule is added - * @param rule the rule to add - */ - public void addRule(Term ntSymbol, Term rule) - { - addRule(pointer, ntSymbol.getPointer(), rule.getPointer()); - } - - private native void addRule(long pointer, long ntSymbolPointer, long rulePointer); - - /** - * Add \p rules to the set of rules corresponding to \p ntSymbol. - * @param ntSymbol the non-terminal to which the rules are added - * @param rules the rules to add - */ - public void addRules(Term ntSymbol, Term[] rules) - { - long[] pointers = Utils.getPointers(rules); - addRules(pointer, ntSymbol.getPointer(), pointers); - } - - public native void addRules(long pointer, long ntSymbolPointer, long[] rulePointers); - - /** - * Allow \p ntSymbol to be an arbitrary constant. - * @param ntSymbol the non-terminal allowed to be any constant - */ - public void addAnyConstant(Term ntSymbol) - { - addAnyConstant(pointer, ntSymbol.getPointer()); - } - - private native void addAnyConstant(long pointer, long ntSymbolPointer); - - /** - * Allow \p ntSymbol to be any input variable to corresponding - * synth-fun/synth-inv with the same sort as \p ntSymbol. - * @param ntSymbol the non-terminal allowed to be any input constant - */ - public void addAnyVariable(Term ntSymbol) - { - addAnyVariable(pointer, ntSymbol.getPointer()); - } - - private native void addAnyVariable(long pointer, long ntSymbolPointer); - - /** - * @return a string representation of this grammar. - */ - protected native String toString(long pointer); -} diff --git a/src/api/java/cvc5/IPointer.java b/src/api/java/cvc5/IPointer.java deleted file mode 100644 index 17d6d5974..000000000 --- a/src/api/java/cvc5/IPointer.java +++ /dev/null @@ -1,20 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -interface IPointer { - long getPointer(); -} diff --git a/src/api/java/cvc5/Op.java b/src/api/java/cvc5/Op.java deleted file mode 100644 index bf908aff2..000000000 --- a/src/api/java/cvc5/Op.java +++ /dev/null @@ -1,137 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -public class Op extends AbstractPointer -{ - // region construction and destruction - Op(Solver solver, long pointer) - { - super(solver, pointer); - } - - protected static native void deletePointer(long pointer); - - public long getPointer() - { - return pointer; - } - - @Override public void finalize() - { - deletePointer(pointer); - } - - // endregion - - /** - * Syntactic equality operator. - * Return true if both operators are syntactically identical. - * Both operators must belong to the same solver object. - * @param t the operator to compare to for equality - * @return true if the operators are equal - */ - @Override public boolean equals(Object t) - { - if (this == t) - return true; - if (t == null || getClass() != t.getClass()) - return false; - return equals(pointer, ((Op) t).getPointer()); - } - - private native boolean equals(long pointer1, long pointer2); - - /** - * @return the kind of this operator - */ - public Kind getKind() - { - try - { - int value = getKind(pointer); - return Kind.fromInt(value); - } - catch (CVC5ApiException e) - { - e.printStackTrace(); - throw new RuntimeException(e.getMessage()); - } - } - - private native int getKind(long pointer); - - /** - * @return true if this operator is a null term - */ - public boolean isNull() - { - return isNull(pointer); - } - - private native boolean isNull(long pointer); - - /** - * @return true iff this operator is indexed - */ - public boolean isIndexed() - { - return isIndexed(pointer); - } - - private native boolean isIndexed(long pointer); - - /** - * @return the number of indices of this op - */ - public int getNumIndices() - { - return getNumIndices(pointer); - } - - private native int getNumIndices(long pointer); - - /** - * Get the indices used to create this Op. - * Check the Op Kind with getKind() to determine which argument to use. - * - * @return the indices used to create this Op - */ - public int[] getIntegerIndices() - { - return getIntegerIndices(pointer); - } - - private native int[] getIntegerIndices(long pointer); - - /** - * Get the indices used to create this Op. - * Check the Op Kind with getKind() to determine which argument to use. - * - * @return the indices used to create this Op - */ - public String[] getStringIndices() - { - return getStringIndices(pointer); - } - - private native String[] getStringIndices(long pointer); - - /** - * @return a string representation of this operator - */ - protected native String toString(long pointer); -} diff --git a/src/api/java/cvc5/OptionInfo.java b/src/api/java/cvc5/OptionInfo.java deleted file mode 100644 index 7690a1bc1..000000000 --- a/src/api/java/cvc5/OptionInfo.java +++ /dev/null @@ -1,209 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Gereon Kremer, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -import java.math.BigInteger; - -/** - * Holds some description about a particular option, including its name, its - * aliases, whether the option was explicitly set by the user, and information - * concerning its value. The `valueInfo` member holds any of the following - * alternatives: - * - VoidInfo if the option holds no value (or the value has no native type) - * - ValueInfo if the option is of type boolean or String, holds the - * current value and the default value. - * - NumberInfo if the option is of type BigInteger or double, holds - * the current and default value, as well as the minimum and maximum. - * - ModeInfo if the option is a mode option, holds the current and default - * values, as well as a list of valid modes. - * Additionally, this class provides convenience functions to obtain the - * current value of an option in a type-safe manner using boolValue(), - * stringValue(), intValue(), and doubleValue(). They assert that - * the option has the respective type and return the current value. - */ -public class OptionInfo extends AbstractPointer -{ - // region construction and destruction - OptionInfo(Solver solver, long pointer) - { - super(solver, pointer); - this.name = getName(pointer); - this.aliases = getAliases(pointer); - this.setByUser = getSetByUser(pointer); - this.baseInfo = getBaseInfo(pointer); - } - - protected static native void deletePointer(long pointer); - - public long getPointer() - { - return pointer; - } - - @Override public void finalize() - { - deletePointer(pointer); - } - - /** - * @return a string representation of this optionInfo. - */ - protected native String toString(long pointer); - - // endregion - - /** Abstract class for OptionInfo values */ - abstract class BaseInfo - { - } - - /** Has the current and the default value */ - public abstract class ValueInfo extends BaseInfo - { - private final T defaultValue; - private final T currentValue; - public ValueInfo(T defaultValue, T currentValue) - { - this.defaultValue = defaultValue; - this.currentValue = currentValue; - } - public T getDefaultValue() - { - return defaultValue; - } - public T getCurrentValue() - { - return currentValue; - } - } - - public class ModeInfo extends ValueInfo - { - private final String[] modes; - - public ModeInfo(String defaultValue, String currentValue, String[] modes) - { - super(defaultValue, currentValue); - this.modes = modes; - } - public String[] getModes() - { - return modes; - } - } - - /** Has no value information */ - public class VoidInfo extends BaseInfo - { - } - - /** Default value, current value, minimum and maximum of a numeric value */ - public class NumberInfo extends ValueInfo - { - private final T minimum; - private final T maximum; - public NumberInfo(T defaultValue, T currentValue, T minimum, T maximum) - { - super(defaultValue, currentValue); - this.minimum = minimum; - this.maximum = maximum; - } - public T getMinimum() - { - return minimum; - } - public T getMaximum() - { - return maximum; - } - } - - private native String getName(long pointer); - - private native String[] getAliases(long pointer); - - private native boolean getSetByUser(long pointer); - - private native BaseInfo getBaseInfo(long pointer); - - /** The option name */ - private final String name; - public String getName() - { - return name; - } - /** The option name aliases */ - private final String[] aliases; - public String[] getAliases() - { - return aliases; - } - /** Whether the option was explicitly set by the user */ - private final boolean setByUser; - public boolean getSetByUser() - { - return setByUser; - } - - /** The option variant information */ - private final BaseInfo baseInfo; - public BaseInfo getBaseInfo() - { - return baseInfo; - } - - /** - * Obtain the current value as a boolean. Asserts that valueInfo holds a boolean. - */ - public boolean booleanValue() - { - return booleanValue(pointer); - } - - private native boolean booleanValue(long pointer); - - /** - * Obtain the current value as a string. Asserts that valueInfo holds a - * string. - */ - public String stringValue() - { - return stringValue(pointer); - } - - private native String stringValue(long pointer); - - /** - * Obtain the current value as as int. Asserts that valueInfo holds an int. - */ - public BigInteger intValue() - { - return intValue(pointer); - } - - private native BigInteger intValue(long pointer); - - /** - * Obtain the current value as a double. Asserts that valueInfo holds a - * double. - */ - public double doubleValue() - { - return doubleValue(pointer); - } - - private native double doubleValue(long pointer); -}; diff --git a/src/api/java/cvc5/Pair.java b/src/api/java/cvc5/Pair.java deleted file mode 100644 index 84c9d8efe..000000000 --- a/src/api/java/cvc5/Pair.java +++ /dev/null @@ -1,39 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -public class Pair -{ - public K first; - public V second; - public Pair(K first, V second) - { - this.first = first; - this.second = second; - } - - @Override public boolean equals(Object pair) - { - if (this == pair) - return true; - if (pair == null || getClass() != pair.getClass()) - return false; - - Pair p = (Pair) pair; - - return first.equals(p.first) && second.equals(p.second); - } -} diff --git a/src/api/java/cvc5/Result.java b/src/api/java/cvc5/Result.java deleted file mode 100644 index 3573094a3..000000000 --- a/src/api/java/cvc5/Result.java +++ /dev/null @@ -1,208 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -import java.util.HashMap; -import java.util.Map; - -public class Result extends AbstractPointer -{ - // region construction and destruction - Result(Solver solver, long pointer) - { - super(solver, pointer); - } - - protected static native void deletePointer(long pointer); - - public long getPointer() - { - return pointer; - } - - @Override public void finalize() - { - deletePointer(pointer); - } - - // endregion - - public enum UnknownExplanation { - REQUIRES_FULL_CHECK(0), - INCOMPLETE(1), - TIMEOUT(2), - RESOURCEOUT(3), - MEMOUT(4), - INTERRUPTED(5), - NO_STATUS(6), - UNSUPPORTED(7), - OTHER(8), - UNKNOWN_REASON(9); - - /* the int value of the UnknownExplanation */ - private int value; - private static Map explanationMap = new HashMap<>(); - private UnknownExplanation(int value) - { - this.value = value; - } - - static - { - for (UnknownExplanation explanation : UnknownExplanation.values()) - { - explanationMap.put(explanation.getValue(), explanation); - } - } - - public static UnknownExplanation fromInt(int value) throws CVC5ApiException - { - if (value < REQUIRES_FULL_CHECK.value || value > UNKNOWN_REASON.value) - { - throw new CVC5ApiException("UnknownExplanation value " + value - + " is outside the valid range [" + REQUIRES_FULL_CHECK.value + "," - + UNKNOWN_REASON.value + "]"); - } - return explanationMap.get(value); - } - - public int getValue() - { - return value; - } - } - - /** - * Return true if Result is empty, i.e., a nullary Result, and not an actual - * result returned from a checkSat() (and friends) query. - */ - public boolean isNull() - { - return isNull(pointer); - } - - private native boolean isNull(long pointer); - - /** - * Return true if query was a satisfiable checkSat() or checkSatAssuming() - * query. - */ - public boolean isSat() - { - return isSat(pointer); - } - - private native boolean isSat(long pointer); - - /** - * Return true if query was an unsatisfiable checkSat() or - * checkSatAssuming() query. - */ - public boolean isUnsat() - { - return isUnsat(pointer); - } - - private native boolean isUnsat(long pointer); - - /** - * Return true if query was a checkSat() or checkSatAssuming() query and - * cvc5 was not able to determine (un)satisfiability. - */ - public boolean isSatUnknown() - { - return isSatUnknown(pointer); - } - - private native boolean isSatUnknown(long pointer); - - /** - * Return true if corresponding query was an entailed checkEntailed() query. - */ - public boolean isEntailed() - { - return isEntailed(pointer); - } - - private native boolean isEntailed(long pointer); - - /** - * Return true if corresponding query was a checkEntailed() query that is - * not entailed. - */ - public boolean isNotEntailed() - { - return isNotEntailed(pointer); - } - - private native boolean isNotEntailed(long pointer); - - /** - * Return true if query was a checkEntailed() query and cvc5 was not able to - * determine if it is entailed. - */ - public boolean isEntailmentUnknown() - { - return isEntailmentUnknown(pointer); - } - - private native boolean isEntailmentUnknown(long pointer); - - /** - * Operator overloading for equality of two results. - * @param r the result to compare to for equality - * @return true if the results are equal - */ - @Override public boolean equals(Object r) - { - if (this == r) - return true; - if (r == null || getClass() != r.getClass()) - return false; - Result result = (Result) r; - if (this.pointer == result.pointer) - { - return true; - } - return equals(pointer, result.getPointer()); - } - - private native boolean equals(long pointer1, long pointer2); - - /** - * @return an explanation for an unknown query result. - */ - public UnknownExplanation getUnknownExplanation() - { - try - { - int explanation = getUnknownExplanation(pointer); - return UnknownExplanation.fromInt(explanation); - } - catch (CVC5ApiException e) - { - e.printStackTrace(); - throw new RuntimeException(e.getMessage()); - } - } - - private native int getUnknownExplanation(long pointer); - - /** - * @return a string representation of this result. - */ - protected native String toString(long pointer); -} diff --git a/src/api/java/cvc5/RoundingMode.java b/src/api/java/cvc5/RoundingMode.java deleted file mode 100644 index 4229bb74a..000000000 --- a/src/api/java/cvc5/RoundingMode.java +++ /dev/null @@ -1,63 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -public enum RoundingMode { - /** - * Round to the nearest even number. - * If the two nearest floating-point numbers bracketing an unrepresentable - * infinitely precise result are equally near, the one with an even least - * significant digit will be delivered. - */ - ROUND_NEAREST_TIES_TO_EVEN(0), - /** - * Round towards positive infinity (+oo). - * The result shall be the format’s floating-point number (possibly +oo) - * closest to and no less than the infinitely precise result. - */ - ROUND_TOWARD_POSITIVE(1), - /** - * Round towards negative infinity (-oo). - * The result shall be the format’s floating-point number (possibly -oo) - * closest to and no less than the infinitely precise result. - */ - ROUND_TOWARD_NEGATIVE(2), - /** - * Round towards zero. - * The result shall be the format’s floating-point number closest to and no - * greater in magnitude than the infinitely precise result. - */ - ROUND_TOWARD_ZERO(3), - /** - * Round to the nearest number away from zero. - * If the two nearest floating-point numbers bracketing an unrepresentable - * infinitely precise result are equally near, the one with larger magnitude - * will be selected. - */ - ROUND_NEAREST_TIES_TO_AWAY(4); - - private int value; - - private RoundingMode(int value) - { - this.value = value; - } - - public int getValue() - { - return value; - } -} diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java deleted file mode 100644 index cc5797570..000000000 --- a/src/api/java/cvc5/Solver.java +++ /dev/null @@ -1,2654 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * The cvc5 java API. - */ - -package cvc5; - -import java.io.IOException; -import java.util.*; - -public class Solver implements IPointer -{ - private final long pointer; - - public long getPointer() - { - return pointer; - } - - private native long newSolver(); - - public void deletePointer() - { - deletePointer(pointer); - } - - private static native void deletePointer(long pointer); - - @Override public void finalize() - { - deletePointer(pointer); - } - - static - { - Utils.loadLibraries(); - } - - /* .................................................................... */ - /* Constructors */ - /* .................................................................... */ - - public Solver() - { - this.pointer = newSolver(); - } - - /* .................................................................... */ - /* Sorts Handling */ - /* .................................................................... */ - - /** - * @return sort null - */ - - public Sort getNullSort() - { - long sortPointer = getNullSort(pointer); - return new Sort(this, sortPointer); - } - - private native long getNullSort(long pointer); - - /** - * @return sort Boolean - */ - public Sort getBooleanSort() - { - long sortPointer = getBooleanSort(pointer); - return new Sort(this, sortPointer); - } - - private native long getBooleanSort(long pointer); - - /** - * @return sort Integer (in cvc5, Integer is a subtype of Real) - */ - public Sort getIntegerSort() - { - long sortPointer = getIntegerSort(pointer); - return new Sort(this, sortPointer); - } - - public native long getIntegerSort(long pointer); - /** - * @return sort Real - */ - public Sort getRealSort() - { - long sortPointer = getRealSort(pointer); - return new Sort(this, sortPointer); - } - - private native long getRealSort(long pointer); - /** - * @return sort RegExp - */ - public Sort getRegExpSort() - { - long sortPointer = getRegExpSort(pointer); - return new Sort(this, sortPointer); - } - - private native long getRegExpSort(long pointer); - /** - * @return sort RoundingMode - */ - public Sort getRoundingModeSort() throws CVC5ApiException - { - long sortPointer = getRoundingModeSort(pointer); - return new Sort(this, sortPointer); - } - - private native long getRoundingModeSort(long pointer) throws CVC5ApiException; - /** - * @return sort String - */ - public Sort getStringSort() - { - long sortPointer = getStringSort(pointer); - return new Sort(this, sortPointer); - } - - private native long getStringSort(long solverPointer); - /** - * Create an array sort. - * @param indexSort the array index sort - * @param elemSort the array element sort - * @return the array sort - */ - public Sort mkArraySort(Sort indexSort, Sort elemSort) - { - long sortPointer = mkArraySort(pointer, indexSort.getPointer(), elemSort.getPointer()); - return new Sort(this, sortPointer); - } - - private native long mkArraySort(long pointer, long indexSortPointer, long elementSortPointer); - - /** - * Create a bit-vector sort. - * @param size the bit-width of the bit-vector sort - * @return the bit-vector sort - */ - public Sort mkBitVectorSort(int size) throws CVC5ApiException - { - Utils.validateUnsigned(size, "size"); - long sortPointer = mkBitVectorSort(pointer, size); - return new Sort(this, sortPointer); - } - - private native long mkBitVectorSort(long pointer, int size); - - /** - * Create a floating-point sort. - * @param exp the bit-width of the exponent of the floating-point sort. - * @param sig the bit-width of the significand of the floating-point sort. - */ - public Sort mkFloatingPointSort(int exp, int sig) throws CVC5ApiException - { - Utils.validateUnsigned(exp, "exp"); - Utils.validateUnsigned(sig, "sig"); - long sortPointer = mkFloatingPointSort(pointer, exp, sig); - return new Sort(this, sortPointer); - } - - private native long mkFloatingPointSort(long solverPointer, int exp, int sig); - - /** - * Create a datatype sort. - * @param dtypedecl the datatype declaration from which the sort is - * created - * @return the datatype sort - */ - public Sort mkDatatypeSort(DatatypeDecl dtypedecl) throws CVC5ApiException - { - long pointer = mkDatatypeSort(this.pointer, dtypedecl.getPointer()); - return new Sort(this, pointer); - } - - private native long mkDatatypeSort(long pointer, long datatypeDeclPointer) - throws CVC5ApiException; - - /** - * Create a vector of datatype sorts. The names of the datatype - * declarations must be distinct. - * - * @param dtypedecls the datatype declarations from which the sort is - * created - * @return the datatype sorts - */ - public Sort[] mkDatatypeSorts(List dtypedecls) throws CVC5ApiException - { - return mkDatatypeSorts(dtypedecls.toArray(new DatatypeDecl[0])); - } - - /** - * Create a vector of datatype sorts. The names of the datatype - * declarations must be distinct. - * - * @param dtypedecls the datatype declarations from which the sort is - * created - * @return the datatype sorts - */ - public Sort[] mkDatatypeSorts(DatatypeDecl[] dtypedecls) throws CVC5ApiException - { - long[] declPointers = Utils.getPointers(dtypedecls); - long[] sortPointers = mkDatatypeSorts(pointer, declPointers); - Sort[] sorts = Utils.getSorts(this, sortPointers); - return sorts; - } - - private native long[] mkDatatypeSorts(long pointer, long[] declPointers) throws CVC5ApiException; - - /** - * Create a vector of datatype sorts using unresolved sorts. The names of - * the datatype declarations in dtypedecls must be distinct. - * - * This method is called when the DatatypeDecl objects dtypedecls have - * been built using "unresolved" sorts. - * - * We associate each sort in unresolvedSorts with exacly one datatype from - * dtypedecls. In particular, it must have the same name as exactly one - * datatype declaration in dtypedecls. - * - * When constructing datatypes, unresolved sorts are replaced by the - * datatype sort constructed for the datatype declaration it is associated - * with. - * - * @param dtypedecls the datatype declarations from which the sort is - * created - * @param unresolvedSorts the set of unresolved sorts - * @return the datatype sorts - */ - public List mkDatatypeSorts(List dtypedecls, Set unresolvedSorts) - throws CVC5ApiException - { - Sort[] array = mkDatatypeSorts( - dtypedecls.toArray(new DatatypeDecl[0]), unresolvedSorts.toArray(new Sort[0])); - return Arrays.asList(array); - } - - /** - * Create a vector of datatype sorts using unresolved sorts. The names of - * the datatype declarations in dtypedecls must be distinct. - * - * This method is called when the DatatypeDecl objects dtypedecls have - * been built using "unresolved" sorts. - * - * We associate each sort in unresolvedSorts with exacly one datatype from - * dtypedecls. In particular, it must have the same name as exactly one - * datatype declaration in dtypedecls. - * - * When constructing datatypes, unresolved sorts are replaced by the - * datatype sort constructed for the datatype declaration it is associated - * with. - * - * @param dtypedecls the datatype declarations from which the sort is - * created - * @param unresolvedSorts the list of unresolved sorts - * @return the datatype sorts - */ - public Sort[] mkDatatypeSorts(DatatypeDecl[] dtypedecls, Sort[] unresolvedSorts) - throws CVC5ApiException - { - long[] declPointers = Utils.getPointers(dtypedecls); - long[] unresolvedPointers = Utils.getPointers(unresolvedSorts); - long[] sortPointers = mkDatatypeSorts(pointer, declPointers, unresolvedPointers); - Sort[] sorts = Utils.getSorts(this, sortPointers); - return sorts; - } - - private native long[] mkDatatypeSorts( - long pointer, long[] declPointers, long[] unresolvedPointers) throws CVC5ApiException; - - /** - * Create function sort. - * @param domain the sort of the fuction argument - * @param codomain the sort of the function return value - * @return the function sort - */ - public Sort mkFunctionSort(Sort domain, Sort codomain) - { - long sortPointer = mkFunctionSort(pointer, domain.getPointer(), codomain.getPointer()); - return new Sort(this, sortPointer); - } - - private native long mkFunctionSort(long pointer, long domainPointer, long codomainPointer); - - /** - * Create function sort. - * @param sorts the sort of the function arguments - * @param codomain the sort of the function return value - * @return the function sort - */ - public Sort mkFunctionSort(Sort[] sorts, Sort codomain) - { - long sortPointer = mkFunctionSort(pointer, Utils.getPointers(sorts), codomain.getPointer()); - return new Sort(this, sortPointer); - } - - private native long mkFunctionSort(long pointer, long[] sortPointers, long codomainPointer); - - /** - * Create a sort parameter. - * @param symbol the name of the sort - * @return the sort parameter - */ - public Sort mkParamSort(String symbol) - { - long sortPointer = mkParamSort(pointer, symbol); - return new Sort(this, sortPointer); - } - - private native long mkParamSort(long pointer, String symbol); - - /** - * Create a predicate sort. - * @param sorts the list of sorts of the predicate - * @return the predicate sort - */ - public Sort mkPredicateSort(Sort[] sorts) - { - long sortPointer = mkPredicateSort(pointer, Utils.getPointers(sorts)); - return new Sort(this, sortPointer); - } - - private native long mkPredicateSort(long pointer, long[] sortPointers); - - /** - * Create a record sort - * @param fields the list of fields of the record - * @return the record sort - */ - public Sort mkRecordSort(Pair[] fields) - { - long sortPointer = mkRecordSort(pointer, Utils.getPairs(fields)); - return new Sort(this, sortPointer); - } - - private native long mkRecordSort(long pointer, Pair[] fields); - - /** - * Create a set sort. - * @param elemSort the sort of the set elements - * @return the set sort - */ - public Sort mkSetSort(Sort elemSort) - { - long sortPointer = mkSetSort(pointer, elemSort.getPointer()); - return new Sort(this, sortPointer); - } - - private native long mkSetSort(long pointer, long elemSortPointer); - /** - * Create a bag sort. - * @param elemSort the sort of the bag elements - * @return the bag sort - */ - public Sort mkBagSort(Sort elemSort) - { - long sortPointer = mkBagSort(pointer, elemSort.getPointer()); - return new Sort(this, sortPointer); - } - - private native long mkBagSort(long pointer, long elemSortPointer); - - /** - * Create a sequence sort. - * @param elemSort the sort of the sequence elements - * @return the sequence sort - */ - public Sort mkSequenceSort(Sort elemSort) - { - long sortPointer = mkSequenceSort(pointer, elemSort.getPointer()); - return new Sort(this, sortPointer); - } - - private native long mkSequenceSort(long pointer, long elemSortPointer); - - /** - * Create an uninterpreted sort. - * @param symbol the name of the sort - * @return the uninterpreted sort - */ - public Sort mkUninterpretedSort(String symbol) - { - long sortPointer = mkUninterpretedSort(pointer, symbol); - return new Sort(this, sortPointer); - } - - private native long mkUninterpretedSort(long pointer, String symbol); - - /** - * Create a sort constructor sort. - * @param symbol the symbol of the sort - * @param arity the arity of the sort - * @return the sort constructor sort - */ - public Sort mkSortConstructorSort(String symbol, int arity) throws CVC5ApiException - { - Utils.validateUnsigned(arity, "arity"); - long sortPointer = mkSortConstructorSort(pointer, symbol, arity); - return new Sort(this, sortPointer); - } - - private native long mkSortConstructorSort(long pointer, String symbol, int arity); - - /** - * Create a tuple sort. - * @param sorts of the elements of the tuple - * @return the tuple sort - */ - public Sort mkTupleSort(Sort[] sorts) - { - long[] sortPointers = Utils.getPointers(sorts); - long sortPointer = mkTupleSort(pointer, sortPointers); - return new Sort(this, sortPointer); - } - - private native long mkTupleSort(long pointer, long[] sortPointers); - - /* .................................................................... */ - /* Create Terms */ - /* .................................................................... */ - - /** - * Create 0-ary term of given kind. - * @param kind the kind of the term - * @return the Term - */ - public Term mkTerm(Kind kind) - { - long termPointer = mkTerm(pointer, kind.getValue()); - return new Term(this, termPointer); - } - - private native long mkTerm(long pointer, int kindValue); - - /** - * Create a unary term of given kind. - * @param kind the kind of the term - * @param child the child of the term - * @return the Term - */ - public Term mkTerm(Kind kind, Term child) - { - long termPointer = mkTerm(pointer, kind.getValue(), child.getPointer()); - return new Term(this, termPointer); - } - - private native long mkTerm(long pointer, int kindValue, long childPointer); - - /** - * Create binary term of given kind. - * @param kind the kind of the term - * @param child1 the first child of the term - * @param child2 the second child of the term - * @return the Term - */ - public Term mkTerm(Kind kind, Term child1, Term child2) - { - long termPointer = mkTerm(pointer, kind.getValue(), child1.getPointer(), child2.getPointer()); - return new Term(this, termPointer); - } - - private native long mkTerm(long pointer, int kindValue, long child1Pointer, long child2Pointer); - - /** - * Create ternary term of given kind. - * @param kind the kind of the term - * @param child1 the first child of the term - * @param child2 the second child of the term - * @param child3 the third child of the term - * @return the Term - */ - public Term mkTerm(Kind kind, Term child1, Term child2, Term child3) - { - long termPointer = mkTerm( - pointer, kind.getValue(), child1.getPointer(), child2.getPointer(), child3.getPointer()); - return new Term(this, termPointer); - } - - private native long mkTerm( - long pointer, int kindValue, long child1Pointer, long child2Pointer, long child3Pointer); - /** - * Create n-ary term of given kind. - * @param kind the kind of the term - * @param children the children of the term - * @return the Term - */ - public Term mkTerm(Kind kind, Term[] children) - { - long[] childPointers = Utils.getPointers(children); - long termPointer = mkTerm(pointer, kind.getValue(), childPointers); - return new Term(this, termPointer); - } - - private native long mkTerm(long pointer, int kindValue, long[] childrenPointers); - - /** - * Create nullary term of given kind from a given operator. - * Create operators with mkOp(). - * @param op the operator - * @return the Term - */ - public Term mkTerm(Op op) - { - long termPointer = mkTerm(pointer, op.getPointer()); - return new Term(this, termPointer); - } - - private native long mkTerm(long pointer, long opPointer); - /** - * Create unary term of given kind from a given operator. - * Create operators with mkOp(). - * @param op the operator - * @param child the child of the term - * @return the Term - */ - public Term mkTerm(Op op, Term child) - { - long termPointer = mkTerm(pointer, op.getPointer(), child.getPointer()); - return new Term(this, termPointer); - } - - private native long mkTerm(long pointer, long opPointer, long childPointer); - - /** - * Create binary term of given kind from a given operator. - * Create operators with mkOp(). - * @param op the operator - * @param child1 the first child of the term - * @param child2 the second child of the term - * @return the Term - */ - public Term mkTerm(Op op, Term child1, Term child2) - { - long termPointer = mkTerm(pointer, op.getPointer(), child1.getPointer(), child2.getPointer()); - return new Term(this, termPointer); - } - - private native long mkTerm(long pointer, long opPointer, long child1Pointer, long child2Pointer); - /** - * Create ternary term of given kind from a given operator. - * Create operators with mkOp(). - * @param op the operator - * @param child1 the first child of the term - * @param child2 the second child of the term - * @param child3 the third child of the term - * @return the Term - */ - public Term mkTerm(Op op, Term child1, Term child2, Term child3) - { - long termPointer = - mkTerm(op.getPointer(), child1.getPointer(), child2.getPointer(), child3.getPointer()); - return new Term(this, termPointer); - } - - private native long mkTerm( - long pointer, long opPointer, long child1Pointer, long child2Pointer, long child3Pointer); - - /** - * Create n-ary term of given kind from a given operator. - * Create operators with mkOp(). - * @param op the operator - * @param children the children of the term - * @return the Term - */ - public Term mkTerm(Op op, List children) - { - return mkTerm(op, children.toArray(new Term[0])); - } - - /** - * Create n-ary term of given kind from a given operator. - * Create operators with mkOp(). - * @param op the operator - * @param children the children of the term - * @return the Term - */ - public Term mkTerm(Op op, Term[] children) - { - long[] childPointers = Utils.getPointers(children); - long termPointer = mkTerm(pointer, op.getPointer(), childPointers); - return new Term(this, termPointer); - } - - private native long mkTerm(long pointer, long opPointer, long[] childrenPointers); - - /** - * Create a tuple term. Terms are automatically converted if sorts are - * compatible. - * @param sorts The sorts of the elements in the tuple - * @param terms The elements in the tuple - * @return the tuple Term - */ - public Term mkTuple(Sort[] sorts, Term[] terms) - { - long[] sortPointers = Utils.getPointers(sorts); - long[] termPointers = Utils.getPointers(terms); - long termPointer = mkTuple(pointer, sortPointers, termPointers); - return new Term(this, termPointer); - } - - private native long mkTuple(long pointer, long[] sortPointers, long[] termPointers); - - /* .................................................................... */ - /* Create Operators */ - /* .................................................................... */ - - /** - * Create an operator for a builtin Kind - * The Kind may not be the Kind for an indexed operator - * (e.g. BITVECTOR_EXTRACT) - * Note: in this case, the Op simply wraps the Kind. - * The Kind can be used in mkTerm directly without - * creating an op first. - * @param kind the kind to wrap - */ - public Op mkOp(Kind kind) - { - long opPointer = mkOp(pointer, kind.getValue()); - return new Op(this, opPointer); - } - - private native long mkOp(long pointer, int kindValue); - /** - * Create operator of kind: - * - RECORD_UPDATE - * - DIVISIBLE (to support arbitrary precision integers) - * See enum Kind for a description of the parameters. - * @param kind the kind of the operator - * @param arg the string argument to this operator - */ - public Op mkOp(Kind kind, String arg) - { - long opPointer = mkOp(pointer, kind.getValue(), arg); - return new Op(this, opPointer); - } - - private native long mkOp(long pointer, int kindValue, String arg); - - /** - * Create operator of kind: - * - DIVISIBLE - * - BITVECTOR_REPEAT - * - BITVECTOR_ZERO_EXTEND - * - BITVECTOR_SIGN_EXTEND - * - BITVECTOR_ROTATE_LEFT - * - BITVECTOR_ROTATE_RIGHT - * - INT_TO_BITVECTOR - * - FLOATINGPOINT_TO_UBV - * - FLOATINGPOINT_TO_UBV_TOTAL - * - FLOATINGPOINT_TO_SBV - * - FLOATINGPOINT_TO_SBV_TOTAL - * - TUPLE_UPDATE - * See enum Kind for a description of the parameters. - * @param kind the kind of the operator - * @param arg the unsigned int argument to this operator - */ - public Op mkOp(Kind kind, int arg) throws CVC5ApiException - { - Utils.validateUnsigned(arg, "arg"); - long opPointer = mkOp(pointer, kind.getValue(), arg); - return new Op(this, opPointer); - } - - private native long mkOp(long pointer, int kindValue, int arg); - - /** - * Create operator of Kind: - * - BITVECTOR_EXTRACT - * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR - * - FLOATINGPOINT_TO_FP_FLOATINGPOINT - * - FLOATINGPOINT_TO_FP_REAL - * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR - * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR - * - FLOATINGPOINT_TO_FP_GENERIC - * See enum Kind for a description of the parameters. - * @param kind the kind of the operator - * @param arg1 the first unsigned int argument to this operator - * @param arg2 the second unsigned int argument to this operator - */ - public Op mkOp(Kind kind, int arg1, int arg2) throws CVC5ApiException - { - Utils.validateUnsigned(arg1, "arg1"); - Utils.validateUnsigned(arg2, "arg2"); - long opPointer = mkOp(pointer, kind.getValue(), arg1, arg2); - return new Op(this, opPointer); - } - - private native long mkOp(long pointer, int kindValue, int arg1, int arg2); - - /** - * Create operator of Kind: - * - TUPLE_PROJECT - * See enum Kind for a description of the parameters. - * @param kind the kind of the operator - * @param args the arguments (indices) of the operator - */ - public Op mkOp(Kind kind, int[] args) throws CVC5ApiException - { - Utils.validateUnsigned(args, "args"); - long opPointer = mkOp(pointer, kind.getValue(), args); - return new Op(this, opPointer); - } - - private native long mkOp(long pointer, int kindValue, int[] args); - - /* .................................................................... */ - /* Create Constants */ - /* .................................................................... */ - - /** - * Create a Boolean true constant. - * @return the true constant - */ - public Term mkTrue() - { - long termPointer = mkTrue(pointer); - return new Term(this, termPointer); - } - - private native long mkTrue(long pointer); - /** - * Create a Boolean false constant. - * @return the false constant - */ - public Term mkFalse() - { - long termPointer = mkFalse(pointer); - return new Term(this, termPointer); - } - - private native long mkFalse(long pointer); - /** - * Create a Boolean constant. - * @return the Boolean constant - * @param val the value of the constant - */ - public Term mkBoolean(boolean val) - { - long termPointer = mkBoolean(pointer, val); - return new Term(this, termPointer); - } - - private native long mkBoolean(long pointer, boolean val); - /** - * Create a constant representing the number Pi. - * @return a constant representing Pi - */ - public Term mkPi() - { - long termPointer = mkPi(pointer); - return new Term(this, termPointer); - } - - private native long mkPi(long pointer); - /** - * Create an integer constant from a string. - * @param s the string representation of the constant, may represent an - * integer (e.g., "123"). - * @return a constant of sort Integer assuming 's' represents an integer) - */ - public Term mkInteger(String s) throws CVC5ApiException - { - long termPointer = mkInteger(pointer, s); - return new Term(this, termPointer); - } - - private native long mkInteger(long pointer, String s) throws CVC5ApiException; - - /** - * Create an integer constant from a c++ int. - * @param val the value of the constant - * @return a constant of sort Integer - */ - public Term mkInteger(long val) - { - long termPointer = mkInteger(pointer, val); - return new Term(this, termPointer); - } - - private native long mkInteger(long pointer, long val); - /** - * Create a real constant from a string. - * @param s the string representation of the constant, may represent an - * integer (e.g., "123") or real constant (e.g., "12.34" or - * "12/34"). - * @return a constant of sort Real - */ - public Term mkReal(String s) throws CVC5ApiException - { - long termPointer = mkReal(pointer, s); - return new Term(this, termPointer); - } - - private native long mkReal(long pointer, String s) throws CVC5ApiException; - /** - * Create a real constant from an integer. - * @param val the value of the constant - * @return a constant of sort Integer - */ - public Term mkReal(long val) - { - long termPointer = mkRealValue(pointer, val); - return new Term(this, termPointer); - } - - private native long mkRealValue(long pointer, long val); - /** - * Create a real constant from a rational. - * @param num the value of the numerator - * @param den the value of the denominator - * @return a constant of sort Real - */ - public Term mkReal(long num, long den) - { - long termPointer = mkReal(pointer, num, den); - return new Term(this, termPointer); - } - - private native long mkReal(long pointer, long num, long den); - - /** - * Create a regular expression empty term. - * @return the empty term - */ - public Term mkRegexpEmpty() - { - long termPointer = mkRegexpEmpty(pointer); - return new Term(this, termPointer); - } - - private native long mkRegexpEmpty(long pointer); - - /** - * Create a regular expression sigma term. - * @return the sigma term - */ - public Term mkRegexpSigma() - { - long termPointer = mkRegexpSigma(pointer); - return new Term(this, termPointer); - } - - private native long mkRegexpSigma(long pointer); - - /** - * Create a constant representing an empty set of the given sort. - * @param sort the sort of the set elements. - * @return the empty set constant - */ - public Term mkEmptySet(Sort sort) - { - long termPointer = mkEmptySet(pointer, sort.getPointer()); - return new Term(this, termPointer); - } - - private native long mkEmptySet(long pointer, long sortPointer); - /** - * Create a constant representing an empty bag of the given sort. - * @param sort the sort of the bag elements. - * @return the empty bag constant - */ - public Term mkEmptyBag(Sort sort) - { - long termPointer = mkEmptyBag(pointer, sort.getPointer()); - return new Term(this, termPointer); - } - - private native long mkEmptyBag(long pointer, long sortPointer); - - /** - * Create a separation logic empty term. - * @return the separation logic empty term - */ - public Term mkSepEmp() - { - long termPointer = mkSepEmp(pointer); - return new Term(this, termPointer); - } - - private native long mkSepEmp(long pointer); - - /** - * Create a separation logic nil term. - * @param sort the sort of the nil term - * @return the separation logic nil term - */ - public Term mkSepNil(Sort sort) - { - long termPointer = mkSepNil(pointer, sort.getPointer()); - return new Term(this, termPointer); - } - - private native long mkSepNil(long pointer, long sortPointer); - - /** - * Create a String constant. - * @param s the string this constant represents - * @return the String constant - */ - public Term mkString(String s) - { - return mkString(s, false); - } - - /** - * Create a String constant. - * @param s the string this constant represents - * @param useEscSequences determines whether escape sequences in `s` - * should be converted to the corresponding unicode character - * @return the String constant - */ - public Term mkString(String s, boolean useEscSequences) - { - // TODO: review unicode - long termPointer = mkString(pointer, s, useEscSequences); - return new Term(this, termPointer); - } - - private native long mkString(long pointer, String s, boolean useEscSequences); - - /** - * Create a String constant. - * @param s a list of unsigned (unicode) values this constant represents - * as - * string - * @return the String constant - */ - public Term mkString(int[] s) throws CVC5ApiException - { - Utils.validateUnsigned(s, "s"); - long termPointer = mkString(pointer, s); - return new Term(this, termPointer); - } - - private native long mkString(long pointer, int[] s); - - /** - * Create an empty sequence of the given element sort. - * @param sort The element sort of the sequence. - * @return the empty sequence with given element sort. - */ - public Term mkEmptySequence(Sort sort) - { - long termPointer = mkEmptySequence(pointer, sort.getPointer()); - return new Term(this, termPointer); - } - - private native long mkEmptySequence(long pointer, long sortPointer); - - /** - * Create a universe set of the given sort. - * @param sort the sort of the set elements - * @return the universe set constant - */ - public Term mkUniverseSet(Sort sort) - { - long termPointer = mkUniverseSet(pointer, sort.getPointer()); - return new Term(this, termPointer); - } - - private native long mkUniverseSet(long pointer, long sortPointer); - - /** - * Create a bit-vector constant of given size and value = 0. - * @param size the bit-width of the bit-vector sort - * @return the bit-vector constant - */ - public Term mkBitVector(int size) throws CVC5ApiException - { - return mkBitVector(size, 0); - } - - /** - * Create a bit-vector constant of given size and value. - * - * Note: The given value must fit into a bit-vector of the given size. - * - * @param size the bit-width of the bit-vector sort - * @param val the value of the constant - * @return the bit-vector constant - */ - public Term mkBitVector(int size, long val) throws CVC5ApiException - { - Utils.validateUnsigned(size, "size"); - Utils.validateUnsigned(val, "val"); - long termPointer = mkBitVector(pointer, size, val); - return new Term(this, termPointer); - } - - private native long mkBitVector(long pointer, int size, long val); - - /** - * Create a bit-vector constant of a given bit-width from a given string of - * base 2, 10 or 16. - * - * Note: The given value must fit into a bit-vector of the given size. - * - * @param size the bit-width of the constant - * @param s the string representation of the constant - * @param base the base of the string representation (2, 10, or 16) - * @return the bit-vector constant - */ - public Term mkBitVector(int size, String s, int base) throws CVC5ApiException - { - Utils.validateUnsigned(size, "size"); - Utils.validateUnsigned(base, "base"); - long termPointer = mkBitVector(pointer, size, s, base); - return new Term(this, termPointer); - } - - private native long mkBitVector(long pointer, int size, String s, int base); - - /** - * Create a constant array with the provided constant value stored at - * every index - * @param sort the sort of the constant array (must be an array sort) - * @param val the constant value to store (must match the sort's element - * sort) - * @return the constant array term - */ - public Term mkConstArray(Sort sort, Term val) - { - long termPointer = mkConstArray(pointer, sort.getPointer(), val.getPointer()); - return new Term(this, termPointer); - } - - private native long mkConstArray(long pointer, long sortPointer, long valPointer); - /** - * Create a positive infinity floating-point constant. - * @param exp Number of bits in the exponent - * @param sig Number of bits in the significand - * @return the floating-point constant - */ - public Term mkPosInf(int exp, int sig) throws CVC5ApiException - { - Utils.validateUnsigned(exp, "exp"); - Utils.validateUnsigned(sig, "sig"); - long termPointer = mkPosInf(pointer, exp, sig); - return new Term(this, termPointer); - } - - private native long mkPosInf(long pointer, int exp, int sig); - /** - * Create a negative infinity floating-point constant. - * @param exp Number of bits in the exponent - * @param sig Number of bits in the significand - * @return the floating-point constant - */ - public Term mkNegInf(int exp, int sig) throws CVC5ApiException - { - Utils.validateUnsigned(exp, "exp"); - Utils.validateUnsigned(sig, "sig"); - long termPointer = mkNegInf(pointer, exp, sig); - return new Term(this, termPointer); - } - - private native long mkNegInf(long pointer, int exp, int sig); - /** - * Create a not-a-number (NaN) floating-point constant. - * @param exp Number of bits in the exponent - * @param sig Number of bits in the significand - * @return the floating-point constant - */ - public Term mkNaN(int exp, int sig) throws CVC5ApiException - { - Utils.validateUnsigned(exp, "exp"); - Utils.validateUnsigned(sig, "sig"); - long termPointer = mkNaN(pointer, exp, sig); - return new Term(this, termPointer); - } - - private native long mkNaN(long pointer, int exp, int sig); - - /** - * Create a positive zero (+0.0) floating-point constant. - * @param exp Number of bits in the exponent - * @param sig Number of bits in the significand - * @return the floating-point constant - */ - public Term mkPosZero(int exp, int sig) throws CVC5ApiException - { - Utils.validateUnsigned(exp, "exp"); - Utils.validateUnsigned(sig, "sig"); - long termPointer = mkPosZero(pointer, exp, sig); - return new Term(this, termPointer); - } - - private native long mkPosZero(long pointer, int exp, int sig); - - /** - * Create a negative zero (-0.0) floating-point constant. - * @param exp Number of bits in the exponent - * @param sig Number of bits in the significand - * @return the floating-point constant - */ - public Term mkNegZero(int exp, int sig) throws CVC5ApiException - { - Utils.validateUnsigned(exp, "exp"); - Utils.validateUnsigned(sig, "sig"); - long termPointer = mkNegZero(pointer, exp, sig); - return new Term(this, termPointer); - } - - private native long mkNegZero(long pointer, int exp, int sig); - - /** - * Create a roundingmode constant. - * @param rm the floating point rounding mode this constant represents - */ - public Term mkRoundingMode(RoundingMode rm) - { - long termPointer = mkRoundingMode(pointer, rm.getValue()); - return new Term(this, termPointer); - } - - private native long mkRoundingMode(long pointer, int rm); - - /** - * Create uninterpreted constant. - * @param sort Sort of the constant - * @param index Index of the constant - */ - public Term mkUninterpretedConst(Sort sort, int index) throws CVC5ApiException - { - Utils.validateUnsigned(index, "index"); - long termPointer = mkUninterpretedConst(pointer, sort.getPointer(), index); - return new Term(this, termPointer); - } - - private native long mkUninterpretedConst(long pointer, long sortPointer, int index); - - /** - * Create an abstract value constant. - * @param index Index of the abstract value - */ - public Term mkAbstractValue(String index) - { - long termPointer = mkAbstractValue(pointer, index); - return new Term(this, termPointer); - } - - private native long mkAbstractValue(long pointer, String index); - - /** - * Create an abstract value constant. - * @param index Index of the abstract value - */ - public Term mkAbstractValue(long index) throws CVC5ApiException - { - Utils.validateUnsigned(index, "index"); - long termPointer = mkAbstractValue(pointer, index); - return new Term(this, termPointer); - } - - private native long mkAbstractValue(long pointer, long index); - - /** - * Create a floating-point constant. - * @param exp Size of the exponent - * @param sig Size of the significand - * @param val Value of the floating-point constant as a bit-vector term - */ - public Term mkFloatingPoint(int exp, int sig, Term val) throws CVC5ApiException - { - Utils.validateUnsigned(exp, "exp"); - Utils.validateUnsigned(sig, "sig"); - long termPointer = mkFloatingPoint(pointer, exp, sig, val.getPointer()); - return new Term(this, termPointer); - } - - private native long mkFloatingPoint(long pointer, int exp, int sig, long valPointer); - - /* .................................................................... */ - /* Create Variables */ - /* .................................................................... */ - - /** - * Create (first-order) constant (0-arity function symbol). - * SMT-LIB: - * {@code - * ( declare-const ) - * ( declare-fun ( ) ) - * } - * - * @param sort the sort of the constant - * @param symbol the name of the constant - * @return the first-order constant - */ - public Term mkConst(Sort sort, String symbol) - { - long termPointer = mkConst(pointer, sort.getPointer(), symbol); - return new Term(this, termPointer); - } - - private native long mkConst(long pointer, long sortPointer, String symbol); - - /** - * Create (first-order) constant (0-arity function symbol), with a default - * symbol name. - * - * @param sort the sort of the constant - * @return the first-order constant - */ - public Term mkConst(Sort sort) - { - long termPointer = mkConst(pointer, sort.getPointer()); - return new Term(this, termPointer); - } - - private native long mkConst(long pointer, long sortPointer); - - /** - * Create a bound variable to be used in a binder (i.e. a quantifier, a - * lambda, or a witness binder). - * @param sort the sort of the variable - * @return the variable - */ - public Term mkVar(Sort sort) - { - return mkVar(sort, ""); - } - - /** - * Create a bound variable to be used in a binder (i.e. a quantifier, a - * lambda, or a witness binder). - * @param sort the sort of the variable - * @param symbol the name of the variable - * @return the variable - */ - public Term mkVar(Sort sort, String symbol) - { - long termPointer = mkVar(pointer, sort.getPointer(), symbol); - return new Term(this, termPointer); - } - - private native long mkVar(long pointer, long sortPointer, String symbol); - - /* .................................................................... */ - /* Create datatype constructor declarations */ - /* .................................................................... */ - - public DatatypeConstructorDecl mkDatatypeConstructorDecl(String name) - { - long declPointer = mkDatatypeConstructorDecl(pointer, name); - return new DatatypeConstructorDecl(this, declPointer); - } - - private native long mkDatatypeConstructorDecl(long pointer, String name); - - /* .................................................................... */ - /* Create datatype declarations */ - /* .................................................................... */ - - /** - * Create a datatype declaration. - * @param name the name of the datatype - * @return the DatatypeDecl - */ - public DatatypeDecl mkDatatypeDecl(String name) - { - return mkDatatypeDecl(name, false); - } - - /** - * Create a datatype declaration. - * @param name the name of the datatype - * @param isCoDatatype true if a codatatype is to be constructed - * @return the DatatypeDecl - */ - public DatatypeDecl mkDatatypeDecl(String name, boolean isCoDatatype) - { - long declPointer = mkDatatypeDecl(pointer, name, isCoDatatype); - return new DatatypeDecl(this, declPointer); - } - - private native long mkDatatypeDecl(long pointer, String name, boolean isCoDatatype); - - /** - * Create a datatype declaration. - * Create sorts parameter with Solver::mkParamSort(). - * @param name the name of the datatype - * @param param the sort parameter - * @return the DatatypeDecl - */ - public DatatypeDecl mkDatatypeDecl(String name, Sort param) - { - return mkDatatypeDecl(name, param, false); - } - - /** - * Create a datatype declaration. - * Create sorts parameter with Solver::mkParamSort(). - * @param name the name of the datatype - * @param param the sort parameter - * @param isCoDatatype true if a codatatype is to be constructed - * @return the DatatypeDecl - */ - public DatatypeDecl mkDatatypeDecl(String name, Sort param, boolean isCoDatatype) - { - long declPointer = mkDatatypeDecl(pointer, name, param.getPointer(), isCoDatatype); - return new DatatypeDecl(this, declPointer); - } - - private native long mkDatatypeDecl( - long pointer, String name, long paramPointer, boolean isCoDatatype); - - /** - * Create a datatype declaration. - * Create sorts parameter with Solver::mkParamSort(). - * @param name the name of the datatype - * @param params a list of sort parameters - * @return the DatatypeDecl - */ - public DatatypeDecl mkDatatypeDecl(String name, List params) - { - return mkDatatypeDecl(name, params.toArray(new Sort[0])); - } - - /** - * Create a datatype declaration. - * Create sorts parameter with Solver::mkParamSort(). - * @param name the name of the datatype - * @param params a list of sort parameters - * @return the DatatypeDecl - */ - public DatatypeDecl mkDatatypeDecl(String name, Sort[] params) - { - return mkDatatypeDecl(name, params, false); - } - - /** - * Create a datatype declaration. - * Create sorts parameter with Solver::mkParamSort(). - * @param name the name of the datatype - * @param params a list of sort parameters - * @param isCoDatatype true if a codatatype is to be constructed - * @return the DatatypeDecl - */ - public DatatypeDecl mkDatatypeDecl(String name, Sort[] params, boolean isCoDatatype) - { - long[] paramPointers = Utils.getPointers(params); - long declPointer = mkDatatypeDecl(pointer, name, paramPointers, isCoDatatype); - return new DatatypeDecl(this, declPointer); - } - - private native long mkDatatypeDecl( - long pointer, String name, long[] paramPointers, boolean isCoDatatype); - - /* .................................................................... */ - /* Formula Handling */ - /* .................................................................... */ - - /** - * Simplify a formula without doing "much" work. Does not involve - * the SAT Engine in the simplification, but uses the current - * definitions, assertions, and the current partial model, if one - * has been constructed. It also involves theory normalization. - * @param t the formula to simplify - * @return the simplified formula - */ - public Term simplify(Term t) - { - long termPointer = simplify(pointer, t.getPointer()); - return new Term(this, termPointer); - } - - private native long simplify(long pointer, long termPointer); - - /** - * Assert a formula. - * SMT-LIB: - * {@code - * ( assert ) - * } - * @param term the formula to assert - */ - public void assertFormula(Term term) - { - assertFormula(pointer, term.getPointer()); - } - - private native void assertFormula(long pointer, long termPointer); - - /** - * Check satisfiability. - * SMT-LIB: - * {@code - * ( check-sat ) - * } - * @return the result of the satisfiability check. - */ - public Result checkSat() - { - long resultPointer = checkSat(pointer); - return new Result(this, resultPointer); - } - - private native long checkSat(long pointer); - /** - * Check satisfiability assuming the given formula. - * SMT-LIB: - * {@code - * ( check-sat-assuming ( ) ) - * } - * @param assumption the formula to assume - * @return the result of the satisfiability check. - */ - public Result checkSatAssuming(Term assumption) - { - long resultPointer = checkSatAssuming(pointer, assumption.getPointer()); - return new Result(this, resultPointer); - } - - private native long checkSatAssuming(long pointer, long assumptionPointer); - - /** - * Check satisfiability assuming the given formulas. - * SMT-LIB: - * {@code - * ( check-sat-assuming ( + ) ) - * } - * @param assumptions the formulas to assume - * @return the result of the satisfiability check. - */ - public Result checkSatAssuming(Term[] assumptions) - { - long[] pointers = Utils.getPointers(assumptions); - long resultPointer = checkSatAssuming(pointer, pointers); - return new Result(this, resultPointer); - } - - private native long checkSatAssuming(long pointer, long[] assumptionPointers); - - /** - * Check entailment of the given formula w.r.t. the current set of assertions. - * @param term the formula to check entailment for - * @return the result of the entailment check. - */ - public Result checkEntailed(Term term) - { - long resultPointer = checkEntailed(pointer, term.getPointer()); - return new Result(this, resultPointer); - } - - private native long checkEntailed(long pointer, long termPointer); - - /** - * Check entailment of the given set of given formulas w.r.t. the current - * set of assertions. - * @param terms the terms to check entailment for - * @return the result of the entailmentcheck. - */ - public Result checkEntailed(Term[] terms) - { - long[] pointers = Utils.getPointers(terms); - long resultPointer = checkEntailed(pointer, pointers); - return new Result(this, resultPointer); - } - - private native long checkEntailed(long pointer, long[] termPointers); - - /** - * Create datatype sort. - * SMT-LIB: - * {@code - * ( declare-datatype ) - * } - * @param symbol the name of the datatype sort - * @param ctors the constructor declarations of the datatype sort - * @return the datatype sort - */ - public Sort declareDatatype(String symbol, DatatypeConstructorDecl[] ctors) - { - long[] pointers = Utils.getPointers(ctors); - long sortPointer = declareDatatype(pointer, symbol, pointers); - return new Sort(this, sortPointer); - } - - private native long declareDatatype(long pointer, String symbol, long[] declPointers); - - /** - * Declare n-ary function symbol. - * SMT-LIB: - * {@code - * ( declare-fun ( * ) ) - * } - * @param symbol the name of the function - * @param sorts the sorts of the parameters to this function - * @param sort the sort of the return value of this function - * @return the function - */ - public Term declareFun(String symbol, Sort[] sorts, Sort sort) - { - long[] sortPointers = Utils.getPointers(sorts); - long termPointer = declareFun(pointer, symbol, sortPointers, sort.getPointer()); - return new Term(this, termPointer); - } - - private native long declareFun( - long pointer, String symbol, long[] sortPointers, long sortPointer); - - /** - * Declare uninterpreted sort. - * SMT-LIB: - * {@code - * ( declare-sort ) - * } - * @param symbol the name of the sort - * @param arity the arity of the sort - * @return the sort - */ - public Sort declareSort(String symbol, int arity) throws CVC5ApiException - { - Utils.validateUnsigned(arity, "arity"); - long sortPointer = declareSort(pointer, symbol, arity); - return new Sort(this, sortPointer); - } - - private native long declareSort(long pointer, String symbol, int arity); - - /** - * Define n-ary function in the current context. - * SMT-LIB: - * {@code - * ( define-fun ) - * } - * @param symbol the name of the function - * @param boundVars the parameters to this function - * @param sort the sort of the return value of this function - * @param term the function body - * @return the function - */ - public Term defineFun(String symbol, Term[] boundVars, Sort sort, Term term) - { - return defineFun(symbol, boundVars, sort, term, false); - } - - /** - * Define n-ary function. - * SMT-LIB: - * {@code - * ( define-fun ) - * } - * @param symbol the name of the function - * @param boundVars the parameters to this function - * @param sort the sort of the return value of this function - * @param term the function body - * @param global determines whether this definition is global (i.e. persists - * when popping the context) - * @return the function - */ - public Term defineFun(String symbol, Term[] boundVars, Sort sort, Term term, boolean global) - { - long[] boundVarPointers = Utils.getPointers(boundVars); - long termPointer = - defineFun(pointer, symbol, boundVarPointers, sort.getPointer(), term.getPointer(), global); - return new Term(this, termPointer); - } - - private native long defineFun(long pointer, - String symbol, - long[] boundVarPointers, - long sortPointer, - long termPointer, - boolean global); - - /** - * Define n-ary function in the current context. - * SMT-LIB: - * {@code - * ( define-fun ) - * } - * Create parameter 'fun' with mkConst(). - * @param fun the sorted function - * @param boundVars the parameters to this function - * @param term the function body - * @return the function - */ - public Term defineFun(Term fun, Term[] boundVars, Term term) - { - return defineFun(fun, boundVars, term, false); - } - /** - * Define n-ary function. - * SMT-LIB: - * {@code - * ( define-fun ) - * } - * Create parameter 'fun' with mkConst(). - * @param fun the sorted function - * @param boundVars the parameters to this function - * @param term the function body - * @param global determines whether this definition is global (i.e. persists - * when popping the context) - * @return the function - */ - public Term defineFun(Term fun, Term[] boundVars, Term term, boolean global) - { - long[] boundVarPointers = Utils.getPointers(boundVars); - long termPointer = - defineFun(pointer, fun.getPointer(), boundVarPointers, term.getPointer(), global); - return new Term(this, termPointer); - } - - private native long defineFun( - long pointer, long funPointer, long[] boundVarPointers, long termPointer, boolean global); - - /** - * Define recursive function in the current context. - * SMT-LIB: - * {@code - * ( define-fun-rec ) - * } - * @param symbol the name of the function - * @param boundVars the parameters to this function - * @param sort the sort of the return value of this function - * @param term the function body - * @return the function - */ - public Term defineFunRec(String symbol, Term[] boundVars, Sort sort, Term term) - { - return defineFunRec(symbol, boundVars, sort, term, false); - } - - /** - * Define recursive function. - * SMT-LIB: - * {@code - * ( define-fun-rec ) - * } - * @param symbol the name of the function - * @param boundVars the parameters to this function - * @param sort the sort of the return value of this function - * @param term the function body - * @param global determines whether this definition is global (i.e. persists - * when popping the context) - * @return the function - */ - public Term defineFunRec(String symbol, Term[] boundVars, Sort sort, Term term, boolean global) - { - long[] boundVarPointers = Utils.getPointers(boundVars); - long termPointer = defineFunRec( - pointer, symbol, boundVarPointers, sort.getPointer(), term.getPointer(), global); - return new Term(this, termPointer); - } - - private native long defineFunRec(long pointer, - String symbol, - long[] boundVarPointers, - long sortPointer, - long termPointer, - boolean global); - - /** - * Define recursive function in the current context. - * SMT-LIB: - * {@code - * ( define-fun-rec ) - * } - * Create parameter 'fun' with mkConst(). - * @param fun the sorted function - * @param boundVars the parameters to this function - * @param term the function body - * @return the function - */ - - public Term defineFunRec(Term fun, Term[] boundVars, Term term) - { - return defineFunRec(fun, boundVars, term, false); - } - - /** - * Define recursive function. - * SMT-LIB: - * {@code - * ( define-fun-rec ) - * } - * Create parameter 'fun' with mkConst(). - * @param fun the sorted function - * @param boundVars the parameters to this function - * @param term the function body - * @param global determines whether this definition is global (i.e. persists - * when popping the context) - * @return the function - */ - public Term defineFunRec(Term fun, Term[] boundVars, Term term, boolean global) - { - long[] boundVarPointers = Utils.getPointers(boundVars); - long termPointer = - defineFunRec(pointer, fun.getPointer(), boundVarPointers, term.getPointer(), global); - return new Term(this, termPointer); - } - - private native long defineFunRec( - long pointer, long funPointer, long[] boundVarPointers, long termPointer, boolean global); - - /** - * Define recursive functions in the current context. - * SMT-LIB: - * {@code - * ( define-funs-rec ( ^{n+1} ) ( ^{n+1} ) ) - * } - * Create elements of parameter 'funs' with mkConst(). - * @param funs the sorted functions - * @param boundVars the list of parameters to the functions - * @param terms the list of function bodies of the functions - */ - public void defineFunsRec(Term[] funs, Term[][] boundVars, Term[] terms) - { - defineFunsRec(funs, boundVars, terms, false); - } - /** - * Define recursive functions. - * SMT-LIB: - * {@code - * ( define-funs-rec ( ^{n+1} ) ( ^{n+1} ) ) - * } - * Create elements of parameter 'funs' with mkConst(). - * @param funs the sorted functions - * @param boundVars the list of parameters to the functions - * @param terms the list of function bodies of the functions - * @param global determines whether this definition is global (i.e. persists - * when popping the context) - */ - public void defineFunsRec(Term[] funs, Term[][] boundVars, Term[] terms, boolean global) - { - long[] funPointers = Utils.getPointers(funs); - long[][] boundVarPointers = Utils.getPointers(boundVars); - long[] termPointers = Utils.getPointers(terms); - defineFunsRec(pointer, funPointers, boundVarPointers, termPointers, global); - } - - private native void defineFunsRec(long pointer, - long[] funPointers, - long[][] boundVarPointers, - long[] termPointers, - boolean global); - - /** - * Echo a given string to the given output stream. - * SMT-LIB: - * {@code - * ( echo ) - * } - * @param out the output stream - * @param str the string to echo - */ - // TODO: void echo(std::ostream& out, String str) - - /** - * Get the list of asserted formulas. - * SMT-LIB: - * {@code - * ( get-assertions ) - * } - * @return the list of asserted formulas - */ - public Term[] getAssertions() - { - long[] retPointers = getAssertions(pointer); - return Utils.getTerms(this, retPointers); - } - - private native long[] getAssertions(long pointer); - - /** - * Get info from the solver. - * SMT-LIB: {@code ( get-info ) } - * @return the info - */ - public String getInfo(String flag) - { - return getInfo(pointer, flag); - } - - private native String getInfo(long pointer, String flag); - - /** - * Get the value of a given option. - * SMT-LIB: - * {@code - * ( get-option ) - * } - * @param option the option for which the value is queried - * @return a string representation of the option value - */ - public String getOption(String option) - { - return getOption(pointer, option); - } - - private native String getOption(long pointer, String option); - - /** - * Get all option names that can be used with `setOption`, `getOption` and - * `getOptionInfo`. - * @return all option names - */ - public String[] getOptionNames() - { - return getOptionNames(pointer); - } - - private native String[] getOptionNames(long pointer); - - /** - * Get some information about the given option. Check the `OptionInfo` class - * for more details on which information is available. - * @return information about the given option - */ - public OptionInfo getOptionInfo(String option) - { - long optionPointer = getOptionInfo(pointer, option); - return new OptionInfo(this, optionPointer); - } - - private native long getOptionInfo(long pointer, String option); - - /** - * Get the set of unsat ("failed") assumptions. - * SMT-LIB: - * {@code - * ( get-unsat-assumptions ) - * } - * Requires to enable option 'produce-unsat-assumptions'. - * @return the set of unsat assumptions. - */ - public Term[] getUnsatAssumptions() - { - long[] retPointers = getUnsatAssumptions(pointer); - return Utils.getTerms(this, retPointers); - } - - private native long[] getUnsatAssumptions(long pointer); - - /** - * Get the unsatisfiable core. - * SMT-LIB: - * {@code - * ( get-unsat-core ) - * } - * Requires to enable option 'produce-unsat-cores'. - * @return a set of terms representing the unsatisfiable core - */ - public Term[] getUnsatCore() - { - long[] retPointers = getUnsatCore(pointer); - return Utils.getTerms(this, retPointers); - } - - private native long[] getUnsatCore(long pointer); - - /** - * Get a difficulty estimate for an asserted formula. This method is - * intended to be called immediately after any response to a checkSat. - * - * @return a map from (a subset of) the input assertions to a real value that - * is an estimate of how difficult each assertion was to solve. Unmentioned - * assertions can be assumed to have zero difficulty. - */ - public Map getDifficulty() - { - Map map = getDifficulty(pointer); - Map ret = new HashMap<>(); - for (Map.Entry entry : map.entrySet()) - { - Term key = new Term(this, entry.getKey()); - Term value = new Term(this, entry.getValue()); - ret.put(key, value); - } - return ret; - } - - private native Map getDifficulty(long pointer); - - /** - * Get the refutation proof - * SMT-LIB: - * {@code - * ( get-proof ) - * } - * Requires to enable option 'produce-proofs'. - * @return a string representing the proof, according to the value of - * proof-format-mode. - */ - public String getProof() - { - return getProof(pointer); - } - - private native String getProof(long pointer); - - /** - * Get the value of the given term in the current model. - * SMT-LIB: - * {@code - * ( get-value ( ) ) - * } - * @param term the term for which the value is queried - * @return the value of the given term - */ - public Term getValue(Term term) - { - long termPointer = getValue(pointer, term.getPointer()); - return new Term(this, termPointer); - } - - private native long getValue(long pointer, long termPointer); - - /** - * Get the values of the given terms in the current model. - * SMT-LIB: - * {@code - * ( get-value ( + ) ) - * } - * @param terms the terms for which the value is queried - * @return the values of the given terms - */ - public Term[] getValue(Term[] terms) - { - long[] pointers = Utils.getPointers(terms); - long[] retPointers = getValue(pointer, pointers); - return Utils.getTerms(this, retPointers); - } - - private native long[] getValue(long pointer, long[] termPointers); - - /** - * Get the domain elements of uninterpreted sort s in the current model. The - * current model interprets s as the finite sort whose domain elements are - * given in the return value of this method. - * - * @param s The uninterpreted sort in question - * @return the domain elements of s in the current model - */ - public Term[] getModelDomainElements(Sort s) - { - long[] pointers = getModelDomainElements(pointer, s.getPointer()); - return Utils.getTerms(this, pointers); - } - - private native long[] getModelDomainElements(long pointer, long sortPointer); - - /** - * This returns false if the model value of free constant v was not essential - * for showing the satisfiability of the last call to checkSat using the - * current model. This method will only return false (for any v) if - * the model-cores option has been set. - * - * @param v The term in question - * @return true if v is a model core symbol - */ - public boolean isModelCoreSymbol(Term v) - { - return isModelCoreSymbol(pointer, v.getPointer()); - } - - private native boolean isModelCoreSymbol(long pointer, long termPointer); - - /** - * Get the model - * SMT-LIB: - * {@code - * ( get-model ) - * } - * Requires to enable option 'produce-models'. - * @param sorts The list of uninterpreted sorts that should be printed in the - * model. - * @param vars The list of free constants that should be printed in the - * model. A subset of these may be printed based on isModelCoreSymbol. - * @return a string representing the model. - */ - public String getModel(Sort[] sorts, Term[] vars) - { - long[] sortPointers = Utils.getPointers(sorts); - long[] varPointers = Utils.getPointers(vars); - return getModel(pointer, sortPointers, varPointers); - } - - private native String getModel(long pointer, long[] sortPointers, long[] varPointers); - - /** - * Do quantifier elimination. - * SMT-LIB: - * {@code - * ( get-qe ) - * } - * Requires a logic that supports quantifier elimination. Currently, the only - * logics supported by quantifier elimination is LRA and LIA. - * @param q a quantified formula of the form: - * Q x1...xn. P( x1...xn, y1...yn ) - * where P( x1...xn, y1...yn ) is a quantifier-free formula - * @return a formula ret such that, given the current set of formulas A - * asserted to this solver: - * - ( A ^ q ) and ( A ^ ret ) are equivalent - * - ret is quantifier-free formula containing only free variables in - * y1...yn. - */ - public Term getQuantifierElimination(Term q) - { - long termPointer = getQuantifierElimination(pointer, q.getPointer()); - return new Term(this, termPointer); - } - - private native long getQuantifierElimination(long pointer, long qPointer); - - /** - * Do partial quantifier elimination, which can be used for incrementally - * computing the result of a quantifier elimination. - * SMT-LIB: - * {@code - * ( get-qe-disjunct ) - * } - * Requires a logic that supports quantifier elimination. Currently, the only - * logics supported by quantifier elimination is LRA and LIA. - * @param q a quantified formula of the form: - * Q x1...xn. P( x1...xn, y1...yn ) - * where P( x1...xn, y1...yn ) is a quantifier-free formula - * @return a formula ret such that, given the current set of formulas A - * asserted to this solver: - * - {@code (A ^ q) => (A ^ ret)} if Q is forall or {@code (A ^ ret) => (A ^ q)} if Q is - * exists, - * - ret is quantifier-free formula containing only free variables in - * y1...yn, - * - If Q is exists, let A^Q_n be the formula - * {@code A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n} - * where for each i=1,...n, formula ret^Q_i is the result of calling - * getQuantifierEliminationDisjunct for q with the set of assertions - * {@code A^Q_{i-1}}. Similarly, if Q is forall, then let {@code A^Q_n} be - * {@code A ^ ret^Q_1 ^ ... ^ ret^Q_n } - * where ret^Q_i is the same as above. In either case, we have - * that ret^Q_j will eventually be true or false, for some finite j. - */ - public Term getQuantifierEliminationDisjunct(Term q) - { - long termPointer = getQuantifierEliminationDisjunct(pointer, q.getPointer()); - return new Term(this, termPointer); - } - - private native long getQuantifierEliminationDisjunct(long pointer, long qPointer); - - /** - * When using separation logic, this sets the location sort and the - * datatype sort to the given ones. This method should be invoked exactly - * once, before any separation logic constraints are provided. - * @param locSort The location sort of the heap - * @param dataSort The data sort of the heap - */ - public void declareSeparationHeap(Sort locSort, Sort dataSort) - { - declareSeparationHeap(pointer, locSort.getPointer(), dataSort.getPointer()); - } - - private native void declareSeparationHeap( - long pointer, long locSortPointer, long dataSortPointer); - - /** - * When using separation logic, obtain the term for the heap. - * @return The term for the heap - */ - public Term getSeparationHeap() - { - long termPointer = getSeparationHeap(pointer); - return new Term(this, termPointer); - } - - private native long getSeparationHeap(long pointer); - - /** - * When using separation logic, obtain the term for nil. - * @return The term for nil - */ - public Term getSeparationNilTerm() - { - long termPointer = getSeparationNilTerm(pointer); - return new Term(this, termPointer); - } - - private native long getSeparationNilTerm(long pointer); - - /** - * Declare a symbolic pool of terms with the given initial value. - * SMT-LIB: - * {@code - * ( declare-pool ( * ) ) - * } - * @param symbol The name of the pool - * @param sort The sort of the elements of the pool. - * @param initValue The initial value of the pool - */ - public Term declarePool(String symbol, Sort sort, Term[] initValue) - { - long[] termPointers = Utils.getPointers(initValue); - long termPointer = declarePool(pointer, symbol, sort.getPointer(), termPointers); - return new Term(this, termPointer); - } - - private native long declarePool( - long pointer, String symbol, long sortPointer, long[] termPointers); - - /** - * Pop a level from the assertion stack. - * SMT-LIB: - * {@code - * ( pop ) - * } - */ - public void pop() throws CVC5ApiException - { - pop(1); - } - - /** - * Pop (a) level(s) from the assertion stack. - * SMT-LIB: - * {@code - * ( pop ) - * } - * @param nscopes the number of levels to pop - */ - public void pop(int nscopes) throws CVC5ApiException - { - Utils.validateUnsigned(nscopes, "nscopes"); - pop(pointer, nscopes); - } - - private native void pop(long pointer, int nscopes); - - /** - * Get an interpolant - * SMT-LIB: - * {@code - * ( get-interpol ) - * } - * Requires to enable option 'produce-interpols'. - * @param conj the conjecture term - * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the - * current set of assertions and B is given in the input by conj. - * @return true if it gets I successfully, false otherwise. - */ - public boolean getInterpolant(Term conj, Term output) - { - return getInterpolant(pointer, conj.getPointer(), output.getPointer()); - } - - private native boolean getInterpolant(long pointer, long conjPointer, long outputPointer); - - /** - * Get an interpolant - * SMT-LIB: - * {@code - * ( get-interpol ) - * } - * Requires to enable option 'produce-interpols'. - * @param conj the conjecture term - * @param grammar the grammar for the interpolant I - * @param output a Term I such that {@code A->I} and {@code I->B} are valid, where A is the - * current set of assertions and B is given in the input by conj. - * @return true if it gets I successfully, false otherwise. - */ - public boolean getInterpolant(Term conj, Grammar grammar, Term output) - { - return getInterpolant(pointer, conj.getPointer(), grammar.getPointer(), output.getPointer()); - } - - private native boolean getInterpolant( - long pointer, long conjPointer, long grammarPointer, long outputPointer); - - /** - * Get an abduct. - * SMT-LIB: - * {@code - * ( get-abduct ) - * } - * Requires enabling option 'produce-abducts' - * @param conj the conjecture term - * @param output a term C such that A^C is satisfiable, and A^~B^C is - * unsatisfiable, where A is the current set of assertions and B is - * given in the input by conj - * @return true if it gets C successfully, false otherwise - */ - public boolean getAbduct(Term conj, Term output) - { - return getAbduct(pointer, conj.getPointer(), output.getPointer()); - } - - private native boolean getAbduct(long pointer, long conjPointer, long outputPointer); - /** - * Get an abduct. - * SMT-LIB: - * {@code - * ( get-abduct ) - * } - * Requires enabling option 'produce-abducts' - * @param conj the conjecture term - * @param grammar the grammar for the abduct C - * @param output a term C such that A^C is satisfiable, and A^~B^C is - * unsatisfiable, where A is the current set of assertions and B is - * given in the input by conj - * @return true if it gets C successfully, false otherwise - */ - public boolean getAbduct(Term conj, Grammar grammar, Term output) - { - return getAbduct(pointer, conj.getPointer(), grammar.getPointer(), output.getPointer()); - } - - private native boolean getAbduct( - long pointer, long conjPointer, long grammarPointer, long outputPointer); - - /** - * Block the current model. Can be called only if immediately preceded by a - * SAT or INVALID query. - * SMT-LIB: - * {@code - * ( block-model ) - * } - * Requires enabling 'produce-models' option and setting 'block-models' option - * to a mode other than "none". - */ - public void blockModel() - { - blockModel(pointer); - } - - private native void blockModel(long pointer); - - /** - * Block the current model values of (at least) the values in terms. Can be - * called only if immediately preceded by a SAT or NOT_ENTAILED query. - * SMT-LIB: - * {@code - * ( block-model-values ( + ) ) - * } - * Requires enabling 'produce-models' option and setting 'block-models' option - * to a mode other than "none". - */ - public void blockModelValues(Term[] terms) - { - long[] pointers = Utils.getPointers(terms); - blockModelValues(pointer, pointers); - } - - private native void blockModelValues(long pointer, long[] termPointers); - - /** - * Print all instantiations made by the quantifiers module. - * @param out the output stream - */ - // TODO: void printInstantiations(std::ostream& out) - - /** - * Push a level to the assertion stack. - * SMT-LIB: - * {@code - * ( push ) - * } - */ - public void push() throws CVC5ApiException - { - push(1); - } - - /** - * Push (a) level(s) to the assertion stack. - * SMT-LIB: - * {@code - * ( push ) - * } - * @param nscopes the number of levels to push - */ - public void push(int nscopes) throws CVC5ApiException - { - Utils.validateUnsigned(nscopes, "nscopes"); - push(pointer, nscopes); - } - - private native void push(long pointer, int nscopes); - - /** - * Remove all assertions. - * SMT-LIB: - * {@code - * ( reset-assertions ) - * } - */ - public void resetAssertions() - { - resetAssertions(pointer); - } - - private native void resetAssertions(long pointer); - - /** - * Set info. - * SMT-LIB: - * {@code - * ( set-info ) - * } - * @param keyword the info flag - * @param value the value of the info flag - */ - public void setInfo(String keyword, String value) throws CVC5ApiException - { - setInfo(pointer, keyword, value); - } - - private native void setInfo(long pointer, String keyword, String value) throws CVC5ApiException; - - /** - * Set logic. - * SMT-LIB: - * {@code - * ( set-logic ) - * } - * @param logic the logic to set - */ - public void setLogic(String logic) throws CVC5ApiException - { - setLogic(pointer, logic); - } - - private native void setLogic(long pointer, String logic) throws CVC5ApiException; - - /** - * Set option. - * SMT-LIB: - * {@code - * ( set-option