[Question] Removing unused variables

[gskorokhod]

Consider this rewrite:

Model before rewriting:

letting A be false
letting NotA be Not(Not(Not(A)))
find b: int(1..20)

such that

(NotA) -> ((b < 3))

--

Not(Not(Not(A))), 
   ~~> remove_double_negation ([("Base", 8400)]) 
Not(A) 

--

(b < 3), 
   ~~> lt_to_leq ([("Minion", 8400)]) 
(b <= Sum([3, -1])) 

--

Sum([3, -1]), 
   ~~> apply_eval_constant ([("Constant", 9001)]) 
2 

--

A, 
   ~~> substitute_value_lettings ([("Base", 5000)]) 
false 

--

Not(false), 
   ~~> apply_eval_constant ([("Constant", 9001)]) 
true 

--

NotA, 
   ~~> substitute_value_lettings ([("Base", 5000)]) 
true 

--

(true) -> ((b <= 2)), 
   ~~> partial_evaluator ([("Base", 9000)]) 
(b <= 2) 

--

(b <= 2), 
   ~~> leq_to_ineq ([("Minion", 4100)]) 
Ineq(b, 2, 0) 

--

Final model:

letting A be false
letting NotA be true
find b: int(1..20)

such that

Ineq(b, 2, 0)

In the final model, A and NotA are not used at all.
So, my question is:

• Should we add a rule to remove "dead code" (unused variables, etc)
• In terms of Reduction / rewriter implementation, should there be a way to remove constraints / symbols as a side-effect as well as adding them?
  How hard would that be to implement?

[niklasdewally]

In the final model, A and NotA are not used at all.

Should we add a rule to remove "dead code" (unused variables, etc)

Lettings will always be unused at the end of rewriting, as we substitute them for their values inside the model. They don't get passed to the solver, so have no solve performance impact.

However, removing dead decision variables is definitely an optimisation we should do, and Savile Row does it with the -S1 flag (iirc). If its a user variable, we cannot fully delete it, and we must give it a value to return to the user.

• In terms of Reduction / rewriter implementation, should there be a way to remove constraints / symbols as a side-effect as well as adding them?

Let's consider variable removal when we design / discuss scope further. Shouldn't be too hard :)

It only makes sense to remove constraints from expressions containing Vec - we are already able to make a rule to do this generically using Uniplate, especially once #596 lands.