diff options
Diffstat (limited to 'examples/api/java/Sequences.java')
| -rw-r--r-- | examples/api/java/Sequences.java | 73 |
1 files changed, 37 insertions, 36 deletions
diff --git a/examples/api/java/Sequences.java b/examples/api/java/Sequences.java index d1bb0440d..0fd578984 100644 --- a/examples/api/java/Sequences.java +++ b/examples/api/java/Sequences.java @@ -21,48 +21,49 @@ public class Sequences { public static void main(String args[]) throws CVC5ApiException { - Solver slv = new Solver(); - - // Set the logic - slv.setLogic("QF_SLIA"); - // Produce models - slv.setOption("produce-models", "true"); - // The option strings-exp is needed - slv.setOption("strings-exp", "true"); - // Set output language to SMTLIB2 - slv.setOption("output-language", "smt2"); + try (Solver slv = new Solver()) + { + // Set the logic + slv.setLogic("QF_SLIA"); + // Produce models + slv.setOption("produce-models", "true"); + // The option strings-exp is needed + slv.setOption("strings-exp", "true"); + // Set output language to SMTLIB2 + slv.setOption("output-language", "smt2"); - // Sequence sort - Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort()); + // Sequence sort + Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort()); - // Sequence variables - Term x = slv.mkConst(intSeq, "x"); - Term y = slv.mkConst(intSeq, "y"); + // Sequence variables + Term x = slv.mkConst(intSeq, "x"); + Term y = slv.mkConst(intSeq, "y"); - // Empty sequence - Term empty = slv.mkEmptySequence(slv.getIntegerSort()); - // Sequence concatenation: x.y.empty - Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty); - // Sequence length: |x.y.empty| - Term concat_len = slv.mkTerm(SEQ_LENGTH, concat); - // |x.y.empty| > 1 - Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1)); - // Sequence unit: seq(1) - Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1)); - // x = seq(1) - Term formula2 = slv.mkTerm(EQUAL, x, unit); + // Empty sequence + Term empty = slv.mkEmptySequence(slv.getIntegerSort()); + // Sequence concatenation: x.y.empty + Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty); + // Sequence length: |x.y.empty| + Term concat_len = slv.mkTerm(SEQ_LENGTH, concat); + // |x.y.empty| > 1 + Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1)); + // Sequence unit: seq(1) + Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1)); + // x = seq(1) + Term formula2 = slv.mkTerm(EQUAL, x, unit); - // Make a query - Term q = slv.mkTerm(AND, formula1, formula2); + // Make a query + Term q = slv.mkTerm(AND, formula1, formula2); - // check sat - Result result = slv.checkSatAssuming(q); - System.out.println("cvc5 reports: " + q + " is " + result + "."); + // check sat + Result result = slv.checkSatAssuming(q); + System.out.println("cvc5 reports: " + q + " is " + result + "."); - if (result.isSat()) - { - System.out.println(" x = " + slv.getValue(x)); - System.out.println(" y = " + slv.getValue(y)); + if (result.isSat()) + { + System.out.println(" x = " + slv.getValue(x)); + System.out.println(" y = " + slv.getValue(y)); + } } } }
\ No newline at end of file |