getFormulaType(T pFormula) {
@Override
public FormulaType getFormulaType(Integer pFormula) {
- return convertType(yices_type_of_term(pFormula));
+ return convertType(Terms.typeOf(pFormula));
}
/** Convert from Yices2 types to JavaSMT FormulaTypes. */
private FormulaType convertType(Integer pType) {
- if (yices_type_is_bool(pType)) {
+ if (Types.isBool(pType)) {
return FormulaType.BooleanType;
- } else if (yices_type_is_int(pType)) {
+ } else if (Types.isInt(pType)) {
return FormulaType.IntegerType;
- } else if (yices_type_is_real(pType)) {
+ } else if (Types.isReal(pType)) {
return FormulaType.RationalType;
- } else if (yices_type_is_bitvector(pType)) {
- return FormulaType.getBitvectorTypeWithSize(yices_bvtype_size(pType));
- } else if (yices_type_is_function(pType)) {
- var domain = yices_type_child(pType, 0);
- var range = yices_type_child(pType, 1);
+ } else if (Types.isBitvector(pType)) {
+ return FormulaType.getBitvectorTypeWithSize(Types.bvSize(pType));
+ } else if (Types.isFunction(pType)) {
+ var domain = Types.child(pType, 0);
+ var range = Types.child(pType, 1);
return FormulaType.getArrayType(convertType(domain), convertType(range));
+ } else {
+ throw new IllegalArgumentException(
+ String.format("Unknown formula type '%s'", Types.toString(pType)));
}
- throw new IllegalArgumentException(
- String.format("Unknown formula type '%s'", yices_type_to_string(pType)));
}
/** Creates a named, free variable. Might retrieve it from the cache if created prior. */
@@ -330,20 +208,22 @@ protected int createNamedVariable(int type, String name) {
!formulaCache.containsRow(name),
"Symbol '%s' already used for a variable of type '%s'",
name,
- formulaCache.row(name));
+ formulaCache.containsRow(name)
+ ? Types.toString(formulaCache.row(name).keySet().iterator().next())
+ : "");
- int var = yices_new_uninterpreted_term(type);
+ int var = Terms.newUninterpretedTerm(type);
// Names in Yices2 behave like a stack. The last variable named is retrieved when asking for
// a term with a specific name. Since we substitute free vars with bound for quantifiers,
// this sometimes mixes them up, hence we track them ourselves.
- yices_set_term_name(var, name);
+ Terms.setName(var, name);
formulaCache.put(name, type, var);
return var;
}
protected int createBoundVariableFromFreeVariable(int unboundVar) {
- int type = yices_type_of_term(unboundVar);
- String name = yices_get_term_name(unboundVar);
+ int type = Terms.typeOf(unboundVar);
+ String name = Terms.getName(unboundVar);
// Search for recently created bound variables and re-use it
// (Names work like a stack in Yices2. If we associate a term with a name, we get that term
@@ -351,17 +231,17 @@ protected int createBoundVariableFromFreeVariable(int unboundVar) {
// them with the same name as the free variable (so that it has the same name). This pushes the
// name stack, and we get the bound var when asking yices_get_term_by_name(). We want to
// re-use the bound variables here, but never the free ones.)
- int termFromName = yices_get_term_by_name(name);
+ int termFromName = Terms.getByName(name);
if (termFromName != -1) {
- int termFromNameType = yices_type_of_term(termFromName);
+ int termFromNameType = Terms.typeOf(termFromName);
checkArgument(
type == termFromNameType,
"Cannot override symbol '%s' with new symbol '%s' of type '%s'",
- yices_type_to_string(termFromNameType),
+ Types.toString(termFromNameType),
name,
- yices_type_to_string(type));
- int constructor = yices_term_constructor(termFromName);
- if (constructor == YICES_VARIABLE) {
+ Types.toString(type));
+ Constructor constructor = Terms.constructor(termFromName);
+ if (constructor == Constructor.VARIABLE) {
// Already a bound var
return termFromName;
}
@@ -369,7 +249,7 @@ protected int createBoundVariableFromFreeVariable(int unboundVar) {
// reset term name binding
// TODO: add yices_remove_term_name();
- int bound = yices_new_variable(type);
+ int bound = Terms.newVariable(type);
// Names in Yices2 behave like a stack. The last variable named is retrieved when asking for
// a term with a specific name. Since we substitute free vars with bound for quantifiers,
// this sometimes mixes them up, hence we track them ourselves.
@@ -377,38 +257,45 @@ protected int createBoundVariableFromFreeVariable(int unboundVar) {
// Meaning that if we remove the new name, the old term gets its name back.
// Since we just want to retrieve the same var for the quantifier we are currently building,
// this is fine.
- yices_set_term_name(bound, name);
+ Terms.setName(bound, name);
return bound;
}
- @SuppressWarnings("deprecation")
+ /**
+ * Returns the name of a variable or uf term.
+ *
+ * Will return an abstract value name if the term has no name. Yices may introduce unnamed
+ * terms while rewriting bv operations
+ */
+ private String lookupName(int term) {
+ return Terms.getName(term) == null ? "@" + term : Terms.getName(term);
+ }
+
@Override
public R visit(FormulaVisitor pVisitor, Formula pFormula, Integer pF) {
- int constructor = yices_term_constructor(pF);
+ Constructor constructor = Terms.constructor(pF);
switch (constructor) {
- case YICES_BOOL_CONST:
- return pVisitor.visitConstant(pFormula, yices_bool_const_value(pF));
- case YICES_ARITH_CONST:
+ case BOOL_CONSTANT:
+ return pVisitor.visitConstant(pFormula, Terms.boolConstValue(pF));
+ case ARITH_CONSTANT:
return pVisitor.visitConstant(pFormula, convertValue(pF, pF));
- case YICES_BV_CONST:
+ case BV_CONSTANT:
return pVisitor.visitConstant(pFormula, convertValue(pF, pF));
- case YICES_LAMBDA_TERM:
+ case LAMBDA_TERM:
// We use lambda terms as array constants
return pVisitor.visitFunction(
pFormula,
- ImmutableList.of(encapsulateWithTypeOf(yices_term_child(pF, 1))),
+ ImmutableList.of(encapsulateWithTypeOf(Terms.child(pF, 1))),
FunctionDeclarationImpl.of(
"const",
FunctionDeclarationKind.CONST,
- ImmutableList.of(getFormulaType(yices_term_child(pF, 1))),
+ ImmutableList.of(getFormulaType(Terms.child(pF, 1))),
getFormulaType(pF),
0));
- case YICES_UNINTERPRETED_TERM:
- return pVisitor.visitFreeVariable(pFormula, yices_get_term_name(pF));
- case YICES_VARIABLE:
- return pVisitor.visitBoundVariable(pFormula, 0);
- case YICES_FORALL_TERM:
+ case FORALL_TERM:
return visitQuantifier(pVisitor, pFormula, pF, Quantifier.FORALL);
+ case UNINTERPRETED_TERM:
+ return pVisitor.visitFreeVariable(pFormula, lookupName(pF));
default:
return visitFunctionApplication(pVisitor, pFormula, pF, constructor);
}
@@ -424,15 +311,14 @@ private R visitQuantifier(
int[] freeVars = new int[boundVars.length];
for (int i = 0; i < boundVars.length; i++) {
// use from cached variable mapping
- freeVars[i] =
- createNamedVariable(yices_type_of_term(boundVars[i]), yices_get_term_name(boundVars[i]));
+ freeVars[i] = createNamedVariable(Terms.typeOf(boundVars[i]), Terms.getName(boundVars[i]));
}
int body = Iterables.getLast(args);
if (pQuantifier == Quantifier.EXISTS) {
- body = yices_not(body); // EXISTS is an alias for NOT(FORALL(x, NOT(body)))
+ body = Terms.not(body); // EXISTS is an alias for NOT(FORALL(x, NOT(body)))
}
- int substBody = yices_subst_term(freeVars.length, boundVars, freeVars, body);
+ int substBody = Terms.subst(body, boundVars, freeVars);
return pVisitor.visitQuantifier(
(BooleanFormula) pFormula,
@@ -444,158 +330,199 @@ private R visitQuantifier(
}
private R visitFunctionApplication(
- FormulaVisitor pVisitor, Formula pFormula, int pF, final int constructor) {
-
- // Map built-in constructors in negative int to avoid collision with UFs.
- int functionDeclaration = -constructor;
-
- assert !CONSTANT_AND_VARIABLE_CONSTRUCTORS.contains(constructor)
- : String.format(
- "Term %s with constructor %d should be handled somewhere else",
- yices_term_to_string(pF), constructor);
-
+ FormulaVisitor pVisitor, Formula pFormula, int pF, final Constructor constructor) {
// filled later, except for some special function applications
String functionName = null;
+ Integer functionDeclaration = null;
List functionArgs = null;
+ List functionIndex = ImmutableList.of();
// filled directly when handling the function application
- final FunctionDeclarationKind functionKind;
+ FunctionDeclarationKind functionKind;
switch (constructor) {
- case YICES_ITE_TERM:
+ case ITE_TERM:
functionKind = FunctionDeclarationKind.ITE;
break;
- case YICES_APP_TERM:
- var fun = yices_term_child(pF, 0);
+ case APP_TERM:
+ var fun = Terms.child(pF, 0);
if (ufSymbols.contains(fun)) {
functionKind = FunctionDeclarationKind.UF;
- functionArgs = getArgs(pF);
- functionName = yices_get_term_name(functionArgs.get(0));
- functionDeclaration = functionArgs.get(0);
- functionArgs.remove(0);
+ var args = getArgs(pF);
+ var f = args.get(0);
+ var x = FluentIterable.from(args).skip(1).toList();
+ functionName = lookupName(f);
+ functionDeclaration = f;
+ functionArgs = x;
} else {
functionKind = FunctionDeclarationKind.SELECT;
functionArgs = getArgs(pF);
functionName = "select";
- functionDeclaration = -YICES_ARRAY_SELECT;
+ var f = Terms.newVariable(Terms.typeOf(functionArgs.get(0)));
+ var x = Terms.newVariable(Terms.typeOf(functionArgs.get(1)));
+ functionDeclaration = Terms.lambda(new int[] {f, x}, Terms.funApplication(f, x));
}
break;
- case YICES_UPDATE_TERM:
+ case UPDATE_TERM:
functionKind = FunctionDeclarationKind.STORE;
- functionArgs =
- ImmutableList.of(
- yices_term_child(pF, 0), yices_term_child(pF, 1), yices_term_child(pF, 2));
- functionDeclaration = -YICES_UPDATE_TERM;
+ functionArgs = getArgs(pF);
+ var f = Terms.newVariable(Terms.typeOf(functionArgs.get(0)));
+ var x = Terms.newVariable(Terms.typeOf(functionArgs.get(1)));
+ var y = Terms.newVariable(Terms.typeOf(functionArgs.get(2)));
+ functionDeclaration = Terms.lambda(new int[] {f, x, y}, Terms.functionUpdate1(f, x, y));
break;
- case YICES_EQ_TERM:
- functionKind = FunctionDeclarationKind.EQ; // Covers all equivalences
+ case EQ_TERM:
+ functionKind = FunctionDeclarationKind.EQ;
break;
- case YICES_DISTINCT_TERM:
+ case DISTINCT_TERM:
functionKind = FunctionDeclarationKind.DISTINCT;
break;
- case YICES_NOT_TERM:
+ case NOT_TERM:
if (isNestedExists(pF)) {
int existsTerm = Iterables.getOnlyElement(getArgs(pF));
return visitQuantifier(pVisitor, pFormula, existsTerm, Quantifier.EXISTS);
} else if (isNestedConjunction(pF)) {
functionKind = FunctionDeclarationKind.AND;
functionArgs = getNestedConjunctionArgs(pF);
- functionDeclaration = -YICES_AND;
} else {
functionKind = FunctionDeclarationKind.NOT;
}
break;
- case YICES_OR_TERM:
+ case OR_TERM:
functionKind = FunctionDeclarationKind.OR;
break;
- case YICES_XOR_TERM:
+ case XOR_TERM:
functionKind = FunctionDeclarationKind.XOR;
break;
- case YICES_BV_DIV:
+ case BV_DIV:
functionKind = FunctionDeclarationKind.BV_UDIV;
break;
- case YICES_BV_REM:
+ case BV_REM:
functionKind = FunctionDeclarationKind.BV_UREM;
break;
- case YICES_BV_SDIV:
+ case BV_SDIV:
functionKind = FunctionDeclarationKind.BV_SDIV;
break;
- case YICES_BV_SREM:
+ case BV_SREM:
functionKind = FunctionDeclarationKind.BV_SREM;
break;
- case YICES_BV_SMOD:
+ case BV_SMOD:
functionKind = FunctionDeclarationKind.BV_SMOD;
break;
- case YICES_BV_SHL:
+ case BV_SHL:
functionKind = FunctionDeclarationKind.BV_SHL;
break;
- case YICES_BV_LSHR:
+ case BV_LSHR:
functionKind = FunctionDeclarationKind.BV_LSHR;
break;
- case YICES_BV_ASHR:
+ case BV_ASHR:
functionKind = FunctionDeclarationKind.BV_ASHR;
break;
- case YICES_BV_GE_ATOM:
+ case BV_GE_ATOM:
functionKind = FunctionDeclarationKind.BV_UGE;
break;
- case YICES_BV_SGE_ATOM:
+ case BV_SGE_ATOM:
functionKind = FunctionDeclarationKind.BV_SGE;
break;
- case YICES_ARITH_GE_ATOM:
+ case ARITH_GE_ATOM:
functionKind = FunctionDeclarationKind.GTE;
break;
- case YICES_FLOOR:
+ case FLOOR:
functionKind = FunctionDeclarationKind.FLOOR;
break;
- case YICES_RDIV:
+ case RDIV:
functionKind = FunctionDeclarationKind.DIV;
break;
- case YICES_IDIV:
+ case IDIV:
functionKind = FunctionDeclarationKind.DIV;
break;
- case YICES_SELECT_TERM:
+ case IMOD:
+ functionKind = FunctionDeclarationKind.MODULO;
+ break;
+ case SELECT_TERM:
functionKind = FunctionDeclarationKind.SELECT;
break;
- case YICES_BV_SUM:
- if (yices_term_num_children(pF) == 1) {
+ case BV_SUM:
+ if (Terms.numChildren(pF) == 1) {
functionKind = FunctionDeclarationKind.BV_MUL;
- functionArgs = getMultiplyBvSumArgsFromSum(pF);
- functionDeclaration = -YICES_BV_MUL;
+ functionArgs = getOnlySumTerm(pF);
} else {
functionKind = FunctionDeclarationKind.BV_ADD;
- functionArgs = getBvSumArgs(pF);
+ var terms = getSumTerms(pF);
+ var right =
+ terms.size() > 2
+ ? Terms.bvAdd(FluentIterable.from(terms).skip(1).toList())
+ : terms.get(1);
+ functionArgs = ImmutableList.of(terms.get(0), right);
}
break;
- case YICES_ARITH_SUM:
- if (yices_term_num_children(pF) == 1) {
+ case ARITH_SUM:
+ if (Terms.numChildren(pF) == 1) {
functionKind = FunctionDeclarationKind.MUL;
- functionArgs = getMultiplySumArgsFromSum(pF);
- functionDeclaration = -YICES_POWER_PRODUCT;
+ functionArgs = getOnlySumTerm(pF);
} else {
functionKind = FunctionDeclarationKind.ADD;
- functionArgs = getSumArgs(pF);
+ functionArgs = getSumTerms(pF);
}
break;
- case YICES_POWER_PRODUCT:
- if (yices_type_is_bitvector(yices_type_of_term(pF))) {
+ case POWER_PRODUCT:
+ if (Terms.isBitvector(pF)) {
functionKind = FunctionDeclarationKind.BV_MUL;
- functionArgs = getMultiplyArgs(pF, true);
- functionDeclaration = -YICES_BV_MUL;
- // TODO Product of more then 2 bitvectors ?
+ var factors = getProductFactors(pF);
+ var right = factors.get(1);
+ for (var p = 2; p < factors.size(); p++) {
+ right = Terms.bvMul(right, factors.get(p));
+ }
+ functionArgs = ImmutableList.of(factors.get(0), right);
} else {
functionKind = FunctionDeclarationKind.MUL;
- functionArgs = getMultiplyArgs(pF, false);
+ functionArgs = getProductFactors(pF);
}
break;
- case YICES_BIT_TERM:
- functionKind = FunctionDeclarationKind.BV_EXTRACT;
- functionArgs = getBitArgs(pF);
+ case BIT_TERM:
+ // Yices rewrites most "bitwise" operations on bitvectors, f.ex bvand(a,b) becomes
+ // (bool-to-bv (and (bit a k) (bit b k)) (and (bit a k-1) (bit b k-1)) ...)
+ // Here (bit a k) returns the k-th bit of the bitvector as a boolean, and bool-to-bv is
+ // used to (re)construct the bitvector from a vector of boolean terms
+ // Since "bit" and "bool-to-bv" are not supported by the visitor, we have to undo the
+ // transformation here
+
+ // Rewrite (bit x n) to (= (extract x n n) #b1). Yices will then further simplify to
+ // (= (bool-to-bv (bit x n)) #b1)
+ // We visit the outer "=" and handle the rest in the arguments
+ functionKind = FunctionDeclarationKind.EQ;
+ functionArgs =
+ ImmutableList.of(
+ Terms.bvExtract(Terms.projArg(pF), Terms.projIndex(pF), Terms.projIndex(pF)),
+ Terms.bvConst(1, 1));
break;
- case YICES_BV_ARRAY:
- functionKind = FunctionDeclarationKind.BV_CONCAT;
+ case BV_ARRAY:
+ if (Terms.numChildren(pF) == 1) {
+ if (Terms.constructor(Terms.child(pF, 0)) == Constructor.BIT_TERM) {
+ // Rewrite (bool-to-bv (bit x n)) to (extract x n n)
+ functionKind = FunctionDeclarationKind.BV_EXTRACT;
+ functionIndex =
+ ImmutableList.of(
+ Terms.projIndex(Terms.child(pF, 0)), Terms.projIndex(Terms.child(pF, 0)));
+ functionArgs = ImmutableList.of(Terms.projArg(Terms.child(pF, 0)));
+ } else {
+ // Rewrite (bool-to-bv _) to (ite _ #1 #0)
+ functionKind = FunctionDeclarationKind.ITE;
+ functionArgs =
+ ImmutableList.of(Terms.child(pF, 0), Terms.bvConst(1, 1), Terms.bvConst(1, 0));
+ }
+ } else {
+ // Rewrite (bool-to-bv a b ...) to (concat ... (ite b #1 #0) (ite a #1 #0))
+ functionKind = FunctionDeclarationKind.BV_CONCAT;
+ functionArgs =
+ transformedImmutableListCopy(
+ getArgs(pF),
+ p -> Terms.ifThenElse(p, Terms.bvConst(1, 1), Terms.bvConst(1, 0)))
+ .reverse();
+ }
break;
default:
- functionKind = FunctionDeclarationKind.OTHER;
+ throw new UnsupportedOperationException(constructor.toString());
}
if (functionName == null) {
@@ -604,8 +531,12 @@ private R visitFunctionApplication(
if (functionArgs == null) {
functionArgs = getArgs(pF);
}
+ if (functionDeclaration == null) {
+ functionDeclaration = buildDeclaration(functionKind, functionIndex, functionArgs);
+ }
- final ImmutableList> argTypes = ImmutableList.copyOf(toType(functionArgs));
+ final ImmutableList> argTypes =
+ ImmutableList.copyOf(Lists.transform(functionArgs, this::getFormulaType));
Preconditions.checkState(
functionArgs.size() == argTypes.size(),
@@ -627,8 +558,246 @@ private R visitFunctionApplication(
functionName, functionKind, argTypes, getFormulaType(pF), functionDeclaration));
}
- private List> toType(final List args) {
- return Lists.transform(args, this::getFormulaType);
+ private int buildDeclaration(
+ FunctionDeclarationKind pKind, List pIndex, List pArgs) {
+ ImmutableList.Builder builder = ImmutableList.builder();
+ int c = 0;
+ for (var arg : pArgs) {
+ builder.add(Terms.newVariable("var" + c++, Terms.typeOf(arg)));
+ }
+ var args = builder.build();
+ int f;
+ switch (pKind) {
+ case AND:
+ f = Terms.and(args);
+ break;
+ case NOT:
+ checkArgument(args.size() == 1);
+ f = Terms.not(args.get(0));
+ break;
+ case OR:
+ f = Terms.or(args);
+ break;
+ case IFF:
+ checkArgument(args.size() == 2);
+ f = Terms.iff(args.get(0), args.get(1));
+ break;
+ case ITE:
+ checkArgument(args.size() == 3);
+ f = Terms.ifThenElse(args.get(0), args.get(1), args.get(2));
+ break;
+ case XOR:
+ f = Terms.xor(args);
+ break;
+ case IMPLIES:
+ checkArgument(args.size() == 2);
+ f = Terms.implies(args.get(0), args.get(1));
+ break;
+ case DISTINCT:
+ f = Terms.distinct(args);
+ break;
+ case STORE:
+ checkArgument(args.size() == 3);
+ f = Terms.functionUpdate1(args.get(0), args.get(1), args.get(2));
+ break;
+ case SELECT:
+ checkArgument(args.size() == 2);
+ f = Terms.funApplication(args.get(0), args.get(1));
+ break;
+ case CONST:
+ checkArgument(args.size() == 1);
+ f = Terms.lambda(new int[] {}, args.get(0));
+ break;
+ case UMINUS:
+ checkArgument(args.size() == 1);
+ f = Terms.neg(args.get(0));
+ break;
+ case SUB:
+ checkArgument(args.size() == 2);
+ f = Terms.sub(args.get(0), args.get(1));
+ break;
+ case ADD:
+ f = Terms.add(args);
+ break;
+ case DIV:
+ checkArgument(args.size() == 2);
+ f = Terms.div(args.get(0), args.get(1));
+ break;
+ case MUL:
+ f = Terms.mul(args);
+ break;
+ case MODULO:
+ checkArgument(args.size() == 2);
+ f = Terms.imod(args.get(0), args.get(1));
+ break;
+ case UF:
+ case VAR:
+ throw new IllegalArgumentException("Expecting builtin kind");
+ case LT:
+ checkArgument(args.size() == 2);
+ f = Terms.arithLt(args.get(0), args.get(1));
+ break;
+ case LTE:
+ checkArgument(args.size() == 2);
+ f = Terms.arithLeq(args.get(0), args.get(1));
+ break;
+ case GT:
+ checkArgument(args.size() == 2);
+ f = Terms.arithGt(args.get(0), args.get(1));
+ break;
+ case GTE:
+ checkArgument(args.size() == 2);
+ f = Terms.arithGeq(args.get(0), args.get(1));
+ break;
+ case EQ:
+ checkArgument(args.size() == 2);
+ f = Terms.eq(args.get(0), args.get(1));
+ break;
+ case EQ_ZERO:
+ throw new UnsupportedOperationException("EQ_ZERO not supported");
+ case GTE_ZERO:
+ throw new UnsupportedOperationException("GTE_ZERO not supported");
+ case FLOOR:
+ checkArgument(args.size() == 1);
+ f = Terms.floor(args.get(0));
+ break;
+ case TO_REAL:
+ throw new UnsupportedOperationException("TO_REAL not supported");
+ case INT_TO_BV:
+ throw new UnsupportedOperationException("INT_TO_BV not supported");
+ case BV_EXTRACT:
+ checkArgument(args.size() == 1 && pIndex.size() == 2);
+ f = Terms.bvExtract(args.get(0), pIndex.get(0), pIndex.get(1));
+ break;
+ case BV_CONCAT:
+ f = Terms.bvConcat(args);
+ break;
+ case BV_SIGN_EXTENSION:
+ checkArgument(args.size() == 1);
+ f = Terms.bvSignExtend(args.get(0), pIndex.get(0));
+ break;
+ case BV_ZERO_EXTENSION:
+ checkArgument(args.size() == 1);
+ f = Terms.bvZeroExtend(args.get(0), pIndex.get(0));
+ break;
+ case BV_NOT:
+ checkArgument(args.size() == 1);
+ f = Terms.bvNot(args.get(0));
+ break;
+ case BV_NEG:
+ checkArgument(args.size() == 1);
+ f = Terms.bvNeg(args.get(0));
+ break;
+ case BV_OR:
+ f = Terms.bvOr(args);
+ break;
+ case BV_AND:
+ f = Terms.bvAnd(args);
+ break;
+ case BV_XOR:
+ f = Terms.bvXor(args);
+ break;
+ case BV_SUB:
+ checkArgument(args.size() == 2);
+ f = Terms.bvSub(args.get(0), args.get(1));
+ break;
+ case BV_ADD:
+ f = Terms.bvAdd(args);
+ break;
+ case BV_SDIV:
+ checkArgument(args.size() == 2);
+ f = Terms.bvSDiv(args.get(0), args.get(1));
+ break;
+ case BV_UDIV:
+ checkArgument(args.size() == 2);
+ f = Terms.bvDiv(args.get(0), args.get(1));
+ break;
+ case BV_SREM:
+ checkArgument(args.size() == 2);
+ f = Terms.bvSRem(args.get(0), args.get(1));
+ break;
+ case BV_UREM:
+ checkArgument(args.size() == 2);
+ f = Terms.bvRem(args.get(0), args.get(1));
+ break;
+ case BV_SMOD:
+ checkArgument(args.size() == 2);
+ f = Terms.bvSMod(args.get(0), args.get(1));
+ break;
+ case BV_MUL:
+ checkArgument(args.size() == 2);
+ f = Terms.bvMul(args.get(0), args.get(1));
+ break;
+ case BV_ULT:
+ checkArgument(args.size() == 2);
+ f = Terms.bvLt(args.get(0), args.get(1));
+ break;
+ case BV_SLT:
+ checkArgument(args.size() == 2);
+ f = Terms.bvSLt(args.get(0), args.get(1));
+ break;
+ case BV_ULE:
+ checkArgument(args.size() == 2);
+ f = Terms.bvLe(args.get(0), args.get(1));
+ break;
+ case BV_SLE:
+ checkArgument(args.size() == 2);
+ f = Terms.bvSLe(args.get(0), args.get(1));
+ break;
+ case BV_UGT:
+ checkArgument(args.size() == 2);
+ f = Terms.bvGt(args.get(0), args.get(1));
+ break;
+ case BV_SGT:
+ checkArgument(args.size() == 2);
+ f = Terms.bvSGt(args.get(0), args.get(1));
+ break;
+ case BV_UGE:
+ checkArgument(args.size() == 2);
+ f = Terms.bvGe(args.get(0), args.get(1));
+ break;
+ case BV_SGE:
+ checkArgument(args.size() == 2);
+ f = Terms.bvSGe(args.get(0), args.get(1));
+ break;
+ case BV_EQ:
+ checkArgument(args.size() == 2);
+ f = Terms.bvEq(args.get(0), args.get(1));
+ break;
+ case BV_SHL:
+ checkArgument(args.size() == 2);
+ f = Terms.bvShl(args.get(0), args.get(1));
+ break;
+ case BV_LSHR:
+ checkArgument(args.size() == 2);
+ f = Terms.bvLshr(args.get(0), args.get(1));
+ break;
+ case BV_ASHR:
+ checkArgument(args.size() == 2);
+ f = Terms.bvAshr(args.get(0), args.get(1));
+ break;
+ case BV_ROTATE_LEFT:
+ throw new UnsupportedOperationException("BV_ROTATE_LEFT not supported");
+ case BV_ROTATE_RIGHT:
+ throw new UnsupportedOperationException("BV_ROTATE_RIGHT not supported");
+ case BV_ROTATE_LEFT_BY_INT:
+ checkArgument(args.size() == 1);
+ f = Terms.bvRotateLeft(args.get(0), pIndex.get(0));
+ break;
+ case BV_ROTATE_RIGHT_BY_INT:
+ checkArgument(args.size() == 1);
+ f = Terms.bvRotateRight(args.get(0), pIndex.get(0));
+ break;
+ case UBV_TO_INT:
+ throw new UnsupportedOperationException("UBV_TO_INT not supported");
+ case SBV_TO_INT:
+ throw new UnsupportedOperationException("SBV_TO_INT not supported");
+ case OTHER:
+ throw new UnsupportedOperationException("OTHER not supported");
+ default:
+ throw new UnsupportedOperationException();
+ }
+ return Terms.lambda(args, f);
}
/**
@@ -638,14 +807,14 @@ private List> toType(final List args) {
* of Yices.
*/
private static boolean isNestedExists(int outerTerm) {
- return yices_term_constructor(outerTerm) == YICES_NOT_TERM
- && yices_term_constructor(yices_term_child(outerTerm, 0)) == YICES_FORALL_TERM;
+ return Terms.constructor(outerTerm) == Constructor.NOT_TERM
+ && Terms.constructor(Terms.child(outerTerm, 0)) == Constructor.FORALL_TERM;
}
/** Yices transforms AND(x,...) into NOT(OR(NOT(X),NOT(...)). */
private static boolean isNestedConjunction(int outerTerm) {
- return yices_term_constructor(outerTerm) == YICES_NOT_TERM
- && yices_term_constructor(yices_term_child(outerTerm, 0)) == YICES_OR_TERM;
+ return Terms.constructor(outerTerm) == Constructor.NOT_TERM
+ && Terms.constructor(Terms.child(outerTerm, 0)) == Constructor.OR_TERM;
}
/**
@@ -654,248 +823,141 @@ private static boolean isNestedConjunction(int outerTerm) {
* Only call this method for terms that are nested conjunctions!
*/
private static List getNestedConjunctionArgs(int outerTerm) {
- checkArgument(yices_term_constructor(outerTerm) == YICES_NOT_TERM);
- int middleTerm = yices_term_child(outerTerm, 0);
- checkArgument(yices_term_constructor(middleTerm) == YICES_OR_TERM);
+ checkArgument(Terms.constructor(outerTerm) == Constructor.NOT_TERM);
+ int middleTerm = Terms.child(outerTerm, 0);
+ checkArgument(Terms.constructor(middleTerm) == Constructor.OR_TERM);
List result = new ArrayList<>();
for (int child : getArgs(middleTerm)) {
- result.add(yices_not(child));
+ result.add(Terms.not(child));
}
return result;
}
private static List getArgs(int parent) {
- try {
- return getArgs0(parent);
- } catch (IllegalArgumentException e) {
- throw new IllegalArgumentException("problematic term: " + yices_term_to_string(parent), e);
+ ImmutableList.Builder children = ImmutableList.builder();
+ for (int i = 0; i < Terms.numChildren(parent); i++) {
+ children.add(Terms.child(parent, i));
}
+ return children.build();
}
- private static List getArgs0(int parent) {
- List children = new ArrayList<>();
- for (int i = 0; i < yices_term_num_children(parent); i++) {
- children.add(yices_term_child(parent, i));
+ /** 1 for the given theory. */
+ private static int mkOne(int type) {
+ if (Types.isArithmetic(type)) {
+ return Terms.one();
+ } else if (Types.isBitvector(type)) {
+ return Terms.bvOne(Types.bvSize(type));
+ } else {
+ throw new IllegalArgumentException();
}
- return children;
}
- private static List getSumArgs(int parent) {
- List children = new ArrayList<>();
- for (int i = 0; i < yices_term_num_children(parent); i++) {
- String[] child = yices_sum_component(parent, i);
- String coeff = child[0];
- int term = Integer.parseInt(child[1]);
- if (term == -1) { // No term just a number
- children.add(yices_parse_rational(coeff));
+ /** Convert value to constant term. */
+ private static int toConstant(Object value) {
+ if (value instanceof BigRational) {
+ var rational = (BigRational) value;
+ if (rational.isInteger()) {
+ return Terms.intConst(rational.getNumerator());
} else {
- int coeffTerm = yices_parse_rational(coeff);
- children.add(yices_mul(coeffTerm, term));
+ return Terms.rationalConst(rational);
}
- }
- return children;
- }
-
- /** extract all entries of a BV sum like "3*x + 2*y + 1". */
- private static List getBvSumArgs(int parent) {
- List children = new ArrayList<>();
- int bitsize = yices_term_bitsize(parent);
- for (int i = 0; i < yices_term_num_children(parent); i++) {
- int[] component = yices_bvsum_component(parent, i, bitsize);
- assert component.length == bitsize + 1;
- // the components consist of coefficient (as bits) and variable (if missing: -1)
- int coeff = yices_bvconst_from_array(bitsize, Arrays.copyOfRange(component, 0, bitsize));
- int term = component[component.length - 1];
- if (term == -1) { // No term
- children.add(coeff);
- } else {
- children.add(yices_bvmul(coeff, term));
+ } else if (value instanceof boolean[]) {
+ var array = (boolean[]) value;
+ ImmutableList.Builder builder = ImmutableList.builder();
+ for (var bit : array) {
+ builder.add(bit ? 1 : 0);
}
+ return Terms.bvConst(builder.build());
+ } else {
+ throw new IllegalArgumentException();
}
- return children;
- }
-
- /** extract -1 and X from the sum of one element [-1*x]. */
- private static List getMultiplyBvSumArgsFromSum(int parent) {
- checkArgument(yices_term_num_children(parent) == 1);
- int bitsize = yices_term_bitsize(parent);
- int[] component = yices_bvsum_component(parent, 0, bitsize);
- int coeff = yices_bvconst_from_array(bitsize, Arrays.copyOfRange(component, 0, bitsize));
- int term = component[component.length - 1];
- checkArgument(term != -1, "unexpected constant coeff without variable");
- return ImmutableList.of(coeff, term);
}
- /** extract -1 and X from the sum of one element [-1*x]. */
- private static List getMultiplySumArgsFromSum(int parent) {
- checkArgument(yices_term_num_children(parent) == 1);
- String[] child = yices_sum_component(parent, 0);
- int term = Integer.parseInt(child[1]);
- checkArgument(term != -1, "unexpected constant coeff without variable");
- int coeffTerm = yices_parse_rational(child[0]);
- return ImmutableList.of(coeffTerm, term);
+ /** Multiply two arithmetic or bv terms. */
+ private static int mkMultiply(int a, int b) {
+ if (Terms.isArithmetic(a) && Terms.isArithmetic(b)) {
+ return Terms.mul(a, b);
+ } else if (Terms.isBitvector(a) && Terms.isBitvector(b)) {
+ return Terms.bvMul(a, b);
+ } else {
+ throw new IllegalArgumentException();
+ }
}
- private static List getMultiplyArgs(int parent, boolean isBV) {
- // TODO Add exponent?
- List result = new ArrayList<>();
- for (int i = 0; i < yices_term_num_children(parent); i++) {
- int[] component = yices_product_component(parent, i);
- if (isBV) {
- result.add(yices_bvpower(component[0], component[1]));
- } else {
- result.add(yices_power(component[0], component[1])); // add term, ignore exponent
- }
+ /**
+ * Returns a list of terms for a sum.
+ *
+ * Splits a sum a*t1 + b*t2 + ... into a list of terms a*t1,
+ * b*t2, ...
+ */
+ private static List getSumTerms(int parent) {
+ ImmutableList.Builder terms = ImmutableList.builder();
+ for (int i = 0; i < Terms.numChildren(parent); i++) {
+ SumComponent component = Terms.projSum(parent, i);
+ var factor = toConstant(component.getFactor());
+ var term =
+ component.getTerm() == Terms.NULL_TERM
+ ? mkOne(Terms.typeOf(parent))
+ : component.getTerm();
+
+ terms.add(mkMultiply(factor, term));
}
- return result;
+ return terms.build();
}
- /** get "index" and "b" from "(bit index b)". */
- private static List getBitArgs(int parent) {
- return ImmutableList.of(yices_proj_arg(parent), yices_int32(yices_proj_index(parent)));
+ /**
+ * Returns coefficient and term for a sum with only a single term.
+ *
+ * Splits the sum term Σ a*t into a and t
+ */
+ private static List getOnlySumTerm(int parent) {
+ checkArgument(Terms.numChildren(parent) == 1);
+ SumComponent component = Terms.projSum(parent, 0);
+ checkArgument(component.getTerm() != Terms.NULL_TERM);
+ return ImmutableList.of(toConstant(component.getFactor()), component.getTerm());
}
- @Override
- public Integer callFunctionImpl(Integer pDeclaration, List pArgs) {
- if (pDeclaration < 0) { // is constant function application from API
- switch (-pDeclaration) {
- case YICES_ITE_TERM:
- checkArgsLength("YICES_ITE_TERM", pArgs, 3);
- return yices_ite(pArgs.get(0), pArgs.get(1), pArgs.get(2));
- case YICES_EQ_TERM:
- checkArgsLength("YICES_EQ_TERM", pArgs, 2);
- return yices_eq(pArgs.get(0), pArgs.get(1));
- case YICES_DISTINCT_TERM:
- return yices_distinct(pArgs.size(), Ints.toArray(pArgs));
- case YICES_NOT_TERM:
- checkArgsLength("YICES_NOT_TERM", pArgs, 1);
- return yices_not(pArgs.get(0));
- case YICES_OR_TERM:
- return yices_or(pArgs.size(), Ints.toArray(pArgs));
- case YICES_XOR_TERM:
- return yices_xor(pArgs.size(), Ints.toArray(pArgs));
- case YICES_BV_DIV:
- checkArgsLength("YICES_BV_DIV", pArgs, 2);
- return yices_bvdiv(pArgs.get(0), pArgs.get(1));
- case YICES_BV_REM:
- checkArgsLength("YICES_BV_REM", pArgs, 2);
- return yices_bvrem(pArgs.get(0), pArgs.get(1));
- case YICES_BV_SDIV:
- checkArgsLength("YICES_BV_SDIV", pArgs, 2);
- return yices_bvsdiv(pArgs.get(0), pArgs.get(1));
- case YICES_BV_SREM:
- checkArgsLength("YICES_BV_SREM", pArgs, 2);
- return yices_bvsrem(pArgs.get(0), pArgs.get(1));
- case YICES_BV_SMOD:
- checkArgsLength("YICES_BV_SMOD", pArgs, 2);
- return yices_bvsmod(pArgs.get(0), pArgs.get(1));
- case YICES_BV_SHL:
- checkArgsLength("YICES_BV_SHL", pArgs, 2);
- return yices_bvshl(pArgs.get(0), pArgs.get(1));
- case YICES_BV_LSHR:
- checkArgsLength("YICES_BV_LSHR", pArgs, 2);
- return yices_bvlshr(pArgs.get(0), pArgs.get(1));
- case YICES_BV_ASHR:
- checkArgsLength("YICES_BV_ASHR", pArgs, 2);
- return yices_bvashr(pArgs.get(0), pArgs.get(1));
- case YICES_BV_GE_ATOM:
- checkArgsLength("YICES_BV_GE_ATOM", pArgs, 2);
- return yices_bvge_atom(pArgs.get(0), pArgs.get(1));
- case YICES_BV_SGE_ATOM:
- checkArgsLength("YICES_BV_SGE_ATOM", pArgs, 2);
- return yices_bvsge_atom(pArgs.get(0), pArgs.get(1));
- case YICES_ARITH_GE_ATOM:
- checkArgsLength("YICES_ARITH_GE_ATOM", pArgs, 2);
- return yices_arith_geq_atom(pArgs.get(0), pArgs.get(1));
- case YICES_ABS:
- checkArgsLength("YICES_ABS", pArgs, 1);
- return yices_abs(pArgs.get(0));
- case YICES_CEIL:
- checkArgsLength("YICES_CEIL", pArgs, 1);
- return yices_ceil(pArgs.get(0));
- case YICES_FLOOR:
- checkArgsLength("YICES_FLOOR", pArgs, 1);
- return yices_floor(pArgs.get(0));
- case YICES_RDIV:
- checkArgsLength("YICES_RDIV", pArgs, 2);
- return yices_division(pArgs.get(0), pArgs.get(1));
- case YICES_IDIV:
- checkArgsLength("YICES_IDIV", pArgs, 2);
- return yices_idiv(pArgs.get(0), pArgs.get(1));
- case YICES_IMOD:
- checkArgsLength("YICES_IMOD", pArgs, 2);
- return yices_imod(pArgs.get(0), pArgs.get(1));
- case YICES_IS_INT_ATOM:
- checkArgsLength("YICES_IS_INT_ATOM", pArgs, 1);
- return yices_is_int_atom(pArgs.get(0));
- case YICES_DIVIDES_ATOM:
- checkArgsLength("YICES_DIVIDES_ATOM", pArgs, 2);
- return yices_divides_atom(pArgs.get(0), pArgs.get(1));
- case YICES_BV_SUM:
- return yices_bvsum(pArgs.size(), Ints.toArray(pArgs));
- case YICES_ARITH_SUM:
- return yices_sum(pArgs.size(), Ints.toArray(pArgs));
- case YICES_POWER_PRODUCT:
- return yices_product(pArgs.size(), Ints.toArray(pArgs));
- case YICES_BIT_TERM:
- checkArgsLength("YICES_BIT_TERM", pArgs, 2);
- return yices_bitextract(pArgs.get(0), toInt(pArgs.get(1)));
- case YICES_BV_ARRAY:
- return yices_bvarray(pArgs.size(), Ints.toArray(pArgs));
- case YICES_BV_MUL:
- return yices_bvproduct(pArgs.size(), Ints.toArray(pArgs));
- case YICES_AND:
- return yices_and(pArgs.size(), Ints.toArray(pArgs));
- case YICES_ARRAY_SELECT:
- return yices_application(pArgs.get(0), 1, new int[] {pArgs.get(1)});
- case YICES_UPDATE_TERM:
- return yices_update(pArgs.get(0), 1, new int[] {pArgs.get(1)}, pArgs.get(2));
- default:
- // TODO add more cases
- // if something bad happens here,
- // in most cases the solution is a fix in the method visitFunctionApplication
- throw new IllegalArgumentException(
- String.format(
- "Unknown function declaration with constructor %d and arguments %s (%s)",
- -pDeclaration,
- pArgs,
- Lists.transform(pArgs, Yices2NativeApi::yices_term_to_string)));
- }
- } else { // is UF Application
- if (pArgs.isEmpty()) {
- return pDeclaration;
- } else {
- int[] argArray = Ints.toArray(pArgs);
- int app = yices_application(pDeclaration, argArray.length, argArray);
- return app;
+ /**
+ * Returns a list of factors for a product term.
+ *
+ * Splits a product a^m * b^n * ... into a list of individual factors a
+ * * ... * b * ...
+ */
+ private static List getProductFactors(int parent) {
+ ImmutableList.Builder builder = ImmutableList.builder();
+ for (int i = 0; i < Terms.numChildren(parent); i++) {
+ ProductComponent component = Terms.projProduct(parent, i);
+ for (int k = 0; k < component.getPower(); k++) {
+ builder.add(component.getTerm());
}
}
+ return builder.build();
}
- private int toInt(int termId) {
- assert yices_term_is_int(termId);
- return Integer.parseInt(yices_rational_const_value(termId));
- }
-
- private void checkArgsLength(String kind, List pArgs, final int expectedLength) {
- checkArgument(
- pArgs.size() == expectedLength,
- "%s with %s expected arguments was called with unexpected arguments: %s",
- kind,
- expectedLength,
- Collections2.transform(pArgs, Yices2NativeApi::yices_term_to_string));
+ @Override
+ public Integer callFunctionImpl(Integer pDeclaration, List pArgs) {
+ if (Terms.isFunction(pDeclaration)) {
+ checkArgument(
+ Types.numChildren(Terms.typeOf(pDeclaration)) == 1 + pArgs.size(),
+ "Expecting %s arguments, but found %s",
+ Types.numChildren(Terms.typeOf(pDeclaration)) - 1,
+ pArgs.size());
+ return Terms.funApplication(pDeclaration, Ints.toArray(pArgs));
+ } else {
+ checkArgument(pArgs.isEmpty(), "Expecting no arguments, but found %s", pArgs.size());
+ return pDeclaration;
+ }
}
@Override
public Integer declareUFImpl(String pName, Integer pReturnType, List pArgTypes) {
- int size = pArgTypes.size();
int[] argTypeArray = Ints.toArray(pArgTypes);
final int yicesFuncType;
if (pArgTypes.isEmpty()) {
// a nullary function is a plain symbol (variable)
yicesFuncType = pReturnType;
} else {
- yicesFuncType = yices_function_type(size, argTypeArray, pReturnType);
+ yicesFuncType = Types.functionType(argTypeArray, pReturnType);
}
int uf = createNamedVariable(yicesFuncType, pName);
ufSymbols.add(uf);
@@ -904,51 +966,82 @@ public Integer declareUFImpl(String pName, Integer pReturnType, List pA
@Override
protected Integer getBooleanVarDeclarationImpl(Integer pTFormulaInfo) {
- return yices_term_constructor(pTFormulaInfo);
+ return pTFormulaInfo;
}
private Object parseNumeralValue(Integer pF, FormulaType type) {
checkArgument(
- yices_term_constructor(pF) == YICES_ARITH_CONST,
+ Terms.isArithConstant(pF),
"Term: '%s' with type '%s' is not an arithmetic constant",
- yices_term_to_string(pF),
- yices_type_to_string(yices_type_of_term(pF)));
+ Terms.toString(pF),
+ Types.toString(Terms.typeOf(pF)));
- String value = yices_rational_const_value(pF);
if (type.isRationalType()) {
- Rational ratValue = Rational.of(value);
- return ratValue.isIntegral() ? ratValue.getNum() : ratValue;
+ var rational = Terms.arithConstValue(pF);
+ return rational.isInteger()
+ ? rational.getNumerator()
+ : Rational.of(rational.getNumerator(), rational.getDenominator());
} else if (type.isIntegerType()) {
- return new BigInteger(value);
+ return Terms.arithConstValue(pF).getNumerator();
} else {
throw new IllegalArgumentException("Unexpected type: " + type);
}
}
+ /**
+ * Converts an array of booleans into a BigInteger value.
+ *
+ * Assumes "little endian" encoding
+ */
+ static BigInteger bitsToInteger(boolean[] bits) {
+ // FIXME We're treating the bv as unsigned. Should we return a signed value instead?
+ var value = BigInteger.ZERO;
+ for (var p = 0; p < bits.length; p++) {
+ if (bits[p]) {
+ value = value.setBit(p);
+ }
+ }
+ return value;
+ }
+
+ /**
+ * Converts a BigInteger into an array of booleans.
+ *
+ *
Inverse of {@link #bitsToInteger}
+ */
+ static boolean[] integerToBits(int bitsize, BigInteger value) {
+ checkArgument(bitsize >= value.bitLength());
+
+ var bits = new boolean[bitsize];
+ for (int p = 0; p < value.bitLength(); p++) {
+ bits[p] = value.testBit(p);
+ }
+ return bits;
+ }
+
private BigInteger parseBitvector(int pF) {
checkArgument(
- yices_term_constructor(pF) == YICES_BV_CONST,
- "Term: '%s' is not a bitvector constant",
- yices_term_to_string(pF));
+ Terms.isBvConstant(pF), "Term: '%s' is not a bitvector constant", Terms.toString(pF));
+ return bitsToInteger(Terms.bvConstValue(pF));
+ }
- int[] littleEndianBV = yices_bv_const_value(pF, yices_term_bitsize(pF));
- checkArgument(littleEndianBV.length != 0, "BV was empty");
- String bigEndianBV = Joiner.on("").join(Lists.reverse(Ints.asList(littleEndianBV)));
- return new BigInteger(bigEndianBV, 2);
+ public boolean isArrayVariable(int term) {
+ checkArgument(Terms.isFunction(term));
+ checkArgument(Terms.isUninterpreted(term));
+ return !ufSymbols.contains(term);
}
@Override
public Object convertValue(Integer typeKey, Integer pF) {
FormulaType type = getFormulaType(typeKey);
if (type.isBooleanType()) {
- return pF.equals(yices_true());
+ return pF.equals(Terms.mkTrue());
} else if (type.isRationalType() || type.isIntegerType()) {
return parseNumeralValue(pF, type);
} else if (type.isBitvectorType()) {
return parseBitvector(pF);
} else {
- throw new IllegalArgumentException(
- "Unexpected type: " + yices_type_to_string(yices_type_of_term(pF)));
+ throw new IllegalArgumentException("Unexpected type: " + Types.toString(Terms.typeOf(pF)));
}
}
}
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java
index 555b658d01..5c6c88db6c 100644
--- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java
@@ -9,30 +9,21 @@
package org.sosy_lab.java_smt.solvers.yices2;
import static com.google.common.base.CharMatcher.inRange;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_APP_TERM;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvtype_size;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_distinct;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_eq;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_parse_term;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_child;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_constructor;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_to_string;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_true;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_children;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_bitvector;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_num_children;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_of_term;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_to_string;
import com.google.common.base.CharMatcher;
import com.google.common.base.Preconditions;
import com.google.common.base.Strings;
import com.google.common.collect.ImmutableList;
import com.google.common.primitives.Ints;
+import com.sri.yices.Constructor;
+import com.sri.yices.Terms;
+import com.sri.yices.Types;
import java.io.IOException;
import java.util.Locale;
import java.util.Map;
+import org.sosy_lab.java_smt.api.BooleanFormula;
import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaManager;
import org.sosy_lab.java_smt.api.FormulaType;
import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
@@ -75,31 +66,31 @@ static Integer getYicesTerm(Formula pT) {
@Override
protected Integer equalImpl(Integer pArg1, Integer pArgs) {
- return yices_eq(pArg1, pArgs);
+ return Terms.eq(pArg1, pArgs);
}
@Override
protected Integer distinctImpl(Iterable pArgs) {
int[] array = Ints.toArray(ImmutableList.copyOf(pArgs));
if (array.length < 2) {
- return yices_true();
+ return Terms.mkTrue();
} else {
- return yices_distinct(array.length, array);
+ return Terms.distinct(array);
}
}
@Override
protected Integer parseImpl(String pSmtScript) throws IllegalArgumentException {
- // TODO Might expect Yices input language instead of smt-lib2 notation
- return yices_parse_term(pSmtScript);
+ // Yices uses its own input language and can't parse smt-lib2
+ throw new UnsupportedOperationException();
}
/** Helper function to (pretty) print yices2 sorts. */
private String getTypeRepr(int type) {
- if (yices_type_is_bitvector(type)) {
- return "(_ BitVec " + yices_bvtype_size(type) + ")";
+ if (Types.isBitvector(type)) {
+ return "(_ BitVec " + Types.bvSize(type) + ")";
}
- String typeRepr = yices_type_to_string(type);
+ String typeRepr = Types.toString(type);
return typeRepr.substring(0, 1).toUpperCase(Locale.getDefault()) + typeRepr.substring(1);
}
@@ -114,17 +105,17 @@ assert getFormulaCreator().getFormulaType(formula) == FormulaType.BooleanType
for (Map.Entry entry : varsAndUFs.entrySet()) {
final int term = ((Yices2Formula) entry.getValue()).getTerm();
final int type;
- if (yices_term_constructor(term) == YICES_APP_TERM) {
+ if (Terms.constructor(term) == Constructor.APP_TERM) {
// Is an UF. Correct type is carried by first child.
- type = yices_type_of_term(yices_term_child(term, 0));
+ type = Terms.typeOf(Terms.child(term, 0));
} else {
- type = yices_type_of_term(term);
+ type = Terms.typeOf(term);
}
final int[] types;
- if (yices_type_num_children(type) == 0) {
+ if (Types.numChildren(type) == 0) {
types = new int[] {type};
} else {
- types = yices_type_children(type); // adds children types and then return type
+ types = Types.children(type); // adds children types and then return type
}
if (types.length > 0) {
out.append("(declare-fun ");
@@ -142,11 +133,19 @@ assert getFormulaCreator().getFormulaType(formula) == FormulaType.BooleanType
}
}
// TODO fold formula to avoid exp. overhead
- out.append("(assert ").append(yices_term_to_string(formula)).append(")");
+ out.append("(assert ").append(Terms.toString(formula, 100000, 1)).append(")");
return out.toString();
}
+ @Override
+ public BooleanFormula translateFrom(BooleanFormula formula, FormulaManager otherManager) {
+ if (otherManager instanceof Yices2FormulaManager) {
+ return formula;
+ }
+ return super.translateFrom(formula, otherManager);
+ }
+
/**
* Quote symbols if required.
*
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2IntegerFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2IntegerFormulaManager.java
index 956b435996..c63c755711 100644
--- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2IntegerFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2IntegerFormulaManager.java
@@ -8,9 +8,7 @@
package org.sosy_lab.java_smt.solvers.yices2;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_idiv;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_imod;
-
+import com.sri.yices.Terms;
import java.math.BigDecimal;
import java.math.BigInteger;
import org.sosy_lab.java_smt.api.IntegerFormulaManager;
@@ -42,20 +40,12 @@ protected Integer makeNumberImpl(BigDecimal pNumber) {
@Override
public Integer divide(Integer pParam1, Integer pParam2) {
- if (isNumeral(pParam2)) {
- return yices_idiv(pParam1, pParam2);
- } else {
- return super.divide(pParam1, pParam2);
- }
+ return Terms.idiv(pParam1, pParam2);
}
@Override
public Integer modulo(Integer pParam1, Integer pParam2) {
- if (isNumeral(pParam2)) {
- return yices_imod(pParam1, pParam2);
- } else {
- return super.modulo(pParam1, pParam2);
- }
+ return Terms.imod(pParam1, pParam2);
}
@Override
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java
new file mode 100644
index 0000000000..749f3a5ccd
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2InterpolatingProver.java
@@ -0,0 +1,125 @@
+/*
+ * This file is part of JavaSMT,
+ * an API wrapper for a collection of SMT solvers:
+ * https://github.com/sosy-lab/java-smt
+ *
+ * SPDX-FileCopyrightText: 2026 Dirk Beyer
+ *
+ * SPDX-License-Identifier: Apache-2.0
+ */
+
+package org.sosy_lab.java_smt.solvers.yices2;
+
+import static com.google.common.base.Preconditions.checkArgument;
+import static org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy;
+
+import com.google.common.collect.FluentIterable;
+import com.google.common.collect.ImmutableSet;
+import com.google.common.collect.Sets;
+import com.google.common.primitives.Ints;
+import com.sri.yices.InterpolationContext;
+import com.sri.yices.Status;
+import com.sri.yices.Terms;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.List;
+import java.util.Set;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownNotifier;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.BooleanFormulaManager;
+import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment;
+import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
+import org.sosy_lab.java_smt.api.SolverException;
+
+class Yices2InterpolatingProver extends Yices2AbstractProver
+ implements InterpolatingProverEnvironment {
+ Yices2InterpolatingProver(
+ Yices2FormulaCreator creator,
+ Set pOptions,
+ BooleanFormulaManager pBmgr,
+ ShutdownNotifier pShutdownNotifier,
+ String pSolverType) {
+ super(creator, pOptions, pBmgr, pShutdownNotifier, pSolverType);
+ }
+
+ @Override
+ protected @Nullable Integer addConstraintImpl(BooleanFormula constraint)
+ throws InterruptedException {
+ return addConstraint0(constraint);
+ }
+
+ @Override
+ public BooleanFormula getInterpolant(Collection formulasOfA)
+ throws SolverException, InterruptedException {
+ checkGenerateInterpolants();
+ checkArgument(
+ getAssertedConstraintIds().containsAll(formulasOfA),
+ "Interpolation can only be done over previously asserted formulas.");
+
+ var setA = ImmutableSet.copyOf(formulasOfA);
+ var setB = Sets.difference(getAssertedConstraintIds(), setA);
+
+ return creator.encapsulateBoolean(
+ interpolate(
+ transformedImmutableSetCopy(setA, stack.peekLast()::get),
+ transformedImmutableSetCopy(setB, stack.peekLast()::get)));
+ }
+
+ private int interpolate(Collection setA, Collection setB)
+ throws InterruptedException {
+ try (var ctxA = newContext("mcsat");
+ var ctxB = newContext("mcsat")) {
+
+ ctxA.assertFormulas(Ints.toArray(setA));
+ ctxB.assertFormulas(Ints.toArray(setB));
+ var context = new InterpolationContext(ctxA, ctxB);
+
+ // TODO How to abort this?
+ // For now, let's just check before and after the call:
+ shutdownNotifier.shutdownIfNecessary();
+ var status = context.check(DEFAULT_PARAMS, false);
+ shutdownNotifier.shutdownIfNecessary();
+ if (status == Status.UNSAT) {
+ return context.getInterpolant();
+ } else {
+ throw new IllegalArgumentException("Solver state must be unsat");
+ }
+ }
+ }
+
+ @Override
+ public List getSeqInterpolants(List> partitions)
+ throws SolverException, InterruptedException {
+ checkGenerateInterpolants();
+ checkArgument(!partitions.isEmpty(), "at least one partition should be available.");
+ final Set assertedConstraintIds = getAssertedConstraintIds();
+ checkArgument(
+ partitions.stream().allMatch(assertedConstraintIds::containsAll),
+ "interpolation can only be done over previously asserted formulas.");
+
+ final int n = partitions.size();
+ final List itps = new ArrayList<>();
+ var previousItp = Terms.mkTrue();
+ for (int i = 1; i < n; i++) {
+ Collection formulasA =
+ FluentIterable.from(partitions.get(i - 1))
+ .transform(stack.peekLast()::get)
+ .append(new Integer[] {previousItp})
+ .toSet();
+ Collection formulasB =
+ FluentIterable.concat(partitions.subList(i, n)).transform(stack.peekLast()::get).toSet();
+ var itp = interpolate(formulasA, formulasB);
+ itps.add(creator.encapsulateBoolean(itp));
+ previousItp = itp;
+ }
+ return itps;
+ }
+
+ @Override
+ public List getTreeInterpolants(
+ List> partitionedFormulas, int[] startOfSubTree)
+ throws SolverException, InterruptedException {
+ throw new UnsupportedOperationException();
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java
index 4e3f8b4765..585539649f 100644
--- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java
+++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java
@@ -8,48 +8,16 @@
package org.sosy_lab.java_smt.solvers.yices2;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YVAL_ALGEBRAIC;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YVAL_BOOL;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YVAL_BV;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YVAL_FUNCTION;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YVAL_MAPPING;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YVAL_RATIONAL;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_application;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvtype_size;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_def_terms;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_eq;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_false;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_free_model;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_term_name;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_value;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_value_as_term;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_model_to_string;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_parse_bvbin;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_parse_float;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_parse_rational;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_to_string;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_true;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_children;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_arithmetic;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_bitvector;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_bool;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_int;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_of_term;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_to_string;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_val_bitsize;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_val_expand_function;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_val_expand_mapping;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_val_function_arity;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_val_get_bool;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_val_get_bv;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_val_get_mpq;
-
-import com.google.common.base.Joiner;
import com.google.common.base.Preconditions;
-import com.google.common.base.Strings;
+import com.google.common.base.Verify;
+import com.google.common.collect.FluentIterable;
import com.google.common.collect.ImmutableList;
-import com.google.common.collect.Lists;
-import com.google.common.primitives.Ints;
+import com.sri.yices.Model;
+import com.sri.yices.Terms;
+import com.sri.yices.Types;
+import com.sri.yices.VectorValue;
+import com.sri.yices.YVal;
+import com.sri.yices.YicesException;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.List;
@@ -59,11 +27,11 @@
class Yices2Model extends AbstractModel {
- private final long model;
- private final Yices2TheoremProver prover;
+ private final Model model;
+ private final Yices2AbstractProver prover;
private final Yices2FormulaCreator formulaCreator;
- Yices2Model(long model, Yices2TheoremProver prover, Yices2FormulaCreator pCreator) {
+ Yices2Model(Model model, Yices2AbstractProver prover, Yices2FormulaCreator pCreator) {
super(prover, pCreator);
this.model = model;
this.prover = prover;
@@ -73,7 +41,7 @@ class Yices2Model extends AbstractModel {
@Override
public void close() {
if (!isClosed()) {
- yices_free_model(model);
+ model.close();
}
super.close();
}
@@ -83,145 +51,180 @@ public ImmutableList asList() {
Preconditions.checkState(!isClosed());
Preconditions.checkState(!prover.isClosed(), "cannot use model after prover is closed");
ImmutableList.Builder assignments = ImmutableList.builder();
- int[] termsInModel = yices_def_terms(model);
+ int[] termsInModel = model.collectDefinedTerms();
for (int term : termsInModel) {
- int[] yvalTag = yices_get_value(model, term);
- switch (yvalTag[1]) {
- case YVAL_BOOL:
- case YVAL_RATIONAL:
- case YVAL_ALGEBRAIC:
- case YVAL_BV:
+ YVal yval = model.getValue(term);
+ switch (yval.tag) {
+ case BOOL:
+ case RATIONAL:
+ case ALGEBRAIC:
+ case BV:
assignments.add(getSimpleAssignment(term));
continue;
- case YVAL_FUNCTION: // UFs and Arrays
- assignments.addAll(getFunctionAssignment(term, yvalTag));
+ case FUNCTION: // UFs and Arrays
+ if (formulaCreator.isArrayVariable(term)) {
+ assignments.addAll(getArrayAssignment(term, yval));
+ } else {
+ assignments.addAll(getFunctionAssignment(term, yval));
+ }
continue;
default:
- throw new UnsupportedOperationException("YVAL with unexpected tag: " + yvalTag[1]);
+ throw new UnsupportedOperationException("YVAL with unexpected tag: " + yval.tag);
}
}
return assignments.build();
}
- private ImmutableList getFunctionAssignment(int t, int[] yval) {
+ private ImmutableList getFunctionAssignment(int f, YVal value) {
+ int[] types = Types.children(Terms.typeOf(f));
+ VectorValue expandFun = model.expandFunction(value);
+
ImmutableList.Builder assignments = ImmutableList.builder();
- int arity = yices_val_function_arity(model, yval[0], yval[1]);
- int[] types = yices_type_children(yices_type_of_term(t));
- int[] argTerms = new int[arity];
- String name = yices_get_term_name(t);
- int[] expandFun = yices_val_expand_function(model, yval[0], yval[1]);
- for (int i = 2; i < expandFun.length - 1; i += 2) {
- int[] expandMap;
- if (expandFun[i + 1] == YVAL_MAPPING) {
- expandMap = yices_val_expand_mapping(model, expandFun[i], arity, expandFun[i + 1]);
- } else {
- throw new IllegalArgumentException("Unexpected YVAL tag " + yval[1]);
- }
- List