Fortress

Исправлено в r525. Теперь Constraint разрешается создавать с пустым списком переменных.

Для проверки написал следующий тест:


public class NoVariableTestCase extends GenericSolverSampleTestBase {
@Override public ISampleConstraint createSample() { return new NoVariable(); }
public static class NoVariable implements ISampleConstraint {
@Override public Constraint getConstraint() {
final ConstraintBuilder builder = new ConstraintBuilder();
builder.setName("NoVariable");
builder.setKind(ConstraintKind.FORMULA_BASED);
builder.setDescription("NoVariable constraint");
Formulas formulas = new Formulas();
formulas.add(NodeValue.newBoolean(true));
builder.setInnerRep(formulas);
return builder.build();
}
@Override
public Iterable<Variable> getExpectedVariables() { return null; }
}
}


В результат библиотека сгенерировала следующий код на SMT-LIB:

(assert true)
(check-sat)
(get-value ())
(get-model)
(exit)

Строка с вызовом get-value все портит - приводит к ошибке

"ERROR: invalid get-value command, empty list of terms"

В приложении - jUnit-тест

Исправлено в r528. Модульный тест добавлен в репозиторий.

Ок