fact: Definition check_BuildDef l := match get_hash (Lit.blit l) with | Fand args => if Lit.is_pos l then l :: List.map Lit.neg (to_list args) else C._true | For args => if Lit.is_pos l then C._true else l :: to_list args | Fimp args => if Lit.is_pos l then C._true else if PArray.length args =? 0 then C._true else let args := or_of_imp args in l :: to_list args | Fxor a b => if Lit.is_pos l then l::a::Lit.neg b::nil else l::a::b::nil | Fiff a b => if Lit.is_pos l then l::Lit.neg a::Lit.neg b::nil else l::a::Lit.neg b::nil | Fite a b c => if Lit.is_pos l then l::a::Lit.neg c::nil else l::a::c::nil | _ => C._true end.
imports: PArray List Bool ZArith Psatz Misc State SMT_terms BVList