Lines Matching defs:literal
29 type literal = int (* a possibly negated variable index, must be <> 0 *)
31 datatype extension = ITE of literal * literal * literal
32 | AND of literal list
34 type resolution = literal list * cindex list
38 * (vindex, literal) Redblackmap.dict
63 (* literal list -> string list -> literal list *)
72 | extension_lits lits (literal :: xs) =
73 extension_lits (int_from_string literal :: lits) xs
94 (* literal list -> string list -> resolution *)
112 (* (vindex, literal) dict -> string list -> (vindex, literal) dict *)
115 | valid_conclusion dict (vindex :: literal :: xs) =
117 (dict, int_from_string vindex, int_from_string literal)) xs
120 "vindex/literal pair expected in conclusion"
258 (* lit processes a literal l, accumulating dependencies in s.
263 vk is passed the literal of the witness,