From 64165dab5d5b901989abaf255e40ac9d63fc44d5 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 16 Nov 2021 19:01:13 -0600 Subject: [PATCH] Update SimpleVC.java (#7647) Update SimpleVC.java with try with resource missed in previous PR --- examples/SimpleVC.java | 39 ++++++++++++++++++++------------------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index de00781d6..900d3710b 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -28,31 +28,32 @@ public class SimpleVC { public static void main(String[] args) { - Solver slv = new Solver(); + try (Solver slv = new Solver()) + { + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 - // Prove that for integers x and y: - // x > 0 AND y > 0 => 2x + y >= 3 + Sort integer = slv.getIntegerSort(); - Sort integer = slv.getIntegerSort(); + Term x = slv.mkConst(integer, "x"); + Term y = slv.mkConst(integer, "y"); + Term zero = slv.mkInteger(0); - Term x = slv.mkConst(integer, "x"); - Term y = slv.mkConst(integer, "y"); - Term zero = slv.mkInteger(0); + Term x_positive = slv.mkTerm(Kind.GT, x, zero); + Term y_positive = slv.mkTerm(Kind.GT, y, zero); - Term x_positive = slv.mkTerm(Kind.GT, x, zero); - Term y_positive = slv.mkTerm(Kind.GT, y, zero); + Term two = slv.mkInteger(2); + Term twox = slv.mkTerm(Kind.MULT, two, x); + Term twox_plus_y = slv.mkTerm(Kind.PLUS, twox, y); - Term two = slv.mkInteger(2); - Term twox = slv.mkTerm(Kind.MULT, two, x); - Term twox_plus_y = slv.mkTerm(Kind.PLUS, twox, y); + Term three = slv.mkInteger(3); + Term twox_plus_y_geq_3 = slv.mkTerm(Kind.GEQ, twox_plus_y, three); - Term three = slv.mkInteger(3); - Term twox_plus_y_geq_3 = slv.mkTerm(Kind.GEQ, twox_plus_y, three); + Term formula = slv.mkTerm(Kind.AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3); - Term formula = slv.mkTerm(Kind.AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3); - - System.out.println("Checking entailment of formula " + formula + " with cvc5."); - System.out.println("cvc5 should report ENTAILED."); - System.out.println("Result from cvc5 is: " + slv.checkEntailed(formula)); + System.out.println("Checking entailment of formula " + formula + " with cvc5."); + System.out.println("cvc5 should report ENTAILED."); + System.out.println("Result from cvc5 is: " + slv.checkEntailed(formula)); + } } } -- 2.30.2