1 files changed, 66 insertions, 0 deletions
diff --git a/src/lfsc/tests/cvc4tov b/src/lfsc/tests/cvc4tov
new file mode 100755
index 0000000..183629e
--- /dev/null
+++ b/src/lfsc/tests/cvc4tov
@@ -0,0 +1,66 @@
+#!/bin/bash
+set -e
+
+name=${1%.*}
+DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
+
+echo "Running CVC4..."
+cvc4 --proof --dump-proof --no-simplification --fewer-preprocessing-holes --no-bv-eq --no-bv-ineq --no-bv-algebraic $1 > $name.lfsc
+
+# sed -i -e '1d' $name.lfsc
+
+# echo "Convert LFSC proof to SMTCoq..."
+$DIR/../lfsctosmtcoq.native $name.lfsc | grep "^1:" -A 9999999 > $name.log
+
+echo "Creating Coq file..."
+cat > $name.v <<EOF
+Require Import SMTCoq Bool List.
+Import ListNotations BVList.BITVECTOR_LIST FArray.
+Local Open Scope list_scope.
+Local Open Scope farray_scope.
+Local Open Scope bv_scope.
+
+Section File.
+  Verit_Checker "$name.smt2" "$name.log".
+End File.
+EOF
+
+cat > ${name}_debug.v <<EOF
+Require Import SMTCoq Bool List.
+Import ListNotations BVList.BITVECTOR_LIST FArray.
+Local Open Scope list_scope.
+Local Open Scope farray_scope.
+Local Open Scope bv_scope.
+
+Section File.
+  Verit_Checker_Debug "$name.smt2" "$name.log".
+End File.
+
+(*
+Section File2.
+  Parse_certif_verit t_i t_func t_atom t_form root used_roots trace "$name.smt2" "$name.log".
+  Compute (
+      let (nclauses, t, confl) := trace in
+      let s := add_roots (S.make nclauses) root used_roots in
+      let s' := Structures.trace_fold
+        (fun s a =>
+          (@Euf_Checker.step_checker t_i t_func t_atom t_form) s a
+        ) s t in
+      let s'' := PArray.mapi (fun i c => (to_Z i, List.map to_Z c)) s' in
+      (PArray.to_list s'', to_Z confl)).
+End File2.
+*)
+EOF
+
+cat > ${name}_debug.sh <<EOF
+#!/bin/sh
+coqc -q -R $DIR/../.. SMTCoq ${name}_debug.v | grep --color -E "\[0(;\s+0)*\]| 0|"
+EOF
+
+chmod +x ${name}_debug.sh
+
+
+echo "Checking with Coq..."
+coqc -q -R $DIR/../.. SMTCoq $name.v
+
+exit 0