Remove dimensions from models

[doyougnu]

sbv does not have the concept of variation or of dimensions, thus we are using plain SBools in sbv land to represent dimensions internally in the solver. This means that every model that is queries from sbv will have bindings for the dimensions:

model := 
Aleft   -->   (ite ~AA (0 :: Integer) ite AA (13 :: Integer) Undefined)
Aright   -->   ite ~AA (13 :: Integer) Undefined
AA   -->   (ite ~AA (False :: Bool) ite AA (False :: Bool) Undefined)

Sat_Model := 
(~AA or AA)

for example. But this not only obfuscates results it also increases runtime in the underlying solver by some constant factor. Thus we should remove the dimensions from the model. The actual fix here will be to spin up another instance of sbv in a separate thread, store the thread, and then use the thread internally to only handle operations on dimensions. This would keep the dimension variable space disjoint from the regular variables space and thus we would retrieve the better models for free.

[doyougnu]

Closed in a6e45befa730bc47820772491cfbba0112637005 the fix was to setup incremental solving for variant contexts:

• fork a thread and spin up a sbv instance reading from channels, the instance constrains a variant context if one exists
• using those channels send over a dimension and flag on whether to negate the function or not
• the sbv instance creates the variable if need and checks sat returning the result, if the variable needs to be negated it is here
• the main thread then takes the result and continues processing