Module Unroller

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.