[m-dev.] Porting Vitaly's set solver to use solver types.

[Ralph Becket]

We should discuss how best to make Vitaly's set solver package a solver
type.

Using the current set solver package, one can
- construct int, set, and multiset expressions,
- construct constraint expressions (equals, less than etc.) within those
  types,
- construct boolean constraint expressions (and, or, not etc.) over
  these constraint expressions,
- add constraint expressions to the constraint store,
- ask for a labelling.

(1) The solver types we have worked on prior to this have not supported 
boolean constraint expressions (relations between expressions have been
implemented as predicates that directly affect the constraint store,
with no need for an explicit "add to constraint store" action).  But
these constraint expressions are clearly an important property of BDDs,
so it seems to me that on this basis we will need to keep the "add
constraint" action in the interface to Vitaly's package.

(2) As far as I can tell, the only time when the posted constraints are
examined for consistency is when the labelling predicate is invoked.
- We need to be able to decide if adding a new set solver constraint is
  consistent or not.  That is, we need an incremental solving option in
  addition to the current batch-mode mechanism.  Vitaly, is there a
  reasonably cheap way of testing the BDD for consistency?
- Should things like equality tests between variables force a
  consistency check (i.e., not be batched)?  My gut feeling is "yes",
  but I'm not sure.

-- Ralph
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------