From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Wed, 30 Mar 2022 03:15:58 +0000 (-0500)
Subject: Fix some documentation warnings  (#8453)
X-Git-Tag: cvc5-1.0.0~130
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=69643856df08ec52eb4567eef582aa779ac8cbfc;p=cvc5.git

Fix some documentation warnings  (#8453)
---

diff --git a/.clang-format b/.clang-format
index fc35b4e00..b240da02a 100644
--- a/.clang-format
+++ b/.clang-format
@@ -24,8 +24,10 @@ AllowShortCaseLabelsOnASingleLine: true
 BinPackArguments: false
 BinPackParameters: false
 BreakBeforeBinaryOperators: NonAssignment
+BreakAfterJavaFieldAnnotations: false
 BraceWrapping:
   AfterCaseLabel: true
+  AfterObjCDeclaration: true
   AfterClass: true
   AfterControlStatement: true
   AfterEnum: true
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 622af563b..cf55b0589 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3932,7 +3932,6 @@ class CVC5_EXPORT Solver
    * @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
    */
   void defineFunsRec(const std::vector<Term>& funs,
                      const std::vector<std::vector<Term>>& bound_vars,
diff --git a/src/api/java/io/github/cvc5/api/Datatype.java b/src/api/java/io/github/cvc5/api/Datatype.java
index f4b73e1f4..6fdaaac37 100644
--- a/src/api/java/io/github/cvc5/api/Datatype.java
+++ b/src/api/java/io/github/cvc5/api/Datatype.java
@@ -116,7 +116,8 @@ public class Datatype extends AbstractPointer implements Iterable<DatatypeConstr
    * @return the parameters of this datatype, if it is parametric. An exception
    * is thrown if this datatype is not parametric.
    */
-  public Sort[] getParameters() {
+  public Sort[] getParameters()
+  {
     long[] sortPointers = getParameters(pointer);
     Sort[] sorts = Utils.getSorts(solver, sortPointers);
     return sorts;
diff --git a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
index da30b3d4a..bd8b7d163 100644
--- a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
+++ b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
@@ -80,14 +80,13 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
    * @param retSort the desired return sort of the constructor
    * @return the constructor term
    */
-  public Term getInstantiatedConstructorTerm(Sort retSort) {
-    long termPointer =
-        getInstantiatedConstructorTerm(pointer, retSort.getPointer());
+  public Term getInstantiatedConstructorTerm(Sort retSort)
+  {
+    long termPointer = getInstantiatedConstructorTerm(pointer, retSort.getPointer());
     return new Term(solver, termPointer);
   }
 
-  private native long getInstantiatedConstructorTerm(
-      long pointer, long retSortPointer);
+  private native long getInstantiatedConstructorTerm(long pointer, long retSortPointer);
 
   /**
    * Get the tester operator of this datatype constructor.
diff --git a/src/api/java/io/github/cvc5/api/IPointer.java b/src/api/java/io/github/cvc5/api/IPointer.java
index 383ef51f6..233548db8 100644
--- a/src/api/java/io/github/cvc5/api/IPointer.java
+++ b/src/api/java/io/github/cvc5/api/IPointer.java
@@ -15,7 +15,6 @@
 
 package io.github.cvc5.api;
 
-interface IPointer
-{
+interface IPointer {
   long getPointer();
 }
diff --git a/src/api/java/io/github/cvc5/api/OptionInfo.java b/src/api/java/io/github/cvc5/api/OptionInfo.java
index 1c47eeedb..9ee43774c 100644
--- a/src/api/java/io/github/cvc5/api/OptionInfo.java
+++ b/src/api/java/io/github/cvc5/api/OptionInfo.java
@@ -206,4 +206,4 @@ public class OptionInfo extends AbstractPointer
   }
 
   private native double doubleValue(long pointer);
-};
+}
diff --git a/src/api/java/io/github/cvc5/api/Pair.java b/src/api/java/io/github/cvc5/api/Pair.java
index 6ebd8c2b2..307273e5e 100644
--- a/src/api/java/io/github/cvc5/api/Pair.java
+++ b/src/api/java/io/github/cvc5/api/Pair.java
@@ -32,8 +32,6 @@ public class Pair<K, V>
     if (pair == null || getClass() != pair.getClass())
       return false;
 
-    Pair<K, V> p = (Pair<K, V>) pair;
-
-    return first.equals(p.first) && second.equals(p.second);
+    return first.equals(((Pair<?, ?>) pair).first) && second.equals(((Pair<?, ?>) pair).second);
   }
 }
diff --git a/src/api/java/io/github/cvc5/api/Result.java b/src/api/java/io/github/cvc5/api/Result.java
index 7af2013fd..856986136 100644
--- a/src/api/java/io/github/cvc5/api/Result.java
+++ b/src/api/java/io/github/cvc5/api/Result.java
@@ -117,7 +117,8 @@ public class Result extends AbstractPointer
    * @return true if query was a checkSat() or checkSatAssuming() query and
    * cvc5 was not able to determine (un)satisfiability.
    */
-  public boolean isUnknown() {
+  public boolean isUnknown()
+  {
     return isUnknown(pointer);
   }
 
diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 4b4c2ccc8..b959cd0da 100644
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -1790,7 +1790,8 @@ public class Solver implements IPointer, AutoCloseable
    *
    * @return the list of learned literals
    */
-  public Term[] getLearnedLiterals() {
+  public Term[] getLearnedLiterals()
+  {
     long[] retPointers = getLearnedLiterals(pointer);
     return Utils.getTerms(this, retPointers);
   }
@@ -2702,7 +2703,8 @@ public class Solver implements IPointer, AutoCloseable
    *         getSynthSolutions, "no solution" if it was determined there is no
    *         solution, or "unknown" otherwise.
    */
-  public SynthResult checkSynth() {
+  public SynthResult checkSynth()
+  {
     long resultPointer = checkSynth(pointer);
     return new SynthResult(this, resultPointer);
   }
@@ -2723,7 +2725,8 @@ public class Solver implements IPointer, AutoCloseable
    *         getSynthSolutions, "no solution" if it was determined there is no
    *         solution, or "unknown" otherwise.
    */
-  public SynthResult checkSynthNext() {
+  public SynthResult checkSynthNext()
+  {
     long resultPointer = checkSynthNext(pointer);
     return new SynthResult(this, resultPointer);
   }
diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java
index 0cd275070..a81993302 100644
--- a/src/api/java/io/github/cvc5/api/Sort.java
+++ b/src/api/java/io/github/cvc5/api/Sort.java
@@ -368,7 +368,7 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
    *
    * An instantiated sort is a sort that has been constructed from
    * instantiating a sort with sort arguments
-   * (see Sort.instantiate()).
+   * (see {@link Sort#instantiate(Sort[])}).
    *
    * @return true if this is an instantiated sort
    */
@@ -428,7 +428,7 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
   /**
    * Get the sorts used to instantiate the sort parameters of a parametric
    * sort (parametric datatype or uninterpreted sort constructor sort,
-   * see Sort.instantiate()).
+   * see {@link Sort#instantiate(Sort[])}).
    *
    * @return the sorts used to instantiate the sort parameters of a
    *         parametric sort
diff --git a/src/api/java/io/github/cvc5/api/Statistics.java b/src/api/java/io/github/cvc5/api/Statistics.java
index df7a82c58..cf8a2c704 100644
--- a/src/api/java/io/github/cvc5/api/Statistics.java
+++ b/src/api/java/io/github/cvc5/api/Statistics.java
@@ -15,10 +15,10 @@
 
 package io.github.cvc5.api;
 
+import java.util.AbstractMap;
 import java.util.Iterator;
-import java.util.NoSuchElementException;
 import java.util.Map;
-import java.util.AbstractMap;
+import java.util.NoSuchElementException;
 
 public class Statistics extends AbstractPointer implements Iterable<Map.Entry<String, Stat>>
 {
@@ -102,18 +102,13 @@ public class Statistics extends AbstractPointer implements Iterable<Map.Entry<St
         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 AbstractMap.SimpleImmutableEntry(pair.first, stat);
+        return new AbstractMap.SimpleImmutableEntry<>(pair.first, stat);
       }
       catch (CVC5ApiException e)
       {
         throw new NoSuchElementException(e.getMessage());
       }
     }
-
-    @Override public void finalize()
-    {
-      deleteIteratorPointer(iteratorPointer);
-    }
   }
 
   public ConstIterator iterator(boolean internal, boolean defaulted)
@@ -124,4 +119,4 @@ public class Statistics extends AbstractPointer implements Iterable<Map.Entry<St
   {
     return new ConstIterator();
   }
-};
+}
diff --git a/src/api/java/io/github/cvc5/api/SynthResult.java b/src/api/java/io/github/cvc5/api/SynthResult.java
index fac196abf..d0b21b604 100644
--- a/src/api/java/io/github/cvc5/api/SynthResult.java
+++ b/src/api/java/io/github/cvc5/api/SynthResult.java
@@ -15,9 +15,6 @@
 
 package io.github.cvc5.api;
 
-import java.util.HashMap;
-import java.util.Map;
-
 public class SynthResult extends AbstractPointer
 {
   // region construction and destruction
diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java
index 02fb42cf4..c8a1b9ddf 100644
--- a/src/api/java/io/github/cvc5/api/Term.java
+++ b/src/api/java/io/github/cvc5/api/Term.java
@@ -630,7 +630,7 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
   public Triplet<Long, Long, Term> getFloatingPointValue()
   {
     Triplet<Long, Long, Long> triplet = getFloatingPointValue(pointer);
-    return new Triplet(triplet.first, triplet.second, new Term(solver, triplet.third));
+    return new Triplet<>(triplet.first, triplet.second, new Term(solver, triplet.third));
   }
 
   private native Triplet<Long, Long, Long> getFloatingPointValue(long pointer);
@@ -692,7 +692,7 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
 
   private native boolean isCardinalityConstraint(long pointer);
 
- /**
+  /**
    * Asserts isCardinalityConstraint().
    * @return the sort the cardinality constraint is for and its upper bound.
    */
diff --git a/src/api/java/io/github/cvc5/api/Triplet.java b/src/api/java/io/github/cvc5/api/Triplet.java
index b9cd36d2f..1b98ac416 100644
--- a/src/api/java/io/github/cvc5/api/Triplet.java
+++ b/src/api/java/io/github/cvc5/api/Triplet.java
@@ -34,8 +34,8 @@ public class Triplet<A, B, C>
     if (object == null || getClass() != object.getClass())
       return false;
 
-    Triplet<A, B, C> triplet = (Triplet<A, B, C>) object;
-    return this.first.equals(triplet.first) && this.second.equals(triplet.second)
-        && this.third.equals(triplet.third);
+    return this.first.equals(((Triplet<?, ?, ?>) object).first)
+        && this.second.equals(((Triplet<?, ?, ?>) object).second)
+        && this.third.equals(((Triplet<?, ?, ?>) object).third);
   }
 }
diff --git a/src/api/java/io/github/cvc5/api/Utils.java b/src/api/java/io/github/cvc5/api/Utils.java
index 6254d43ba..5c814a7f5 100644
--- a/src/api/java/io/github/cvc5/api/Utils.java
+++ b/src/api/java/io/github/cvc5/api/Utils.java
@@ -15,7 +15,6 @@
 
 package io.github.cvc5.api;
 
-import java.io.IOException;
 import java.math.BigInteger;
 import java.util.ArrayList;
 import java.util.List;
@@ -131,6 +130,7 @@ public class Utils
     }
   }
 
+  @SuppressWarnings("unchecked")
   public static <K> Pair<K, Long>[] getPairs(Pair<K, ? extends AbstractPointer>[] abstractPointers)
   {
     Pair<K, Long>[] pointers = new Pair[abstractPointers.length];
diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java
index 8e05cb164..aeea03d56 100644
--- a/test/unit/api/java/DatatypeTest.java
+++ b/test/unit/api/java/DatatypeTest.java
@@ -541,12 +541,10 @@ class DatatypeTest
 
     AtomicReference<Term> atomicTerm = new AtomicReference<>();
     // get the specialized constructor term for list[Int]
-    assertDoesNotThrow(
-        () -> atomicTerm.set(nilc.getInstantiatedConstructorTerm(listInt)));
+    assertDoesNotThrow(() -> atomicTerm.set(nilc.getInstantiatedConstructorTerm(listInt)));
     Term testConsTerm = atomicTerm.get();
     assertNotEquals(testConsTerm, nilc.getConstructorTerm());
     // error to get the specialized constructor term for Int
-    assertThrows(CVC5ApiException.class,
-        () -> nilc.getInstantiatedConstructorTerm(isort));
+    assertThrows(CVC5ApiException.class, () -> nilc.getInstantiatedConstructorTerm(isort));
   }
 }
diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java
index 9f93c54b0..4cca6e711 100644
--- a/test/unit/api/java/OpTest.java
+++ b/test/unit/api/java/OpTest.java
@@ -173,8 +173,7 @@ class OpTest
     Op tupleProject = d_solver.mkOp(TUPLE_PROJECT, indices);
     for (int i = 0, size = tupleProject.getNumIndices(); i < size; i++)
     {
-      assertEquals(
-          indices[i], tupleProject.get(i).getIntegerValue().intValue());
+      assertEquals(indices[i], tupleProject.get(i).getIntegerValue().intValue());
     }
   }
 
diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java
index f21d5e8f0..ffe1ee412 100644
--- a/test/unit/api/java/ResultTest.java
+++ b/test/unit/api/java/ResultTest.java
@@ -83,8 +83,8 @@ class ResultTest
     assertFalse(res.isUnknown());
   }
 
-  @Test
-  void isUnknown() throws CVC5ApiException {
+  @Test void isUnknown() throws CVC5ApiException
+  {
     d_solver.setLogic("QF_NIA");
     d_solver.setOption("incremental", "false");
     d_solver.setOption("solve-int-as-bv", "32");
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index e678d3d50..58fe0d9e7 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1350,7 +1350,7 @@ class SolverTest
     Sort bsort = d_solver.getBooleanSort();
     Term truen = d_solver.mkBoolean(true);
     Term start = d_solver.mkVar(bsort);
-    Term output2  = d_solver.getNullTerm();
+    Term output2 = d_solver.getNullTerm();
     Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
     Term conj2 = d_solver.mkTerm(GT, x, zero);
     assertDoesNotThrow(() -> g.addRule(start, truen));
@@ -1372,7 +1372,7 @@ class SolverTest
     d_solver.assertFormula(d_solver.mkTerm(GT, x, zero));
     // Conjecture for abduction: y > 0
     Term conj = d_solver.mkTerm(GT, y, zero);
-    Term output  = d_solver.getNullTerm();
+    Term output = d_solver.getNullTerm();
     // Fails due to option not set
     assertThrows(CVC5ApiException.class, () -> d_solver.getAbduct(conj));
   }
@@ -1399,7 +1399,6 @@ class SolverTest
     assertNotEquals(output, output2);
   }
 
-
   @Test void getInterpolant() throws CVC5ApiException
   {
     d_solver.setLogic("QF_LIA");
@@ -1519,14 +1518,14 @@ class SolverTest
       assertions.add(() -> assertEquals("print-success", info.getName()));
       assertions.add(
           () -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases())));
-      assertions.add(
-          () -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ValueInfo.class));
-      OptionInfo.ValueInfo<Boolean> valInfo =
-          (OptionInfo.ValueInfo<Boolean>) info.getBaseInfo();
+      assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ValueInfo.class));
+      OptionInfo.ValueInfo<Boolean> valInfo = (OptionInfo.ValueInfo<Boolean>) info.getBaseInfo();
       assertions.add(() -> assertEquals(false, valInfo.getDefaultValue().booleanValue()));
       assertions.add(() -> assertEquals(false, valInfo.getCurrentValue().booleanValue()));
       assertions.add(() -> assertEquals(info.booleanValue(), false));
-      assertions.add(() -> assertEquals(info.toString(), "OptionInfo{ print-success | bool | false | default false }"));
+      assertions.add(()
+                         -> assertEquals(info.toString(),
+                             "OptionInfo{ print-success | bool | false | default false }"));
     }
     {
       // int64 type with default
@@ -1543,14 +1542,14 @@ class SolverTest
       assertions.add(
           () -> assertTrue(numInfo.getMinimum() == null && numInfo.getMaximum() == null));
       assertions.add(() -> assertEquals(info.intValue().intValue(), 0));
-      assertions.add(() -> assertEquals(info.toString(), "OptionInfo{ verbosity | int64_t | 0 | default 0 }"));
+      assertions.add(
+          () -> assertEquals(info.toString(), "OptionInfo{ verbosity | int64_t | 0 | default 0 }"));
     }
     assertAll(assertions);
     {
       OptionInfo info = d_solver.getOptionInfo("rlimit");
       assertEquals(info.getName(), "rlimit");
-      assertEquals(
-          Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
+      assertEquals(Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
       assertTrue(info.getBaseInfo().getClass() == OptionInfo.NumberInfo.class);
       OptionInfo.NumberInfo<BigInteger> ni = (OptionInfo.NumberInfo<BigInteger>) info.getBaseInfo();
       assertEquals(ni.getCurrentValue().intValue(), 0);
@@ -1572,13 +1571,13 @@ class SolverTest
       assertEquals(ni.getMinimum(), 0.0);
       assertEquals(ni.getMaximum(), 1.0);
       assertEquals(info.doubleValue(), 0.0);
-      assertEquals(info.toString(), "OptionInfo{ random-freq, random-frequency | double | 0 | default 0 | 0 <= x <= 1 }");
+      assertEquals(info.toString(),
+          "OptionInfo{ random-freq, random-frequency | double | 0 | default 0 | 0 <= x <= 1 }");
     }
     {
       OptionInfo info = d_solver.getOptionInfo("force-logic");
       assertEquals(info.getName(), "force-logic");
-      assertEquals(
-          Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
+      assertEquals(Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
       assertTrue(info.getBaseInfo().getClass() == OptionInfo.ValueInfo.class);
       OptionInfo.ValueInfo<String> ni = (OptionInfo.ValueInfo<String>) info.getBaseInfo();
       assertEquals(ni.getCurrentValue(), "");
@@ -1591,8 +1590,9 @@ class SolverTest
       OptionInfo info = d_solver.getOptionInfo("simplification");
       assertions.clear();
       assertions.add(() -> assertEquals("simplification", info.getName()));
-      assertions.add(
-          () -> assertEquals(Arrays.asList(new String[] {"simplification-mode"}), Arrays.asList(info.getAliases())));
+      assertions.add(()
+                         -> assertEquals(Arrays.asList(new String[] {"simplification-mode"}),
+                             Arrays.asList(info.getAliases())));
       assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ModeInfo.class));
       OptionInfo.ModeInfo modeInfo = (OptionInfo.ModeInfo) info.getBaseInfo();
       assertions.add(() -> assertEquals("batch", modeInfo.getDefaultValue()));
@@ -1600,7 +1600,8 @@ class SolverTest
       assertions.add(() -> assertEquals(2, modeInfo.getModes().length));
       assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("batch")));
       assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("none")));
