From 1a79f9534c086a90911233b1127d3269b27a7c4e Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Tue, 16 Nov 2021 12:13:19 -0600 Subject: [PATCH] Fix compile errors with java examples (#7646) Fix compile errors with java examples --- examples/SimpleVC.java | 51 +++++++++---------- examples/api/java/Exceptions.java | 4 +- examples/api/java/Relations.java | 81 +++++++++++++++---------------- examples/api/java/Sets.java | 28 +++++------ examples/api/java/Statistics.java | 44 ++++++++--------- examples/api/java/UnsatCores.java | 2 +- examples/simple_vc_cxx.cpp | 6 +-- 7 files changed, 104 insertions(+), 112 deletions(-) diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index 0ae1b4a51..de00781d6 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -14,48 +14,45 @@ * * To run the resulting class file, you need to do something like the * following: - * + * javac "-cp" "../build/src/api/java/cvc5.jar" SimpleVC.java * java \ - * -cp path/to/CVC4.jar:SimpleVC.jar \ - * -Djava.library.path=/dir/containing/libcvc4jni.so \ + * "-Djava.library.path=../build/src/api/java" "-cp" "../build/src/api/java/cvc5.jar:." \ * SimpleVC - * */ -import edu.stanford.CVC4.*; +import static io.github.cvc5.api.Kind.*; -public class SimpleVC { - public static void main(String[] args) { - System.loadLibrary("cvc4jni"); +import io.github.cvc5.api.*; - ExprManager em = new ExprManager(); - SmtEngine smt = new SmtEngine(em); +public class SimpleVC +{ + public static void main(String[] args) + { + Solver slv = new Solver(); // Prove that for integers x and y: // x > 0 AND y > 0 => 2x + y >= 3 - Type integer = em.integerType(); + Sort integer = slv.getIntegerSort(); - Expr x = em.mkVar("x", integer); - Expr y = em.mkVar("y", integer); - Expr zero = em.mkConst(new Rational(0)); + Term x = slv.mkConst(integer, "x"); + Term y = slv.mkConst(integer, "y"); + Term zero = slv.mkInteger(0); - Expr x_positive = em.mkExpr(Kind.GT, x, zero); - Expr y_positive = em.mkExpr(Kind.GT, y, zero); + Term x_positive = slv.mkTerm(Kind.GT, x, zero); + Term y_positive = slv.mkTerm(Kind.GT, y, zero); - Expr two = em.mkConst(new Rational(2)); - Expr twox = em.mkExpr(Kind.MULT, two, x); - Expr twox_plus_y = em.mkExpr(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); - Expr three = em.mkConst(new Rational(3)); - Expr twox_plus_y_geq_3 = em.mkExpr(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); - Expr formula = - em.mkExpr(Kind.AND, x_positive, y_positive).impExpr(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 CVC4."); - System.out.println("CVC4 should report ENTAILED."); - System.out.println("Result from CVC4 is: " + smt.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)); } } diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java index bc142571d..0ac1f628c 100644 --- a/examples/api/java/Exceptions.java +++ b/examples/api/java/Exceptions.java @@ -10,9 +10,9 @@ * directory for licensing information. * **************************************************************************** * - * Catching CVC4 exceptions via the Java API. + * Catching cvc5 exceptions via the Java API. * - * A simple demonstration of catching CVC4 execptions via the Java API. + * A simple demonstration of catching cvc5 execptions via the Java API. */ import io.github.cvc5.api.*; diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java index fb082fc11..a3e2b2a7e 100644 --- a/examples/api/java/Relations.java +++ b/examples/api/java/Relations.java @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * A simple demonstration of reasoning about relations with CVC4 via Java API. + * A simple demonstration of reasoning about relations with cvc5 via Java API. */ import static io.github.cvc5.api.Kind.*; @@ -20,47 +20,42 @@ import io.github.cvc5.api.*; /* This file uses the API to make a sat call equivalent to the following benchmark: (set-logic ALL) + (set-option :finite-model-find true) (set-option :produce-models true) (set-option :sets-ext true) -(set-option :output-language "smt2") + (declare-sort Person 0) + (declare-fun people () (Set (Tuple Person))) (declare-fun males () (Set (Tuple Person))) -(declare-fun females() (Set (Tuple Person))) +(declare-fun females () (Set (Tuple Person))) (declare-fun father () (Set (Tuple Person Person))) (declare-fun mother () (Set (Tuple Person Person))) (declare-fun parent () (Set (Tuple Person Person))) (declare-fun ancestor () (Set (Tuple Person Person))) (declare-fun descendant () (Set (Tuple Person Person))) -(assert (= people (as univset (Set (Tuple Person))))) -(assert (not (= males (as emptyset (Set (Tuple Person)))))) -(assert (not (= females (as emptyset (Set (Tuple Person)))))) -(assert (= (intersection males females) (as emptyset (Set (Tuple Person))))) - +(assert (= people (as set.universe (Set (Tuple Person))))) +(assert (not (= males (as set.empty (Set (Tuple Person)))))) +(assert (not (= females (as set.empty (Set (Tuple Person)))))) +(assert (= (set.inter males females) (as set.empty (Set (Tuple Person))))) ; father relation is not empty -(assert (not (= father (as emptyset (Set (Tuple Person Person)))))) +(assert (not (= father (as set.empty (Set (Tuple Person Person)))))) ; mother relation is not empty -(assert (not (= mother (as emptyset (Set (Tuple Person Person)))))) - +(assert (not (= mother (as set.empty (Set (Tuple Person Person)))))) ; fathers are males -(assert (subset (join father people) males)) +(assert (set.subset (rel.join father people) males)) ; mothers are females -(assert (subset (join mother people) females)) - +(assert (set.subset (rel.join mother people) females)) ; parent -(assert (= parent (union father mother))) - +(assert (= parent (set.union father mother))) ; no self ancestor -(assert (forall ((x Person)) (not (member (mkTuple x x) ancestor)))) - +(assert (forall ((x Person)) (not (set.member (tuple x x) ancestor)))) ; descendant -(assert (= descendant (tclosure parent))) - +(assert (= descendant (rel.tclosure parent))) ; ancestor -(assert (= ancestor (transpose descendant))) - +(assert (= ancestor (rel.transpose descendant))) (check-sat) (get-model) */ @@ -115,53 +110,53 @@ public class Relations Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm); Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm); - // (assert (= people (as univset (Set (Tuple Person))))) + // (assert (= people (as set.universe (Set (Tuple Person))))) Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet); - // (assert (not (= males (as emptyset (Set (Tuple Person)))))) + // (assert (not (= males (as set.empty (Set (Tuple Person)))))) Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1); - // (assert (not (= females (as emptyset (Set (Tuple Person)))))) + // (assert (not (= females (as set.empty (Set (Tuple Person)))))) Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2); - // (assert (= (intersection males females) (as emptyset (Set (Tuple + // (assert (= (set.inter males females) (as set.empty (Set (Tuple // Person))))) - Term malesFemalesIntersection = solver.mkTerm(INTERSECTION, males, females); + Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females); Term malesAndFemalesAreDisjoint = solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm); - // (assert (not (= father (as emptyset (Set (Tuple Person Person)))))) - // (assert (not (= mother (as emptyset (Set (Tuple Person Person)))))) + // (assert (not (= father (as set.empty (Set (Tuple Person Person)))))) + // (assert (not (= mother (as set.empty (Set (Tuple Person Person)))))) Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm); Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm); Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3); Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4); // fathers are males - // (assert (subset (join father people) males)) - Term fathers = solver.mkTerm(JOIN, father, people); - Term fathersAreMales = solver.mkTerm(SUBSET, fathers, males); + // (assert (set.subset (rel.join father people) males)) + Term fathers = solver.mkTerm(RELATION_JOIN, father, people); + Term fathersAreMales = solver.mkTerm(SET_SUBSET, fathers, males); // mothers are females - // (assert (subset (join mother people) females)) - Term mothers = solver.mkTerm(JOIN, mother, people); - Term mothersAreFemales = solver.mkTerm(SUBSET, mothers, females); + // (assert (set.subset (rel.join mother people) females)) + Term mothers = solver.mkTerm(RELATION_JOIN, mother, people); + Term mothersAreFemales = solver.mkTerm(SET_SUBSET, mothers, females); - // (assert (= parent (union father mother))) - Term unionFatherMother = solver.mkTerm(UNION, father, mother); + // (assert (= parent (set.union father mother))) + Term unionFatherMother = solver.mkTerm(SET_UNION, father, mother); Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother); - // (assert (= parent (union father mother))) - Term transitiveClosure = solver.mkTerm(TCLOSURE, parent); + // (assert (= descendant (rel.tclosure parent))) + Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, parent); Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure); - // (assert (= parent (union father mother))) - Term transpose = solver.mkTerm(TRANSPOSE, descendant); + // (assert (= ancestor (rel.transpose descendant))) + Term transpose = solver.mkTerm(RELATION_TRANSPOSE, descendant); Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose); - // (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor)))) + // (assert (forall ((x Person)) (not (set.member (mkTuple x x) ancestor)))) Term x = solver.mkVar(personSort, "x"); DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0); Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), x, x); - Term member = solver.mkTerm(MEMBER, xxTuple, ancestor); + Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor); Term notMember = solver.mkTerm(NOT, member); Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, x); diff --git a/examples/api/java/Sets.java b/examples/api/java/Sets.java index 3edc49ae6..7eaa3a256 100644 --- a/examples/api/java/Sets.java +++ b/examples/api/java/Sets.java @@ -41,24 +41,24 @@ public class Sets Term B = slv.mkConst(set, "B"); Term C = slv.mkConst(set, "C"); - Term unionAB = slv.mkTerm(UNION, A, B); - Term lhs = slv.mkTerm(INTERSECTION, unionAB, C); + Term unionAB = slv.mkTerm(SET_UNION, A, B); + Term lhs = slv.mkTerm(SET_INTER, unionAB, C); - Term intersectionAC = slv.mkTerm(INTERSECTION, A, C); - Term intersectionBC = slv.mkTerm(INTERSECTION, B, C); - Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC); + Term intersectionAC = slv.mkTerm(SET_INTER, A, C); + Term intersectionBC = slv.mkTerm(SET_INTER, B, C); + Term rhs = slv.mkTerm(SET_UNION, intersectionAC, intersectionBC); Term theorem = slv.mkTerm(EQUAL, lhs, rhs); System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); } - // Verify emptset is a subset of any set + // Verify set.empty is a subset of any set { Term A = slv.mkConst(set, "A"); Term emptyset = slv.mkEmptySet(set); - Term theorem = slv.mkTerm(SUBSET, emptyset, A); + Term theorem = slv.mkTerm(SET_SUBSET, emptyset, A); System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + "."); } @@ -69,16 +69,16 @@ public class Sets Term two = slv.mkInteger(2); Term three = slv.mkInteger(3); - Term singleton_one = slv.mkTerm(SINGLETON, one); - Term singleton_two = slv.mkTerm(SINGLETON, two); - Term singleton_three = slv.mkTerm(SINGLETON, three); - Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two); - Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three); - Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three); + Term singleton_one = slv.mkTerm(SET_SINGLETON, one); + Term singleton_two = slv.mkTerm(SET_SINGLETON, two); + Term singleton_three = slv.mkTerm(SET_SINGLETON, three); + Term one_two = slv.mkTerm(SET_UNION, singleton_one, singleton_two); + Term two_three = slv.mkTerm(SET_UNION, singleton_two, singleton_three); + Term intersection = slv.mkTerm(SET_INTER, one_two, two_three); Term x = slv.mkConst(integer, "x"); - Term e = slv.mkTerm(MEMBER, x, intersection); + Term e = slv.mkTerm(SET_MEMBER, x, intersection); Result result = slv.checkSatAssuming(e); System.out.println("cvc5 reports: " + e + " is " + result + "."); diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java index 7db7cc4f3..635be65f6 100644 --- a/examples/api/java/Statistics.java +++ b/examples/api/java/Statistics.java @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * An example of accessing CVC4's statistics using the Java API. + * An example of accessing cvc5's statistics using the Java API. */ import static io.github.cvc5.api.Kind.*; @@ -158,52 +158,52 @@ public class Statistics Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm); Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm); - // (assert (= people (as univset (Set (Tuple Person))))) + // (assert (= people (as set.universe (Set (Tuple Person))))) Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet); - // (assert (not (= males (as emptyset (Set (Tuple Person)))))) + // (assert (not (= males (as set.empty (Set (Tuple Person)))))) Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1); - // (assert (not (= females (as emptyset (Set (Tuple Person)))))) + // (assert (not (= females (as set.empty (Set (Tuple Person)))))) Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2); - // (assert (= (intersection males females) (as emptyset (Set (Tuple + // (assert (= (set.inter males females) (as set.empty (Set (Tuple // Person))))) - Term malesFemalesIntersection = solver.mkTerm(INTERSECTION, males, females); + Term malesFemalesIntersection = solver.mkTerm(SET_INTER, males, females); Term malesAndFemalesAreDisjoint = solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm); - // (assert (not (= father (as emptyset (Set (Tuple Person Person)))))) - // (assert (not (= mother (as emptyset (Set (Tuple Person Person)))))) + // (assert (not (= father (as set.empty (Set (Tuple Person Person)))))) + // (assert (not (= mother (as set.empty (Set (Tuple Person Person)))))) Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm); Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm); Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3); Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4); // fathers are males - // (assert (subset (join father people) males)) - Term fathers = solver.mkTerm(JOIN, father, people); - Term fathersAreMales = solver.mkTerm(SUBSET, fathers, males); + // (assert (set.subset (rel.join father people) males)) + Term fathers = solver.mkTerm(RELATION_JOIN, father, people); + Term fathersAreMales = solver.mkTerm(SET_SUBSET, fathers, males); // mothers are females - // (assert (subset (join mother people) females)) - Term mothers = solver.mkTerm(JOIN, mother, people); - Term mothersAreFemales = solver.mkTerm(SUBSET, mothers, females); + // (assert (set.subset (rel.join mother people) females)) + Term mothers = solver.mkTerm(RELATION_JOIN, mother, people); + Term mothersAreFemales = solver.mkTerm(SET_SUBSET, mothers, females); - // (assert (= parent (union father mother))) - Term unionFatherMother = solver.mkTerm(UNION, father, mother); + // (assert (= parent (set.union father mother))) + Term unionFatherMother = solver.mkTerm(SET_UNION, father, mother); Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother); - // (assert (= parent (union father mother))) - Term transitiveClosure = solver.mkTerm(TCLOSURE, parent); + // (assert (= descendant (rel.tclosure parent))) + Term transitiveClosure = solver.mkTerm(RELATION_TCLOSURE, parent); Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure); - // (assert (= parent (union father mother))) - Term transpose = solver.mkTerm(TRANSPOSE, descendant); + // (assert (= ancestor (rel.transpose descendant))) + Term transpose = solver.mkTerm(RELATION_TRANSPOSE, descendant); Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose); - // (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor)))) + // (assert (forall ((x Person)) (not (set.member (mkTuple x x) ancestor)))) Term var = solver.mkVar(personSort, "x"); DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0); Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), var, var); - Term member = solver.mkTerm(MEMBER, xxTuple, ancestor); + Term member = solver.mkTerm(SET_MEMBER, xxTuple, ancestor); Term notMember = solver.mkTerm(NOT, member); Term quantifiedVariables = solver.mkTerm(VARIABLE_LIST, var); diff --git a/examples/api/java/UnsatCores.java b/examples/api/java/UnsatCores.java index feec35dbd..b91a94ab7 100644 --- a/examples/api/java/UnsatCores.java +++ b/examples/api/java/UnsatCores.java @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * An example of interacting with unsat cores using CVC4's Java API. + * An example of interacting with unsat cores using cvc5's Java API. */ import io.github.cvc5.api.*; diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index 026665561..1c0663a00 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -47,10 +47,10 @@ int main() { Term formula = slv.mkTerm(Kind::AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3); - std::cout << "Checking entailment of formula " << formula << " with CVC4." + std::cout << "Checking entailment of formula " << formula << " with cvc5." << std::endl; - std::cout << "CVC4 should report ENTAILED." << std::endl; - std::cout << "Result from CVC4 is: " << slv.checkEntailed(formula) + std::cout << "cvc5 should report ENTAILED." << std::endl; + std::cout << "Result from cvc5 is: " << slv.checkEntailed(formula) << std::endl; return 0; -- 2.30.2