structure Cvc.Actlit : Type

• mk' :: (
• getTerm : Formula
• )

instance Cvc.Actlit.instCoeFormula : Coe Actlit Formula

Equations

• Cvc.Actlit.instCoeFormula = { coe := Cvc.Actlit.getTerm }

structure Cvc.Actlit.Ident : Type

• mk' :: (
• getIdent : String
• )

def Cvc.Actlit.Ident.reservedPref : String

Equations

• Cvc.Actlit.Ident.reservedPref = "__cvc_reserved_actlit_"

def Cvc.Actlit.Ident.identOfIdx (idx : Nat) (desc : String := "") : String

Equations

• Cvc.Actlit.Ident.identOfIdx idx desc = toString "" ++ toString Cvc.Actlit.Ident.reservedPref ++ toString "" ++ toString desc ++ toString "_" ++ toString idx ++ toString ""

def Cvc.Actlit.Ident.ofIdx (idx : Nat) (desc : String := "") : Actlit.Ident

Equations

• Cvc.Actlit.Ident.ofIdx idx desc = { getIdent := Cvc.Actlit.Ident.identOfIdx idx desc }

instance Cvc.Actlit.Ident.instCoeString : Coe Actlit.Ident String

Equations

• Cvc.Actlit.Ident.instCoeString = { coe := Cvc.Actlit.Ident.getIdent }

instance Cvc.Actlit.Ident.instToString : ToString Actlit.Ident

Equations

• Cvc.Actlit.Ident.instToString = { toString := Cvc.Actlit.Ident.getIdent }

def Cvc.Actlit.Ident.declare (ident : Actlit.Ident) : Smt Actlit

Equations

• ident.declare = do let __do_lift ← Cvc.Smt.declare ident.getIdent Bool pure { getTerm := __do_lift }

def Cvc.Actlit.ofIdx (idx : Nat) (desc : String := "") : Smt Actlit

Equations

• Cvc.Actlit.ofIdx idx desc = (Cvc.Actlit.Ident.ofIdx idx desc).declare

def Cvc.Actlit.isActlitIdent (s : String) : Bool

Equations

• Cvc.Actlit.isActlitIdent s = s.startsWith Cvc.Actlit.Ident.reservedPref

def Cvc.Actlit.isActlitTerm (term : Formula) : Bool

Equations

• Cvc.Actlit.isActlitTerm term = (Option.map Cvc.Actlit.isActlitIdent (Cvc.Term.getSymbol? term)).getD false

def Cvc.Actlit.fresh (desc : String := "") : Smt Actlit

Equations

• Cvc.Actlit.fresh desc = do let x ← Cvc.Smt.nextActlitIdx Cvc.Actlit.ofIdx x desc

def Cvc.Actlit.activate (a : Actlit) (term : Formula) : Smt Unit

Equations

• a.activate term = do let __do_lift ← liftM (Cvc.Term.implies a.getTerm term) Cvc.Smt.assert __do_lift

def Cvc.Actlit.equate (a : Actlit) (term : Formula) : Smt Unit

Equations

• a.equate term = do let __do_lift ← liftM (Cvc.Term.equal a.getTerm term) Cvc.Smt.assert __do_lift

def Cvc.Actlit.deactivate (a : Actlit) : Smt Unit

Equations

• a.deactivate = do let __do_lift ← liftM (Cvc.Term.not a.getTerm) Cvc.Smt.assert __do_lift

def Cvc.Smt.freshActlit : Smt Actlit

Equations

• Cvc.Smt.freshActlit = Cvc.Actlit.fresh

def Cvc.Term.isActlit : Formula → Bool

Equations

• Cvc.Term.isActlit = Cvc.Actlit.isActlitTerm

def Cvc.Formula.isActlit : Formula → Bool

Equations

• Cvc.Formula.isActlit = Cvc.Actlit.isActlitTerm