Module Unroller

module Unroller: sig .. end
Very basic helper functions for unrolling. More precisely, asserting one- and two-state invariants.

val assert_0_to : SMTSolver.t -> Numeral.t -> Term.t -> unit
Asserts some terms from 0 to k-1.
val assert_1_to : SMTSolver.t -> Numeral.t -> Term.t -> unit
Asserts some terms from 1 to k-1.
val assert_new_invs_to : SMTSolver.t -> Numeral.t -> Term.TermSet.t * Term.TermSet.t -> unit
Asserts some new one- and two-state invariant up to k-1, starting at * 0 for one-state invariants, * 1 for two-state invariants.