src/HOL/SMT/lib/scripts/cert_smt.pl

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SMT/lib/scripts/cert_smt.pl	Tue Oct 20 10:11:30 2009 +0200
@@ -0,0 +1,33 @@
+#
+# Author: Sascha Boehme, TU Muenchen
+#
+# Fake SMT solver: check that input matches previously computed input and
+# and return previously computed output.
+#
+
+use strict;
+use File::Compare;
+
+
+# arguments
+
+my $cert_path = $ARGV[0];
+my $new_problem = $ARGV[1];
+
+
+# check content of new problem file against old problem file
+
+my $old_problem = $cert_path;
+my $old_proof = $cert_path . ".proof";
+
+if (-e $old_problem and compare($old_problem, $new_problem) == 0) {
+  if (-e $old_proof) {
+    open FILE, "<$old_proof";
+    foreach (<FILE>) {
+      print $_;
+    }
+    close FILE;
+  }
+  else { print "ERROR: unable to open proof file\n"; }
+}
+else { print "ERROR: bad problem\n"; }