¿Puede la función mkOr(Expr … t) en la API de Z3 para Java recibir una lista como entrada?
Desafortunadamente, no puedo publicar el código completo aquí, porque estoy programando (modelando) en un DSL que se basa en Java. Sin embargo, la pregunta no requiere necesariamente eso:
Estoy tratando de crear una expresión OR más larga, como: p == 1 Or p == 2 Or p == 3, etc.
Tengo una lista de BoolExpr, que contiene la lista de esas expresiones EQ (es decir, p == 1, etc).
En python, ahora podría simplemente darle esta lista de expresiones al método mkOr de la API y eso era todo. Sin embargo, mi fragmento de código a continuación se queja de que list
list<BoolExpr> eqExprList = new ArrayList<BoolExpr>;
// poblamos esta lista con p == 1, p == 2, etc.
MyContext.mkOr(eqExrList); // esto produce el error
Entonces, la pregunta básicamente es si debería funcionar normalmente (en un Java real) de esta manera o si estoy entendiendo mal la documentación de la API: https://z3prover.github.io/api/html/classcom11microsoft11z311_context.html#aea714fc46f4c625ecc15397522099330
davy.ai
Según la documentación de la API, parece que el método mkOr() requiere un arreglo de objetos BoolExpr como entrada. Sin embargo, en el fragmento de código proporcionado, la variable eqExprList está declarada como una lista de BoolExpr, que no es un subtipo de arreglo de BoolExpr. Por lo tanto, se produce el error “la lista no es un subtipo de BoolExpr” al pasar la lista al método mkOr().
Para resolver este problema, la lista debe convertirse en un arreglo de BoolExpr antes de pasarla al método mkOr(). Esto se puede hacer utilizando el método toArray() de la clase ArrayList:
Esto permitirá que el código cree la expresión Or deseada.