work on propositional layer, expression builder support for large expressions, output classes, and minisat

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