diff options
author | ckeller <ckeller@users.noreply.github.com> | 2019-01-28 23:19:12 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-28 23:19:12 +0100 |
commit | 7021c53d4ecf97c82ccebb6bb45f5305d8b482ea (patch) | |
tree | ba7537e1e813cabf9ee0d910f845c71fa5f446e7 /src/lia | |
parent | 36548d6634864a131cc83ce21491c797163de305 (diff) | |
download | smtcoq-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/lia')
-rw-r--r-- | src/lia/Lia.v | 77 | ||||
-rw-r--r-- | src/lia/lia.ml | 9 | ||||
-rw-r--r-- | src/lia/lia.mli | 12 |
3 files changed, 53 insertions, 45 deletions
diff --git a/src/lia/Lia.v b/src/lia/Lia.v index dbd3b9c..cafac1b 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -1,31 +1,19 @@ (**************************************************************************) (* *) (* 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 *) (* *) (**************************************************************************) -Require Import Bool. -Require Import List. -Require Import Int63. -Require Import PArray. -Require Import RingMicromega. -Require Import ZMicromega. -Require Import Tauto. -Require Import Psatz. +Require Import Bool List Int63 PArray. +Require Import Misc State SMT_terms Euf. -Require Import Misc State. -Require Import SMT_terms. -Require Import SMTCoq.euf.Euf. +Require Import RingMicromega ZMicromega Tauto Psatz. Local Open Scope array_scope. Local Open Scope int63_scope. @@ -265,6 +253,7 @@ Section certif. end | None => None end + | Form.FbbT _ _ => None end. End Build_form. @@ -365,7 +354,7 @@ Section certif. Section Proof. - Variables (t_i : array typ_eqb) + Variables (t_i : array SMT_classes.typ_compdec) (t_func : array (Atom.tval t_i)) (ch_atom : Atom.check_atom t_atom) (ch_form : Form.check_form t_form) @@ -377,8 +366,11 @@ Section certif. Local Notation interp_form_hatom := (Atom.interp_form_hatom t_i t_func t_atom). + Local Notation interp_form_hatom_bv := + (Atom.interp_form_hatom_bv t_i t_func t_atom). + Local Notation rho := - (Form.interp_state_var interp_form_hatom t_form). + (Form.interp_state_var interp_form_hatom interp_form_hatom_bv t_form). Local Notation t_interp := (t_interp t_i t_func t_atom). @@ -393,17 +385,17 @@ Section certif. Let def_t_form : default t_form = Form.Ftrue. Proof. - destruct (Form.check_form_correct interp_form_hatom _ ch_form) as [H _]; destruct H; auto. + destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [H _]; destruct H; auto. Qed. Let wf_t_form : Form.wf t_form. Proof. - destruct (Form.check_form_correct interp_form_hatom _ ch_form) as [H _]; destruct H; auto. + destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form) as [H _]; destruct H; auto. Qed. Let wf_rho : Valuation.wf rho. Proof. - destruct (Form.check_form_correct interp_form_hatom _ ch_form); auto. + destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form); auto. Qed. Lemma build_positive_atom_aux_correct : @@ -446,7 +438,7 @@ Section certif. Proof. intros a z. destruct a;simpl;try discriminate;auto. - destruct c;[discriminate | intros Heq;inversion Heq;trivial]. + destruct c;[discriminate | intros Heq;inversion Heq;trivial | discriminate]. destruct u;try discriminate; case_eq (build_positive i);try discriminate; intros p Hp Heq;inversion Heq;clear Heq;subst; @@ -682,10 +674,10 @@ Opaque build_z_atom interp_aux. case a;simpl; try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). - intros u; destruct u; intros j vm vm' pe _H_ Hlt Ht; + intros u; destruct u; intros jind vm vm' pe _H_ Hlt Ht; try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). - generalize (Hb j vm vm'). - destruct (build_pexpr vm j) as (vm0, pe0); intro W1. + generalize (Hb jind vm vm'). + destruct (build_pexpr vm jind) as (vm0, pe0); intro W1. intros Heq Hwf;inversion Heq;clear Heq;subst. assert (W:= W1 pe0 Hlt Ht (refl_equal _) Hwf). decompose [and] W;clear W W1. @@ -786,10 +778,10 @@ Transparent build_z_atom. Opaque build_z_atom interp_aux. case a;simpl; try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). - intro u; destruct u; intros i vm vm' pe Ht; + intro u; destruct u; intros ind vm vm' pe Ht; try (intros;apply build_pexpr_atom_aux_correct_z;trivial;fail). - generalize (Hb i vm); clear Hb. - destruct (build_pexpr vm i) as (vm0,pe0); intro IH. + generalize (Hb ind vm); clear Hb. + destruct (build_pexpr vm ind) as (vm0,pe0); intro IH. intros Heq Hwf;inversion Heq;clear Heq;subst. assert (W:= IH vm' pe0 Ht (refl_equal _) Hwf). decompose [and] W;clear W IH. @@ -1007,7 +999,6 @@ Transparent build_z_atom. destruct t0;inversion H13;clear H13;subst. simpl. apply (Z.eqb_eq (Zeval_expr (interp_vmap vm') pe1) (Zeval_expr (interp_vmap vm') pe2)). - Qed. Lemma build_formula_correct : @@ -1037,7 +1028,7 @@ Transparent build_z_atom. Lemma build_not2_pos_correct : forall vm f l i, - bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l -> bounded_bformula (fst vm) (build_not2 i f) /\ (Form.interp interp_form_hatom t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (build_not2 i f)). + bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l -> bounded_bformula (fst vm) (build_not2 i f) /\ (Form.interp interp_form_hatom interp_form_hatom_bv t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (build_not2 i f)). Proof. simpl; intros vm f l i H1 H2 H3; split; unfold build_not2. apply fold_ind; auto. @@ -1050,7 +1041,7 @@ Transparent build_z_atom. Lemma build_not2_neg_correct : forall vm f l i, - bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l = false -> bounded_bformula (fst vm) (N (build_not2 i f)) /\ (Form.interp interp_form_hatom t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (N (build_not2 i f))). + bounded_bformula (fst vm) f -> (rho (Lit.blit l) <-> eval_f (Zeval_formula (interp_vmap vm)) f) -> Lit.is_pos l = false -> bounded_bformula (fst vm) (N (build_not2 i f)) /\ (Form.interp interp_form_hatom interp_form_hatom_bv t_form (Form.Fnot2 i l) <-> eval_f (Zeval_formula (interp_vmap vm)) (N (build_not2 i f))). Proof. simpl; intros vm f l i H1 H2 H3; split; unfold build_not2. apply fold_ind; auto. @@ -1124,9 +1115,9 @@ Transparent build_z_atom. nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = nth_error (snd vm')(nat_of_P (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ - (Form.interp interp_form_hatom t_form f <-> eval_f (Zeval_formula (interp_vmap vm')) bf). + (Form.interp interp_form_hatom interp_form_hatom_bv t_form f <-> eval_f (Zeval_formula (interp_vmap vm')) bf). Proof. - unfold build_hform; intros build_var Hbv [h| | |i l|l|l|l|a b|a b|a b c] vm vm' bf; try discriminate. + unfold build_hform; intros build_var Hbv [h| | |i l|l|l|l|a b|a b|a b c|a ls] vm vm' bf; try discriminate. (* Fatom *) case_eq (build_formula vm h); try discriminate; intros [vm0 f] Heq H1 H2; inversion H1; subst vm0; subst bf; apply build_formula_correct; auto. (* Ftrue *) @@ -1259,7 +1250,7 @@ Transparent build_z_atom. (Var.interp rho v <-> eval_f (Zeval_formula (interp_vmap vm')) bf). Proof. unfold build_var; apply foldi_down_cont_ind; try discriminate. - intros i cont _ Hlen Hrec v vm vm' bf; unfold is_true; intros H1 H2; replace (Var.interp rho v) with (Form.interp interp_form_hatom t_form (t_form.[v])). + intros i cont _ Hlen Hrec v vm vm' bf; unfold is_true; intros H1 H2; replace (Var.interp rho v) with (Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form.[v])). apply (build_hform_correct cont); auto. unfold Var.interp; rewrite <- wf_interp_form; auto. Qed. @@ -1275,7 +1266,7 @@ Transparent build_z_atom. nth_error (snd vm) (nat_of_P (fst vm - p) - 1) = nth_error (snd vm')(nat_of_P (fst vm' - p) - 1)) /\ bounded_bformula (fst vm') bf /\ - (Form.interp interp_form_hatom t_form f <-> eval_f (Zeval_formula (interp_vmap vm')) bf). + (Form.interp interp_form_hatom interp_form_hatom_bv t_form f <-> eval_f (Zeval_formula (interp_vmap vm')) bf). Proof. apply build_hform_correct; apply build_var_correct. Qed. @@ -1293,7 +1284,7 @@ Transparent build_z_atom. Proof. unfold build_nlit; intros l vm vm' bf; case_eq (build_form vm (t_form .[ Lit.blit (Lit.neg l)])); try discriminate. intros [vm1 f] Heq H1 H2; inversion H1; subst vm1; subst bf; case_eq (Lit.is_pos (Lit.neg l)); intro Heq2. - replace (negb (Lit.interp rho l)) with (Form.interp interp_form_hatom t_form (t_form .[ Lit.blit (Lit.neg l)])). + replace (negb (Lit.interp rho l)) with (Form.interp interp_form_hatom interp_form_hatom_bv t_form (t_form .[ Lit.blit (Lit.neg l)])). apply build_form_correct; auto. unfold Lit.interp; replace (Lit.is_pos l) with false. rewrite negb_involutive; unfold Var.interp; rewrite <- wf_interp_form; auto; rewrite Lit.blit_neg; auto. @@ -1495,9 +1486,9 @@ Transparent build_z_atom. unfold C.valid;rewrite H5. apply ZTautoChecker_sound with c;trivial. apply C.interp_true. - destruct (Form.check_form_correct interp_form_hatom _ ch_form);trivial. + destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form);trivial. intros _;apply C.interp_true. - destruct (Form.check_form_correct interp_form_hatom _ ch_form);trivial. + destruct (Form.check_form_correct interp_form_hatom interp_form_hatom_bv _ ch_form);trivial. Qed. @@ -1610,3 +1601,11 @@ Transparent build_z_atom. End Proof. End certif. + + + +(* + Local Variables: + coq-load-path: ((rec ".." "SMTCoq")) + End: +*) diff --git a/src/lia/lia.ml b/src/lia/lia.ml index e5f2fe9..adeed4e 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.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 *) (* *) @@ -160,6 +156,7 @@ let rec smt_Form_to_coq_micromega_formula tbl l = failwith "Lia.smt_Form_to_coq_micromega_formula: wrong number of arguments for Fnot2" else smt_Form_to_coq_micromega_formula tbl l.(0) + | FbbT _ -> assert false | Fapp (Fforall _, _) -> assert false in if Form.is_pos l then v diff --git a/src/lia/lia.mli b/src/lia/lia.mli index 3c8e582..93361f2 100644 --- a/src/lia/lia.mli +++ b/src/lia/lia.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 pos_of_int : int -> Structures.Micromega_plugin_Micromega.positive val z_of_int : int -> Structures.Micromega_plugin_Micromega.z type my_tbl = { tbl : (SmtAtom.hatom, int) Hashtbl.t; mutable count : int; } |