kdrag.theories.seq

Built in smtlib theory of finite sequences.

Functions

`Cons`(x, tl)
`Head`(s)
`Nil`(s)
`Seq`(T)	Make sort of Sequences and prove useful lemmas.
`Tail`(s)
`Unit`(x)	Construct a sequence of length 1.
`induct`(T, P)
`induct_list`(x, P)
`seq`(*args)	Helper to construct sequences.

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.Head(s: SeqRef)

>>> x = smt.Const("x", Seq(smt.BoolSort()))
>>> Head(x)
Nth(x, 0)
>>> kd.prove(smt.Implies(smt.Length(x) > 0, smt.Concat([smt.Unit(Head(x)), Tail(x)]) == x))
|= Implies(Length(x) > 0,
    Concat(Unit(Nth(x, 0)),
            seq.extract(x, 1, Length(x) - 1)) ==
    x)

Parameters:: s (SeqRef)

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.Tail(s: SeqSortRef)

>>> x = smt.Const("x", Seq(smt.BoolSort()))
>>> Tail(x)
seq.extract(x, 1, Length(x) - 1)

Parameters:: s (SeqSortRef)

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

Construct a sequence of length 1.

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

kdrag.theories.seq.induct(T: SortRef, P) → Proof

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

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)

kdrag.theories.seq.seq(*args): Helper to construct sequences. >>> seq(1, 2, 3) Concat(Unit(1), Concat(Unit(2), Unit(3))) >>> seq(1) Unit(1)