(**************************************************************************) (* *) (* SMTCoq *) (* Copyright (C) 2011 - 2022 *) (* *) (* See file "AUTHORS" for the list of authors *) (* *) (* This file is distributed under the terms of the CeCILL-C licence *) (* *) (**************************************************************************) open Ast module H = struct let mp_add = Hstring.make "mp_add" let mp_mul = Hstring.make "mp_mul" let mp_is_neg = Hstring.make "mp_is_neg" let mp_is_zero = Hstring.make "mp_is_zero" let uminus = Hstring.make "~" let bool_lfsc = Hstring.make "bool_lfsc" let tt = Hstring.make "tt" let ff = Hstring.make "ff" let var = Hstring.make "var" let lit = Hstring.make "lit" let clause = Hstring.make "clause" let cln = Hstring.make "cln" let okay = Hstring.make "okay" let ok = Hstring.make "ok" let pos = Hstring.make "pos" let neg = Hstring.make "neg" let clc = Hstring.make "clc" let concat_cl = Hstring.make "concat_cl" let clr = Hstring.make "clr" let formula = Hstring.make "formula" let not_ = Hstring.make "not" let and_ = Hstring.make "and" let or_ = Hstring.make "or" let impl_ = Hstring.make "impl" let iff_ = Hstring.make "iff" let xor_ = Hstring.make "xor" let ifte_ = Hstring.make "ifte" let ite = Hstring.make "ite" let iff = Hstring.make "iff" let flet = Hstring.make "flet" let impl = Hstring.make "impl" let gt_Int = Hstring.make ">_Int" let ge_Int = Hstring.make ">=_Int" let lt_Int = Hstring.make "<_Int" let le_Int = Hstring.make "<=_Int" let plus_Int = Hstring.make "+_Int" let minus_Int = Hstring.make "-_Int" let times_Int = Hstring.make "*_Int" let div_Int = Hstring.make "/_Int" let uminus_Int = Hstring.make "u-_Int" let sort = Hstring.make "sort" let term = Hstring.make "term" let tBool = Hstring.make "Bool" let p_app = Hstring.make "p_app" let arrow = Hstring.make "arrow" let apply = Hstring.make "apply" let bitVec = Hstring.make "BitVec" let bit = Hstring.make "bit" let b0 = Hstring.make "b0" let b1 = Hstring.make "b1" let bv = Hstring.make "bv" let bvn = Hstring.make "bvn" let bvc = Hstring.make "bvc" let bblt = Hstring.make "bblt" let bbltn = Hstring.make "bbltn" let bbltc = Hstring.make "bbltc" let var_bv = Hstring.make "var_bv" (* let a_var_bv = Hstring.make "a_var_bv" *) let a_bv = Hstring.make "a_bv" let a_int = Hstring.make "a_int" let bitof = Hstring.make "bitof" let bblast_term = Hstring.make "bblast_term" (* let eq = Hstring.make "=" *) let bvand = Hstring.make "bvand" let bvor = Hstring.make "bvor" let bvxor = Hstring.make "bvxor" let bvnand = Hstring.make "bvnand" let bvnor = Hstring.make "bvnor" let bvxnor = Hstring.make "bvxnor" let bvmul = Hstring.make "bvmul" let bvadd = Hstring.make "bvadd" let bvsub = Hstring.make "bvsub" let bvudiv = Hstring.make "bvudiv" let bvurem = Hstring.make "bvurem" let bvsdiv = Hstring.make "bvsdiv" let bvsrem = Hstring.make "bvsrem" let bvsmod = Hstring.make "bvsmod" let bvshl = Hstring.make "bvshl" let bvlshr = Hstring.make "bvlshr" let bvashr = Hstring.make "bvashr" let bvnot = Hstring.make "bvnot" let bvneg = Hstring.make "bvneg" let bvult = Hstring.make "bvult" let bvslt = Hstring.make "bvslt" let bvule = Hstring.make "bvule" let bvsle = Hstring.make "bvsle" let concat = Hstring.make "concat" let extract = Hstring.make "extract" let zero_extend = Hstring.make "zero_extend" let sign_extend = Hstring.make "sign_extend" let array = Hstring.make "Array" let read = Hstring.make "read" let write = Hstring.make "write" let diff = Hstring.make "diff" let append = Hstring.make "append" let simplify_clause = Hstring.make "simplify_clause" let bv_constants_are_disequal = Hstring.make "bv_constants_are_disequal" let bblt_len = Hstring.make "bblt_len" let bblast_const = Hstring.make "bblast_const" let bblast_var = Hstring.make "bblast_var" let bblast_concat = Hstring.make "bblast_concat" let bblast_extract = Hstring.make "bblast_extract" let bblast_zextend = Hstring.make "bblast_zextend" let bblast_sextend = Hstring.make "bblast_sextend" let bblast_bvand = Hstring.make "bblast_bvand" let bblast_bvnot = Hstring.make "bblast_bvnot" let bblast_bvor = Hstring.make "bblast_bvor" let bblast_bvxor = Hstring.make "bblast_bvxor" let bblast_bvadd = Hstring.make "bblast_bvadd" let bblast_zero = Hstring.make "bblast_zero" let bblast_bvneg = Hstring.make "bblast_bvneg" let bblast_bvmul = Hstring.make "bblast_bvmul" let bblast_eq = Hstring.make "bblast_eq" let bblast_bvult = Hstring.make "bblast_bvult" let bblast_bvslt = Hstring.make "bblast_bvslt" let th_let_pf = Hstring.make "th_let_pf" let th_holds = Hstring.make "th_holds" let ttrue = Hstring.make "true" let tfalse = Hstring.make "false" let a_var_bv = Hstring.make "a_var_bv" let eq = Hstring.make "=" (* let trust_f = Hstring.make "trust_f" *) let ext = Hstring.make "ext" let decl_atom = Hstring.make "decl_atom" let asf = Hstring.make "asf" let ast = Hstring.make "ast" let cong = Hstring.make "cong" let symm = Hstring.make "symm" let negsymm = Hstring.make "negsymm" let trans = Hstring.make "trans" let negtrans = Hstring.make "negtrans" let negtrans1 = Hstring.make "negtrans1" let negtrans2 = Hstring.make "negtrans2" let refl = Hstring.make "refl" let or_elim_1 = Hstring.make "or_elim_1" let or_elim_2 = Hstring.make "or_elim_2" let iff_elim_1 = Hstring.make "iff_elim_1" (* let iff_elim_2 = Hstring.make "iff_elim_2" *) let impl_elim = Hstring.make "impl_elim" let not_and_elim = Hstring.make "not_and_elim" let xor_elim_1 = Hstring.make "xor_elim_1" let xor_elim_2 = Hstring.make "xor_elim_2" let ite_elim_1 = Hstring.make "ite_elim_1" let ite_elim_2 = Hstring.make "ite_elim_2" let ite_elim_3 = Hstring.make "ite_elim_3" let not_ite_elim_1 = Hstring.make "not_ite_elim_1" let not_ite_elim_2 = Hstring.make "not_ite_elim_2" let not_ite_elim_3 = Hstring.make "not_ite_elim_3" let not_iff_elim = Hstring.make "not_iff_elim" let not_xor_elim = Hstring.make "not_xor_elim" let iff_elim_2 = Hstring.make "iff_elim_2" let and_elim_1 = Hstring.make "and_elim_1" let not_impl_elim = Hstring.make "not_impl_elim" let not_or_elim = Hstring.make "not_or_elim" let and_elim_2 = Hstring.make "and_elim_2" let not_not_elim = Hstring.make "not_not_elim" let not_not_intro = Hstring.make "not_not_intro" let pred_eq_t = Hstring.make "pred_eq_t" let pred_eq_f = Hstring.make "pred_eq_f" let trust_f = Hstring.make "trust_f" let tInt = Hstring.make "Int" let eq_transitive = Hstring.make "eq_transitive" let row1 = Hstring.make "row1" let row = Hstring.make "row" let negativerow = Hstring.make "negativerow" let bv_disequal_constants = Hstring.make "bv_disequal_constants" let truth = Hstring.make "truth" let holds = Hstring.make "holds" let q = Hstring.make "Q" let r = Hstring.make "R" let satlem_simplify = Hstring.make "satlem_simplify" let intro_assump_f = Hstring.make "intro_assump_f" let intro_assump_t = Hstring.make "intro_assump_t" let clausify_false = Hstring.make "clausify_false" let trust = Hstring.make "trust" let contra = Hstring.make "contra" let bb_cl = Hstring.make "bb.cl" let satlem = Hstring.make "satlem" let bv_bbl_var = Hstring.make "bv_bbl_var" let bv_bbl_const = Hstring.make "bv_bbl_const" let bv_bbl_bvand = Hstring.make "bv_bbl_bvand" let bv_bbl_bvor = Hstring.make "bv_bbl_bvor" let bv_bbl_bvxor = Hstring.make "bv_bbl_bvxor" let bv_bbl_bvnot = Hstring.make "bv_bbl_bvnot" let bv_bbl_bvneg = Hstring.make "bv_bbl_bvneg" let bv_bbl_bvadd = Hstring.make "bv_bbl_bvadd" let bv_bbl_bvmul = Hstring.make "bv_bbl_bvmul" (* let bv_bbl_bvult = Hstring.make "bv_bbl_bvult" *) (* let bv_bbl_bvslt = Hstring.make "bv_bbl_bvslt" *) let bv_bbl_concat = Hstring.make "bv_bbl_concat" let bv_bbl_extract = Hstring.make "bv_bbl_extract" let bv_bbl_zero_extend = Hstring.make "bv_bbl_zero_extend" let bv_bbl_sign_extend = Hstring.make "bv_bbl_sign_extend" let decl_bblast = Hstring.make "decl_bblast" let decl_bblast_with_alias = Hstring.make "decl_bblast_with_alias" let bv_bbl_eq = Hstring.make "bv_bbl_=" let bv_bbl_eq_swap = Hstring.make "bv_bbl_=_swap" let bv_bbl_bvult = Hstring.make "bv_bbl_bvult" let bv_bbl_bvslt = Hstring.make "bv_bbl_bvslt" end let scope = ref [] let declare_get s = scope := [s]; fun ty -> mk_declare s ty; let c = mk_const s in scope := []; c let define s = scope := [s]; fun t -> mk_define s t; scope := [] let pi n ty = let n = String.concat "." (List.rev (n :: !scope)) in let s = mk_symbol n ty in register_symbol s; fun t -> let pi_abstr = mk_pi s t in remove_symbol s; pi_abstr let pi_d n ty ft = let n = String.concat "." (List.rev (n :: !scope)) in let s = mk_symbol n ty in register_symbol s; let pi_abstr = mk_pi s (ft (symbol_to_const s)) in remove_symbol s; pi_abstr let mp_add_s = declare_get "mp_add" (pi "a" mpz (pi "b" mpz mpz)) let mp_add x y = match value x, value y with | Int xi, Int yi -> mk_mpz (Big_int.add_big_int xi yi) | _ -> mk_app mp_add_s [x; y] let mp_mul_s = declare_get "mp_mul" (pi "a" mpz (pi "b" mpz mpz)) let mp_mul x y = match value x, value y with | Int xi, Int yi -> mk_mpz (Big_int.mult_big_int xi yi) | _ -> mk_app mp_add_s [x; y] let rec eval_arg x = match app_name x with | Some (n, [x; y]) when n == H.mp_add -> mp_add (eval_arg x) (eval_arg y) | Some (n, [x; y]) when n == H.mp_mul -> mp_mul (eval_arg x) (eval_arg y) | _ -> x let mp_isneg x = (* eprintf "mp_isneg %a .@." print_term x; *) match value x with | Int n -> Big_int.sign_big_int n < 0 | _ -> failwith ("mp_isneg") let mp_iszero x = match value x with | Int n -> Big_int.sign_big_int n = 0 | _ -> failwith ("mp_iszero") let uminus = declare_get "~" (pi "a" mpz mpz) let bool_lfsc = declare_get "bool_lfsc" lfsc_type let tt = declare_get "tt" bool_lfsc let ff = declare_get "ff" bool_lfsc let var = declare_get "var" lfsc_type let lit = declare_get "lit" lfsc_type let clause = declare_get "clause" lfsc_type let cln = declare_get "cln" clause let okay = declare_get "okay" lfsc_type let ok = declare_get "ok" okay let pos_s = declare_get "pos" (pi "x" var lit) let neg_s = declare_get "neg" (pi "x" var lit) let clc_s = declare_get "clc" (pi "x" lit (pi "c" clause clause)) let concat_cl_s = declare_get "concat_cl" (pi "c1" clause (pi "c2" clause clause)) let clr_s = declare_get "clr" (pi "l" lit (pi "c" clause clause)) let formula = declare_get "formula" lfsc_type let th_holds_s = declare_get "th_holds" (pi "f" formula lfsc_type) let th_holds f = mk_app th_holds_s [f] let ttrue = declare_get "true" formula let tfalse = declare_get "false" formula (* some definitions *) let _ = define "formula_op1" (pi "f" formula formula); define "formula_op2" (pi "f1" formula (pi "f2" formula formula)); define "formula_op3" (pi "f1" formula (pi "f2" formula (pi "f3" formula formula))) let not_s = declare_get "not" (mk_const "formula_op1") let and_s = declare_get "and" (mk_const "formula_op2") let or_s = declare_get "or" (mk_const "formula_op2") let impl_s = declare_get "impl" (mk_const "formula_op2") let iff_s = declare_get "iff" (mk_const "formula_op2") let xor_s = declare_get "xor" (mk_const "formula_op2") let ifte_s = declare_get "ifte" (mk_const "formula_op3") let sort = declare_get "sort" lfsc_type let term_s = declare_get "term" (pi "t" sort lfsc_type) let term x = mk_app term_s [x] let tBool = declare_get "Bool" sort let p_app_s = declare_get "p_app" (pi "x" (term tBool) formula) let p_app b = mk_app p_app_s [b] let arrow_s = declare_get "arrow" (pi "s1" sort (pi "s2" sort sort)) let arrow s1 s2 = mk_app arrow_s [s1; s2] let apply_s = declare_get "apply" (pi_d "s1" sort (fun s1 -> (pi_d "s2" sort (fun s2 -> (pi "t1" (term (arrow s1 s2)) (pi "t2" (term s1) (term s2))))))) let apply s1 s2 f x = mk_app apply_s [s1; s2; f; x] let eq_s = declare_get "=" (pi_d "s" sort (fun s -> (pi "x" (term s) (pi "y" (term s) formula)))) let eq ty x y = mk_app eq_s [ty; x; y] let pos v = mk_app pos_s [v] let neg v = mk_app neg_s [v] let clc x c = mk_app clc_s [x; c] let clr l c = mk_app clr_s [l; c] let concat_cl c1 c2 = mk_app concat_cl_s [c1; c2] let not_ a = mk_app not_s [a] let and_ a b = mk_app and_s [a; b] let or_ a b = mk_app or_s [a; b] let impl_ a b = mk_app impl_s [a; b] let iff_ a b = mk_app iff_s [a; b] let xor_ a b = mk_app xor_s [a; b] let ifte_ a b c = mk_app ifte_s [a; b; c] (* Bit vector syntax / symbols *) let bitVec_s = declare_get "BitVec" (pi "n" mpz sort) let bitVec n = mk_app bitVec_s [n] let bit = declare_get "bit" lfsc_type let b0 = declare_get "b0" bit let b1 = declare_get "b1" bit let bv = declare_get "bv" lfsc_type let bvn = declare_get "bvn" bv let bvc_s = declare_get "bvc" (pi "b" bit (pi "v" bv bv)) let bvc b v = mk_app bvc_s [b; v] let bblt = declare_get "bblt" lfsc_type let bbltn = declare_get "bbltn" bblt let bbltc_s = declare_get "bbltc" (pi "f" formula (pi "v" bblt bblt)) let bbltc f v = mk_app bbltc_s [f; v] let var_bv = declare_get "var_bv" lfsc_type let a_var_bv_s = declare_get "a_var_bv" (pi_d "n" mpz (fun n -> (pi "v" var_bv (term (bitVec n))))) let a_var_bv n v = mk_app a_var_bv_s [n; v] let a_bv_s = declare_get "a_bv" (pi_d "n" mpz (fun n -> (pi "v" bv (term (bitVec n))))) let a_bv n v = mk_app a_bv_s [n; v] let bitof_s = declare_get "bitof" (pi "x" var_bv (pi "n" mpz formula)) let bitof x n = mk_app bitof_s [x; n] let bblast_term_s = declare_get "bblast_term" (pi_d "n" mpz (fun n -> (pi "x" (term (bitVec n)) (pi "y" bblt lfsc_type)))) let bblast_term n x y = mk_app bblast_term_s [n; x; y] let _ = define "bvop2" (pi_d "n" mpz (fun n -> (pi "x" (term (bitVec n)) (pi "y" (term (bitVec n)) (term (bitVec n)))))) let bvand_s = declare_get "bvand" (mk_const "bvop2") let bvor_s = declare_get "bvor" (mk_const "bvop2") let bvxor_s = declare_get "bvxor" (mk_const "bvop2") let bvnand_s = declare_get "bvnand" (mk_const "bvop2") let bvnor_s = declare_get "bvnor" (mk_const "bvop2") let bvxnor_s = declare_get "bvxnor" (mk_const "bvop2") let bvmul_s = declare_get "bvmul" (mk_const "bvop2") let bvadd_s = declare_get "bvadd" (mk_const "bvop2") let bvsub_s = declare_get "bvsub" (mk_const "bvop2") let bvudiv_s = declare_get "bvudiv" (mk_const "bvop2") let bvurem_s = declare_get "bvurem" (mk_const "bvop2") let bvsdiv_s = declare_get "bvsdiv" (mk_const "bvop2") let bvsrem_s = declare_get "bvsrem" (mk_const "bvop2") let bvsmod_s = declare_get "bvsmod" (mk_const "bvop2") let bvshl_s = declare_get "bvshl" (mk_const "bvop2") let bvlshr_s = declare_get "bvlshr" (mk_const "bvop2") let bvashr_s = declare_get "bvashr" (mk_const "bvop2") let bvand n a b = mk_app bvand_s [n; a; b] let bvor n a b = mk_app bvor_s [n; a; b] let bvxor n a b = mk_app bvxor_s [n; a; b] let bvnand n a b = mk_app bvnand_s [n; a; b] let bvnor n a b = mk_app bvnor_s [n; a; b] let bvxnor n a b = mk_app bvxnor_s [n; a; b] let bvmul n a b = mk_app bvmul_s [n; a; b] let bvadd n a b = mk_app bvadd_s [n; a; b] let bvsub n a b = mk_app bvsub_s [n; a; b] let bvudiv n a b = mk_app bvudiv_s [n; a; b] let bvurem n a b = mk_app bvurem_s [n; a; b] let bvsdiv n a b = mk_app bvsdiv_s [n; a; b] let bvsrem n a b = mk_app bvsrem_s [n; a; b] let bvsmod n a b = mk_app bvsmod_s [n; a; b] let bvshl n a b = mk_app bvshl_s [n; a; b] let bvlshr n a b = mk_app bvlshr_s [n; a; b] let bvashr n a b = mk_app bvashr_s [n; a; b] let _ = define "bvop1" (pi_d "n" mpz (fun n -> (pi "x" (term (bitVec n)) (term (bitVec n))))) let bvnot_s = declare_get "bvnot" (mk_const "bvop1") let bvneg_s = declare_get "bvneg" (mk_const "bvop1") let bvnot n a = mk_app bvnot_s [n; a] let bvneg n a = mk_app bvneg_s [n; a] let _ = define "bvpred" (pi_d "n" mpz (fun n -> (pi "x" (term (bitVec n)) (pi "y" (term (bitVec n)) formula)))) let bvult_s = declare_get "bvult" (mk_const "bvpred") let bvslt_s = declare_get "bvslt" (mk_const "bvpred") let bvult n a b = mk_app bvult_s [n; a; b] let bvslt n a b = mk_app bvslt_s [n; a; b] let concat_s = declare_get "concat" (pi_d "n" mpz (fun n -> (pi_d "m" mpz (fun m -> (pi_d "m'" mpz (fun m' -> (pi "t1" (term (bitVec m)) (pi "t2" (term (bitVec m')) (term (bitVec n)))))))))) let concat n m m' a b = mk_app concat_s [n; m; m'; a; b] let extract_s = declare_get "extract" (pi_d "n" mpz (fun n -> (pi "i" mpz (pi "j" mpz (pi_d "m" mpz (fun m -> (pi "t2" (term (bitVec m)) (term (bitVec n))))))))) let extract n i j m b = mk_app extract_s [n; i; j; m; b] let zero_extend_s = declare_get "zero_extend" (pi_d "n" mpz (fun n -> (pi "i" mpz (pi_d "m" mpz (fun m -> (pi "t2" (term (bitVec m)) (term (bitVec n)))))))) let zero_extend n i m b = mk_app zero_extend_s [n; i; m; b] let sign_extend_s = declare_get "sign_extend" (pi_d "n" mpz (fun n -> (pi "i" mpz (pi_d "m" mpz (fun m -> (pi "t2" (term (bitVec m)) (term (bitVec n)))))))) let sign_extend n i m b = mk_app sign_extend_s [n; i; m; b] (* arrays constructors and functions *) let array_s = declare_get "Array" (pi "s1" sort (pi "s2" sort sort)) let array s1 s2 = mk_app array_s [s1; s2] let read_s = declare_get "read" (pi_d "s1" sort (fun s1 -> (pi_d "s2" sort (fun s2 -> (term (arrow (array s1 s2) (arrow s1 s2))))))) let read s1 s2 = mk_app read_s [s1; s2] let write_s = declare_get "write" (pi_d "s1" sort (fun s1 -> (pi_d "s2" sort (fun s2 -> (term (arrow (array s1 s2) (arrow s1 (arrow s2 (array s1 s2))))))))) let write s1 s2 = mk_app write_s [s1; s2] let diff_s = declare_get "diff" (pi_d "s1" sort (fun s1 -> (pi_d "s2" sort (fun s2 -> (term (arrow (array s1 s2) (arrow (array s1 s2) s1))))))) let diff s1 s2 = mk_app diff_s [s1; s2] (* sortcuts *) let apply_read s1 s2 a i = apply s1 s2 (apply (array s1 s2) (arrow s1 s2) (read s1 s2) a) i let apply_write s1 s2 a i v = apply s2 (array s1 s2) (apply s1 (arrow s2 (array s1 s2)) (apply (array s1 s2) (arrow s1 (arrow s2 (array s1 s2))) (write s1 s2) a) i) v let apply_diff s1 s2 a b = apply (array s1 s2) s1 (apply (array s1 s2) (arrow (array s1 s2) s1) (diff s1 s2) a) b let refl_s = declare_get "refl" (pi_d "s" sort (fun s -> (pi_d "t" (term s) (fun t -> (th_holds (eq s t t)))))) let refl s t = mk_app refl_s [s; t] let cong_s = declare_get "cong" (pi_d "s1" sort (fun s1 -> (pi_d "s2" sort (fun s2 -> (pi_d "a1" (term (arrow s1 s2)) (fun a1 -> (pi_d "b1" (term (arrow s1 s2)) (fun b1 -> (pi_d "a2" (term s1) (fun a2 -> (pi_d "b2" (term s1) (fun b2 -> (pi_d "u1" (th_holds (eq (arrow s1 s2) a1 b1)) (fun u1 -> (pi_d "u2" (th_holds (eq s1 a2 b2)) (fun u2 -> (th_holds (eq s2 (apply s1 s2 a1 a2) (apply s1 s2 b1 b2))))))))))))))))))) let cong s1 s2 a1 b1 a2 b2 u1 u2 = mk_app cong_s [s1; s2; a1; b1; a2; b2; u1; u2] module MInt = Map.Make (struct type t = int let compare = Stdlib.compare end) module STerm = Set.Make (Term) type mark_map = STerm.t MInt.t let empty_marks = MInt.empty let is_marked i m v = try STerm.mem v (MInt.find i m) with Not_found -> false let if_marked_do i m v then_v else_v = if is_marked i m v then (then_v m) else (else_v m) let markvar_with i m v = let set = try MInt.find i m with Not_found -> STerm.empty in MInt.add i (STerm.add v set) m let ifmarked m v = if_marked_do 1 m v let ifmarked1 m v = ifmarked m v let ifmarked2 m v = if_marked_do 2 m v let ifmarked3 m v = if_marked_do 3 m v let ifmarked4 m v = if_marked_do 4 m v let markvar m v = markvar_with 1 m v let markvar1 m v = markvar m v let markvar2 m v = markvar_with 2 m v let markvar3 m v = markvar_with 3 m v let markvar4 m v = markvar_with 4 m v (*******************) (* Side conditions *) (*******************) let rec append c1 c2 = match value c1 with | Const _ when term_equal c1 cln -> c2 | App (f, [l; c1']) when term_equal f clc_s -> clc l (append c1' c2) | _ -> failwith "Match failure" (* we use marks as follows: - mark 1 to record if we are supposed to remove a positive occurrence of the variable. - mark 2 to record if we are supposed to remove a negative occurrence of the variable. - mark 3 if we did indeed remove the variable positively - mark 4 if we did indeed remove the variable negatively *) let rec simplify_clause mark_map c = (* eprintf "simplify_clause[rec] %a@." print_term c; *) match value c with | Const _ when term_equal c cln -> cln, mark_map | App(f, [l; c1]) when term_equal f clc_s -> begin match value l with (* Set mark 1 on v if it is not set, to indicate we should remove it. After processing the rest of the clause, set mark 3 if we were already supposed to remove v (so if mark 1 was set when we began). Clear mark3 if we were not supposed to be removing v when we began this call. *) | App (f, [v]) when term_equal f pos_s -> let v = deref v in let m, mark_map = ifmarked mark_map v (fun mark_map -> tt, mark_map) (fun mark_map -> ff, markvar mark_map v) in let c', mark_map = simplify_clause mark_map c1 in begin match value m with | Const _ when term_equal m tt -> let mark_map = ifmarked3 mark_map v (fun mark_map -> mark_map) (fun mark_map -> markvar3 mark_map v) in c', mark_map | Const _ when term_equal m ff -> let mark_map = ifmarked3 mark_map v (fun mark_map -> markvar3 mark_map v) (fun mark_map -> mark_map) in let mark_map = markvar mark_map v in clc l c', mark_map | _ -> failwith "Match failure1" end | App (f, [v]) when term_equal f neg_s -> let v = deref v in let m, mark_map = ifmarked2 mark_map v (fun mark_map -> tt, mark_map) (fun mark_map -> ff, markvar2 mark_map v) in let c', mark_map = simplify_clause mark_map c1 in begin match value m with | Const _ when term_equal m tt -> let mark_map = ifmarked4 mark_map v (fun mark_map -> mark_map) (fun mark_map -> markvar4 mark_map v) in c', mark_map | Const _ when term_equal m ff -> let mark_map = ifmarked4 mark_map v (fun mark_map -> markvar4 mark_map v) (fun mark_map -> mark_map) in let mark_map = markvar2 mark_map v in clc l c', mark_map | _ -> failwith "Match failure2" end | _ -> failwith "Match failure3" end | App(f, [c1; c2]) when term_equal f concat_cl_s -> let new_c1, mark_map = simplify_clause mark_map c1 in let new_c2, mark_map = simplify_clause mark_map c2 in append new_c1 new_c2, mark_map | App(f, [l; c1]) when term_equal f clr_s -> begin match value l with (* set mark 1 to indicate we should remove v, and fail if mark 3 is not set after processing the rest of the clause (we will set mark 3 if we remove a positive occurrence of v). *) | App (f, [v]) when term_equal f pos_s -> let v = deref v in let m, mark_map = ifmarked mark_map v (fun mark_map -> tt, mark_map) (fun mark_map -> ff, markvar mark_map v) in let m3, mark_map = ifmarked3 mark_map v (fun mark_map -> tt, markvar3 mark_map v) (fun mark_map -> ff, mark_map) in let c', mark_map = simplify_clause mark_map c1 in let mark_map = ifmarked3 mark_map v (fun mark_map -> let mark_map = match value m3 with | Const _ when term_equal m3 tt -> mark_map | Const _ when term_equal m3 ff -> markvar3 mark_map v | _ -> failwith "Match failure4" in let mark_map = match value m with | Const _ when term_equal m tt -> mark_map | Const _ when term_equal m ff -> markvar mark_map v | _ -> failwith "Match failure5" in mark_map ) (fun _ -> failwith "Match failure6") in c', mark_map | App (f, [v]) when term_equal f neg_s -> let v = deref v in let m2, mark_map = ifmarked2 mark_map v (fun mark_map -> tt, mark_map) (fun mark_map -> ff, markvar2 mark_map v) in let m4, mark_map = ifmarked4 mark_map v (fun mark_map -> tt, markvar4 mark_map v) (fun mark_map -> ff, mark_map) in let c', mark_map = simplify_clause mark_map c1 in let mark_map = ifmarked4 mark_map v (fun mark_map -> let mark_map = match value m4 with | Const _ when term_equal m4 tt -> mark_map | Const _ when term_equal m4 ff -> markvar4 mark_map v | _ -> failwith "Match failure7" in let mark_map = match value m2 with | Const _ when term_equal m2 tt -> mark_map | Const _ when term_equal m2 ff -> markvar2 mark_map v | _ -> failwith "Match failure8" in mark_map ) (fun _ -> failwith "Match failure9") in c', mark_map | _ -> failwith "Match failure10" end | _ -> failwith "Match failure11" let simplify_clause c = let c', _ = simplify_clause empty_marks c in c' let () = List.iter (fun (s, f) -> Hstring.H.add callbacks_table s f) [ H.append, (function | [c1; c2] -> append c1 c2 | _ -> failwith "append: Wrong number of arguments"); H.simplify_clause, (function | [c] -> simplify_clause c | _ -> failwith "simplify_clause: Wrong number of arguments"); ] let mpz_sub x y = mp_add x (mp_mul (mpz_of_int (-1)) y) let rec bv_constants_are_disequal x y = match value x with | Const _ when term_equal x bvn -> failwith "bv_constants_are_disequal" | App (f, [bx; x']) when term_equal f bvc_s -> (match value y with | Const _ when term_equal y bvn -> failwith "bv_constants_are_disequal" | App (f, [by; y']) when term_equal f bvc_s -> if term_equal bx b0 then if term_equal by b0 then bv_constants_are_disequal x' y' else ttrue else if term_equal bx b1 then if term_equal by b1 then bv_constants_are_disequal x' y' else ttrue else failwith "bv_constants_are_disequal" | _ -> failwith "bv_constants_are_disequal") | _ -> failwith "bv_constants_are_disequal" (* calculate the length of a bit-blasted term *) let rec bblt_len v = (* eprintf "bblt_len %a@." print_term v; *) match value v with | Const _ when term_equal v bbltn -> mpz_of_int 0 | App (f, [b; v']) when term_equal f bbltc_s -> mp_add (bblt_len v') (mpz_of_int 1) | _ -> failwith "bblt_len" let rec bblast_const v n = if mp_isneg n then match value v with | Const _ when term_equal v bvn -> bbltn | _ -> failwith "blast_const" else match value v with | App (f, [b; v']) when term_equal f bvc_s -> bbltc (match value b with | Const _ when term_equal b b0 -> tfalse | Const _ when term_equal b b1 -> ttrue | _ -> failwith "bblast_const") (bblast_const v' (mp_add n (mpz_of_int (-1)))) | _ -> failwith "bblast_const" let rec bblast_var x n = if mp_isneg n then bbltn else bbltc (bitof x n) (bblast_var x (mp_add n (mpz_of_int (-1)))) let rec bblast_concat x y = match value x with | Const _ when term_equal x bbltn -> (match value y with | App (f, [by; y']) when term_equal f bbltc_s -> bbltc by (bblast_concat x y') | Const _ when term_equal y bbltn -> bbltn | _ -> failwith "bblast_concat: wrong application") | App (f, [bx; x']) when term_equal f bbltc_s -> bbltc bx (bblast_concat x' y) | _ -> failwith "bblast_concat: wrong application" let rec bblast_extract_rec x i j n = match value x with | App (f, [bx; x']) when term_equal f bbltc_s -> if mp_isneg (mpz_sub (mpz_sub j n) (mpz_of_int 1)) then if mp_isneg (mpz_sub (mpz_sub n i) (mpz_of_int 1)) then bbltc bx (bblast_extract_rec x' i j (mpz_sub n (mpz_of_int 1))) else bblast_extract_rec x' i j (mpz_sub n (mpz_of_int 1)) else bbltn | Const _ when term_equal x bbltn -> bbltn | _ -> failwith "bblast_extract_rec: wrong application" let bblast_extract x i j n = bblast_extract_rec x i j (mpz_sub n (mpz_of_int 1)) let rec extend_rec x i b = if mp_isneg i then x else bbltc b (extend_rec x (mpz_sub i (mpz_of_int 1)) b) let bblast_zextend x i = extend_rec x (mpz_sub i (mpz_of_int 1)) tfalse let bblast_sextend x i = match value x with | App (f, [xb; x']) when term_equal f bbltc_s -> extend_rec x (mpz_sub i (mpz_of_int 1)) xb | _ -> failwith "bblast_sextend" let rec bblast_bvand x y = (* eprintf "bblast_bvand %a %a@." print_term x print_term y; *) match value x with | Const _ when term_equal x bbltn -> (match value y with | Const _ when term_equal y bbltn -> bbltn | _ -> failwith "bblast_bvand1") | App (f, [bx; x']) when term_equal f bbltc_s -> (match value y with | App (f, [by; y']) when term_equal f bbltc_s -> bbltc (and_ bx by) (bblast_bvand x' y') | _ -> failwith "bblast_bvand2") | _ -> failwith "bblast_bvand3" let rec bblast_bvnot x = match value x with | Const _ when term_equal x bbltn -> bbltn | App (f, [bx; x']) when term_equal f bbltc_s -> bbltc (not_ bx) (bblast_bvnot x') | _ -> failwith "bblast_bnot" let rec bblast_bvor x y = match value x with | Const _ when term_equal x bbltn -> (match value y with | Const _ when term_equal y bbltn -> bbltn | _ -> failwith "bblast_bvor") | App (f, [bx; x']) when term_equal f bbltc_s -> (match value y with | App (f, [by; y']) when term_equal f bbltc_s -> bbltc (or_ bx by) (bblast_bvor x' y') | _ -> failwith "bblast_bvor") | _ -> failwith "bblast_bvor" let rec bblast_bvxor x y = match value x with | Const _ when term_equal x bbltn -> (match value y with | Const _ when term_equal y bbltn -> bbltn | _ -> failwith "bblast_bvxor") | App (f, [bx; x']) when term_equal f bbltc_s -> (match value y with | App (f, [by; y']) when term_equal f bbltc_s -> bbltc (xor_ bx by) (bblast_bvxor x' y') | _ -> failwith "bblast_bvxor") | _ -> failwith "bblast_bvxor" (* ;; return the carry bit after adding x y ;; FIXME: not the most efficient thing in the world *) let rec bblast_bvadd_carry a b carry = match value a with | Const _ when term_equal a bbltn -> (match value b with | Const _ when term_equal b bbltn -> carry | _ -> failwith "bblast_bvadd_carry") | App (f, [ai; a']) when term_equal f bbltc_s -> (match value b with | App (f, [bi; b']) when term_equal f bbltc_s -> (or_ (and_ ai bi) (and_ (xor_ ai bi) (bblast_bvadd_carry a' b' carry))) | _ -> failwith "bblast_bvadd_carry") | _ -> failwith "bblast_bvadd_carry" let rec bblast_bvadd a b carry = match value a with | Const _ when term_equal a bbltn -> (match value b with | Const _ when term_equal b bbltn -> bbltn | _ -> failwith "bblast_bvadd") | App (f, [ai; a']) when term_equal f bbltc_s -> (match value b with | App (f, [bi; b']) when term_equal f bbltc_s -> bbltc (xor_ (xor_ ai bi) (bblast_bvadd_carry a' b' carry)) (bblast_bvadd a' b' carry) | _ -> failwith "bblast_bvadd") | _ -> failwith "bblast_bvadd" let rec bblast_zero n = if mp_iszero n then bbltn else bbltc tfalse (bblast_zero (mp_add n (mpz_of_int (-1)))) let bblast_bvneg x n = bblast_bvadd (bblast_bvnot x) (bblast_zero n) ttrue let rec reverse_help x acc = match value x with | Const _ when term_equal x bbltn -> acc | App (f, [xi; x']) when term_equal f bbltc_s -> reverse_help x' (bbltc xi acc) | _ -> failwith "reverse_help" let reverseb x = reverse_help x bbltn let rec top_k_bits a k = if mp_iszero k then bbltn else match value a with | App (f, [ai; a']) when term_equal f bbltc_s -> bbltc ai (top_k_bits a' (mpz_sub k (mpz_of_int 1))) | _ -> failwith "top_k_bits" let bottom_k_bits a k = reverseb (top_k_bits (reverseb a) k) (* assumes the least signigicant bit is at the beginning of the list *) let rec k_bit a k = if mp_isneg k then failwith "k_bit" else match value a with | App (f, [ai; a']) when term_equal f bbltc_s -> if mp_iszero k then ai else k_bit a' (mpz_sub k (mpz_of_int 1)) | _ -> failwith "k_bit" let rec and_with_bit a bt = match value a with | Const _ when term_equal a bbltn -> bbltn | App (f, [ai; a']) when term_equal f bbltc_s -> bbltc (and_ bt ai) (and_with_bit a' bt) | _ -> failwith "add_with_bit" (* ;; a is going to be the current result ;; carry is going to be false initially ;; b is the and of a and b[k] ;; res is going to be bbltn initially *) let rec mult_step_k_h a b res carry k = match value a with | Const _ when term_equal a bbltn -> (match value b with | Const _ when term_equal b bbltn -> res | _ -> failwith "mult_step_k_h") | App (f, [ai; a']) when term_equal f bbltc_s -> (match value b with | App (f, [bi; b']) when term_equal f bbltc_s -> if mp_isneg (mpz_sub k (mpz_of_int 1)) then let carry_out = (or_ (and_ ai bi) (and_ (xor_ ai bi) carry)) in let curr = (xor_ (xor_ ai bi) carry) in mult_step_k_h a' b' (bbltc curr res) carry_out (mpz_sub k (mpz_of_int 1)) else mult_step_k_h a' b (bbltc ai res) carry (mpz_sub k (mpz_of_int 1)) | _ -> failwith "mult_step_k_h") | _ -> failwith "mult_step_k_h" (* assumes that a, b and res have already been reversed *) let rec mult_step a b res n k = let k' = mpz_sub n k in let ak = top_k_bits a k' in let b' = and_with_bit ak (k_bit b k) in if mp_iszero (mpz_sub k' (mpz_of_int 1)) then mult_step_k_h res b' bbltn tfalse k else let res' = mult_step_k_h res b' bbltn tfalse k in mult_step a b (reverseb res') n (mp_add k (mpz_of_int 1)) let bblast_bvmul a b n = let ar = reverseb a in (* reverse a and b so that we can build the circuit *) let br = reverseb b in (* from the least significant bit up *) let res = and_with_bit ar (k_bit br (mpz_of_int 0)) in if mp_iszero (mpz_sub n (mpz_of_int 1)) then res else (* if multiplying 1 bit numbers no need to call mult_step *) mult_step ar br res n (mpz_of_int 1) (* ; bit blast x = y ; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1}))) ; f is the accumulator formula that builds the equality in the right order *) let rec bblast_eq_rec x y f = match value x with | Const _ when term_equal x bbltn -> (match value y with | Const _ when term_equal x bbltn -> f | _ -> failwith "bblast_eq_rec") | App (ff, [fx; x']) when term_equal ff bbltc_s -> (match value y with | App (ff, [fy; y']) when term_equal ff bbltc_s -> bblast_eq_rec x' y' (and_ (iff_ fx fy) f) | _ -> failwith "bblast_eq_rec") | _ -> failwith "bblast_eq_rec" let bblast_eq x y = match value x with | App (ff, [bx; x']) when term_equal ff bbltc_s -> (match value y with | App (ff, [by; y']) when term_equal ff bbltc_s -> bblast_eq_rec x' y' (iff_ bx by) | _ -> failwith "sc1: bblast_eq") | _ -> failwith "sc2: bblast_eq" let rec bblast_bvult x y n = match value x with | App (ff, [xi; x']) when term_equal ff bbltc_s -> (match value y with | App (ff, [yi; y']) when term_equal ff bbltc_s -> if mp_iszero n then (and_ (not_ xi) yi) else (or_ (and_ (iff_ xi yi) (bblast_bvult x' y' (mp_add n (mpz_of_int (-1))))) (and_ (not_ xi) yi)) | _ -> failwith "bblast_bvult") | _ -> failwith "bblast_bvult" let bblast_bvslt x y n = match value x with | App (ff, [xi; x']) when term_equal ff bbltc_s -> (match value y with | App (ff, [yi; y']) when term_equal ff bbltc_s -> if mp_iszero (mpz_sub n (mpz_of_int 1)) then (and_ xi (not_ yi)) else (or_ (and_ (iff_ xi yi) (bblast_bvult x' y' (mpz_sub n (mpz_of_int 2)))) (and_ xi (not_ yi))) | _ -> failwith "bblast_bvslt") | _ -> failwith "bblast_bvslt" let rec mk_ones n = if mp_iszero n then bvn else bvc b1 (mk_ones (mpz_sub n (mpz_of_int 1))) let rec mk_zero n = if mp_iszero n then bvn else bvc b0 (mk_zero (mpz_sub n (mpz_of_int 1))) (** Registering callbacks for side conditions *) let () = List.iter (fun (s, f) -> Hstring.H.add callbacks_table s f) [ H.append, (function | [c1; c2] -> append c1 c2 | _ -> failwith "append: Wrong number of arguments"); H.simplify_clause, (function | [c] -> simplify_clause c | _ -> failwith "simplify_clause: Wrong number of arguments"); H.bv_constants_are_disequal, (function | [x; y] -> bv_constants_are_disequal x y | _ -> failwith "bv_constants_are_disequal: Wrong number of arguments"); H.bblt_len, (function | [v] -> bblt_len v | _ -> failwith "bblt_len: Wrong number of arguments"); H.bblast_const, (function | [v; n] -> bblast_const v n | _ -> failwith "bblast_const: Wrong number of arguments"); H.bblast_var, (function | [v; n] -> bblast_var v n | _ -> failwith "bblast_var: Wrong number of arguments"); H.bblast_concat, (function | [x; y] -> bblast_concat x y | _ -> failwith "bblast_concat: Wrong number of arguments"); H.bblast_extract, (function | [x; i; j; n] -> bblast_extract x i j n | _ -> failwith "bblast_extract: Wrong number of arguments"); H.bblast_zextend, (function | [x; i] -> bblast_zextend x i | _ -> failwith "bblast_zextend: Wrong number of arguments"); H.bblast_sextend, (function | [x; i] -> bblast_sextend x i | _ -> failwith "bblast_sextend: Wrong number of arguments"); H.bblast_bvand, (function | [x; y] -> bblast_bvand x y | _ -> failwith "bblast_bvand: Wrong number of arguments"); H.bblast_bvnot, (function | [x] -> bblast_bvnot x | _ -> failwith "bblast_bvnot: Wrong number of arguments"); H.bblast_bvor, (function | [x; y] -> bblast_bvor x y | _ -> failwith "bblast_bvor: Wrong number of arguments"); H.bblast_bvxor, (function | [x; y] -> bblast_bvxor x y | _ -> failwith "bblast_bvxor: Wrong number of arguments"); H.bblast_bvadd, (function | [x; y; c] -> bblast_bvadd x y c | _ -> failwith "bblast_bvadd: Wrong number of arguments"); H.bblast_zero, (function | [n] -> bblast_zero n | _ -> failwith "bblast_zero: Wrong number of arguments"); H.bblast_bvneg, (function | [v; n] -> bblast_bvneg v n | _ -> failwith "bblast_bvneg: Wrong number of arguments"); H.bblast_bvmul, (function | [x; y; n] -> bblast_bvmul x y n | _ -> failwith "bblast_bvmul: Wrong number of arguments"); H.bblast_eq, (function | [x; y] -> bblast_eq x y | _ -> failwith "bblast_eq: Wrong number of arguments"); H.bblast_bvult, (function | [x; y; n] -> bblast_bvult x y n | _ -> failwith "bblast_bvult: Wrong number of arguments"); H.bblast_bvslt, (function | [x; y; n] -> bblast_bvslt x y n | _ -> failwith "bblast_bvslt: Wrong number of arguments"); ]