[55827] trunk/dports/science/sbsat
snc at macports.org
snc at macports.org
Wed Aug 19 19:03:18 PDT 2009
Revision: 55827
http://trac.macports.org/changeset/55827
Author: snc at macports.org
Date: 2009-08-19 19:03:16 -0700 (Wed, 19 Aug 2009)
Log Message:
-----------
add variant
Modified Paths:
--------------
trunk/dports/science/sbsat/Portfile
Added Paths:
-----------
trunk/dports/science/sbsat/files/
trunk/dports/science/sbsat/files/patch-configure.ac.diff
trunk/dports/science/sbsat/files/patch-src-generator-Makefile.am.diff
trunk/dports/science/sbsat/files/patch-src-generator-gentest.cc.diff
trunk/dports/science/sbsat/files/slider3_base.py
Modified: trunk/dports/science/sbsat/Portfile
===================================================================
--- trunk/dports/science/sbsat/Portfile 2009-08-20 01:52:53 UTC (rev 55826)
+++ trunk/dports/science/sbsat/Portfile 2009-08-20 02:03:16 UTC (rev 55827)
@@ -21,6 +21,19 @@
sha1 08e9d0a447105fcd36518fab4653fcc8a0973ced \
rmd160 0ef8e2ee04d54b71fe837407ba3f771cca381636
+variant jeremy description {Enable Jeremy's modifications} {
+ patchfiles patch-src-generator-Makefile.am.diff \
+ patch-src-generator-gentest.cc.diff \
+ patch-configure.ac.diff
+ post-patch {
+ file copy ${filespath}/slider3_base.py ${worksrcpath}/src/generator/
+ reinplace s|@@PREFIX@@|${prefix}/bin| ${worksrcpath}/src/generator/gentest.cc
+ }
+
+ use_autoreconf yes
+
+}
+
configure.args --enable-optimization
test.run yes
Added: trunk/dports/science/sbsat/files/patch-configure.ac.diff
===================================================================
--- trunk/dports/science/sbsat/files/patch-configure.ac.diff (rev 0)
+++ trunk/dports/science/sbsat/files/patch-configure.ac.diff 2009-08-20 02:03:16 UTC (rev 55827)
@@ -0,0 +1,10 @@
+--- configure.ac 2009-06-14 12:58:58.000000000 -0400
++++ /Users/snc/Source/sbsat/configure.ac 2009-08-19 14:10:22.000000000 -0400
+@@ -312,6 +312,7 @@
+ AM_PROG_LEX
+ AC_PROG_YACC("bison -y")
+ # AC_PROG_LIBTOOL
++AM_PATH_PYTHON([2.5],, [:])
+
+ AC_SUBST(ECHO_N)
+ AC_SUBST(ECHO_C)
Added: trunk/dports/science/sbsat/files/patch-src-generator-Makefile.am.diff
===================================================================
--- trunk/dports/science/sbsat/files/patch-src-generator-Makefile.am.diff (rev 0)
+++ trunk/dports/science/sbsat/files/patch-src-generator-Makefile.am.diff 2009-08-20 02:03:16 UTC (rev 55827)
@@ -0,0 +1,25 @@
+--- src/generator/Makefile.am 2008-08-27 00:39:49.000000000 -0400
++++ /Users/snc/Source/sbsat/src/generator/Makefile.am 2009-08-17 11:00:07.000000000 -0400
+@@ -1,11 +1,19 @@
+ INCLUDES=-I$(top_srcdir)/include
+-EXTRA_DIST=testite.sh
++EXTRA_DIST=testite.sh slider3_base.py
+ noinst_LIBRARIES = libgen.a
+-libgen_a_SOURCES= xorgen.cc vanDerWaerden.cc rn.cc slider2.cc trans.cc rksat.cc \
+-add_tree.cc #rand_bdd.cc
++libgen_a_SOURCES= xorgen.cc vanDerWaerden.cc rn.cc slider2.cc trans.cc \
++rksat.cc add_tree.cc #rand_bdd.cc
++
+
+ bin_PROGRAMS = gentest
+ gentest_SOURCES = gentest.cc
+ gentest_LDADD = libgen.a #../libsbsat.la $(LIBM)
+
++bin_SCRIPTS = slider3.py
++CLEANFILES = $(bin_SCRIPTS)
+
++slider3.py: slider3_base.py
++ rm -f slider3.py
++ echo "#! " $(PYTHON) > slider3.py
++ cat slider3_base.py >> slider3.py
++ chmod +x slider3.py
Added: trunk/dports/science/sbsat/files/patch-src-generator-gentest.cc.diff
===================================================================
--- trunk/dports/science/sbsat/files/patch-src-generator-gentest.cc.diff (rev 0)
+++ trunk/dports/science/sbsat/files/patch-src-generator-gentest.cc.diff 2009-08-20 02:03:16 UTC (rev 55827)
@@ -0,0 +1,37 @@
+--- src/generator/gentest.cc 2008-08-27 00:39:49.000000000 -0400
++++ /Users/snc/Source/sbsat/src/generator/gentest.cc 2009-08-18 13:32:36.000000000 -0400
+@@ -122,7 +122,7 @@
+ if (argc < 3 || (argc > 2 && !strcmp(argv[2], "--help"))) {
+ fprintf(stderr, "usage: %s size sat\n", argv[0]);
+ fprintf(stderr, " size - num variables\n");
+- //fprintf(stderr, " sat - 0/1 = un/sat\n");
++ fprintf(stderr, " sat - 0/1 = un/sat\n");
+ return 0;
+ }
+ int size = atoi(argv[2]);
+@@ -130,6 +130,17 @@
+ slider2("ite", size, sat);
+ return 0;
+ } else
++ if (argc > 1 && !strcmp(argv[1], "slider3")) {
++ char *argv2[argc];
++ memset(argv2,0,sizeof(argv2));
++ argv2[0] = "@@PREFIX@@/slider3.py";
++
++ memcpy(argv2 + 1, argv + 2, sizeof(char *) * (argc - 2));
++ int oranges = execv(argv2[0], argv2);
++
++ printf("%s\n", strerror(oranges));
++ return oranges;
++ } else
+ if (argc > 1 && !strcmp(argv[1], "trans")) {
+ if (argc < 4 || (argc > 2 && !strcmp(argv[2], "--help"))) {
+ fprintf(stderr, "usage: %s trans size mult [seed]\n", argv[0]);
+@@ -276,6 +287,7 @@
+ fprintf(stderr, "usage: %s vdw --help\n", argv[0]);
+ fprintf(stderr, "usage: %s rn --help\n", argv[0]);
+ fprintf(stderr, "usage: %s slider2 --help\n", argv[0]);
++ fprintf(stderr, "usage: %s slider3 --help\n", argv[0]);
+ fprintf(stderr, "usage: %s rbdd --help\n", argv[0]);
+ fprintf(stderr, "usage: %s trans --help\n", argv[0]);
+ fprintf(stderr, "usage: %s add_tree --help\n", argv[0]);
Added: trunk/dports/science/sbsat/files/slider3_base.py
===================================================================
--- trunk/dports/science/sbsat/files/slider3_base.py (rev 0)
+++ trunk/dports/science/sbsat/files/slider3_base.py 2009-08-20 02:03:16 UTC (rev 55827)
@@ -0,0 +1,146 @@
+
+import sys
+from optparse import OptionParser
+
+def slider3(out_type, size, sat, offset):
+ if sat == 0:
+ slider3_unsat(out_type, size, offset)
+ elif sat == 1:
+ slider3_sat(out_type, size, offset)
+ else:
+ print >> sys.stderr, 'Error: Unknown out_type: %s' % out_type
+ exit(0)
+
+'''
+ * sliders
+ *
+ * unsat
+ * (first function -- notice 1,2,3,4,5,6)
+ #define add_state1(1, 2, 3, 4, 5, 6)
+ #equ(xor(1, and(-3, 5), nand(6, 4)), ite(2, or(5, -6), -5)))
+ *
+ * (second/third function)
+ #define add_state2(1, 2, 3, 4, 5, 6, 7)
+ #equ(6, xor(-1, xor(3, and(-4, 5), 4), equ(7, 2)))
+ #define add_state3(1, 2, 3, 4, 5, 6, 7)
+ #not(equ(6, xor(-1, xor(3, and(-4, 5), 4), equ(7, 2))))
+ *
+ * sat
+ * (first function -- notice 1,2,3,5,4,6 -- 5,4 switched)
+ #define add_state1(1, 2, 3, 5, 4, 6)\n");
+ #equ(xor(1, and(-3, 5), nand(6, 4)), ite(2, or(5, -6), -5)))
+ *
+ * (second/third functions - notice -- they are the same)
+ #define add_state2(1, 2, 3, 4, 5, 6)
+ #xor(-1, xor(3, and(-4, 5), 4), equ(6, 2))
+ #define add_state3(1, 2, 3, 4, 5, 6)
+ #xor(-1, xor(3, and(-4, 5), 4), equ(6, 2))
+ *
+ * numbers are generated the same way for both sat and unsat
+ int start1[6] = {1, 2*s+3, 2*s+1, size/2-1-3*s, size/2-1, size/2};
+ int start2[7] = {1, 2*s-1, 2*s+2, size/2-1-4*s, size/2-1-2*s, size/2-1-s, size/2};
+ *
+ * Please note that UNSAT version seems to be harder than SAT.
+ *
+ * Disclaimer: no formal analysis was done to verify SAT and UNSAT
+ * This means that for some n SAT might return UNSAT and UNSAT might return SAT problem.
+ * Please use the solver to verify UN/SAT.
+ *
+ * I have tested n for mulple of 10 starting 20.
+ * SAT instances seem to have at most 2 solutions.
+ *'''
+
+def slider3_sat(out_type, size, offset):
+ s = size/20
+ start1 = [1, 2*s+3, 2*s+1, size/2-1-3*s, size/2-1, size/2+1+offset]
+ start2 = [1, 2*s-1, 2*s+2, size/2-1-4*s, size/2-1-2*s, size/2-1-s, size/2+1+offset]
+ '''
+ print >> sys.stderr, start1
+ print >> sys.stderr, start2
+ '''
+ print "p bdd %d %d" % (size+offset,size)
+ print "; automatically generated SAT slider3 with size=%d " % size
+ print "; Disclaimer: no formal analysis was done to verify SAT and UNSAT"
+
+ #first function
+ print "#define add_state1(1, 2, 3, 5, 4, 6)"
+ print "#equ(xor(1, and(-3, 5), nand(6, 4)), ite(2, or(5, -6), -5)))"
+ for i in range(0, size/2):
+ sys.stdout.write("add_state1")
+ print tuple(start1)
+ for item in range(len(start1)):
+ start1[item] += 1
+
+ #second and third function
+ print("#define add_state2(1, 2, 3, 4, 5, 6)")
+ print("#xor(-1, xor(3, and(-4, 5), 4), equ(6, 2))")
+ print("#define add_state3(1, 2, 3, 4, 5, 6)")
+ print("#xor(-1, xor(3, and(-4, 5), 4), equ(6, 2))")
+ for i in range(0, size-size/2):
+ test = (i%2)+2
+ sys.stdout.write("add_state%d" % test)
+ print tuple(start2[0:5]+start2[6:])
+ for item in range(len(start2)):
+ start2[item] += 1
+
+def slider3_unsat(out_type, size):
+ # 80: 1675229 124.090s
+ # {1, 11, 9, 27, 39, 40 }
+ # {1, 7, 10, 21, 33, 35, 40}
+ # int start1[6] = {1, 17-6, 15-6, 24+3, 33+6, size/2};
+ # int start2[7] = {1, 12-5, 16-6, 18+3, 27+6, 29+6, size/2};
+
+ # {1, 11, 9, 27, 39, 40 }
+ # {1, 7, 10, 23, 31, 35, 40}
+ # int start1[6] = {1, 17-6, 15-6, 24+3, 33+6, size/2};
+ # int start2[7] = {1, 12-5, 16-6, 18+5, 27+4, 29+6, size/2};
+ #
+ # good one for 80 and more unsat
+ # int s=size/20;
+ # int start1[6] = {1, 2*s+3, 2*s+1, size/2-1-3*s, size/2-1, size/2};
+ # int start2[7] = {1, 2*s-1, 2*s+2, size/2-1-4*s, size/2-1-2*s, size/2-1-s, size/2};
+ #
+ # UNSAT
+
+ # fprintf(stderr, "{%d, %d, %d, %d, %d, %d}\n", start1[0], start1[1], start1[2], start1[3], start1[4], start1[5]);
+ # fprintf(stderr, "{%d, %d, %d, %d, %d, %d, %d}\n", start2[0], start2[1], start2[2], start2[3], start2[4], start2[5], start2[6]);
+ print "p bdd {0:d), {0:d)".format(size)
+ print("; automatically generated UNSAT slider3 with size={0:d}".format(size))
+ print("; Disclaimer: no formal analysis was done to verify SAT and UNSAT")
+
+ #first function
+ print("#define add_state1(1, 2, 3, 4, 5, 6)")
+ print("#equ(xor(1, and(-3, 5), nand(6, 4)), ite(2, or(5, -6), -5)))")
+
+ for i in range(0, size/2):
+ print "add_state1{0}".format(start1)
+ for item in start1:
+ start1[item] += 1
+
+ #Second and Third Function
+ print("#define add_state2(1, 2, 3, 4, 5, 6, 7)")
+ print("#equ(6, xor(-1, xor(3, and(-4, 5), 4), equ(7, 2)))")
+ print("#define add_state3(1, 2, 3, 4, 5, 6, 7)")
+ print("#not(equ(6, xor(-1, xor(3, and(-4, 5), 4), equ(7, 2))))")
+ for i in range(0, size-size/2):
+ print "add_state{0}".format([i%2+2] + start2)
+ for item in range(len(start2)):
+ start2[item] += 1
+
+
+#main method. Option parsing
+def main():
+ usage = "usage: %prog [options] size sat\n size num variables\n sat 1/0 (un/sat)"
+ parser = OptionParser(usage=usage)
+ parser.add_option("-o", "--offset", type="int", nargs=1, default=0, help="sets the offset", dest="offset")
+
+ (options, args) = parser.parse_args()
+ if len(args) != 2:
+ parser.error("Try again")
+ [size, sat] = map(int, args)
+
+ slider3('ite', size, sat, offset=options.offset)
+
+if __name__ == "__main__":
+ main()
+
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.macosforge.org/pipermail/macports-changes/attachments/20090819/6ab6a51d/attachment-0001.html>
More information about the macports-changes
mailing list