                                                    [v (var-name ha-id v "enter" last-t)])
                                                  vars))
                               _ (assert (not (empty? v0-vars)))
+                              mid-t (var-name "mid-t" new-t last-t)
+                              vmid-vars (into {}
+                                              (map (fn [v] [v (var-name ha-id v "check" last-t)])
+                                                   vars))
                               vT-vars (into {}
                                             (map (fn [v] [v (var-name ha-id v "exit" last-t)])
                                                  vars))]
-                          (flow-constraints z3 ha-id (:bounds ha-def) sdef v0-vars vT-vars last-t new-t)))
+                          (flow-constraints z3 ha-id (:bounds ha-def) sdef v0-vars vmid-vars vT-vars last-t mid-t new-t)))
                       has))
     (if (<= bound 0)
       (do

            bins (flow-bins bmin bmax)]
        (cond
          (= dflow 0)
          (into [:or]
                (map (fn [[a b]]
                       [:and
                        [:geq flow0 a]
                        [:leq flow0 b]
                        [:geq f1 [:+ f0 [:* a dt]]]
                        [:leq f1 [:+ f0 [:* b dt]]]])
                     bins))
          (vector? dflow)
          (let [[acc limit] dflow
                dv [:- limit flow0]

      (throw e)
      (.mkFalse ctx))))

(defn update-ha-defs [{context        :context
                       use-datatypes? :use-datatypes :as z3}
                      ha-defs]
  (let [state-sorts
        (into {}
              (for [[ha-type {states :states}] ha-defs
                    :let [sort-name (var-name ha-type "state")
                          state-ids (sort (map (fn [[sid _s]]
                                                 (name sid))
                                               states))
                          sort (.mkEnumSort context
                                            ^String sort-name
                                            ^"[Ljava.lang.String;" (into-array state-ids))]]
                [sort-name
                 {:sort   (if use-datatypes?
                            sort
                            (.mkIntSort context))
                  :consts (zipmap state-ids
                                  (if use-datatypes?
                                    (.getConsts sort)
                                    (map #(.mkInt context %) (range 0 (count state-ids)))))}]))]
    (assoc z3 :state-sorts state-sorts
              :ha-defs ha-defs)))

(defn ->z3 [ha-defs settings]
  (let [settings (merge {:use-datatypes? false}
                        settings)]
    (update-ha-defs (merge settings
                           {:context (Context. (reduce
                                                 (fn [m [k v]]
                                                   (.put m k v)
                                                   m)
                                                 (HashMap.)
                                                 (merge {"proof"             "false"
                                                         "well_sorted_check" "true"
                                                         "model"             "true"
                                                         "model_validate"    "true"
                                                         "unsat_core"        "false"}
                                                        (into {}
                                                              (map (fn [[k v]]
                                                                     [(name k) (str v)])
                                                                   (dissoc
                                                                     settings
                                                                     :must-semantics?
                                                                     :stuck-implies-done?
                                                                     :use-datatypes?
                                                                     :linearize?))))))})
                    ha-defs)))

(defn map->params [ctx m]
  (reduce
    (fn [params [k v]]
      (.add params (name k) v)
      params)
    (.mkParams ctx)
    m))

(defn map-vals [fnk kvmap]
  (reduce
    (fn [m [k v]]
      (assoc m k (fnk v)))
    kvmap
    kvmap))

(defn with-solver [{ctx :context :as z3} func]
  (let [stacs (.andThen ctx
                        (.usingParams ctx
                                      (.mkTactic ctx "simplify")
                                      (map->params ctx {:som             true :arith-lhs true
                                                        :hoist-cmul      true :hoist-mul true
                                                        :ite-extra-rules true :local-ctx true
                                                        :pull-cheap-ite  true :push-ite-arith true}))
                        (.mkTactic ctx "purify-arith")
                        (into-array Tactic [(.mkTactic ctx "propagate-values")
                                            (.mkTactic ctx "solve-eqs")
                                            (.usingParams ctx
                                                          (.mkTactic ctx "simplify")
                                                          (map->params ctx {:som             true :arith-lhs true
                                                                            :hoist-cmul      true :hoist-mul true
                                                                            :ite-extra-rules true :local-ctx true
                                                                            :pull-cheap-ite  true :push-ite-arith true}))
                                            ;skip QE because lira/smt can handle linear quantifiers
                                            #_(.usingParams ctx
                                                            (.mkTactic ctx "qe")
                                                            (map->params ctx {:qe-nonlinear true}))
                                            (.mkTactic ctx "propagate-values")
                                            (.mkTactic ctx "solve-eqs")
                                            (.cond ctx (.mkProbe ctx "is-lira")
                                                   (.mkTactic ctx "lira")
                                                   (.andThen ctx
                                                             (.mkTactic ctx "tseitin-cnf")
                                                             (.cond ctx (.mkProbe ctx "is-nra")
                                                                    (.orElse ctx
                                                                             (.mkTactic ctx "qfnra-nlsat")
                                                                             (.mkTactic ctx "qfnra"))
                                                                    (.fail ctx))
                                                             (into-array Tactic [])))]))
        s (.mkSolver ctx stacs)
        oparams (.mkParams ctx)
        o nil #_(.mkOptimize ctx)
        z3 (assoc z3 :optimizer o :solver s :last-t nil :prev-last-t nil)
        ret (func z3)]
    (Global/setParameter "pp.decimal" "true")
    (Global/setParameter "verbose" "10")
    (when s
      (.setParameters s (map->params ctx
                                     {"smt.arith.nl" false
                                      "smt.mbqi"     false})))
    (when o
      (.setParameters o oparams))
    (when (seq? ret)
      (doall ret))
    ret))

(defn pop! [{o :optimizer s :solver :as z3}]
  (when o (.Pop o))
  (when s (.pop s))
  z3)

(defn push! [{o :optimizer s :solver :as z3}]
  (when o (.Push o))
  (when s (.push s))
  z3)
(defn model? [m] (instance? Model m))

(defn not-model? [m] (not (model? m)))

(defn check! [{s :solver}]
  #_(println "check\n" (.toString s))
  (println "call solver")
  (let [status (time (.check s))]
    (println status)
    (cond
      (= status Status/UNSATISFIABLE) :unsat                ;todo: unsat core?
      (= status Status/SATISFIABLE) (.getModel s)
      (= status Status/UNKNOWN) (do
                                  (Thread/sleep 100)
                                  (println "-----CHECK-----\n" s "\n-----\n" "NAs:" (.getNumAssertions s) "\n" "Stats:" (.getStatistics s))
                                  (println "reason:" (.toString (.getReasonUnknown s)))
                                  (Thread/sleep 500)
                                  (assert false)
                                  :unknown)
      :else (throw (IllegalStateException. (str "Unrecognizable status from solver" status))))))

(defn value [{ctx :context} ^Model model var]
  (assert (model? model))
  (let [var-expr (if (instance? Expr var)
                   var
                   (.mkRealConst ctx var))
        ;_ (println "get var from model" var var-expr)
        ;todo: if the var is not in the model, return nil. don't just use try/catch!
        result (try
                 (.getConstInterp model ^Expr var-expr)
                 (catch Z3Exception _e
                   #_(println "z3exception" (.toString _e))
                   nil))]
    (cond
      (nil? result) nil
      (or (.isReal result) (.isInt result)) (rat->float result)
      (.isTrue result) true
      (.isFalse result) false
      :else (.toString result))))

(defn picked-out-edge-c [{has     :has
                          ha-defs :ha-defs
                          ctx     :context} ha-id state edge-idx t]
  (let [ha-type (get has ha-id)
        ha-def (get ha-defs ha-type)
        max-edge-count (apply max (map #(count (:edges %)) (vals (:states ha-def))))
        edges (range -1 max-edge-count)
        sdef (get-in ha-def [:states state])]
    (assert (>= edge-idx -1))
    (assert (< edge-idx (count (:edges sdef))) (str "Picked out edge " edge-idx " for state " state " with " (count (:edges sdef)) " edges: " sdef))
    (into [:and]
          (map (fn [i]
                 (let [nom (var-name ha-id "out-edge" i t)
                       bc (.mkBoolConst ctx nom)]
                   (if (= i edge-idx)
                     [:eq bc true]
                     [:eq bc false])))
               edges))))

(defn in-state-c [{has     :has
                   ha-defs :ha-defs
                   ctx     :context} ha-id state-name t]
  (let [ha-type (get has ha-id)
        states (keys (get-in ha-defs [ha-type :states]))]
    (into [:and]
          (map (fn [id]
                 (let [nom (var-name ha-id "state" id t)
                       bc (.mkBoolConst ctx nom)]
                   (if (= id state-name)
                     [:eq bc true]
                     [:eq bc false])))
               states))))

(defn path-component [{has :has ha-defs :ha-defs ctx :context :as z3}
                      model
                      ha-id
                      t]
  (let [ha-type (get has ha-id)
        ha-def (get ha-defs ha-type)
        states (:states ha-def)
        in-state (some (fn [{id :id :as s}]
                         (if (value z3 model (.mkBoolConst ctx (var-name ha-id "state" id t)))
                           s
                           nil))
                       (vals states))
        out-edge (some
                   (fn [{i :index :as e}]
                     (if (value z3 model (.mkBoolConst ctx (var-name ha-id "out-edge" i t)))
                       e
                       nil))
                   (concat [{:index -1 :sample-edge true}]
                           (:edges in-state)))]
    [(:id in-state) (:index out-edge)]))

(defn path-components [{has :has :as z3}
                       model
                       t]
  (into {}
        (map (fn [ha-id]
               [ha-id (path-component z3 model ha-id t)])
             (keys has))))

(defn ha-moves [z3 model last-t new-t]
  (let [out-state-edges-by-ha-id (ha/spy "components old" (path-components z3 model last-t))
        new-states-by-ha-id (map-vals first (ha/spy "components new" (path-components z3 model new-t)))]
    (into {}
          (map (fn [[ha-id [prev-state out-edge]]]
                 (let [in-state (get new-states-by-ha-id ha-id)]
                   [ha-id [prev-state out-edge in-state]]))
               out-state-edges-by-ha-id))))

(defn assert-all! [{opt  :optimizer
                    solv :solver :as z3} constraints]
  (let [translated (translate-constraint z3 (into [:and] constraints))]
