diff options
Diffstat (limited to 'src/api')
23 files changed, 5765 insertions, 233 deletions
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<DatatypeConstructor> { // 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<DatatypeConstructor> + { + 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<DatatypeConstructor> 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<DatatypeSelector> { // 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<DatatypeSelector> + { + 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<DatatypeSelector> 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<K, V> +{ + 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<K, V> p = (Pair<K, V>) 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,11 +27,6 @@ public class Solver implements IPointer return pointer; } - public Solver() - { - this.pointer = newSolver(); - } - private native long newSolver(); public void deletePointer() @@ -38,24 +34,2487 @@ public class Solver implements IPointer deletePointer(pointer); } - private static native void deletePointer(long solverPointer); + private static native void deletePointer(long pointer); + + @Override public void finalize() + { + deletePointer(pointer); + } static { Utils.loadLibraries(); } + /* .................................................................... */ + /* Constructors */ + /* .................................................................... */ + + public Solver() + { + this.pointer = newSolver(); + } + + /* .................................................................... */ + /* Sorts Handling */ + /* .................................................................... */ + /** - * Set logic. - * SMT-LIB: ( set-logic <symbol> ) + * @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<DatatypeDecl> 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<Sort> mkDatatypeSorts(List<DatatypeDecl> dtypedecls, Set<Sort> 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<String, Sort>[] fields) + { + long sortPointer = mkRecordSort(pointer, Utils.getPairs(fields)); + return new Sort(this, sortPointer); + } + + private native long mkRecordSort(long pointer, Pair<String, Long>[] 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<Term> 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 <symbol> <sort> ) + * ( declare-fun <symbol> ( ) <sort> ) + * \endverbatim * - * @param logic - * @throws CVC5ApiException + * @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<Sort> 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 <term> ) + * \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 ( <prop_literal> ) ) + * \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 ( <prop_literal>+ ) ) + * \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 <symbol> <datatype_decl> ) + * \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 <symbol> ( <sort>* ) <sort> ) + * \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 <symbol> <numeral> ) + * \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 <function_def> ) + * \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 <function_def> ) + * \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 <function_def> ) + * \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 <function_def> ) + * \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 <function_def> ) + * \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 <function_def> ) + * \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 <function_def> ) + * \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 <function_def> ) + * \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 ( <function_decl>^{n+1} ) ( <term>^{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 ( <function_decl>^{n+1} ) ( <term>^{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 <std::string> ) + * \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 <info_flag> )\verbatim + * @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: + * \verbatim + * ( get-option <keyword> ) + * \endverbatim + * @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 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() + { + long[] retPointers = getUnsatAssumptions(pointer); + return Utils.getTerms(this, retPointers); + } + + private native long[] getUnsatAssumptions(long pointer); + + /** + * 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 ( <term> ) ) + * \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 ( <term>+ ) ) + * \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 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 <q> ) + * \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 <q> ) + * \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 <numeral> ) + * \endverbatim + */ + public void pop() throws CVC5ApiException + { + pop(1); + } + + /** + * Pop (a) level(s) from the assertion stack. + * SMT-LIB: + * \verbatim + * ( pop <numeral> ) + * \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 <conj> ) + * \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 <conj> <g> ) + * \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 <conj> ) + * \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 <conj> <g> ) + * \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 ( <terms>+ ) ) + * \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 <numeral> ) + * \endverbatim + */ + public void push() throws CVC5ApiException + { + push(1); + } + + /** + * Push (a) level(s) to the assertion stack. + * SMT-LIB: + * \verbatim + * ( push <numeral> ) + * \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 <attribute> ) + * \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 <symbol> ) + * \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 <option> ) + * \endverbatim + * @param option the option name + * @param value the option value + */ + public void setOption(String option, String value) + { + setOption(pointer, option, value); + } + + private native void setOption(long pointer, String option, String value); + + /** + * If needed, convert this term to a given sort. Note that the sort of the + * term must be convertible into the target sort. Currently only Int to Real + * conversions are supported. + * @param t the term + * @param s the target sort + * @return the term wrapped into a sort conversion if needed + */ + public Term ensureTermSort(Term t, Sort s) + { + long termPointer = ensureTermSort(pointer, t.getPointer(), s.getPointer()); + return new Term(this, termPointer); + } + + private native long ensureTermSort(long pointer, long termPointer, long sortPointer); + + /** + * Append \p symbol to the current list of universal variables. + * @param sort the sort of the universal variable + * @return the universal variable + */ + public Term mkSygusVar(Sort sort) + { + return mkSygusVar(sort, ""); + } + /** + * Append \p symbol to the current list of universal variables. + * SyGuS v2: + * \verbatim + * ( declare-var <symbol> <sort> ) + * \endverbatim + * @param sort the sort of the universal variable + * @param symbol the name of the universal variable + * @return the universal variable + */ + public Term mkSygusVar(Sort sort, String symbol) + { + long termPointer = mkSygusVar(pointer, sort.getPointer(), symbol); + return new Term(this, termPointer); + } + + private native long mkSygusVar(long pointer, long sortPointer, String symbol); + + /** + * Create a Sygus grammar. The first non-terminal is treated as the starting + * non-terminal, so the order of non-terminals matters. + * + * @param boundVars the parameters to corresponding synth-fun/synth-inv + * @param ntSymbols the pre-declaration of the non-terminal symbols + * @return the grammar + */ + public Grammar mkSygusGrammar(Term[] boundVars, Term[] ntSymbols) + { + long[] boundVarPointers = Utils.getPointers(boundVars); + long[] ntSymbolPointers = Utils.getPointers(ntSymbols); + long grammarPointer = mkSygusGrammar(pointer, boundVarPointers, ntSymbolPointers); + return new Grammar(this, grammarPointer); + } + + private native long mkSygusGrammar( + long pointer, long[] boundVarPointers, long[] ntSymbolPointers); + + /** + * Synthesize n-ary function. + * SyGuS v2: + * \verbatim + * ( synth-fun <symbol> ( <boundVars>* ) <sort> ) + * \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 + * @return the function + */ + public Term synthFun(String symbol, Term[] boundVars, Sort sort) + { + long[] boundVarPointers = Utils.getPointers(boundVars); + long termPointer = synthFun(pointer, symbol, boundVarPointers, sort.getPointer()); + return new Term(this, termPointer); + } + + private native long synthFun( + long pointer, String symbol, long[] boundVarPointers, long sortPointer); + + /** + * Synthesize n-ary function following specified syntactic constraints. + * SyGuS v2: + * \verbatim + * ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> ) + * \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 grammar the syntactic constraints + * @return the function + */ + public Term synthFun(String symbol, Term[] boundVars, Sort sort, Grammar grammar) + { + long[] boundVarPointers = Utils.getPointers(boundVars); + long termPointer = + synthFun(pointer, symbol, boundVarPointers, sort.getPointer(), grammar.getPointer()); + return new Term(this, termPointer); + } + + private native long synthFun( + long pointer, String symbol, long[] boundVarPointers, long sortPointer, long grammarPointer); + + /** + * Synthesize invariant. + * SyGuS v2: + * \verbatim + * ( synth-inv <symbol> ( <boundVars>* ) ) + * \endverbatim + * @param symbol the name of the invariant + * @param boundVars the parameters to this invariant + * @return the invariant + */ + public Term synthInv(String symbol, Term[] boundVars) + { + long[] boundVarPointers = Utils.getPointers(boundVars); + long termPointer = synthInv(pointer, symbol, boundVarPointers); + return new Term(this, termPointer); + } + + private native long synthInv(long pointer, String symbol, long[] boundVarPointers); + + /** + * Synthesize invariant following specified syntactic constraints. + * SyGuS v2: + * \verbatim + * ( synth-inv <symbol> ( <boundVars>* ) <g> ) + * \endverbatim + * @param symbol the name of the invariant + * @param boundVars the parameters to this invariant + * @param grammar the syntactic constraints + * @return the invariant + */ + public Term synthInv(String symbol, Term[] boundVars, Grammar grammar) + { + long[] boundVarPointers = Utils.getPointers(boundVars); + long termPointer = synthInv(pointer, symbol, boundVarPointers, grammar.getPointer()); + return new Term(this, termPointer); + } + + private native long synthInv( + long pointer, String symbol, long[] boundVarPointers, long grammarPointer); + + /** + * Add a forumla to the set of Sygus constraints. + * SyGuS v2: + * \verbatim + * ( constraint <term> ) + * \endverbatim + * @param term the formula to add as a constraint + */ + public void addSygusConstraint(Term term) + { + addSygusConstraint(pointer, term.getPointer()); + } + + private native void addSygusConstraint(long pointer, long termPointer); + /** + * Add a set of Sygus constraints to the current state that correspond to an + * invariant synthesis problem. + * SyGuS v2: + * \verbatim + * ( inv-constraint <inv> <pre> <trans> <post> ) + * \endverbatim + * @param inv the function-to-synthesize + * @param pre the pre-condition + * @param trans the transition relation + * @param post the post-condition + */ + public void addSygusInvConstraint(Term inv, Term pre, Term trans, Term post) + { + addSygusInvConstraint( + pointer, inv.getPointer(), pre.getPointer(), trans.getPointer(), post.getPointer()); + } + + private native void addSygusInvConstraint( + long pointer, long invPointer, long prePointer, long transPointer, long postPointer); + + /** + * Try to find a solution for the synthesis conjecture corresponding to the + * current list of functions-to-synthesize, universal variables and + * constraints. + * SyGuS v2: + * \verbatim + * ( check-synth ) + * \endverbatim + * @return the result of the synthesis conjecture. + */ + public Result checkSynth() + { + long resultPointer = checkSynth(pointer); + return new Result(this, resultPointer); + } + + private native long checkSynth(long pointer); + + /** + * Get the synthesis solution of the given term. This method should be called + * immediately after the solver answers unsat for sygus input. + * @param term the term for which the synthesis solution is queried + * @return the synthesis solution of the given term + */ + public Term getSynthSolution(Term term) + { + long termPointer = getSynthSolution(pointer, term.getPointer()); + return new Term(this, termPointer); + } + + private native long getSynthSolution(long pointer, long termPointer); + + /** + * Get the synthesis solutions of the given terms. This method should be + * called immediately after the solver answers unsat for sygus input. + * @param terms the terms for which the synthesis solutions is queried + * @return the synthesis solutions of the given terms + */ + public Term[] getSynthSolutions(Term[] terms) + { + long[] termPointers = Utils.getPointers(terms); + long[] retPointers = getSynthSolutions(pointer, termPointers); + return Utils.getTerms(this, retPointers); + } + + private native long[] getSynthSolutions(long pointer, long[] termPointers); + + /** + * Print solution for synthesis conjecture to the given output stream. + * @param out the output stream + */ + // TODO: void printSynthSolution(std::ostream& out) + + /** + * @return null term + */ + public Term getNullTerm() + { + long termPointer = getNullTerm(pointer); + return new Term(this, termPointer); + } + + private native long getNullTerm(long pointer); + + /** + * @return null result + */ + public Result getNullResult() + { + long resultPointer = getNullResult(pointer); + return new Result(this, resultPointer); + } + + private native long getNullResult(long pointer); + + /** + * @return null op + */ + public Op getNullOp() + { + long opPointer = getNullOp(pointer); + return new Op(this, opPointer); + } + + private native long getNullOp(long pointer); + + /** + * @return null op + */ + public DatatypeDecl getNullDatatypeDecl() + { + long declPointer = getNullDatatypeDecl(pointer); + return new DatatypeDecl(this, declPointer); + } + + private native long getNullDatatypeDecl(long pointer); } diff --git a/src/api/java/cvc5/Sort.java b/src/api/java/cvc5/Sort.java index a52a249f8..f1f541e35 100644 --- a/src/api/java/cvc5/Sort.java +++ b/src/api/java/cvc5/Sort.java @@ -32,8 +32,7 @@ public class Sort extends AbstractPointer implements Comparable<Sort> return pointer; } - @Override - public void finalize() + @Override public void finalize() { deletePointer(pointer); } @@ -428,7 +427,7 @@ public class Sort extends AbstractPointer implements Comparable<Sort> * Create sorts parameter with Solver.mkParamSort(). * @param params the list of sort parameters to instantiate with */ - Sort instantiate(List<Sort> params) + public Sort instantiate(List<Sort> params) { return instantiate(params.toArray(new Sort[0])); } @@ -438,7 +437,7 @@ public class Sort extends AbstractPointer implements Comparable<Sort> * Create sorts parameter with Solver.mkParamSort(). * @param params the list of sort parameters to instantiate with */ - Sort instantiate(Sort[] params) + public Sort instantiate(Sort[] params) { long[] paramsPointers = Utils.getPointers(params); long sortPointer = instantiate(pointer, paramsPointers); @@ -465,7 +464,7 @@ public class Sort extends AbstractPointer implements Comparable<Sort> * @param sorts the subsorts to be substituted within this sort. * @param replacements the sort replacing the substituted subsorts. */ - Sort substitute(Sort[] sorts, Sort[] replacements) + public Sort substitute(Sort[] sorts, Sort[] replacements) { long[] sortPointers = Utils.getPointers(sorts); long[] replacementPointers = Utils.getPointers(sorts); @@ -513,7 +512,7 @@ public class Sort extends AbstractPointer implements Comparable<Sort> /** * @return the codomain sort of a constructor sort */ - Sort getConstructorCodomainSort() + public Sort getConstructorCodomainSort() { long sortPointer = getConstructorCodomainSort(pointer); return new Sort(solver, sortPointer); @@ -800,4 +799,4 @@ public class Sort extends AbstractPointer implements Comparable<Sort> } private native long[] getTupleSorts(long pointer); -} +}
\ No newline at end of file diff --git a/src/api/java/cvc5/Stat.java b/src/api/java/cvc5/Stat.java index 964f4025c..00ea50797 100644 --- a/src/api/java/cvc5/Stat.java +++ b/src/api/java/cvc5/Stat.java @@ -28,26 +28,25 @@ import java.util.Map; */ public class Stat extends AbstractPointer { - // region construction and destruction - Stat(Solver solver, long pointer) - { - super(solver, pointer); - } + // region construction and destruction + Stat(Solver solver, long pointer) + { + super(solver, pointer); + } - protected static native void deletePointer(long pointer); + protected static native void deletePointer(long pointer); - public long getPointer() - { - return pointer; - } + public long getPointer() + { + return pointer; + } - @Override - public void finalize() - { - deletePointer(pointer); - } + @Override public void finalize() + { + deletePointer(pointer); + } - // endregion + // endregion /** * @return a string representation of this Stat @@ -159,7 +158,7 @@ public class Stat extends AbstractPointer */ public Map<String, Long> getHistogram() { - return getHistogram(pointer); + return getHistogram(pointer); } private native Map<String, Long> getHistogram(long pointer); diff --git a/src/api/java/cvc5/Statistics.java b/src/api/java/cvc5/Statistics.java index ba4828284..a85220e21 100644 --- a/src/api/java/cvc5/Statistics.java +++ b/src/api/java/cvc5/Statistics.java @@ -20,33 +20,31 @@ import java.util.NoSuchElementException; public class Statistics extends AbstractPointer implements Iterable<Pair<String, Stat>> { - // region construction and destruction - Statistics(Solver solver, long pointer) - { - super(solver, pointer); - } + // region construction and destruction + Statistics(Solver solver, long pointer) + { + super(solver, pointer); + } - protected static native void deletePointer(long pointer); + protected static native void deletePointer(long pointer); - public long getPointer() - { - return pointer; - } + public long getPointer() + { + return pointer; + } - @Override - public void finalize() - { - deletePointer(pointer); - } + @Override public void finalize() + { + deletePointer(pointer); + } - // endregion + // endregion /** * @return a string representation of this Statistics */ protected native String toString(long pointer); - /** * Retrieve the statistic with the given name. * Asserts that a statistic with the given name actually exists and throws @@ -70,58 +68,54 @@ public class Statistics extends AbstractPointer implements Iterable<Pair<String, * @param defaulted If set to true, defaulted statistics are shown as well. */ + private native long getIterator(long pointer); + + private native boolean hasNext(long pointer, long iteratorPointer); - private native long getIterator(long pointer); - - private native boolean hasNext(long pointer, long iteratorPointer); - - private native Pair<String, Long> getNext(long pointer, long iteratorPointer) throws CVC5ApiException; - - private native long increment(long pointer, long iteratorPointer) throws CVC5ApiException; - - private native void deleteIteratorPointer(long iteratorPointer); - - public class ConstIterator implements Iterator<Pair<String, Stat>> - { - private long iteratorPointer = 0; - - public ConstIterator() - { - iteratorPointer = getIterator(pointer); - } - - @Override - public boolean hasNext() - { - return Statistics.this.hasNext(pointer, iteratorPointer); - } - - @Override - public Pair<String, Stat> next() - { - try - { - Pair<String, Long> pair = Statistics.this.getNext(pointer, iteratorPointer); - Stat stat = new Stat(solver, pair.second); - this.iteratorPointer = Statistics.this.increment(pointer, iteratorPointer); - return new Pair<>(pair.first, stat); - } - catch(CVC5ApiException e) - { - throw new NoSuchElementException(e.getMessage()); - } - } - - @Override - public void finalize() - { - deleteIteratorPointer(iteratorPointer); - } - } - - @Override - public Iterator<Pair<String, Stat>> iterator() - { - return new ConstIterator(); - } + private native Pair<String, Long> getNext(long pointer, long iteratorPointer) + throws CVC5ApiException; + + private native long increment(long pointer, long iteratorPointer) throws CVC5ApiException; + + private native void deleteIteratorPointer(long iteratorPointer); + + public class ConstIterator implements Iterator<Pair<String, Stat>> + { + private long iteratorPointer = 0; + + public ConstIterator() + { + iteratorPointer = getIterator(pointer); + } + + @Override public boolean hasNext() + { + return Statistics.this.hasNext(pointer, iteratorPointer); + } + + @Override public Pair<String, Stat> next() + { + try + { + Pair<String, Long> pair = Statistics.this.getNext(pointer, iteratorPointer); + Stat stat = new Stat(solver, pair.second); + this.iteratorPointer = Statistics.this.increment(pointer, iteratorPointer); + return new Pair<>(pair.first, stat); + } + catch (CVC5ApiException e) + { + throw new NoSuchElementException(e.getMessage()); + } + } + + @Override public void finalize() + { + deleteIteratorPointer(iteratorPointer); + } + } + + @Override public Iterator<Pair<String, Stat>> iterator() + { + return new ConstIterator(); + } }; diff --git a/src/api/java/cvc5/Term.java b/src/api/java/cvc5/Term.java index 276c288d1..ebf55116b 100644 --- a/src/api/java/cvc5/Term.java +++ b/src/api/java/cvc5/Term.java @@ -15,25 +15,28 @@ package cvc5; +import java.math.BigInteger; import java.util.Iterator; import java.util.List; import java.util.NoSuchElementException; -public class Term - extends AbstractPointer implements Comparable<Term>, Iterable<Term> { +public class Term extends AbstractPointer implements Comparable<Term>, Iterable<Term> +{ // region construction and destruction - Term(Solver solver, long pointer) { + Term(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); } @@ -47,14 +50,15 @@ public class Term * @param t the term to compare to for equality * @return true if the terms 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()) return false; Term term = (Term) t; - if (this.pointer == term.pointer) { + if (this.pointer == term.pointer) + { return true; } return equals(pointer, term.getPointer()); @@ -69,8 +73,8 @@ public class Term * @return a negative integer, zero, or a positive integer as this term * is less than, equal to, or greater than the specified term. */ - @Override - public int compareTo(Term t) { + @Override public int compareTo(Term t) + { return this.compareTo(pointer, t.getPointer()); } @@ -79,7 +83,8 @@ public class Term /** * @return the number of children of this term */ - public int getNumChildren() { + public int getNumChildren() + { return getNumChildren(pointer); } @@ -91,7 +96,8 @@ public class Term * @param index the index of the child term to return * @return the child term with the given index */ - public Term getChild(int index) throws CVC5ApiException { + public Term getChild(int index) throws CVC5ApiException + { Utils.validateUnsigned(index, "index"); long termPointer = getChild(pointer, index); return new Term(solver, termPointer); @@ -102,7 +108,8 @@ public class Term /** * @return the id of this term */ - public long getId() { + public long getId() + { return getId(pointer); } @@ -111,7 +118,8 @@ public class Term /** * @return the kind of this term */ - public Kind getKind() throws CVC5ApiException { + public Kind getKind() throws CVC5ApiException + { int value = getKind(pointer); return Kind.fromInt(value); } @@ -121,7 +129,8 @@ public class Term /** * @return the sort of this term */ - public Sort getSort() { + public Sort getSort() + { long sortPointer = getSort(pointer); return new Sort(solver, sortPointer); } @@ -131,35 +140,37 @@ public class Term /** * @return the result of replacing 'term' by 'replacement' in this term */ - public Term substitute(Term term, Term replacement) { - long termPointer = - substitute(pointer, term.getPointer(), replacement.getPointer()); + public Term substitute(Term term, Term replacement) + { + long termPointer = substitute(pointer, term.getPointer(), replacement.getPointer()); return new Term(solver, termPointer); } - private native long substitute( - long pointer, long termPointer, long replacementPointer); + private native long substitute(long pointer, long termPointer, long replacementPointer); /** * @return the result of simultaneously replacing 'terms' by 'replacements' * in this term */ - public Term substitute(List<Term> terms, List<Term> replacements) { - return substitute( - terms.toArray(new Term[0]), replacements.toArray(new Term[0])); + public Term substitute(List<Term> terms, List<Term> replacements) + { + return substitute(terms.toArray(new Term[0]), replacements.toArray(new Term[0])); } /** * @return the result of simultaneously replacing 'terms' by 'replacements' * in this term */ - public Term substitute(Term[] terms, Term[] replacements) { + public Term substitute(Term[] terms, Term[] replacements) + { long[] termPointers = new long[terms.length]; - for (int i = 0; i < termPointers.length; i++) { + for (int i = 0; i < termPointers.length; i++) + { termPointers[i] = terms[i].getPointer(); } long[] replacementPointers = new long[replacements.length]; - for (int i = 0; i < replacements.length; i++) { + for (int i = 0; i < replacements.length; i++) + { replacementPointers[i] = replacements[i].getPointer(); } @@ -167,13 +178,13 @@ public class Term return new Term(solver, termPointer); } - private native long substitute( - long pointer, long[] termPointers, long[] replacementPointers); + private native long substitute(long pointer, long[] termPointers, long[] replacementPointers); /** * @return true iff this term has an operator */ - public boolean hasOp() { + public boolean hasOp() + { return hasOp(pointer); } @@ -183,7 +194,8 @@ public class Term * @return the Op used to create this term * Note: This is safe to call when hasOp() returns true. */ - public Op getOp() { + public Op getOp() + { long opPointer = getOp(pointer); return new Op(solver, opPointer); } @@ -193,7 +205,8 @@ public class Term /** * @return true if this Term is a null term */ - public boolean isNull() { + public boolean isNull() + { return isNull(pointer); } @@ -205,7 +218,8 @@ public class Term * * @return the base value */ - public Term getConstArrayBase() { + public Term getConstArrayBase() + { long termPointer = getConstArrayBase(pointer); return new Term(solver, termPointer); } @@ -218,10 +232,12 @@ public class Term * * @return the elements of the constant sequence. */ - public Term[] getConstSequenceElements() { + public Term[] getConstSequenceElements() + { long[] termPointers = getConstSequenceElements(pointer); Term[] terms = new Term[termPointers.length]; - for (int i = 0; i < termPointers.length; i++) { + for (int i = 0; i < termPointers.length; i++) + { terms[i] = new Term(solver, termPointers[i]); } @@ -235,7 +251,8 @@ public class Term * * @return the Boolean negation of this term */ - public Term notTerm() { + public Term notTerm() + { long termPointer = notTerm(pointer); return new Term(solver, termPointer); } @@ -248,7 +265,8 @@ public class Term * @param t a Boolean term * @return the conjunction of this term and the given term */ - public Term andTerm(Term t) { + public Term andTerm(Term t) + { long termPointer = andTerm(pointer, t.getPointer()); return new Term(solver, termPointer); } @@ -261,7 +279,8 @@ public class Term * @param t a Boolean term * @return the disjunction of this term and the given term */ - public Term orTerm(Term t) { + public Term orTerm(Term t) + { long termPointer = orTerm(pointer, t.getPointer()); return new Term(solver, termPointer); } @@ -274,7 +293,8 @@ public class Term * @param t a Boolean term * @return the exclusive disjunction of this term and the given term */ - public Term xorTerm(Term t) { + public Term xorTerm(Term t) + { long termPointer = xorTerm(pointer, t.getPointer()); return new Term(solver, termPointer); } @@ -287,7 +307,8 @@ public class Term * @param t a Boolean term * @return the Boolean equivalence of this term and the given term */ - public Term eqTerm(Term t) { + public Term eqTerm(Term t) + { long termPointer = eqTerm(pointer, t.getPointer()); return new Term(solver, termPointer); } @@ -300,7 +321,8 @@ public class Term * @param t a Boolean term * @return the implication of this term and the given term */ - public Term impTerm(Term t) { + public Term impTerm(Term t) + { long termPointer = impTerm(pointer, t.getPointer()); return new Term(solver, termPointer); } @@ -314,9 +336,9 @@ public class Term * @param elseTerm the 'else' term * @return the if-then-else term with this term as the Boolean condition */ - public Term iteTerm(Term thenTerm, Term elseTerm) { - long termPointer = - iteTerm(pointer, thenTerm.getPointer(), elseTerm.getPointer()); + public Term iteTerm(Term thenTerm, Term elseTerm) + { + long termPointer = iteTerm(pointer, thenTerm.getPointer(), elseTerm.getPointer()); return new Term(solver, termPointer); } @@ -330,7 +352,8 @@ public class Term /** * @return true if the term is an integer that fits within a Java integer. */ - public boolean isInt() { + public boolean isInt() + { return isInt(pointer); } @@ -340,7 +363,8 @@ public class Term * @return the stored integer as an int. * Note: Asserts isInt(). */ - public int getInt() { + public int getInt() + { return getInt(pointer); } @@ -349,7 +373,8 @@ public class Term /** * @return true if the term is an integer that fits within a Java long. */ - public boolean isLong() { + public boolean isLong() + { return isLong(pointer); } @@ -359,7 +384,8 @@ public class Term * @return the stored integer as a long. * Note: Asserts isLong(). */ - public long getLong() { + public long getLong() + { return getLong(pointer); } @@ -368,7 +394,8 @@ public class Term /** * @return true if the term is an integer. */ - public boolean isInteger() { + public boolean isInteger() + { return isInteger(pointer); } @@ -378,7 +405,8 @@ public class Term * @return the stored integer in (decimal) string representation. * Note: Asserts isInteger(). */ - public String getInteger() { + public String getInteger() + { return getInteger(pointer); } @@ -387,7 +415,8 @@ public class Term /** * @return true if the term is a string constant. */ - public boolean isString() { + public boolean isString() + { return isString(pointer); } @@ -400,43 +429,73 @@ public class Term * term in some string representation, whatever data it may hold. * Asserts isString(). */ - public String getString() { + public String getString() + { return getString(pointer); } private native String getString(long pointer); - public class ConstIterator implements Iterator<Term> { + /** + * @return true if the term is a rational value. + */ + public boolean isRealValue() + { + return isRealValue(pointer); + } + + private native boolean isRealValue(long pointer); + + /** + * Asserts isRealValue(). + * @return the representation of a rational value as a pair of its numerator + * and denominator. + */ + public Pair<BigInteger, BigInteger> getRealValue() + { + String rational = getRealValue(pointer); + return Utils.getRational(rational); + } + + private native String getRealValue(long pointer); + + public class ConstIterator implements Iterator<Term> + { private int currentIndex; private int size; - public ConstIterator() { + public ConstIterator() + { currentIndex = -1; size = getNumChildren(); } - @Override - public boolean hasNext() { + @Override public boolean hasNext() + { return currentIndex < size - 1; } - @Override - public Term next() { - if (currentIndex >= size - 1) { + @Override public Term next() + { + if (currentIndex >= size - 1) + { throw new NoSuchElementException(); } currentIndex++; - try { + try + { return getChild(currentIndex); - } catch (CVC5ApiException e) { + } + catch (CVC5ApiException e) + { e.printStackTrace(); throw new RuntimeException(e.getMessage()); } } } - @Override - public Iterator<Term> iterator() { + @Override public Iterator<Term> iterator() + { return new ConstIterator(); } } diff --git a/src/api/java/cvc5/Utils.java b/src/api/java/cvc5/Utils.java index 7f32932e4..077b77168 100644 --- a/src/api/java/cvc5/Utils.java +++ b/src/api/java/cvc5/Utils.java @@ -1,4 +1,3 @@ - /****************************************************************************** * Top contributors (to current version): * Mudathir Mohamed @@ -17,8 +16,11 @@ package cvc5; import java.io.IOException; +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.List; -class Utils +public class Utils { static { @@ -32,4 +34,180 @@ class Utils { System.loadLibrary("cvc5jni"); } + + /** + * return sorts array from array of pointers + */ + public static Sort[] getSorts(Solver solver, long[] pointers) + { + Sort[] sorts = new Sort[pointers.length]; + for (int i = 0; i < pointers.length; i++) + { + sorts[i] = new Sort(solver, pointers[i]); + } + return sorts; + } + + /** + * return terms array from array of pointers + */ + public static Term[] getTerms(Solver solver, long[] pointers) + { + Term[] terms = new Term[pointers.length]; + for (int i = 0; i < pointers.length; i++) + { + terms[i] = new Term(solver, pointers[i]); + } + return terms; + } + + /** + * get pointers from one dimensional array + */ + public static long[] getPointers(IPointer[] objects) + { + long[] pointers = new long[objects.length]; + for (int i = 0; i < pointers.length; i++) + { + pointers[i] = objects[i].getPointer(); + } + return pointers; + } + + /** + * get pointers from two dimensional matrix + */ + public static long[][] getPointers(IPointer[][] objects) + { + long[][] pointers = new long[objects.length][]; + for (int i = 0; i < pointers.length; i++) + { + pointers[i] = new long[objects[i].length]; + for (int j = 0; j < objects[i].length; j++) + { + pointers[i][j] = objects[i][j].getPointer(); + } + } + return pointers; + } + + public static void validateUnsigned(int integer, String name) throws CVC5ApiException + { + if (integer < 0) + { + throw new CVC5ApiException("Expected " + name + " '" + integer + "' to be non negative."); + } + } + + public static void validateUnsigned(long integer, String name) throws CVC5ApiException + { + if (integer < 0) + { + throw new CVC5ApiException("Expected " + name + " '" + integer + "' to be non negative."); + } + } + + public static void validateUnsigned(int[] integers, String name) throws CVC5ApiException + { + for (int i = 0; i < integers.length; i++) + { + if (integers[i] < 0) + { + throw new CVC5ApiException( + "Expected " + name + "[" + i + "] '" + integers[i] + "' to be non negative."); + } + } + } + + public static void validateUnsigned(long[] integers, String name) throws CVC5ApiException + { + for (int i = 0; i < integers.length; i++) + { + if (integers[i] < 0) + { + throw new CVC5ApiException( + "Expected " + name + "[" + i + "] '" + integers[i] + "' to be non negative."); + } + } + } + + public static <K> Pair<K, Long>[] getPairs(Pair<K, ? extends AbstractPointer>[] abstractPointers) + { + Pair<K, Long>[] pointers = new Pair[abstractPointers.length]; + for (int i = 0; i < pointers.length; i++) + { + pointers[i] = new Pair<>(abstractPointers[i].first, abstractPointers[i].second.getPointer()); + } + return pointers; + } + + /** + Convert a rational string a/b to a pair of BigIntegers + */ + public static Pair<BigInteger, BigInteger> getRational(String rational) + { + if (rational.contains("/")) + { + String[] pair = rational.split("/"); + return new Pair<>(new BigInteger(pair[0]), new BigInteger(pair[1])); + } + return new Pair<>(new BigInteger(rational), new BigInteger("1")); + } + + /** + * Get the string version of define-fun command. + * @param f the function to print + * @param params the function parameters + * @param body the function body + * @return a string version of define-fun + */ + private static String defineFunToString(Term f, Term[] params, Term body) + { + Sort sort = f.getSort(); + if (sort.isFunction()) + { + sort = sort.getFunctionCodomainSort(); + } + StringBuilder ss = new StringBuilder(); + ss.append("(define-fun ").append(f).append(" ("); + for (int i = 0; i < params.length; ++i) + { + if (i > 0) + { + ss.append(' '); + } + ss.append('(').append(params[i]).append(' ').append(params[i].getSort()).append(')'); + } + ss.append(") ").append(sort).append(' ').append(body).append(')'); + return ss.toString(); + } + + /** + * Print solutions for synthesis conjecture to the standard output stream. + * @param terms the terms for which the synthesis solutions were retrieved + * @param sols the synthesis solutions of the given terms + */ + public static void printSynthSolutions(Term[] terms, Term[] sols) throws CVC5ApiException + { + System.out.println('('); + + for (int i = 0; i < terms.length; ++i) + { + List<Term> params = new ArrayList<>(); + Term body = null; + if (sols[i].getKind() == Kind.LAMBDA) + { + for (Term t : sols[i].getChild(0)) + { + params.add(t); + } + body = sols[i].getChild(1); + } + if (body != null) + { + System.out.println(" " + defineFunToString(terms[i], params.toArray(new Term[0]), body)); + } + } + System.out.println(')'); + } } diff --git a/src/api/java/jni/cvc5JavaApi.h b/src/api/java/jni/cvc5JavaApi.h index 2aa860f40..fc4399fed 100644 --- a/src/api/java/jni/cvc5JavaApi.h +++ b/src/api/java/jni/cvc5JavaApi.h @@ -13,6 +13,8 @@ * The cvc5 Java API. */ +#include <jni.h> + #ifndef CVC5__JAVA_API_H #define CVC5__JAVA_API_H @@ -36,3 +38,49 @@ CVC5_JAVA_API_TRY_CATCH_END(env) \ return returnValue; #endif // CVC5__JAVA_API_H + +/** + * Convert pointers coming from Java to cvc5 objects + * @tparam T cvc5 class (Term, Sort, Grammar, etc) + * @param env jni environment + * @param jPointers pointers coming from java + * @return a vector of cvc5 objects + */ +template <class T> +std::vector<T> getObjectsFromPointers(JNIEnv* env, jlongArray jPointers) +{ + // get the size of pointers + jsize size = env->GetArrayLength(jPointers); + // allocate a buffer for c pointers + std::vector<jlong> cPointers(size); + // copy java array to the buffer + env->GetLongArrayRegion(jPointers, 0, size, cPointers.data()); + // copy the terms into a vector + std::vector<T> objects; + for (jlong pointer : cPointers) + { + T* term = reinterpret_cast<T*>(pointer); + objects.push_back(*term); + } + return objects; +} + +/** + * Convert cvc5 objects into pointers + * @tparam T cvc5 class (Term, Sort, Grammar, etc) + * @param env jni environment + * @param objects cvc5 objects + * @return jni array of pointers + */ +template <class T> +jlongArray getPointersFromObjects(JNIEnv* env, std::vector<T> objects) +{ + std::vector<jlong> pointers(objects.size()); + for (size_t i = 0; i < objects.size(); i++) + { + pointers[i] = reinterpret_cast<jlong>(new T(objects[i])); + } + jlongArray ret = env->NewLongArray(objects.size()); + env->SetLongArrayRegion(ret, 0, objects.size(), pointers.data()); + return ret; +}
\ No newline at end of file diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp index 9d7690e59..9bcecd07f 100644 --- a/src/api/java/jni/cvc5_Solver.cpp +++ b/src/api/java/jni/cvc5_Solver.cpp @@ -28,7 +28,7 @@ using namespace cvc5::api; JNIEXPORT jlong JNICALL Java_cvc5_Solver_newSolver(JNIEnv*, jobject) { Solver* solver = new Solver(); - return ((jlong)solver); + return reinterpret_cast<jlong>(solver); } /* @@ -37,27 +37,2542 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_newSolver(JNIEnv*, jobject) * Signature: (J)V */ JNIEXPORT void JNICALL Java_cvc5_Solver_deletePointer(JNIEnv*, - jclass, + jclass, + jlong pointer) +{ + delete (reinterpret_cast<Solver*>(pointer)); +} + +/* + * Class: cvc5_Solver + * Method: getNullSort + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullSort(JNIEnv* env, + jobject, jlong pointer) { - delete ((Solver*)pointer); + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sortPointer = new Sort(solver->getNullSort()); + return reinterpret_cast<jlong>(sortPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getBooleanSort + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getBooleanSort(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sortPointer = new Sort(solver->getBooleanSort()); + return reinterpret_cast<jlong>(sortPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getIntegerSort + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getIntegerSort(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sortPointer = new Sort(solver->getIntegerSort()); + return reinterpret_cast<jlong>(sortPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getRealSort + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getRealSort(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sortPointer = new Sort(solver->getRealSort()); + return reinterpret_cast<jlong>(sortPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getRegExpSort + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getRegExpSort(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sortPointer = new Sort(solver->getRegExpSort()); + return reinterpret_cast<jlong>(sortPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getRoundingModeSort + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getRoundingModeSort(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sortPointer = new Sort(solver->getRoundingModeSort()); + return reinterpret_cast<jlong>(sortPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getStringSort + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getStringSort(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sortPointer = new Sort(solver->getStringSort()); + return reinterpret_cast<jlong>(sortPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkArraySort + * Signature: (JJJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkArraySort(JNIEnv* env, + jobject, + jlong pointer, + jlong indexSortPointer, + jlong elementSortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* indexSort = reinterpret_cast<Sort*>(indexSortPointer); + Sort* elementSort = reinterpret_cast<Sort*>(elementSortPointer); + Sort* retPointer = new Sort(solver->mkArraySort(*indexSort, *elementSort)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkBitVectorSort + * Signature: (JI)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBitVectorSort(JNIEnv* env, + jobject, + jlong pointer, + jint size) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sortPointer = new Sort(solver->mkBitVectorSort((uint32_t)size)); + return reinterpret_cast<jlong>(sortPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkFloatingPointSort + * Signature: (JII)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkFloatingPointSort( + JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sortPointer = + new Sort(solver->mkFloatingPointSort((uint32_t)exp, (uint32_t)sig)); + return reinterpret_cast<jlong>(sortPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkDatatypeSort + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkDatatypeSort( + JNIEnv* env, jobject, jlong pointer, jlong datatypeDeclPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + DatatypeDecl* decl = reinterpret_cast<DatatypeDecl*>(datatypeDeclPointer); + Sort* retPointer = new Sort(solver->mkDatatypeSort(*decl)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkDatatypeSorts + * Signature: (J[J)[J + */ +JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_mkDatatypeSorts__J_3J( + JNIEnv* env, jobject, jlong pointer, jlongArray jDecls) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<DatatypeDecl> decls = + getObjectsFromPointers<DatatypeDecl>(env, jDecls); + std::vector<Sort> sorts = solver->mkDatatypeSorts(decls); + std::vector<jlong> sortPointers(sorts.size()); + + for (size_t i = 0; i < sorts.size(); i++) + { + sortPointers[i] = reinterpret_cast<jlong>(new Sort(sorts[i])); + } + + jlongArray ret = env->NewLongArray(sorts.size()); + env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data()); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Solver + * Method: mkDatatypeSorts + * Signature: (J[J[J)[J + */ +JNIEXPORT jlongArray JNICALL +Java_cvc5_Solver_mkDatatypeSorts__J_3J_3J(JNIEnv* env, + jobject, + jlong pointer, + jlongArray jDecls, + jlongArray jUnresolved) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<DatatypeDecl> decls = + getObjectsFromPointers<DatatypeDecl>(env, jDecls); + std::vector<Sort> cUnresolved = + getObjectsFromPointers<Sort>(env, jUnresolved); + std::set<Sort> unresolved(cUnresolved.begin(), cUnresolved.end()); + std::vector<Sort> sorts = solver->mkDatatypeSorts(decls, unresolved); + jlongArray ret = getPointersFromObjects<Sort>(env, sorts); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Solver + * Method: mkFunctionSort + * Signature: (JJJ)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_mkFunctionSort__JJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong domainPointer, + jlong codomainPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* domain = reinterpret_cast<Sort*>(domainPointer); + Sort* codomain = reinterpret_cast<Sort*>(codomainPointer); + Sort* sortPointer = new Sort(solver->mkFunctionSort(*domain, *codomain)); + return reinterpret_cast<jlong>(sortPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkFunctionSort + * Signature: (J[JJ)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_mkFunctionSort__J_3JJ(JNIEnv* env, + jobject, + jlong pointer, + jlongArray sortPointers, + jlong codomainPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* codomain = reinterpret_cast<Sort*>(codomainPointer); + std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers); + Sort* retPointer = new Sort(solver->mkFunctionSort(sorts, *codomain)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkParamSort + * Signature: (JLjava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkParamSort(JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + Sort* retPointer = new Sort(solver->mkParamSort(cSymbol)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkPredicateSort + * Signature: (J[J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPredicateSort( + JNIEnv* env, jobject, jlong pointer, jlongArray sortPointers) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers); + Sort* retPointer = new Sort(solver->mkPredicateSort(sorts)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkRecordSort + * Signature: (J[Lcvc5/Pair;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRecordSort(JNIEnv* env, + jobject, + jlong pointer, + jobjectArray jFields) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + jsize size = env->GetArrayLength(jFields); + // Lcvc5/Pair; is signature of cvc5.Pair<String, Long> + jclass pairClass = env->FindClass("Lcvc5/Pair;"); + jclass longClass = env->FindClass("Ljava/lang/Long;"); + // Ljava/lang/Object; is the signature of cvc5.Pair.first field + jfieldID firstFieldId = + env->GetFieldID(pairClass, "first", "Ljava/lang/Object;"); + // Ljava/lang/Object; is the signature of cvc5.Pair.second field + jfieldID secondFieldId = + env->GetFieldID(pairClass, "second", "Ljava/lang/Object;"); + // we need to call method longValue to get long Long object + jmethodID methodId = env->GetMethodID(longClass, "longValue", "()J"); + + std::vector<std::pair<std::string, Sort>> cFields; + for (jsize i = 0; i < size; i++) + { + // get the pair at index i + jobject object = env->GetObjectArrayElement(jFields, i); + + // get the object at cvc5.Pair.first and convert it to char * + jstring jFirst = (jstring)env->GetObjectField(object, firstFieldId); + const char* cFirst = env->GetStringUTFChars(jFirst, nullptr); + + // get the object at cvc5.Pair.second and convert it to Sort + jobject jSecond = env->GetObjectField(object, secondFieldId); + jlong sortPointer = env->CallLongMethod(jSecond, methodId); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + + // add the pair to to the list of fields + cFields.push_back(std::make_pair(std::string(cFirst), *sort)); + } + // get the record sort from the solver + Sort* retPointer = new Sort(solver->mkRecordSort(cFields)); + // return a pointer to the sort + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkSetSort + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSetSort(JNIEnv* env, + jobject, + jlong pointer, + jlong elemSortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* elemSort = reinterpret_cast<Sort*>(elemSortPointer); + Sort* retPointer = new Sort(solver->mkSetSort(*elemSort)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkBagSort + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBagSort(JNIEnv* env, + jobject, + jlong pointer, + jlong elemSortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* elemSort = reinterpret_cast<Sort*>(elemSortPointer); + Sort* retPointer = new Sort(solver->mkBagSort(*elemSort)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkSequenceSort + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSequenceSort(JNIEnv* env, + jobject, + jlong pointer, + jlong elemSortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* elemSort = reinterpret_cast<Sort*>(elemSortPointer); + Sort* sortPointer = new Sort(solver->mkSequenceSort(*elemSort)); + return reinterpret_cast<jlong>(sortPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkUninterpretedSort + * Signature: (JLjava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkUninterpretedSort(JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* cSymbol = env->GetStringUTFChars(jSymbol, nullptr); + Sort* sort = new Sort(solver->mkUninterpretedSort(std::string(cSymbol))); + env->ReleaseStringUTFChars(jSymbol, cSymbol); + return reinterpret_cast<jlong>(sort); + + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkSortConstructorSort + * Signature: (JLjava/lang/String;I)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSortConstructorSort( + JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + Sort* retPointer = + new Sort(solver->mkSortConstructorSort(cSymbol, (size_t)arity)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTupleSort + * Signature: (J[J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTupleSort(JNIEnv* env, + jobject, + jlong pointer, + jlongArray sortPointers) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers); + Sort* retPointer = new Sort(solver->mkTupleSort(sorts)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTerm + * Signature: (JI)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JI(JNIEnv* env, + jobject, + jlong pointer, + jint kindValue) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Kind kind = (Kind)kindValue; + Term* retPointer = new Term(solver->mkTerm(kind)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTerm + * Signature: (JIJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JIJ( + JNIEnv* env, jobject, jlong pointer, jint kindValue, jlong childPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Kind kind = (Kind)kindValue; + Term* child = reinterpret_cast<Term*>(childPointer); + Term* termPointer = new Term(solver->mkTerm(kind, *child)); + return reinterpret_cast<jlong>(termPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTerm + * Signature: (JIJJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JIJJ(JNIEnv* env, + jobject, + jlong pointer, + jint kindValue, + jlong child1Pointer, + jlong child2Pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Kind kind = (Kind)kindValue; + Term* child1 = reinterpret_cast<Term*>(child1Pointer); + Term* child2 = reinterpret_cast<Term*>(child2Pointer); + Term* termPointer = new Term(solver->mkTerm(kind, *child1, *child2)); + return reinterpret_cast<jlong>(termPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTerm + * Signature: (JIJJJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JIJJJ(JNIEnv* env, + jobject, + jlong pointer, + jint kindValue, + jlong child1Pointer, + jlong child2Pointer, + jlong child3Pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Kind kind = (Kind)kindValue; + Term* child1 = reinterpret_cast<Term*>(child1Pointer); + Term* child2 = reinterpret_cast<Term*>(child2Pointer); + Term* child3 = reinterpret_cast<Term*>(child3Pointer); + Term* retPointer = new Term(solver->mkTerm(kind, *child1, *child2, *child3)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTerm + * Signature: (JI[J)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_mkTerm__JI_3J(JNIEnv* env, + jobject, + jlong pointer, + jint kindValue, + jlongArray childrenPointers) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Kind kind = (Kind)kindValue; + std::vector<Term> children = + getObjectsFromPointers<Term>(env, childrenPointers); + Term* retPointer = new Term(solver->mkTerm(kind, children)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTerm + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJ(JNIEnv* env, + jobject, + jlong pointer, + jlong opPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Op* op = reinterpret_cast<Op*>(opPointer); + Term* retPointer = new Term(solver->mkTerm(*op)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTerm + * Signature: (JJJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJJ( + JNIEnv* env, jobject, jlong pointer, jlong opPointer, jlong childPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Op* op = reinterpret_cast<Op*>(opPointer); + Term* child = reinterpret_cast<Term*>(childPointer); + Term* retPointer = new Term(solver->mkTerm(*op, *child)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTerm + * Signature: (JJJJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong opPointer, + jlong child1Pointer, + jlong child2Pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Op* op = reinterpret_cast<Op*>(opPointer); + Term* child1 = reinterpret_cast<Term*>(child1Pointer); + Term* child2 = reinterpret_cast<Term*>(child2Pointer); + Term* retPointer = new Term(solver->mkTerm(*op, *child1, *child2)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTerm + * Signature: (JJJJJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTerm__JJJJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong opPointer, + jlong child1Pointer, + jlong child2Pointer, + jlong child3Pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Op* op = reinterpret_cast<Op*>(opPointer); + Term* child1 = reinterpret_cast<Term*>(child1Pointer); + Term* child2 = reinterpret_cast<Term*>(child2Pointer); + Term* child3 = reinterpret_cast<Term*>(child3Pointer); + Term* retPointer = new Term(solver->mkTerm(*op, *child1, *child2, *child3)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTerm + * Signature: (JJ[J)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_mkTerm__JJ_3J(JNIEnv* env, + jobject, + jlong pointer, + jlong opPointer, + jlongArray childrenPointers) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Op* op = reinterpret_cast<Op*>(opPointer); + std::vector<Term> children = + getObjectsFromPointers<Term>(env, childrenPointers); + Term* retPointer = new Term(solver->mkTerm(*op, children)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTuple + * Signature: (J[J[J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTuple(JNIEnv* env, + jobject, + jlong pointer, + jlongArray sortPointers, + jlongArray termPointers) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers); + std::vector<Term> terms = getObjectsFromPointers<Term>(env, termPointers); + Term* retPointer = new Term(solver->mkTuple(sorts, terms)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkOp + * Signature: (JI)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JI(JNIEnv* env, + jobject, + jlong pointer, + jint kindValue) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Kind kind = (Kind)kindValue; + Op* retPointer = new Op(solver->mkOp(kind)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkOp + * Signature: (JILjava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JILjava_lang_String_2( + JNIEnv* env, jobject, jlong pointer, jint kindValue, jstring jArg) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Kind kind = (Kind)kindValue; + const char* s = env->GetStringUTFChars(jArg, nullptr); + std::string cArg(s); + + Op* retPointer = new Op(solver->mkOp(kind, cArg)); + + env->ReleaseStringUTFChars(jArg, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkOp + * Signature: (JII)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JII( + JNIEnv* env, jobject, jlong pointer, jint kindValue, jint arg) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Kind kind = (Kind)kindValue; + Op* retPointer = new Op(solver->mkOp(kind, (uint32_t)arg)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkOp + * Signature: (JIII)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JIII( + JNIEnv* env, jobject, jlong pointer, jint kindValue, jint arg1, jint arg2) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Kind kind = (Kind)kindValue; + Op* retPointer = new Op(solver->mkOp(kind, (uint32_t)arg1, (uint32_t)arg2)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkOp + * Signature: (JI[I)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkOp__JI_3I( + JNIEnv* env, jobject, jlong pointer, jint kindValue, jintArray jArgs) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Kind kind = (Kind)kindValue; + + jsize size = env->GetArrayLength(jArgs); + jint* argElements = env->GetIntArrayElements(jArgs, nullptr); + + std::vector<uint32_t> cArgs(size); + for (jsize i = 0; i < size; i++) + { + cArgs[i] = (uint32_t)argElements[i]; + } + env->ReleaseIntArrayElements(jArgs, argElements, 0); + + Op* retPointer = new Op(solver->mkOp(kind, cArgs)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkTrue + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkTrue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* termPointer = new Term(solver->mkTrue()); + return reinterpret_cast<jlong>(termPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkFalse + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkFalse(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* termPointer = new Term(solver->mkFalse()); + return reinterpret_cast<jlong>(termPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkBoolean + * Signature: (JZ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBoolean(JNIEnv* env, + jobject, + jlong pointer, + jboolean val) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkBoolean((bool)val)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkPi + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPi(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkPi()); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkInteger + * Signature: (JLjava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkInteger__JLjava_lang_String_2( + JNIEnv* env, jobject, jlong pointer, jstring jS) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jS, nullptr); + std::string cS(s); + Term* retPointer = new Term(solver->mkInteger(cS)); + env->ReleaseStringUTFChars(jS, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkInteger + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkInteger__JJ(JNIEnv* env, + jobject, + jlong pointer, + jlong val) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* termPointer = new Term(solver->mkInteger((int64_t)val)); + return reinterpret_cast<jlong>(termPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkReal + * Signature: (JLjava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkReal__JLjava_lang_String_2( + JNIEnv* env, jobject, jlong pointer, jstring jS) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jS, nullptr); + std::string cS(s); + Term* retPointer = new Term(solver->mkReal(cS)); + env->ReleaseStringUTFChars(jS, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkRealValue + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRealValue(JNIEnv* env, + jobject, + jlong pointer, + jlong val) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkReal((int64_t)val)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkReal + * Signature: (JJJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkReal__JJJ( + JNIEnv* env, jobject, jlong pointer, jlong num, jlong den) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkReal((int64_t)num, (int64_t)den)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkRegexpEmpty + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRegexpEmpty(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkRegexpEmpty()); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkRegexpSigma + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRegexpSigma(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkRegexpSigma()); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkEmptySet + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptySet(JNIEnv* env, + jobject, + jlong pointer, + jlong sortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* retPointer = new Term(solver->mkEmptySet(*sort)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkEmptyBag + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptyBag(JNIEnv* env, + jobject, + jlong pointer, + jlong sortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* retPointer = new Term(solver->mkEmptyBag(*sort)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkSepNil + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSepNil(JNIEnv* env, + jobject, + jlong pointer, + jlong sortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* retPointer = new Term(solver->mkSepNil(*sort)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkString + * Signature: (JLjava/lang/String;Z)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkString__JLjava_lang_String_2Z( + JNIEnv* env, jobject, jlong pointer, jstring jS, jboolean useEscSequences) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jS, nullptr); + std::string cS(s); + Term* retPointer = new Term(solver->mkString(cS, (bool)useEscSequences)); + env->ReleaseStringUTFChars(jS, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkEmptySequence + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptySequence(JNIEnv* env, + jobject, + jlong pointer, + jlong sortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* retPointer = new Term(solver->mkEmptySequence(*sort)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkUniverseSet + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkUniverseSet(JNIEnv* env, + jobject, + jlong pointer, + jlong sortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* retPointer = new Term(solver->mkUniverseSet(*sort)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkBitVector + * Signature: (JIJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBitVector__JIJ( + JNIEnv* env, jobject, jlong pointer, jint size, jlong val) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = + new Term(solver->mkBitVector((uint32_t)size, (uint64_t)val)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkBitVector + * Signature: (JILjava/lang/String;I)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkBitVector__JILjava_lang_String_2I( + JNIEnv* env, jobject, jlong pointer, jint size, jstring jS, jint base) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jS, nullptr); + std::string cS(s); + Term* retPointer = + new Term(solver->mkBitVector((uint32_t)size, cS, (uint32_t)base)); + env->ReleaseStringUTFChars(jS, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkConstArray + * Signature: (JJJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkConstArray( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jlong valPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* val = reinterpret_cast<Term*>(valPointer); + Term* retPointer = new Term(solver->mkConstArray(*sort, *val)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkPosInf + * Signature: (JII)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPosInf( + JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkPosInf((uint32_t)exp, (uint32_t)sig)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkNegInf + * Signature: (JII)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkNegInf( + JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkNegInf((uint32_t)exp, (uint32_t)sig)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkNaN + * Signature: (JII)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_mkNaN(JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkNaN((uint32_t)exp, (uint32_t)sig)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkPosZero + * Signature: (JII)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkPosZero( + JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkPosZero((uint32_t)exp, (uint32_t)sig)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkNegZero + * Signature: (JII)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkNegZero( + JNIEnv* env, jobject, jlong pointer, jint exp, jint sig) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkNegZero((uint32_t)exp, (uint32_t)sig)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkRoundingMode + * Signature: (JI)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRoundingMode(JNIEnv* env, + jobject, + jlong pointer, + jint rm) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkRoundingMode((RoundingMode)rm)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkUninterpretedConst + * Signature: (JJI)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkUninterpretedConst( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jint index) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* retPointer = + new Term(solver->mkUninterpretedConst(*sort, (int32_t)index)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkAbstractValue + * Signature: (JLjava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkAbstractValue__JLjava_lang_String_2( + JNIEnv* env, jobject, jlong pointer, jstring jIndex) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jIndex, nullptr); + std::string cIndex(s); + Term* retPointer = new Term(solver->mkAbstractValue(cIndex)); + env->ReleaseStringUTFChars(jIndex, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkAbstractValue + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkAbstractValue__JJ(JNIEnv* env, + jobject, + jlong pointer, + jlong index) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->mkAbstractValue((uint64_t)index)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkFloatingPoint + * Signature: (JIIJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkFloatingPoint( + JNIEnv* env, jobject, jlong pointer, jint exp, jint sig, jlong valPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* val = reinterpret_cast<Term*>(valPointer); + Term* retPointer = + new Term(solver->mkFloatingPoint((uint32_t)exp, (uint32_t)sig, *val)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkConst + * Signature: (JJLjava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkConst__JJLjava_lang_String_2( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jstring jSymbol) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + Term* retPointer = new Term(solver->mkConst(*sort, cSymbol)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkConst + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkConst__JJ(JNIEnv* env, + jobject, + jlong pointer, + jlong sortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* retPointer = new Term(solver->mkConst(*sort)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkVar + * Signature: (JJLjava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkVar( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jstring jSymbol) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + Term* ret = new Term(solver->mkVar(*sort, cSymbol)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkDatatypeConstructorDecl + * Signature: (JLjava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkDatatypeConstructorDecl( + JNIEnv* env, jobject, jlong pointer, jstring jName) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jName, nullptr); + std::string cName(s); + + DatatypeConstructorDecl* retPointer = + new DatatypeConstructorDecl(solver->mkDatatypeConstructorDecl(cName)); + env->ReleaseStringUTFChars(jName, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkDatatypeDecl + * Signature: (JLjava/lang/String;Z)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2Z( + JNIEnv* env, jobject, jlong pointer, jstring jName, jboolean isCoDatatype) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jName, nullptr); + std::string cName(s); + DatatypeDecl* retPointer = + new DatatypeDecl(solver->mkDatatypeDecl(cName, (bool)isCoDatatype)); + env->ReleaseStringUTFChars(jName, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkDatatypeDecl + * Signature: (JLjava/lang/String;JZ)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2JZ(JNIEnv* env, + jobject, + jlong pointer, + jstring jName, + jlong paramPointer, + jboolean isCoDatatype) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jName, nullptr); + std::string cName(s); + Sort* param = reinterpret_cast<Sort*>(paramPointer); + DatatypeDecl* retPointer = new DatatypeDecl( + solver->mkDatatypeDecl(cName, *param, (bool)isCoDatatype)); + env->ReleaseStringUTFChars(jName, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkDatatypeDecl + * Signature: (JLjava/lang/String;[JZ)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_mkDatatypeDecl__JLjava_lang_String_2_3JZ(JNIEnv* env, + jobject, + jlong pointer, + jstring jName, + jlongArray jParams, + jboolean isCoDatatype) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jName, nullptr); + std::string cName(s); + std::vector<Sort> params = getObjectsFromPointers<Sort>(env, jParams); + DatatypeDecl* retPointer = new DatatypeDecl( + solver->mkDatatypeDecl(cName, params, (bool)isCoDatatype)); + env->ReleaseStringUTFChars(jName, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: simplify + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_simplify(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* term = reinterpret_cast<Term*>(termPointer); + Term* retPointer = new Term(solver->simplify(*term)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: assertFormula + * Signature: (JJ)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_assertFormula(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* term = reinterpret_cast<Term*>(termPointer); + solver->assertFormula(*term); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver + * Method: checkSat + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSat(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Result* retPointer = new Result(solver->checkSat()); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: checkSatAssuming + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSatAssuming__JJ( + JNIEnv* env, jobject, jlong pointer, jlong assumptionPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* assumption = reinterpret_cast<Term*>(assumptionPointer); + Result* retPointer = new Result(solver->checkSatAssuming(*assumption)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: checkSatAssuming + * Signature: (J[J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSatAssuming__J_3J( + JNIEnv* env, jobject, jlong pointer, jlongArray jAssumptions) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Term> assumptions = + getObjectsFromPointers<Term>(env, jAssumptions); + Result* retPointer = new Result(solver->checkSatAssuming(assumptions)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: checkEntailed + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkEntailed__JJ(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* term = reinterpret_cast<Term*>(termPointer); + Result* retPointer = new Result(solver->checkEntailed(*term)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: checkEntailed + * Signature: (J[J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkEntailed__J_3J(JNIEnv* env, + jobject, + jlong pointer, + jlongArray jTerms) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Term> terms = getObjectsFromPointers<Term>(env, jTerms); + Result* retPointer = new Result(solver->checkEntailed(terms)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: declareDatatype + * Signature: (JLjava/lang/String;[J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_declareDatatype( + JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jlongArray jCtors) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + std::vector<DatatypeConstructorDecl> ctors = + getObjectsFromPointers<DatatypeConstructorDecl>(env, jCtors); + Sort* retPointer = new Sort(solver->declareDatatype(cSymbol, ctors)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: declareFun + * Signature: (JLjava/lang/String;[JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_declareFun(JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jSorts, + jlong sortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, jSorts); + Term* retPointer = new Term(solver->declareFun(cSymbol, sorts, *sort)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: declareSort + * Signature: (JLjava/lang/String;I)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_declareSort( + JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jint arity) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + Sort* retPointer = new Sort(solver->declareSort(cSymbol, (uint32_t)arity)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: defineFun + * Signature: (JLjava/lang/String;[JJJZ)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_defineFun__JLjava_lang_String_2_3JJJZ(JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jVars, + jlong sortPointer, + jlong termPointer, + jboolean global) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* term = reinterpret_cast<Term*>(termPointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars); + Term* retPointer = + new Term(solver->defineFun(cSymbol, vars, *sort, *term, (bool)global)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: defineFun + * Signature: (JJ[JJZ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_defineFun__JJ_3JJZ(JNIEnv* env, + jobject, + jlong pointer, + jlong funPointer, + jlongArray jVars, + jlong termPointer, + jboolean global) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* fun = reinterpret_cast<Term*>(funPointer); + Term* term = reinterpret_cast<Term*>(termPointer); + std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars); + Term* retPointer = + new Term(solver->defineFun(*fun, vars, *term, (bool)global)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: defineFunRec + * Signature: (JLjava/lang/String;[JJJZ)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_defineFunRec__JLjava_lang_String_2_3JJJZ(JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jVars, + jlong sortPointer, + jlong termPointer, + jboolean global) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* term = reinterpret_cast<Term*>(termPointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars); + Term* retPointer = + new Term(solver->defineFunRec(cSymbol, vars, *sort, *term, (bool)global)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: defineFunRec + * Signature: (JJ[JJZ)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_defineFunRec__JJ_3JJZ(JNIEnv* env, + jobject, + jlong pointer, + jlong funPointer, + jlongArray jVars, + jlong termPointer, + jboolean global) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* fun = reinterpret_cast<Term*>(funPointer); + Term* term = reinterpret_cast<Term*>(termPointer); + std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars); + Term* retPointer = + new Term(solver->defineFunRec(*fun, vars, *term, (bool)global)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: defineFunsRec + * Signature: (J[J[[J[JZ)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_defineFunsRec(JNIEnv* env, + jobject, + jlong pointer, + jlongArray jFuns, + jobjectArray jVars, + jlongArray jTerms, + jboolean global) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Term> funs = getObjectsFromPointers<Term>(env, jFuns); + std::vector<Term> terms = getObjectsFromPointers<Term>(env, jTerms); + std::vector<std::vector<Term>> varsMatrix; + jsize rows = env->GetArrayLength(jVars); + for (jint i = 0; i < rows; i++) + { + std::vector<Term> vars; + jlongArray row = (jlongArray)env->GetObjectArrayElement(jVars, i); + jsize columns = env->GetArrayLength(row); + jlong* columnElements = env->GetLongArrayElements(row, nullptr); + for (jint j = 0; j < columns; j++) + { + Term* var = reinterpret_cast<Term*>((jlongArray)columnElements[j]); + vars.push_back(*var); + } + varsMatrix.push_back(vars); + } + solver->defineFunsRec(funs, varsMatrix, terms, (bool)global); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver + * Method: getAssertions + * Signature: (J)[J + */ +JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getAssertions(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Term> assertions = solver->getAssertions(); + jlongArray ret = getPointersFromObjects<Term>(env, assertions); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Solver + * Method: getInfo + * Signature: (JLjava/lang/String;)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Solver_getInfo(JNIEnv* env, + jobject, + jlong pointer, + jstring jFlag) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jFlag, nullptr); + std::string cFlag(s); + env->ReleaseStringUTFChars(jFlag, s); + return env->NewStringUTF(solver->getInfo(cFlag).c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getOption + * Signature: (JLjava/lang/String;)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Solver_getOption(JNIEnv* env, + jobject, + jlong pointer, + jstring jOption) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jOption, nullptr); + std::string cOption(s); + env->ReleaseStringUTFChars(jOption, s); + return env->NewStringUTF(solver->getOption(cOption).c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getUnsatAssumptions + * Signature: (J)[J + */ +JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getUnsatAssumptions(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Term> core = solver->getUnsatAssumptions(); + jlongArray ret = getPointersFromObjects<Term>(env, core); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Solver + * Method: getUnsatCore + * Signature: (J)[J + */ +JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getUnsatCore(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Term> core = solver->getUnsatCore(); + jlongArray ret = getPointersFromObjects<Term>(env, core); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Solver + * Method: getValue + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getValue__JJ(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* term = reinterpret_cast<Term*>(termPointer); + Term* retPointer = new Term(solver->getValue(*term)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getValue + * Signature: (J[J)[J + */ +JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getValue__J_3J( + JNIEnv* env, jobject, jlong pointer, jlongArray termPointers) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Term> terms = getObjectsFromPointers<Term>(env, termPointers); + std::vector<Term> values = solver->getValue(terms); + jlongArray ret = getPointersFromObjects<Term>(env, values); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: isModelCoreSymbol + * Signature: (JJ)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Solver_isModelCoreSymbol(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* term = reinterpret_cast<Term*>(termPointer); + return static_cast<jboolean>(solver->isModelCoreSymbol(*term)); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false)); +} + +/* + * Class: cvc5_Solver + * Method: getModel + * Signature: (J[J[J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Solver_getModel(JNIEnv* env, + jobject, + jlong pointer, + jlongArray sortPointers, + jlongArray varPointers) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Sort> sorts = getObjectsFromPointers<Sort>(env, sortPointers); + std::vector<Term> vars = getObjectsFromPointers<Term>(env, varPointers); + std::string model = solver->getModel(sorts, vars); + return env->NewStringUTF(model.c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getQuantifierElimination + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getQuantifierElimination( + JNIEnv* env, jobject, jlong pointer, jlong qPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* q = reinterpret_cast<Term*>(qPointer); + Term* retPointer = new Term(solver->getQuantifierElimination(*q)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getQuantifierEliminationDisjunct + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getQuantifierEliminationDisjunct( + JNIEnv* env, jobject, jlong pointer, jlong qPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* q = reinterpret_cast<Term*>(qPointer); + Term* retPointer = new Term(solver->getQuantifierEliminationDisjunct(*q)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: declareSeparationHeap + * Signature: (JJJ)V + */ +JNIEXPORT void JNICALL +Java_cvc5_Solver_declareSeparationHeap(JNIEnv* env, + jobject, + jlong pointer, + jlong locSortPointer, + jlong dataSortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* locSort = reinterpret_cast<Sort*>(locSortPointer); + Sort* dataSort = reinterpret_cast<Sort*>(dataSortPointer); + solver->declareSeparationHeap(*locSort, *dataSort); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver + * Method: getSeparationHeap + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getSeparationHeap(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->getSeparationHeap()); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getSeparationNilTerm + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getSeparationNilTerm(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* retPointer = new Term(solver->getSeparationNilTerm()); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: pop + * Signature: (JI)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_pop(JNIEnv* env, + jobject, + jlong pointer, + jint nscopes) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + solver->pop((uint32_t)nscopes); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver + * Method: getInterpolant + * Signature: (JJJ)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Solver_getInterpolant__JJJ( + JNIEnv* env, jobject, jlong pointer, jlong conjPointer, jlong outputPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* conj = reinterpret_cast<Term*>(conjPointer); + Term* output = reinterpret_cast<Term*>(outputPointer); + return (jboolean)solver->getInterpolant(*conj, *output); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getInterpolant + * Signature: (JJJJ)Z + */ +JNIEXPORT jboolean JNICALL +Java_cvc5_Solver_getInterpolant__JJJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong conjPointer, + jlong grammarPointer, + jlong outputPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* conj = reinterpret_cast<Term*>(conjPointer); + Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer); + Term* output = reinterpret_cast<Term*>(outputPointer); + return (jboolean)solver->getInterpolant(*conj, *grammar, *output); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getAbduct + * Signature: (JJJ)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Solver_getAbduct__JJJ( + JNIEnv* env, jobject, jlong pointer, jlong conjPointer, jlong outputPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* conj = reinterpret_cast<Term*>(conjPointer); + Term* output = reinterpret_cast<Term*>(outputPointer); + return (jboolean)solver->getAbduct(*conj, *output); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getAbduct + * Signature: (JJJJ)Z + */ +JNIEXPORT jboolean JNICALL +Java_cvc5_Solver_getAbduct__JJJJ(JNIEnv* env, + jobject, + jlong pointer, + jlong conjPointer, + jlong grammarPointer, + jlong outputPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* conj = reinterpret_cast<Term*>(conjPointer); + Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer); + Term* output = reinterpret_cast<Term*>(outputPointer); + return (jboolean)solver->getAbduct(*conj, *grammar, *output); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: blockModel + * Signature: (J)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_blockModel(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + solver->blockModel(); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver + * Method: blockModelValues + * Signature: (J[J)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_blockModelValues(JNIEnv* env, + jobject, + jlong pointer, + jlongArray jTerms) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Term> terms = getObjectsFromPointers<Term>(env, jTerms); + solver->blockModelValues(terms); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver + * Method: push + * Signature: (JI)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_push(JNIEnv* env, + jobject, + jlong pointer, + jint nscopes) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + solver->push((uint32_t)nscopes); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver + * Method: resetAssertions + * Signature: (J)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_resetAssertions(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + solver->resetAssertions(); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver + * Method: setInfo + * Signature: (JLjava/lang/String;Ljava/lang/String;)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_setInfo( + JNIEnv* env, jobject, jlong pointer, jstring jKeyword, jstring jValue) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* sKeyword = env->GetStringUTFChars(jKeyword, nullptr); + const char* sValue = env->GetStringUTFChars(jValue, nullptr); + std::string cKeyword(sKeyword); + std::string cValue(sValue); + solver->setInfo(cKeyword, cValue); + env->ReleaseStringUTFChars(jKeyword, sKeyword); + env->ReleaseStringUTFChars(jValue, sValue); + CVC5_JAVA_API_TRY_CATCH_END(env); } /* * Class: cvc5_Solver * Method: setLogic - * Signature: (Ljava/lang/String;)V + * Signature: (JLjava/lang/String;)V */ JNIEXPORT void JNICALL Java_cvc5_Solver_setLogic(JNIEnv* env, - jobject, - jlong solverPointer, - jstring jLogic) + jobject, + jlong pointer, + jstring jLogic) { CVC5_JAVA_API_TRY_CATCH_BEGIN; - Solver* solver = (Solver*)solverPointer; + Solver* solver = reinterpret_cast<Solver*>(pointer); const char* cLogic = env->GetStringUTFChars(jLogic, nullptr); solver->setLogic(std::string(cLogic)); CVC5_JAVA_API_TRY_CATCH_END(env); } + +/* + * Class: cvc5_Solver + * Method: setOption + * Signature: (JLjava/lang/String;Ljava/lang/String;)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_setOption( + JNIEnv* env, jobject, jlong pointer, jstring jOption, jstring jValue) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* sOption = env->GetStringUTFChars(jOption, nullptr); + const char* sValue = env->GetStringUTFChars(jValue, nullptr); + std::string cOption(sOption); + std::string cValue(sValue); + solver->setOption(cOption, cValue); + env->ReleaseStringUTFChars(jOption, sOption); + env->ReleaseStringUTFChars(jValue, sValue); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver + * Method: ensureTermSort + * Signature: (JJJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_ensureTermSort( + JNIEnv* env, jobject, jlong pointer, jlong termPointer, jlong sortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* term = reinterpret_cast<Term*>(termPointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Term* retPointer = new Term(solver->ensureTermSort(*term, *sort)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkSygusVar + * Signature: (JJLjava/lang/String;)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSygusVar( + JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jstring jSymbol) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + Term* retPointer = new Term(solver->mkSygusVar(*sort, cSymbol)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: mkSygusGrammar + * Signature: (J[J[J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSygusGrammar(JNIEnv* env, + jobject, + jlong pointer, + jlongArray jBoundVars, + jlongArray jNtSymbols) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Term> boundVars = getObjectsFromPointers<Term>(env, jBoundVars); + std::vector<Term> ntSymbols = getObjectsFromPointers<Term>(env, jNtSymbols); + Grammar* retPointer = + new Grammar(solver->mkSygusGrammar(boundVars, ntSymbols)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: synthFun + * Signature: (JLjava/lang/String;[JJ)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_synthFun__JLjava_lang_String_2_3JJ(JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jVars, + jlong sortPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + std::vector<Term> boundVars = getObjectsFromPointers<Term>(env, jVars); + Term* retPointer = new Term(solver->synthFun(cSymbol, boundVars, *sort)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: synthFun + * Signature: (JLjava/lang/String;[JJJ)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_synthFun__JLjava_lang_String_2_3JJJ(JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jVars, + jlong sortPointer, + jlong grammarPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Sort* sort = reinterpret_cast<Sort*>(sortPointer); + Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + std::vector<Term> boundVars = getObjectsFromPointers<Term>(env, jVars); + Term* retPointer = + new Term(solver->synthFun(cSymbol, boundVars, *sort, *grammar)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: synthInv + * Signature: (JLjava/lang/String;[J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_synthInv__JLjava_lang_String_2_3J( + JNIEnv* env, jobject, jlong pointer, jstring jSymbol, jlongArray jVars) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars); + Term* retPointer = new Term(solver->synthInv(cSymbol, vars)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: synthInv + * Signature: (JLjava/lang/String;[JJ)J + */ +JNIEXPORT jlong JNICALL +Java_cvc5_Solver_synthInv__JLjava_lang_String_2_3JJ(JNIEnv* env, + jobject, + jlong pointer, + jstring jSymbol, + jlongArray jVars, + jlong grammarPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Grammar* grammar = reinterpret_cast<Grammar*>(grammarPointer); + const char* s = env->GetStringUTFChars(jSymbol, nullptr); + std::string cSymbol(s); + std::vector<Term> vars = getObjectsFromPointers<Term>(env, jVars); + Term* retPointer = new Term(solver->synthInv(cSymbol, vars, *grammar)); + env->ReleaseStringUTFChars(jSymbol, s); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: addSygusConstraint + * Signature: (JJ)V + */ +JNIEXPORT void JNICALL Java_cvc5_Solver_addSygusConstraint(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* term = reinterpret_cast<Term*>(termPointer); + solver->addSygusConstraint(*term); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver + * Method: addSygusInvConstraint + * Signature: (JJJJJ)V + */ +JNIEXPORT void JNICALL +Java_cvc5_Solver_addSygusInvConstraint(JNIEnv* env, + jobject, + jlong pointer, + jlong invPointer, + jlong prePointer, + jlong transPointer, + jlong postPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* inv = reinterpret_cast<Term*>(invPointer); + Term* pre = reinterpret_cast<Term*>(prePointer); + Term* trans = reinterpret_cast<Term*>(transPointer); + Term* post = reinterpret_cast<Term*>(postPointer); + solver->addSygusInvConstraint(*inv, *pre, *trans, *post); + CVC5_JAVA_API_TRY_CATCH_END(env); +} + +/* + * Class: cvc5_Solver + * Method: checkSynth + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_checkSynth(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Result* retPointer = new Result(solver->checkSynth()); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getSynthSolution + * Signature: (JJ)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getSynthSolution(JNIEnv* env, + jobject, + jlong pointer, + jlong termPointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + Term* term = reinterpret_cast<Term*>(termPointer); + Term* retPointer = new Term(solver->getSynthSolution(*term)); + return reinterpret_cast<jlong>(retPointer); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getSynthSolutions + * Signature: (J[J)[J + */ +JNIEXPORT jlongArray JNICALL Java_cvc5_Solver_getSynthSolutions( + JNIEnv* env, jobject, jlong pointer, jlongArray jTerms) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Solver* solver = reinterpret_cast<Solver*>(pointer); + std::vector<Term> terms = getObjectsFromPointers<Term>(env, jTerms); + std::vector<Term> solutions = solver->getSynthSolutions(terms); + jlongArray ret = getPointersFromObjects<Term>(env, solutions); + return ret; + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); +} + +/* + * Class: cvc5_Solver + * Method: getNullTerm + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullTerm(JNIEnv* env, + jobject, + jlong) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* ret = new Term(); + return reinterpret_cast<jlong>(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getNullResult + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullResult(JNIEnv* env, + jobject, + jlong) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Result* ret = new Result(); + return reinterpret_cast<jlong>(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getNullOp + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullOp(JNIEnv* env, jobject, jlong) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Op* ret = new Op(); + return reinterpret_cast<jlong>(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Solver + * Method: getNullDatatypeDecl + * Signature: (J)J + */ +JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullDatatypeDecl(JNIEnv* env, + jobject, + jlong) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + DatatypeDecl* ret = new DatatypeDecl(); + return reinterpret_cast<jlong>(ret); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +}
\ No newline at end of file diff --git a/src/api/java/jni/cvc5_Term.cpp b/src/api/java/jni/cvc5_Term.cpp index 6c4d00ff3..0de1b5673 100644 --- a/src/api/java/jni/cvc5_Term.cpp +++ b/src/api/java/jni/cvc5_Term.cpp @@ -572,6 +572,37 @@ JNIEXPORT jstring JNICALL Java_cvc5_Term_getString(JNIEnv* env, /* * Class: cvc5_Term + * Method: isRealValue + * Signature: (J)Z + */ +JNIEXPORT jboolean JNICALL Java_cvc5_Term_isRealValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast<Term*>(pointer); + return static_cast<jboolean>(current->isRealValue()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false)); +} + +/* + * Class: cvc5_Term + * Method: getRealValue + * Signature: (J)Ljava/lang/String; + */ +JNIEXPORT jstring JNICALL Java_cvc5_Term_getRealValue(JNIEnv* env, + jobject, + jlong pointer) +{ + CVC5_JAVA_API_TRY_CATCH_BEGIN; + Term* current = reinterpret_cast<Term*>(pointer); + std::string realValue = current->getRealValue(); + return env->NewStringUTF(realValue.c_str()); + CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); +} + +/* + * Class: cvc5_Term * Method: iterator * Signature: (J)J */ |