Skip to content

Instantly share code, notes, and snippets.

@beala
Created May 23, 2015 04:55
Show Gist options
  • Save beala/9f89fbbe5f5134ceedcb to your computer and use it in GitHub Desktop.
Save beala/9f89fbbe5f5134ceedcb to your computer and use it in GitHub Desktop.
smt scheduling
import Data.SBV
sched :: SInteger -> SInteger -> SInteger -> SInteger -> SInteger -> SInteger -> SBool
sched t_11 t_12 t_21 t_22 t_31 t_32 = (t_11 .>= 0) &&& (t_12 .>= t_11 + 2) &&& (t_12 + 1 .<= 8) &&&
(t_21 .>= 0) &&& (t_22 .>= t_21 + 3) &&& (t_22 + 1 .<= 8) &&&
(t_31 .>= 0) &&& (t_32 .>= t_31 + 2) &&& (t_32 + 3 .<= 8) &&&
((t_11 .>= t_21 + 3) ||| (t_21 .>= t_11 + 2)) &&&
((t_11 .>= t_31 + 2) ||| (t_31 .>= t_11 + 2)) &&&
((t_21 .>= t_31 + 2) ||| (t_31 .>= t_21 + 3)) &&&
((t_12 .>= t_22 + 1) ||| (t_22 .>= t_12 + 1)) &&&
((t_12 .>= t_32 + 3) ||| (t_32 .>= t_12 + 1)) &&&
((t_22 .>= t_32 + 3) ||| (t_22 .>= t_22 + 1))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment