aboutsummaryrefslogtreecommitdiffstats
path: root/src/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'src/extraction')
-rw-r--r--src/extraction/Extract.v4
-rw-r--r--src/extraction/extrNative.ml16
-rw-r--r--src/extraction/extrNative.mli16
-rw-r--r--src/extraction/sat_checker.ml16
-rw-r--r--src/extraction/sat_checker.mli16
-rw-r--r--src/extraction/smt_checker.ml16
-rw-r--r--src/extraction/smt_checker.mli16
-rw-r--r--src/extraction/smtcoq.ml16
-rw-r--r--src/extraction/test.ml16
-rw-r--r--src/extraction/verit_checker.ml16
-rw-r--r--src/extraction/zchaff_checker.ml16
11 files changed, 162 insertions, 2 deletions
diff --git a/src/extraction/Extract.v b/src/extraction/Extract.v
index 1161f48..2663fb3 100644
--- a/src/extraction/Extract.v
+++ b/src/extraction/Extract.v
@@ -1,13 +1,13 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2015 *)
+(* Copyright (C) 2011 - 2016 *)
(* *)
(* Michaël Armand *)
(* Benjamin Grégoire *)
(* Chantal Keller *)
(* *)
-(* Inria - École Polytechnique - MSR-Inria Joint Lab *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
diff --git a/src/extraction/extrNative.ml b/src/extraction/extrNative.ml
index 4d56287..d8d1265 100644
--- a/src/extraction/extrNative.ml
+++ b/src/extraction/extrNative.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
type comparison = Eq | Lt | Gt
type 'a carry = C0 of 'a | C1 of 'a
diff --git a/src/extraction/extrNative.mli b/src/extraction/extrNative.mli
index 14eff5f..3f255bf 100644
--- a/src/extraction/extrNative.mli
+++ b/src/extraction/extrNative.mli
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
type comparison = Eq | Lt | Gt
type 'a carry = C0 of 'a | C1 of 'a
diff --git a/src/extraction/sat_checker.ml b/src/extraction/sat_checker.ml
index 59635e0..0ed36a3 100644
--- a/src/extraction/sat_checker.ml
+++ b/src/extraction/sat_checker.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
(** val negb : bool -> bool **)
let negb = function
diff --git a/src/extraction/sat_checker.mli b/src/extraction/sat_checker.mli
index 5fa2757..ed63e26 100644
--- a/src/extraction/sat_checker.mli
+++ b/src/extraction/sat_checker.mli
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
val negb : bool -> bool
type 'a list =
diff --git a/src/extraction/smt_checker.ml b/src/extraction/smt_checker.ml
index 53aa130..ed446b7 100644
--- a/src/extraction/smt_checker.ml
+++ b/src/extraction/smt_checker.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f
diff --git a/src/extraction/smt_checker.mli b/src/extraction/smt_checker.mli
index 502d6f3..2fbf9b8 100644
--- a/src/extraction/smt_checker.mli
+++ b/src/extraction/smt_checker.mli
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
type __ = Obj.t
type unit0 =
diff --git a/src/extraction/smtcoq.ml b/src/extraction/smtcoq.ml
index f3bd6b1..07ed9a3 100644
--- a/src/extraction/smtcoq.ml
+++ b/src/extraction/smtcoq.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
type solver = Zchaff | Verit
diff --git a/src/extraction/test.ml b/src/extraction/test.ml
index 0b16b7f..f91a661 100644
--- a/src/extraction/test.ml
+++ b/src/extraction/test.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
let _ = Printf.printf "Zchaff_checker.checker \"tests/sat1.cnf\" \"tests/sat1.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat1.cnf" "tests/sat1.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"tests/sat2.cnf\" \"tests/sat2.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat2.cnf" "tests/sat2.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"tests/sat3.cnf\" \"tests/sat3.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat3.cnf" "tests/sat3.zlog")
diff --git a/src/extraction/verit_checker.ml b/src/extraction/verit_checker.ml
index e317dcf..20040bc 100644
--- a/src/extraction/verit_checker.ml
+++ b/src/extraction/verit_checker.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
open SmtMisc
open SmtCertif
open SmtForm
diff --git a/src/extraction/zchaff_checker.ml b/src/extraction/zchaff_checker.ml
index 79e87cc..60d0a38 100644
--- a/src/extraction/zchaff_checker.ml
+++ b/src/extraction/zchaff_checker.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
open SmtCertif
open SmtForm
open SatAtom
generated by cgit (git 2.34.1) at 2024-07-01 12:18:33 +0000