parse

abstract fun parse(smtLibFile: Path): List<KExpr<KBoolSort>>

Parse the given file smtLibFile using the SMT-LIB2 parser.

Return

a list of assertions.

Throws

if smtLibFile does not conform to the SMT-LIB2 format.

Note. If the string contains push/pop commands, the set of assertions returned are the ones in the last scope level.


abstract fun parse(smtLibString: String): List<KExpr<KBoolSort>>

Parse the given string smtLibString using the SMT-LIB2 parser.

Return

a list of assertions.

Throws

if smtLibString does not conform to the SMT-LIB2 format.

Note. If the string contains push/pop commands, the set of assertions returned are the ones in the last scope level.