src/HOL/SMT/lib/scripts/cert_smt.pl
author boehmes
Thu, 22 Oct 2009 09:49:48 +0200
changeset 33058 70f5c18e975d
parent 33010 39f73a59e855
permissions -rw-r--r--
fixed permissions -- this is a script, not an executable
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33010
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     1
#
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     2
# Author: Sascha Boehme, TU Muenchen
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     3
#
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     4
# Fake SMT solver: check that input matches previously computed input and
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     5
# and return previously computed output.
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     6
#
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     7
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     8
use strict;
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
     9
use File::Compare;
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    10
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    11
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    12
# arguments
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    13
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    14
my $cert_path = $ARGV[0];
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    15
my $new_problem = $ARGV[1];
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    16
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    17
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    18
# check content of new problem file against old problem file
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    19
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    20
my $old_problem = $cert_path;
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    21
my $old_proof = $cert_path . ".proof";
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    22
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    23
if (-e $old_problem and compare($old_problem, $new_problem) == 0) {
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    24
  if (-e $old_proof) {
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    25
    open FILE, "<$old_proof";
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    26
    foreach (<FILE>) {
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    27
      print $_;
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    28
    }
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    29
    close FILE;
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    30
  }
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    31
  else { print "ERROR: unable to open proof file\n"; }
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    32
}
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset
    33
else { print "ERROR: bad problem\n"; }