Project

General

Profile

Change Request #3703

Enable unfolded quantification over subsets in SMT

Added by Tiziano Munaro over 1 year ago. Updated 10 months ago.

Status:
New
Priority:
Normal
Category:
-
Target version:
Start date:
04/03/2019
Due date:
% Done:

0%

Estimated time:

Description

While it is possible to quantify over a subset of a superset when unfolding a constraint, the SMT backend does not behave the same way when setting the unfoldQuantifier parameter of the SMTConstraint to false. As it is possible to specify arbitrary subsets in both cases when defining IQuantifierExpression (i.e. ForAll and Exists), the difference in behavior is misleading.

The proposed changes is also likely increase the solvers performance in cases where the selection of the elements is not trivial. Assuming that a subset is defined by the combination of multiple properties, the evaluation of the left side of the implication used for selection becomes expensive, especially considering that it has to be evaluated for every member of the superset. With a selector only one function has to be evaluated.

Expected Behavior:

The following snippets should express the same constraints. Currently the first one specifies a correct pre-allocation constraint, applying one task and one ECU only while the second one ignores the specified tasks and quantifies over both complete supersets leading to an unsatisfiable statement.

Set<Task> tasks = createSet(
        superSetMap.get(Task.class),
        superSetMap.get(Task.class).getEntries().stream()
                .filter(t -> t.getName().equals("Task 1")).findAny().get(),
        Task.class);
Set<ExecutionUnit> ecus = createSet(
        superSetMap.get(ExecutionUnit.class),
        superSetMap.get(ExecutionUnit.class).getEntries().stream()
                .filter(e -> e.getName().equals("ECU 2")).findAny().get(),
        ExecutionUnit.class);

Allocation allocation = createAllocation(createModelElementLiteral(tasks),
        createModelElementLiteral(ecus));
ForAll forAll = generateForAll(tasks, generateForAll(ecus, allocation));

SMTConstraint constraint = createSMTConstraint("Pre-allocation constraint", forAll, false, true);
Set<Task> tasks = createSet(
        superSetMap.get(Task.class),
        superSetMap.get(Task.class).getEntries().stream()
                .filter(t -> t.getName().equals("Task 1")).findAny().get(),
        Task.class);
Set<ExecutionUnit> ecus = createSet(
        superSetMap.get(ExecutionUnit.class),
        superSetMap.get(ExecutionUnit.class).getEntries().stream()
                .filter(e -> e.getName().equals("ECU 2")).findAny().get(),
        ExecutionUnit.class);

Allocation allocation = createAllocation(createModelElementLiteral(tasks),
        createModelElementLiteral(ecus));
ForAll forAll = generateForAll(tasks, generateForAll(ecus, allocation));

SMTConstraint constraint = createSMTConstraint("Pre-allocation constraint", forAll, false, false);

Tasks

  • Set default value for IQuantifiedExpression::unfold to false again to revert the temporary workaround from #3787.
  • Implement a selector function, which combined with an implication achieves the desired behavior (as shown in the following SMT-LIB snipped)
  • Evaluate different options for selector functions (e.g. bit vectors, arrays etc.)
(declare-datatypes () ((Type a b c)))
(declare-fun prop (Type) Int)

(assert (= (prop a) 1))
(assert (= (prop b) 2))
(assert (= (prop c) 3))

(declare-fun sel (Type) Bool)
(assert (sel a))
(assert (sel b))
(assert (not (sel c)))

(assert (forall ((t Type)) (=> (sel t) (< (prop t) 3))))

(check-sat)

History

#1 Updated by Tiziano Munaro over 1 year ago

  • Description updated (diff)

#2 Updated by Simon Barner over 1 year ago

  • Description updated (diff)

Reference #3787.

#3 Updated by Tiziano Munaro about 1 year ago

  • Target version changed from AF3 2.16 RC1 (Feature Freeze) to AF3 2.17 (Feature Freeze)

#4 Updated by Alexander Diewald 10 months ago

  • Target version changed from AF3 2.17 (Feature Freeze) to Backlog

Also available in: Atom PDF