Project

General

Profile

Bug #4813

[solver][constraint] Невозможно создавать тривиальные ограничения

Added by Sergey Smolov almost 6 years ago. Updated over 5 years ago.

Status:
Closed
Priority:
High
Assignee:
Andrei Tatarnikov
Category:
-
Target version:
Start date:
04/02/2014
Due date:
% Done:

100%

Estimated time:
Detected in build:
svn
Platform:
Published in build:
140915

Description

Средствами Fortress нельзя сформировать следующий код на SMT-LIB:

(assert true)
(check-sat)
(exit)

Это происходит потому, что для создания Constraint требуется явно указать задействованные в нем переменные (которых в данном примере нет).

Необходимо поддерживать создание таких тривиальных ограничений.


Files

NoVariableTestCase.java (1.17 KB) NoVariableTestCase.java Sergey Smolov, 07/26/2014 01:41 PM

History

#1

Updated by Sergey Smolov almost 6 years ago

  • Subject changed from Невозможно создавать тривиальные ограничения to [solver][constraint] Невозможно создавать тривиальные ограничения
#2

Updated by Sergey Smolov over 5 years ago

  • Priority changed from Normal to High
#3

Updated by Alexander Kamkin over 5 years ago

Что с этой задачей?

#4

Updated by Andrei Tatarnikov over 5 years ago

  • Status changed from New to Resolved
  • % Done changed from 0 to 100

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

#5

Updated by Sergey Smolov over 5 years ago

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


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-тест

#6

Updated by Sergey Smolov over 5 years ago

  • Status changed from Resolved to Open
#7

Updated by Andrei Tatarnikov over 5 years ago

  • Status changed from Open to Resolved

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

#8

Updated by Sergey Smolov over 5 years ago

  • Status changed from Resolved to Verified

Ок

#9

Updated by Andrei Tatarnikov over 5 years ago

  • Status changed from Verified to Closed
  • Published in build set to 140915

Also available in: Atom PDF