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

#
# 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"; }