Fixpoint3.Ast.Ram.BoolExp
enum BoolExpSourcecase Not(BoolExp)case IsEmpty(RelSym)case NotMemberOf(Vector[RamTerm], RelSym, Bool)case NotBot(RamTerm, Boxed -> (Boxed -> Bool), Boxed)case Leq(Boxed, RowVar, RelSym)case Eq(RamTerm, RamTerm)case Guard1(Boxed -> Bool, RamTerm)case Guard2(Boxed -> (Boxed -> Bool), RamTerm, RamTerm)case Guard3(Boxed -> (Boxed -> (Boxed -> Bool)), RamTerm, RamTerm, RamTerm)case Guard4(Boxed -> (Boxed -> (Boxed -> (Boxed -> Bool))), RamTerm, RamTerm, RamTerm, RamTerm)case Guard5(Boxed -> (Boxed -> (Boxed -> (Boxed -> (Boxed -> Bool)))), RamTerm, RamTerm, RamTerm, RamTerm, RamTerm)Not(b): True if b is false.
IsEmpty(relSym): True if there are no facts in relation relSym.
NotMemberOf(terms, relSym, repNegative): True if the tuple constructed from terms is not
in relation relSym. repNegative is true if NotMemberOf is introduced by a not A(...).
NotBot(term, leq, bot): True if term is not a bot.
term must be a Meet or RowLoad of a lattice var.
Leq(const, rv, relSym): True if const is less than the lattice element of rv.
Eq(term1, term2): True if term1 == term2.
Guard1(f, term1): True if f(term1) == true.
Guard2(f, term1, term2): True if f(term1, term2) == true.
Guard3(f, term1, term2, term3): True if f(term1, term2, term3) == true.
Guard4(f, term1, term2, term3, term4): True if f(term1, term2, term3, term4) == true.
Guard5(f, term1, term2, term3, term4, term5): True if f(term1, term2, term3, term4, term5) == true.