Module FlatCurry.Names2SMT

Definition of some names of primitive operations occurring in FlatCurry programs, like arithmetic and relational operators, and their counterparts used in SMT solvers.

Author: Michael Hanus

Version: September 2024

Summary of exported operations:

unaryPrimOps :: [(String,String)]  Deterministic 
Primitive unary operations of the prelude and their SMT names.
binaryPrimOps :: [(String,String)]  Deterministic 
Primitive binary operations of the prelude and their SMT names.

Exported operations:

unaryPrimOps :: [(String,String)]  Deterministic 

Primitive unary operations of the prelude and their SMT names.

Further infos:
  • solution complete, i.e., able to compute all solutions

binaryPrimOps :: [(String,String)]  Deterministic 

Primitive binary operations of the prelude and their SMT names.

Further infos:
  • solution complete, i.e., able to compute all solutions