fact: Definition build_hform vm f : option (vmap*(BFormula (Formula Z) isProp)) := match f with | Form.Fatom h => match build_formula vm h with | Some (vm,f) => Some (vm, A isProp f tt) | None => None end | Form.Ftrue => Some (vm, TT isProp) | Form.Ffalse => Some (vm, FF isProp) | Form.Fnot2 i l => match build_var vm (Lit.blit l) with | Some (vm, f) => let f' := build_not2 i f in let f'' := if Lit.is_pos l then f' else NOT f' in Some (vm,f'') | None => None end | Form.Fand args => afold_left _ (fun vm => Some (vm, TT isProp)) (fun a b vm => match a vm with | Some (vm1, f1) => match b vm1 with | Some (vm2, f2) => Some (vm2, AND f1 f2) | None => None end | None => None end) (amap (fun l vm => match build_var vm (Lit.blit l) with | Some (vm', f) => Some (vm', if Lit.is_pos l then f else NOT f) | None => None end) args) vm | Form.For args => afold_left _ (fun vm => Some (vm, FF isProp)) (fun a b vm => match a vm with | Some (vm1, f1) => match b vm1 with | Some (vm2, f2) => Some (vm2, OR f1 f2) | None => None end | None => None end) (amap (fun l vm => match build_var vm (Lit.blit l) with | Some (vm', f) => Some (vm', if Lit.is_pos l then f else NOT f) | None => None end) args) vm | Form.Fxor a b => match build_var vm (Lit.blit a) with | Some (vm1, f1) => match build_var vm1 (Lit.blit b) with | Some (vm2, f2) => let f1' := if Lit.is_pos a then f1 else NOT f1 in let f2' := if Lit.is_pos b then f2 else NOT f2 in Some (vm2, AND (OR f1' f2') (OR (NOT f1') (NOT f2'))) | None => None end | None => None end | Form.Fimp args => afold_right _ (fun vm => Some (vm, TT isProp)) (fun a b vm => match b vm with | Some (vm2, f2) => match a vm2 with | Some (vm1, f1) => Some (vm1, IMPL f1 None f2) | None => None end | None => None end) (amap (fun l vm => match build_var vm (Lit.blit l) with | Some (vm', f) => Some (vm', if Lit.is_pos l then f else NOT f) | None => None end) args) vm | Form.Fiff a b => match build_var vm (Lit.blit a) with | Some (vm1, f1) => match build_var vm1 (Lit.blit b) with | Some (vm2, f2) => let f1' := if Lit.is_pos a then f1 else NOT f1 in let f2' := if Lit.is_pos b then f2 else NOT f2 in Some (vm2, AND (OR f1' (NOT f2')) (OR (NOT f1') f2')) | None => None end | None => None end | Form.Fite a b c => match build_var vm (Lit.blit a) with | Some (vm1, f1) => match build_var vm1 (Lit.blit b) with | Some (vm2, f2) => match build_var vm2 (Lit.blit c) with | Some (vm3, f3) => let f1' := if Lit.is_pos a then f1 else NOT f1 in let f2' := if Lit.is_pos b then f2 else NOT f2 in let f3' := if Lit.is_pos c then f3 else NOT f3 in Some (vm3, OR (AND f1' f2') (AND (NOT f1') f3')) | None => None end | None => None end | None => None end | Form.FbbT _ _ => None end.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz