From cfeaf40ed6a9d4d7fec925352e30d2470a1ca567 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 31 Mar 2020 18:12:16 -0700 Subject: Rename checkValid/query to checkEntailed. (#4191) This renames api::Solver::checkValidAssuming to checkEntailed and removes api::Solver::checkValid. Internally, SmtEngine::query is renamed to SmtEngine::checkEntailed, and these changes are further propagated to the Result class. --- examples/api/java/BitVectors.java | 8 ++++---- examples/api/java/Combination.java | 7 +++---- examples/api/java/HelloWorld.java | 2 +- examples/api/java/LinearArith.java | 5 +++-- 4 files changed, 11 insertions(+), 11 deletions(-) (limited to 'examples/api/java') diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java index 17111b63a..bb2245a6f 100644 --- a/examples/api/java/BitVectors.java +++ b/examples/api/java/BitVectors.java @@ -86,8 +86,8 @@ public class BitVectors { Expr new_x_eq_new_x_ = em.mkExpr(Kind.EQUAL, new_x, new_x_); System.out.println(" Querying: " + new_x_eq_new_x_); - System.out.println(" Expect valid. "); - System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_)); + System.out.println(" Expect entailed. "); + System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_)); System.out.println(" Popping context. "); smt.pop(); @@ -102,7 +102,7 @@ public class BitVectors { smt.assertFormula(assignment2); System.out.println(" Querying: " + new_x_eq_new_x_); - System.out.println(" Expect valid. "); - System.out.println(" CVC4: " + smt.query(new_x_eq_new_x_)); + System.out.println(" Expect entailed. "); + System.out.println(" CVC4: " + smt.checkEntailed(new_x_eq_new_x_)); } } diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java index 0c9ca84d6..53b1fa92d 100644 --- a/examples/api/java/Combination.java +++ b/examples/api/java/Combination.java @@ -83,10 +83,9 @@ public class Combination { System.out.println("Given the following assumptions:"); System.out.println(assumptions); - System.out.println("Prove x /= y is valid. " + - "CVC4 says: " + smt.query(em.mkExpr(Kind.DISTINCT, x, y)) + - "."); - + System.out.println("Prove x /= y is entailed. " + + "CVC4 says: " + smt.checkEntailed(em.mkExpr(Kind.DISTINCT, x, y)) + + "."); System.out.println("Now we call checksat on a trivial query to show that"); System.out.println("the assumptions are satisfiable: " + diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java index 393ce40f0..a08f3d452 100644 --- a/examples/api/java/HelloWorld.java +++ b/examples/api/java/HelloWorld.java @@ -30,6 +30,6 @@ public class HelloWorld { Expr helloworld = em.mkVar("Hello World!", em.booleanType()); SmtEngine smt = new SmtEngine(em); - System.out.println(helloworld + " is " + smt.query(helloworld)); + System.out.println(helloworld + " is " + smt.checkEntailed(helloworld)); } } diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java index 2ddf92584..e060263b4 100644 --- a/examples/api/java/LinearArith.java +++ b/examples/api/java/LinearArith.java @@ -61,8 +61,9 @@ public class LinearArith { smt.push(); Expr diff_leq_two_thirds = em.mkExpr(Kind.LEQ, diff, two_thirds); System.out.println("Prove that " + diff_leq_two_thirds + " with CVC4."); - System.out.println("CVC4 should report VALID."); - System.out.println("Result from CVC4 is: " + smt.query(diff_leq_two_thirds)); + System.out.println("CVC4 should report ENTAILED."); + System.out.println( + "Result from CVC4 is: " + smt.checkEntailed(diff_leq_two_thirds)); smt.pop(); System.out.println(); -- cgit v1.2.3