aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace
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
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')
-rw-r--r--src/trace/coqTerms.ml297
-rw-r--r--src/trace/coqTerms.mli186
-rw-r--r--src/trace/satAtom.ml13
-rw-r--r--src/trace/satAtom.mli84
-rw-r--r--src/trace/smtAtom.ml1143
-rw-r--r--src/trace/smtAtom.mli148
-rw-r--r--src/trace/smtBtype.ml216
-rw-r--r--src/trace/smtBtype.mli64
-rw-r--r--src/trace/smtCertif.ml203
-rw-r--r--src/trace/smtCertif.mli215
-rw-r--r--src/trace/smtCnf.ml12
-rw-r--r--src/trace/smtCnf.mli12
-rw-r--r--src/trace/smtCommands.ml708
-rw-r--r--src/trace/smtCommands.mli143
-rw-r--r--src/trace/smtForm.ml437
-rw-r--r--src/trace/smtForm.mli25
-rw-r--r--src/trace/smtMisc.ml32
-rw-r--r--src/trace/smtMisc.mli16
-rw-r--r--src/trace/smtTrace.ml91
-rw-r--r--src/trace/smtTrace.mli29
20 files changed, 3191 insertions, 883 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 96d5a69..76f213b 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.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,7 +12,8 @@
open Coqlib
-let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
+let gen_constant modules constant =
+ lazy (gen_constant_in_modules "SMT" modules constant)
(* Int63 *)
let cint = Structures.cint
@@ -25,6 +22,11 @@ let ceq63 = gen_constant Structures.int63_modules "eqb"
(* PArray *)
let carray = gen_constant Structures.parray_modules "array"
+(* nat *)
+let cnat = gen_constant init_modules "nat"
+let cO = gen_constant init_modules "O"
+let cS = gen_constant init_modules "S"
+
(* Positive *)
let positive_modules = [["Coq";"Numbers";"BinNums"];
["Coq";"PArith";"BinPosDef";"Pos"]]
@@ -35,6 +37,16 @@ let cxO = gen_constant positive_modules "xO"
let cxH = gen_constant positive_modules "xH"
let ceqbP = gen_constant positive_modules "eqb"
+(* N *)
+let n_modules = [["Coq";"NArith";"BinNat";"N"]]
+
+let cN = gen_constant positive_modules "N"
+let cN0 = gen_constant positive_modules "N0"
+let cNpos = gen_constant positive_modules "Npos"
+
+let cof_nat = gen_constant n_modules "of_nat"
+
+
(* Z *)
let z_modules = [["Coq";"Numbers";"BinNums"];
["Coq";"ZArith";"BinInt"];
@@ -52,7 +64,8 @@ let cltb = gen_constant z_modules "ltb"
let cleb = gen_constant z_modules "leb"
let cgeb = gen_constant z_modules "geb"
let cgtb = gen_constant z_modules "gtb"
-let ceqbZ = gen_constant z_modules "eqb"
+let ceqbZ = gen_constant z_modules "eqb"
+let cZeqbsym = gen_constant z_modules "eqb_sym"
(* Booleans *)
let bool_modules = [["Coq";"Bool";"Bool"]]
@@ -67,13 +80,14 @@ let cnegb = gen_constant init_modules "negb"
let cimplb = gen_constant init_modules "implb"
let ceqb = gen_constant bool_modules "eqb"
let cifb = gen_constant bool_modules "ifb"
+let ciff = gen_constant init_modules "iff"
let creflect = gen_constant bool_modules "reflect"
(* Lists *)
let clist = gen_constant init_modules "list"
let cnil = gen_constant init_modules "nil"
let ccons = gen_constant init_modules "cons"
-
+let clength = gen_constant init_modules "length"
(* Option *)
let coption = gen_constant init_modules "option"
@@ -82,9 +96,16 @@ let cNone = gen_constant init_modules "None"
(* Pairs *)
let cpair = gen_constant init_modules "pair"
+let cprod = gen_constant init_modules "prod"
(* Dependent pairs *)
let csigT = gen_constant init_modules "sigT"
+let cprojT1 = gen_constant init_modules "projT1"
+let cprojT2 = gen_constant init_modules "projT2"
+let cprojT3 = gen_constant init_modules "projT3"
+
+let csigT2 = gen_constant init_modules "sigT2"
+let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2"
(* Logical Operators *)
let cnot = gen_constant init_modules "not"
@@ -93,8 +114,43 @@ let crefl_equal = gen_constant init_modules "eq_refl"
let cconj = gen_constant init_modules "conj"
let cand = gen_constant init_modules "and"
-(* SMT_terms *)
+(* Bit vectors *)
+let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]]
+let cbitvector = gen_constant bv_modules "bitvector"
+let cof_bits = gen_constant bv_modules "of_bits"
+let c_of_bits = gen_constant bv_modules "_of_bits"
+let cbitOf = gen_constant bv_modules "bitOf"
+let cbv_eq = gen_constant bv_modules "bv_eq"
+let cbv_not = gen_constant bv_modules "bv_not"
+let cbv_neg = gen_constant bv_modules "bv_neg"
+let cbv_and = gen_constant bv_modules "bv_and"
+let cbv_or = gen_constant bv_modules "bv_or"
+let cbv_xor = gen_constant bv_modules "bv_xor"
+let cbv_add = gen_constant bv_modules "bv_add"
+let cbv_mult = gen_constant bv_modules "bv_mult"
+let cbv_ult = gen_constant bv_modules "bv_ult"
+let cbv_slt = gen_constant bv_modules "bv_slt"
+let cbv_concat = gen_constant bv_modules "bv_concat"
+let cbv_extr = gen_constant bv_modules "bv_extr"
+let cbv_zextn = gen_constant bv_modules "bv_zextn"
+let cbv_sextn = gen_constant bv_modules "bv_sextn"
+let cbv_shl = gen_constant bv_modules "bv_shl"
+let cbv_shr = gen_constant bv_modules "bv_shr"
+
+
+(* Arrays *)
+let array_modules = [["SMTCoq";"array";"FArray"]]
+let cfarray = gen_constant array_modules "FArray.farray"
+let cselect = gen_constant array_modules "select"
+let cstore = gen_constant array_modules "store"
+let cdiff = gen_constant array_modules "diff"
+let cequalarray = gen_constant array_modules "FArray.equal"
+
+(* OrderedType *)
+let cOrderedTypeCompare =
+ gen_constant [["Coq";"Structures";"OrderedType"]] "Compare"
+(* SMT_terms *)
let smt_modules = [ ["SMTCoq";"Misc"];
["SMTCoq";"State"];
["SMTCoq";"SMT_terms"];
@@ -104,6 +160,7 @@ let smt_modules = [ ["SMTCoq";"Misc"];
]
let cState_C_t = gen_constant [["SMTCoq";"State";"C"]] "t"
+let cState_S_t = gen_constant [["SMTCoq";"State";"S"]] "t"
let cdistinct = gen_constant smt_modules "distinct"
@@ -111,26 +168,56 @@ let ctype = gen_constant smt_modules "type"
let cTZ = gen_constant smt_modules "TZ"
let cTbool = gen_constant smt_modules "Tbool"
let cTpositive = gen_constant smt_modules "Tpositive"
+let cTBV = gen_constant smt_modules "TBV"
+let cTFArray = gen_constant smt_modules "TFArray"
let cTindex = gen_constant smt_modules "Tindex"
-let ctyp_eqb = gen_constant smt_modules "typ_eqb"
-let cTyp_eqb = gen_constant smt_modules "Typ_eqb"
-let cte_carrier = gen_constant smt_modules "te_carrier"
-let cte_eqb = gen_constant smt_modules "te_eqb"
-let ctyp_eqb_of_typ_eqb_param = gen_constant smt_modules "typ_eqb_of_typ_eqb_param"
-let cunit_typ_eqb = gen_constant smt_modules "unit_typ_eqb"
+let ct_i = gen_constant smt_modules "t_i"
+let cinterp_t = gen_constant smt_modules "Typ.interp"
+let cdec_interp = gen_constant smt_modules "dec_interp"
+let cord_interp = gen_constant smt_modules "ord_interp"
+let ccomp_interp = gen_constant smt_modules "comp_interp"
+let cinh_interp = gen_constant smt_modules "inh_interp"
+
+let cinterp_eqb = gen_constant smt_modules "i_eqb"
+let cinterp_eqb_eqb = gen_constant smt_modules "i_eqb_eqb"
+
+let classes_modules = [["SMTCoq";"classes";"SMT_classes"];
+ ["SMTCoq";"classes";"SMT_classes_instances"]]
+
+let ctyp_compdec = gen_constant classes_modules "typ_compdec"
+let cTyp_compdec = gen_constant classes_modules "Typ_compdec"
+let ctyp_compdec_from = gen_constant classes_modules "typ_compdec_from"
+let cunit_typ_compdec = gen_constant classes_modules "unit_typ_compdec"
+let cte_carrier = gen_constant classes_modules "te_carrier"
+let cte_compdec = gen_constant classes_modules "te_compdec"
+let ceqb_of_compdec = gen_constant classes_modules "eqb_of_compdec"
+let cCompDec = gen_constant classes_modules "CompDec"
+
+let cbool_compdec = gen_constant classes_modules "bool_compdec"
+let cZ_compdec = gen_constant classes_modules "Z_compdec"
+let cPositive_compdec = gen_constant classes_modules "Positive_compdec"
+let cBV_compdec = gen_constant classes_modules "BV_compdec"
+let cFArray_compdec = gen_constant classes_modules "FArray_compdec"
let ctval = gen_constant smt_modules "tval"
let cTval = gen_constant smt_modules "Tval"
let cCO_xH = gen_constant smt_modules "CO_xH"
let cCO_Z0 = gen_constant smt_modules "CO_Z0"
+let cCO_BV = gen_constant smt_modules "CO_BV"
let cUO_xO = gen_constant smt_modules "UO_xO"
let cUO_xI = gen_constant smt_modules "UO_xI"
let cUO_Zpos = gen_constant smt_modules "UO_Zpos"
let cUO_Zneg = gen_constant smt_modules "UO_Zneg"
let cUO_Zopp = gen_constant smt_modules "UO_Zopp"
+let cUO_BVbitOf = gen_constant smt_modules "UO_BVbitOf"
+let cUO_BVnot = gen_constant smt_modules "UO_BVnot"
+let cUO_BVneg = gen_constant smt_modules "UO_BVneg"
+let cUO_BVextr = gen_constant smt_modules "UO_BVextr"
+let cUO_BVzextn = gen_constant smt_modules "UO_BVzextn"
+let cUO_BVsextn = gen_constant smt_modules "UO_BVsextn"
let cBO_Zplus = gen_constant smt_modules "BO_Zplus"
let cBO_Zminus = gen_constant smt_modules "BO_Zminus"
@@ -140,6 +227,20 @@ let cBO_Zle = gen_constant smt_modules "BO_Zle"
let cBO_Zge = gen_constant smt_modules "BO_Zge"
let cBO_Zgt = gen_constant smt_modules "BO_Zgt"
let cBO_eq = gen_constant smt_modules "BO_eq"
+let cBO_BVand = gen_constant smt_modules "BO_BVand"
+let cBO_BVor = gen_constant smt_modules "BO_BVor"
+let cBO_BVxor = gen_constant smt_modules "BO_BVxor"
+let cBO_BVadd = gen_constant smt_modules "BO_BVadd"
+let cBO_BVmult = gen_constant smt_modules "BO_BVmult"
+let cBO_BVult = gen_constant smt_modules "BO_BVult"
+let cBO_BVslt = gen_constant smt_modules "BO_BVslt"
+let cBO_BVconcat = gen_constant smt_modules "BO_BVconcat"
+let cBO_BVshl = gen_constant smt_modules "BO_BVshl"
+let cBO_BVshr = gen_constant smt_modules "BO_BVshr"
+let cBO_select = gen_constant smt_modules "BO_select"
+let cBO_diffarray = gen_constant smt_modules "BO_diffarray"
+
+let cTO_store = gen_constant smt_modules "TO_store"
let cNO_distinct = gen_constant smt_modules "NO_distinct"
@@ -147,6 +248,7 @@ let catom = gen_constant smt_modules "atom"
let cAcop = gen_constant smt_modules "Acop"
let cAuop = gen_constant smt_modules "Auop"
let cAbop = gen_constant smt_modules "Abop"
+let cAtop = gen_constant smt_modules "Atop"
let cAnop = gen_constant smt_modules "Anop"
let cAapp = gen_constant smt_modules "Aapp"
@@ -161,6 +263,7 @@ let cFxor = gen_constant smt_modules "Fxor"
let cFimp = gen_constant smt_modules "Fimp"
let cFiff = gen_constant smt_modules "Fiff"
let cFite = gen_constant smt_modules "Fite"
+let cFbbT = gen_constant smt_modules "FbbT"
let cis_true = gen_constant smt_modules "is_true"
@@ -172,26 +275,160 @@ let make_certif_ops modules args =
match args with
| Some args -> lazy (SmtMisc.mklApp (gen_constant modules c) args)
| None -> gen_constant modules c in
- (gen_constant "step",
- gen_constant "Res", gen_constant "ImmFlatten",
- gen_constant "CTrue", gen_constant "CFalse",
- gen_constant "BuildDef", gen_constant "BuildDef2",
- gen_constant "BuildProj",
- gen_constant "ImmBuildProj", gen_constant"ImmBuildDef",
+ (gen_constant "step",
+ gen_constant "Res", gen_constant "Weaken", gen_constant "ImmFlatten",
+ gen_constant "CTrue", gen_constant "CFalse",
+ gen_constant "BuildDef", gen_constant "BuildDef2",
+ gen_constant "BuildProj",
+ gen_constant "ImmBuildProj", gen_constant"ImmBuildDef",
gen_constant"ImmBuildDef2",
- gen_constant "EqTr", gen_constant "EqCgr", gen_constant "EqCgrP",
- gen_constant "LiaMicromega", gen_constant "LiaDiseq", gen_constant "SplArith", gen_constant "SplDistinctElim",
+ gen_constant "EqTr", gen_constant "EqCgr", gen_constant "EqCgrP",
+ gen_constant "LiaMicromega", gen_constant "LiaDiseq",
+ gen_constant "SplArith", gen_constant "SplDistinctElim",
+ gen_constant "BBVar", gen_constant "BBConst",
+ gen_constant "BBOp", gen_constant "BBNot", gen_constant "BBEq",
+ gen_constant "BBDiseq",
+ gen_constant "BBNeg", gen_constant "BBAdd", gen_constant "BBMul",
+ gen_constant "BBUlt", gen_constant "BBSlt", gen_constant "BBConcat",
+ gen_constant "BBExtract", gen_constant "BBZextend", gen_constant "BBSextend",
+ gen_constant "BBShl", gen_constant "BBShr",
+ gen_constant "RowEq", gen_constant "RowNeq", gen_constant "Ext",
gen_constant "Hole", gen_constant "ForallInst")
-
-(** Useful construction *)
-let ceq_refl_true =
+(** Useful constructions *)
+
+let ceq_refl_true =
lazy (SmtMisc.mklApp crefl_equal [|Lazy.force cbool;Lazy.force ctrue|])
let eq_refl_true () = Lazy.force ceq_refl_true
-let vm_cast_true t =
+let vm_cast_true_no_check t =
Term.mkCast(eq_refl_true (),
- Term.VMcast,
- SmtMisc.mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|])
+ Term.VMcast,
+ SmtMisc.mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|])
+
+(* This version checks convertibility right away instead of delaying it at
+ Qed. This allows to report issues to the user as soon as he/she runs one of
+ SMTCoq's tactics. *)
+let vm_cast_true env t =
+ try
+ Structures.vm_conv Reduction.CUMUL env
+ (SmtMisc.mklApp ceq
+ [|Lazy.force cbool; Lazy.force ctrue; Lazy.force ctrue|])
+ (SmtMisc.mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]);
+ vm_cast_true_no_check t
+ with Reduction.NotConvertible ->
+ Structures.error ("SMTCoq was not able to check the proof certificate.")
+
+
+(* Compute a nat *)
+let rec mkNat = function
+ | 0 -> Lazy.force cO
+ | i -> SmtMisc.mklApp cS [|mkNat (i-1)|]
+
+(* Compute a positive *)
+let rec mkPositive = function
+ | 1 -> Lazy.force cxH
+ | i ->
+ let c = if (i mod 2) = 0 then cxO else cxI in
+ SmtMisc.mklApp c [|mkPositive (i / 2)|]
+
+(* Compute a N *)
+let mkN = function
+ | 0 -> Lazy.force cN0
+ | i -> SmtMisc.mklApp cNpos [|mkPositive i|]
+
+(* Compute a Boolean *)
+let rec mkBool = function
+ | true -> Lazy.force ctrue
+ | false -> Lazy.force cfalse
+
+(* Compute a Boolean list *)
+let rec mk_bv_list = function
+ | [] -> SmtMisc.mklApp cnil [|Lazy.force cbool|]
+ | b :: bv ->
+ SmtMisc.mklApp ccons [|Lazy.force cbool; mkBool b; mk_bv_list bv|]
+
+
+(* Reification *)
+
+let mk_bool b =
+ let c, args = Term.decompose_app b in
+ if Term.eq_constr c (Lazy.force ctrue) then true
+ else if Term.eq_constr c (Lazy.force cfalse) then false
+ else assert false
+
+let rec mk_bool_list bs =
+ let c, args = Term.decompose_app bs in
+ if Term.eq_constr c (Lazy.force cnil) then []
+ else if Term.eq_constr c (Lazy.force ccons) then
+ match args with
+ | [_; b; bs] -> mk_bool b :: mk_bool_list bs
+ | _ -> assert false
+ else assert false
+
+let rec mk_nat n =
+ let c, args = Term.decompose_app n in
+ if Term.eq_constr c (Lazy.force cO) then
+ 0
+ else if Term.eq_constr c (Lazy.force cS) then
+ match args with
+ | [n] -> (mk_nat n) + 1
+ | _ -> assert false
+ else assert false
+
+let rec mk_positive n =
+ let c, args = Term.decompose_app n in
+ if Term.eq_constr c (Lazy.force cxH) then
+ 1
+ else if Term.eq_constr c (Lazy.force cxO) then
+ match args with
+ | [n] -> 2 * (mk_positive n)
+ | _ -> assert false
+ else if Term.eq_constr c (Lazy.force cxI) then
+ match args with
+ | [n] -> 2 * (mk_positive n) + 1
+ | _ -> assert false
+ else assert false
+
+
+let mk_N n =
+ let c, args = Term.decompose_app n in
+ if Term.eq_constr c (Lazy.force cN0) then
+ 0
+ else if Term.eq_constr c (Lazy.force cNpos) then
+ match args with
+ | [n] -> mk_positive n
+ | _ -> assert false
+ else assert false
+
+
+let mk_Z n =
+ let c, args = Term.decompose_app n in
+ if Term.eq_constr c (Lazy.force cZ0) then 0
+ else if Term.eq_constr c (Lazy.force cZpos) then
+ match args with
+ | [n] -> mk_positive n
+ | _ -> assert false
+ else if Term.eq_constr c (Lazy.force cZneg) then
+ match args with
+ | [n] -> - mk_positive n
+ | _ -> assert false
+ else assert false
+
+
+(* size of bivectors are either N.of_nat (length l) or an N *)
+let mk_bvsize n =
+ let c, args = Term.decompose_app n in
+ if Term.eq_constr c (Lazy.force cof_nat) then
+ match args with
+ | [nl] ->
+ let c, args = Term.decompose_app nl in
+ if Term.eq_constr c (Lazy.force clength) then
+ match args with
+ | [_; l] -> List.length (mk_bool_list l)
+ | _ -> assert false
+ else assert false
+ | _ -> assert false
+ else mk_N n
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index 7d7fe6a..b21bef8 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -1,14 +1,43 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
val gen_constant : string list list -> string -> Term.constr lazy_t
+
+(* Int63 *)
val cint : Term.constr lazy_t
val ceq63 : Term.constr lazy_t
+
+(* PArray *)
val carray : Term.constr lazy_t
-val positive_modules : string list list
+
+(* nat *)
+val cnat : Term.constr lazy_t
+val cO : Term.constr lazy_t
+val cS : Term.constr lazy_t
+
+(* Positive *)
val cpositive : Term.constr lazy_t
val cxI : Term.constr lazy_t
val cxO : Term.constr lazy_t
val cxH : Term.constr lazy_t
val ceqbP : Term.constr lazy_t
-val z_modules : string list list
+
+(* N *)
+val cN : Term.constr lazy_t
+val cN0 : Term.constr lazy_t
+val cNpos : Term.constr lazy_t
+val cof_nat : Term.constr lazy_t
+
+(* Z *)
val cZ : Term.constr lazy_t
val cZ0 : Term.constr lazy_t
val cZpos : Term.constr lazy_t
@@ -22,7 +51,8 @@ val cleb : Term.constr lazy_t
val cgeb : Term.constr lazy_t
val cgtb : Term.constr lazy_t
val ceqbZ : Term.constr lazy_t
-val bool_modules : string list list
+
+(* Booleans *)
val cbool : Term.constr lazy_t
val ctrue : Term.constr lazy_t
val cfalse : Term.constr lazy_t
@@ -33,43 +63,119 @@ val cnegb : Term.constr lazy_t
val cimplb : Term.constr lazy_t
val ceqb : Term.constr lazy_t
val cifb : Term.constr lazy_t
+val ciff : Term.constr lazy_t
val creflect : Term.constr lazy_t
+
+(* Lists *)
val clist : Term.constr lazy_t
val cnil : Term.constr lazy_t
val ccons : Term.constr lazy_t
+val clength : Term.constr lazy_t
+
+(* Option *)
val coption : Term.constr lazy_t
val cSome : Term.constr lazy_t
val cNone : Term.constr lazy_t
+
+(* Pairs *)
val cpair : Term.constr lazy_t
+val cprod : Term.constr lazy_t
+
+(* Dependent pairs *)
val csigT : Term.constr lazy_t
+
+(* Logical Operators *)
val cnot : Term.constr lazy_t
val ceq : Term.constr lazy_t
val crefl_equal : Term.constr lazy_t
val cconj : Term.constr lazy_t
val cand : Term.constr lazy_t
-val smt_modules : string list list
+
+(* Bit vectors *)
+val cbitvector : Term.constr lazy_t
+val cof_bits : Term.constr lazy_t
+val cbitOf : Term.constr lazy_t
+val cbv_eq : Term.constr lazy_t
+val cbv_not : Term.constr lazy_t
+val cbv_neg : Term.constr lazy_t
+val cbv_and : Term.constr lazy_t
+val cbv_or : Term.constr lazy_t
+val cbv_xor : Term.constr lazy_t
+val cbv_add : Term.constr lazy_t
+val cbv_mult : Term.constr lazy_t
+val cbv_ult : Term.constr lazy_t
+val cbv_slt : Term.constr lazy_t
+val cbv_concat : Term.constr lazy_t
+val cbv_extr : Term.constr lazy_t
+val cbv_zextn : Term.constr lazy_t
+val cbv_sextn : Term.constr lazy_t
+val cbv_shl : Term.constr lazy_t
+val cbv_shr : Term.constr lazy_t
+
+(* Arrays *)
+val cfarray : Term.constr lazy_t
+val cselect : Term.constr lazy_t
+val cstore : Term.constr lazy_t
+val cdiff : Term.constr lazy_t
+val cequalarray : Term.constr lazy_t
+
+(* OrderedType *)
+
+(* SMT_terms *)
val cState_C_t : Term.constr lazy_t
+val cState_S_t : Term.constr lazy_t
+
val cdistinct : Term.constr lazy_t
+
val ctype : Term.constr lazy_t
val cTZ : Term.constr lazy_t
val cTbool : Term.constr lazy_t
val cTpositive : Term.constr lazy_t
+val cTBV : Term.constr lazy_t
+val cTFArray : Term.constr lazy_t
val cTindex : Term.constr lazy_t
-val ctyp_eqb : Term.constr lazy_t
-val cTyp_eqb : Term.constr lazy_t
+
+val cinterp_t : Term.constr lazy_t
+val cdec_interp : Term.constr lazy_t
+val cord_interp : Term.constr lazy_t
+val ccomp_interp : Term.constr lazy_t
+val cinh_interp : Term.constr lazy_t
+
+val cinterp_eqb : Term.constr lazy_t
+
+val ctyp_compdec : Term.constr lazy_t
+val cTyp_compdec : Term.constr lazy_t
+val cunit_typ_compdec : Term.constr lazy_t
val cte_carrier : Term.constr lazy_t
-val cte_eqb : Term.constr lazy_t
-val ctyp_eqb_of_typ_eqb_param : Term.constr lazy_t
-val cunit_typ_eqb : Term.constr lazy_t
+val cte_compdec : Term.constr lazy_t
+val ceqb_of_compdec : Term.constr lazy_t
+val cCompDec : Term.constr lazy_t
+
+val cbool_compdec : Term.constr lazy_t
+val cZ_compdec : Term.constr lazy_t
+val cPositive_compdec : Term.constr lazy_t
+val cBV_compdec : Term.constr lazy_t
+val cFArray_compdec : Term.constr lazy_t
+
val ctval : Term.constr lazy_t
val cTval : Term.constr lazy_t
+
val cCO_xH : Term.constr lazy_t
val cCO_Z0 : Term.constr lazy_t
+val cCO_BV : Term.constr lazy_t
+
val cUO_xO : Term.constr lazy_t
val cUO_xI : Term.constr lazy_t
val cUO_Zpos : Term.constr lazy_t
val cUO_Zneg : Term.constr lazy_t
val cUO_Zopp : Term.constr lazy_t
+val cUO_BVbitOf : Term.constr lazy_t
+val cUO_BVnot : Term.constr lazy_t
+val cUO_BVneg : Term.constr lazy_t
+val cUO_BVextr : Term.constr lazy_t
+val cUO_BVzextn : Term.constr lazy_t
+val cUO_BVsextn : Term.constr lazy_t
+
val cBO_Zplus : Term.constr lazy_t
val cBO_Zminus : Term.constr lazy_t
val cBO_Zmult : Term.constr lazy_t
@@ -78,13 +184,31 @@ val cBO_Zle : Term.constr lazy_t
val cBO_Zge : Term.constr lazy_t
val cBO_Zgt : Term.constr lazy_t
val cBO_eq : Term.constr lazy_t
+val cBO_BVand : Term.constr lazy_t
+val cBO_BVor : Term.constr lazy_t
+val cBO_BVxor : Term.constr lazy_t
+val cBO_BVadd : Term.constr lazy_t
+val cBO_BVmult : Term.constr lazy_t
+val cBO_BVult : Term.constr lazy_t
+val cBO_BVslt : Term.constr lazy_t
+val cBO_BVconcat : Term.constr lazy_t
+val cBO_BVshl : Term.constr lazy_t
+val cBO_BVshr : Term.constr lazy_t
+val cBO_select : Term.constr lazy_t
+val cBO_diffarray : Term.constr lazy_t
+
+val cTO_store : Term.constr lazy_t
+
val cNO_distinct : Term.constr lazy_t
+
val catom : Term.constr lazy_t
val cAcop : Term.constr lazy_t
val cAuop : Term.constr lazy_t
val cAbop : Term.constr lazy_t
+val cAtop : Term.constr lazy_t
val cAnop : Term.constr lazy_t
val cAapp : Term.constr lazy_t
+
val cform : Term.constr lazy_t
val cFatom : Term.constr lazy_t
val cFtrue : Term.constr lazy_t
@@ -96,19 +220,43 @@ val cFxor : Term.constr lazy_t
val cFimp : Term.constr lazy_t
val cFiff : Term.constr lazy_t
val cFite : Term.constr lazy_t
+val cFbbT : Term.constr lazy_t
+
val cis_true : Term.constr lazy_t
+
val cvalid_sat_checker : Term.constr lazy_t
val cinterp_var_sat_checker : Term.constr lazy_t
+
val make_certif_ops :
- string list list ->
- Term.constr array option ->
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t
+ string list list ->
+ Term.constr array option ->
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+ Term.constr lazy_t * Term.constr lazy_t
+
+(* Some constructions *)
val ceq_refl_true : Term.constr lazy_t
val eq_refl_true : unit -> Term.constr
-val vm_cast_true : Term.constr -> Term.constr
+val vm_cast_true_no_check : Term.constr -> Term.constr
+val vm_cast_true : Environ.env -> Term.constr -> Term.constr
+val mkNat : int -> Term.constr
+val mkN : int -> Term.constr
+val mk_bv_list : bool list -> Term.constr
+
+(* Reification *)
+val mk_bool : Term.constr -> bool
+val mk_bool_list : Term.constr -> bool list
+val mk_nat : Term.constr -> int
+val mk_N : Term.constr -> int
+val mk_bvsize : Term.constr -> int
diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
index f65e850..549462c 100644
--- a/src/trace/satAtom.ml
+++ b/src/trace/satAtom.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 *)
(* *)
@@ -27,6 +23,7 @@ module Atom =
let equal a1 a2 = a1 == a2
let is_bool_type a = true
+ let is_bv_type a = false
type reify_tbl =
{ mutable count : int;
@@ -56,6 +53,10 @@ module Atom =
let interp_tbl reify =
Structures.mkArray (Lazy.force cbool, atom_tbl reify)
+ let logic _ = SL.empty
+
+ let to_smt = Format.pp_print_int
+
end
module Form = SmtForm.Make(Atom)
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
index 4577d42..b5fe759 100644
--- a/src/trace/satAtom.mli
+++ b/src/trace/satAtom.mli
@@ -1,52 +1,42 @@
-module Atom :
- sig
- type t = int
- val index : 'a -> 'a
- val equal : 'a -> 'a -> bool
- val is_bool_type : 'a -> bool
- type reify_tbl = {
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+module Atom : sig
+ type t = int
+ val index : t -> int
+
+ val equal : t -> t -> bool
+
+ val is_bool_type : t -> bool
+ val is_bv_type : t -> bool
+ val to_smt : Format.formatter -> t -> unit
+ val logic : t -> SmtMisc.logic
+
+ val is_bool_type : t -> bool
+ type reify_tbl = {
mutable count : int;
- tbl : (Term.constr, int) Hashtbl.t;
+ tbl : (Term.constr, t) Hashtbl.t;
}
- val create : unit -> reify_tbl
- val declare : reify_tbl -> Term.constr -> int
- val get : reify_tbl -> Term.constr -> int
- val atom_tbl : reify_tbl -> Term.constr array
- val interp_tbl : reify_tbl -> Term.constr
- end
-module Form :
- sig
- type hatom = Atom.t
- type t = SmtForm.Make(Atom).t
- type pform = (hatom, t) SmtForm.gen_pform
- val pform_true : pform
- val pform_false : pform
- val equal : t -> t -> bool
- val to_lit : t -> int
- val index : t -> int
- val pform : t -> pform
- val neg : t -> t
- val is_pos : t -> bool
- val is_neg : t -> bool
- val to_string : ?pi:bool -> (hatom -> string) -> t -> string
- val to_smt : (hatom -> string) -> Format.formatter -> t -> unit
- exception NotWellTyped of pform
- type reify = SmtForm.Make(Atom).reify
- val create : unit -> reify
- val clear : reify -> unit
- val get : ?declare:bool -> reify -> pform -> t
- val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
- val hash_hform : (hatom -> hatom) -> reify -> t -> t
- val flatten : reify -> t -> t
- val to_coq : t -> Term.constr
- val pform_tbl : reify -> pform array
- val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
- val interp_tbl : reify -> Term.constr * Term.constr
- val nvars : reify -> int
- val interp_to_coq :
- (hatom -> Term.constr) ->
- (int, Term.constr) Hashtbl.t -> t -> Term.constr
- end
+ val create : unit -> reify_tbl
+ val declare : reify_tbl -> Term.constr -> t
+ val get : reify_tbl -> Term.constr -> t
+ val atom_tbl : reify_tbl -> Term.constr array
+ val interp_tbl : reify_tbl -> Term.constr
+end
+
+
+module Form : SmtForm.FORM with type hatom = Atom.t
+
+
module Trace :
sig
val share_value : Form.t SmtCertif.clause -> unit
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
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index 47734fb..a542ad6 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -1,34 +1,38 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
+
open SmtBtype
(** Operators *)
-type cop =
+type cop =
| CO_xH
| CO_Z0
+ | CO_BV of bool list
type uop =
| UO_xO
| UO_xI
- | UO_Zpos
+ | UO_Zpos
| UO_Zneg
| UO_Zopp
-
-type bop =
+ | 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
@@ -37,21 +41,37 @@ type bop =
| 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
-type indexed_op
-
type index = Index of int
| Rel_name of string
+type indexed_op
+
val dummy_indexed_op: index -> btype array -> btype -> indexed_op
val indexed_op_index : indexed_op -> int
+val debruijn_indexed_op : int -> btype -> indexed_op
module Op :
sig
-
+
type reify_tbl
val create : unit -> reify_tbl
@@ -61,93 +81,117 @@ module Op :
val of_coq : reify_tbl -> Term.constr -> indexed_op
- val interp_tbl : Term.constr ->
- (btype array -> btype -> Term.constr -> Term.constr) ->
- reify_tbl -> Term.constr
+ val interp_tbl : Term.constr ->
+ (btype array -> btype -> Term.constr -> Term.constr) ->
+ reify_tbl -> Term.constr
val to_list : reify_tbl -> (int * (btype array) * btype * indexed_op) list
+ val logic_ro : reify_tbl -> SmtMisc.logic
+
end
(** Definition of atoms *)
-type hatom
+type hatom
-type atom =
+type atom =
| Acop of cop
- | Auop of uop * hatom
- | Abop of bop * hatom * hatom
+ | 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
-module Atom :
- sig
+module Atom :
+ sig
type t = hatom
- val equal : hatom -> hatom -> bool
+ val equal : t -> t -> bool
- val index : hatom -> int
+ val index : t -> int
- val atom : hatom -> atom
-
- val type_of : hatom -> btype
+ val atom : t -> atom
+
+ val type_of : t -> btype
- val to_string : ?pi:bool -> hatom -> string
-
val to_smt : Format.formatter -> t -> unit
exception NotWellTyped of atom
- type reify_tbl
+ type reify_tbl
val create : unit -> reify_tbl
val clear : reify_tbl -> unit
- val get : ?declare:bool -> reify_tbl -> atom -> hatom
+ val get : ?declare:bool -> reify_tbl -> atom -> t
- val mk_eq : reify_tbl -> bool -> btype -> hatom -> hatom -> hatom
+ val mk_neg : reify_tbl -> t -> t
- val mk_neg : reify_tbl -> hatom -> hatom
-
- val hash_hatom : reify_tbl -> hatom -> hatom
+ val hash_hatom : reify_tbl -> t -> t
(** for debugging purposes **)
val copy : reify_tbl -> reify_tbl
-
+
val print_atoms : reify_tbl -> string -> unit
-
+
(** Given a coq term, build the corresponding atom *)
val of_coq : ?hash:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
- reify_tbl -> Environ.env -> Evd.evar_map -> Term.constr -> t
+ reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Term.constr -> t
+
+ val get_coq_term_op : int -> Term.constr
- val to_coq : hatom -> Term.constr
+ val to_coq : t -> Term.constr
val to_array : reify_tbl -> 'a -> (atom -> 'a) -> 'a array
val interp_tbl : reify_tbl -> Term.constr
- val interp_to_coq : (int, Term.constr) Hashtbl.t ->
+ val interp_to_coq : Term.constr -> (int, Term.constr) Hashtbl.t ->
t -> Term.constr
+ val logic : t -> SmtMisc.logic
+
(* Generation of atoms *)
- val hatom_Z_of_int : reify_tbl -> int -> hatom
- val hatom_Z_of_bigint : reify_tbl -> Big_int.big_int -> hatom
-
- val mk_lt : reify_tbl -> bool -> hatom -> hatom -> hatom
- val mk_le : reify_tbl -> bool -> hatom -> hatom -> hatom
- val mk_gt : reify_tbl -> bool -> hatom -> hatom -> hatom
- val mk_ge : reify_tbl -> bool -> hatom -> hatom -> hatom
- val mk_plus : reify_tbl -> bool -> hatom -> hatom -> hatom
- val mk_minus : reify_tbl -> bool -> hatom -> hatom -> hatom
- val mk_mult : reify_tbl -> bool -> hatom -> hatom -> hatom
- val mk_opp : reify_tbl -> ?declare:bool -> hatom -> hatom
- val mk_distinct : reify_tbl -> btype -> ?declare:bool -> hatom array -> hatom
+ val hatom_Z_of_int : reify_tbl -> int -> t
+ val hatom_Z_of_bigint : reify_tbl -> Big_int.big_int -> t
+ val mk_eq : reify_tbl -> ?declare:bool -> btype -> t -> t -> t
+ val mk_lt : reify_tbl -> ?declare:bool -> t -> t -> t
+ val mk_le : reify_tbl -> ?declare:bool -> t -> t -> t
+ val mk_gt : reify_tbl -> ?declare:bool -> t -> t -> t
+ val mk_ge : reify_tbl -> ?declare:bool -> t -> t -> t
+ val mk_plus : reify_tbl -> ?declare:bool -> t -> t -> t
+ val mk_minus : reify_tbl -> ?declare:bool -> t -> t -> t
+ val mk_mult : reify_tbl -> ?declare:bool -> t -> t -> t
+ val mk_bvand : reify_tbl -> ?declare:bool -> int -> t -> t -> t
+ val mk_bvor : reify_tbl -> ?declare:bool -> int -> t -> t -> t
+ val mk_bvxor : reify_tbl -> ?declare:bool -> int -> t -> t -> t
+ val mk_bvadd : reify_tbl -> ?declare:bool -> int -> t -> t -> t
+ val mk_bvmult : reify_tbl -> ?declare:bool -> int -> t -> t -> t
+ val mk_bvult : reify_tbl -> ?declare:bool -> int -> t -> t -> t
+ val mk_bvslt : reify_tbl -> ?declare:bool -> int -> t -> t -> t
+ val mk_bvconcat : reify_tbl -> ?declare:bool -> int -> int -> t -> t -> t
+ val mk_opp : reify_tbl -> ?declare:bool -> t -> t
+ val mk_distinct : reify_tbl -> ?declare:bool -> btype -> t array -> t
+ val mk_bitof : reify_tbl -> ?declare:bool -> int -> int -> t -> t
+ val mk_bvnot : reify_tbl -> ?declare:bool -> int -> t -> t
+ val mk_bvneg : reify_tbl -> ?declare:bool -> int -> t -> t
+ val mk_bvconst : reify_tbl -> bool list -> t
+ val mk_bvextr : reify_tbl -> ?declare:bool -> i:int -> n:int -> s:int -> t -> t
+ val mk_bvzextn : reify_tbl -> ?declare:bool -> s:int -> n:int -> t -> t
+ val mk_bvsextn : reify_tbl -> ?declare:bool -> s:int -> n:int -> t -> t
+ val mk_bvshl : reify_tbl -> ?declare:bool -> int -> t -> t -> t
+ val mk_bvshr : reify_tbl -> ?declare:bool -> int -> t -> t -> t
+ val mk_select : reify_tbl -> ?declare:bool -> btype -> btype -> t -> t -> t
+ val mk_diffarray : reify_tbl -> ?declare:bool -> btype -> btype -> t -> t -> t
+ val mk_store :
+ reify_tbl -> ?declare:bool -> btype -> btype -> t -> t -> t -> t
end
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index f3245ea..8580ed0 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -1,3 +1,15 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
open SmtMisc
open CoqTerms
@@ -13,6 +25,8 @@ type btype =
| TZ
| Tbool
| Tpositive
+ | TBV of int
+ | TFArray of btype * btype
| Tindex of indexed_type
let index_tbl = Hashtbl.create 17
@@ -26,31 +40,45 @@ let index_to_coq i =
let indexed_type_of_int i =
{index = i; hval = index_to_coq i }
-
-let equal t1 t2 =
+
+let rec equal t1 t2 =
match t1,t2 with
- | Tindex i, Tindex j -> i.index == j.index
- | _ -> t1 == t2
+ | Tindex i, Tindex j -> i.index == j.index
+ | TBV i, TBV j -> i == j
+ | TFArray (ti, te), TFArray (ti', te') -> equal ti ti' && equal te te'
+ | _ -> t1 == t2
-let to_coq = function
+let rec to_coq = function
| TZ -> Lazy.force cTZ
| Tbool -> Lazy.force cTbool
| Tpositive -> Lazy.force cTpositive
+ | TBV n -> mklApp cTBV [|mkN n|]
| Tindex i -> index_to_coq i.index
-
-let to_string = function
- | TZ -> "Int"
- | Tbool -> "Bool"
- | Tpositive -> "Int"
- | Tindex i -> "Tindex_" ^ string_of_int i.index
-
-let to_smt fmt b = Format.fprintf fmt "%s" (to_string b)
+ | TFArray (ti, te) ->
+ mklApp cTFArray [|to_coq ti; to_coq te|]
+
+let rec to_smt fmt = function
+ | TZ -> Format.fprintf fmt "Int"
+ | Tbool -> Format.fprintf fmt "Bool"
+ | Tpositive -> Format.fprintf fmt "Int"
+ | TBV i -> Format.fprintf fmt "(_ BitVec %i)" i
+ | Tindex i -> Format.fprintf fmt "Tindex_%i" i.index
+ | TFArray (ti, te) ->
+ Format.fprintf fmt "(Array %a %a)" to_smt ti to_smt te
+
+let rec logic = function
+ | TZ | Tpositive -> SL.singleton LLia
+ | Tbool -> SL.empty
+ | TBV _ -> SL.singleton LBitvectors
+ | Tindex _ -> SL.singleton LUF
+ | TFArray (ti, te) -> SL.add LArrays (SL.union (logic ti) (logic te))
(* reify table *)
type reify_tbl =
{ mutable count : int;
tbl : (Term.constr, btype) Hashtbl.t;
- mutable cuts : (Structures.names_id_t * Term.types) list
+ mutable cuts : (Structures.names_id_t * Term.types) list;
+ unsup_tbl : (btype, btype) Hashtbl.t;
}
let create () =
@@ -60,58 +88,148 @@ let create () =
(* Hashtbl.add htbl (Lazy.force cpositive) Tpositive; *)
{ count = 0;
tbl = htbl;
- cuts = [] }
-
-let get_cuts reify = reify.cuts
-
-let declare reify t typ_eqb =
- (* TODO: allows to have only typ_eqb *)
- assert (not (Hashtbl.mem reify.tbl t));
- let res = Tindex {index = reify.count; hval = typ_eqb} in
- Hashtbl.add reify.tbl t res;
- reify.count <- reify.count + 1;
- res
+ cuts = [];
+ unsup_tbl = Hashtbl.create 17;
+ }
-let of_coq reify t =
- try
- Hashtbl.find reify.tbl t
- with | Not_found ->
- let n = string_of_int (List.length reify.cuts) in
- let eq_name = Names.id_of_string ("eq"^n) in
- let eq_var = Term.mkVar eq_name in
- let eq_ty = Term.mkArrow t (Term.mkArrow t (Lazy.force cbool)) in
+(* Should we give a way to clear it? *)
+let op_coq_types = Hashtbl.create 17
+let get_coq_type_op = Hashtbl.find op_coq_types
- let eq = mkName "eq" in
- let x = mkName "x" in
- let y = mkName "y" in
- let req = Term.mkRel 3 in
- let rx = Term.mkRel 2 in
- let ry = Term.mkRel 1 in
- let refl_ty = Term.mkLambda (eq, eq_ty, Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|]; Term.mkApp (req, [|rx;ry|])|]))) in
- let pair_ty = mklApp csigT [|eq_ty; refl_ty|] in
+(* let logic_of_coq reify t = logic (of_coq reify t) *)
- reify.cuts <- (eq_name, pair_ty)::reify.cuts;
- let ce = mklApp ctyp_eqb_of_typ_eqb_param [|t; eq_var|] in
- declare reify t ce
let interp_tbl reify =
- let t = Array.make (reify.count + 1) (Lazy.force cunit_typ_eqb) in
+ let t = Array.make (reify.count + 1) (Lazy.force cunit_typ_compdec) in
let set _ = function
| Tindex it -> t.(it.index) <- it.hval
| _ -> () in
Hashtbl.iter set reify.tbl;
- Structures.mkArray (Lazy.force ctyp_eqb, t)
+ Structures.mkArray (Lazy.force ctyp_compdec, t)
+
let to_list reify =
let set _ t acc = match t with
- | Tindex it -> (it.index,it)::acc
- | _ -> acc in
+ | Tindex it -> (it.index,it)::acc
+ | _ -> acc in
Hashtbl.fold set reify.tbl []
-let interp_to_coq reify = function
+let make_t_i rt = interp_tbl rt
+
+
+let interp_t t_i t =
+ mklApp cinterp_t [|t_i ; to_coq t|]
+
+let dec_interp t_i t =
+ mklApp cdec_interp [|t_i ; to_coq t|]
+
+let ord_interp t_i t =
+ mklApp cord_interp [|t_i ; to_coq t|]
+
+let comp_interp t_i t =
+ mklApp ccomp_interp [|t_i ; to_coq t|]
+
+let inh_interp t_i t =
+ mklApp cinh_interp [|t_i ; to_coq t|]
+
+let rec interp t_i = function
| TZ -> Lazy.force cZ
| Tbool -> Lazy.force cbool
| Tpositive -> Lazy.force cpositive
+ | TBV n -> mklApp cbitvector [|mkN n|]
| Tindex c -> mklApp cte_carrier [|c.hval|]
+ (* | TFArray _ as t -> interp_t t_i t *)
+ | TFArray (ti,te) ->
+ mklApp cfarray [| interp t_i ti; interp t_i te;
+ ord_interp t_i ti; inh_interp t_i te |]
+
+
+let interp_to_coq reify t = interp (make_t_i reify) t
+
+let get_cuts reify = reify.cuts
+
+let declare reify t typ_compdec =
+ (* TODO: allows to have only typ_compdec *)
+ assert (not (Hashtbl.mem reify.tbl t));
+ let res = Tindex {index = reify.count; hval = typ_compdec} in
+ Hashtbl.add reify.tbl t res;
+ reify.count <- reify.count + 1;
+ res
+
+exception Unknown_type of btype
+
+let check_known ty known_logic =
+ let l = logic ty in
+ if not (SL.subset l known_logic) then raise (Unknown_type ty)
+ else ty
+
+let rec compdec_btype reify = function
+ | Tbool -> Lazy.force cbool_compdec
+ | TZ -> Lazy.force cZ_compdec
+ | Tpositive -> Lazy.force cPositive_compdec
+ | TBV s -> mklApp cBV_compdec [|mkN s|]
+ | TFArray (ti, te) ->
+ mklApp cFArray_compdec
+ [|interp_to_coq reify ti; interp_to_coq reify te;
+ compdec_btype reify ti; compdec_btype reify te|]
+ | Tindex i ->
+ let c, args = Term.decompose_app i.hval in
+ if Term.eq_constr c (Lazy.force cTyp_compdec) then
+ match args with
+ | [_; tic] -> tic
+ | _ -> assert false
+ else assert false
+
+
+let declare_and_compdec reify t ty =
+ try Hashtbl.find reify.unsup_tbl ty
+ with Not_found ->
+ let res =
+ declare reify t (mklApp cTyp_compdec [|t; compdec_btype reify ty|])
+ in
+ Hashtbl.add reify.unsup_tbl ty res;
+ res
+
+
+let rec of_coq reify known_logic t =
+ try
+ let c, args = Term.decompose_app t in
+ if Term.eq_constr c (Lazy.force cbool) ||
+ Term.eq_constr c (Lazy.force cTbool) then Tbool
+ else if Term.eq_constr c (Lazy.force cZ) ||
+ Term.eq_constr c (Lazy.force cTZ) then
+ check_known TZ known_logic
+ else if Term.eq_constr c (Lazy.force cpositive) ||
+ Term.eq_constr c (Lazy.force cTpositive) then
+ check_known Tpositive known_logic
+ else if Term.eq_constr c (Lazy.force cbitvector) ||
+ Term.eq_constr c (Lazy.force cTBV) then
+ match args with
+ | [s] -> check_known (TBV (mk_bvsize s)) known_logic
+ | _ -> assert false
+ else if Term.eq_constr c (Lazy.force cfarray) ||
+ Term.eq_constr c (Lazy.force cTFArray) then
+ match args with
+ | ti :: te :: _ ->
+ let ty = TFArray (of_coq reify known_logic ti,
+ of_coq reify known_logic te) in
+ check_known ty known_logic
+ | _ -> assert false
+ else
+ try Hashtbl.find reify.tbl t
+ with Not_found ->
+ let n = string_of_int (List.length reify.cuts) in
+ let compdec_name = Names.id_of_string ("CompDec"^n) in
+ let compdec_var = Term.mkVar compdec_name in
+ let compdec_type = mklApp cCompDec [| t |]in
+ reify.cuts <- (compdec_name, compdec_type) :: reify.cuts;
+ let ce = mklApp cTyp_compdec [|t; compdec_var|] in
+ let ty = declare reify t ce in
+ (match ty with Tindex h -> Hashtbl.add op_coq_types h.index t | _ -> assert false);
+ ty
+
+ with Unknown_type ty ->
+ try Hashtbl.find reify.tbl t
+ with Not_found -> declare_and_compdec reify t ty
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli
index 29e91bf..559e809 100644
--- a/src/trace/smtBtype.mli
+++ b/src/trace/smtBtype.mli
@@ -1,18 +1,64 @@
-type indexed_type
-val dummy_indexed_type : int -> indexed_type
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
+open SmtMisc
+
+
+type indexed_type = Term.constr gen_hashed
+
+val dummy_indexed_type: int -> indexed_type
val indexed_type_index : indexed_type -> int
val indexed_type_hval : indexed_type -> Term.constr
-type btype = TZ | Tbool | Tpositive | Tindex of indexed_type
-val indexed_type_of_int : int -> indexed_type
+
+type btype =
+ | TZ
+ | Tbool
+ | Tpositive
+ | TBV of int
+ | TFArray of btype * btype
+ | Tindex of indexed_type
+
+val indexed_type_of_int : int -> Term.constr SmtMisc.gen_hashed
+
val equal : btype -> btype -> bool
+
val to_coq : btype -> Term.constr
-val to_string : btype -> string
+
val to_smt : Format.formatter -> btype -> unit
+
type reify_tbl
+
val create : unit -> reify_tbl
-val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
+
val declare : reify_tbl -> Term.constr -> Term.constr -> btype
-val of_coq : reify_tbl -> Term.types -> btype
+
+val of_coq : reify_tbl -> logic -> Term.constr -> btype
+
+val get_coq_type_op : int -> Term.constr
+
val interp_tbl : reify_tbl -> Term.constr
-val to_list : reify_tbl -> (int * indexed_type) list
-val interp_to_coq : 'a -> btype -> Term.constr
+
+val to_list : reify_tbl -> (int * indexed_type) list
+
+val make_t_i : reify_tbl -> Term.constr
+
+val dec_interp : Term.constr -> btype -> Term.constr
+val ord_interp : Term.constr -> btype -> Term.constr
+val comp_interp : Term.constr -> btype -> Term.constr
+val inh_interp : Term.constr -> btype -> Term.constr
+val interp : Term.constr -> btype -> Term.constr
+
+val interp_to_coq : reify_tbl -> btype -> Term.constr
+
+val get_cuts : reify_tbl -> (Structures.names_id_t * Term.types) list
+
+val logic : btype -> logic
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index 275f6d1..b1468e4 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.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 *)
(* *)
@@ -21,6 +17,11 @@ type used = int
type clause_id = int
type 'hform rule =
+ (* Weakening *)
+ | Weaken of 'hform clause * 'hform list
+ (* * weaken : {a_1 ... a_n} --> {a_1 ... a_n b_1 ... b_n} *)
+
+ (* Simplification *)
| ImmFlatten of 'hform clause * 'hform
(* CNF Transformations *)
@@ -108,6 +109,114 @@ type 'hform rule =
(* Elimination of operators *)
| SplDistinctElim of 'hform clause * 'hform
+ (* Bit-blasting *)
+ | BBVar of 'hform
+ (* Bit-blasting a variable:
+
+ ----------------------- bbVar
+ bbT(x, [x0; ...; xn])
+ *)
+ | BBConst of 'hform
+ (* Bit-blasting a constant:
+
+ ----------------------- bbConst
+ bbT(#0100, [0; 0; 1; 0])
+ *)
+ | BBOp of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitwise operations: bbAnd, bbOr, ...
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbAnd
+ bbT(a&b, [a0 /\ b0; ...; an /\ bn])
+ *)
+ | BBNot of 'hform clause * 'hform
+ (* Bit-blasting bitvector not
+ bbT(a, [a0; ...; an])
+ ------------------------------ bbNot
+ bbT(not a, [~a0 ; ...; ~an])
+ *)
+ | BBNeg of 'hform clause * 'hform
+ (* Bit-blasting bitvector negation
+ bbT(a, [a0; ...; an])
+ ------------------------------ bbNot
+ bbT(-a, [...])
+ *)
+ | BBAdd of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector addition
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbAnd
+ bbT(a+b, [...])
+ *)
+ | BBMul of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector multiplication
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbAnd
+ bbT(a*b, [...])
+ *)
+ | BBUlt of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector unsigned comparison
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbAnd
+ bvult a b <-> ...
+ *)
+ | BBSlt of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector signed comparison
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbAnd
+ bvslt a b <-> ...
+ *)
+ | BBConc of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector concatenation
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbConc
+ bbT(concat a b, [a0; ...; an; b0; ...; bn])
+ *)
+ | BBExtr of 'hform clause * 'hform
+ (* Bit-blasting bitvector extraction
+ bbT(a, [a0; ...; an])
+ ----------------------------------- bbExtr
+ bbT(extract i j a, [ai; ...; aj])
+ *)
+ | BBZextn of 'hform clause * 'hform
+ | BBSextn of 'hform clause * 'hform
+ (* Bit-blasting bitvector extensions
+
+ *)
+ | BBShl of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector shift left *)
+ | BBShr of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector shift right *)
+ | BBEq of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting equality
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbEq
+ (a = b) <-> [(a0 <-> b0) /\ ... /\ (an <-> bn)]
+ *)
+
+ | BBDiseq of 'hform
+ (* disequality over constant bitvectors
+
+ ----------------------------- bbDiseq
+ #b000010101 <> #b00000000
+ *)
+
+ | RowEq of 'hform
+ (* Read over write same index
+ ------------------------------- roweq
+ select (store a i v) i = v
+ *)
+
+ | RowNeq of 'hform list
+ (* Read over write other index
+ ------------------------------------------------- rowneq
+ i <> j -> select (store a i v) j = select a j
+ *)
+
+ | Ext of 'hform
+ (* Extensionality over arrays
+ ------------------------------------------------------- ext
+ a = b \/ select a (diff a b) <> select b (diff a b)
+ *)
+
(* Possibility to introduce "holes" in proofs (that should be filled in Coq) *)
| Hole of ('hform clause) list * 'hform list
| Forall_inst of 'hform clause * 'hform
@@ -139,12 +248,26 @@ and 'hform resolution = {
let used_clauses r =
match r with
| ImmBuildProj (c, _) | ImmBuildDef c | ImmBuildDef2 c
- | ImmFlatten (c,_) | SplArith (c,_,_) | SplDistinctElim (c,_)
- | Forall_inst (c, _) | Qf_lemma (c, _) -> [c]
+
+ | Weaken (c,_) | ImmFlatten (c,_)
+ | SplArith (c,_,_) | SplDistinctElim (c,_)
+ | BBNot (c, _) | BBNeg (c, _) | BBExtr (c, _)
+ | BBZextn (c, _) | BBSextn (c, _) -> [c]
+
+ | BBOp (c1,c2,_) | BBAdd (c1,c2,_)
+ | BBMul (c1,c2,_) | BBConc (c1,c2,_)
+ | BBUlt (c1,c2,_) | BBSlt (c1,c2,_)
+ | BBShl (c1,c2,_) | BBShr (c1,c2,_)
+ | BBEq (c1,c2,_) -> [c1;c2]
+
| Hole (cs, _) -> cs
+ | Forall_inst (c, _) | Qf_lemma (c, _) -> [c]
+
| True | False | BuildDef _ | BuildDef2 _ | BuildProj _
| EqTr _ | EqCgr _ | EqCgrP _
- | LiaMicromega _ | LiaDiseq _ -> []
+ | LiaMicromega _ | LiaDiseq _
+ | BBVar _ | BBConst _ | BBDiseq _
+ | RowEq _ | RowNeq _ | Ext _ -> []
(* For debugging certif processing purposes : <add_scertif> <select> <occur> <alloc> *)
let to_string r =
@@ -158,27 +281,47 @@ let to_string r =
"Res [" ^ id1 ^ "; " ^ id2 ^ rest_ids ^"]"
| Other x -> "Other(" ^
begin match x with
- | True -> "True"
- | False -> "False"
- | BuildDef _ -> "BuildDef"
- | BuildDef2 _ -> "BuildDef2"
- | BuildProj _ -> "BuildProj"
- | EqTr _ -> "EqTr"
- | EqCgr _ -> "EqCgr"
- | EqCgrP _ -> "EqCgrP"
- | LiaMicromega _ -> "LiaMicromega"
- | LiaDiseq _ -> "LiaDiseq"
- | Qf_lemma _ -> "Qf_lemma"
-
- | Hole _ -> "Hole"
-
- | ImmFlatten _ -> "ImmFlatten"
- | ImmBuildDef _ -> "ImmBuildDef"
- | ImmBuildDef2 _ -> "ImmBuildDef2"
- | ImmBuildProj _ -> "ImmBuildProj"
- | SplArith _ -> "SplArith"
- | SplDistinctElim _ -> "SplDistinctElim"
- | Forall_inst _ -> "Forall_inst" end ^ ")"
+ | Weaken _ -> "Weaken"
+ | ImmFlatten _ -> "ImmFlatten"
+ | True -> "True"
+ | False -> "False"
+ | BuildDef _ -> "BuildDef"
+ | BuildDef2 _ -> "BuildDef2"
+ | BuildProj _ -> "BuildProj"
+ | ImmBuildDef _ -> "ImmBuildDef"
+ | ImmBuildDef2 _ -> "ImmBuildDef2"
+ | ImmBuildProj _ -> "ImmBuildProj"
+ | EqTr _ -> "EqTr"
+ | EqCgr _ -> "EqCgr"
+ | EqCgrP _ -> "EqCgrP"
+ | LiaMicromega _ -> "LiaMicromega"
+ | LiaDiseq _ -> "LiaDiseq"
+ | SplArith _ -> "SplArith"
+ | SplDistinctElim _ -> "SplDistinctElim"
+ | BBVar _ -> "BBVar"
+ | BBConst _ -> "BBConst"
+ | BBOp _ -> "BBOp"
+ | BBNot _ -> "BBNot"
+ | BBNeg _ -> "BBNeg"
+ | BBAdd _ -> "BBAdd"
+ | BBMul _ -> "BBMul"
+ | BBUlt _ -> "BBUlt"
+ | BBSlt _ -> "BBSlt"
+ | BBConc _ -> "BBConc"
+ | BBExtr _ -> "BBExtr"
+ | BBZextn _ -> "BBZextn"
+ | BBSextn _ -> "BBSextn"
+ | BBShl _ -> "BBShl"
+ | BBShr _ -> "BBShr"
+ | BBEq _ -> "BBEq"
+ | BBDiseq _ -> "BBDiseq"
+ | RowEq _ -> "RowEq"
+ | RowNeq _ -> "RowNeq"
+ | Ext _ -> "Ext"
+ | Hole _ -> "Hole"
+ | Forall_inst _ -> "Forall_inst"
+ | Qf_lemma _ -> "Qf_lemma"
+ end ^ ")"
diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli
index 010934a..6a145bb 100644
--- a/src/trace/smtCertif.mli
+++ b/src/trace/smtCertif.mli
@@ -1,25 +1,220 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
type used = int
type clause_id = int
type 'hform rule =
- ImmFlatten of 'hform clause * 'hform
+ (* Weakening *)
+ | Weaken of 'hform clause * 'hform list
+ (* * weaken : {a_1 ... a_n} --> {a_1 ... a_n b_1 ... b_n} *)
+
+ (* Simplification *)
+ | ImmFlatten of 'hform clause * 'hform
+
+ (* CNF Transformations *)
| True
+ (* * true : {true}
+ *)
| False
- | BuildDef of 'hform
- | BuildDef2 of 'hform
+ (* * false : {(not false)}
+ *)
+ | BuildDef of 'hform (* the first literal of the clause *)
+ (* * and_neg : {(and a_1 ... a_n) (not a_1) ... (not a_n)}
+ * or_pos : {(not (or a_1 ... a_n)) a_1 ... a_n}
+ * implies_pos : {(not (implies a b)) (not a) b}
+ * xor_pos1 : {(not (xor a b)) a b}
+ * xor_neg1 : {(xor a b) a (not b)}
+ * equiv_pos1 : {(not (iff a b)) a (not b)}
+ * equiv_neg1 : {(iff a b) (not a) (not b)}
+ * ite_pos1 : {(not (if_then_else a b c)) a c}
+ * ite_neg1 : {(if_then_else a b c) a (not c)}
+ *)
+ | BuildDef2 of 'hform (* the first literal of the clause *)
+ (* * xor_pos2 : {(not (xor a b)) (not a) (not b)}
+ * xor_neg2 : {(xor a b) (not a) b}
+ * equiv_pos2 : {(not (iff a b)) (not a) b}
+ * equiv_neg2 : {(iff a b) a b}
+ * ite_pos2 : {(not (if_then_else a b c)) (not a) b}
+ * ite_neg2 : {(if_then_else a b c) (not a) (not b)}
+
+ *)
| BuildProj of 'hform * int
+ (* * or_neg : {(or a_1 ... a_n) (not a_i)}
+ * and_pos : {(not (and a_1 ... a_n)) a_i}
+ * implies_neg1 : {(implies a b) a}
+ * implies_neg2 : {(implies a b) (not b)}
+ *)
+
+ (* Immediate CNF transformation : CNF transformation + Reso *)
| ImmBuildDef of 'hform clause
+ (* * not_and : {(not (and a_1 ... a_n))} --> {(not a_1) ... (not a_n)}
+ * or : {(or a_1 ... a_n)} --> {a_1 ... a_n}
+ * implies : {(implies a b)} --> {(not a) b}
+ * xor1 : {(xor a b)} --> {a b}
+ * not_xor1 : {(not (xor a b))} --> {a (not b)}
+ * equiv2 : {(iff a b)} --> {a (not b)}
+ * not_equiv2 : {(not (iff a b))} --> {(not a) (not b)}
+ * ite1 : {(if_then_else a b c)} --> {a c}
+ * not_ite1 : {(not (if_then_else a b c))} --> {a (not c)}
+ *)
| ImmBuildDef2 of 'hform clause
+ (* * xor2 : {(xor a b)} --> {(not a) (not b)}
+ * not_xor2 : {(not (xor a b))} --> {(not a) b}
+ * equiv1 : {(iff a b)} --> {(not a) b}
+ * not_equiv1 : {(not (iff a b))} --> {a b}
+ * ite2 : {(if_then_else a b c)} --> {(not a) b}
+ * not_ite2 : {(not (if_then_else a b c))} --> {(not a) (not b)}
+ *)
| ImmBuildProj of 'hform clause * int
+ (* * and : {(and a_1 ... a_n)} --> {a_i}
+ * not_or : {(not (or a_1 ... a_n))} --> {(not a_i)}
+ * not_implies1 : {(not (implies a b))} --> {a}
+ * not_implies2 : {(not (implies a b))} --> {(not b)}
+ *)
+
+ (* Equality *)
| EqTr of 'hform * 'hform list
- | EqCgr of 'hform * 'hform option list
- | EqCgrP of 'hform * 'hform * 'hform option list
- | LiaMicromega of 'hform list *
- Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+ (* * eq_reflexive : {(= x x)}
+ * eq_transitive : {(not (= x_1 x_2)) ... (not (= x_{n-1} x_n)) (= x_1 x_n)}
+ *)
+ | EqCgr of 'hform * ('hform option) list
+ (* * eq_congruent : {(not (= x_1 y_1)) ... (not (= x_n y_n))
+ (= (f x_1 ... x_n) (f y_1 ... y_n))}
+ *)
+ | EqCgrP of 'hform * 'hform * ('hform option) list
+ (* * eq_congruent_pred : {(not (= x_1 y_1)) ... (not (= x_n y_n))
+ (not (p x_1 ... x_n)) (p y_1 ... y_n)}
+ *)
+
+ (* Linear arithmetic *)
+ | LiaMicromega of 'hform list * Structures.Micromega_plugin_Certificate.Mc.zArithProof list
| LiaDiseq of 'hform
- | SplArith of 'hform clause * 'hform *
- Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+
+ (* Arithmetic simplifications *)
+ | SplArith of 'hform clause * 'hform * Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+
+ (* Elimination of operators *)
| SplDistinctElim of 'hform clause * 'hform
- | Hole of 'hform clause list * 'hform list
+
+ (* Bit-blasting *)
+ | BBVar of 'hform
+ (* Bit-blasting a variable:
+
+ ----------------------- bbVar
+ bbT(x, [x0; ...; xn])
+ *)
+ | BBConst of 'hform
+ (* Bit-blasting a constant:
+
+ ----------------------- bbConst
+ bbT(#0100, [0; 0; 1; 0])
+ *)
+ | BBOp of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitwise operations: bbAnd, bbOr, ...
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbAnd
+ bbT(a&b, [a0 /\ b0; ...; an /\ bn])
+ *)
+ | BBNot of 'hform clause * 'hform
+ (* Bit-blasting bitvector not
+ bbT(a, [a0; ...; an])
+ ------------------------------ bbNot
+ bbT(not a, [~a0 ; ...; ~an])
+ *)
+ | BBNeg of 'hform clause * 'hform
+ (* Bit-blasting bitvector negation
+ bbT(a, [a0; ...; an])
+ ------------------------------ bbNot
+ bbT(-a, [...])
+ *)
+ | BBAdd of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector addition
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbAnd
+ bbT(a+b, [...])
+ *)
+ | BBMul of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector multiplication
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbAnd
+ bbT(a*b, [...])
+ *)
+ | BBUlt of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector unsigned comparison
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbAnd
+ bvult a b <-> ...
+ *)
+ | BBSlt of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector signed comparison
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbAnd
+ bvslt a b <-> ...
+ *)
+ | BBConc of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector concatenation
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbConc
+ bbT(concat a b, [a0; ...; an; b0; ...; bn])
+ *)
+ | BBExtr of 'hform clause * 'hform
+ (* Bit-blasting bitvector extraction
+ bbT(a, [a0; ...; an])
+ ----------------------------------- bbExtr
+ bbT(extract i j a, [ai; ...; aj])
+ *)
+ | BBZextn of 'hform clause * 'hform
+ | BBSextn of 'hform clause * 'hform
+ (* Bit-blasting bitvector extensions
+
+ *)
+ | BBShl of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector shift left *)
+ | BBShr of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting bitvector shift right *)
+ | BBEq of 'hform clause * 'hform clause * 'hform
+ (* Bit-blasting equality
+ bbT(a, [a0; ...; an]) bbT(b, [b0; ...; bn])
+ -------------------------------------------------- bbEq
+ (a = b) <-> [(a0 <-> b0) /\ ... /\ (an <-> bn)]
+ *)
+
+ | BBDiseq of 'hform
+ (* disequality over constant bitvectors
+
+ ----------------------------- bbDiseq
+ #b000010101 <> #b00000000
+ *)
+
+ | RowEq of 'hform
+ (* Read over write same index
+ ------------------------------- roweq
+ select (store a i v) i = v
+ *)
+
+ | RowNeq of 'hform list
+ (* Read over write other index
+ ------------------------------------------------- rowneq
+ i <> j -> select (store a i v) j = select a j
+ *)
+
+ | Ext of 'hform
+ (* Extensionality over arrays
+ ------------------------------------------------------- ext
+ a = b \/ select a (diff a b) <> select b (diff a b)
+ *)
+
+ (* Possibility to introduce "holes" in proofs (that should be filled in Coq) *)
+ | Hole of ('hform clause) list * 'hform list
| Forall_inst of 'hform clause * 'hform
| Qf_lemma of 'hform clause * 'hform
diff --git a/src/trace/smtCnf.ml b/src/trace/smtCnf.ml
index 62a040d..0b82824 100644
--- a/src/trace/smtCnf.ml
+++ b/src/trace/smtCnf.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 *)
(* *)
@@ -79,7 +75,7 @@ module MakeCnf (Form:FORM) =
| Immediate _ | Done -> ()
| Todo ->
match Form.pform l with
- | Fatom _ -> ()
+ | Fatom _ | FbbT _ -> ()
| Fapp (op,args) ->
match op with
@@ -179,7 +175,7 @@ module MakeCnf (Form:FORM) =
set_immediate l;
match Form.pform l with
- | Fatom _ -> ()
+ | Fatom _ | FbbT _ -> ()
| Fapp (op,args) ->
match op with
diff --git a/src/trace/smtCnf.mli b/src/trace/smtCnf.mli
index 47fbd8c..1025ac4 100644
--- a/src/trace/smtCnf.mli
+++ b/src/trace/smtCnf.mli
@@ -1,3 +1,15 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
module MakeCnf :
functor (Form : SmtForm.FORM) ->
sig
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 27b8210..58793b6 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.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 *)
(* *)
@@ -38,7 +34,53 @@ let cchecker_b = gen_constant euf_checker_modules "checker_b"
let cchecker_eq_correct =
gen_constant euf_checker_modules "checker_eq_correct"
let cchecker_eq = gen_constant euf_checker_modules "checker_eq"
-let cZeqbsym = gen_constant z_modules "eqb_sym"
+let csetup_checker_step_debug =
+ gen_constant euf_checker_modules "setup_checker_step_debug"
+let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug"
+let cstep = gen_constant euf_checker_modules "step"
+let cchecker_debug = gen_constant euf_checker_modules "checker_debug"
+
+let cname_step = gen_constant euf_checker_modules "name_step"
+
+let cName_Res = gen_constant euf_checker_modules "Name_Res"
+let cName_Weaken= gen_constant euf_checker_modules "Name_Weaken"
+let cName_ImmFlatten= gen_constant euf_checker_modules "Name_ImmFlatten"
+let cName_CTrue= gen_constant euf_checker_modules "Name_CTrue"
+let cName_CFalse = gen_constant euf_checker_modules "Name_CFalse"
+let cName_BuildDef= gen_constant euf_checker_modules "Name_BuildDef"
+let cName_BuildDef2= gen_constant euf_checker_modules "Name_BuildDef2"
+let cName_BuildProj = gen_constant euf_checker_modules "Name_BuildProj"
+let cName_ImmBuildDef= gen_constant euf_checker_modules "Name_ImmBuildDef"
+let cName_ImmBuildDef2= gen_constant euf_checker_modules "Name_ImmBuildDef2"
+let cName_ImmBuildProj = gen_constant euf_checker_modules "Name_ImmBuildProj"
+let cName_EqTr = gen_constant euf_checker_modules "Name_EqTr"
+let cName_EqCgr = gen_constant euf_checker_modules "Name_EqCgr"
+let cName_EqCgrP= gen_constant euf_checker_modules "Name_EqCgrP"
+let cName_LiaMicromega = gen_constant euf_checker_modules "Name_LiaMicromega"
+let cName_LiaDiseq= gen_constant euf_checker_modules "Name_LiaDiseq"
+let cName_SplArith= gen_constant euf_checker_modules "Name_SplArith"
+let cName_SplDistinctElim = gen_constant euf_checker_modules "Name_SplDistinctElim"
+let cName_BBVar= gen_constant euf_checker_modules "Name_BBVar"
+let cName_BBConst= gen_constant euf_checker_modules "Name_BBConst"
+let cName_BBOp= gen_constant euf_checker_modules "Name_BBOp"
+let cName_BBNot= gen_constant euf_checker_modules "Name_BBNot"
+let cName_BBNeg= gen_constant euf_checker_modules "Name_BBNeg"
+let cName_BBAdd= gen_constant euf_checker_modules "Name_BBAdd"
+let cName_BBConcat= gen_constant euf_checker_modules "Name_BBConcat"
+let cName_BBMul= gen_constant euf_checker_modules "Name_BBMul"
+let cName_BBUlt= gen_constant euf_checker_modules "Name_BBUlt"
+let cName_BBSlt= gen_constant euf_checker_modules "Name_BBSlt"
+let cName_BBEq= gen_constant euf_checker_modules "Name_BBEq"
+let cName_BBDiseq= gen_constant euf_checker_modules "Name_BBDiseq"
+let cName_BBExtract= gen_constant euf_checker_modules "Name_BBExtract"
+let cName_BBZextend= gen_constant euf_checker_modules "Name_BBZextend"
+let cName_BBSextend= gen_constant euf_checker_modules "Name_BBSextend"
+let cName_BBShl= gen_constant euf_checker_modules "Name_BBShl"
+let cName_BBShr= gen_constant euf_checker_modules "Name_BBShr"
+let cName_RowEq= gen_constant euf_checker_modules "Name_RowEq"
+let cName_RowNeq= gen_constant euf_checker_modules "Name_RowNeq"
+let cName_Ext= gen_constant euf_checker_modules "Name_Ext"
+let cName_Hole= gen_constant euf_checker_modules "Name_Hole"
(* Given an SMT-LIB2 file and a certif, build the corresponding objects *)
@@ -50,42 +92,40 @@ let compute_roots roots last_root =
let rec find_root i root = function
| [] -> assert false
- | t::q -> if Form.equal t root then (i,q) else find_root (i+1) root q in
+ | t::q -> if Form.equal t root then i else find_root (i+1) root q in
- let rec used_roots acc i roots r =
+ let rec used_roots acc r =
if isRoot r.kind then
match r.value with
| Some [root] ->
- let (j,roots') = find_root i root roots in
- used_roots (j::acc) (j+1) roots' (next r)
+ let j = find_root 0 root roots in
+ used_roots (j::acc) (next r)
| _ -> assert false
- else
- acc in
+ else acc
+ in
- used_roots [] 0 roots !r
+ used_roots [] !r
-let interp_uf ta tf c =
+let interp_uf t_i ta tf c =
let rec interp = function
| [] -> Lazy.force cfalse
- | [l] -> Form.interp_to_coq (Atom.interp_to_coq ta) tf l
- | l::c -> mklApp corb [|Form.interp_to_coq (Atom.interp_to_coq ta) tf l; interp c|] in
+ | [l] -> Form.interp_to_coq (Atom.interp_to_coq t_i ta) tf l
+ | l::c -> mklApp corb [|Form.interp_to_coq (Atom.interp_to_coq t_i ta) tf l; interp c|] in
interp c
-let interp_conseq_uf (prem, concl) =
+let interp_conseq_uf t_i (prem, concl) =
let ta = Hashtbl.create 17 in
let tf = Hashtbl.create 17 in
let rec interp = function
- | [] -> mklApp cis_true [|interp_uf ta tf concl|]
- | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf ta tf c|]) (interp prem) in
+ | [] -> mklApp cis_true [|interp_uf t_i ta tf concl|]
+ | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
interp prem
let print_assm ty =
- let rec fix rf x = rf (fix rf) x in
- let pr = fix Ppconstr.modular_constr_pr Pp.mt Structures.ppconstr_lsimpleconstr in
- Printf.printf "WARNING: assuming the following hypothesis:\n%s\n\n" (Pp.string_of_ppcmds (pr (Structures.constrextern_extern_constr ty)));
- flush stdout
+ Format.printf "WARNING: assuming the following hypothesis:\n%s\n@."
+ (string_coq_constr ty)
let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf, roots, max_id, confl) =
@@ -107,7 +147,8 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
let ct_form = Term.mkConst (declare_constant t_form (DefinitionEntry ce2, IsDefinition Definition)) in
(* EMPTY LEMMA LIST *)
- let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
+ let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+ (interp_conseq_uf ct_i) (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
List.iter (fun (v,ty) ->
let _ = Structures.declare_new_variable v ty in
print_assm ty
@@ -140,8 +181,8 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
(* Given an SMT-LIB2 file and a certif, build the corresponding theorem *)
-let interp_roots roots =
- let interp = Form.interp_to_coq (Atom.interp_to_coq (Hashtbl.create 17)) (Hashtbl.create 17) in
+let interp_roots t_i roots =
+ let interp = Form.interp_to_coq (Atom.interp_to_coq t_i (Hashtbl.create 17)) (Hashtbl.create 17) in
match roots with
| [] -> Lazy.force ctrue
| f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots
@@ -163,7 +204,9 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
let t_form = snd (Form.interp_tbl rf) in
(* EMPTY LEMMA LIST *)
- let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
+ let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+ (interp_conseq_uf t_i)
+ (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
List.iter (fun (v,ty) ->
let _ = Structures.declare_new_variable v ty in
print_assm ty
@@ -185,10 +228,10 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
Structures.mkArray (Lazy.force cint, res) in
- let theorem_concl = mklApp cis_true [|mklApp cnegb [|interp_roots roots|]|] in
+ let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots t_i roots|]|] in
let theorem_proof_cast =
Term.mkCast (
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+ Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
@@ -197,13 +240,13 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
mklApp cchecker_correct
[|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*);
- vm_cast_true
+ vm_cast_true_no_check
(mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|])|]))))))),
Term.VMcast,
theorem_concl)
in
let theorem_proof_nocast =
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+ Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
@@ -238,7 +281,9 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
let t_form = snd (Form.interp_tbl rf) in
(* EMPTY LEMMA LIST *)
- let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i)) interp_conseq_uf (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
+ let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+ (interp_conseq_uf t_i)
+ (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
List.iter (fun (v,ty) ->
let _ = Structures.declare_new_variable v ty in
print_assm ty
@@ -261,7 +306,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
Structures.mkArray (Lazy.force cint, res) in
let tm =
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
+ Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
@@ -275,10 +320,256 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
(if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then
"true" else "false")
+let count_used confl =
+ let cpt = ref 0 in
+ let rec count c =
+ incr cpt;
+ (* if c.used = 1 then incr cpt; *)
+ match c.prev with
+ | None -> !cpt
+ | Some c -> count c
+ in
+ count confl
+
+
+let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
+ let nti = mkName "t_i" in
+ let ntfunc = mkName "t_func" in
+ let ntatom = mkName "t_atom" in
+ let ntform = mkName "t_form" in
+ let nc = mkName "c" in
+ let nused_roots = mkName "used_roots" in
+ let nd = mkName "d" in
+
+ let v = Term.mkRel in
+
+ let t_i = make_t_i rt in
+ let t_func = make_t_func ro (v 1 (*t_i*)) in
+ let t_atom = Atom.interp_tbl ra in
+ let t_form = snd (Form.interp_tbl rf) in
+
+ let (tres,last_root,cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+ (interp_conseq_uf t_i)
+ (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*);
+ v 2(*t_atom*); v 1(* t_form *)|])) confl None in
+ List.iter (fun (v,ty) ->
+ let _ = Structures.declare_new_variable v ty in
+ print_assm ty
+ ) cuts;
+
+ let certif =
+ mklApp cCertif [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *);
+ mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+
+ let used_roots = compute_roots roots last_root in
+ let used_rootsCstr =
+ let l = List.length used_roots in
+ let res = Array.make (l + 1) (mkInt 0) in
+ let i = ref (l-1) in
+ List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
+ mklApp cSome [|mklApp carray [|Lazy.force cint|];
+ Structures.mkArray (Lazy.force cint, res)|] in
+ let rootsCstr =
+ let res = Array.make (List.length roots + 1) (mkInt 0) in
+ let i = ref 0 in
+ List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
+ Structures.mkArray (Lazy.force cint, res) in
+
+ let tm =
+ Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+ Term.mkLetIn (ntfunc, t_func,
+ mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
+ Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+ Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+ Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*);
+ v 2 (*t_atom*); v 1 (*t_form*)|],
+ Term.mkLetIn (nused_roots, used_rootsCstr,
+ mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+ Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+ mklApp cchecker_debug [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*);
+ v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in
+
+ let res = Vnorm.cbv_vm (Global.env ()) tm
+ (mklApp coption
+ [|mklApp cprod
+ [|Lazy.force cnat; Lazy.force cname_step|]|]) in
+
+ match Term.decompose_app res with
+ | c, _ when Term.eq_constr c (Lazy.force cNone) ->
+ Structures.error ("Debug checker is only meant to be used for certificates \
+ that fail to be checked by SMTCoq.")
+ | c, [_; n] when Term.eq_constr c (Lazy.force cSome) ->
+ (match Term.decompose_app n with
+ | c, [_; _; cnb; cn] when Term.eq_constr c (Lazy.force cpair) ->
+ let n = fst (Term.decompose_app cn) in
+ let name =
+ if Term.eq_constr n (Lazy.force cName_Res ) then "Res"
+ else if Term.eq_constr n (Lazy.force cName_Weaken) then "Weaken"
+ else if Term.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten"
+ else if Term.eq_constr n (Lazy.force cName_CTrue) then "CTrue"
+ else if Term.eq_constr n (Lazy.force cName_CFalse ) then "CFalse"
+ else if Term.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef"
+ else if Term.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2"
+ else if Term.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj"
+ else if Term.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef"
+ else if Term.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2"
+ else if Term.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj"
+ else if Term.eq_constr n (Lazy.force cName_EqTr ) then "EqTr"
+ else if Term.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr"
+ else if Term.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP"
+ else if Term.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega"
+ else if Term.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq"
+ else if Term.eq_constr n (Lazy.force cName_SplArith) then "SplArith"
+ else if Term.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim"
+ else if Term.eq_constr n (Lazy.force cName_BBVar) then "BBVar"
+ else if Term.eq_constr n (Lazy.force cName_BBConst) then "BBConst"
+ else if Term.eq_constr n (Lazy.force cName_BBOp) then "BBOp"
+ else if Term.eq_constr n (Lazy.force cName_BBNot) then "BBNot"
+ else if Term.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg"
+ else if Term.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd"
+ else if Term.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat"
+ else if Term.eq_constr n (Lazy.force cName_BBMul) then "BBMul"
+ else if Term.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt"
+ else if Term.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt"
+ else if Term.eq_constr n (Lazy.force cName_BBEq) then "BBEq"
+ else if Term.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq"
+ else if Term.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract"
+ else if Term.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend"
+ else if Term.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend"
+ else if Term.eq_constr n (Lazy.force cName_BBShl) then "BBShl"
+ else if Term.eq_constr n (Lazy.force cName_BBShr) then "BBShr"
+ else if Term.eq_constr n (Lazy.force cName_RowEq) then "RowEq"
+ else if Term.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq"
+ else if Term.eq_constr n (Lazy.force cName_Ext) then "Ext"
+ else if Term.eq_constr n (Lazy.force cName_Hole) then "Hole"
+ else string_coq_constr n
+ in
+ let nb = mk_nat cnb + List.length roots + (confl.id + 1 - count_used confl) in
+ Structures.error ("Step number " ^ string_of_int nb ^
+ " (" ^ name ^ ") of the certificate likely failed.")
+ | _ -> assert false
+ )
+ | _ -> assert false
+
+
+
+let rec of_coq_list cl =
+ match Term.decompose_app cl with
+ | c, _ when Term.eq_constr c (Lazy.force cnil) -> []
+ | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) ->
+ x :: of_coq_list cr
+ | _ -> assert false
+
+
+let checker_debug_step t_i t_func t_atom t_form root used_root trace
+ (rt, ro, ra, rf, roots, max_id, confl) =
+
+ let t_i' = make_t_i rt in
+ let ce5 = Structures.mkUConst t_i' in
+ let ct_i = Term.mkConst (declare_constant t_i
+ (DefinitionEntry ce5, IsDefinition Definition)) in
+
+ let t_func' = make_t_func ro ct_i in
+ let ce6 = Structures.mkUConst t_func' in
+ let ct_func =
+ Term.mkConst (declare_constant t_func
+ (DefinitionEntry ce6, IsDefinition Definition)) in
+
+ let t_atom' = Atom.interp_tbl ra in
+ let ce1 = Structures.mkUConst t_atom' in
+ let ct_atom =
+ Term.mkConst (declare_constant t_atom
+ (DefinitionEntry ce1, IsDefinition Definition)) in
+
+ let t_form' = snd (Form.interp_tbl rf) in
+ let ce2 = Structures.mkUConst t_form' in
+ let ct_form =
+ Term.mkConst (declare_constant t_form
+ (DefinitionEntry ce2, IsDefinition Definition)) in
+
+ let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+ (interp_conseq_uf ct_i)
+ (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
+ List.iter (fun (v,ty) ->
+ let _ = Structures.declare_new_variable v ty in
+ print_assm ty
+ ) cuts;
+
+ let used_roots = compute_roots roots last_root in
+ let croots =
+ let res = Array.make (List.length roots + 1) (mkInt 0) in
+ let i = ref 0 in
+ List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
+ Structures.mkArray (Lazy.force cint, res) in
+ let cused_roots =
+ let l = List.length used_roots in
+ let res = Array.make (l + 1) (mkInt 0) in
+ let i = ref (l-1) in
+ List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
+ mklApp cSome [|mklApp carray [|Lazy.force cint|];
+ Structures.mkArray (Lazy.force cint, res)|] in
+ let ce3 = Structures.mkUConst croots in
+ let _ = declare_constant root
+ (DefinitionEntry ce3, IsDefinition Definition) in
+ let ce3' = Structures.mkUConst cused_roots in
+ let _ = declare_constant used_root
+ (DefinitionEntry ce3', IsDefinition Definition) in
+
+ let certif =
+ mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1);
+ tres;mkInt (get_pos confl)|] in
+ let ce4 = Structures.mkUConst certif in
+ let _ = declare_constant trace
+ (DefinitionEntry ce4, IsDefinition Definition) in
+
+ let setup =
+ mklApp csetup_checker_step_debug
+ [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in
+
+ let setup = Vnorm.cbv_vm (Global.env ()) setup
+ (mklApp cprod
+ [|Lazy.force cState_S_t;
+ mklApp clist [|mklApp cstep
+ [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in
+
+ let s, steps = match Term.decompose_app setup with
+ | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) ->
+ s, of_coq_list csteps
+ | _ -> assert false
+ in
+
+ let cpt = ref (List.length roots) in
+ let debug_step s step =
+ incr cpt;
+ Format.eprintf "%d@." !cpt;
+ let tm =
+ mklApp cchecker_step_debug
+ [| ct_i; ct_func; ct_atom; ct_form; s; step |] in
+
+ let res =
+ Vnorm.cbv_vm (Global.env ()) tm
+ (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in
+
+ match Term.decompose_app res with
+ | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) ->
+ if not (mk_bool cbad) then s
+ else Structures.error ("Step number " ^ string_of_int !cpt ^
+ " (" ^ string_coq_constr
+ (fst (Term.decompose_app step)) ^ ")" ^
+ " of the certificate likely failed." )
+ | _ -> assert false
+ in
+
+ List.fold_left debug_step s steps |> ignore;
+
+ Structures.error ("Debug checker is only meant to be used for certificates \
+ that fail to be checked by SMTCoq.")
+
+
(* Tactic *)
-let build_body rt ro ra rf l b (max_id, confl) find =
+let build_body rt ro ra rf l b (max_id, confl) vm_cast find =
let nti = mkName "t_i" in
let ntfunc = mkName "t_func" in
let ntatom = mkName "t_atom" in
@@ -291,34 +582,49 @@ let build_body rt ro ra rf l b (max_id, confl) find =
let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in
let t_atom = Atom.interp_tbl ra in
let t_form = snd (Form.interp_tbl rf) in
- let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl find in
+ let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq
+ (interp_conseq_uf t_i)
+ (certif_ops
+ (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|]))
+ confl find
+ in
let certif =
- mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
+ mklApp cCertif
+ [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*);
+ mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
- let proof_cast =
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
- Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
+ let add_lets t =
+ Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+ Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
- mklApp cchecker_b_correct
- [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*);
- vm_cast_true (mklApp cchecker_b [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*)|])|])))))
+ Term.mkLetIn (nc, certif, mklApp ccertif
+ [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+ t))))) in
+
+ let cbc =
+ add_lets
+ (mklApp cchecker_b [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*);
+ v 2 (*t_form*); l; b; v 1 (*certif*)|])
+ |> vm_cast
in
+
+ let proof_cast =
+ add_lets
+ (mklApp cchecker_b_correct
+ [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*);
+ l; b; v 1 (*certif*); cbc |]) in
+
let proof_nocast =
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
- Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
- Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
- Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
- mklApp cchecker_b_correct
- [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l; b; v 1 (*certif*)|])))))
- in
+ add_lets
+ (mklApp cchecker_b_correct
+ [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*);
+ l; b; v 1 (*certif*)|]) in
(proof_cast, proof_nocast, cuts)
-let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) find =
+let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find =
let nti = mkName "t_i" in
let ntfunc = mkName "t_func" in
let ntatom = mkName "t_atom" in
@@ -331,28 +637,39 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) find =
let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i*))) in
let t_atom = Atom.interp_tbl ra in
let t_form = snd (Form.interp_tbl rf) in
- let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq interp_conseq_uf (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl find in
+ let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq
+ (interp_conseq_uf t_i)
+ (certif_ops (Some [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|])) confl find in
let certif =
mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
- let proof_cast =
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
- Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
+ let add_lets t =
+ Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+ Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
- mklApp cchecker_eq_correct
- [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*);
- vm_cast_true (mklApp cchecker_eq [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*)|])|])))))
+ Term.mkLetIn (nc, certif, mklApp ccertif
+ [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+ t))))) in
+
+ let ceqc =
+ add_lets
+ (mklApp cchecker_eq [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*);
+ v 2 (*t_form*); l1; l2; l; v 1 (*certif*)|])
+ |> vm_cast
+ in
+
+ let proof_cast =
+ add_lets
+ (mklApp cchecker_eq_correct
+ [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*);
+ l1; l2; l; v 1 (*certif*); ceqc|])
in
let proof_nocast =
- Term.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_eqb|],
- Term.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1 (*t_i*)|]|],
- Term.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
- Term.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
- Term.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
- mklApp cchecker_eq_correct
- [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*); l1; l2; l; v 1 (*certif*)|])))))
+ add_lets
+ (mklApp cchecker_eq_correct
+ [|v 5 (*t_i*);v 4 (*t_func*);v 3 (*t_atom*); v 2 (*t_form*);
+ l1; l2; l; v 1 (*certif*)|])
in
(proof_cast, proof_nocast, cuts)
@@ -366,23 +683,23 @@ let get_arguments concl =
| _ -> failwith ("Verit.tactic: can only deal with equality over bool")
-let make_proof call_solver rt ro rf ra' rf' l' ls_smtc=
- let fl' = Form.flatten rf' l' in
+let make_proof call_solver env rt ro ra' rf' l' ls_smtc =
let root = SmtTrace.mkRootV [l'] in
- call_solver rt ro ra' rf' (Some (root, l')) (fl'::ls_smtc)
+ call_solver env rt ro ra' rf' (root,l') ls_smtc
+(* TODO: not generic anymore, the "lemma" part is currently specific to veriT *)
(* <of_coq_lemma> reifies the coq lemma given, we can then easily print it in a
.smt2 file. We need the reify tables to correctly recognize unbound variables
of the lemma. We also need to make sure to leave unchanged the tables because
the new objects may contain bound (by forall of the lemma) variables. *)
exception Axiom_form_unsupported
-
-let of_coq_lemma rt ro ra' rf' env sigma clemma =
+
+let of_coq_lemma rt ro ra' rf' env sigma solver_logic clemma =
let rel_context, qf_lemma = Term.decompose_prod_assum clemma in
let env_lemma = List.fold_right Environ.push_rel rel_context env in
let forall_args =
let fmap r = let n, t = Structures.destruct_rel_decl r in
- string_of_name n, SmtBtype.of_coq rt t in
+ string_of_name n, SmtBtype.of_coq rt solver_logic t in
List.map fmap rel_context in
let f, args = Term.decompose_app qf_lemma in
let core_f =
@@ -397,19 +714,20 @@ let of_coq_lemma rt ro ra' rf' env sigma clemma =
arg1
| _ -> raise Axiom_form_unsupported
else raise Axiom_form_unsupported in
- let core_smt = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env_lemma sigma)
+ let core_smt = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env_lemma sigma)
rf' core_f in
match forall_args with
[] -> core_smt
| _ -> Form.get rf' (Fapp (Fforall forall_args, [|core_smt|]))
-let core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl env sigma concl =
+let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl env sigma concl =
let a, b = get_arguments concl in
+
let tlcepl = List.map (Structures.interp_constr env sigma) lcepl in
let lcpl = lcpl @ tlcepl in
let lcl = List.map (Retyping.get_type_of env sigma) lcpl in
- let lsmt = List.map (of_coq_lemma rt ro ra' rf' env sigma) lcl in
+ let lsmt = List.map (of_coq_lemma rt ro ra' rf' env sigma solver_logic) lcl in
let l_pl_ls = List.combine (List.combine lcl lcpl) lsmt in
let lem_tbl : (int, Term.constr * Term.constr) Hashtbl.t =
@@ -418,7 +736,7 @@ let core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl env sigma concl =
Hashtbl.add lem_tbl (Form.index ls) (l, pl) in
List.iter new_ref l_pl_ls;
-
+
let find_lemma cl =
let re_hash hf = Form.hash_hform (Atom.hash_hatom ra') rf' hf in
match cl.value with
@@ -427,39 +745,231 @@ let core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl env sigma concl =
begin try Hashtbl.find lem_tbl (Form.index hl)
with Not_found ->
let oc = open_out "/tmp/find_lemma.log" in
- List.iter (fun u -> Printf.fprintf oc "%s\n"
- (VeritSyntax.string_hform u)) lsmt;
- Printf.fprintf oc "\n%s\n" (VeritSyntax.string_hform hl);
+ let fmt = Format.formatter_of_out_channel oc in
+ List.iter (fun u -> Format.fprintf fmt "%a\n" VeritSyntax.hform_to_smt u) lsmt;
+ Format.fprintf fmt "\n%a\n" VeritSyntax.hform_to_smt hl;
flush oc; close_out oc; failwith "find_lemma" end
| _ -> failwith "unexpected form of root" in
-
+
let (body_cast, body_nocast, cuts) =
- if ((Term.eq_constr b (Lazy.force ctrue)) || (Term.eq_constr b (Lazy.force cfalse))) then
- let l = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
- let l' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' a in
- let l' = if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l' else l' in
- let max_id_confl = make_proof call_solver rt ro rf ra' rf' l' lsmt in
- build_body rt ro ra rf (Form.to_coq l) b max_id_confl (Some find_lemma)
+ if ((Term.eq_constr b (Lazy.force ctrue)) ||
+ (Term.eq_constr b (Lazy.force cfalse))) then
+ let l = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
+ let l' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
+ let l' =
+ if (Term.eq_constr b (Lazy.force ctrue)) then Form.neg l' else l' in
+ let max_id_confl = make_proof call_solver env rt ro ra' rf' l' lsmt in
+ build_body rt ro ra rf (Form.to_coq l) b max_id_confl (vm_cast env) (Some find_lemma)
else
- let l1 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf a in
- let l2 = Form.of_coq (Atom.of_coq rt ro ra env sigma) rf b in
+ let l1 = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
+ let l2 = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf b in
let l = Form.neg (Form.get rf (Fapp(Fiff,[|l1;l2|]))) in
- let l1' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' a in
- let l2' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' env sigma) rf' b in
+ let l1' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' a in
+ let l2' = Form.of_coq (Atom.of_coq ~hash:true rt ro ra' solver_logic env sigma) rf' b in
let l' = Form.neg (Form.get rf' (Fapp(Fiff,[|l1';l2'|]))) in
- let max_id_confl = make_proof call_solver rt ro rf ra' rf' l' lsmt in
- build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2) (Form.to_coq l) max_id_confl (Some find_lemma) in
+ let max_id_confl = make_proof call_solver env rt ro ra' rf' l' lsmt in
+ build_body_eq rt ro ra rf (Form.to_coq l1) (Form.to_coq l2)
+ (Form.to_coq l) max_id_confl (vm_cast env) (Some find_lemma) in
- let cuts = SmtBtype.get_cuts rt @ cuts in
+ let cuts = (SmtBtype.get_cuts rt) @ cuts in
List.fold_right (fun (eqn, eqt) tac ->
- Structures.tclTHENLAST (Structures.assert_before (Names.Name eqn) eqt) tac)
- cuts
+ Structures.tclTHENLAST
+ (Structures.assert_before (Names.Name eqn) eqt)
+ tac
+ ) cuts
(Structures.tclTHEN
(Structures.set_evars_tac body_nocast)
(Structures.vm_cast_no_check body_cast))
-let tactic call_solver rt ro ra rf ra' rf' lcpl lcepl =
+
+let tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl =
Structures.tclTHEN
Tactics.intros
- (Structures.mk_tactic (core_tactic call_solver rt ro ra rf ra' rf' lcpl lcepl))
+ (Structures.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl))
+
+
+(**********************************************)
+(* Show solver models as Coq counter-examples *)
+(**********************************************)
+
+
+open SExpr
+open Smtlib2_genConstr
+open Format
+
+
+let string_index_of_constr env i cf =
+ try
+ let s = string_coq_constr cf in
+ let nc = Environ.named_context env in
+ let nd = Environ.lookup_named (Names.id_of_string s) env in
+ let cpt = ref 0 in
+ (try List.iter (fun n -> incr cpt; if n == nd then raise Exit) nc
+ with Exit -> ());
+ s, !cpt
+ with _ -> string_coq_constr cf, -i
+
+
+let vstring_i env i =
+ let cf = SmtAtom.Atom.get_coq_term_op i in
+ if Term.isRel cf then
+ let dbi = Term.destRel cf in
+ let s =
+ Environ.lookup_rel dbi env
+ |> Structures.get_rel_dec_name
+ |> function
+ | Names.Name id -> Names.string_of_id id
+ | Names.Anonymous -> "?" in
+ s, dbi
+ else
+ string_index_of_constr env i cf
+
+
+let sstring_i env i v =
+ let tf = SmtBtype.get_coq_type_op i in
+ let (s, idx) = string_index_of_constr env i tf in
+ (s^"#"^v, idx)
+
+
+let smt2_id_to_coq_string env t_i ra rf name =
+ try
+ let l = String.split_on_char '_' name in
+ match l with
+ | ["op"; i] -> vstring_i env (int_of_string i)
+ | ["@uc"; "Tindex"; i; j] -> sstring_i env (int_of_string i) j
+ | _ -> raise Not_found
+ with _ -> (name, 0)
+
+
+let op_to_coq_string op = match op with
+ | "=" | "+" | "-" | "*" | "/" -> op
+ | "or" -> "||"
+ | "and" -> "&&"
+ | "xor" -> "xorb"
+ | "=>" -> "implb"
+ | _ -> op
+
+
+let coq_bv_string s =
+ let rec aux acc = function
+ | true :: r -> aux (acc ^ "|1") r
+ | false :: r -> aux (acc ^ "|0") r
+ | [] -> "#b" ^ acc ^ "|"
+ in
+ if String.length s < 3 ||
+ not (s.[0] = '#' && s.[1] = 'b') then failwith "not bv";
+ aux "" (parse_smt2bv s)
+
+
+let is_bvint bs =
+ try Scanf.sscanf bs "bv%s" (fun s ->
+ try ignore (Big_int.big_int_of_string s); true
+ with _ -> false)
+ with _ -> false
+
+
+let rec smt2_sexpr_to_coq_string env t_i ra rf =
+ let open SExpr in function
+ | Atom "true" -> "true"
+ | Atom "false" -> "false"
+ | Atom s ->
+ (try ignore (int_of_string s); s
+ with Failure _ ->
+ try coq_bv_string s
+ with Failure _ ->
+ try fst (smt2_id_to_coq_string env t_i ra rf s)
+ with _ -> s)
+ | List [Atom "as"; Atom "const"; _] -> "const_farray"
+ | List [Atom "as"; s; _] -> smt2_sexpr_to_coq_string env t_i ra rf s
+ | List [Atom "_"; Atom bs; Atom s] when is_bvint bs ->
+ Scanf.sscanf bs "bv%s" (fun i ->
+ coq_bv_string (bigint_bv (Big_int.big_int_of_string i)
+ (int_of_string s)))
+ | List [Atom "-"; Atom _ as s] ->
+ sprintf "-%s"
+ (smt2_sexpr_to_coq_string env t_i ra rf s)
+ | List [Atom "-"; s] ->
+ sprintf "(- %s)"
+ (smt2_sexpr_to_coq_string env t_i ra rf s)
+ | List [Atom (("+"|"-"|"*"|"/"|"or"|"and"|"=") as op); s1; s2] ->
+ sprintf "%s %s %s"
+ (smt2_sexpr_to_coq_string env t_i ra rf s1)
+ (op_to_coq_string op)
+ (smt2_sexpr_to_coq_string env t_i ra rf s2)
+ | List [Atom (("xor"|"=>"|"") as op); s1; s2] ->
+ sprintf "(%s %s %s)"
+ (op_to_coq_string op)
+ (smt2_sexpr_to_coq_string env t_i ra rf s1)
+ (smt2_sexpr_to_coq_string env t_i ra rf s2)
+ | List [Atom "select"; a; i] ->
+ sprintf "%s[%s]"
+ (smt2_sexpr_to_coq_string env t_i ra rf a)
+ (smt2_sexpr_to_coq_string env t_i ra rf i)
+ | List [Atom "store"; a; i; v] ->
+ sprintf "%s[%s <- %s]"
+ (smt2_sexpr_to_coq_string env t_i ra rf a)
+ (smt2_sexpr_to_coq_string env t_i ra rf i)
+ (smt2_sexpr_to_coq_string env t_i ra rf v)
+ | List [Atom "ite"; c; s1; s2] ->
+ sprintf "if %s then %s else %s"
+ (smt2_sexpr_to_coq_string env t_i ra rf c)
+ (smt2_sexpr_to_coq_string env t_i ra rf s1)
+ (smt2_sexpr_to_coq_string env t_i ra rf s2)
+ | List l ->
+ sprintf "(%s)"
+ (String.concat " " (List.map (smt2_sexpr_to_coq_string env t_i ra rf) l))
+
+
+let str_contains s1 s2 =
+ let re = Str.regexp_string s2 in
+ try ignore (Str.search_forward re s1 0); true
+ with Not_found -> false
+
+let lambda_to_coq_string l s =
+ Format.sprintf "fun %s => %s"
+ (String.concat " "
+ (List.map (function
+ | List [Atom v; _] ->
+ if str_contains s v then v else "_"
+ | _ -> assert false) l))
+ s
+
+type model =
+ | Fun of ((string * int) * string)
+ | Sort
+
+let model_item env rt ro ra rf =
+ let t_i = make_t_i rt in
+ function
+ | List [Atom "define-fun"; Atom n; List []; _; expr] ->
+ Fun (smt2_id_to_coq_string env t_i ra rf n,
+ smt2_sexpr_to_coq_string env t_i ra rf expr)
+
+ | List [Atom "define-fun"; Atom n; List l; _; expr] ->
+ Fun (smt2_id_to_coq_string env t_i ra rf n,
+ lambda_to_coq_string l
+ (smt2_sexpr_to_coq_string env t_i ra rf expr))
+
+ | List [Atom "declare-sort"; Atom n; _] ->
+ Sort
+
+ | l ->
+ (* let out = open_out_gen [Open_append] 700 "/tmp/test.log" in
+ * let outf = Format.formatter_of_out_channel out in
+ * SExpr.print outf l; pp_print_flush outf ();
+ * close_out out; *)
+ Structures.error ("Could not reconstruct model")
+
+
+let model env rt ro ra rf = function
+ | List (Atom "model" :: l) ->
+ List.fold_left (fun acc m -> match model_item env rt ro ra rf m with Fun m -> m::acc | Sort -> acc) [] l
+ |> List.sort (fun ((_ ,i1), _) ((_, i2), _) -> i2 - i1)
+ | _ -> Structures.error ("No model")
+
+
+let model_string env rt ro ra rf s =
+ String.concat "\n"
+ (List.map (fun ((x, _) ,v) -> Format.sprintf "%s := %s" x v)
+ (model env rt ro ra rf s))
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
index 6248270..d7b6ae6 100644
--- a/src/trace/smtCommands.mli
+++ b/src/trace/smtCommands.mli
@@ -1,98 +1,63 @@
-val euf_checker_modules : string list list
-val certif_ops :
- Term.constr array option ->
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
- Term.constr lazy_t * Term.constr lazy_t
-val cCertif : Term.constr lazy_t
-val ccertif : Term.constr lazy_t
-val cchecker : Term.constr lazy_t
-val cchecker_correct : Term.constr lazy_t
-val cchecker_b_correct : Term.constr lazy_t
-val cchecker_b : Term.constr lazy_t
-val cchecker_eq_correct : Term.constr lazy_t
-val cchecker_eq : Term.constr lazy_t
-val compute_roots :
- SmtAtom.Form.t list -> SmtAtom.Form.t SmtCertif.clause -> int list
-val interp_uf :
- (int, Term.constr) Hashtbl.t ->
- (int, Term.constr) Hashtbl.t -> SmtAtom.Form.t list -> Term.constr
-val interp_conseq_uf :
- SmtAtom.Form.t list list * SmtAtom.Form.t list -> Term.types
-val print_assm : Term.constr -> unit
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
val parse_certif :
- Names.identifier ->
- Names.identifier ->
- Names.identifier ->
- Names.identifier ->
- Names.identifier ->
- Names.identifier ->
- Names.identifier ->
- SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
- SmtAtom.Form.reify * SmtAtom.Form.t list * int *
- SmtAtom.Form.t SmtCertif.clause -> unit
-val interp_roots : SmtAtom.Form.t list -> Term.constr
+ Structures.names_id ->
+ Structures.names_id ->
+ Structures.names_id ->
+ Structures.names_id ->
+ Structures.names_id ->
+ Structures.names_id ->
+ Structures.names_id ->
+ SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
+ SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
+ SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause ->
+ unit
+
+val checker_debug :
+ SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
+ SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
+ SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> 'a
+
val theorem :
- Names.identifier ->
- SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
- SmtAtom.Form.reify * SmtAtom.Form.t list * int *
- SmtAtom.Form.t SmtCertif.clause -> unit
+ Structures.names_id ->
+ SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
+ SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
+ SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause ->
+ unit
+
val checker :
- SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
- SmtAtom.Form.reify * SmtAtom.Form.t list * int *
- SmtAtom.Form.t SmtCertif.clause -> unit
-val build_body :
+ SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
+ SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
+ SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause ->
+ unit
+
+val tactic :
+ (Environ.env ->
+ SmtBtype.reify_tbl ->
+ SmtAtom.Op.reify_tbl ->
+ SmtAtom.Atom.reify_tbl ->
+ SmtAtom.Form.reify ->
+ (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) ->
+ SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause) ->
+ SmtMisc.logic ->
SmtBtype.reify_tbl ->
SmtAtom.Op.reify_tbl ->
SmtAtom.Atom.reify_tbl ->
SmtAtom.Form.reify ->
- Term.constr ->
- Term.constr ->
- int * SmtAtom.Form.t SmtCertif.clause ->
- (SmtAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr) option ->
- Term.constr * Term.constr * (Names.identifier * Term.types) list
-val build_body_eq :
- SmtBtype.reify_tbl ->
- SmtAtom.Op.reify_tbl ->
SmtAtom.Atom.reify_tbl ->
SmtAtom.Form.reify ->
- Term.constr ->
- Term.constr ->
- Term.constr ->
- int * SmtAtom.Form.t SmtCertif.clause ->
- (SmtAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr) option ->
- Term.constr * Term.constr * (Names.identifier * Term.types) list
-val get_arguments : Term.constr -> Term.constr * Term.constr
-val make_proof :
- (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
- SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
- (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
- SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause) ->
- SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
- SmtAtom.Form.reify ->
- SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
- SmtAtom.Form.t -> SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause
-val core_tactic :
- (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
- SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
- (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
- SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause) ->
- SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
- SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
- SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
- Term.constr list -> Structures.constr_expr list ->
- Environ.env -> Evd.evar_map -> Term.constr -> Structures.tactic
-val tactic :
- (SmtBtype.reify_tbl -> SmtAtom.Op.reify_tbl ->
- SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
- (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
- SmtAtom.Form.t list -> int * SmtAtom.Form.t SmtCertif.clause) ->
- SmtBtype.reify_tbl ->
- SmtAtom.Op.reify_tbl ->
- SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
- SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify ->
- Term.constr list -> Structures.constr_expr list -> Structures.tactic
+ (Environ.env -> Term.constr -> Term.constr) ->
+ Term.constr list ->
+ Structures.constr_expr list -> Structures.tactic
+
+val model_string : Environ.env -> SmtBtype.reify_tbl -> 'a -> 'b -> 'c -> SExpr.t -> string
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index d2e039b..4138e7c 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.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 *)
(* *)
@@ -28,6 +24,9 @@ module type ATOM =
val equal : t -> t -> bool
val is_bool_type : t -> bool
+ val is_bv_type : t -> bool
+ val to_smt : Format.formatter -> t -> unit
+ val logic : t -> logic
end
@@ -47,6 +46,7 @@ type fop =
type ('a,'f) gen_pform =
| Fatom of 'a
| Fapp of fop * 'f array
+ | FbbT of 'a * 'f list
module type FORM =
@@ -68,9 +68,11 @@ module type FORM =
val is_pos : t -> bool
val is_neg : t -> bool
- val to_string : ?pi:bool -> (hatom -> string) -> t -> string
- val to_smt : (hatom -> string) -> Format.formatter ->
- t -> unit
+ val to_smt : ?pi:bool ->
+ (Format.formatter -> hatom -> unit) ->
+ Format.formatter -> t -> unit
+
+ val logic : t -> logic
(* Building formula from positive formula *)
exception NotWellTyped of pform
@@ -86,6 +88,10 @@ module type FORM =
(** Flattening of [Fand] and [For], removing of [Fnot2] *)
val flatten : reify -> t -> t
+ (** Turn n-ary [Fand] and [For] into their right-associative
+ counter-parts *)
+ val right_assoc : reify -> t -> t
+
(** Producing Coq terms *)
val to_coq : t -> Term.constr
@@ -150,39 +156,69 @@ module Make (Atom:ATOM) =
| Pos hp -> hp.hval
| Neg hp -> hp.hval
- let rec to_string ?pi:(pi=false) atom_to_string = function
- | Pos hp -> (if pi then string_of_int hp.index ^ ":" else "")
- ^ to_string_pform atom_to_string hp.hval
- | Neg hp -> (if pi then string_of_int hp.index ^ ":" else "") ^ "(not "
- ^ to_string_pform atom_to_string hp.hval ^ ")"
-
- and to_string_pform atom_to_string = function
- | Fatom a -> atom_to_string a
- | Fapp (op,args) -> to_string_op_args atom_to_string op args
-
- and to_string_op_args atom_to_string op args =
- let (s1,s2) = if Array.length args = 0 then ("","") else ("(",")") in
- s1 ^ to_string_op op ^
- Array.fold_left (fun acc h -> acc ^ " " ^ to_string atom_to_string h) "" args ^ s2
-
- and to_string_op = function
- | Ftrue -> "true"
- | Ffalse -> "false"
- | Fand -> "and"
- | For -> "or"
- | Fxor -> "xor"
- | Fimp -> "=>"
- | Fiff -> "="
- | Fite -> "ite"
- | Fnot2 _ -> ""
- | Fforall l -> "forall (" ^
- to_string_args l ^
- ")"
-
- and to_string_args = function
- | [] -> " "
- | (s, t)::rest -> " (" ^ s ^ " " ^ SmtBtype.to_string t ^ ")"
- ^ to_string_args rest
+
+ let rec to_smt ?pi:(pi=false) atom_to_smt fmt = function
+ | Pos hp ->
+ if pi then Format.fprintf fmt "%s" (string_of_int hp.index ^ ":");
+ to_smt_pform atom_to_smt fmt hp.hval
+ | Neg hp ->
+ if pi then Format.fprintf fmt "%s" (string_of_int hp.index ^ ":");
+ Format.fprintf fmt "(not ";
+ to_smt_pform atom_to_smt fmt hp.hval;
+ Format.fprintf fmt ")"
+
+ and to_smt_pform atom_to_smt fmt = function
+ | Fatom a -> atom_to_smt fmt a
+ | Fapp (op,args) -> to_smt_op atom_to_smt fmt op args
+ (* This is an intermediate object of proofs, it correspond to nothing in SMT *)
+ | FbbT (a, l) ->
+ Format.fprintf fmt "(bbT %a [" atom_to_smt a;
+ let fi = ref true in
+ List.iter (fun f -> Format.fprintf fmt "%s%a"
+ (if !fi then "" else "; ")
+ (to_smt atom_to_smt) f; fi := false) l;
+ Format.fprintf fmt "])"
+
+ and to_smt_op atom_to_smt fmt op args =
+ let (s1,s2) = if ((Array.length args = 0) || (match op with Fnot2 _ -> true | _ -> false)) then ("","") else ("(",")") in
+ Format.fprintf fmt "%s" s1;
+ (match op with
+ | Ftrue -> Format.fprintf fmt "true"
+ | Ffalse -> Format.fprintf fmt "false"
+ | Fand -> Format.fprintf fmt "and"
+ | For -> Format.fprintf fmt "or"
+ | Fxor -> Format.fprintf fmt "xor"
+ | Fimp -> Format.fprintf fmt "=>"
+ | Fiff -> Format.fprintf fmt "="
+ | Fite -> Format.fprintf fmt "ite"
+ | Fnot2 _ -> ()
+ | Fforall l ->
+ (Format.fprintf fmt "forall (";
+ to_smt_args fmt l;
+ Format.fprintf fmt ")")
+ );
+
+ Array.iter (fun h -> Format.fprintf fmt " "; to_smt atom_to_smt fmt h) args;
+ Format.fprintf fmt "%s" s2
+
+ and to_smt_args fmt = function
+ | [] -> Format.fprintf fmt " "
+ | (s, t)::rem ->
+ (Format.fprintf fmt " (%s " s;
+ SmtBtype.to_smt fmt t;
+ Format.fprintf fmt ")";
+ to_smt_args fmt rem)
+
+ let rec logic_pform = function
+ | Fatom a -> Atom.logic a
+ | Fapp (_, args) ->
+ Array.fold_left (fun l f ->
+ SL.union (logic f) l
+ ) SL.empty args
+ | FbbT _ -> SL.singleton LBitvectors
+
+ and logic = function
+ | Pos hp | Neg hp -> logic_pform hp.hval
let dumbed_down op =
let dumbed_down_bt = function
@@ -192,8 +228,6 @@ module Make (Atom:ATOM) =
| Fforall l -> Fforall (List.map (fun (x, bt) -> x, dumbed_down_bt bt) l)
| x -> x
- let to_smt atom_to_string fmt f =
- Format.fprintf fmt "%s" (to_string atom_to_string f)
module HashedForm =
struct
@@ -203,31 +237,44 @@ module Make (Atom:ATOM) =
let equal pf1 pf2 =
match pf1, pf2 with
| Fatom ha1, Fatom ha2 -> Atom.equal ha1 ha2
- | Fapp(op1,args1), Fapp(op2,args2) ->
- dumbed_down op1 = dumbed_down op2 &&
- Array.length args1 == Array.length args2 &&
- (try
- for i = 0 to Array.length args1 - 1 do
- if not (equal args1.(i) args2.(i)) then raise Not_found
- done;
- true
- with Not_found -> false)
+ | Fapp(op1,args1), Fapp(op2,args2) ->
+ dumbed_down op1 = dumbed_down op2 &&
+ Array.length args1 == Array.length args2 &&
+ (try
+ for i = 0 to Array.length args1 - 1 do
+ if not (equal args1.(i) args2.(i)) then raise Not_found
+ done;
+ true
+ with Not_found -> false)
+ | FbbT(ha1, l1), FbbT(ha2, l2) ->
+ (try
+ Atom.equal ha1 ha2 &&
+ List.for_all2 (fun i j -> equal i j) l1 l2
+ with | Invalid_argument _ -> false)
| _, _ -> false
let hash pf =
match pf with
| Fatom ha1 -> Atom.index ha1 * 2
| Fapp(op, args) ->
- let hash_args =
- match Array.length args with
- | 0 -> 0
- | 1 -> to_lit args.(0)
- | 2 -> (to_lit args.(1)) lsl 2 + to_lit args.(0)
- | _ ->
- (to_lit args.(2)) lsl 4 + (to_lit args.(1)) lsl 2 +
- to_lit args.(0) in
- (hash_args * 10 + Hashtbl.hash (dumbed_down op)) * 2 + 1
-
+ let hash_args =
+ match Array.length args with
+ | 0 -> 0
+ | 1 -> to_lit args.(0)
+ | 2 -> (to_lit args.(1)) lsl 2 + to_lit args.(0)
+ | _ ->
+ (to_lit args.(2)) lsl 4 + (to_lit args.(1)) lsl 2 +
+ to_lit args.(0) in
+ (hash_args * 10 + Hashtbl.hash (dumbed_down op)) * 2 + 1
+ | FbbT(ha, l) ->
+ let hash_args =
+ match l with
+ | [] -> 0
+ | [a0] -> to_lit a0
+ | [a0;a1] -> (to_lit a1) lsl 2 + to_lit a0
+ | a0::a1::a2::_ ->
+ (to_lit a2) lsl 4 + (to_lit a1) lsl 2 + to_lit a0 in
+ (hash_args * 10 + Atom.index ha) * 2 + 1
end
module HashForm = Hashtbl.Make (HashedForm)
@@ -241,19 +288,36 @@ module Make (Atom:ATOM) =
let check pf =
match pf with
- | Fatom ha -> if not (Atom.is_bool_type ha) then raise (NotWellTyped pf)
+ | Fatom ha -> if not (Atom.is_bool_type ha) then
+ raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+ NotWellTyped pf)
| Fapp (op, args) ->
- match op with
+ (match op with
| Ftrue | Ffalse ->
- if Array.length args <> 0 then raise (NotWellTyped pf)
+ if Array.length args <> 0 then
+ raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+ NotWellTyped pf)
| Fnot2 _ ->
- if Array.length args <> 1 then raise (NotWellTyped pf)
+ if Array.length args <> 1 then
+ raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+ NotWellTyped pf)
| Fand | For -> ()
| Fxor | Fimp | Fiff ->
- if Array.length args <> 2 then raise (NotWellTyped pf)
- | Fite ->
- if Array.length args <> 3 then raise (NotWellTyped pf)
+ if Array.length args <> 2 then
+ raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+ NotWellTyped pf)
+
+ | Fite ->
+ if Array.length args <> 3 then
+ raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+ NotWellTyped pf)
+
| Fforall l -> ()
+ )
+
+ | FbbT (ha, l) -> if not (Atom.is_bv_type ha) then
+ raise (Format.eprintf "nwt: %a" (to_smt_pform Atom.to_smt) pf;
+ NotWellTyped pf)
let declare reify pf =
check pf;
@@ -278,7 +342,7 @@ module Make (Atom:ATOM) =
()
let get ?declare:(decl=true) reify pf =
- if decl then
+ if decl then
try HashForm.find reify.tbl pf
with Not_found -> declare reify pf
else Pos {index = -1; hval = pf}
@@ -324,100 +388,104 @@ module Make (Atom:ATOM) =
let rec mk_hform h =
let c, args = Term.decompose_app h in
match get_cst c with
- | CCtrue -> get reify (Fapp(Ftrue,empty_args))
- | CCfalse -> get reify (Fapp(Ffalse,empty_args))
- | CCnot -> mk_fnot 1 args
- | CCand -> mk_fand [] args
- | CCor -> mk_for [] args
- | CCxor -> op2 (fun l -> Fapp(Fxor,l)) args
- | CCiff -> op2 (fun l -> Fapp(Fiff,l)) args
- | CCimp ->
- (match args with
- | [b1;b2] ->
- let l1 = mk_hform b1 in
- let l2 = mk_hform b2 in
- get reify (Fapp (Fimp, [|l1;l2|]))
- | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb")
- | CCifb ->
- (* We should also be able to reify if then else *)
- begin match args with
- | [b1;b2;b3] ->
- let l1 = mk_hform b1 in
- let l2 = mk_hform b2 in
- let l3 = mk_hform b3 in
- get reify (Fapp (Fite, [|l1;l2;l3|]))
- | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
- end
- | _ ->
- let a = atom_of_coq h in
- get reify (Fatom a)
+ | CCtrue -> get reify (Fapp(Ftrue,empty_args))
+ | CCfalse -> get reify (Fapp(Ffalse,empty_args))
+ | CCnot -> mk_fnot 1 args
+ | CCand -> mk_fand [] args
+ | CCor -> mk_for [] args
+ | CCxor -> op2 (fun l -> Fapp(Fxor,l)) args
+ | CCiff -> op2 (fun l -> Fapp(Fiff,l)) args
+ | CCimp ->
+ (match args with
+ | [b1;b2] ->
+ let l1 = mk_hform b1 in
+ let l2 = mk_hform b2 in
+ get reify (Fapp (Fimp, [|l1;l2|]))
+ | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb")
+ | CCifb ->
+ (* We should also be able to reify if then else *)
+ begin match args with
+ | [b1;b2;b3] ->
+ let l1 = mk_hform b1 in
+ let l2 = mk_hform b2 in
+ let l3 = mk_hform b3 in
+ get reify (Fapp (Fite, [|l1;l2;l3|]))
+ | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
+ end
+ | _ ->
+ let a = atom_of_coq h in
+ get reify (Fatom a)
and op2 f args =
match args with
- | [b1;b2] ->
- let l1 = mk_hform b1 in
- let l2 = mk_hform b2 in
- get reify (f [|l1; l2|])
- | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments"
+ | [b1;b2] ->
+ let l1 = mk_hform b1 in
+ let l2 = mk_hform b2 in
+ get reify (f [|l1; l2|])
+ | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments"
and mk_fnot i args =
match args with
- | [t] ->
- let c,args = Term.decompose_app t in
- if Term.eq_constr c (Lazy.force cnegb) then
- mk_fnot (i+1) args
- else
- let q,r = i lsr 1 , i land 1 in
- let l = mk_hform t in
- let l = if r = 0 then l else neg l in
- if q = 0 then l
- else get reify (Fapp(Fnot2 q, [|l|]))
- | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
+ | [t] ->
+ let c,args = Term.decompose_app t in
+ if Term.eq_constr c (Lazy.force cnegb) then
+ mk_fnot (i+1) args
+ else
+ let q,r = i lsr 1 , i land 1 in
+ let l = mk_hform t in
+ let l = if r = 0 then l else neg l in
+ if q = 0 then l
+ else get reify (Fapp(Fnot2 q, [|l|]))
+ | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
and mk_fand acc args =
match args with
- | [t1;t2] ->
- let l2 = mk_hform t2 in
- let c, args = Term.decompose_app t1 in
- if Term.eq_constr c (Lazy.force candb) then
- mk_fand (l2::acc) args
- else
- let l1 = mk_hform t1 in
- get reify (Fapp(Fand, Array.of_list (l1::l2::acc)))
- | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb"
+ | [t1;t2] ->
+ let l2 = mk_hform t2 in
+ let c, args = Term.decompose_app t1 in
+ if Term.eq_constr c (Lazy.force candb) then
+ mk_fand (l2::acc) args
+ else
+ let l1 = mk_hform t1 in
+ get reify (Fapp(Fand, Array.of_list (l1::l2::acc)))
+ | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb"
and mk_for acc args =
match args with
- | [t1;t2] ->
- let l2 = mk_hform t2 in
- let c, args = Term.decompose_app t1 in
- if Term.eq_constr c (Lazy.force corb) then
- mk_for (l2::acc) args
- else
- let l1 = mk_hform t1 in
- get reify (Fapp(For, Array.of_list (l1::l2::acc)))
- | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
+ | [t1;t2] ->
+ let l2 = mk_hform t2 in
+ let c, args = Term.decompose_app t1 in
+ if Term.eq_constr c (Lazy.force corb) then
+ mk_for (l2::acc) args
+ else
+ let l1 = mk_hform t1 in
+ get reify (Fapp(For, Array.of_list (l1::l2::acc)))
+ | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
mk_hform c
+
let hash_hform hash_hatom rf' hf =
let rec mk_hform = function
| Pos hp -> Pos (mk_hpform hp)
| Neg hp -> Neg (mk_hpform hp)
and mk_hpform {index = _; hval = hv} =
let new_hv = match hv with
- | Fatom a -> Fatom (hash_hatom a)
- | Fapp (fop, arr) -> Fapp (fop, Array.map mk_hform arr) in
+ | Fatom a -> Fatom (hash_hatom a)
+ | Fapp (fop, arr) -> Fapp (fop, Array.map mk_hform arr)
+ | FbbT (a, l) -> FbbT (hash_hatom a, List.map mk_hform l)
+ in
match get rf' new_hv with Pos x | Neg x -> x in
mk_hform hf
+
(** Flattening of Fand and For, removing of Fnot2 *)
let set_sign f f' =
if is_pos f then f' else neg f'
let rec flatten reify f =
match pform f with
- | Fatom _ -> f
+ | Fatom _ | FbbT _ -> f
| Fapp(Fnot2 _,args) -> set_sign f (flatten reify args.(0))
| Fapp(Fand, args) -> set_sign f (flatten_and reify [] (Array.to_list args))
| Fapp(For,args) -> set_sign f (flatten_or reify [] (Array.to_list args))
@@ -447,6 +515,21 @@ module Make (Atom:ATOM) =
flatten_or reify acc args
| _ -> flatten_or reify (flatten reify a :: acc) args
+ let rec right_assoc reify f =
+ match pform f with
+ | Fapp(Fand, args) when Array.length args > 2 ->
+ let a = args.(0) in
+ let rargs = Array.sub args 1 (Array.length args - 1) in
+ let f' = right_assoc reify (get reify (Fapp (Fand, rargs))) in
+ set_sign f (get reify (Fapp (Fand, [|a; f'|])))
+ | Fapp(For, args) when Array.length args > 2 ->
+ let a = args.(0) in
+ let rargs = Array.sub args 1 (Array.length args - 1) in
+ let f' = right_assoc reify (get reify (Fapp (For, rargs))) in
+ set_sign f (get reify (Fapp (For, [|a; f'|])))
+ | _ -> f
+
+
(** Producing Coq terms *)
let to_coq hf = let i = to_lit hf in
@@ -461,17 +544,20 @@ module Make (Atom:ATOM) =
let pf_to_coq = function
| Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|]
| Fapp(op,args) ->
- match op with
- | Ftrue -> Lazy.force cFtrue
- | Ffalse -> Lazy.force cFfalse
- | Fand -> mklApp cFand [| args_to_coq args|]
- | For -> mklApp cFor [| args_to_coq args|]
- | Fimp -> mklApp cFimp [| args_to_coq args|]
- | Fxor -> mklApp cFxor (Array.map to_coq args)
- | Fiff -> mklApp cFiff (Array.map to_coq args)
- | Fite -> mklApp cFite (Array.map to_coq args)
- | Fnot2 i -> mklApp cFnot2 [|mkInt i; to_coq args.(0)|]
- | Fforall _ -> failwith "pf_to_coq on forall"
+ (match op with
+ | Ftrue -> Lazy.force cFtrue
+ | Ffalse -> Lazy.force cFfalse
+ | Fand -> mklApp cFand [| args_to_coq args|]
+ | For -> mklApp cFor [| args_to_coq args|]
+ | Fimp -> mklApp cFimp [| args_to_coq args|]
+ | Fxor -> mklApp cFxor (Array.map to_coq args)
+ | Fiff -> mklApp cFiff (Array.map to_coq args)
+ | Fite -> mklApp cFite (Array.map to_coq args)
+ | Fnot2 i -> mklApp cFnot2 [|mkInt i; to_coq args.(0)|]
+ | Fforall _ -> failwith "pf_to_coq on forall")
+ | FbbT(a, l) -> mklApp cFbbT
+ [|mkInt (Atom.index a);
+ List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; to_coq f; l|]) l (mklApp cnil [|Lazy.force cint|])|]
let pform_tbl reify =
let t = Array.make reify.count pform_true in
@@ -512,33 +598,40 @@ module Make (Atom:ATOM) =
else
let pc =
match pform f with
- | Fatom a -> interp_atom a
- | Fapp(op, args) ->
- match op with
- | Ftrue -> Lazy.force ctrue
- | Ffalse -> Lazy.force cfalse
- | Fand -> interp_args candb args
- | For -> interp_args corb args
- | Fxor -> interp_args cxorb args
- | Fimp ->
- let r = ref (interp_form args.(Array.length args - 1)) in
- for i = Array.length args - 2 downto 0 do
- r := mklApp cimplb [|interp_form args.(i); !r|]
- done;
- !r
- | Fiff -> interp_args ceqb args
- | Fite ->
- (* TODO with if here *)
- mklApp cifb (Array.map interp_form args)
- | Fnot2 n ->
- let r = ref (interp_form args.(0)) in
- for i = 1 to n do
- r := mklApp cnegb [|!r|]
- done;
- !r
- |Fforall _ -> failwith "interp_to_coq on forall" in
+ | Fatom a -> interp_atom a
+ | Fapp(op, args) ->
+ (match op with
+ | Ftrue -> Lazy.force ctrue
+ | Ffalse -> Lazy.force cfalse
+ | Fand -> interp_args candb args
+ | For -> interp_args corb args
+ | Fxor -> interp_args cxorb args
+ | Fimp ->
+ let r = ref (interp_form args.(Array.length args - 1)) in
+ for i = Array.length args - 2 downto 0 do
+ r := mklApp cimplb [|interp_form args.(i); !r|]
+ done;
+ !r
+ | Fiff -> interp_args ceqb args
+ | Fite ->
+ (* TODO with if here *)
+ mklApp cifb (Array.map interp_form args)
+ | Fnot2 n ->
+ (let r = ref (interp_form args.(0)) in
+ for i = 1 to n do
+ r := mklApp cnegb [|!r|]
+ done;
+ !r)
+ | Fforall _ -> failwith "interp_to_coq on forall")
+ | FbbT(a, l) ->
+ mklApp cbv_eq
+ [|mkN (List.length l);
+ interp_atom a;
+ mklApp cof_bits [|List.fold_right (fun f l -> mklApp ccons [|Lazy.force cbool; interp_form f; l|]) l (mklApp cnil [|Lazy.force cbool|])|]|]
+ in
Hashtbl.add form_tbl l pc;
- pc
+ pc
+
and interp_args op args =
let r = ref (interp_form args.(0)) in
for i = 1 to Array.length args - 1 do
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index 4ee86e2..c26e279 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -1,19 +1,17 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
+open SmtMisc
+
module type ATOM =
sig
@@ -23,6 +21,9 @@ module type ATOM =
val equal : t -> t -> bool
val is_bool_type : t -> bool
+ val is_bv_type : t -> bool
+ val to_smt : Format.formatter -> t -> unit
+ val logic : t -> logic
end
@@ -42,6 +43,7 @@ type fop =
type ('a,'f) gen_pform =
| Fatom of 'a
| Fapp of fop * 'f array
+ | FbbT of 'a * 'f list
module type FORM =
sig
@@ -62,8 +64,11 @@ module type FORM =
val is_pos : t -> bool
val is_neg : t -> bool
- val to_string : ?pi:bool -> (hatom -> string) -> t -> string
- val to_smt : (hatom -> string) -> Format.formatter -> t -> unit
+ val to_smt : ?pi:bool ->
+ (Format.formatter -> hatom -> unit) ->
+ Format.formatter -> t -> unit
+
+ val logic : t -> logic
(* Building formula from positive formula *)
exception NotWellTyped of pform
@@ -80,6 +85,10 @@ module type FORM =
(** Flattening of [Fand] and [For], removing of [Fnot2] *)
val flatten : reify -> t -> t
+ (** Turn n-ary [Fand] and [For] into their right-associative
+ counter-parts *)
+ val right_assoc : reify -> t -> t
+
(** Producing Coq terms *)
val to_coq : t -> Term.constr
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 58de402..f839869 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.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 *)
(* *)
@@ -39,6 +35,30 @@ let mkName s =
let id = Names.id_of_string s in
Names.Name id
+
+let string_coq_constr t =
+ let rec fix rf x = rf (fix rf) x in
+ let pr = fix
+ Ppconstr.modular_constr_pr Pp.mt Structures.ppconstr_lsimpleconstr in
+ Pp.string_of_ppcmds (pr (Structures.constrextern_extern_constr t))
+
+
let string_of_name = function
Names.Name id -> Names.string_of_id id
| _ -> failwith "unnamed rel"
+
+
+(** Logics *)
+
+type logic_item =
+ | LUF
+ | LLia
+ | LBitvectors
+ | LArrays
+
+module SL = Set.Make (struct
+ type t = logic_item
+ let compare = Pervasives.compare
+ end)
+
+type logic = SL.t
diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli
index e5cf69f..a9de935 100644
--- a/src/trace/smtMisc.mli
+++ b/src/trace/smtMisc.mli
@@ -1,3 +1,15 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
val cInt_tbl : (int, Term.constr) Hashtbl.t
val mkInt : int -> Term.constr
type 'a gen_hashed = { index : int; hval : 'a; }
@@ -5,4 +17,8 @@ val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr
val declare_new_type : Names.variable -> Term.constr
val declare_new_variable : Names.variable -> Term.types -> Term.constr
val mkName : string -> Names.name
+val string_coq_constr : Term.constr -> string
val string_of_name : Names.name -> string
+type logic_item = LUF | LLia | LBitvectors | LArrays
+module SL : Set.S with type elt = logic_item
+type logic = SL.t
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 9042b8b..b410f88 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.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 *)
(* *)
@@ -352,11 +348,16 @@ let build_certif first_root confl =
let to_coq to_lit interp (cstep,
- cRes, cImmFlatten,
+ cRes, cWeaken, cImmFlatten,
cTrue, cFalse, cBuildDef, cBuildDef2, cBuildProj,
cImmBuildProj,cImmBuildDef,cImmBuildDef2,
cEqTr, cEqCgr, cEqCgrP,
cLiaMicromega, cLiaDiseq, cSplArith, cSplDistinctElim,
+ cBBVar, cBBConst, cBBOp, cBBNot, cBBEq, cBBDiseq,
+ cBBNeg, cBBAdd, cBBMul, cBBUlt, cBBSlt, cBBConc,
+ cBBExtr, cBBZextn, cBBSextn,
+ cBBShl, cBBShr,
+ cRowEq, cRowNeq, cExt,
cHole, cForallInst) confl sf =
let cuts = ref [] in
@@ -382,6 +383,12 @@ let to_coq to_lit interp (cstep,
mklApp cRes [|mkInt (get_pos c); Structures.mkArray (Lazy.force cint, args)|]
| Other other ->
begin match other with
+ | Weaken (c',l') ->
+ let out_cl cl =
+ List.fold_right (fun f l ->
+ mklApp ccons [|Lazy.force cint; out_f f; l|])
+ cl (mklApp cnil [|Lazy.force cint|]) in
+ mklApp cWeaken [|out_c c;out_c c'; out_cl l'|]
| ImmFlatten (c',f) -> mklApp cImmFlatten [|out_c c;out_c c'; out_f f|]
| True -> mklApp cTrue [|out_c c|]
| False -> mklApp cFalse [|out_c c|]
@@ -410,6 +417,45 @@ let to_coq to_lit interp (cstep,
let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm; Structures.Micromega_plugin_Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm|]) in
mklApp cSplArith [|out_c c; out_c orig; res'; l'|]
| SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|]
+ | BBVar res -> mklApp cBBVar [|out_c c; out_f res|]
+ | BBConst res -> mklApp cBBConst [|out_c c; out_f res|]
+ | BBOp (c1,c2,res) ->
+ mklApp cBBOp [|out_c c; out_c c1; out_c c2; out_f res|]
+ | BBNot (c1,res) ->
+ mklApp cBBNot [|out_c c; out_c c1; out_f res|]
+ | BBNeg (c1,res) ->
+ mklApp cBBNeg [|out_c c; out_c c1; out_f res|]
+ | BBAdd (c1,c2,res) ->
+ mklApp cBBAdd [|out_c c; out_c c1; out_c c2; out_f res|]
+ | BBMul (c1,c2,res) ->
+ mklApp cBBMul [|out_c c; out_c c1; out_c c2; out_f res|]
+ | BBUlt (c1,c2,res) ->
+ mklApp cBBUlt [|out_c c; out_c c1; out_c c2; out_f res|]
+ | BBSlt (c1,c2,res) ->
+ mklApp cBBSlt [|out_c c; out_c c1; out_c c2; out_f res|]
+ | BBConc (c1,c2,res) ->
+ mklApp cBBConc [|out_c c; out_c c1; out_c c2; out_f res|]
+ | BBExtr (c1,res) ->
+ mklApp cBBExtr [|out_c c; out_c c1; out_f res|]
+ | BBZextn (c1,res) ->
+ mklApp cBBZextn [|out_c c; out_c c1; out_f res|]
+ | BBSextn (c1,res) ->
+ mklApp cBBSextn [|out_c c; out_c c1; out_f res|]
+ | BBShl (c1,c2,res) ->
+ mklApp cBBShl [|out_c c; out_c c1; out_c c2; out_f res|]
+ | BBShr (c1,c2,res) ->
+ mklApp cBBShr [|out_c c; out_c c1; out_c c2; out_f res|]
+ | BBEq (c1,c2,res) ->
+ mklApp cBBEq [|out_c c; out_c c1; out_c c2; out_f res|]
+ | BBDiseq (res) -> mklApp cBBDiseq [|out_c c; out_f res|]
+ | RowEq (res) -> mklApp cRowEq [|out_c c; out_f res|]
+ | RowNeq (cl) ->
+ let out_cl cl =
+ List.fold_right (fun f l ->
+ mklApp ccons [|Lazy.force cint; out_f f; l|])
+ cl (mklApp cnil [|Lazy.force cint|]) in
+ mklApp cRowNeq [|out_c c; out_cl cl|]
+ | Ext (res) -> mklApp cExt [|out_c c; out_f res|]
| Hole (prem_id, concl) ->
let prem = List.map (fun cl -> match cl.value with Some l -> l | None -> assert false) prem_id in
let ass_name = Names.id_of_string ("ass"^(string_of_int (Hashtbl.hash concl))) in
@@ -439,32 +485,11 @@ let to_coq to_lit interp (cstep,
let nc = ref 0 in
while not (isRoot !r.kind) do r := prev !r; incr nc done;
let last_root = !r in
-
- (* let size = !nc in *)
- (* let max = Structures.max_array_size - 1 in *)
- (* let q,r1 = size / max, size mod max in *)
- (* let trace = *)
- (* let len = if r1 = 0 then q + 1 else q + 2 in *)
- (* Array.make len (Structures.mkArray (step, [|def_step|])) in *)
- (* for j = 0 to q - 1 do *)
- (* let tracej = Array.make Structures.max_array_size def_step in *)
- (* for i = 0 to max - 1 do *)
- (* r := next !r; *)
- (* tracej.(i) <- step_to_coq !r; *)
- (* done; *)
- (* trace.(j) <- Structures.mkArray (step, tracej) *)
- (* done; *)
- (* if r1 <> 0 then begin *)
- (* let traceq = Array.make (r1 + 1) def_step in *)
- (* for i = 0 to r1-1 do *)
- (* r := next !r; *)
- (* traceq.(i) <- step_to_coq !r; *)
- (* done; *)
- (* trace.(q) <- Structures.mkArray (step, traceq) *)
- (* end; *)
- (* (Structures.mkArray (mklApp carray [|step|], trace), last_root, !cuts) *)
- let tres = Structures.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r in
- (tres, last_root, !cuts)
+ (* Be careful, step_to_coq makes a side effect on cuts so it needs to be called first *)
+ let res =
+ Structures.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r
+ in
+ (res, last_root, !cuts)
diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli
index 57d0d42..f06ade4 100644
--- a/src/trace/smtTrace.mli
+++ b/src/trace/smtTrace.mli
@@ -1,3 +1,15 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2019 *)
+(* *)
+(* See file "AUTHORS" for the list of authors *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
val notUsed : int
val clear : unit -> unit
val next_id : unit -> SmtCertif.clause_id
@@ -37,15 +49,24 @@ val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int
val to_coq :
('a -> Term.constr) ->
('a list list * 'a list -> Term.types) ->
- Term.types Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
- Term.constr Lazy.t * Term.constr Lazy.t -> 'a SmtCertif.clause ->
- ('a SmtCertif.clause -> Term.constr * Term.constr) option ->
- Term.constr * 'a SmtCertif.clause * (Names.identifier * Term.types) list
+ Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+ Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+ Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+ Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+ Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+ Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+ Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+ Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+ Term.constr Lazy.t * Term.constr Lazy.t ->
+ 'a SmtCertif.clause ->
+ ('a SmtCertif.clause -> Term.types * Term.constr) option ->
+ Term.constr * 'a SmtCertif.clause *
+ (Names.identifier * Term.types) list
module MakeOpt :
functor (Form : SmtForm.FORM) ->
sig
generated by cgit (git 2.34.1) at 2024-06-29 02:58:05 +0000