From: Andres Noetzli Date: Thu, 31 Mar 2022 04:09:03 +0000 (-0700) Subject: Move Java package to `io.github.cvc5` (#8469) X-Git-Tag: cvc5-1.0.0~101 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c93de62d8b084cbcdb88c87ff856d240f2f49efe;p=cvc5.git Move Java package to `io.github.cvc5` (#8469) Previously, we were using io.github.cvc5.api to mirror the C++ namespace that the API was in. The namespace of the C++ API changed to simply cvc5 and so this commit updates the Java package accordingly. --- diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt index 2fcf74767..def6524be 100644 --- a/docs/api/java/CMakeLists.txt +++ b/docs/api/java/CMakeLists.txt @@ -27,7 +27,7 @@ if(BUILD_BINDINGS_JAVA) add_custom_command( OUTPUT ${JAVADOC_INDEX_FILE} COMMAND - ${Java_JAVADOC_EXECUTABLE} io.github.cvc5.api + ${Java_JAVADOC_EXECUTABLE} io.github.cvc5 -sourcepath ${CMAKE_SOURCE_DIR}/src/api/java/:${CMAKE_BINARY_DIR}/src/api/java/ -d ${JAVADOC_OUTPUT_DIR} -cp ${CVC5_JAR_FILE} diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index dc1a6de1c..b1aafdbb0 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -20,9 +20,9 @@ * SimpleVC */ -import static io.github.cvc5.api.Kind.*; +import static io.github.cvc5.Kind.*; -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class SimpleVC { diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index e5a78e86c..2abbc35fe 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -15,7 +15,7 @@ * */ -import io.github.cvc5.api.*; +import io.github.cvc5.*; import java.util.*; public class BitVectors diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java index c72106082..f036e090e 100644 --- a/examples/api/java/BitVectorsAndArrays.java +++ b/examples/api/java/BitVectorsAndArrays.java @@ -15,7 +15,7 @@ * */ -import io.github.cvc5.api.*; +import io.github.cvc5.*; import java.util.*; public class BitVectorsAndArrays diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index f2c6d046b..60a9e803b 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -17,7 +17,7 @@ * The model is displayed using getValue(). */ -import io.github.cvc5.api.*; +import io.github.cvc5.*; import java.util.Iterator; public class Combination diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java index 77cfea040..35d6914f1 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 io.github.cvc5.api.*; +import io.github.cvc5.*; import java.util.Iterator; public class Datatypes diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java index 0ac1f628c..9c2bef99e 100644 --- a/examples/api/java/Exceptions.java +++ b/examples/api/java/Exceptions.java @@ -15,7 +15,7 @@ * A simple demonstration of catching cvc5 execptions via the Java API. */ -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class Exceptions { diff --git a/examples/api/java/Extract.java b/examples/api/java/Extract.java index c9c325bb0..c5f77c815 100644 --- a/examples/api/java/Extract.java +++ b/examples/api/java/Extract.java @@ -15,7 +15,7 @@ * */ -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class Extract { diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java index 92b03ec6c..b799ff460 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 io.github.cvc5.api.Kind.*; +import static io.github.cvc5.Kind.*; -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class FloatingPointArith { diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index b222a57e1..7cef12966 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -13,7 +13,7 @@ * A very simple CVC5 tutorial example. */ -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class HelloWorld { diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index 0e59b7109..7ba565ff3 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 io.github.cvc5.api.*; +import io.github.cvc5.*; 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 ee169c490..359601c31 100644 --- a/examples/api/java/QuickStart.java +++ b/examples/api/java/QuickStart.java @@ -14,7 +14,7 @@ * */ -import io.github.cvc5.api.*; +import io.github.cvc5.*; 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 8f0c48090..a4b568ccd 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 cvc5 via Java API. */ -import static io.github.cvc5.api.Kind.*; +import static io.github.cvc5.Kind.*; -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class Relations { diff --git a/examples/api/java/Sequences.java b/examples/api/java/Sequences.java index 0fd578984..74921a9b9 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 io.github.cvc5.api.Kind.*; +import static io.github.cvc5.Kind.*; -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class Sequences { diff --git a/examples/api/java/Sets.java b/examples/api/java/Sets.java index b7b20905c..6002c0e69 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 io.github.cvc5.api.Kind.*; +import static io.github.cvc5.Kind.*; -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class Sets { diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java index a09127fe8..da1bbeb8c 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -13,9 +13,9 @@ * An example of accessing cvc5's statistics using the Java API. */ -import static io.github.cvc5.api.Kind.*; +import static io.github.cvc5.Kind.*; -import io.github.cvc5.api.*; +import io.github.cvc5.*; import java.util.List; import java.util.Map; @@ -27,7 +27,7 @@ public class Statistics { // Get the statistics from the `Solver` and iterate over them. The // `Statistics` class implements the `Iterable>` interface. - io.github.cvc5.api.Statistics stats = solver.getStatistics(); + io.github.cvc5.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 28487b852..10fe70fdd 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 io.github.cvc5.api.Kind.*; +import static io.github.cvc5.Kind.*; -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class Strings { diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java index 6063a8239..3ce5a5e45 100644 --- a/examples/api/java/SygusFun.java +++ b/examples/api/java/SygusFun.java @@ -16,9 +16,9 @@ * functions. This is a direct translation of sygus-fun.cpp. */ -import static io.github.cvc5.api.Kind.*; +import static io.github.cvc5.Kind.*; -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class SygusFun { diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java index cb8a5106a..127da1c5f 100644 --- a/examples/api/java/SygusGrammar.java +++ b/examples/api/java/SygusGrammar.java @@ -17,9 +17,9 @@ * of sygus-grammar.cpp. */ -import static io.github.cvc5.api.Kind.*; +import static io.github.cvc5.Kind.*; -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class SygusGrammar { diff --git a/examples/api/java/SygusInv.java b/examples/api/java/SygusInv.java index 8e9f79eac..e24adc68c 100644 --- a/examples/api/java/SygusInv.java +++ b/examples/api/java/SygusInv.java @@ -16,9 +16,9 @@ * invariant. This is a direct translation of sygus-inv.cpp. */ -import static io.github.cvc5.api.Kind.*; +import static io.github.cvc5.Kind.*; -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class SygusInv { diff --git a/examples/api/java/Transcendentals.java b/examples/api/java/Transcendentals.java index a44a1e4c0..8638dcff5 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 io.github.cvc5.api.Kind.*; +import static io.github.cvc5.Kind.*; -import io.github.cvc5.api.*; +import io.github.cvc5.*; public class Transcendentals { diff --git a/examples/api/java/UnsatCores.java b/examples/api/java/UnsatCores.java index b91a94ab7..cbd076713 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 cvc5's Java API. */ -import io.github.cvc5.api.*; +import io.github.cvc5.*; import java.util.Arrays; public class UnsatCores diff --git a/examples/api/java/Utils.java b/examples/api/java/Utils.java index 6cfd6c766..9a2054d86 100644 --- a/examples/api/java/Utils.java +++ b/examples/api/java/Utils.java @@ -16,10 +16,10 @@ import java.util.ArrayList; import java.util.List; -import io.github.cvc5.api.CVC5ApiException; -import io.github.cvc5.api.Kind; -import io.github.cvc5.api.Sort; -import io.github.cvc5.api.Term; +import io.github.cvc5.CVC5ApiException; +import io.github.cvc5.Kind; +import io.github.cvc5.Sort; +import io.github.cvc5.Term; public class Utils { diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index b274a5145..79a95bd57 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -22,7 +22,7 @@ configure_file(genenums.py.in genenums.py) # Generate Kind.java set(JAVA_KIND_FILE - "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/Kind.java" + "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/Kind.java" ) add_custom_command( OUTPUT @@ -31,7 +31,7 @@ add_custom_command( "${PYTHON_EXECUTABLE}" "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" --enums-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" - --java-api-path "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/" + --java-api-path "${CMAKE_CURRENT_BINARY_DIR}/io/github/" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" "${PROJECT_SOURCE_DIR}/src/api/parseenums.py" @@ -40,9 +40,9 @@ add_custom_command( add_custom_target(generate-java-kinds DEPENDS ${JAVA_KIND_FILE}) set(JAVA_TYPES_FILES - "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/BlockModelsMode.java" - "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/RoundingMode.java" - "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/UnknownExplanation.java" + "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/BlockModelsMode.java" + "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/RoundingMode.java" + "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/UnknownExplanation.java" ) add_custom_command( OUTPUT @@ -51,7 +51,7 @@ add_custom_command( "${PYTHON_EXECUTABLE}" "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" --enums-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_types.h" - --java-api-path "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/" + --java-api-path "${CMAKE_CURRENT_BINARY_DIR}/io/github/" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" "${PROJECT_SOURCE_DIR}/src/api/parseenums.py" @@ -65,35 +65,49 @@ include(UseJava) # specify java source files set(JAVA_FILES - ${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/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/SynthResult.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 + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/AbstractPointer.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/CVC5ApiException.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/CVC5ApiOptionException.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/CVC5ApiRecoverableException.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Datatype.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/DatatypeConstructor.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/DatatypeConstructorDecl.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/DatatypeDecl.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/DatatypeSelector.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Grammar.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/IPointer.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Op.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/OptionInfo.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Pair.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Result.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Solver.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Sort.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Stat.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Statistics.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/SynthResult.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Term.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Triplet.java + ${CMAKE_CURRENT_LIST_DIR}/io/github/cvc5/Utils.java ${JAVA_KIND_FILE} ) # specify generated jni headers set(JNI_HEADERS - ${JNI_DIR}/io_github_cvc5_api_Solver.h + ${JNI_DIR}/io_github_cvc5_DatatypeConstructorDecl.h + ${JNI_DIR}/io_github_cvc5_DatatypeConstructor.h + ${JNI_DIR}/io_github_cvc5_DatatypeDecl.h + ${JNI_DIR}/io_github_cvc5_Datatype.h + ${JNI_DIR}/io_github_cvc5_DatatypeSelector.h + ${JNI_DIR}/io_github_cvc5_Grammar.h + ${JNI_DIR}/io_github_cvc5_Op.h + ${JNI_DIR}/io_github_cvc5_OptionInfo.h + ${JNI_DIR}/io_github_cvc5_Result.h + ${JNI_DIR}/io_github_cvc5_Solver.h + ${JNI_DIR}/io_github_cvc5_Sort.h + ${JNI_DIR}/io_github_cvc5_Stat.h + ${JNI_DIR}/io_github_cvc5_Statistics.h + ${JNI_DIR}/io_github_cvc5_SynthResult.h + ${JNI_DIR}/io_github_cvc5_Term.h ) # generate jni headers diff --git a/src/api/java/genenums.py.in b/src/api/java/genenums.py.in index b9d4a3026..a83076486 100644 --- a/src/api/java/genenums.py.in +++ b/src/api/java/genenums.py.in @@ -34,7 +34,7 @@ DEFAULT_PREFIX = 'Kind' # Code Blocks ENUM_JAVA_TOP = \ - r"""package io.github.cvc5.{namespace}; + r"""package io.github.{namespace}; import java.util.HashMap; import java.util.Map; @@ -161,11 +161,7 @@ def format_comment(comment): def gen_java(parser: EnumParser, path): for namespace in parser.namespaces: for enum in namespace.enums: - subnamespace = namespace.name.split('::')[-1] - # Workaround to make it work without moving the java files. Will be - # done in a subsequent PR by Andres - if subnamespace == 'cvc5': - subnamespace = 'api' + subnamespace = namespace.name.replace('::', '.') filedir = os.path.join(path, subnamespace) if not os.path.exists(filedir): os.mkdir(filedir) diff --git a/src/api/java/io/github/cvc5/AbstractPointer.java b/src/api/java/io/github/cvc5/AbstractPointer.java new file mode 100644 index 000000000..d9636807a --- /dev/null +++ b/src/api/java/io/github/cvc5/AbstractPointer.java @@ -0,0 +1,58 @@ +/****************************************************************************** + * 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 io.github.cvc5; + +abstract class AbstractPointer implements IPointer +{ + protected final Solver solver; + protected long pointer; + + public long getPointer() + { + return pointer; + } + + protected abstract void deletePointer(long pointer); + + void deletePointer() + { + if (pointer != 0) + { + deletePointer(pointer); + } + pointer = 0; + } + + 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; + solver.addAbstractPointer(this); + } +} diff --git a/src/api/java/io/github/cvc5/CVC5ApiException.java b/src/api/java/io/github/cvc5/CVC5ApiException.java new file mode 100644 index 000000000..e883b70d0 --- /dev/null +++ b/src/api/java/io/github/cvc5/CVC5ApiException.java @@ -0,0 +1,24 @@ +/****************************************************************************** + * 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 io.github.cvc5; + +public class CVC5ApiException extends Exception +{ + public CVC5ApiException(String message) + { + super(message); + } +} diff --git a/src/api/java/io/github/cvc5/CVC5ApiOptionException.java b/src/api/java/io/github/cvc5/CVC5ApiOptionException.java new file mode 100644 index 000000000..f2a4c2706 --- /dev/null +++ b/src/api/java/io/github/cvc5/CVC5ApiOptionException.java @@ -0,0 +1,24 @@ +/****************************************************************************** + * 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 io.github.cvc5; + +public class CVC5ApiOptionException extends CVC5ApiRecoverableException +{ + public CVC5ApiOptionException(String message) + { + super(message); + } +} diff --git a/src/api/java/io/github/cvc5/CVC5ApiRecoverableException.java b/src/api/java/io/github/cvc5/CVC5ApiRecoverableException.java new file mode 100644 index 000000000..20b61201f --- /dev/null +++ b/src/api/java/io/github/cvc5/CVC5ApiRecoverableException.java @@ -0,0 +1,24 @@ +/****************************************************************************** + * 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 io.github.cvc5; + +public class CVC5ApiRecoverableException extends CVC5ApiException +{ + public CVC5ApiRecoverableException(String message) + { + super(message); + } +} diff --git a/src/api/java/io/github/cvc5/Datatype.java b/src/api/java/io/github/cvc5/Datatype.java new file mode 100644 index 000000000..677ae7909 --- /dev/null +++ b/src/api/java/io/github/cvc5/Datatype.java @@ -0,0 +1,240 @@ +/****************************************************************************** + * 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 io.github.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 native void deletePointer(long pointer); + + public long getPointer() + { + return 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. + * @param name the name of the datatype constructor + * @return a Term representing the datatype constructor with the given name + */ + 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); + + /** + * @apiNote This method is experimental and may change in future versions. + * + * @return the parameters of this datatype, if it is parametric. An exception + * is thrown if this datatype is not parametric. + */ + public Sort[] getParameters() + { + long[] sortPointers = getParameters(pointer); + Sort[] sorts = Utils.getSorts(solver, sortPointers); + return sorts; + } + + private native long[] getParameters(long pointer); + + /** + * @apiNote This method is experimental and may change in future versions. + * + * @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); + + /** + * @apiNote This method is experimental and may change in future versions. + * + * @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); + + /** + * @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/io/github/cvc5/DatatypeConstructor.java b/src/api/java/io/github/cvc5/DatatypeConstructor.java new file mode 100644 index 000000000..e7d8182f9 --- /dev/null +++ b/src/api/java/io/github/cvc5/DatatypeConstructor.java @@ -0,0 +1,201 @@ +/****************************************************************************** + * 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 io.github.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 native void deletePointer(long pointer); + + public long getPointer() + { + return 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. + * + * @apiNote This method is experimental and may change in future versions. + * + * @param retSort the desired return sort of the constructor + * @return the constructor term + */ + public Term getInstantiatedConstructorTerm(Sort retSort) + { + long termPointer = getInstantiatedConstructorTerm(pointer, retSort.getPointer()); + return new Term(solver, termPointer); + } + + private native long getInstantiatedConstructorTerm(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); + + /** + * Get the DatatypeSelector at the given index + * @param index the given index i + * @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/io/github/cvc5/DatatypeConstructorDecl.java b/src/api/java/io/github/cvc5/DatatypeConstructorDecl.java new file mode 100644 index 000000000..45e79f1f1 --- /dev/null +++ b/src/api/java/io/github/cvc5/DatatypeConstructorDecl.java @@ -0,0 +1,73 @@ +/****************************************************************************** + * 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 io.github.cvc5; + +public class DatatypeConstructorDecl extends AbstractPointer +{ + // region construction and destruction + DatatypeConstructorDecl(Solver solver, long pointer) + { + super(solver, pointer); + } + + protected native void deletePointer(long pointer); + + public long getPointer() + { + return pointer; + } + + // endregion + + /** + * Add datatype selector declaration. + * @param name the name of the datatype selector declaration to add + * @param sort the codomain 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 codomain 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/io/github/cvc5/DatatypeDecl.java b/src/api/java/io/github/cvc5/DatatypeDecl.java new file mode 100644 index 000000000..3c15a049d --- /dev/null +++ b/src/api/java/io/github/cvc5/DatatypeDecl.java @@ -0,0 +1,83 @@ +/****************************************************************************** + * 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 io.github.cvc5; + +public class DatatypeDecl extends AbstractPointer +{ + // region construction and destruction + DatatypeDecl(Solver solver, long pointer) + { + super(solver, pointer); + } + + protected native void deletePointer(long pointer); + + public long getPointer() + { + return 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); + + /** @return true if this datatype is 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/io/github/cvc5/DatatypeSelector.java b/src/api/java/io/github/cvc5/DatatypeSelector.java new file mode 100644 index 000000000..4f64c045c --- /dev/null +++ b/src/api/java/io/github/cvc5/DatatypeSelector.java @@ -0,0 +1,90 @@ +/****************************************************************************** + * 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 io.github.cvc5; + +public class DatatypeSelector extends AbstractPointer +{ + // region construction and destruction + DatatypeSelector(Solver solver, long pointer) + { + super(solver, pointer); + } + + protected native void deletePointer(long pointer); + + public long getPointer() + { + return pointer; + } + + // endregion + + /** @return the name of this Datatype selector. */ + public 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 codomain sort of this selector. */ + public Sort getCodomainSort() + { + long sortPointer = getCodomainSort(pointer); + return new Sort(solver, sortPointer); + } + + private native long getCodomainSort(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/io/github/cvc5/Grammar.java b/src/api/java/io/github/cvc5/Grammar.java new file mode 100644 index 000000000..36c6ad789 --- /dev/null +++ b/src/api/java/io/github/cvc5/Grammar.java @@ -0,0 +1,94 @@ +/****************************************************************************** + * 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 io.github.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 native void deletePointer(long pointer); + + public long getPointer() + { + return 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/io/github/cvc5/IPointer.java b/src/api/java/io/github/cvc5/IPointer.java new file mode 100644 index 000000000..fb235944a --- /dev/null +++ b/src/api/java/io/github/cvc5/IPointer.java @@ -0,0 +1,20 @@ +/****************************************************************************** + * 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 io.github.cvc5; + +interface IPointer { + long getPointer(); +} diff --git a/src/api/java/io/github/cvc5/Op.java b/src/api/java/io/github/cvc5/Op.java new file mode 100644 index 000000000..68a24fb42 --- /dev/null +++ b/src/api/java/io/github/cvc5/Op.java @@ -0,0 +1,121 @@ +/****************************************************************************** + * 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 io.github.cvc5; + +public class Op extends AbstractPointer +{ + // region construction and destruction + Op(Solver solver, long pointer) + { + super(solver, pointer); + } + + protected native void deletePointer(long pointer); + + public long getPointer() + { + return 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 index at position i. + * @param i the position of the index to return + * @return the index at position i + */ + public Term get(int i) throws CVC5ApiException + { + Utils.validateUnsigned(i, "index"); + long termPointer = get(pointer, i); + return new Term(solver, termPointer); + } + + private native long get(long pointer, int i); + + /** + * @return a string representation of this operator + */ + protected native String toString(long pointer); +} diff --git a/src/api/java/io/github/cvc5/OptionInfo.java b/src/api/java/io/github/cvc5/OptionInfo.java new file mode 100644 index 000000000..bd8edc8b0 --- /dev/null +++ b/src/api/java/io/github/cvc5/OptionInfo.java @@ -0,0 +1,209 @@ +/****************************************************************************** + * 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 io.github.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 native void deletePointer(long pointer); + + public long getPointer() + { + return pointer; + } + + public String toString() + { + return toString(pointer); + } + + /** + * @return a string representation of this optionInfo. + */ + protected native String toString(long pointer); + + // endregion + + /** Abstract class for OptionInfo values */ + public abstract class BaseInfo + { + } + + /** Has the current and the default value */ + public 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/io/github/cvc5/Pair.java b/src/api/java/io/github/cvc5/Pair.java new file mode 100644 index 000000000..d2bd1ff8a --- /dev/null +++ b/src/api/java/io/github/cvc5/Pair.java @@ -0,0 +1,38 @@ +/****************************************************************************** + * 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 io.github.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; + + return first.equals(((Pair) pair).first) && second.equals(((Pair) pair).second); + } +} diff --git a/src/api/java/io/github/cvc5/Result.java b/src/api/java/io/github/cvc5/Result.java new file mode 100644 index 000000000..7607e6276 --- /dev/null +++ b/src/api/java/io/github/cvc5/Result.java @@ -0,0 +1,127 @@ +/****************************************************************************** + * 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 io.github.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 native void deletePointer(long pointer); + + public long getPointer() + { + return pointer; + } + + // endregion + + /** + * @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 isUnknown() + { + return isUnknown(pointer); + } + + private native boolean isUnknown(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/io/github/cvc5/Solver.java b/src/api/java/io/github/cvc5/Solver.java new file mode 100644 index 000000000..686a16c72 --- /dev/null +++ b/src/api/java/io/github/cvc5/Solver.java @@ -0,0 +1,2833 @@ +/****************************************************************************** + * 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 io.github.cvc5; + +import java.io.IOException; +import java.util.*; + +public class Solver implements IPointer, AutoCloseable +{ + private long pointer; + + public long getPointer() + { + return pointer; + } + + private native long newSolver(); + + public void deletePointer() + { + if (pointer != 0) + { + deletePointer(pointer); + } + pointer = 0; + } + + private static native void deletePointer(long pointer); + + // store pointers for terms, sorts, etc + List abstractPointers = new ArrayList<>(); + + @Override + public void close() + { + // delete heap memory for terms, sorts, etc + for (int i = abstractPointers.size() - 1; i >= 0; i--) + { + abstractPointers.get(i).deletePointer(); + } + // delete the heap memory for this solver + deletePointer(); + } + + void addAbstractPointer(AbstractPointer abstractPointer) + { + abstractPointers.add(abstractPointer); + } + + 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 + * @throws CVC5ApiException + */ + 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 + * @throws CVC5ApiException + */ + 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. + * @throws CVC5ApiException + */ + 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 + * @throws CVC5ApiException + */ + 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 + * @throws CVC5ApiException + */ + 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 + * @throws CVC5ApiException + */ + 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. + * + * @apiNote Create unresolved sorts with Solver::mkUnresolvedSort(). + * + * @param dtypedecls the datatype declarations from which the sort is + * created + * @param unresolvedSorts the set of unresolved sorts + * @return the datatype sorts + * @throws CVC5ApiException + */ + 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. + * + * @apiNote This method is experimental and may change in future versions. + * + * @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 + * + * @apiNote This method is experimental and may change in future versions. + * + * @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 an unresolved sort. + * + * This is for creating yet unresolved sort placeholders for mutually + * recursive datatypes. + * + * @param symbol the symbol of the sort + * @param arity the number of sort parameters of the sort + * @return the unresolved sort + * @throws CVC5ApiException + */ + public Sort mkUnresolvedSort(String symbol, int arity) throws CVC5ApiException + { + Utils.validateUnsigned(arity, "arity"); + long sortPointer = mkUnresolvedSort(pointer, symbol, arity); + return new Sort(this, sortPointer); + } + + private native long mkUnresolvedSort(long pointer, String symbol, int arity); + + /** + * Create an unresolved sort. + * + * This is for creating yet unresolved sort placeholders for mutually + * recursive datatypes without sort parameters. + * + * @param symbol the symbol of the sort + * @return the unresolved sort + * @throws CVC5ApiException + */ + public Sort mkUnresolvedSort(String symbol) throws CVC5ApiException + { + return mkUnresolvedSort(symbol, 0); + } + + /** + * Create a sort constructor sort. + * + * An uninterpreted sort constructor is an uninterpreted sort with + * arity > 0. + * + * @param symbol the symbol of the sort + * @param arity the arity of the sort (must be > 0) + * @return the sort constructor sort + * @throws CVC5ApiException + */ + public Sort mkUninterpretedSortConstructorSort(String symbol, int arity) throws CVC5ApiException + { + Utils.validateUnsigned(arity, "arity"); + long sortPointer = mkUninterpretedSortConstructorSort(pointer, symbol, arity); + return new Sort(this, sortPointer); + } + + private native long mkUninterpretedSortConstructorSort(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). + * + * @apiNote 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 {@link 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 {@link Kind} for a description of the parameters. + * @param kind the kind of the operator + * @param arg the unsigned int argument to this operator + * @throws CVC5ApiException + */ + 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_FROM_IEEE_BV + * - FLOATINGPOINT_TO_FP_FROM_FP + * - FLOATINGPOINT_TO_FP_FROM_REAL + * - FLOATINGPOINT_TO_FP_FROM_SBV + * - FLOATINGPOINT_TO_FP_FROM_UBV + * See enum {@link 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 + * @throws CVC5ApiException + */ + 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 {@link Kind} for a description of the parameters. + * @param kind the kind of the operator + * @param args the arguments (indices) of the operator + * @throws CVC5ApiException + */ + 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) + * @throws CVC5ApiException + */ + 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 + * @throws CVC5ApiException + */ + 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 none (re.none) term. + * @return the none term + */ + public Term mkRegexpNone() + { + long termPointer = mkRegexpNone(pointer); + return new Term(this, termPointer); + } + + private native long mkRegexpNone(long pointer); + + /** + * Create a regular expression all (re.all) term. + * @return the all term + */ + public Term mkRegexpAll() + { + long termPointer = mkRegexpAll(pointer); + return new Term(this, termPointer); + } + + private native long mkRegexpAll(long pointer); + + /** + * Create a regular expression allchar (re.allchar) term. + * @return the allchar term + */ + public Term mkRegexpAllchar() + { + long termPointer = mkRegexpAllchar(pointer); + return new Term(this, termPointer); + } + + private native long mkRegexpAllchar(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. + * + * @apiNote This method is experimental and may change in future versions. + * + * @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. + * + * @apiNote This method is experimental and may change in future versions. + * + * @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 + * @throws CVC5ApiException + */ + 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. + * + * @apiNote 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 + * @throws CVC5ApiException + */ + 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. + * + * @apiNote 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 + * @throws CVC5ApiException + */ + 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 + * @throws CVC5ApiException + */ + public Term mkFloatingPointPosInf(int exp, int sig) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long termPointer = mkFloatingPointPosInf(pointer, exp, sig); + return new Term(this, termPointer); + } + + private native long mkFloatingPointPosInf(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 + * @throws CVC5ApiException + */ + public Term mkFloatingPointNegInf(int exp, int sig) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long termPointer = mkFloatingPointNegInf(pointer, exp, sig); + return new Term(this, termPointer); + } + + private native long mkFloatingPointNegInf(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 + * @throws CVC5ApiException + */ + public Term mkFloatingPointNaN(int exp, int sig) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long termPointer = mkFloatingPointNaN(pointer, exp, sig); + return new Term(this, termPointer); + } + + private native long mkFloatingPointNaN(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 + * @throws CVC5ApiException + */ + public Term mkFloatingPointPosZero(int exp, int sig) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long termPointer = mkFloatingPointPosZero(pointer, exp, sig); + return new Term(this, termPointer); + } + + private native long mkFloatingPointPosZero(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 + * @throws CVC5ApiException + */ + public Term mkFloatingPointNegZero(int exp, int sig) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long termPointer = mkFloatingPointNegZero(pointer, exp, sig); + return new Term(this, termPointer); + } + + private native long mkFloatingPointNegZero(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 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 + * @throws CVC5ApiException + */ + 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 a cardinality constraint for an uninterpreted sort. + * + * @apiNote This method is experimental and may change in future versions. + * + * @param sort the sort the cardinality constraint is for + * @param upperBound the upper bound on the cardinality of the sort + * @return the cardinality constraint + * @throws CVC5ApiException + */ + public Term mkCardinalityConstraint(Sort sort, int upperBound) throws CVC5ApiException + { + Utils.validateUnsigned(upperBound, "upperBound"); + long termPointer = mkCardinalityConstraint(pointer, sort.getPointer(), upperBound); + return new Term(this, termPointer); + } + + private native long mkCardinalityConstraint(long pointer, long sortPointer, int upperBound); + + /* .................................................................... */ + /* 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 */ + /* .................................................................... */ + + /** + * Create a datatype constructor declaration. + * @param name the name of the datatype constructor + * @return the DatatypeConstructorDecl + */ + 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. + * + * @apiNote This method is experimental and may change in future versions. + * + * @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); + + /** + * 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 ) + * } + * + * @apiNote This corresponds to mkUninterpretedSort() const if arity = 0, and + * to mkUninterpretedSortConstructorSort() const if arity > 0. + * + * @param symbol the name of the sort + * @param arity the arity of the sort + * @return the sort + * @throws CVC5ApiException + */ + 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 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); + + /** + * Get a list of literals that are entailed by the current set of assertions + * SMT-LIB: + * {@code + * ( get-learned-literals ) + * } + * + * @apiNote This method is experimental and may change in future versions. + * + * @return the list of learned literals + */ + public Term[] getLearnedLiterals() + { + long[] retPointers = getLearnedLiterals(pointer); + return Utils.getTerms(this, retPointers); + } + + private native long[] getLearnedLiterals(long pointer); + + /** + * 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'. + * + * @apiNote In contrast to SMT-LIB, the API does not distinguish between + * named and unnamed assertions when producing an unsatisfiable + * core. Additionally, the API allows this option to be called after + * a check with assumptions. A subset of those assumptions may be + * included in the unsatisfiable core returned by this method. + * + * @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. + * + * @apiNote This method is experimental and may change in future versions. + * + * @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'. + * + * @apiNote This method is experimental and may change in future versions. + * + * @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. + * + * @apiNote This method is experimental and may change in future versions. + * + * @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'. + * + * @apiNote This method is experimental and may change in future versions. + * + * @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 ) + * } + * Quantifier Elimination is is only complete for logics such as LRA, + * LIA and BV. + * + * @apiNote This method is experimental and may change in future versions. + * + * @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 ) + * } + * Quantifier Elimination is is only complete for logics such as LRA, + * LIA and BV. + * + * @apiNote This method is experimental and may change in future versions. + * + * @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. + * + * @apiNote This method is experimental and may change in future versions. + * + * @param locSort The location sort of the heap + * @param dataSort The data sort of the heap + */ + public void declareSepHeap(Sort locSort, Sort dataSort) + { + declareSepHeap(pointer, locSort.getPointer(), dataSort.getPointer()); + } + + private native void declareSepHeap(long pointer, long locSortPointer, long dataSortPointer); + + /** + * When using separation logic, obtain the term for the heap. + * + * @apiNote This method is experimental and may change in future versions. + * + * @return The term for the heap + */ + public Term getValueSepHeap() + { + long termPointer = getValueSepHeap(pointer); + return new Term(this, termPointer); + } + + private native long getValueSepHeap(long pointer); + + /** + * When using separation logic, obtain the term for nil. + * + * @apiNote This method is experimental and may change in future versions. + * + * @return The term for nil + */ + public Term getValueSepNil() + { + long termPointer = getValueSepNil(pointer); + return new Term(this, termPointer); + } + + private native long getValueSepNil(long pointer); + + /** + * Declare a symbolic pool of terms with the given initial value. + * SMT-LIB: + * {@code + * ( declare-pool ( * ) ) + * } + * + * @apiNote This method is experimental and may change in future versions. + * + * @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 ) + * } + * @throws CVC5ApiException + */ + 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 + * @throws CVC5ApiException + */ + 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-interpolant ) + * } + * Requires 'produce-interpolants' to be set to a mode different from 'none'. + * + * @apiNote This method is experimental and may change in future versions. + * + * @param conj the conjecture term + * @return 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, or the null term if such a term cannot be found. + */ + public Term getInterpolant(Term conj) + { + long interpolPtr = getInterpolant(pointer, conj.getPointer()); + return new Term(this, interpolPtr); + } + + private native long getInterpolant(long pointer, long conjPointer); + + /** + * Get an interpolant + * SMT-LIB: + * {@code + * ( get-interpolant ) + * } + * Requires 'produce-interpolants' to be set to a mode different from 'none'. + * + * @apiNote This method is experimental and may change in future versions. + * + * @param conj the conjecture term + * @param grammar the grammar for the interpolant I + * @return 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, or the null term if such a term cannot be found. + */ + public Term getInterpolant(Term conj, Grammar grammar) + { + long interpolPtr = getInterpolant(pointer, conj.getPointer(), grammar.getPointer()); + return new Term(this, interpolPtr); + } + + private native long getInterpolant(long pointer, long conjPointer, long grammarPointer); + + /** + * Get the next interpolant. Can only be called immediately after a successful + * call to get-interpolant or get-interpolant-next. Is guaranteed to produce a + * syntactically different interpolant wrt the last returned interpolant if + * successful. + * + * SMT-LIB: + * + * \verbatim embed:rst:leading-asterisk + * .. code:: smtlib + * + * (get-interpolant-next) + * + * Requires to enable incremental mode, and option 'produce-interpolants' to be + * set to a mode different from 'none'. + * \endverbatim + * + * @apiNote This method is experimental and may change in future versions. + * + * @return 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 on the last call to getInterpolant, or the null term if such + * a term cannot be found. + */ + public Term getInterpolantNext() + { + long interpolPtr = getInterpolantNext(pointer); + return new Term(this, interpolPtr); + } + + private native long getInterpolantNext(long pointer); + + /** + * Get an abduct. + * SMT-LIB: + * {@code + * ( get-abduct ) + * } + * Requires enabling option 'produce-abducts' + * + * @apiNote This method is experimental and may change in future versions. + * + * @param conj the conjecture term + * @return 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, or the null term if such a term cannot + * be found. + */ + public Term getAbduct(Term conj) + { + long abdPtr = getAbduct(pointer, conj.getPointer()); + return new Term(this, abdPtr); + } + + private native long getAbduct(long pointer, long conjPointer); + /** + * Get an abduct. + * SMT-LIB: + * {@code + * ( get-abduct ) + * } + * Requires enabling option 'produce-abducts' + * + * @apiNote This method is experimental and may change in future versions. + * + * @param conj the conjecture term + * @param grammar the grammar for the abduct C + * @return 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, or the null term if such a term cannot + * be found. + */ + public Term getAbduct(Term conj, Grammar grammar) + { + long abdPtr = getAbduct(pointer, conj.getPointer(), grammar.getPointer()); + return new Term(this, abdPtr); + } + + private native long getAbduct(long pointer, long conjPointer, long grammarPointer); + + /** + * Get the next abduct. Can only be called immediately after a successful + * call to get-abduct or get-abduct-next. Is guaranteed to produce a + * syntactically different abduct wrt the last returned abduct if successful. + * SMT-LIB: + * {@code + * ( get-abduct-next ) + * } + * Requires enabling incremental mode and option 'produce-abducts' + * + * @apiNote This method is experimental and may change in future versions. + * + * @return 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 in the last call to getAbduct, or the + * null term if such a term cannot be found. + */ + public Term getAbductNext() + { + long abdPtr = getAbductNext(pointer); + return new Term(this, abdPtr); + } + + private native long getAbductNext(long pointer); + + /** + * 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". + * + * @apiNote This method is experimental and may change in future versions. + */ + 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. + * + * @apiNote This method is experimental and may change in future versions. + */ + public void blockModelValues(Term[] terms) + { + long[] pointers = Utils.getPointers(terms); + blockModelValues(pointer, pointers); + } + + private native void blockModelValues(long pointer, long[] termPointers); + + /** + * Return a string that contains information about all instantiations made by + * the quantifiers module. + * + * @apiNote This method is experimental and may change in future versions. + */ + public String getInstantiations() + { + return getInstantiations(pointer); + } + + private native String getInstantiations(long pointer); + + /** + * Push a level to the assertion stack. + * SMT-LIB: + * {@code + * ( push ) + * } + * @throws CVC5ApiException + */ + 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 + * @throws CVC5ApiException + */ + 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 + * @throws CVC5ApiException + */ + 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 + * @throws CVC5ApiException + */ + 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