test/java/Combination.java

   1 /*********************                                                        */
   2 /*! \file Combination.java
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Pat Hawks
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 import static org.junit.Assert.assertEquals;
  19
  20 import edu.stanford.CVC4.*;
  21 import org.junit.Before;
  22 import org.junit.Test;
  23
  24 public class Combination {
  25   static {
  26     System.loadLibrary("cvc4jni");
  27   }
  28   ExprManager em;
  29   SmtEngine smt;
  30
  31   @Before
  32   public void initialize() {
  33     em = new ExprManager();
  34     smt = new SmtEngine(em);
  35   }
  36
  37   @Test
  38   public void evaluatesExpression() {
  39     smt.setOption("tlimit", new SExpr(100));
  40     smt.setOption("produce-models", new SExpr(true)); // Produce Models
  41     smt.setOption("output-language", new SExpr("cvc4")); // output-language
  42     smt.setOption("dag-thresh", new SExpr(0)); //Disable dagifying the output
  43     smt.setLogic("QF_UFLIRA");
  44
  45     // Sorts
  46     SortType u = em.mkSort("u");
  47     Type integer = em.integerType();
  48     Type booleanType = em.booleanType();
  49     Type uToInt = em.mkFunctionType(u, integer);
  50     Type intPred = em.mkFunctionType(integer, booleanType);
  51
  52     // Variables
  53     Expr x = em.mkVar("x", u);
  54     Expr y = em.mkVar("y", u);
  55
  56     // Functions
  57     Expr f = em.mkVar("f", uToInt);
  58     Expr p = em.mkVar("p", intPred);
  59
  60     // Constants
  61     Expr zero = em.mkConst(new Rational(0));
  62     Expr one = em.mkConst(new Rational(1));
  63
  64     // Terms
  65     Expr f_x = em.mkExpr(Kind.APPLY_UF, f, x);
  66     Expr f_y = em.mkExpr(Kind.APPLY_UF, f, y);
  67     Expr sum = em.mkExpr(Kind.PLUS, f_x, f_y);
  68     Expr p_0 = em.mkExpr(Kind.APPLY_UF, p, zero);
  69     Expr p_f_y = em.mkExpr(Kind.APPLY_UF, p, f_y);
  70
  71     // Construct the assumptions
  72     Expr assumptions =
  73       em.mkExpr(Kind.AND,
  74                 em.mkExpr(Kind.LEQ, zero, f_x), // 0 <= f(x)
  75                 em.mkExpr(Kind.LEQ, zero, f_y), // 0 <= f(y)
  76                 em.mkExpr(Kind.LEQ, sum, one),  // f(x) + f(y) <= 1
  77                 p_0.notExpr(),                  // not p(0)
  78                 p_f_y);                         // p(f(y))
  79     smt.assertFormula(assumptions);
  80
  81     assertEquals(Result.Entailment.ENTAILED,
  82         smt.checkEntailed(em.mkExpr(Kind.DISTINCT, x, y)).isEntailed());
  83
  84     assertEquals(
  85         Result.Sat.SAT,
  86         smt.checkSat(em.mkConst(true)).isSat()
  87     );
  88   }
  89 }