Enable unfolded quantification over subsets in SMT
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(
supersetmaget(task.class),
supersetmaget(task.class).getentries().stream()
.filter(t -> t.getname().equals("task 1")).findany().get(),
task.class);
set<executionunit> ecus = createset(
supersetmaget(executionunit.class),
supersetmaget(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);
<code class="java
Set<Task> tasks = createSet(
superSetMaget(Task.class),
superSetMaget(Task.class).getEntries().stream()
.filter(t -> t.getName().equals("Task 1")).findAny().get(),
Task.class);
Set<ExecutionUnit> ecus = createSet(
superSetMaget(ExecutionUnit.class),
superSetMaget(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.](https://rise4fun.com/Z3/tutorial/guide))
<!-- -->
(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)
*(from redmine: issue id 3703, created on 2019-04-03)*