aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace/smtAtom.ml
diff options
context:
space:
mode:
authorckeller <ckeller@users.noreply.github.com>2019-01-28 23:19:12 +0100
committerGitHub <noreply@github.com>2019-01-28 23:19:12 +0100
commit7021c53d4ecf97c82ccebb6bb45f5305d8b482ea (patch)
treeba7537e1e813cabf9ee0d910f845c71fa5f446e7 /src/trace/smtAtom.ml
parent36548d6634864a131cc83ce21491c797163de305 (diff)
downloadsmtcoq-7021c53d4ecf97c82ccebb6bb45f5305d8b482ea.tar.gz
smtcoq-7021c53d4ecf97c82ccebb6bb45f5305d8b482ea.zip
Merge from LFSC (#26)
* Showing models as coq counter examples in tactic without constructing coq terms * also read models when calling cvc4 with a file (deactivated because cvc4 crashes) * Show counter examples with variables in the order they are quantified in the Coq goal * Circumvent issue with ocamldep * fix issue with dependencies * fix issue with dependencies * Translation and OCaml support for extract, zero_extend, sign_extend * Show run times of components * print time on stdout instead * Tests now work with new version (master) of CVC4 * fix small printing issue * look for date on mac os x * proof of valid_check_bbShl: some cases to prove. * full proof of "left shift checker". * full proof of "rigth shift checker". * Support translation of terms bvlshr, bvshl but LFSC rules do not exists at the moment Bug fix for bitvector extract (inverted arguments) * Typo * More modularity on the format of traces depending on the version of coq * More straightforward definitions in Int63Native_standard * Use the Int31 library with coq-8.5 * Use the most efficient operations of Int31 * Improved performance with coq-8.5 * Uniform treatment of sat and smt tactics * Hopefully solved the problem with universes for the tactic * Updated the installation instructions * Holes for unsupported bit blasting rules * Cherry-picking from smtcoq/smtcoq * bug fix hole for bitblast * Predefined arrays are not required anymore * fix issue with coq bbT and bitof construction from ocaml * bug fix in smtAtom for uninterpreted functions fix verit test file * fix issue with smtlib2 extract parsing * It looks like we still need the PArray function instances for some examples (see vmcai_bytes.smt2) * Solver specific reification: Each solver has a list of supported theories which is passed to Atom.of_coq, this function creates uninterpreted functions / sorts for unsupported features. * show counter-examples with const_farray instead of const for constant array definitions * Vernacular commands to debug checkers. Verit/Lfsc_Checker_Debug will always fail, reporting the first proof step of the certificate that failed be checked * Update INSTALL.md * show smtcoq proof when converting * (Hopefully) repared the universes problems * Corrected a bug with holes in proofs * scripts for tests: create a folder "work" under "lfsc/tests/", locate the benchmarks there. create a folder "results" under "lfsc/tests/work/" in which you'll find the results of ./cvc4tocoq. * make sure to give correct path for your benchs... * Checker for array extensionality modulo symmetry of equality * fix oversight with bitvectors larger than 63 bits * some printing functions for smt2 ast * handle smtlib2 files with more complicated equivalence with (= ... ) * revert: ./cvc4tocoq does not output lfsc proofs... * bug fix one input was ignored * Don't show verit translation of LFSC proof if environment variable DONTSHOWVERIT is set (e.g. put export DONTSHOWVERIT="" in your .bashrc or .bashprofile) * Also sort names of introduced variables when showing counter-example * input files for which SMTCoq retuns false. * input files for which SMTCoq retuns false. * use debug checker for debug file * More efficient debug checker * better approximate number of failing step of certificate in debug checker * fix mistake in ml4 * very first attempt to support goals in Prop * bvs: comparison predicates in Prop and their <-> proofs with the ones in bool farrays: equality predicate in Prop and its <-> proof with the one in bool. * unit, Bool, Z, Pos: comparison and equality predicates in Prop. * a typo fixed. * an example of array equality in Prop (converted into Bool by hand)... TODO: enhance the search space of cvc4 tactic. * first version of cvc4' tactic: "solves" the goals in Prop. WARNING: supports only bv and array goals and might not be complete TODO: add support for lia goals * cvc4' support for lia WARNING: might not be complete! * small fix in cvc4' and some variations of examples * small fix + support for goals in Bool and Bool = true + use of solve tactical WARNING: does not support UF and INT63 goals in Prop * cvc4': better arrangement * cvc4': Prop2Bool by context search... * cvc4': solve tactial added -> do not modify unsolved goals. * developer documentation for the smtcoq repo * cvc4': rudimentary support for uninterpreted function goals in Prop. * cvc4': support for goals with Leibniz equality... WARNING: necessary use of "Grab Existential Variables." to instantiate variable types for farrays! * cvc4': Z.lt adapted + better support from verit... * cvc4': support for Z.le, Z.ge, Z.gt. * Try arrays with default value (with a constructor for constant arrays), but extensionality is not provable * cvc4': support for equality over uninterpreted types * lfsc demo: goals in Coq's Prop. * lfsc demo: goals in Bool. * Fix issue with existential variables generated by prop2bool. - prop2bool tactic exported by SMTCoq - remove useless stuff * update usage and installation instructions * Update INSTALL.md * highlighting * the tactic: bool2prop. * clean up * the tactic smt: very first version. * smt: return unsolved goals in Prop. * Show when a certificate cannot be checked when running the tactic instead of at Qed * Tactic improvements - Handle negation/True/False in prop/bool conversions tactic. - Remove alias for farray (this caused problem for matching on this type in tactics). - Tactic `smt` that combines cvc4 and veriT. - return subgoals in prop * test change header * smt: support for negated goals + some reorganization. * conflicts resolved + some reorganization. * a way to solve the issue with ambiguous coercions. * reorganization. * small change. * another small change. * developer documentation of the tactics. * developer guide: some improvements. * developer guide: some more improvements. * developer guide: some more improvements. * developer guide: some more improvements. * pass correct environment for conversion + better error messages * cleaning * ReflectFacts added. * re-organizing developers' guide. * re-organizing developers' guide. * re-organizing developers' guide. * removing unused maps. * headers. * artifact readme getting started... * first attempt * second... * third... * 4th... * 5th... * 6th... * 7th... * 8th... * 9th... * 10th... * 11th... * 12th... * 13th... * 14th... * 15th... * 16th... * 17th... * Update artifact.md Use links to lfsc repository like in the paper * 18th... * 19th... * 20th... * 21st... * 22nd... * 23rd... * 24th... * 25th... * 26th... * 27th... * 28th... * Update artifact.md Small reorganization * minor edits * More minor edits * revised description of tactics * Final pass * typo * name changed: artifact-readme.md * file added... * passwd chaged... * links... * removal * performance statement... * typos... * the link to the artifact image updated... * suggestions by Guy... * aux files removed... * clean-up... * clean-up... * some small changes... * small fix... * additional information on newly created files after running cvc4tocoq script... * some small fix... * another small fix... * typo... * small fix... * another small fix... * fix... * link to the artifact image... * We do not want to force vm_cast for the Theorem commands * no_check variants of the tactics * TODO: a veriT test does not work anymore * Compiles with both versions of Coq * Test of the tactics in real conditions * Comment on this case study * an example for the FroCoS paper. * Fix smt tactic that doesn't return cvc4's subgoals * readme modifications * readme modifications 2 * small typo in readme. * small changes in readme. * small changes in readme. * typo in readme. * Sync with https://github.com/LFSC/smtcoq * Port to Coq 8.6 * README * README * INSTALL * Missing file * Yves' proposition for installation instructions * Updated link to CVC4 * Compiles again with native-coq * Compiles with both versions of Coq * Command to bypass typechecking when generating a zchaff theorem * Solved bug on cuts from Hole * Counter-models for uninterpreted sorts (improves issue #13) * OCaml version note (#15) * update .gitignore * needs OCaml 4.04.0 * Solving merge issues (under progress) * Make SmtBtype compile * Compilation of SmtForm under progress * Make SmtForm compile * Make SmtCertif compile * Make SmtTrace compile * Make SatAtom compile * Make smtAtom compile * Make CnfParser compile * Make Zchaff compile * Make VeritSyntax compile * Make VeritParser compile * Make lfsc/tosmtcoq compile * Make smtlib2_genconstr compile * smtCommand under progress * smtCommands and verit compile again * lfsc compiles * ml4 compiles * Everything compiles * All ZChaff unit tests and most verit unit tests (but taut5 and un_menteur) go through * Most LFSC tests ok; some fail due to the problem of verit; a few fail due to an error "Not_found" to investigate * Authors and headings * Compiles with native-coq * Typo
Diffstat (limited to 'src/trace/smtAtom.ml')
-rw-r--r--src/trace/smtAtom.ml1143
1 files changed, 931 insertions, 212 deletions
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 7ccaa95..6554a8f 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -1,13 +1,9 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2016 *)
+(* Copyright (C) 2011 - 2019 *)
(* *)
-(* Michaël Armand *)
-(* Benjamin Grégoire *)
-(* Chantal Keller *)
-(* *)
-(* Inria - École Polytechnique - Université Paris-Sud *)
+(* See file "AUTHORS" for the list of authors *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
@@ -16,30 +12,58 @@
open SmtMisc
open CoqTerms
+open Entries
+open Declare
+open Decl_kinds
open SmtBtype
+
(** Operators *)
type cop =
- | CO_xH
- | CO_Z0
+ | CO_xH
+ | CO_Z0
+ | CO_BV of bool list
type uop =
- | UO_xO
- | UO_xI
- | UO_Zpos
- | UO_Zneg
- | UO_Zopp
+ | UO_xO
+ | UO_xI
+ | UO_Zpos
+ | UO_Zneg
+ | UO_Zopp
+ | UO_BVbitOf of int * int
+ | UO_BVnot of int
+ | UO_BVneg of int
+ | UO_BVextr of int * int * int
+ | UO_BVzextn of int * int
+ | UO_BVsextn of int * int
type bop =
- | BO_Zplus
- | BO_Zminus
- | BO_Zmult
- | BO_Zlt
- | BO_Zle
- | BO_Zge
- | BO_Zgt
- | BO_eq of btype
+ | BO_Zplus
+ | BO_Zminus
+ | BO_Zmult
+ | BO_Zlt
+ | BO_Zle
+ | BO_Zge
+ | BO_Zgt
+ | BO_eq of btype
+ | BO_BVand of int
+ | BO_BVor of int
+ | BO_BVxor of int
+ | BO_BVadd of int
+ | BO_BVmult of int
+ | BO_BVult of int
+ | BO_BVslt of int
+ | BO_BVconcat of int * int
+ | BO_BVshl of int
+ | BO_BVshr of int
+ | BO_select of btype * btype
+ | BO_diffarray of btype * btype
+
+
+type top =
+ | TO_store of btype * btype
+
type nop =
| NO_distinct of btype
@@ -55,26 +79,35 @@ type index = Index of int
type indexed_op = index * op_def
let destruct s (i, hval) = match i with
- | Index index -> index, hval
- | Rel_name _ -> failwith s
+ | Index index -> index, hval
+ | Rel_name _ -> failwith s
+
+let dummy_indexed_op i dom codom =
+ (i, {tparams = dom; tres = codom; op_val = Term.mkProp})
+
+let indexed_op_index i =
+ let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in
+ index
-let dummy_indexed_op i dom codom = i, {tparams = dom; tres = codom; op_val = Term.mkProp}
-let indexed_op_index i = let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in
- index
+let debruijn_indexed_op i ty =
+ (Index i, {tparams = [||]; tres = ty; op_val = Term.mkRel i})
module Op =
struct
let c_to_coq = function
| CO_xH -> Lazy.force cCO_xH
| CO_Z0 -> Lazy.force cCO_Z0
+ | CO_BV bv -> mklApp cCO_BV [|mk_bv_list bv; mkN (List.length bv)|]
let c_type_of = function
| CO_xH -> Tpositive
| CO_Z0 -> TZ
+ | CO_BV bv -> TBV (List.length bv)
let interp_cop = function
| CO_xH -> Lazy.force cxH
| CO_Z0 -> Lazy.force cZ0
+ | CO_BV bv -> mklApp cof_bits [|mk_bv_list bv|]
let u_to_coq = function
| UO_xO -> Lazy.force cUO_xO
@@ -82,14 +115,29 @@ module Op =
| UO_Zpos -> Lazy.force cUO_Zpos
| UO_Zneg -> Lazy.force cUO_Zneg
| UO_Zopp -> Lazy.force cUO_Zopp
+ | UO_BVbitOf (s, i) -> mklApp cUO_BVbitOf [|mkN s; mkNat i|]
+ | UO_BVnot s -> mklApp cUO_BVnot [|mkN s|]
+ | UO_BVneg s -> mklApp cUO_BVneg [|mkN s|]
+ | UO_BVextr (i, n, s) -> mklApp cUO_BVextr [|mkN i; mkN n; mkN s|]
+ | UO_BVzextn (s, n) -> mklApp cUO_BVzextn [|mkN s; mkN n|]
+ | UO_BVsextn (s, n) -> mklApp cUO_BVsextn [|mkN s; mkN n|]
let u_type_of = function
| UO_xO | UO_xI -> Tpositive
| UO_Zpos | UO_Zneg | UO_Zopp -> TZ
+ | UO_BVbitOf _ -> Tbool
+ | UO_BVnot s | UO_BVneg s -> TBV s
+ | UO_BVextr (_, n, _) -> TBV n
+ | UO_BVzextn (s, n) | UO_BVsextn (s, n) -> TBV (s + n)
let u_type_arg = function
| UO_xO | UO_xI | UO_Zpos | UO_Zneg -> Tpositive
| UO_Zopp -> TZ
+ | UO_BVbitOf (s,_) -> TBV s
+ | UO_BVnot s | UO_BVneg s -> TBV s
+ | UO_BVextr (_, _, s) -> TBV s
+ | UO_BVzextn (s, _) | UO_BVsextn (s, _) -> TBV s
+
let interp_uop = function
| UO_xO -> Lazy.force cxO
@@ -97,8 +145,17 @@ module Op =
| UO_Zpos -> Lazy.force cZpos
| UO_Zneg -> Lazy.force cZneg
| UO_Zopp -> Lazy.force copp
+ | UO_BVbitOf (s,i) -> mklApp cbitOf [|mkN s; mkNat i|]
+ | UO_BVnot s -> mklApp cbv_not [|mkN s|]
+ | UO_BVneg s -> mklApp cbv_neg [|mkN s|]
+ | UO_BVextr (i, n, s) -> mklApp cbv_extr [|mkN i; mkN n; mkN s|]
+ | UO_BVzextn (s, n) -> mklApp cbv_zextn [|mkN s; mkN n|]
+ | UO_BVsextn (s, n) -> mklApp cbv_sextn [|mkN s; mkN n|]
let eq_tbl = Hashtbl.create 17
+ let select_tbl = Hashtbl.create 17
+ let store_tbl = Hashtbl.create 17
+ let diffarray_tbl = Hashtbl.create 17
let eq_to_coq t =
try Hashtbl.find eq_tbl t
@@ -107,6 +164,27 @@ module Op =
Hashtbl.add eq_tbl t op;
op
+ let select_to_coq ti te =
+ try Hashtbl.find select_tbl (ti, te)
+ with Not_found ->
+ let op = mklApp cBO_select [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in
+ Hashtbl.add select_tbl (ti, te) op;
+ op
+
+ let store_to_coq ti te =
+ try Hashtbl.find store_tbl (ti, te)
+ with Not_found ->
+ let op = mklApp cTO_store [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in
+ Hashtbl.add store_tbl (ti, te) op;
+ op
+
+ let diffarray_to_coq ti te =
+ try Hashtbl.find diffarray_tbl (ti, te)
+ with Not_found ->
+ let op = mklApp cBO_diffarray [|SmtBtype.to_coq ti; SmtBtype.to_coq te|] in
+ Hashtbl.add diffarray_tbl (ti, te) op;
+ op
+
let b_to_coq = function
| BO_Zplus -> Lazy.force cBO_Zplus
| BO_Zminus -> Lazy.force cBO_Zminus
@@ -116,23 +194,97 @@ module Op =
| BO_Zge -> Lazy.force cBO_Zge
| BO_Zgt -> Lazy.force cBO_Zgt
| BO_eq t -> eq_to_coq t
+ | BO_BVand s -> mklApp cBO_BVand [|mkN s|]
+ | BO_BVor s -> mklApp cBO_BVor [|mkN s|]
+ | BO_BVxor s -> mklApp cBO_BVxor [|mkN s|]
+ | BO_BVadd s -> mklApp cBO_BVadd [|mkN s|]
+ | BO_BVmult s -> mklApp cBO_BVmult [|mkN s|]
+ | BO_BVult s -> mklApp cBO_BVult [|mkN s|]
+ | BO_BVslt s -> mklApp cBO_BVslt [|mkN s|]
+ | BO_BVconcat (s1, s2) -> mklApp cBO_BVconcat [|mkN s1; mkN s2|]
+ | BO_BVshl s -> mklApp cBO_BVshl [|mkN s|]
+ | BO_BVshr s -> mklApp cBO_BVshr [|mkN s|]
+ | BO_select (ti, te) -> select_to_coq ti te
+ | BO_diffarray (ti, te) -> diffarray_to_coq ti te
let b_type_of = function
| BO_Zplus | BO_Zminus | BO_Zmult -> TZ
- | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt | BO_eq _ -> Tbool
+ | BO_Zlt | BO_Zle | BO_Zge | BO_Zgt | BO_eq _
+ | BO_BVult _ | BO_BVslt _ -> Tbool
+ | BO_BVand s | BO_BVor s | BO_BVxor s | BO_BVadd s | BO_BVmult s
+ | BO_BVshl s | BO_BVshr s -> TBV s
+ | BO_BVconcat (s1, s2) -> TBV (s1 + s2)
+ | BO_select (_, te) -> te
+ | BO_diffarray (ti, _) -> ti
let b_type_args = function
- | BO_Zplus | BO_Zminus | BO_Zmult
+ | BO_Zplus | BO_Zminus | BO_Zmult
| BO_Zlt | BO_Zle | BO_Zge | BO_Zgt -> (TZ,TZ)
| BO_eq t -> (t,t)
-
- let interp_eq = function
+ | BO_BVand s | BO_BVor s | BO_BVxor s | BO_BVadd s | BO_BVmult s
+ | BO_BVult s | BO_BVslt s | BO_BVshl s | BO_BVshr s ->
+ (TBV s,TBV s)
+ | BO_BVconcat (s1, s2) -> (TBV s1, TBV s2)
+ | BO_select (ti, te) -> (TFArray (ti, te), ti)
+ | BO_diffarray (ti, te) -> (TFArray (ti, te), TFArray (ti, te))
+
+
+ let interp_ieq t_i t =
+ mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|]
+
+ (* let veval_t te =
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let evd, ty = Typing.type_of env evd te in
+ Vnorm.cbv_vm env te ty
+
+
+ let interp_ieq_eval t_i t =
+ let te = mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|] in
+ veval_t te
+ *)
+
+ let interp_eqarray t_i ti te =
+ mklApp cequalarray
+ SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+ SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+ SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
+ SmtBtype.inh_interp t_i te |]
+
+ let interp_select t_i ti te =
+ mklApp cselect
+ SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+ SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+ SmtBtype.inh_interp t_i te|]
+
+ let interp_diff t_i ti te =
+ mklApp cdiff
+ SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+ SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+ SmtBtype.dec_interp t_i te; SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
+ SmtBtype.inh_interp t_i ti; SmtBtype.inh_interp t_i te |]
+
+
+ let interp_store t_i ti te =
+ mklApp cstore
+ SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+ SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+ SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; SmtBtype.inh_interp t_i te |]
+
+
+ let interp_eq t_i = function
| TZ -> Lazy.force ceqbZ
| Tbool -> Lazy.force ceqb
| Tpositive -> Lazy.force ceqbP
- | Tindex i -> mklApp cte_eqb [|indexed_type_hval i|]
+ | TBV s -> mklApp cbv_eq [|mkN s|]
+ | Tindex i ->
+ mklApp ceqb_of_compdec [|mklApp cte_carrier [|i.hval|];
+ mklApp cte_compdec [|i.hval|]|]
+ | TFArray (ti, te) -> interp_eqarray t_i ti te
+
+
- let interp_bop = function
+ let interp_bop t_i = function
| BO_Zplus -> Lazy.force cadd
| BO_Zminus -> Lazy.force csub
| BO_Zmult -> Lazy.force cmul
@@ -140,7 +292,32 @@ module Op =
| BO_Zle -> Lazy.force cleb
| BO_Zge -> Lazy.force cgeb
| BO_Zgt -> Lazy.force cgtb
- | BO_eq t -> interp_eq t
+ | BO_eq t -> interp_eq t_i t
+ | BO_BVand s -> mklApp cbv_and [|mkN s|]
+ | BO_BVor s -> mklApp cbv_or [|mkN s|]
+ | BO_BVxor s -> mklApp cbv_xor [|mkN s|]
+ | BO_BVadd s -> mklApp cbv_add [|mkN s|]
+ | BO_BVmult s -> mklApp cbv_mult [|mkN s|]
+ | BO_BVult s -> mklApp cbv_ult [|mkN s|]
+ | BO_BVslt s -> mklApp cbv_slt [|mkN s|]
+ | BO_BVconcat (s1,s2) -> mklApp cbv_concat [|mkN s1; mkN s2|]
+ | BO_BVshl s -> mklApp cbv_shl [|mkN s|]
+ | BO_BVshr s -> mklApp cbv_shr [|mkN s|]
+ | BO_select (ti, te) -> interp_select t_i ti te
+ | BO_diffarray (ti, te) -> interp_diff t_i ti te
+
+ let t_to_coq = function
+ | TO_store (ti, te) -> store_to_coq ti te
+
+ let t_type_of = function
+ | TO_store (ti, te) -> TFArray (ti, te)
+
+ let t_type_args = function
+ | TO_store (ti, te) -> TFArray (ti, te), ti, te
+
+ let interp_top t_i = function
+ | TO_store (ti, te) -> interp_store t_i ti te
+
let n_to_coq = function
| NO_distinct t -> mklApp cNO_distinct [|SmtBtype.to_coq t|]
@@ -151,14 +328,9 @@ module Op =
let n_type_args = function
| NO_distinct ty -> ty
- let interp_distinct = function
- | TZ -> Lazy.force cZ
- | Tbool -> Lazy.force cbool
- | Tpositive -> Lazy.force cpositive
- | Tindex i -> mklApp cte_carrier [|indexed_type_hval i|]
-
- let interp_nop = function
- | NO_distinct ty -> mklApp cdistinct [|interp_distinct ty;interp_eq ty|]
+ let interp_nop t_i = function
+ | NO_distinct ty ->
+ mklApp cdistinct [|SmtBtype.interp t_i ty; interp_eq t_i ty|]
let i_to_coq i = let index, _ = destruct "destruct on a Rel: called by i_to_coq" i in
mkInt index
@@ -206,14 +378,50 @@ module Op =
(index, hval.tparams, hval.tres, op)::acc in
Hashtbl.fold set reify.tbl []
- let c_equal op1 op2 = op1 == op2
+ let c_equal op1 op2 = match op1, op2 with
+ | CO_BV bv1, CO_BV bv2 ->
+ (try List.for_all2 (=) bv1 bv2 with
+ | Invalid_argument _ -> false)
+ | _ -> op1 == op2
- let u_equal op1 op2 = op1 == op2
+ let u_equal op1 op2 =
+ match op1,op2 with
+ | UO_xO, UO_xO
+ | UO_xI, UO_xI
+ | UO_Zpos, UO_Zpos
+ | UO_Zneg, UO_Zneg
+ | UO_Zopp, UO_Zopp -> true
+ | UO_BVbitOf (s1,i1), UO_BVbitOf (s2,i2) -> s1 == s2 && i1 == i2
+ | UO_BVnot s1, UO_BVnot s2 -> s1 == s2
+ | UO_BVneg s1, UO_BVneg s2 -> s1 == s2
+ | UO_BVextr (i1, n1, s1) , UO_BVextr (i2, n2, s2) ->
+ i1 == i2 && n1 == n2 && s1 == s2
+ | UO_BVzextn (s1, n1), UO_BVzextn (s2, n2) -> s1 == s2 && n1 == n2
+ | UO_BVsextn (s1, n1), UO_BVsextn (s2, n2) -> s1 == s2 && n1 == n2
+ | _ -> false
let b_equal op1 op2 =
match op1,op2 with
- | BO_eq t1, BO_eq t2 -> SmtBtype.equal t1 t2
- | _ -> op1 == op2
+ | BO_eq t1, BO_eq t2 -> SmtBtype.equal t1 t2
+ | BO_BVand n1, BO_BVand n2 -> n1 == n2
+ | BO_BVor n1, BO_BVor n2 -> n1 == n2
+ | BO_BVxor n1, BO_BVxor n2 -> n1 == n2
+ | BO_BVadd n1, BO_BVadd n2 -> n1 == n2
+ | BO_BVmult n1, BO_BVmult n2 -> n1 == n2
+ | BO_BVult n1, BO_BVult n2 -> n1 == n2
+ | BO_BVslt n1, BO_BVslt n2 -> n1 == n2
+ | BO_BVconcat (n1,m1), BO_BVconcat (n2,m2) -> n1 == n2 && m1 == m2
+ | BO_BVshl n1, BO_BVshl n2 -> n1 == n2
+ | BO_BVshr n1, BO_BVshr n2 -> n1 == n2
+ | BO_select (ti1, te1), BO_select (ti2, te2)
+ | BO_diffarray (ti1, te1), BO_diffarray (ti2, te2) ->
+ SmtBtype.equal ti1 ti2 && SmtBtype.equal te1 te2
+ | _ -> op1 == op2
+
+ let t_equal op1 op2 =
+ match op1,op2 with
+ | TO_store (ti1, te1), TO_store (ti2, te2) ->
+ SmtBtype.equal ti1 ti2 && SmtBtype.equal te1 te2
let n_equal op1 op2 =
match op1,op2 with
@@ -221,6 +429,62 @@ module Op =
let i_equal (i1, _) (i2, _) = i1 = i2
+
+
+
+ let logic_of_cop = function
+ | CO_xH | CO_Z0 -> SL.singleton LLia
+ | CO_BV _ -> SL.singleton LBitvectors
+
+ let logic_of_uop = function
+ | UO_xO | UO_xI
+ | UO_Zpos | UO_Zneg | UO_Zopp -> SL.singleton LLia
+ | UO_BVbitOf _ | UO_BVnot _ | UO_BVneg _
+ | UO_BVextr _ | UO_BVzextn _ | UO_BVsextn _ -> SL.singleton LBitvectors
+
+ let logic_of_bop = function
+ | BO_Zplus
+ | BO_Zminus
+ | BO_Zmult
+ | BO_Zlt
+ | BO_Zle
+ | BO_Zge
+ | BO_Zgt -> SL.singleton LLia
+ | BO_eq ty -> SmtBtype.logic ty
+ | BO_BVand _
+ | BO_BVor _
+ | BO_BVxor _
+ | BO_BVadd _
+ | BO_BVmult _
+ | BO_BVult _
+ | BO_BVslt _
+ | BO_BVshl _
+ | BO_BVshr _
+ | BO_BVconcat _ -> SL.singleton LBitvectors
+ | BO_select (ti, te)
+ | BO_diffarray (ti, te) ->
+ SL.add LArrays (SL.union (SmtBtype.logic ti) (SmtBtype.logic te))
+
+
+ let logic_of_top = function
+ | TO_store (ti, te) ->
+ SL.add LArrays (SL.union (SmtBtype.logic ti) (SmtBtype.logic te))
+
+ let logic_of_nop = function
+ | NO_distinct ty -> SmtBtype.logic ty
+
+
+ let logic_of_indexed t =
+ let (_, hval) = destruct "destruct on a Rel: called by logic_of_indexed" t in
+ Array.fold_left (fun l ty ->
+ SL.union (SmtBtype.logic ty) l
+ ) (SmtBtype.logic hval.tres) hval.tparams
+
+
+ let logic_ro reify =
+ Hashtbl.fold (fun _ op -> SL.union (logic_of_indexed op))
+ reify.tbl SL.empty
+
end
@@ -230,6 +494,7 @@ type atom =
| Acop of cop
| Auop of uop * hatom
| Abop of bop * hatom * hatom
+ | Atop of top * hatom * hatom * hatom
| Anop of nop * hatom array
| Aapp of indexed_op * hatom array
@@ -271,17 +536,24 @@ module HashedAtom =
| Acop opa, Acop opb -> Op.c_equal opa opb
| Auop(opa,ha), Auop(opb,hb) -> Op.u_equal opa opb && ha.index == hb.index
| Abop(opa,ha1,ha2), Abop(opb,hb1,hb2) ->
- Op.b_equal opa opb && ha1.index == hb1.index && ha2.index == hb2.index
+ Op.b_equal opa opb && ha1.index == hb1.index && ha2.index == hb2.index
+ | Atop(opa,ha1,ha2,ha3), Atop(opb,hb1,hb2,hb3) ->
+ Op.t_equal opa opb && ha1.index == hb1.index &&
+ ha2.index == hb2.index && ha3.index == hb3.index
| Anop (opa,ha), Anop (opb,hb) ->
- let na = Array.length ha in
- let nb = Array.length hb in
- let i = ref (-1) in
- Op.n_equal opa opb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
+ let na = Array.length ha in
+ let nb = Array.length hb in
+ let i = ref (-1) in
+ Op.n_equal opa opb && na == nb &&
+ Array.fold_left
+ (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
| Aapp (va,ha), Aapp (vb,hb) ->
- let na = Array.length ha in
- let nb = Array.length hb in
- let i = ref (-1) in
- Op.i_equal va vb && na == nb && Array.fold_left (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
+ let na = Array.length ha in
+ let nb = Array.length hb in
+ let i = ref (-1) in
+ Op.i_equal va vb && na == nb &&
+ Array.fold_left
+ (fun b h -> incr i; b && h.index == hb.(!i).index) true ha
| _, _ -> false
let hash = function
@@ -289,24 +561,31 @@ module HashedAtom =
| Auop (op,h) ->
(( (h.index lsl 3) + (Hashtbl.hash op)) lsl 3) lxor 2
| Abop (op,h1,h2) ->
- (((( (h1.index lsl 2) + h2.index) lsl 3) + Hashtbl.hash op) lsl 3) lxor 3
+ (((( (h1.index lsl 2) + h2.index) lsl 3) + Hashtbl.hash op) lsl 3) lxor 3
+ | Atop (op,h1,h2,h3) ->
+ (((( ((h1.index lsl 2) + h2.index) lsl 3) + h3.index) lsl 4
+ + Hashtbl.hash op) lsl 4) lxor 4
| Anop (op, args) ->
- let hash_args =
- match Array.length args with
- | 0 -> 0
- | 1 -> args.(0).index
- | 2 -> args.(1).index lsl 2 + args.(0).index
- | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in
- (hash_args lsl 5 + (Hashtbl.hash op) lsl 3) lxor 4
+ let hash_args =
+ match Array.length args with
+ | 0 -> 0
+ | 1 -> args.(0).index
+ | 2 -> args.(1).index lsl 2 + args.(0).index
+ | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index
+ in
+ (hash_args lsl 5 + (Hashtbl.hash op) lsl 3) lxor 4
| Aapp (op, args) ->
let op_index = try fst (destruct "destruct on a Rel: called by hash" op) with _ -> 0 in
- let hash_args =
- match Array.length args with
- | 0 -> 0
- | 1 -> args.(0).index
- | 2 -> args.(1).index lsl 2 + args.(0).index
- | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index in
- (hash_args lsl 5 + op_index lsl 3) lxor 4
+ let hash_args =
+ match Array.length args with
+ | 0 -> 0
+ | 1 -> args.(0).index
+ | 2 -> args.(1).index lsl 2 + args.(0).index
+ | _ -> args.(2).index lsl 4 + args.(1).index lsl 2 + args.(0).index
+ in
+ (hash_args lsl 5 + op_index lsl 3) lxor 4
+
+
end
@@ -327,124 +606,189 @@ module Atom =
| Acop op -> Op.c_type_of op
| Auop (op,_) -> Op.u_type_of op
| Abop (op,_,_) -> Op.b_type_of op
+ | Atop (op,_,_,_) -> Op.t_type_of op
| Anop (op,_) -> Op.n_type_of op
| Aapp (op,_) -> Op.i_type_of op
let is_bool_type h = SmtBtype.equal (type_of h) Tbool
+ let is_bv_type h = match type_of h with | TBV _ -> true | _ -> false
let rec compute_int = function
| Acop c ->
(match c with
| CO_xH -> 1
- | CO_Z0 -> 0)
+ | CO_Z0 -> 0
+ | CO_BV _ -> assert false)
| Auop (op,h) ->
(match op with
| UO_xO -> 2*(compute_hint h)
| UO_xI -> 2*(compute_hint h) + 1
| UO_Zpos -> compute_hint h
| UO_Zneg -> - (compute_hint h)
- | UO_Zopp -> assert false)
+ | UO_Zopp | UO_BVbitOf _
+ | UO_BVnot _ | UO_BVneg _
+ | UO_BVextr _ | UO_BVzextn _ | UO_BVsextn _ -> assert false)
| _ -> assert false
and compute_hint h = compute_int (atom h)
- let to_string_int i =
+ let to_smt_int fmt i =
let s1 = if i < 0 then "(- " else "" in
let s2 = if i < 0 then ")" else "" in
let j = if i < 0 then -i else i in
- s1 ^ string_of_int j ^ s2
-
- let to_string ?pi:(pi=false) h =
- let rec to_string h =
- (if pi then string_of_int (index h) ^":" else "")
- ^ to_string_atom (atom h)
-
- and to_string_atom = function
- | Acop _ as a -> to_string_int (compute_int a)
- | Auop (UO_Zopp,h) ->
- "(- " ^
- to_string h ^
- ")"
- | Auop _ as a -> to_string_int (compute_int a)
- | Abop (op,h1,h2) -> to_string_bop op h1 h2
- | Anop (op,a) -> to_string_nop op a
- | Aapp ((i, op), a) ->
- let op_string = begin match i with
- | Index index -> "op_" ^ string_of_int index
- | Rel_name name -> name end
- ^ if pi then to_string_op op else "" in
+ Format.fprintf fmt "%s%i%s" s1 j s2
+
+
+ let rec bv_to_smt fmt = function
+ | true :: bv -> Format.fprintf fmt "%a1" bv_to_smt bv
+ | false :: bv -> Format.fprintf fmt "%a0" bv_to_smt bv
+ | [] -> ()
+
+
+ let to_smt_named ?pi:(pi=false) (fmt:Format.formatter) h =
+ let rec to_smt fmt h =
+ if pi then Format.fprintf fmt "%d:" (index h);
+ to_smt_atom (atom h)
+
+ and to_smt_atom = function
+ | Acop (CO_BV bv) -> Format.fprintf fmt "#b%a" bv_to_smt bv
+ | Acop _ as a -> to_smt_int fmt (compute_int a)
+ | Auop (UO_Zopp,h) ->
+ Format.fprintf fmt "(- ";
+ to_smt fmt h;
+ Format.fprintf fmt ")"
+ | Auop (UO_BVbitOf (_, i), h) ->
+ Format.fprintf fmt "(bitof %d %a)" i to_smt h
+ | Auop (UO_BVnot _, h) ->
+ Format.fprintf fmt "(bvnot %a)" to_smt h
+ | Auop (UO_BVneg _, h) ->
+ Format.fprintf fmt "(bvneg %a)" to_smt h
+ | Auop (UO_BVextr (i, n, _), h) ->
+ Format.fprintf fmt "((_ extract %d %d) %a)" (i+n-1) i to_smt h
+ | Auop (UO_BVzextn (_, n), h) ->
+ Format.fprintf fmt "((_ zero_extend %d) %a)" n to_smt h
+ | Auop (UO_BVsextn (_, n), h) ->
+ Format.fprintf fmt "((_ sign_extend %d) %a)" n to_smt h
+ | Auop _ as a -> to_smt_int fmt (compute_int a)
+ | Abop (op,h1,h2) -> to_smt_bop op h1 h2
+ | Atop (op,h1,h2,h3) -> to_smt_top op h1 h2 h3
+ | Anop (op,a) -> to_smt_nop op a
+ | Aapp ((i,op),a) ->
+ let op_smt () =
+ (match i with
+ | Index index -> Format.fprintf fmt "op_%i" index
+ | Rel_name name -> Format.fprintf fmt "%s" name);
+ if pi then to_smt_op op
+ in
if Array.length a = 0 then (
- op_string
+ op_smt ()
) else (
- "(" ^ op_string ^
- Array.fold_left (fun acc h -> acc ^ " " ^ to_string h) "" a ^
- ")"
+ Format.fprintf fmt "(";
+ op_smt ();
+ Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a;
+ Format.fprintf fmt ")"
)
- and to_string_op {tparams=bta; tres=bt; op_val=t} =
- "[(" ^ Array.fold_left (fun acc bt -> acc ^ SmtBtype.to_string bt ^ " ")
- " " bta ^ ") ( " ^ SmtBtype.to_string bt ^ " ) ( " ^
- Pp.string_of_ppcmds (Printer.pr_constr t) ^ " )]"
- and to_string_bop op h1 h2 =
+ and to_smt_op {tparams=bta; tres=bt; op_val=t} =
+ Format.fprintf fmt "[(";
+ Array.iter (fun bt -> SmtBtype.to_smt fmt bt; Format.fprintf fmt " ") bta;
+ Format.fprintf fmt ") ( ";
+ SmtBtype.to_smt fmt bt;
+ Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Printer.pr_constr t))
+
+ and to_smt_bop op h1 h2 =
let s = match op with
- | BO_Zplus -> "+"
- | BO_Zminus -> "-"
- | BO_Zmult -> "*"
- | BO_Zlt -> "<"
- | BO_Zle -> "<="
- | BO_Zge -> ">="
- | BO_Zgt -> ">"
- | BO_eq _ -> "=" in
- "(" ^ s ^ " " ^
- to_string h1 ^
- " " ^
- to_string h2 ^
- ")"
-
- and to_string_nop op a =
+ | BO_Zplus -> "+"
+ | BO_Zminus -> "-"
+ | BO_Zmult -> "*"
+ | BO_Zlt -> "<"
+ | BO_Zle -> "<="
+ | BO_Zge -> ">="
+ | BO_Zgt -> ">"
+ | BO_eq _ -> "="
+ | BO_BVand _ -> "bvand"
+ | BO_BVor _ -> "bvor"
+ | BO_BVxor _ -> "bvxor"
+ | BO_BVadd _ -> "bvadd"
+ | BO_BVmult _ -> "bvmul"
+ | BO_BVult _ -> "bvult"
+ | BO_BVslt _ -> "bvslt"
+ | BO_BVconcat _ -> "concat"
+ | BO_BVshl _ -> "bvshl"
+ | BO_BVshr _ -> "bvlshr"
+ | BO_select _ -> "select"
+ | BO_diffarray _ -> "diff" (* should not be used in goals *)
+ in
+ Format.fprintf fmt "(%s %a %a)" s to_smt h1 to_smt h2
+
+ and to_smt_top op h1 h2 h3=
let s = match op with
- | NO_distinct _ -> "distinct" in
- "(" ^ s ^
- Array.fold_left (fun acc h -> acc ^ " " ^ to_string h) "" a ^
- ")" in
- to_string h
+ | TO_store _ -> "store"
+ in
+ Format.fprintf fmt "(%s %a %a %a)" s to_smt h1 to_smt h2 to_smt h3
+
+ and to_smt_nop op a =
+ let s = match op with
+ | NO_distinct _ -> "distinct" in
+ Format.fprintf fmt "(%s" s;
+ Array.iter (fun h -> Format.fprintf fmt " "; to_smt fmt h) a;
+ Format.fprintf fmt ")"
+
+ in
+ to_smt fmt h
- let to_smt fmt t = Format.fprintf fmt "%s@." (to_string t)
+ let to_smt (fmt:Format.formatter) h = to_smt_named fmt h
exception NotWellTyped of atom
let check a =
+ (* Format.eprintf "Checking %a @." to_smt_atom a; *)
match a with
| Acop _ -> ()
| Auop(op,h) ->
- if not (SmtBtype.equal (Op.u_type_arg op) (type_of h))
- then raise (NotWellTyped a)
+ if not (SmtBtype.equal (Op.u_type_arg op) (type_of h)) then
+ raise (NotWellTyped a)
| Abop(op,h1,h2) ->
- let (t1,t2) = Op.b_type_args op in
- if not (SmtBtype.equal t1 (type_of h1) && SmtBtype.equal t2 (type_of h2))
- then raise (NotWellTyped a)
+ let (t1,t2) = Op.b_type_args op in
+ if not (SmtBtype.equal t1 (type_of h1) && SmtBtype.equal t2 (type_of h2))
+ then (Format.eprintf "1. Wanted %a, got %a@.2. Wanted %a, got %a@."
+ SmtBtype.to_smt t1 SmtBtype.to_smt (type_of h1)
+ SmtBtype.to_smt t2 SmtBtype.to_smt (type_of h2);
+ raise (NotWellTyped a))
+ | Atop(op,h1,h2,h3) ->
+ let (t1,t2,t3) = Op.t_type_args op in
+ if not (SmtBtype.equal t1 (type_of h1) &&
+ SmtBtype.equal t2 (type_of h2) &&
+ SmtBtype.equal t3 (type_of h3))
+ then raise (NotWellTyped a)
| Anop(op,ha) ->
- let ty = Op.n_type_args op in
- Array.iter (fun h -> if not (SmtBtype.equal ty (type_of h)) then raise (NotWellTyped a)) ha
+ let ty = Op.n_type_args op in
+ Array.iter
+ (fun h -> if not (SmtBtype.equal ty (type_of h)) then
+ raise (NotWellTyped a)) ha
| Aapp(op,args) ->
- let tparams = Op.i_type_args op in
- Array.iteri (fun i t ->
- if not (SmtBtype.equal t (type_of args.(i))) then
- raise (NotWellTyped a)) tparams
+ let tparams = Op.i_type_args op in
+ Array.iteri (fun i t ->
+ if not (SmtBtype.equal t (type_of args.(i))) then
+ (Format.eprintf "Wanted %a, got %a@."
+ SmtBtype.to_smt t SmtBtype.to_smt (type_of args.(i));
+ raise (NotWellTyped a))) tparams
type reify_tbl =
{ mutable count : int;
- tbl : hatom HashAtom.t
+ tbl : hatom HashAtom.t
}
-
let create () =
{ count = 0;
tbl = HashAtom.create 17 }
+ let op_coq_terms = Hashtbl.create 17
+
let clear reify =
+ Hashtbl.clear op_coq_terms;
reify.count <- 0;
HashAtom.clear reify.tbl
@@ -461,7 +805,7 @@ module Atom =
with Not_found -> declare reify a
else {index = -1; hval = a}
- let mk_eq reify decl ty h1 h2 =
+ let mk_eq reify ?declare:(decl=true) ty h1 h2 =
let op = BO_eq ty in
try
HashAtom.find reify.tbl (Abop (op, h1, h2))
@@ -473,7 +817,7 @@ module Atom =
let mk_neg reify ({index = i; hval = a} as ha) =
try HashAtom.find reify.tbl (Auop (UO_Zopp, ha))
- with Not_found ->
+ with Not_found ->
let na = match a with
| Auop (UO_Zpos, x) -> Auop (UO_Zneg, x)
| Auop (UO_Zneg, x) -> Auop (UO_Zpos, x)
@@ -481,20 +825,25 @@ module Atom =
get reify na
let rec hash_hatom ra' {index = _; hval = a} =
- match a with
+ match a with
| Acop cop -> get ra' a
| Auop (uop, ha) -> get ra' (Auop (uop, hash_hatom ra' ha))
| Abop (bop, ha1, ha2) ->
let new_ha1 = hash_hatom ra' ha1 in
let new_ha2 = hash_hatom ra' ha2 in
begin match bop with
- | BO_eq ty -> mk_eq ra' true ty new_ha1 new_ha2
+ | BO_eq ty -> mk_eq ra' ~declare:true ty new_ha1 new_ha2
| _ -> get ra' (Abop (bop, new_ha1, new_ha2)) end
+ | Atop (top, ha1, ha2, ha3) ->
+ let new_ha1 = hash_hatom ra' ha1 in
+ let new_ha2 = hash_hatom ra' ha2 in
+ let new_ha3 = hash_hatom ra' ha3 in
+ get ra' (Atop (top, new_ha1, new_ha2, new_ha3))
| Anop _ -> assert false
| Aapp (op, arr) -> get ra' (Aapp (op, Array.map (hash_hatom ra') arr))
-
+
let copy {count=c; tbl=t} = {count = c; tbl = HashAtom.copy t}
-
+
let print_atoms reify where =
let oc = open_out where in
let fmt = Format.formatter_of_out_channel oc in
@@ -513,11 +862,15 @@ module Atom =
type coq_cst =
| CCxH
| CCZ0
+ | CCBV
| CCxO
| CCxI
| CCZpos
| CCZneg
| CCZopp
+ | CCBVbitOf
+ | CCBVnot
+ | CCBVneg
| CCZplus
| CCZminus
| CCZmult
@@ -525,39 +878,164 @@ module Atom =
| CCZle
| CCZge
| CCZgt
+ | CCBVand
+ | CCBVor
+ | CCBVxor
+ | CCBVadd
+ | CCBVmult
+ | CCBVult
+ | CCBVslt
+ | CCBVconcat
+ | CCBVextr
+ | CCBVsextn
+ | CCBVzextn
+ | CCBVshl
+ | CCBVshr
| CCeqb
| CCeqbP
| CCeqbZ
+ | CCeqbBV
+ | CCeqbA
+ | CCselect
+ | CCdiff
+ | CCstore
| CCunknown
+ | CCunknown_deps of int
+
+
+ let logic_coq_cst = function
+ | CCxH
+ | CCZ0
+ | CCxO
+ | CCxI
+ | CCZpos
+ | CCZneg
+ | CCZopp
+ | CCZplus
+ | CCZminus
+ | CCZmult
+ | CCZlt
+ | CCZle
+ | CCZge
+ | CCZgt -> SL.singleton LLia
+
+ | CCBV
+ | CCBVbitOf
+ | CCBVnot
+ | CCBVneg
+ | CCBVand
+ | CCBVor
+ | CCBVxor
+ | CCBVadd
+ | CCBVmult
+ | CCBVult
+ | CCBVslt
+ | CCBVconcat
+ | CCBVextr
+ | CCBVsextn
+ | CCBVzextn
+ | CCBVshl
+ | CCBVshr -> SL.singleton LBitvectors
+
+ | CCselect | CCdiff | CCstore -> SL.singleton LArrays
+
+ | CCeqb -> SL.empty
+
+ (* | CCeqbP | CCeqbZ -> SL.singleton LLia *)
+ (* | CCeqbBV -> SL.singleton LBitvectors *)
+ (* | CCeqbA -> SL.singleton LArrays *)
+
+ | CCeqbP | CCeqbZ | CCeqbBV | CCeqbA
+ | CCunknown | CCunknown_deps _ -> SL.singleton LUF
+
+
+ let gobble_of_coq_cst = function
+ | CCBV
+ | CCBVbitOf
+ | CCBVnot
+ | CCBVneg
+ | CCBVand
+ | CCBVor
+ | CCBVxor
+ | CCBVadd
+ | CCBVmult
+ | CCBVult
+ | CCBVslt
+ | CCBVsextn
+ | CCBVzextn
+ | CCBVshl
+ | CCBVshr -> 1
+
+ | CCBVconcat -> 2
+ | CCBVextr -> 3
+
+ | CCselect -> 5
+ | CCdiff -> 10
+ | CCstore -> 8
+
+ | _ -> 0
+
let op_tbl () =
let tbl = Hashtbl.create 29 in
let add (c1,c2) = Hashtbl.add tbl (Lazy.force c1) c2 in
List.iter add
- [ cxH,CCxH; cZ0,CCZ0;
+ [ cxH,CCxH; cZ0,CCZ0; cof_bits, CCBV;
cxO,CCxO; cxI,CCxI; cZpos,CCZpos; cZneg,CCZneg; copp,CCZopp;
+ cbitOf, CCBVbitOf; cbv_not, CCBVnot; cbv_neg, CCBVneg;
+ cbv_extr, CCBVextr; cbv_zextn, CCBVzextn; cbv_sextn, CCBVsextn;
cadd,CCZplus; csub,CCZminus; cmul,CCZmult; cltb,CCZlt;
- cleb,CCZle; cgeb,CCZge; cgtb,CCZgt; ceqb,CCeqb; ceqbP,CCeqbP;
- ceqbZ, CCeqbZ
+ cleb,CCZle; cgeb,CCZge; cgtb,CCZgt;
+ cbv_and, CCBVand; cbv_or, CCBVor; cbv_xor, CCBVxor;
+ cbv_add, CCBVadd; cbv_mult, CCBVmult;
+ cbv_ult, CCBVult; cbv_slt, CCBVslt; cbv_concat, CCBVconcat;
+ cbv_shl, CCBVshl; cbv_shr, CCBVshr;
+ ceqb,CCeqb; ceqbP,CCeqbP; ceqbZ, CCeqbZ; cbv_eq, CCeqbBV;
+ cselect, CCselect; cdiff, CCdiff;
+ cstore, CCstore;
+ cequalarray, CCeqbA;
];
tbl
let op_tbl = lazy (op_tbl ())
- let of_coq ?hash:(h=false) rt ro reify env sigma c =
+
+ let split_list_at n l =
+ let rec aux acc n l = match n, l with
+ | 0, _ -> List.rev acc, l
+ | _, [] -> assert false
+ | _, x :: l -> aux (x :: acc) (n-1) l
+ in
+ aux [] n l
+
+
+ let get_coq_term_op =
+ Hashtbl.find op_coq_terms
+
+
+ let of_coq ?hash:(h=false) rt ro reify known_logic env sigma c =
let op_tbl = Lazy.force op_tbl in
let get_cst c =
- try Hashtbl.find op_tbl c with Not_found -> CCunknown in
+ try
+ let cc = Hashtbl.find op_tbl c in
+ if SL.subset (logic_coq_cst cc) known_logic then cc
+ else CCunknown_deps (gobble_of_coq_cst cc)
+ with Not_found -> CCunknown
+ in
let rec mk_hatom h =
let c, args = Term.decompose_app h in
match get_cst c with
- | CCxH -> mk_cop CO_xH
- | CCZ0 -> mk_cop CO_Z0
+ | CCxH -> mk_cop CCxH args
+ | CCZ0 -> mk_cop CCZ0 args
+ | CCBV -> mk_cop CCBV args
| CCxO -> mk_uop UO_xO args
| CCxI -> mk_uop UO_xI args
| CCZpos -> mk_uop UO_Zpos args
| CCZneg -> mk_uop UO_Zneg args
| CCZopp -> mk_uop UO_Zopp args
+ | CCBVbitOf -> mk_bvbitof args
+ | CCBVnot -> mk_bvnot args
+ | CCBVneg -> mk_bvneg args
| CCZplus -> mk_bop BO_Zplus args
| CCZminus -> mk_bop BO_Zminus args
| CCZmult -> mk_bop BO_Zmult args
@@ -565,25 +1043,79 @@ module Atom =
| CCZle -> mk_bop BO_Zle args
| CCZge -> mk_bop BO_Zge args
| CCZgt -> mk_bop BO_Zgt args
- | CCeqb -> mk_teq Tbool args
- | CCeqbP -> mk_teq Tpositive args
- | CCeqbZ -> mk_teq TZ args
- | CCunknown -> let ty = Retyping.get_type_of env sigma h in
- mk_unknown c args ty
+ | CCBVand -> mk_bop_bvand args
+ | CCBVor -> mk_bop_bvor args
+ | CCBVxor -> mk_bop_bvxor args
+ | CCBVadd -> mk_bop_bvadd args
+ | CCBVmult -> mk_bop_bvmult args
+ | CCBVult -> mk_bop_bvult args
+ | CCBVslt -> mk_bop_bvslt args
+ | CCBVconcat -> mk_bop_bvconcat args
+ | CCBVextr -> mk_bvextr args
+ | CCBVzextn -> mk_bvzextn args
+ | CCBVsextn -> mk_bvsextn args
+ | CCBVshl -> mk_bop_bvshl args
+ | CCBVshr -> mk_bop_bvshr args
+ | CCeqb -> mk_bop (BO_eq Tbool) args
+ | CCeqbP -> mk_bop (BO_eq Tpositive) args
+ | CCeqbZ -> mk_bop (BO_eq TZ) args
+ | CCeqbA -> mk_bop_farray_equal args
+ | CCeqbBV -> mk_bop_bveq args
+ | CCselect -> mk_bop_select args
+ | CCdiff -> mk_bop_diff args
+ | CCstore -> mk_top_store args
+ | CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h)
+ | CCunknown_deps gobble ->
+ mk_unknown_deps c args (Retyping.get_type_of env sigma h) gobble
+
+
+ and mk_cop op args = match op, args with
+ | CCxH, [] -> get reify (Acop CO_xH)
+ | CCZ0, [] -> get reify (Acop CO_Z0)
+ | CCBV, [bs] -> get reify (Acop (CO_BV (mk_bool_list bs)))
+ | _ -> assert false
- and mk_cop op = get reify (Acop op)
and mk_uop op = function
- | [a] -> let h = mk_hatom a in get reify (Auop (op,h))
- | _ -> failwith "unexpected number of arguments for mk_uop"
-
- and mk_teq ty args =
- if h then match args with
- | [a1; a2] -> let h1 = mk_hatom a1 in
- let h2 = mk_hatom a2 in
- mk_eq reify true ty h1 h2
- | _ -> failwith "unexpected number of arguments for mk_teq"
- else mk_bop (BO_eq ty) args
+ | [a] -> let h = mk_hatom a in
+ get reify (Auop (op,h))
+ | _ -> assert false
+
+ and mk_bvbitof = function
+ | [s;n;a] ->
+ let h = mk_hatom a in
+ get reify (Auop (UO_BVbitOf (mk_bvsize s, mk_nat n), h))
+ | _ -> assert false
+
+ and mk_bvnot = function
+ | [s;a] ->
+ let h = mk_hatom a in
+ get reify (Auop (UO_BVnot (mk_bvsize s), h))
+ | _ -> assert false
+
+ and mk_bvneg = function
+ | [s;a] ->
+ let h = mk_hatom a in
+ get reify (Auop (UO_BVneg (mk_bvsize s), h))
+ | _ -> assert false
+
+ and mk_bvextr = function
+ | [i;n;s;a] ->
+ let h = mk_hatom a in
+ get reify (Auop (UO_BVextr (mk_N i, mk_N n, mk_bvsize s), h))
+ | _ -> assert false
+
+ and mk_bvzextn = function
+ | [s;n;a] ->
+ let h = mk_hatom a in
+ get reify (Auop (UO_BVzextn (mk_bvsize s, mk_N n), h))
+ | _ -> assert false
+
+ and mk_bvsextn = function
+ | [s;n;a] ->
+ let h = mk_hatom a in
+ get reify (Auop (UO_BVsextn (mk_bvsize s, mk_N n), h))
+ | _ -> assert false
and mk_bop op = function
| [a1;a2] ->
@@ -592,19 +1124,148 @@ module Atom =
get reify (Abop (op,h1,h2))
| _ -> failwith "unexpected number of arguments for mk_bop"
+ and mk_top op = function
+ | [a1;a2;a3] ->
+ let h1 = mk_hatom a1 in
+ let h2 = mk_hatom a2 in
+ let h3 = mk_hatom a3 in
+ get reify (Atop (op,h1,h2,h3))
+ | _ -> assert false
+
+ and mk_bop_bvand = function
+ | [s;a1;a2] ->
+ let s' = mk_bvsize s in
+ mk_bop (BO_BVand s') [a1;a2]
+ | _ -> assert false
+
+ and mk_bop_bvor = function
+ | [s;a1;a2] ->
+ let s' = mk_bvsize s in
+ mk_bop (BO_BVor s') [a1;a2]
+ | _ -> assert false
+
+ and mk_bop_bvxor = function
+ | [s;a1;a2] ->
+ let s' = mk_bvsize s in
+ mk_bop (BO_BVxor s') [a1;a2]
+ | _ -> assert false
+
+ and mk_bop_bvadd = function
+ | [s;a1;a2] ->
+ let s' = mk_bvsize s in
+ mk_bop (BO_BVadd s') [a1;a2]
+ | _ -> assert false
+
+ and mk_bop_bvmult = function
+ | [s;a1;a2] ->
+ let s' = mk_bvsize s in
+ mk_bop (BO_BVmult s') [a1;a2]
+ | _ -> assert false
+
+ and mk_bop_bvult = function
+ | [s;a1;a2] ->
+ let s' = mk_bvsize s in
+ mk_bop (BO_BVult s') [a1;a2]
+ | _ -> assert false
+
+ and mk_bop_bvslt = function
+ | [s;a1;a2] ->
+ let s' = mk_bvsize s in
+ mk_bop (BO_BVslt s') [a1;a2]
+ | _ -> assert false
+
+ and mk_bop_bvshl = function
+ | [s;a1;a2] ->
+ let s' = mk_bvsize s in
+ mk_bop (BO_BVshl s') [a1;a2]
+ | _ -> assert false
+
+ and mk_bop_bvshr = function
+ | [s;a1;a2] ->
+ let s' = mk_bvsize s in
+ mk_bop (BO_BVshr s') [a1;a2]
+ | _ -> assert false
+
+ and mk_bop_bvconcat = function
+ | [s1;s2;a1;a2] ->
+ mk_bop (BO_BVconcat (mk_bvsize s1, mk_bvsize s2)) [a1;a2]
+ | _ -> assert false
+
+ and mk_bop_bveq = function
+ | [s;a1;a2] when SL.mem LBitvectors known_logic ->
+ let s' = mk_bvsize s in
+ mk_bop (BO_eq (TBV s')) [a1;a2]
+ (* We still want to interpret bv equality as uninterpreted
+ smtlib2 equality if the solver doesn't support bitvectors *)
+ | [s;a1;a2] ->
+ let ty = SmtBtype.of_coq rt known_logic (mklApp cbitvector [|s|]) in
+ mk_bop (BO_eq ty) [a1;a2]
+ | _ -> assert false
+
+ and mk_bop_select = function
+ | [ti;te;_;_;_;a;i] ->
+ let ti' = SmtBtype.of_coq rt known_logic ti in
+ let te' = SmtBtype.of_coq rt known_logic te in
+ mk_bop (BO_select (ti', te')) [a; i]
+ | _ -> assert false
+
+ and mk_bop_diff = function
+ | [ti;te;_;_;_;_;_;_;_;_;a;b] ->
+ let ti' = SmtBtype.of_coq rt known_logic ti in
+ let te' = SmtBtype.of_coq rt known_logic te in
+ mk_bop (BO_diffarray (ti', te')) [a; b]
+ | _ -> assert false
+
+ and mk_top_store = function
+ | [ti;te;_;_;_;_;_;_;a;i;e] ->
+ let ti' = SmtBtype.of_coq rt known_logic ti in
+ let te' = SmtBtype.of_coq rt known_logic te in
+ mk_top (TO_store (ti', te')) [a; i; e]
+ | _ -> assert false
+
+ and mk_bop_farray_equal = function
+ | [ti;te;_;_;_;_;_;a;b] when SL.mem LArrays known_logic ->
+ let ti' = SmtBtype.of_coq rt known_logic ti in
+ let te' = SmtBtype.of_coq rt known_logic te in
+ mk_bop (BO_eq (TFArray (ti', te'))) [a; b]
+ (* We still want to interpret array equality as uninterpreted
+ smtlib2 equality if the solver doesn't support arrays *)
+ | [ti;te;ord_ti;_;_;_;inh_te;a;b] ->
+ let ty = SmtBtype.of_coq rt known_logic
+ (mklApp cfarray [|ti; te; ord_ti; inh_te|]) in
+ mk_bop (BO_eq ty) [a;b]
+ | _ -> assert false
+
and mk_unknown c args ty =
let hargs = Array.of_list (List.map mk_hatom args) in
- let op = try Op.of_coq ro c
- with Not_found ->
- let targs = Array.map type_of hargs in
- let tres = SmtBtype.of_coq rt ty in
- let os = if Term.isRel c
- then let i = Term.destRel c in
- let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in
- Some (string_of_name n)
- else None in
- Op.declare ro c targs tres os in
- get reify (Aapp (op,hargs)) in
+ let op =
+ try Op.of_coq ro c
+ with | Not_found ->
+ let targs = Array.map type_of hargs in
+ let tres = SmtBtype.of_coq rt known_logic ty in
+ let os = if Term.isRel c then
+ let i = Term.destRel c in
+ let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in
+ Some (string_of_name n)
+ else
+ None
+ in
+ Op.declare ro c targs tres os in
+ (try
+ let (i, _) = destruct "" op in
+ Hashtbl.add op_coq_terms i c (* Chantal: I think we should move it to "Not_found" (otherwise it is already in the table) *)
+ with | Failure _ -> ());
+ get reify (Aapp (op,hargs))
+
+ (* create an uninterpreted symbol for an unsupported symbol but fisrt do
+ partial application to its dependent arguments whose number is given by
+ [gobble] *)
+ and mk_unknown_deps c args ty gobble =
+ let deps, args = split_list_at gobble args in
+ let c = Term.mkApp (c, Array.of_list deps) in
+ mk_unknown c args ty
+
+ in
mk_hatom c
@@ -616,15 +1277,21 @@ module Atom =
| Acop op -> mklApp cAcop [|Op.c_to_coq op|]
| Auop (op,h) -> mklApp cAuop [|Op.u_to_coq op; to_coq h|]
| Abop (op,h1,h2) ->
- mklApp cAbop [|Op.b_to_coq op;to_coq h1; to_coq h2|]
+ mklApp cAbop [|Op.b_to_coq op;to_coq h1; to_coq h2|]
+ | Atop (op,h1,h2,h3) ->
+ mklApp cAtop [|Op.t_to_coq op;to_coq h1; to_coq h2; to_coq h3|]
| Anop (op,ha) ->
- let cop = Op.n_to_coq op in
- let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) ha (mklApp cnil [|Lazy.force cint|]) in
- mklApp cAnop [|cop; cargs|]
+ let cop = Op.n_to_coq op in
+ let cargs = Array.fold_right
+ (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|])
+ ha (mklApp cnil [|Lazy.force cint|]) in
+ mklApp cAnop [|cop; cargs|]
| Aapp (op,args) ->
- let cop = Op.i_to_coq op in
- let cargs = Array.fold_right (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|]) args (mklApp cnil [|Lazy.force cint|]) in
- mklApp cAapp [|cop; cargs|]
+ let cop = Op.i_to_coq op in
+ let cargs = Array.fold_right
+ (fun h l -> mklApp ccons [|Lazy.force cint; to_coq h; l|])
+ args (mklApp cnil [|Lazy.force cint|]) in
+ mklApp cAapp [|cop; cargs|]
let dft_atom = lazy (mklApp cAcop [| Lazy.force cCO_xH |])
@@ -640,22 +1307,30 @@ module Atom =
(** Producing a Coq term corresponding to the interpretation of an atom *)
- let interp_to_coq atom_tbl a =
+ let interp_to_coq t_i atom_tbl a =
let rec interp_atom a =
let l = index a in
try Hashtbl.find atom_tbl l
with Not_found ->
let pc =
match atom a with
- | Acop c -> Op.interp_cop c
- | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|])
- | Abop (op,h1,h2) -> Term.mkApp (Op.interp_bop op, [|interp_atom h1; interp_atom h2|])
- | Anop (NO_distinct ty as op,ha) ->
- let cop = Op.interp_nop op in
- let typ = Op.interp_distinct ty in
- let cargs = Array.fold_right (fun h l -> mklApp ccons [|typ; interp_atom h; l|]) ha (mklApp cnil [|typ|]) in
- Term.mkApp (cop,[|cargs|])
- | Aapp ((_, hval),t) -> Term.mkApp (hval.op_val, Array.map interp_atom t) in
+ | Acop c -> Op.interp_cop c
+ | Auop (op,h) -> Term.mkApp (Op.interp_uop op, [|interp_atom h|])
+ | Abop (op,h1,h2) ->
+ Term.mkApp (Op.interp_bop t_i op,
+ [|interp_atom h1; interp_atom h2|])
+ | Atop (op,h1,h2,h3) ->
+ Term.mkApp (Op.interp_top t_i op,
+ [|interp_atom h1; interp_atom h2; interp_atom h3|])
+ | Anop (NO_distinct ty as op,ha) ->
+ let cop = Op.interp_nop t_i op in
+ let typ = SmtBtype.interp t_i ty in
+ let cargs = Array.fold_right (fun h l ->
+ mklApp ccons [|typ; interp_atom h; l|])
+ ha (mklApp cnil [|typ|]) in
+ Term.mkApp (cop,[|cargs|])
+ | Aapp (op,t) ->
+ Term.mkApp ((snd op).op_val, Array.map interp_atom t) in
Hashtbl.add atom_tbl l pc;
pc in
interp_atom a
@@ -663,11 +1338,13 @@ module Atom =
(* Generation of atoms *)
- let mk_nop op reify ?declare:(decl=true) a = get ~declare:decl reify (Anop (op,a))
+ let mk_nop ?declare:(decl=true) op reify a = get ~declare:decl reify (Anop (op,a))
+
+ let mk_binop ?declare:(decl=true) op reify h1 h2 = get ~declare:decl reify (Abop (op, h1, h2))
- let mk_binop op reify decl h1 h2 = get ~declare:decl reify (Abop (op, h1, h2))
+ let mk_terop ?declare:(decl=true) op reify h1 h2 h3 = get ~declare:decl reify (Atop (op, h1, h2, h3))
- let mk_unop op reify ?declare:(decl=true) h = get ~declare:decl reify (Auop (op, h))
+ let mk_unop ?declare:(decl=true) op reify h = get ~declare:decl reify (Auop (op, h))
let rec hatom_pos_of_int reify i =
if i <= 1 then
@@ -702,19 +1379,57 @@ module Atom =
if Big_int.gt_big_int i Big_int.zero_big_int then
mk_unop UO_Zpos reify (hatom_pos_of_bigint reify i)
else
- mk_unop UO_Zneg reify (hatom_pos_of_bigint reify (Big_int.minus_big_int i))
-
- let mk_unop op reify ?declare:(decl=true) h = get ~declare:decl reify (Auop (op, h))
-
- let mk_lt = mk_binop BO_Zlt
- let mk_le = mk_binop BO_Zle
- let mk_gt = mk_binop BO_Zgt
- let mk_ge = mk_binop BO_Zge
- let mk_plus = mk_binop BO_Zplus
- let mk_minus = mk_binop BO_Zminus
- let mk_mult = mk_binop BO_Zmult
- let mk_opp = mk_unop UO_Zopp
- let mk_distinct reify ty = mk_nop (NO_distinct ty) reify
+ mk_unop UO_Zneg reify
+ (hatom_pos_of_bigint reify (Big_int.minus_big_int i))
+
+ let mk_unop ?declare:(decl=true) op reify h = get ~declare:decl reify (Auop (op, h))
+
+ let mk_lt ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zlt ra
+ let mk_le ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zle ra
+ let mk_gt ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zgt ra
+ let mk_ge ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zge ra
+ let mk_plus ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zplus ra
+ let mk_minus ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zminus ra
+ let mk_mult ra ?declare:(decl=true) = mk_binop ~declare:decl BO_Zmult ra
+ let mk_bvand reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVand s) reify
+ let mk_bvor reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVor s) reify
+ let mk_bvxor reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVxor s) reify
+ let mk_bvadd reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVadd s) reify
+ let mk_bvmult reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVmult s) reify
+ let mk_bvult reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVult s) reify
+ let mk_bvslt reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVslt s) reify
+ let mk_bvconcat reify ?declare:(decl=true) s1 s2 = mk_binop ~declare:decl (BO_BVconcat (s1, s2)) reify
+ let mk_opp ra ?declare:(decl=true) = mk_unop ~declare:decl UO_Zopp ra
+ let mk_distinct reify ?declare:(decl=true) ty = mk_nop ~declare:decl (NO_distinct ty) reify
+ let mk_bitof reify ?declare:(decl=true) s i = mk_unop ~declare:decl (UO_BVbitOf (s, i)) reify
+ let mk_bvnot reify ?declare:(decl=true) s = mk_unop ~declare:decl (UO_BVnot s) reify
+ let mk_bvneg reify ?declare:(decl=true) s = mk_unop ~declare:decl (UO_BVneg s) reify
+ let mk_bvconst reify bool_list = get reify (Acop (CO_BV bool_list))
+ let mk_select reify ?declare:(decl=true) ti te = mk_binop ~declare:decl (BO_select (ti, te)) reify
+ let mk_diffarray reify ?declare:(decl=true) ti te = mk_binop ~declare:decl (BO_diffarray (ti, te)) reify
+ let mk_store reify ?declare:(decl=true) ti te = mk_terop ~declare:decl (TO_store (ti, te)) reify
+ let mk_bvextr reify ?declare:(decl=true) ~i ~n ~s = mk_unop ~declare:decl (UO_BVextr (i, n, s)) reify
+ let mk_bvzextn reify ?declare:(decl=true) ~s ~n = mk_unop ~declare:decl (UO_BVzextn (s, n)) reify
+ let mk_bvsextn reify ?declare:(decl=true) ~s ~n = mk_unop ~declare:decl (UO_BVsextn (s, n)) reify
+ let mk_bvshl reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVshl s) reify
+ let mk_bvshr reify ?declare:(decl=true) s = mk_binop ~declare:decl (BO_BVshr s) reify
+
+
+ let rec logic_atom = function
+ | Acop c -> Op.logic_of_cop c
+ | Auop (u, h) -> SL.union (Op.logic_of_uop u) (logic h)
+ | Abop (b, h1, h2) ->
+ SL.union (Op.logic_of_bop b) (SL.union (logic h1) (logic h2))
+ | Atop (t, h1, h2, h3) ->
+ SL.union (Op.logic_of_top t)
+ (SL.union (logic h1) (SL.union (logic h2) (logic h3)))
+ | Anop (n, ha) ->
+ Array.fold_left (fun l h -> SL.union (logic h) l) (Op.logic_of_nop n) ha
+ | Aapp (i, ha) ->
+ Array.fold_left (fun l h -> SL.union (logic h) l)
+ (Op.logic_of_indexed i) ha
+
+ and logic h = logic_atom h.hval
end
@@ -728,9 +1443,13 @@ module Trace = SmtTrace.MakeOpt(Form)
let mk_ftype cod dom =
let typeb = Lazy.force ctype in
let typea = mklApp clist [|typeb|] in
- let a = Array.fold_right (fun bt acc -> mklApp ccons [|typeb; SmtBtype.to_coq bt; acc|]) cod (mklApp cnil [|typeb|]) in
+ let a = Array.fold_right
+ (fun bt acc -> mklApp ccons [|typeb; SmtBtype.to_coq bt; acc|])
+ cod (mklApp cnil [|typeb|]) in
let b = SmtBtype.to_coq dom in
mklApp cpair [|typea;typeb;a;b|]
-let make_t_i rt = SmtBtype.interp_tbl rt
-let make_t_func ro t_i = Op.interp_tbl (mklApp ctval [|t_i|]) (fun cod dom value -> mklApp cTval [|t_i; mk_ftype cod dom; value|]) ro
+let make_t_i = SmtBtype.make_t_i
+let make_t_func ro t_i =
+ Op.interp_tbl (mklApp ctval [|t_i|])
+ (fun cod dom value -> mklApp cTval [|t_i; mk_ftype cod dom; value|]) ro
generated by cgit (git 2.34.1) at 2024-06-28 18:44:28 +0000