Вызов конструкторов без аргументов пользовательских типов данных с параметрами типа в CVC4

Я пытаюсь определить параметризованный тип данных option в CVC4, используя Java API.

 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)

Когда я удаляю строку описания типа, она не выводит правильный тип, поэтому я предполагаю, что описание типа необходимо. Вот ошибка, которую я получаю без описания типа:

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?


java cvc4
person Peter Zeller    schedule 27.07.2020    source источник
comment
Я не уверен насчет уровня Java, но если бы вы писали это в SMTLib, вам потребовалось бы приписывание. Что-то вроде: (as None (Option Int)). Это то, что пытается закодировать версия Java?   -  person alias    schedule 27.07.2020
comment
Да, это то, что я хочу, чтобы мой код делал. Однако я думаю, что неправильно использовал API.   -  person Peter Zeller    schedule 27.07.2020
comment
Я бы рекомендовал задать вопрос непосредственно на странице вопросов CVC4. Вы получите гораздо более быстрый ответ: github.com/CVC4/CVC4/issues Пожалуйста, опубликуйте что вы найдете в качестве ответа здесь.   -  person alias    schedule 27.07.2020

Ответы (1)


arrow_upward
0
arrow_downward

Получил ответ от Эндрю Рейнольдса в списке рассылки CVC4:

Во-первых, обратите внимание, что мы обновили API до нового (https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.h).
По совпадению, я только что представил PR, который добавляет интерфейс для получения требуемого конструктора, который вы ищете в новом API: https://github.com/CVC4/CVC4/pull/4817

Если вы заинтересованы в старом API, ваш код почти правильный, однако есть небольшая разница в том, что мы ожидаем получить.

В частности, в SMT-LIB приведения применяются к операторам-конструкторам, а не к терминам (вам может быть интересно это обсуждение https://github.com/Z3Prover/z3/issues/2135). Это означает, что AST приведенного термина nil в CVC4 имеет вид: (APPLY_CONSTRUCTOR (APPLY_TYPE_ASCRIPTION None T)) not (APPLY_TYPE_ASCRIPTION (APPLY_CONSTRUCTOR None) option[Int]) К сожалению, в старом API есть сложность в отношении того, что такое T. Это не option[Int], а тип конструкторов типа option[Int], или то, что мы называем типом конструктора.

Вот исправленный код для создания выражения:

    // 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);
  1. Существует разница между типом option[INT] и конструктором типа option[INT]. Приписывание типа должно использовать тип конструктора.
  2. Приписывание должно идти в конструкторе, а не в прикладном конструкторе.
person Community    schedule 01.08.2020