From 720e3afc907f429cf8105ee49b3628ddaacbf7a3 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Thu, 30 Sep 2021 12:07:39 -0500 Subject: [PATCH] Finish the Java Api (#6396) This commit finishes the implementation of the Java API. It also includes all java files in the build along with their unit tests. --- .clang-format | 14 +- src/api/java/CMakeLists.txt | 28 +- src/api/java/cvc5/AbstractPointer.java | 40 + .../cvc5/CVC5ApiRecoverableException.java | 1 - src/api/java/cvc5/Datatype.java | 41 +- src/api/java/cvc5/DatatypeConstructor.java | 55 +- .../java/cvc5/DatatypeConstructorDecl.java | 3 +- src/api/java/cvc5/DatatypeDecl.java | 3 +- src/api/java/cvc5/DatatypeSelector.java | 3 +- src/api/java/cvc5/Grammar.java | 31 +- src/api/java/cvc5/IPointer.java | 3 +- src/api/java/cvc5/Op.java | 42 +- src/api/java/cvc5/Pair.java | 41 + src/api/java/cvc5/Result.java | 6 +- src/api/java/cvc5/RoundingMode.java | 63 + src/api/java/cvc5/Solver.java | 2483 +++++++++++++++- src/api/java/cvc5/Sort.java | 13 +- src/api/java/cvc5/Stat.java | 33 +- src/api/java/cvc5/Statistics.java | 134 +- src/api/java/cvc5/Term.java | 185 +- src/api/java/cvc5/Utils.java | 182 +- src/api/java/jni/cvc5JavaApi.h | 48 + src/api/java/jni/cvc5_Solver.cpp | 2531 ++++++++++++++++- src/api/java/jni/cvc5_Term.cpp | 31 + test/unit/api/java/CMakeLists.txt | 9 +- test/unit/api/java/cvc5/GrammarTest.java | 56 +- test/unit/api/java/cvc5/OpTest.java | 83 +- test/unit/api/java/cvc5/SolverTest.java | 2315 ++++++++++++++- test/unit/api/java/cvc5/SortTest.java | 38 +- test/unit/api/java/cvc5/TermTest.java | 168 +- 30 files changed, 8239 insertions(+), 444 deletions(-) create mode 100644 src/api/java/cvc5/AbstractPointer.java create mode 100644 src/api/java/cvc5/Pair.java create mode 100644 src/api/java/cvc5/RoundingMode.java diff --git a/.clang-format b/.clang-format index a4e83f330..fc35b4e00 100644 --- a/.clang-format +++ b/.clang-format @@ -20,8 +20,20 @@ DerivePointerAlignment: false --- Language: Java BasedOnStyle: Google -ColumnLimit: 80 +AllowShortCaseLabelsOnASingleLine: true BinPackArguments: false BinPackParameters: false BreakBeforeBinaryOperators: NonAssignment +BraceWrapping: + AfterCaseLabel: true + AfterClass: true + AfterControlStatement: true + AfterEnum: true + AfterFunction: true + AfterStruct: true + AfterUnion: true + BeforeCatch: true + BeforeElse: true +BreakBeforeBraces: Custom +DerivePointerAlignment: false ... diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index d1e818f30..69605c06a 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -48,10 +48,25 @@ include(UseJava) # specify java source files set(JAVA_FILES + ${CMAKE_CURRENT_LIST_DIR}/cvc5/AbstractPointer.java ${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiException.java ${CMAKE_CURRENT_LIST_DIR}/cvc5/CVC5ApiRecoverableException.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Datatype.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/DatatypeConstructor.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/DatatypeConstructorDecl.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/DatatypeDecl.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/DatatypeSelector.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Grammar.java ${CMAKE_CURRENT_LIST_DIR}/cvc5/IPointer.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Op.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Pair.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Result.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/RoundingMode.java ${CMAKE_CURRENT_LIST_DIR}/cvc5/Solver.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Sort.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Stat.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Statistics.java + ${CMAKE_CURRENT_LIST_DIR}/cvc5/Term.java ${CMAKE_CURRENT_LIST_DIR}/cvc5/Utils.java ${JAVA_KIND_FILE} ) @@ -92,8 +107,19 @@ message(STATUS "JAVA_INCLUDE_PATH2 : ${JAVA_INCLUDE_PATH2}") message(STATUS "JAVA_AWT_INCLUDE_PATH: ${JAVA_AWT_INCLUDE_PATH}") add_library(cvc5jni SHARED + jni/cvc5_Datatype.cpp + jni/cvc5_DatatypeConstructor.cpp + jni/cvc5_DatatypeConstructorDecl.cpp + jni/cvc5_DatatypeDecl.cpp + jni/cvc5_DatatypeSelector.cpp + jni/cvc5_Grammar.cpp + jni/cvc5_Op.cpp + jni/cvc5_Result.cpp jni/cvc5_Solver.cpp -) + jni/cvc5_Sort.cpp + jni/cvc5_Stat.cpp + jni/cvc5_Statistics.cpp + jni/cvc5_Term.cpp) add_dependencies(cvc5jni generate-jni-headers) target_include_directories(cvc5jni PUBLIC ${JNI_INCLUDE_DIRS}) diff --git a/src/api/java/cvc5/AbstractPointer.java b/src/api/java/cvc5/AbstractPointer.java new file mode 100644 index 000000000..f6cdff8ad --- /dev/null +++ b/src/api/java/cvc5/AbstractPointer.java @@ -0,0 +1,40 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 java API. + */ + +package cvc5; + +abstract class AbstractPointer implements IPointer +{ + protected final Solver solver; + protected final long pointer; + + public long getPointer() + { + return pointer; + } + + @Override public String toString() + { + return toString(pointer); + } + + abstract protected String toString(long pointer); + + AbstractPointer(Solver solver, long pointer) + { + this.solver = solver; + this.pointer = pointer; + } +} diff --git a/src/api/java/cvc5/CVC5ApiRecoverableException.java b/src/api/java/cvc5/CVC5ApiRecoverableException.java index 3f434d0ff..035a79ab6 100644 --- a/src/api/java/cvc5/CVC5ApiRecoverableException.java +++ b/src/api/java/cvc5/CVC5ApiRecoverableException.java @@ -13,7 +13,6 @@ * The cvc5 java API. */ - package cvc5; public class CVC5ApiRecoverableException extends CVC5ApiException diff --git a/src/api/java/cvc5/Datatype.java b/src/api/java/cvc5/Datatype.java index be1e47671..42e06286c 100644 --- a/src/api/java/cvc5/Datatype.java +++ b/src/api/java/cvc5/Datatype.java @@ -15,7 +15,10 @@ package cvc5; -public class Datatype extends AbstractPointer +import java.util.Iterator; +import java.util.NoSuchElementException; + +public class Datatype extends AbstractPointer implements Iterable { // region construction and destruction Datatype(Solver solver, long pointer) @@ -30,8 +33,7 @@ public class Datatype extends AbstractPointer return pointer; } - @Override - public void finalize() + @Override public void finalize() { deletePointer(pointer); } @@ -195,4 +197,37 @@ public class Datatype extends AbstractPointer * @return a string representation of this datatype */ protected native String toString(long pointer); + + public class ConstIterator implements Iterator + { + private int currentIndex; + private int size; + + public ConstIterator() + { + currentIndex = -1; + size = getNumConstructors(); + } + + @Override public boolean hasNext() + { + return currentIndex < size - 1; + } + + @Override public DatatypeConstructor next() + { + if (currentIndex >= size - 1) + { + throw new NoSuchElementException(); + } + currentIndex++; + + return getConstructor(currentIndex); + } + } + + @Override public Iterator iterator() + { + return new ConstIterator(); + } } diff --git a/src/api/java/cvc5/DatatypeConstructor.java b/src/api/java/cvc5/DatatypeConstructor.java index eb489456b..7c0ee21d5 100644 --- a/src/api/java/cvc5/DatatypeConstructor.java +++ b/src/api/java/cvc5/DatatypeConstructor.java @@ -15,7 +15,10 @@ package cvc5; -public class DatatypeConstructor extends AbstractPointer +import java.util.Iterator; +import java.util.NoSuchElementException; + +public class DatatypeConstructor extends AbstractPointer implements Iterable { // region construction and destruction DatatypeConstructor(Solver solver, long pointer) @@ -30,8 +33,7 @@ public class DatatypeConstructor extends AbstractPointer return pointer; } - @Override - public void finalize() + @Override public void finalize() { deletePointer(pointer); } @@ -39,7 +41,7 @@ public class DatatypeConstructor extends AbstractPointer // endregion /** @return the name of this Datatype constructor. */ - String getName() + public String getName() { return getName(pointer); } @@ -50,7 +52,7 @@ public class DatatypeConstructor extends AbstractPointer * Get the constructor operator of this datatype constructor. * @return the constructor term */ - Term getConstructorTerm() + public Term getConstructorTerm() { long termPointer = getConstructorTerm(pointer); return new Term(solver, termPointer); @@ -81,7 +83,7 @@ public class DatatypeConstructor extends AbstractPointer * @param retSort the desired return sort of the constructor * @return the constructor term */ - Term getSpecializedConstructorTerm(Sort retSort) + public Term getSpecializedConstructorTerm(Sort retSort) { long termPointer = getSpecializedConstructorTerm(pointer, retSort.getPointer()); return new Term(solver, termPointer); @@ -93,7 +95,7 @@ public class DatatypeConstructor extends AbstractPointer * Get the tester operator of this datatype constructor. * @return the tester operator */ - Term getTesterTerm() + public Term getTesterTerm() { long termPointer = getTesterTerm(pointer); return new Term(solver, termPointer); @@ -103,7 +105,7 @@ public class DatatypeConstructor extends AbstractPointer /** * @return the number of selectors (so far) of this Datatype constructor. */ - int getNumSelectors() + public int getNumSelectors() { return getNumSelectors(pointer); } @@ -138,7 +140,7 @@ public class DatatypeConstructor extends AbstractPointer * @param name the name of the datatype selector * @return a term representing the datatype selector with the given name */ - Term getSelectorTerm(String name) + public Term getSelectorTerm(String name) { long termPointer = getSelectorTerm(pointer, name); return new Term(solver, termPointer); @@ -148,7 +150,7 @@ public class DatatypeConstructor extends AbstractPointer /** * @return true if this DatatypeConstructor is a null object */ - boolean isNull() + public boolean isNull() { return isNull(pointer); } @@ -159,4 +161,37 @@ public class DatatypeConstructor extends AbstractPointer * @return a string representation of this datatype constructor */ protected native String toString(long pointer); + + public class ConstIterator implements Iterator + { + private int currentIndex; + private int size; + + public ConstIterator() + { + currentIndex = -1; + size = getNumSelectors(); + } + + @Override public boolean hasNext() + { + return currentIndex < size - 1; + } + + @Override public DatatypeSelector next() + { + if (currentIndex >= size - 1) + { + throw new NoSuchElementException(); + } + currentIndex++; + + return getSelector(currentIndex); + } + } + + @Override public Iterator iterator() + { + return new ConstIterator(); + } } diff --git a/src/api/java/cvc5/DatatypeConstructorDecl.java b/src/api/java/cvc5/DatatypeConstructorDecl.java index 8c1cfed7d..9769aa2fb 100644 --- a/src/api/java/cvc5/DatatypeConstructorDecl.java +++ b/src/api/java/cvc5/DatatypeConstructorDecl.java @@ -30,8 +30,7 @@ public class DatatypeConstructorDecl extends AbstractPointer return pointer; } - @Override - public void finalize() + @Override public void finalize() { deletePointer(pointer); } diff --git a/src/api/java/cvc5/DatatypeDecl.java b/src/api/java/cvc5/DatatypeDecl.java index 4be50f92f..fa78c68ac 100644 --- a/src/api/java/cvc5/DatatypeDecl.java +++ b/src/api/java/cvc5/DatatypeDecl.java @@ -30,8 +30,7 @@ public class DatatypeDecl extends AbstractPointer return pointer; } - @Override - public void finalize() + @Override public void finalize() { deletePointer(pointer); } diff --git a/src/api/java/cvc5/DatatypeSelector.java b/src/api/java/cvc5/DatatypeSelector.java index b4e9fd6b6..77136173e 100644 --- a/src/api/java/cvc5/DatatypeSelector.java +++ b/src/api/java/cvc5/DatatypeSelector.java @@ -30,8 +30,7 @@ public class DatatypeSelector extends AbstractPointer return pointer; } - @Override - public void finalize() + @Override public void finalize() { deletePointer(pointer); } diff --git a/src/api/java/cvc5/Grammar.java b/src/api/java/cvc5/Grammar.java index f8c6b05c5..72558d15b 100644 --- a/src/api/java/cvc5/Grammar.java +++ b/src/api/java/cvc5/Grammar.java @@ -15,20 +15,23 @@ package cvc5; -public class Grammar extends AbstractPointer { +public class Grammar extends AbstractPointer +{ // region construction and destruction - Grammar(Solver solver, long pointer) { + Grammar(Solver solver, long pointer) + { super(solver, pointer); } protected static native void deletePointer(long pointer); - public long getPointer() { + public long getPointer() + { return pointer; } - @Override - public void finalize() { + @Override public void finalize() + { deletePointer(pointer); } @@ -39,31 +42,32 @@ public class Grammar extends AbstractPointer { * @param ntSymbol the non-terminal to which the rule is added * @param rule the rule to add */ - public void addRule(Term ntSymbol, Term rule) { + public void addRule(Term ntSymbol, Term rule) + { addRule(pointer, ntSymbol.getPointer(), rule.getPointer()); } - private native void addRule( - long pointer, long ntSymbolPointer, long rulePointer); + 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) { + 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); + 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 */ - void addAnyConstant(Term ntSymbol) { + public void addAnyConstant(Term ntSymbol) + { addAnyConstant(pointer, ntSymbol.getPointer()); } @@ -74,7 +78,8 @@ public class Grammar extends AbstractPointer { * synth-fun/synth-inv with the same sort as \p ntSymbol. * @param ntSymbol the non-terminal allowed to be any input constant */ - void addAnyVariable(Term ntSymbol) { + public void addAnyVariable(Term ntSymbol) + { addAnyVariable(pointer, ntSymbol.getPointer()); } diff --git a/src/api/java/cvc5/IPointer.java b/src/api/java/cvc5/IPointer.java index fc9c95338..17d6d5974 100644 --- a/src/api/java/cvc5/IPointer.java +++ b/src/api/java/cvc5/IPointer.java @@ -15,7 +15,6 @@ package cvc5; -interface IPointer -{ +interface IPointer { long getPointer(); } diff --git a/src/api/java/cvc5/Op.java b/src/api/java/cvc5/Op.java index 98915c1d1..6819946b6 100644 --- a/src/api/java/cvc5/Op.java +++ b/src/api/java/cvc5/Op.java @@ -15,20 +15,23 @@ package cvc5; -public class Op extends AbstractPointer { +public class Op extends AbstractPointer +{ // region construction and destruction - Op(Solver solver, long pointer) { + Op(Solver solver, long pointer) + { super(solver, pointer); } protected static native void deletePointer(long pointer); - public long getPointer() { + public long getPointer() + { return pointer; } - @Override - public void finalize() { + @Override public void finalize() + { deletePointer(pointer); } @@ -41,8 +44,8 @@ public class Op extends AbstractPointer { * @param t the operator to compare to for equality * @return true if the operators are equal */ - @Override - public boolean equals(Object t) { + @Override public boolean equals(Object t) + { if (this == t) return true; if (t == null || getClass() != t.getClass()) @@ -55,11 +58,15 @@ public class Op extends AbstractPointer { /** * @return the kind of this operator */ - Kind getKind() { - try { + Kind getKind() + { + try + { int value = getKind(pointer); return Kind.fromInt(value); - } catch (CVC5ApiException e) { + } + catch (CVC5ApiException e) + { e.printStackTrace(); throw new RuntimeException(e.getMessage()); } @@ -70,7 +77,8 @@ public class Op extends AbstractPointer { /** * @return true if this operator is a null term */ - public boolean isNull() { + public boolean isNull() + { return isNull(pointer); } @@ -79,7 +87,8 @@ public class Op extends AbstractPointer { /** * @return true iff this operator is indexed */ - public boolean isIndexed() { + public boolean isIndexed() + { return isIndexed(pointer); } @@ -88,7 +97,8 @@ public class Op extends AbstractPointer { /** * @return the number of indices of this op */ - public int getNumIndices() { + public int getNumIndices() + { return getNumIndices(pointer); } @@ -100,7 +110,8 @@ public class Op extends AbstractPointer { * * @return the indices used to create this Op */ - public int[] getIntegerIndices() { + public int[] getIntegerIndices() + { return getIntegerIndices(pointer); } @@ -112,7 +123,8 @@ public class Op extends AbstractPointer { * * @return the indices used to create this Op */ - public String[] getStringIndices() { + public String[] getStringIndices() + { return getStringIndices(pointer); } diff --git a/src/api/java/cvc5/Pair.java b/src/api/java/cvc5/Pair.java new file mode 100644 index 000000000..19cd3e797 --- /dev/null +++ b/src/api/java/cvc5/Pair.java @@ -0,0 +1,41 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 java API. + */ + +package cvc5; + +public class Pair +{ + public K first; + public V second; + public Pair(K first, V second) + { + this.first = first; + this.second = second; + } + + @Override public boolean equals(Object pair) + { + if (this == pair) + return true; + if (pair == null || getClass() != pair.getClass()) + return false; + + Pair p = (Pair) pair; + + if (!first.equals(p.first)) + return false; + return second.equals(p.second); + } +} diff --git a/src/api/java/cvc5/Result.java b/src/api/java/cvc5/Result.java index 4399df1e4..3573094a3 100644 --- a/src/api/java/cvc5/Result.java +++ b/src/api/java/cvc5/Result.java @@ -33,16 +33,14 @@ public class Result extends AbstractPointer return pointer; } - @Override - public void finalize() + @Override public void finalize() { deletePointer(pointer); } // endregion - public enum UnknownExplanation - { + public enum UnknownExplanation { REQUIRES_FULL_CHECK(0), INCOMPLETE(1), TIMEOUT(2), diff --git a/src/api/java/cvc5/RoundingMode.java b/src/api/java/cvc5/RoundingMode.java new file mode 100644 index 000000000..4229bb74a --- /dev/null +++ b/src/api/java/cvc5/RoundingMode.java @@ -0,0 +1,63 @@ +/****************************************************************************** + * Top contributors (to current version): + * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * The cvc5 java API. + */ + +package cvc5; + +public enum RoundingMode { + /** + * Round to the nearest even number. + * If the two nearest floating-point numbers bracketing an unrepresentable + * infinitely precise result are equally near, the one with an even least + * significant digit will be delivered. + */ + ROUND_NEAREST_TIES_TO_EVEN(0), + /** + * Round towards positive infinity (+oo). + * The result shall be the format’s floating-point number (possibly +oo) + * closest to and no less than the infinitely precise result. + */ + ROUND_TOWARD_POSITIVE(1), + /** + * Round towards negative infinity (-oo). + * The result shall be the format’s floating-point number (possibly -oo) + * closest to and no less than the infinitely precise result. + */ + ROUND_TOWARD_NEGATIVE(2), + /** + * Round towards zero. + * The result shall be the format’s floating-point number closest to and no + * greater in magnitude than the infinitely precise result. + */ + ROUND_TOWARD_ZERO(3), + /** + * Round to the nearest number away from zero. + * If the two nearest floating-point numbers bracketing an unrepresentable + * infinitely precise result are equally near, the one with larger magnitude + * will be selected. + */ + ROUND_NEAREST_TIES_TO_AWAY(4); + + private int value; + + private RoundingMode(int value) + { + this.value = value; + } + + public int getValue() + { + return value; + } +} diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java index 6bb1b6b1e..65efcb170 100644 --- a/src/api/java/cvc5/Solver.java +++ b/src/api/java/cvc5/Solver.java @@ -16,6 +16,7 @@ package cvc5; import java.io.IOException; +import java.util.*; public class Solver implements IPointer { @@ -26,36 +27,2494 @@ public class Solver implements IPointer return pointer; } + private native long newSolver(); + + public void deletePointer() + { + deletePointer(pointer); + } + + private static native void deletePointer(long pointer); + + @Override public void finalize() + { + deletePointer(pointer); + } + + static + { + Utils.loadLibraries(); + } + + /* .................................................................... */ + /* Constructors */ + /* .................................................................... */ + public Solver() { - this.pointer = newSolver(); + this.pointer = newSolver(); + } + + /* .................................................................... */ + /* Sorts Handling */ + /* .................................................................... */ + + /** + * @return sort null + */ + + public Sort getNullSort() + { + long sortPointer = getNullSort(pointer); + return new Sort(this, sortPointer); + } + + private native long getNullSort(long pointer); + + /** + * @return sort Boolean + */ + public Sort getBooleanSort() + { + long sortPointer = getBooleanSort(pointer); + return new Sort(this, sortPointer); + } + + private native long getBooleanSort(long pointer); + + /** + * @return sort Integer (in cvc5, Integer is a subtype of Real) + */ + public Sort getIntegerSort() + { + long sortPointer = getIntegerSort(pointer); + return new Sort(this, sortPointer); + } + + public native long getIntegerSort(long pointer); + /** + * @return sort Real + */ + public Sort getRealSort() + { + long sortPointer = getRealSort(pointer); + return new Sort(this, sortPointer); + } + + private native long getRealSort(long pointer); + /** + * @return sort RegExp + */ + public Sort getRegExpSort() + { + long sortPointer = getRegExpSort(pointer); + return new Sort(this, sortPointer); + } + + private native long getRegExpSort(long pointer); + /** + * @return sort RoundingMode + */ + public Sort getRoundingModeSort() throws CVC5ApiException + { + long sortPointer = getRoundingModeSort(pointer); + return new Sort(this, sortPointer); + } + + private native long getRoundingModeSort(long pointer) throws CVC5ApiException; + /** + * @return sort String + */ + public Sort getStringSort() + { + long sortPointer = getStringSort(pointer); + return new Sort(this, sortPointer); + } + + private native long getStringSort(long solverPointer); + /** + * Create an array sort. + * @param indexSort the array index sort + * @param elemSort the array element sort + * @return the array sort + */ + public Sort mkArraySort(Sort indexSort, Sort elemSort) + { + long sortPointer = mkArraySort(pointer, indexSort.getPointer(), elemSort.getPointer()); + return new Sort(this, sortPointer); + } + + private native long mkArraySort(long pointer, long indexSortPointer, long elementSortPointer); + + /** + * Create a bit-vector sort. + * @param size the bit-width of the bit-vector sort + * @return the bit-vector sort + */ + public Sort mkBitVectorSort(int size) throws CVC5ApiException + { + Utils.validateUnsigned(size, "size"); + long sortPointer = mkBitVectorSort(pointer, size); + return new Sort(this, sortPointer); + } + + private native long mkBitVectorSort(long pointer, int size); + + /** + * Create a floating-point sort. + * @param exp the bit-width of the exponent of the floating-point sort. + * @param sig the bit-width of the significand of the floating-point sort. + */ + public Sort mkFloatingPointSort(int exp, int sig) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long sortPointer = mkFloatingPointSort(pointer, exp, sig); + return new Sort(this, sortPointer); + } + + private native long mkFloatingPointSort(long solverPointer, int exp, int sig); + + /** + * Create a datatype sort. + * @param dtypedecl the datatype declaration from which the sort is + * created + * @return the datatype sort + */ + public Sort mkDatatypeSort(DatatypeDecl dtypedecl) throws CVC5ApiException + { + long pointer = mkDatatypeSort(this.pointer, dtypedecl.getPointer()); + return new Sort(this, pointer); + } + + private native long mkDatatypeSort(long pointer, long datatypeDeclPointer) + throws CVC5ApiException; + + /** + * Create a vector of datatype sorts. The names of the datatype + * declarations must be distinct. + * + * @param dtypedecls the datatype declarations from which the sort is + * created + * @return the datatype sorts + */ + public Sort[] mkDatatypeSorts(List dtypedecls) throws CVC5ApiException + { + return mkDatatypeSorts(dtypedecls.toArray(new DatatypeDecl[0])); + } + + /** + * Create a vector of datatype sorts. The names of the datatype + * declarations must be distinct. + * + * @param dtypedecls the datatype declarations from which the sort is + * created + * @return the datatype sorts + */ + public Sort[] mkDatatypeSorts(DatatypeDecl[] dtypedecls) throws CVC5ApiException + { + long[] declPointers = Utils.getPointers(dtypedecls); + long[] sortPointers = mkDatatypeSorts(pointer, declPointers); + Sort[] sorts = Utils.getSorts(this, sortPointers); + return sorts; + } + + private native long[] mkDatatypeSorts(long pointer, long[] declPointers) throws CVC5ApiException; + + /** + * Create a vector of datatype sorts using unresolved sorts. The names of + * the datatype declarations in dtypedecls must be distinct. + * + * This method is called when the DatatypeDecl objects dtypedecls have + * been built using "unresolved" sorts. + * + * We associate each sort in unresolvedSorts with exacly one datatype from + * dtypedecls. In particular, it must have the same name as exactly one + * datatype declaration in dtypedecls. + * + * When constructing datatypes, unresolved sorts are replaced by the + * datatype sort constructed for the datatype declaration it is associated + * with. + * + * @param dtypedecls the datatype declarations from which the sort is + * created + * @param unresolvedSorts the set of unresolved sorts + * @return the datatype sorts + */ + public List mkDatatypeSorts(List dtypedecls, Set unresolvedSorts) + throws CVC5ApiException + { + Sort[] array = mkDatatypeSorts( + dtypedecls.toArray(new DatatypeDecl[0]), unresolvedSorts.toArray(new Sort[0])); + return Arrays.asList(array); + } + + /** + * Create a vector of datatype sorts using unresolved sorts. The names of + * the datatype declarations in dtypedecls must be distinct. + * + * This method is called when the DatatypeDecl objects dtypedecls have + * been built using "unresolved" sorts. + * + * We associate each sort in unresolvedSorts with exacly one datatype from + * dtypedecls. In particular, it must have the same name as exactly one + * datatype declaration in dtypedecls. + * + * When constructing datatypes, unresolved sorts are replaced by the + * datatype sort constructed for the datatype declaration it is associated + * with. + * + * @param dtypedecls the datatype declarations from which the sort is + * created + * @param unresolvedSorts the list of unresolved sorts + * @return the datatype sorts + */ + public Sort[] mkDatatypeSorts(DatatypeDecl[] dtypedecls, Sort[] unresolvedSorts) + throws CVC5ApiException + { + long[] declPointers = Utils.getPointers(dtypedecls); + long[] unresolvedPointers = Utils.getPointers(unresolvedSorts); + long[] sortPointers = mkDatatypeSorts(pointer, declPointers, unresolvedPointers); + Sort[] sorts = Utils.getSorts(this, sortPointers); + return sorts; + } + + private native long[] mkDatatypeSorts( + long pointer, long[] declPointers, long[] unresolvedPointers) throws CVC5ApiException; + + /** + * Create function sort. + * @param domain the sort of the fuction argument + * @param codomain the sort of the function return value + * @return the function sort + */ + public Sort mkFunctionSort(Sort domain, Sort codomain) + { + long sortPointer = mkFunctionSort(pointer, domain.getPointer(), codomain.getPointer()); + return new Sort(this, sortPointer); + } + + private native long mkFunctionSort(long pointer, long domainPointer, long codomainPointer); + + /** + * Create function sort. + * @param sorts the sort of the function arguments + * @param codomain the sort of the function return value + * @return the function sort + */ + public Sort mkFunctionSort(Sort[] sorts, Sort codomain) + { + long sortPointer = mkFunctionSort(pointer, Utils.getPointers(sorts), codomain.getPointer()); + return new Sort(this, sortPointer); + } + + private native long mkFunctionSort(long pointer, long[] sortPointers, long codomainPointer); + + /** + * Create a sort parameter. + * @param symbol the name of the sort + * @return the sort parameter + */ + public Sort mkParamSort(String symbol) + { + long sortPointer = mkParamSort(pointer, symbol); + return new Sort(this, sortPointer); + } + + private native long mkParamSort(long pointer, String symbol); + + /** + * Create a predicate sort. + * @param sorts the list of sorts of the predicate + * @return the predicate sort + */ + public Sort mkPredicateSort(Sort[] sorts) + { + long sortPointer = mkPredicateSort(pointer, Utils.getPointers(sorts)); + return new Sort(this, sortPointer); + } + + private native long mkPredicateSort(long pointer, long[] sortPointers); + + /** + * Create a record sort + * @param fields the list of fields of the record + * @return the record sort + */ + public Sort mkRecordSort(Pair[] fields) + { + long sortPointer = mkRecordSort(pointer, Utils.getPairs(fields)); + return new Sort(this, sortPointer); + } + + private native long mkRecordSort(long pointer, Pair[] fields); + + /** + * Create a set sort. + * @param elemSort the sort of the set elements + * @return the set sort + */ + public Sort mkSetSort(Sort elemSort) + { + long sortPointer = mkSetSort(pointer, elemSort.getPointer()); + return new Sort(this, sortPointer); + } + + private native long mkSetSort(long pointer, long elemSortPointer); + /** + * Create a bag sort. + * @param elemSort the sort of the bag elements + * @return the bag sort + */ + public Sort mkBagSort(Sort elemSort) + { + long sortPointer = mkBagSort(pointer, elemSort.getPointer()); + return new Sort(this, sortPointer); + } + + private native long mkBagSort(long pointer, long elemSortPointer); + + /** + * Create a sequence sort. + * @param elemSort the sort of the sequence elements + * @return the sequence sort + */ + public Sort mkSequenceSort(Sort elemSort) + { + long sortPointer = mkSequenceSort(pointer, elemSort.getPointer()); + return new Sort(this, sortPointer); + } + + private native long mkSequenceSort(long pointer, long elemSortPointer); + + /** + * Create an uninterpreted sort. + * @param symbol the name of the sort + * @return the uninterpreted sort + */ + public Sort mkUninterpretedSort(String symbol) + { + long sortPointer = mkUninterpretedSort(pointer, symbol); + return new Sort(this, sortPointer); + } + + private native long mkUninterpretedSort(long pointer, String symbol); + + /** + * Create a sort constructor sort. + * @param symbol the symbol of the sort + * @param arity the arity of the sort + * @return the sort constructor sort + */ + public Sort mkSortConstructorSort(String symbol, int arity) throws CVC5ApiException + { + Utils.validateUnsigned(arity, "arity"); + long sortPointer = mkSortConstructorSort(pointer, symbol, arity); + return new Sort(this, sortPointer); + } + + private native long mkSortConstructorSort(long pointer, String symbol, int arity); + + /** + * Create a tuple sort. + * @param sorts of the elements of the tuple + * @return the tuple sort + */ + public Sort mkTupleSort(Sort[] sorts) + { + long[] sortPointers = Utils.getPointers(sorts); + long sortPointer = mkTupleSort(pointer, sortPointers); + return new Sort(this, sortPointer); + } + + private native long mkTupleSort(long pointer, long[] sortPointers); + + /* .................................................................... */ + /* Create Terms */ + /* .................................................................... */ + + /** + * Create 0-ary term of given kind. + * @param kind the kind of the term + * @return the Term + */ + public Term mkTerm(Kind kind) + { + long termPointer = mkTerm(pointer, kind.getValue()); + return new Term(this, termPointer); + } + + private native long mkTerm(long pointer, int kindValue); + + /** + * Create a unary term of given kind. + * @param kind the kind of the term + * @param child the child of the term + * @return the Term + */ + public Term mkTerm(Kind kind, Term child) + { + long termPointer = mkTerm(pointer, kind.getValue(), child.getPointer()); + return new Term(this, termPointer); + } + + private native long mkTerm(long pointer, int kindValue, long childPointer); + + /** + * Create binary term of given kind. + * @param kind the kind of the term + * @param child1 the first child of the term + * @param child2 the second child of the term + * @return the Term + */ + public Term mkTerm(Kind kind, Term child1, Term child2) + { + long termPointer = mkTerm(pointer, kind.getValue(), child1.getPointer(), child2.getPointer()); + return new Term(this, termPointer); + } + + private native long mkTerm(long pointer, int kindValue, long child1Pointer, long child2Pointer); + + /** + * Create ternary term of given kind. + * @param kind the kind of the term + * @param child1 the first child of the term + * @param child2 the second child of the term + * @param child3 the third child of the term + * @return the Term + */ + public Term mkTerm(Kind kind, Term child1, Term child2, Term child3) + { + long termPointer = mkTerm( + pointer, kind.getValue(), child1.getPointer(), child2.getPointer(), child3.getPointer()); + return new Term(this, termPointer); + } + + private native long mkTerm( + long pointer, int kindValue, long child1Pointer, long child2Pointer, long child3Pointer); + /** + * Create n-ary term of given kind. + * @param kind the kind of the term + * @param children the children of the term + * @return the Term + */ + public Term mkTerm(Kind kind, Term[] children) + { + long[] childPointers = Utils.getPointers(children); + long termPointer = mkTerm(pointer, kind.getValue(), childPointers); + return new Term(this, termPointer); + } + + private native long mkTerm(long pointer, int kindValue, long[] childrenPointers); + + /** + * Create nullary term of given kind from a given operator. + * Create operators with mkOp(). + * @param op the operator + * @return the Term + */ + public Term mkTerm(Op op) + { + long termPointer = mkTerm(pointer, op.getPointer()); + return new Term(this, termPointer); + } + + private native long mkTerm(long pointer, long opPointer); + /** + * Create unary term of given kind from a given operator. + * Create operators with mkOp(). + * @param op the operator + * @param child the child of the term + * @return the Term + */ + public Term mkTerm(Op op, Term child) + { + long termPointer = mkTerm(pointer, op.getPointer(), child.getPointer()); + return new Term(this, termPointer); + } + + private native long mkTerm(long pointer, long opPointer, long childPointer); + + /** + * Create binary term of given kind from a given operator. + * Create operators with mkOp(). + * @param op the operator + * @param child1 the first child of the term + * @param child2 the second child of the term + * @return the Term + */ + public Term mkTerm(Op op, Term child1, Term child2) + { + long termPointer = mkTerm(pointer, op.getPointer(), child1.getPointer(), child2.getPointer()); + return new Term(this, termPointer); + } + + private native long mkTerm(long pointer, long opPointer, long child1Pointer, long child2Pointer); + /** + * Create ternary term of given kind from a given operator. + * Create operators with mkOp(). + * @param op the operator + * @param child1 the first child of the term + * @param child2 the second child of the term + * @param child3 the third child of the term + * @return the Term + */ + public Term mkTerm(Op op, Term child1, Term child2, Term child3) + { + long termPointer = + mkTerm(op.getPointer(), child1.getPointer(), child2.getPointer(), child3.getPointer()); + return new Term(this, termPointer); + } + + private native long mkTerm( + long pointer, long opPointer, long child1Pointer, long child2Pointer, long child3Pointer); + + /** + * Create n-ary term of given kind from a given operator. + * Create operators with mkOp(). + * @param op the operator + * @param children the children of the term + * @return the Term + */ + public Term mkTerm(Op op, List children) + { + return mkTerm(op, children.toArray(new Term[0])); + } + + /** + * Create n-ary term of given kind from a given operator. + * Create operators with mkOp(). + * @param op the operator + * @param children the children of the term + * @return the Term + */ + public Term mkTerm(Op op, Term[] children) + { + long[] childPointers = Utils.getPointers(children); + long termPointer = mkTerm(pointer, op.getPointer(), childPointers); + return new Term(this, termPointer); + } + + private native long mkTerm(long pointer, long opPointer, long[] childrenPointers); + + /** + * Create a tuple term. Terms are automatically converted if sorts are + * compatible. + * @param sorts The sorts of the elements in the tuple + * @param terms The elements in the tuple + * @return the tuple Term + */ + public Term mkTuple(Sort[] sorts, Term[] terms) + { + long[] sortPointers = Utils.getPointers(sorts); + long[] termPointers = Utils.getPointers(terms); + long termPointer = mkTuple(pointer, sortPointers, termPointers); + return new Term(this, termPointer); + } + + private native long mkTuple(long pointer, long[] sortPointers, long[] termPointers); + + /* .................................................................... */ + /* Create Operators */ + /* .................................................................... */ + + /** + * Create an operator for a builtin Kind + * The Kind may not be the Kind for an indexed operator + * (e.g. BITVECTOR_EXTRACT) + * Note: in this case, the Op simply wraps the Kind. + * The Kind can be used in mkTerm directly without + * creating an op first. + * @param kind the kind to wrap + */ + public Op mkOp(Kind kind) + { + long opPointer = mkOp(pointer, kind.getValue()); + return new Op(this, opPointer); + } + + private native long mkOp(long pointer, int kindValue); + /** + * Create operator of kind: + * - RECORD_UPDATE + * - DIVISIBLE (to support arbitrary precision integers) + * See enum Kind for a description of the parameters. + * @param kind the kind of the operator + * @param arg the string argument to this operator + */ + public Op mkOp(Kind kind, String arg) + { + long opPointer = mkOp(pointer, kind.getValue(), arg); + return new Op(this, opPointer); + } + + private native long mkOp(long pointer, int kindValue, String arg); + + /** + * Create operator of kind: + * - DIVISIBLE + * - BITVECTOR_REPEAT + * - BITVECTOR_ZERO_EXTEND + * - BITVECTOR_SIGN_EXTEND + * - BITVECTOR_ROTATE_LEFT + * - BITVECTOR_ROTATE_RIGHT + * - INT_TO_BITVECTOR + * - FLOATINGPOINT_TO_UBV + * - FLOATINGPOINT_TO_UBV_TOTAL + * - FLOATINGPOINT_TO_SBV + * - FLOATINGPOINT_TO_SBV_TOTAL + * - TUPLE_UPDATE + * See enum Kind for a description of the parameters. + * @param kind the kind of the operator + * @param arg the unsigned int argument to this operator + */ + public Op mkOp(Kind kind, int arg) throws CVC5ApiException + { + Utils.validateUnsigned(arg, "arg"); + long opPointer = mkOp(pointer, kind.getValue(), arg); + return new Op(this, opPointer); + } + + private native long mkOp(long pointer, int kindValue, int arg); + + /** + * Create operator of Kind: + * - BITVECTOR_EXTRACT + * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR + * - FLOATINGPOINT_TO_FP_FLOATINGPOINT + * - FLOATINGPOINT_TO_FP_REAL + * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR + * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR + * - FLOATINGPOINT_TO_FP_GENERIC + * See enum Kind for a description of the parameters. + * @param kind the kind of the operator + * @param arg1 the first unsigned int argument to this operator + * @param arg2 the second unsigned int argument to this operator + */ + public Op mkOp(Kind kind, int arg1, int arg2) throws CVC5ApiException + { + Utils.validateUnsigned(arg1, "arg1"); + Utils.validateUnsigned(arg2, "arg2"); + long opPointer = mkOp(pointer, kind.getValue(), arg1, arg2); + return new Op(this, opPointer); + } + + private native long mkOp(long pointer, int kindValue, int arg1, int arg2); + + /** + * Create operator of Kind: + * - TUPLE_PROJECT + * See enum Kind for a description of the parameters. + * @param kind the kind of the operator + * @param args the arguments (indices) of the operator + */ + public Op mkOp(Kind kind, int[] args) throws CVC5ApiException + { + Utils.validateUnsigned(args, "args"); + long opPointer = mkOp(pointer, kind.getValue(), args); + return new Op(this, opPointer); + } + + private native long mkOp(long pointer, int kindValue, int[] args); + + /* .................................................................... */ + /* Create Constants */ + /* .................................................................... */ + + /** + * Create a Boolean true constant. + * @return the true constant + */ + public Term mkTrue() + { + long termPointer = mkTrue(pointer); + return new Term(this, termPointer); + } + + private native long mkTrue(long pointer); + /** + * Create a Boolean false constant. + * @return the false constant + */ + public Term mkFalse() + { + long termPointer = mkFalse(pointer); + return new Term(this, termPointer); + } + + private native long mkFalse(long pointer); + /** + * Create a Boolean constant. + * @return the Boolean constant + * @param val the value of the constant + */ + public Term mkBoolean(boolean val) + { + long termPointer = mkBoolean(pointer, val); + return new Term(this, termPointer); + } + + private native long mkBoolean(long pointer, boolean val); + /** + * Create a constant representing the number Pi. + * @return a constant representing Pi + */ + public Term mkPi() + { + long termPointer = mkPi(pointer); + return new Term(this, termPointer); + } + + private native long mkPi(long pointer); + /** + * Create an integer constant from a string. + * @param s the string representation of the constant, may represent an + * integer (e.g., "123"). + * @return a constant of sort Integer assuming 's' represents an integer) + */ + public Term mkInteger(String s) throws CVC5ApiException + { + long termPointer = mkInteger(pointer, s); + return new Term(this, termPointer); + } + + private native long mkInteger(long pointer, String s) throws CVC5ApiException; + + /** + * Create an integer constant from a c++ int. + * @param val the value of the constant + * @return a constant of sort Integer + */ + public Term mkInteger(long val) + { + long termPointer = mkInteger(pointer, val); + return new Term(this, termPointer); + } + + private native long mkInteger(long pointer, long val); + /** + * Create a real constant from a string. + * @param s the string representation of the constant, may represent an + * integer (e.g., "123") or real constant (e.g., "12.34" or + * "12/34"). + * @return a constant of sort Real + */ + public Term mkReal(String s) throws CVC5ApiException + { + long termPointer = mkReal(pointer, s); + return new Term(this, termPointer); + } + + private native long mkReal(long pointer, String s) throws CVC5ApiException; + /** + * Create a real constant from an integer. + * @param val the value of the constant + * @return a constant of sort Integer + */ + public Term mkReal(long val) + { + long termPointer = mkRealValue(pointer, val); + return new Term(this, termPointer); + } + + private native long mkRealValue(long pointer, long val); + /** + * Create a real constant from a rational. + * @param num the value of the numerator + * @param den the value of the denominator + * @return a constant of sort Real + */ + public Term mkReal(long num, long den) + { + long termPointer = mkReal(pointer, num, den); + return new Term(this, termPointer); + } + + private native long mkReal(long pointer, long num, long den); + + /** + * Create a regular expression empty term. + * @return the empty term + */ + public Term mkRegexpEmpty() + { + long termPointer = mkRegexpEmpty(pointer); + return new Term(this, termPointer); + } + + private native long mkRegexpEmpty(long pointer); + + /** + * Create a regular expression sigma term. + * @return the sigma term + */ + public Term mkRegexpSigma() + { + long termPointer = mkRegexpSigma(pointer); + return new Term(this, termPointer); + } + + private native long mkRegexpSigma(long pointer); + + /** + * Create a constant representing an empty set of the given sort. + * @param sort the sort of the set elements. + * @return the empty set constant + */ + public Term mkEmptySet(Sort sort) + { + long termPointer = mkEmptySet(pointer, sort.getPointer()); + return new Term(this, termPointer); + } + + private native long mkEmptySet(long pointer, long sortPointer); + /** + * Create a constant representing an empty bag of the given sort. + * @param sort the sort of the bag elements. + * @return the empty bag constant + */ + public Term mkEmptyBag(Sort sort) + { + long termPointer = mkEmptyBag(pointer, sort.getPointer()); + return new Term(this, termPointer); + } + + private native long mkEmptyBag(long pointer, long sortPointer); + + /** + * Create a separation logic nil term. + * @param sort the sort of the nil term + * @return the separation logic nil term + */ + public Term mkSepNil(Sort sort) + { + long termPointer = mkSepNil(pointer, sort.getPointer()); + return new Term(this, termPointer); + } + + private native long mkSepNil(long pointer, long sortPointer); + + /** + * Create a String constant. + * @param s the string this constant represents + * @return the String constant + */ + public Term mkString(String s) + { + return mkString(s, false); + } + + /** + * Create a String constant. + * @param s the string this constant represents + * @param useEscSequences determines whether escape sequences in `s` + * should be converted to the corresponding unicode character + * @return the String constant + */ + public Term mkString(String s, boolean useEscSequences) + { + // TODO: review unicode + long termPointer = mkString(pointer, s, useEscSequences); + return new Term(this, termPointer); + } + + private native long mkString(long pointer, String s, boolean useEscSequences); + + /** + * Create a String constant. + * @param s a list of unsigned (unicode) values this constant represents + * as + * string + * @return the String constant + */ + public Term mkString(int[] s) throws CVC5ApiException + { + Utils.validateUnsigned(s, "s"); + long termPointer = mkString(pointer, s); + return new Term(this, termPointer); + } + + private native long mkString(long pointer, int[] s); + + /** + * Create an empty sequence of the given element sort. + * @param sort The element sort of the sequence. + * @return the empty sequence with given element sort. + */ + public Term mkEmptySequence(Sort sort) + { + long termPointer = mkEmptySequence(pointer, sort.getPointer()); + return new Term(this, termPointer); + } + + private native long mkEmptySequence(long pointer, long sortPointer); + + /** + * Create a universe set of the given sort. + * @param sort the sort of the set elements + * @return the universe set constant + */ + public Term mkUniverseSet(Sort sort) + { + long termPointer = mkUniverseSet(pointer, sort.getPointer()); + return new Term(this, termPointer); + } + + private native long mkUniverseSet(long pointer, long sortPointer); + + /** + * Create a bit-vector constant of given size and value = 0. + * @param size the bit-width of the bit-vector sort + * @return the bit-vector constant + */ + public Term mkBitVector(int size) throws CVC5ApiException + { + return mkBitVector(size, 0); + } + + /** + * Create a bit-vector constant of given size and value. + * + * Note: The given value must fit into a bit-vector of the given size. + * + * @param size the bit-width of the bit-vector sort + * @param val the value of the constant + * @return the bit-vector constant + */ + public Term mkBitVector(int size, long val) throws CVC5ApiException + { + Utils.validateUnsigned(size, "size"); + Utils.validateUnsigned(val, "val"); + long termPointer = mkBitVector(pointer, size, val); + return new Term(this, termPointer); + } + + private native long mkBitVector(long pointer, int size, long val); + + /** + * Create a bit-vector constant of a given bit-width from a given string of + * base 2, 10 or 16. + * + * Note: The given value must fit into a bit-vector of the given size. + * + * @param size the bit-width of the constant + * @param s the string representation of the constant + * @param base the base of the string representation (2, 10, or 16) + * @return the bit-vector constant + */ + public Term mkBitVector(int size, String s, int base) throws CVC5ApiException + { + Utils.validateUnsigned(size, "size"); + Utils.validateUnsigned(base, "base"); + long termPointer = mkBitVector(pointer, size, s, base); + return new Term(this, termPointer); + } + + private native long mkBitVector(long pointer, int size, String s, int base); + + /** + * Create a constant array with the provided constant value stored at + * every index + * @param sort the sort of the constant array (must be an array sort) + * @param val the constant value to store (must match the sort's element + * sort) + * @return the constant array term + */ + public Term mkConstArray(Sort sort, Term val) + { + long termPointer = mkConstArray(pointer, sort.getPointer(), val.getPointer()); + return new Term(this, termPointer); + } + + private native long mkConstArray(long pointer, long sortPointer, long valPointer); + /** + * Create a positive infinity floating-point constant. + * @param exp Number of bits in the exponent + * @param sig Number of bits in the significand + * @return the floating-point constant + */ + public Term mkPosInf(int exp, int sig) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long termPointer = mkPosInf(pointer, exp, sig); + return new Term(this, termPointer); + } + + private native long mkPosInf(long pointer, int exp, int sig); + /** + * Create a negative infinity floating-point constant. + * @param exp Number of bits in the exponent + * @param sig Number of bits in the significand + * @return the floating-point constant + */ + public Term mkNegInf(int exp, int sig) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long termPointer = mkNegInf(pointer, exp, sig); + return new Term(this, termPointer); + } + + private native long mkNegInf(long pointer, int exp, int sig); + /** + * Create a not-a-number (NaN) floating-point constant. + * @param exp Number of bits in the exponent + * @param sig Number of bits in the significand + * @return the floating-point constant + */ + public Term mkNaN(int exp, int sig) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long termPointer = mkNaN(pointer, exp, sig); + return new Term(this, termPointer); + } + + private native long mkNaN(long pointer, int exp, int sig); + + /** + * Create a positive zero (+0.0) floating-point constant. + * @param exp Number of bits in the exponent + * @param sig Number of bits in the significand + * @return the floating-point constant + */ + public Term mkPosZero(int exp, int sig) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long termPointer = mkPosZero(pointer, exp, sig); + return new Term(this, termPointer); + } + + private native long mkPosZero(long pointer, int exp, int sig); + + /** + * Create a negative zero (-0.0) floating-point constant. + * @param exp Number of bits in the exponent + * @param sig Number of bits in the significand + * @return the floating-point constant + */ + public Term mkNegZero(int exp, int sig) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long termPointer = mkNegZero(pointer, exp, sig); + return new Term(this, termPointer); + } + + private native long mkNegZero(long pointer, int exp, int sig); + + /** + * Create a roundingmode constant. + * @param rm the floating point rounding mode this constant represents + */ + public Term mkRoundingMode(RoundingMode rm) + { + long termPointer = mkRoundingMode(pointer, rm.getValue()); + return new Term(this, termPointer); + } + + private native long mkRoundingMode(long pointer, int rm); + + /** + * Create uninterpreted constant. + * @param sort Sort of the constant + * @param index Index of the constant + */ + public Term mkUninterpretedConst(Sort sort, int index) throws CVC5ApiException + { + Utils.validateUnsigned(index, "index"); + long termPointer = mkUninterpretedConst(pointer, sort.getPointer(), index); + return new Term(this, termPointer); + } + + private native long mkUninterpretedConst(long pointer, long sortPointer, int index); + + /** + * Create an abstract value constant. + * @param index Index of the abstract value + */ + public Term mkAbstractValue(String index) + { + long termPointer = mkAbstractValue(pointer, index); + return new Term(this, termPointer); + } + + private native long mkAbstractValue(long pointer, String index); + + /** + * Create an abstract value constant. + * @param index Index of the abstract value + */ + public Term mkAbstractValue(long index) throws CVC5ApiException + { + Utils.validateUnsigned(index, "index"); + long termPointer = mkAbstractValue(pointer, index); + return new Term(this, termPointer); + } + + private native long mkAbstractValue(long pointer, long index); + + /** + * Create a floating-point constant. + * @param exp Size of the exponent + * @param sig Size of the significand + * @param val Value of the floating-point constant as a bit-vector term + */ + public Term mkFloatingPoint(int exp, int sig, Term val) throws CVC5ApiException + { + Utils.validateUnsigned(exp, "exp"); + Utils.validateUnsigned(sig, "sig"); + long termPointer = mkFloatingPoint(pointer, exp, sig, val.getPointer()); + return new Term(this, termPointer); + } + + private native long mkFloatingPoint(long pointer, int exp, int sig, long valPointer); + + /* .................................................................... */ + /* Create Variables */ + /* .................................................................... */ + + /** + * Create (first-order) constant (0-arity function symbol). + * SMT-LIB: + * \verbatim + * ( declare-const ) + * ( declare-fun ( ) ) + * \endverbatim + * + * @param sort the sort of the constant + * @param symbol the name of the constant + * @return the first-order constant + */ + public Term mkConst(Sort sort, String symbol) + { + long termPointer = mkConst(pointer, sort.getPointer(), symbol); + return new Term(this, termPointer); + } + + private native long mkConst(long pointer, long sortPointer, String symbol); + + /** + * Create (first-order) constant (0-arity function symbol), with a default + * symbol name. + * + * @param sort the sort of the constant + * @return the first-order constant + */ + public Term mkConst(Sort sort) + { + long termPointer = mkConst(pointer, sort.getPointer()); + return new Term(this, termPointer); + } + + private native long mkConst(long pointer, long sortPointer); + + /** + * Create a bound variable to be used in a binder (i.e. a quantifier, a + * lambda, or a witness binder). + * @param sort the sort of the variable + * @return the variable + */ + public Term mkVar(Sort sort) + { + return mkVar(sort, ""); + } + + /** + * Create a bound variable to be used in a binder (i.e. a quantifier, a + * lambda, or a witness binder). + * @param sort the sort of the variable + * @param symbol the name of the variable + * @return the variable + */ + public Term mkVar(Sort sort, String symbol) + { + long termPointer = mkVar(pointer, sort.getPointer(), symbol); + return new Term(this, termPointer); + } + + private native long mkVar(long pointer, long sortPointer, String symbol); + + /* .................................................................... */ + /* Create datatype constructor declarations */ + /* .................................................................... */ + + public DatatypeConstructorDecl mkDatatypeConstructorDecl(String name) + { + long declPointer = mkDatatypeConstructorDecl(pointer, name); + return new DatatypeConstructorDecl(this, declPointer); + } + + private native long mkDatatypeConstructorDecl(long pointer, String name); + + /* .................................................................... */ + /* Create datatype declarations */ + /* .................................................................... */ + + /** + * Create a datatype declaration. + * @param name the name of the datatype + * @return the DatatypeDecl + */ + public DatatypeDecl mkDatatypeDecl(String name) + { + return mkDatatypeDecl(name, false); + } + + /** + * Create a datatype declaration. + * @param name the name of the datatype + * @param isCoDatatype true if a codatatype is to be constructed + * @return the DatatypeDecl + */ + public DatatypeDecl mkDatatypeDecl(String name, boolean isCoDatatype) + { + long declPointer = mkDatatypeDecl(pointer, name, isCoDatatype); + return new DatatypeDecl(this, declPointer); + } + + private native long mkDatatypeDecl(long pointer, String name, boolean isCoDatatype); + + /** + * Create a datatype declaration. + * Create sorts parameter with Solver::mkParamSort(). + * @param name the name of the datatype + * @param param the sort parameter + * @return the DatatypeDecl + */ + public DatatypeDecl mkDatatypeDecl(String name, Sort param) + { + return mkDatatypeDecl(name, param, false); + } + + /** + * Create a datatype declaration. + * Create sorts parameter with Solver::mkParamSort(). + * @param name the name of the datatype + * @param param the sort parameter + * @param isCoDatatype true if a codatatype is to be constructed + * @return the DatatypeDecl + */ + public DatatypeDecl mkDatatypeDecl(String name, Sort param, boolean isCoDatatype) + { + long declPointer = mkDatatypeDecl(pointer, name, param.getPointer(), isCoDatatype); + return new DatatypeDecl(this, declPointer); + } + + private native long mkDatatypeDecl( + long pointer, String name, long paramPointer, boolean isCoDatatype); + + /** + * Create a datatype declaration. + * Create sorts parameter with Solver::mkParamSort(). + * @param name the name of the datatype + * @param params a list of sort parameters + * @return the DatatypeDecl + */ + public DatatypeDecl mkDatatypeDecl(String name, List params) + { + return mkDatatypeDecl(name, params.toArray(new Sort[0])); + } + + /** + * Create a datatype declaration. + * Create sorts parameter with Solver::mkParamSort(). + * @param name the name of the datatype + * @param params a list of sort parameters + * @return the DatatypeDecl + */ + public DatatypeDecl mkDatatypeDecl(String name, Sort[] params) + { + return mkDatatypeDecl(name, params, false); + } + + /** + * Create a datatype declaration. + * Create sorts parameter with Solver::mkParamSort(). + * @param name the name of the datatype + * @param params a list of sort parameters + * @param isCoDatatype true if a codatatype is to be constructed + * @return the DatatypeDecl + */ + public DatatypeDecl mkDatatypeDecl(String name, Sort[] params, boolean isCoDatatype) + { + long[] paramPointers = Utils.getPointers(params); + long declPointer = mkDatatypeDecl(pointer, name, paramPointers, isCoDatatype); + return new DatatypeDecl(this, declPointer); + } + + private native long mkDatatypeDecl( + long pointer, String name, long[] paramPointers, boolean isCoDatatype); + + /* .................................................................... */ + /* Formula Handling */ + /* .................................................................... */ + + /** + * Simplify a formula without doing "much" work. Does not involve + * the SAT Engine in the simplification, but uses the current + * definitions, assertions, and the current partial model, if one + * has been constructed. It also involves theory normalization. + * @param t the formula to simplify + * @return the simplified formula + */ + public Term simplify(Term t) + { + long termPointer = simplify(pointer, t.getPointer()); + return new Term(this, termPointer); + } + + private native long simplify(long pointer, long termPointer); + + /** + * Assert a formula. + * SMT-LIB: + * \verbatim + * ( assert ) + * \endverbatim + * @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: + * \verbatim + * ( check-sat ) + * \endverbatim + * @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: + * \verbatim + * ( check-sat-assuming ( ) ) + * \endverbatim + * @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: + * \verbatim + * ( check-sat-assuming ( + ) ) + * \endverbatim + * @param assumptions the formulas to assume + * @return the result of the satisfiability check. + */ + public Result checkSatAssuming(Term[] assumptions) + { + long[] pointers = Utils.getPointers(assumptions); + long resultPointer = checkSatAssuming(pointer, pointers); + return new Result(this, resultPointer); + } + + private native long checkSatAssuming(long pointer, long[] assumptionPointers); + + /** + * Check entailment of the given formula w.r.t. the current set of assertions. + * @param term the formula to check entailment for + * @return the result of the entailment check. + */ + public Result checkEntailed(Term term) + { + long resultPointer = checkEntailed(pointer, term.getPointer()); + return new Result(this, resultPointer); + } + + private native long checkEntailed(long pointer, long termPointer); + + /** + * Check entailment of the given set of given formulas w.r.t. the current + * set of assertions. + * @param terms the terms to check entailment for + * @return the result of the entailmentcheck. + */ + public Result checkEntailed(Term[] terms) + { + long[] pointers = Utils.getPointers(terms); + long resultPointer = checkEntailed(pointer, pointers); + return new Result(this, resultPointer); + } + + private native long checkEntailed(long pointer, long[] termPointers); + + /** + * Create datatype sort. + * SMT-LIB: + * \verbatim + * ( declare-datatype ) + * \endverbatim + * @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: + * \verbatim + * ( declare-fun ( * ) ) + * \endverbatim + * @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: + * \verbatim + * ( declare-sort ) + * \endverbatim + * @param symbol the name of the sort + * @param arity the arity of the sort + * @return the sort + */ + public Sort declareSort(String symbol, int arity) throws CVC5ApiException + { + Utils.validateUnsigned(arity, "arity"); + long sortPointer = declareSort(pointer, symbol, arity); + return new Sort(this, sortPointer); + } + + private native long declareSort(long pointer, String symbol, int arity); + + /** + * Define n-ary function in the current context. + * SMT-LIB: + * \verbatim + * ( define-fun ) + * \endverbatim + * @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: + * \verbatim + * ( define-fun ) + * \endverbatim + * @param symbol the name of the function + * @param boundVars the parameters to this function + * @param sort the sort of the return value of this function + * @param term the function body + * @param global determines whether this definition is global (i.e. persists + * when popping the context) + * @return the function + */ + public Term defineFun(String symbol, Term[] boundVars, Sort sort, Term term, boolean global) + { + long[] boundVarPointers = Utils.getPointers(boundVars); + long termPointer = + defineFun(pointer, symbol, boundVarPointers, sort.getPointer(), term.getPointer(), global); + return new Term(this, termPointer); + } + + private native long defineFun(long pointer, + String symbol, + long[] boundVarPointers, + long sortPointer, + long termPointer, + boolean global); + + /** + * Define n-ary function in the current context. + * SMT-LIB: + * \verbatim + * ( define-fun ) + * \endverbatim + * Create parameter 'fun' with mkConst(). + * @param fun the sorted function + * @param boundVars the parameters to this function + * @param term the function body + * @return the function + */ + public Term defineFun(Term fun, Term[] boundVars, Term term) + { + return defineFun(fun, boundVars, term, false); + } + /** + * Define n-ary function. + * SMT-LIB: + * \verbatim + * ( define-fun ) + * \endverbatim + * Create parameter 'fun' with mkConst(). + * @param fun the sorted function + * @param boundVars the parameters to this function + * @param term the function body + * @param global determines whether this definition is global (i.e. persists + * when popping the context) + * @return the function + */ + public Term defineFun(Term fun, Term[] boundVars, Term term, boolean global) + { + long[] boundVarPointers = Utils.getPointers(boundVars); + long termPointer = + defineFun(pointer, fun.getPointer(), boundVarPointers, term.getPointer(), global); + return new Term(this, termPointer); + } + + private native long defineFun( + long pointer, long funPointer, long[] boundVarPointers, long termPointer, boolean global); + + /** + * Define recursive function in the current context. + * SMT-LIB: + * \verbatim + * ( define-fun-rec ) + * \endverbatim + * @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: + * \verbatim + * ( define-fun-rec ) + * \endverbatim + * @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: + * \verbatim + * ( define-fun-rec ) + * \endverbatim + * 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: + * \verbatim + * ( define-fun-rec ) + * \endverbatim + * 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: + * \verbatim + * ( define-funs-rec ( ^{n+1} ) ( ^{n+1} ) ) + * \endverbatim + * 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 + * @return the function + */ + public void defineFunsRec(Term[] funs, Term[][] boundVars, Term[] terms) + { + defineFunsRec(funs, boundVars, terms, false); + } + /** + * Define recursive functions. + * SMT-LIB: + * \verbatim + * ( define-funs-rec ( ^{n+1} ) ( ^{n+1} ) ) + * \endverbatim + * 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) + * @return the function + */ + public void defineFunsRec(Term[] funs, Term[][] boundVars, Term[] terms, boolean global) + { + long[] funPointers = Utils.getPointers(funs); + long[][] boundVarPointers = Utils.getPointers(boundVars); + long[] termPointers = Utils.getPointers(terms); + defineFunsRec(pointer, funPointers, boundVarPointers, termPointers, global); + } + + private native void defineFunsRec(long pointer, + long[] funPointers, + long[][] boundVarPointers, + long[] termPointers, + boolean global); + + /** + * Echo a given string to the given output stream. + * SMT-LIB: + * \verbatim + * ( echo ) + * \endverbatim + * @param out the output stream + * @param str the string to echo + */ + // TODO: void echo(std::ostream& out, String str) + + /** + * Get the list of asserted formulas. + * SMT-LIB: + * \verbatim + * ( get-assertions ) + * \endverbatim + * @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: \verbatim( get-info )\verbatim + * @return the info + */ + public String getInfo(String flag) + { + return getInfo(pointer, flag); } - private native long newSolver(); + private native String getInfo(long pointer, String flag); - public void deletePointer() + /** + * Get the value of a given option. + * SMT-LIB: + * \verbatim + * ( get-option ) + * \endverbatim + * @param option the option for which the value is queried + * @return a string representation of the option value + */ + public String getOption(String option) { - deletePointer(pointer); + return getOption(pointer, option); } - private static native void deletePointer(long solverPointer); + private native String getOption(long pointer, String option); - static + /** + * Get the set of unsat ("failed") assumptions. + * SMT-LIB: + * \verbatim + * ( get-unsat-assumptions ) + * \endverbatim + * Requires to enable option 'produce-unsat-assumptions'. + * @return the set of unsat assumptions. + */ + public Term[] getUnsatAssumptions() { - Utils.loadLibraries(); + long[] retPointers = getUnsatAssumptions(pointer); + return Utils.getTerms(this, retPointers); } + private native long[] getUnsatAssumptions(long pointer); + /** - * Set logic. - * SMT-LIB: ( set-logic ) + * Get the unsatisfiable core. + * SMT-LIB: + * \verbatim + * ( get-unsat-core ) + * \endverbatim + * Requires to enable option 'produce-unsat-cores'. + * @return a set of terms representing the unsatisfiable core + */ + public Term[] getUnsatCore() + { + long[] retPointers = getUnsatCore(pointer); + return Utils.getTerms(this, retPointers); + } + + private native long[] getUnsatCore(long pointer); + + /** + * Get the value of the given term. + * SMT-LIB: + * \verbatim + * ( get-value ( ) ) + * \endverbatim + * @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. + * SMT-LIB: + * \verbatim + * ( get-value ( + ) ) + * \endverbatim + * @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); + + /** + * This returns false if the model value of free constant v was not essential + * for showing the satisfiability of the last call to checkSat using the + * current model. This method will only return false (for any v) if + * the model-cores option has been set. * - * @param logic - * @throws CVC5ApiException + * @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: + * \verbatim + * ( get-model ) + * \endverbatim + * Requires to enable option 'produce-models'. + * @param sorts The list of uninterpreted sorts that should be printed in the + * model. + * @param vars The list of free constants that should be printed in the + * model. A subset of these may be printed based on isModelCoreSymbol. + * @return a string representing the model. + */ + public String getModel(Sort[] sorts, Term[] vars) + { + long[] sortPointers = Utils.getPointers(sorts); + long[] varPointers = Utils.getPointers(vars); + return getModel(pointer, sortPointers, varPointers); + } + + private native String getModel(long pointer, long[] sortPointers, long[] varPointers); + + /** + * Do quantifier elimination. + * SMT-LIB: + * \verbatim + * ( get-qe ) + * \endverbatim + * Requires a logic that supports quantifier elimination. Currently, the only + * logics supported by quantifier elimination is LRA and LIA. + * @param q a quantified formula of the form: + * Q x1...xn. P( x1...xn, y1...yn ) + * where P( x1...xn, y1...yn ) is a quantifier-free formula + * @return a formula ret such that, given the current set of formulas A + * asserted to this solver: + * - ( A ^ q ) and ( A ^ ret ) are equivalent + * - ret is quantifier-free formula containing only free variables in + * y1...yn. + */ + public Term getQuantifierElimination(Term q) + { + long termPointer = getQuantifierElimination(pointer, q.getPointer()); + return new Term(this, termPointer); + } + + private native long getQuantifierElimination(long pointer, long qPointer); + + /** + * Do partial quantifier elimination, which can be used for incrementally + * computing the result of a quantifier elimination. + * SMT-LIB: + * \verbatim + * ( get-qe-disjunct ) + * \endverbatim + * Requires a logic that supports quantifier elimination. Currently, the only + * logics supported by quantifier elimination is LRA and LIA. + * @param q a quantified formula of the form: + * Q x1...xn. P( x1...xn, y1...yn ) + * where P( x1...xn, y1...yn ) is a quantifier-free formula + * @return a formula ret such that, given the current set of formulas A + * asserted to this solver: + * - (A ^ q) => (A ^ ret) if Q is forall or (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 + * 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 + * A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be + * A ^ ret^Q_1 ^ ... ^ ret^Q_n + * where ret^Q_i is the same as above. In either case, we have + * that ret^Q_j will eventually be true or false, for some finite j. + */ + public Term getQuantifierEliminationDisjunct(Term q) + { + long termPointer = getQuantifierEliminationDisjunct(pointer, q.getPointer()); + return new Term(this, termPointer); + } + + private native long getQuantifierEliminationDisjunct(long pointer, long qPointer); + + /** + * When using separation logic, this sets the location sort and the + * datatype sort to the given ones. This method should be invoked exactly + * once, before any separation logic constraints are provided. + * @param locSort The location sort of the heap + * @param dataSort The data sort of the heap + */ + public void declareSeparationHeap(Sort locSort, Sort dataSort) + { + declareSeparationHeap(pointer, locSort.getPointer(), dataSort.getPointer()); + } + + private native void declareSeparationHeap( + long pointer, long locSortPointer, long dataSortPointer); + + /** + * When using separation logic, obtain the term for the heap. + * @return The term for the heap + */ + public Term getSeparationHeap() + { + long termPointer = getSeparationHeap(pointer); + return new Term(this, termPointer); + } + + private native long getSeparationHeap(long pointer); + + /** + * When using separation logic, obtain the term for nil. + * @return The term for nil + */ + public Term getSeparationNilTerm() + { + long termPointer = getSeparationNilTerm(pointer); + return new Term(this, termPointer); + } + + private native long getSeparationNilTerm(long pointer); + + /** + * Pop a level from the assertion stack. + * SMT-LIB: + * \verbatim + * ( pop ) + * \endverbatim + */ + public void pop() throws CVC5ApiException + { + pop(1); + } + + /** + * Pop (a) level(s) from the assertion stack. + * SMT-LIB: + * \verbatim + * ( pop ) + * \endverbatim + * @param nscopes the number of levels to pop + */ + public void pop(int nscopes) throws CVC5ApiException + { + Utils.validateUnsigned(nscopes, "nscopes"); + pop(pointer, nscopes); + } + + private native void pop(long pointer, int nscopes); + + /** + * Get an interpolant + * SMT-LIB: + * \verbatim + * ( get-interpol ) + * \endverbatim + * Requires to enable option 'produce-interpols'. + * @param conj the conjecture term + * @param output a Term I such that A->I and I->B are valid, where A is the + * current set of assertions and B is given in the input by conj. + * @return true if it gets I successfully, false otherwise. + */ + public boolean getInterpolant(Term conj, Term output) + { + return getInterpolant(pointer, conj.getPointer(), output.getPointer()); + } + + private native boolean getInterpolant(long pointer, long conjPointer, long outputPointer); + + /** + * Get an interpolant + * SMT-LIB: + * \verbatim + * ( get-interpol ) + * \endverbatim + * Requires to enable option 'produce-interpols'. + * @param conj the conjecture term + * @param grammar the grammar for the interpolant I + * @param output a Term I such that A->I and I->B are valid, where A is the + * current set of assertions and B is given in the input by conj. + * @return true if it gets I successfully, false otherwise. + */ + public boolean getInterpolant(Term conj, Grammar grammar, Term output) + { + return getInterpolant(pointer, conj.getPointer(), grammar.getPointer(), output.getPointer()); + } + + private native boolean getInterpolant( + long pointer, long conjPointer, long grammarPointer, long outputPointer); + + /** + * Get an abduct. + * SMT-LIB: + * \verbatim + * ( get-abduct ) + * \endverbatim + * Requires enabling option 'produce-abducts' + * @param conj the conjecture term + * @param output a term C such that A^C is satisfiable, and A^~B^C is + * unsatisfiable, where A is the current set of assertions and B is + * given in the input by conj + * @return true if it gets C successfully, false otherwise + */ + public boolean getAbduct(Term conj, Term output) + { + return getAbduct(pointer, conj.getPointer(), output.getPointer()); + } + + private native boolean getAbduct(long pointer, long conjPointer, long outputPointer); + /** + * Get an abduct. + * SMT-LIB: + * \verbatim + * ( get-abduct ) + * \endverbatim + * Requires enabling option 'produce-abducts' + * @param conj the conjecture term + * @param grammar the grammar for the abduct C + * @param output a term C such that A^C is satisfiable, and A^~B^C is + * unsatisfiable, where A is the current set of assertions and B is + * given in the input by conj + * @return true if it gets C successfully, false otherwise + */ + public boolean getAbduct(Term conj, Grammar grammar, Term output) + { + return getAbduct(pointer, conj.getPointer(), grammar.getPointer(), output.getPointer()); + } + + private native boolean getAbduct( + long pointer, long conjPointer, long grammarPointer, long outputPointer); + + /** + * Block the current model. Can be called only if immediately preceded by a + * SAT or INVALID query. + * SMT-LIB: + * \verbatim + * ( block-model ) + * \endverbatim + * Requires enabling 'produce-models' option and setting 'block-models' option + * to a mode other than "none". + */ + public void blockModel() + { + blockModel(pointer); + } + + private native void blockModel(long pointer); + + /** + * Block the current model values of (at least) the values in terms. Can be + * called only if immediately preceded by a SAT or NOT_ENTAILED query. + * SMT-LIB: + * \verbatim + * ( block-model-values ( + ) ) + * \endverbatim + * Requires enabling 'produce-models' option and setting 'block-models' option + * to a mode other than "none". + */ + public void blockModelValues(Term[] terms) + { + long[] pointers = Utils.getPointers(terms); + blockModelValues(pointer, pointers); + } + + private native void blockModelValues(long pointer, long[] termPointers); + + /** + * Print all instantiations made by the quantifiers module. + * @param out the output stream + */ + // TODO: void printInstantiations(std::ostream& out) + + /** + * Push a level to the assertion stack. + * SMT-LIB: + * \verbatim + * ( push ) + * \endverbatim + */ + public void push() throws CVC5ApiException + { + push(1); + } + + /** + * Push (a) level(s) to the assertion stack. + * SMT-LIB: + * \verbatim + * ( push ) + * \endverbatim + * @param nscopes the number of levels to push + */ + public void push(int nscopes) throws CVC5ApiException + { + Utils.validateUnsigned(nscopes, "nscopes"); + push(pointer, nscopes); + } + + private native void push(long pointer, int nscopes); + + /** + * Remove all assertions. + * SMT-LIB: + * \verbatim + * ( reset-assertions ) + * \endverbatim + */ + public void resetAssertions() + { + resetAssertions(pointer); + } + + private native void resetAssertions(long pointer); + + /** + * Set info. + * SMT-LIB: + * \verbatim + * ( set-info ) + * \endverbatim + * @param keyword the info flag + * @param value the value of the info flag + */ + public void setInfo(String keyword, String value) throws CVC5ApiException + { + setInfo(pointer, keyword, value); + } + + private native void setInfo(long pointer, String keyword, String value) throws CVC5ApiException; + + /** + * Set logic. + * SMT-LIB: + * \verbatim + * ( set-logic ) + * \endverbatim + * @param logic the logic to set */ public void setLogic(String logic) throws CVC5ApiException { setLogic(pointer, logic); } - private native void setLogic(long solverPointer, String logic) throws CVC5ApiException; + private native void setLogic(long pointer, String logic) throws CVC5ApiException; + + /** + * Set option. + * SMT-LIB: + * \verbatim + * ( set-option