nuZ's minimum != get-model

interval.clj

;; Interval(begin, end)
(declare-datatypes (BeginT EndT) ((IntervalT (makeInterval (begin BeginT) (end EndT)))))
(define-sort Interval () (IntervalT Int Int))


(define-fun intervalExpandsIntoFuture? ((interval Interval)) (Bool)
  (< (begin interval) (end interval)))

(define-fun intervalDuration ((interval Interval)) (Int)
  (- (end interval) (begin interval)))

(define-fun intervalRequiresIntervalOver ((lhs Interval) (rhs Interval)) (Bool)
  (> (begin lhs) (end rhs)))

(define-fun intervalDuringInterval? ((lhs Interval) (rhs Interval)) (Bool)
  (and
    (> (begin lhs) (begin rhs))
    (< (end lhs) (end rhs))))



(declare-const schedule Interval)

(declare-const makeDough Interval)
(declare-const sliceOnions Interval)
(declare-const sliceTomatos Interval)
(declare-const bakeInOven Interval)
(declare-const servePizza Interval)
(declare-const pourWine Interval)



(assert (and
          (= 0 (begin schedule))
          (intervalExpandsIntoFuture? schedule)

          (intervalExpandsIntoFuture? makeDough)
          (intervalExpandsIntoFuture? sliceOnions)
          (intervalExpandsIntoFuture? sliceTomatos)
          (intervalExpandsIntoFuture? bakeInOven)
          (intervalExpandsIntoFuture? servePizza)
          (intervalExpandsIntoFuture? pourWine)

          (intervalDuringInterval? makeDough schedule)
          (intervalDuringInterval? sliceOnions schedule)
          (intervalDuringInterval? sliceTomatos schedule)
          (intervalDuringInterval? bakeInOven schedule)
          (intervalDuringInterval? servePizza schedule)
          (intervalDuringInterval? pourWine schedule)

          (< 3 (intervalDuration makeDough) 10)
          (< 2 (intervalDuration sliceOnions) 10)
          (< 2 (intervalDuration sliceTomatos) 20)
          (= 35 (intervalDuration bakeInOven))
          (= 2 (intervalDuration servePizza))
          (= 2 (intervalDuration pourWine))

          (intervalRequiresIntervalOver bakeInOven makeDough)
          (intervalRequiresIntervalOver bakeInOven sliceOnions)
          (intervalRequiresIntervalOver bakeInOven sliceTomatos)

          (intervalRequiresIntervalOver servePizza bakeInOven)

          true))


(minimize (intervalDuration schedule))


(check-sat)
(get-model)


;; vim: set filetype=clojure:

out.txt

(- (end schedule) (begin schedule)) |-> 46
sat
(model 
  (define-fun pourWine () (IntervalT Int Int)
    (makeInterval 1 3))
  (define-fun schedule () (IntervalT Int Int)
    (makeInterval 0 83))
  (define-fun sliceTomatos () (IntervalT Int Int)
    (makeInterval 38 41))
  (define-fun servePizza () (IntervalT Int Int)
    (makeInterval 80 82))
  (define-fun sliceOnions () (IntervalT Int Int)
    (makeInterval 40 43))
  (define-fun makeDough () (IntervalT Int Int)
    (makeInterval 39 43))
  (define-fun bakeInOven () (IntervalT Int Int)
    (makeInterval 44 79))
)