*
* 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));
}
}
* 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.*;
* 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.*;
/*
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)
*/
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);
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) + ".");
}
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 + ".");
* 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.*;
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);
* 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.*;
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;
projects / cvc5.git / commitdiff