>source

매개 변수화 된 데이터 유형을 정의하려고합니다. option Java API를 사용하여 CVC4에서.

DATATYPE option[T] =
        None
      | Some(elem: T)
 END;

내 문제는 호출하는 방법을 모른다는 것입니다. None 건설자. 다음 코드를 시도했습니다.

class Cvc4Test3 {
    public static void main(String... args) {
        Cvc4Solver.loadLibrary();
        ExprManager em = new ExprManager();
        SmtEngine smt = new SmtEngine(em);
        DatatypeType dt = createOptionDatatype(em);
        // instantiate to int
        DatatypeType dtInt = dt.instantiate(vector(em.integerType()));
        // x is an integer variable
        Expr x = em.mkVar("x", em.integerType());
        // create equation: None::option[INT] = Some(x)
        Expr l = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("None"));
        Expr la = em.mkExpr(Kind.APPLY_TYPE_ASCRIPTION, em.mkConst(new AscriptionType(dtInt)), l);
        Expr r = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("Some"), x);
        Expr eq = em.mkExpr(Kind.EQUAL, la, r);
        // Try to solve equation:
        smt.setOption("produce-models", new SExpr(true));
        smt.assertFormula(eq);
        Result res = smt.checkSat();
        System.out.println("res = " + res);
    }
    /**
     * DATATYPE option[T] =
     * None
     * | Some(elem: T)
     * END;
     */
    private static DatatypeType createOptionDatatype(ExprManager em) {
        Type t = em.mkSort("T");
        vectorType types = vector(t);
        Datatype dt = new Datatype("option", types);
        DatatypeConstructor cNone = new DatatypeConstructor("None");
        dt.addConstructor(cNone);
        DatatypeConstructor cSome = new DatatypeConstructor("Some");
        cSome.addArg("elem", t);
        dt.addConstructor(cSome);
        return em.mkDatatypeType(dt);
    }
    private static vectorType vector(Type... types) {
        vectorType res = new vectorType();
        for (Type t : types) {
            res.add(t);
        }
        return res;
    }
}

다음과 같은 오류가 발생합니다.

Exception in thread "main" java.lang.RuntimeException: matching failed for type ascription argument of parameterized datatype: matching failed for type ascription argument of parameterized datatype
    at edu.nyu.acsys.CVC4.CVC4JNI.SmtEngine_assertFormula__SWIG_1(Native Method)
    at edu.nyu.acsys.CVC4.SmtEngine.assertFormula(SmtEngine.java:149)

타입 ascription 줄을 제거하면 올바른 타입을 유추하지 않으므로 타입 ascription이 필요하다고 가정합니다. 여기에 형식 설명없이 오류가 발생합니다.

Exception in thread "main" java.lang.RuntimeException: Subexpressions must have a common base type:
Equation: None = Some(x)
Type 1: option[T]
Type 2: option[INT]
: Subexpressions must have a common base type:
Equation: None = Some(x)
Type 1: option[T]
Type 2: option[INT]
    at edu.nyu.acsys.CVC4.CVC4JNI.SmtEngine_assertFormula__SWIG_1(Native Method)
    at edu.nyu.acsys.CVC4.SmtEngine.assertFormula(SmtEngine.java:149)

Java API를 사용하여이 데이터 유형과 공식을 올바르게 작성하려면 어떻게해야합니까?


  • 답변 # 1

    CVC4 메일 링리스트의 Andrew Reynolds로부터 답변을 받았습니다 :

    First, notice that we have updated to a new API (https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.h).
    Coincidentally, I just submitted a PR that adds the interface for getting the required constructor you are looking for, in the new API: https://github.com/CVC4/CVC4/pull/4817

    If you are interested in the old API, your code is almost correct, however, there is a subtle difference in what we expect to be cast.

    In particular, in SMT-LIB casts are applied to constructor operators, not terms (you may be interested in this discussion https://github.com/Z3Prover/z3/issues/2135). This means that the AST of a casted nil term in CVC4 is: (APPLY_CONSTRUCTOR (APPLY_TYPE_ASCRIPTION None T)) not (APPLY_TYPE_ASCRIPTION (APPLY_CONSTRUCTOR None) option[Int]) Unfortunately, there is a complication in the old API about what T is. It is not "option[Int]", instead it is "the type of constructors of type option[Int]", or what we call a "constructor type".

    표현식을 작성하기위한 올바른 코드는 다음과 같습니다.

       // create equation: None::option[INT] = Some(x)
        Type noneInt = dtInt.getDatatype().get("None").getSpecializedConstructorType(dtInt);
        Expr la = em.mkExpr(Kind.APPLY_TYPE_ASCRIPTION, em.mkConst(new AscriptionType(noneInt)), dtInt.getConstructor("None"));
        Expr l = em.mkExpr(Kind.APPLY_CONSTRUCTOR, la);
        Expr r = em.mkExpr(Kind.APPLY_CONSTRUCTOR, dtInt.getConstructor("Some"), x);
        Expr eq = em.mkExpr(Kind.EQUAL, l, r);
    
    

    유형 옵션 [INT]과 생성자 유형 옵션 [INT]에는 차이가 있습니다. 형식 설명은 생성자 형식을 사용해야합니다.

    설명은 적용된 생성자가 아니라 생성자에 적용되어야합니다.

  • 이전 reactjs - React Hook useEffect에 종속성이 누락되었습니다
  • 다음 r - cran 패키지 릴리스 피드백 - 쉽게 억제 할 수없는 정보 메시지를 콘솔에 작성