kdrag.theories.seq

Built in smtlib theory of finite sequences.

Functions

`Cons`(x, tl)
`Nil`(s)
`Seq`(T)	Make sort of Sequences and prove useful lemmas.
`Unit`(x)	Construct a sequence of length 1.
`induct_list`(x, P)

kdrag.theories.seq.Cons(x: ExprRef, tl: SeqSortRef)

>>> smt.simplify(Cons(smt.IntVal(3), Nil(smt.IntSort())))
Unit(3)

Parameters:

x (ExprRef)
tl (SeqSortRef)

kdrag.theories.seq.Nil(s: SortRef)

Parameters:: s (SortRef)

kdrag.theories.seq.Seq(T: SortRef) → SeqSortRef

Make sort of Sequences and prove useful lemmas.

>>> BoolSeq = Seq(smt.BoolSort())
>>> x,y,z = smt.Consts("x y z", BoolSeq)
>>> x + y
Concat(x, y)

Parameters:: T (SortRef)
Return type:: SeqSortRef

kdrag.theories.seq.Unit(x: ExprRef) → SeqRef

Construct a sequence of length 1.

Parameters:: x (ExprRef)
Return type:: SeqRef

kdrag.theories.seq.induct_list(x: SeqRef, P)

>>> x = smt.Const("x", Seq(smt.IntSort()))
>>> P = smt.Function("P", Seq(smt.IntSort()), smt.BoolSort())
>>> induct_list(x, P)
|= Implies(And(P(Empty(Seq(Int))),
            ForAll([hd!..., tl!...],
                  Implies(P(tl!...),
                          P(Concat(Unit(hd!...), tl!...))))),
        P(x))

Parameters:: x (SeqRef)