equal
deleted
inserted
replaced
728 |
728 |
729 fun merge a b = Symtab.merge (op =) (a, b) |
729 fun merge a b = Symtab.merge (op =) (a, b) |
730 |
730 |
731 fun mergemap f ts = fold (fn x => fn table => merge table (f x)) ts Symtab.empty |
731 fun mergemap f ts = fold (fn x => fn table => merge table (f x)) ts Symtab.empty |
732 |
732 |
733 fun diff a b = Symtab.fold (fn (k, v) => fn a => |
733 fun diff a b = Symtab.fold (Symtab.delete_safe o fst) b a |
734 (Symtab.delete k a) handle UNDEF => a) |
|
735 b a |
|
736 |
734 |
737 fun collect_vars (cplexVar v) = singleton v |
735 fun collect_vars (cplexVar v) = singleton v |
738 | collect_vars (cplexNeg t) = collect_vars t |
736 | collect_vars (cplexNeg t) = collect_vars t |
739 | collect_vars (cplexProd (t1, t2)) = |
737 | collect_vars (cplexProd (t1, t2)) = |
740 merge (collect_vars t1) (collect_vars t2) |
738 merge (collect_vars t1) (collect_vars t2) |