-      assertEquals(info.toString(), "OptionInfo{ simplification, simplification-mode | mode | batch | default batch | modes: batch, none }");
+      assertEquals(info.toString(),
+          "OptionInfo{ simplification, simplification-mode | mode | batch | default batch | modes: batch, none }");
     }
     assertAll(assertions);
   }
@@ -1630,7 +1631,10 @@ class SolverTest
       assertTrue(s.isInt());
       assertTrue(s.getInt() >= 0);
     }
-    for (Map.Entry<String, Stat> s : stats) {}
+    for (Map.Entry<String, Stat> s : stats)
+    {
+      assertFalse(s.getKey().isEmpty());
+    }
     for (Statistics.ConstIterator it = stats.iterator(true, true); it.hasNext();)
     {
       Map.Entry<String, Stat> elem = it.next();
@@ -1774,8 +1778,8 @@ class SolverTest
     }
   }
 
-  @Test
-  void getLearnedLiterals() {
+  @Test void getLearnedLiterals()
+  {
     d_solver.setOption("produce-learned-literals", "true");
     // cannot ask before a check sat
     assertThrows(CVC5ApiException.class, () -> d_solver.getLearnedLiterals());
@@ -1783,8 +1787,8 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.getLearnedLiterals());
   }
 
-  @Test
-  void getLearnedLiterals2() {
+  @Test void getLearnedLiterals2()
+  {
     d_solver.setOption("produce-learned-literals", "true");
     Sort intSort = d_solver.getIntegerSort();
     Term x = d_solver.mkConst(intSort, "x");
@@ -1792,8 +1796,7 @@ class SolverTest
     Term zero = d_solver.mkInteger(0);
     Term ten = d_solver.mkInteger(10);
     Term f0 = d_solver.mkTerm(GEQ, x, ten);
-    Term f1 = d_solver.mkTerm(
-        OR, d_solver.mkTerm(GEQ, zero, x), d_solver.mkTerm(GEQ, y, zero));
+    Term f1 = d_solver.mkTerm(OR, d_solver.mkTerm(GEQ, zero, x), d_solver.mkTerm(GEQ, y, zero));
     d_solver.assertFormula(f0);
     d_solver.assertFormula(f1);
     d_solver.checkSat();
@@ -2469,7 +2472,8 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.declareSygusVar(funSort, ""));
 
     assertThrows(CVC5ApiException.class, () -> d_solver.declareSygusVar(d_solver.getNullSort()));
-    assertThrows(CVC5ApiException.class, () -> d_solver.declareSygusVar(d_solver.getNullSort(), "a"));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.declareSygusVar(d_solver.getNullSort(), "a"));
 
     Solver slv = new Solver();
     slv.setOption("sygus", "true");