sig
  type numconstraint = CEq | CNeq | CLt | CGt | CLte | CGte
  type varname = string
  type recordindex = string * string * int
  type constraintbinop = CPlus | CMinus | CTimes | CDivide
  type cvar =
      CVar of Constraint.Constraint.varname
    | CRecordVar of Constraint.Constraint.recordindex
  type cexp =
      CVarExp of Constraint.Constraint.cvar
    | CInt of int
    | CArithop of Constraint.Constraint.constraintbinop *
        Constraint.Constraint.cexp * Constraint.Constraint.cexp
    | CBoolop of Constraint.Constraint.numconstraint *
        Constraint.Constraint.cexp * Constraint.Constraint.cexp
    | CGuard of Constraint.Constraint.cexp * Constraint.Constraint.cexp *
        Constraint.Constraint.cexp
    | CAnd of Constraint.Constraint.cexp list
    | COr of Constraint.Constraint.cexp list
    | CTrue
    | CFalse
  val negate : Constraint.Constraint.cexp -> Constraint.Constraint.cexp
  val mkEqs :
    Constraint.Constraint.cexp ->
    Constraint.Constraint.cexp -> Constraint.Constraint.cexp
  val mkVar : string -> Constraint.Constraint.cexp
  val mkRVar : string -> string -> int -> Constraint.Constraint.cexp
end