mantiserve.liftsmt2 module

This module is an interface to a custom SMTLIBv2 parser that is able to lift SMTLIBv2 statements into python expressions and support the insertion of python variables and values into the lifted SMT statement through the parsing of a unique replacement identifier.

exception mantiserve.liftsmt2.LiftingError

Bases: Exception

Generic error during lifting of SMT expression.

exception mantiserve.liftsmt2.MismatchedDeclReplace

Bases: mantiserve.liftsmt2.LiftingError

Exception for when replacement of declaration goes wrong.

class mantiserve.liftsmt2.SMTLIBv2Lifter(decls: Optional[List[Any]] = None)

Bases: smt2lib.SMTLIBv2Listener.SMTLIBv2Listener

Parameters

decls (Optional[List[Any]]) –

Return type

None

enterReplace_identifier(ctx: smt2lib.SMTLIBv2Parser.SMTLIBv2Parser.Replace_identifierContext) → None

Replaces the special identifier with what is listed in our declarations.

Parameters

ctx (smt2lib.SMTLIBv2Parser.SMTLIBv2Parser.Replace_identifierContext) –

Return type

None

enterSpec_constant(ctx: smt2lib.SMTLIBv2Parser.SMTLIBv2Parser.Spec_constantContext) → None

A constant identifier.

Add to the current operator’s argument stack

Parameters

ctx (smt2lib.SMTLIBv2Parser.SMTLIBv2Parser.Spec_constantContext) –

Return type

None

enterSymbol(ctx: smt2lib.SMTLIBv2Parser.SMTLIBv2Parser.SymbolContext) → None

Symbol is an operation on a (term | identifier | spec_constant).

Set as the current operator.

Parameters

ctx (smt2lib.SMTLIBv2Parser.SMTLIBv2Parser.SymbolContext) –

Return type

None

exitCommand(_: smt2lib.SMTLIBv2Parser.SMTLIBv2Parser.CommandContext) → None

End of the command.

Apply our operations to the collected arguments

Parameters

_ (smt2lib.SMTLIBv2Parser.SMTLIBv2Parser.CommandContext) –

Return type

None

property expr: Any

The resulting expression after lifting.

exception mantiserve.liftsmt2.UnhandledCase

Bases: mantiserve.liftsmt2.LiftingError

Exception for when we encounter an SMT formula with a case that we don’t handle yet.

exception mantiserve.liftsmt2.UnsupportedArithOp

Bases: mantiserve.liftsmt2.LiftingError

Exception for when we encounter unsupported arithmetic mapping operations from string to Python operation.

mantiserve.liftsmt2.lift_smt2_to_python(smt2: Union[antlr4.InputStream.InputStream, str], decls: List[Any]) → Any

Lift the custom smt2 expression with the special replacement identifier and insert the decls.

Parameters

  • smt2 – The SMT2 formula to lift into Python

  • decls – A list of Python declaration expressions to place in the lifted SMT2 formula

  • smt2 (Union[antlr4.InputStream.InputStream, str]) –

  • decls (List[Any]) –

Returns

Python expression equivalent to SMT2 formula

Return type

Any

mantiserve.liftsmt2.main() → Any
Return type

Any

mantiserve.liftsmt2.validate_smt2(smt2: Union[antlr4.InputStream.InputStream, str], replacements: List[int]) → List[str]

Validate the smt2 formula according to our grammar. Return empty list if valid, or list of errors otherwise.

Parameters

  • smt2 – The SMT2 formula to validate

  • replacements – List of replacements corresponding to replacement keywords within smt2

  • smt2 (Union[antlr4.InputStream.InputStream, str]) –

  • replacements (List[int]) –

Returns

List of errors if any, or empty list

Return type

List[str]