The datakind for the types in our EUF logic.

A singleton type for natural numbers that can be used as the widths of bitvectors.

Create a BVWidth object for a KnownNat that is non-zero

A singleton type that represents type-level EUFTypes at the object level

A list of TypeReprs for each type in a type-level list

An EUFType with a known TypeRepr representation

A sequence of types EUFType with a known TypeReprs representation

An uninterpreted function in our EUF logic, which is a string name plus the input and output types.

The operations of our EUF logic, which are indexed by a list of 0 or more input types and a single output type.

Create an uninterpreted Op of known type

Get the input types and output type of an Op

Get the input types of an Op

The expressions of our EUF logic, which are just operations applied to argument expressions.

A sequence of expressions for each type in a type-level list

Build the type EUFExpr in1 -> ... -> EUFExpr inn -> out

Build an EUFExprFun from a function on EUFExprs

Apply an Op to EUFExprs for its input types, returning an EUFExpr for its output type

Build an expression from an uninterpreted operation of a known type

Convert an EUFType to a type of SBV expressions

Convert the type inputs plus output of an Op to a function over SBV values

Create an SMTDefinable instance for the type returned by OpTypes2SBV and pass it to a local function

An uninterpreted function that has been resolved to an SBV function

A Map for resolving uninterpreted operations

Look up the uninterpreted op associated with a String in an UnintMap at a particular type, raising an error if that String is associated with a different type. If the String is not associated with any uninterpreted function, create one and return it, updating the UnintMap.

The monad for interpreting EUFExprs into SBV, which is just a state monad over an UnintMap

Run an InterpM computation starting with the empty UnintMap

Interpret an Op into a function over SBV values

Interpret an EUFExpr into an SBV value.

Apply an interpretation of an operator to the interpretations of a sequence of arguments for it.

Top-level call to interpret an EUFExpr to an SBV value

Example EUF problem

f (f (a) - f (b)) /= f (c), b >= a, a >= b + c, c >= 0

from https://goto.ucsd.edu/~rjhala/classes/sp13/cse291/slides/lec-smt.markdown.pdf noting that x >= y is the same as not (x < y). We have:

>>> sat $ interpEUF example
Satisfiable. Model:
  a =  996506182 :: Word32
  b = 3298461113 :: Word32
  c = 1445036292 :: Word32

  f :: Word32 -> Word32
  f 0          = 4188219399
  f 1445036292 = 285239361
  f 3298461113 = 4054018119
  f 996506182  = 4054018119
  f _          = 0

Note that the original example is unsatisfiable over integers. It is however satisfiable over 32-bit words, hence the model above.