contrib/dimacs_to_smt.pl

   1 #!/usr/bin/perl -w
   2 # DIMACS to SMT
   3 # Morgan Deters
   4 # Copyright (c) 2009, 2010, 2011  The CVC4 Project
   5
   6 use strict;
   7
   8 my ($nvars, $nclauses);
   9 while(<>) {
  10     next if /^c/;
  11
  12     if(/^p cnf (\d+) (\d+)/) {
  13         ($nvars, $nclauses) = ($1, $2);
  14         print "(benchmark b\n";
  15         print ":status unknown\n";
  16         print ":logic QF_UF\n";
  17         for(my $i = 1; $i <= $nvars; ++$i) {
  18             print ":extrapreds ((x$i))\n";
  19         }
  20         print ":formula (and\n";
  21         next;
  22     }
  23
  24     print "(or";
  25     chomp;
  26     @_ = split(/ /);
  27     for(my $i = 0; $i < $#_; ++$i) {
  28         if($_[$i] < 0) {
  29             print " (not x" . -$_[$i] . ")";
  30         } else {
  31             print " x" . $_[$i];
  32         }
  33     }
  34     print ")\n";
  35 }
  36
  37 print "))\n";