From 2163539a8b839acf98bda0e1a65f1fcca5232fb2 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Tue, 8 Dec 2009 10:10:20 +0000
Subject: work on propositional layer, expression builder support for large
 expressions, output classes, and minisat

---
 contrib/dimacs_to_smt.pl | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100755 contrib/dimacs_to_smt.pl

(limited to 'contrib')

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";
-- 
cgit v1.2.3