     (assert (<= (Math/abs ^double (- (rat->float rat) (/ (double val-int) val-denom))) 1)
             (str "R: " (.toString rat) " RF: " (rat->float rat) " VALDIV: " val-int "/" val-denom " = " (/ (double val-int) val-denom)))
     rat))
-
-(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}))
-                                            (.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")
-                                                   ; tried using the 'lira' tactic here but it was slower...
-                                                   (.mkTactic ctx "smt")
-                                                   (.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"     true})))
-    (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 ^Expr translate-constraint [{ctx :context :as z3} c]
   (try

                                                                   (map :guard
                                                                        (filter ha/required-transition? (:edges state))))))
                                           v0-vars
                                           vT-vars
                                           last-t
                                           new-t
                                           dt)
                               true)]
    (into
      [:and

                                   (str "bmc-step-" idx)
                                   (.mkRealSort ctx)))
                  (range 0 unroll-limit))
        _ (println "bmc")
        [z3 _t-vars status path]
        (time (reduce
                (fn [[z3 used-vars status path] t-var]
                  (println "generate one-step" (count used-vars))
                  (let [z3 (if (not= t-var "t00")
                             (time (bmc-1! z3 t-var))
                             z3)
                        _ (println "done generating one-step" (count used-vars))
                        next-vars (conj used-vars t-var)
                        [z3 model] (if (> (count next-vars) unroll-min)
                                     (let [z3 (push! z3)
                                           z3 (assert-reached-states! z3 next-vars target-states)
                                           model (check! z3)
                                           z3 (pop! z3)]
                                       [z3 model])
                                     [z3 nil])]
                    (if (model? model)
                      (reduced
                        ; assert them again so z3 is in the right state with the right push/pop nesting
                        (let [z3 (assert-reached-states! z3 next-vars target-states)
                              path-steps (map (fn [prev next]
                                                (ha-moves z3 model prev next))
                                              (butlast next-vars)
                                              (rest next-vars))
                              witness-path (ha/spy "witness path"
                                                   (map (fn [ts edge-state]
                                                          [(.toString ts)
                                                           (value z3 model ts)
                                                           edge-state])
                                                        (rest next-vars)
                                                        path-steps))]
                          (if target-states
                            [z3 next-vars :witness witness-path]
                            [z3 next-vars :sat witness-path])))
                      [z3 next-vars status path])))
                [z3 [] :unsat nil]
                (concat ["t00"] vars)))]
    (println "done bmc")
    [z3 status path]))

;todo: spec
(defn path-constraints [{has :has :as z3} time-steps]
