diff options
Diffstat (limited to 'contrib/dimacs_to_smt.pl')
-rwxr-xr-x | contrib/dimacs_to_smt.pl | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/contrib/dimacs_to_smt.pl b/contrib/dimacs_to_smt.pl new file mode 100755 index 000000000..305db1d8e --- /dev/null +++ b/contrib/dimacs_to_smt.pl @@ -0,0 +1,36 @@ +#!/usr/bin/perl -w +# DIMACS to SMT +# Morgan Deters 2009 + +use strict; + +my ($nvars, $nclauses); +while(<>) { + next if /^c/; + + if(/^p cnf (\d+) (\d+)/) { + ($nvars, $nclauses) = ($1, $2); + print "(benchmark b\n"; + print ":status unknown\n"; + print ":logic QF_UF\n"; + for(my $i = 1; $i <= $nvars; ++$i) { + print ":extrapreds ((x$i))\n"; + } + print ":formula (and\n"; + next; + } + + print "(or"; + chomp; + @_ = split(/ /); + for(my $i = 0; $i < $#_; ++$i) { + if($_[$i] < 0) { + print " (not x" . -$_[$i] . ")"; + } else { + print " x" . $_[$i]; + } + } + print ")\n"; +} + +print "))\n"; |