Merge branch 'feat/functionalsynthesis'

.gitignore

@@ -0,0 +1,80 @@
+# Build system and binaries
+Makefile
+cadet
+
+# Compiled source #
+###################
+*.com
+*.class
+*.dll
+*.exe
+*.o
+*.so
+
+# Logs and databases #
+######################
+*.log
+*.sql
+*.sqlite
+
+# OS generated files #
+######################
+*~
+.DS_Store
+.DS_Store?
+._*
+.Spotlight-V100
+.Trashes
+ehthumbs.db
+Thumbs.db
+
+# Xcode
+*.pbxuser
+*.mode1v3
+*.mode2v3
+*.perspectivev3
+*.xcuserstate
+project.xcworkspace/
+xcuserdata/
+
+# Python noise
+__pycache__
+*.pyc
+
+# Temp files
+*.*~
+
+# LaTeX noise
+*.acn
+*.acr
+*.alg
+*.aux
+*.bbl
+*.bcf
+*.blg
+*.dvi
+*.fdb_latexmk
+*.glg
+*.glo
+*.gls
+*.idx
+*.ilg
+*.ind
+*.ist
+*.lof
+*.log
+*.lot
+*.maf
+*.mtc
+*.mtc0
+*.nav
+*.nlo
+*.out
+*.pdfsync
+*.ps
+*.run.xml
+*.snm
+*.synctex.gz
+*.toc
+*.vrb
+*.xdy

Makefile.in

@@ -12,20 +12,27 @@ default: $(TARGET)
 OBJECTS = $(patsubst %.c, %.o, $(wildcard $(SRCDIR)/*.c))
 HEADERS = $(wildcard $(SRCDIR)/*.h)
 
-%.o: %.c $(HEADERS)
+LGL_OBJECTS = $(patsubst %.c, %.o, $(wildcard $(SRCDIR)/lingeling/*.c))
+LGL_HEADERS = $(wildcard $(SRCDIR)/lingeling/*.h)
+
+MINISAT_OBJECTS = $(patsubst %.cc, %.o, $(wildcard $(SRCDIR)/minisat/*.cc))
+MINISAT_OBJECTS += $(SRCDIR)/satsolver_minisat.o
+
+%.o: %.c $(HEADERS) $(LGL_HEADERS)
 	$(CC) $(CFLAGS) -c $< -o $@
 
-.PRECIOUS: $(TARGET) $(OBJECTS)
+.PRECIOUS: $(TARGET) $(OBJECTS) $(LGL_OBJECTS) $(MINISAT_OBJECTS)
 
-$(TARGET): $(OBJECTS)
-	$(CC) $(CFLAGS) $(OBJECTS) $(LIBS) -o $@
+$(TARGET): $(OBJECTS) $(LGL_OBJECTS) $(MINISAT_OBJECTS)
+	$(CC) $(CFLAGS) $(OBJECTS) $(LGL_OBJECTS) $(MINISAT_OBJECTS) $(LIBS) -o $@
 
 test: default
 	python scripts/tester.py --test
 
 profile: default
-	$(CC) $(CFLAGS) -pg $(OBJECTS) $(LIBS) -o $(TARGET) 
+	$(CC) $(CFLAGS) -pg $(OBJECTS) $(MINISAT_OBJECTS) $(LIBS) -o $(TARGET) 
 
 clean:
-	cd $(SRCDIR) && rm -f *.o *.h.gch *.plist 
+	cd $(SRCDIR) && rm -f *.o *.h.gch *.plist minisat/*.o lingeling/*.o
 	-rm -f $(TARGET)
+

certtools/and.qdimacs

@@ -0,0 +1,6 @@
+p cnf 3 3
+a 1 2 0
+e 3 0
+-1 -2 3 0
+1 -3 0
+2 -3 0

certtools/caqecertprove.sh

@@ -0,0 +1,20 @@
+#!/bin/bash
+
+./../cadet -c tmp.aig $1
+
+abc -c "read tmp.aig; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2;  print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; print_stats; dc2; write tmp.aig;"
+
+# abc -c "&r tmp.aig; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &put; write tmp.aig"
+
+./../../tools/caqe/certcheck $1 tmp.aig > tmp.aag
+
+aigtoaig tmp.aag tmp2.aig
+
+abc -c "&r tmp2.aig; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &dc2; &ps; &put; write tmp2.aig"
+
+cat tmp2.aig | aigtocnf | lingeling
+
+# picosat 
+
+# rm tmp.aag tmp.aig tmp.dimacs
+rm tmp.aig tmp.aag tmp2.aig

certtools/certshow.sh

@@ -0,0 +1,16 @@
+#!/bin/bash
+
+./../cadet -c tmp.aag $1
+
+aigtoaig tmp.aag tmp.aig
+
+# abc -c "read tmp.aig; dc2; write tmp.aig"
+# abc -c "read tmp.aig; rewrite; dfraig; write tmp.aig"
+abc -c "read tmp.aig; write tmp.aig"
+
+echo "Calling dot to generate the PDF"
+aigtodot tmp.aig | dot -Tpdf -o$1.pdf
+
+open $1.pdf
+
+rm tmp.aig tmp.aag $1.pdf

certtools/experiments/random.txt

@@ -0,0 +1,18 @@
+../qbf-instances/random2QBF/2qbf-5cnf-160var-320cl.1.qdimacs
+../qbf-instances/random2QBF/2qbf-5cnf-160var-320cl.4.qdimacs
+../qbf-instances/random2QBF/2qbf-5cnf-20var-40cl.3.qdimacs
+../qbf-instances/random2QBF/2qbf-5cnf-20var-40cl.6.qdimacs
+../qbf-instances/random2QBF/2qbf-5cnf-20var-80cl.5.qdimacs
+../qbf-instances/random2QBF/2qbf-5cnf-40var-160cl.4.qdimacs
+../qbf-instances/random2QBF/2qbf-5cnf-40var-160cl.5.qdimacs
+../qbf-instances/random2QBF/2qbf-5cnf-40var-160cl.9.qdimacs
+../qbf-instances/synthesis/add4y.aag.split02.qdimacs
+../qbf-instances/synthesis/bs8n.aag.split02.qdimacs
+../qbf-instances/synthesis/mult7.aag.split01.qdimacs
+../qbf-instances/synthesis/mv2n.aag.split02.qdimacs
+../qbf-instances/synthesis/mvs12y.aag.split02.qdimacs
+../qbf-instances/synthesis/mvs4n.aag.split02.qdimacs
+../qbf-instances/synthesis/mvs4y.aag.split02.qdimacs
+../qbf-instances/pec-2qbf/pec_example_circuit_6_1_2.qdimacs
+../qbf-instances/pec-2qbf/pec_example_circuit_6_3_1.qdimacs
+../qbf-instances/HardwareFixpoint/small-bug1-fixpoint-6.qdimacs

certtools/experiments/run_cadet.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+while read line; do 
+    echo $line
+    filename=${line%.qdimacs}
+    filename=${filename##*/}
+    gtimeout 60 ../cadet -c $filename.aig $line
+    abc -q "read $filename.aig; dc2; dc2; dc2; dc2; dc2; write $filename.minimized.aig"
+    ands=`head -n 1 $filename.aig | sed -E 's/(aig [0-9]* [0-9]* [0-9]* [0-9]* ([0-9]*))|.*/\2/'`
+    echo "Certificate has $ands gates."
+    ands=`head -n 1 $filename.minimized.aig | sed -E 's/(aig [0-9]* [0-9]* [0-9]* [0-9]* ([0-9]*))|.*/\2/'`
+    echo "Minimized certificate has $ands gates."
+done < "random.txt"

certtools/experiments/run_depqbf.sh

@@ -0,0 +1,13 @@
+#!/usr/bin/env bash
+
+solver="depqbf --trace --dep-man=simple --no-lazy-qpup"
+
+while read line; do 
+    echo $line 
+    filename=${line%.qdimacs}
+    filename=${filename##*/}
+    gtimeout 120 $solver $line > $filename.qrp
+    ../certificate/third_party/qrpcert-1.0.1/qrpcert --simplify $filename.qrp > $filename.depqbf.aag
+    ands=`head -n 1 $filename.depqbf.aag | sed -E 's/(aig [0-9]* [0-9]* [0-9]* [0-9]* ([0-9]*))|.*/\2/'`
+    echo "Certificate has $ands gates."
+done < "random.txt"

certtools/or.qdimacs

@@ -0,0 +1,6 @@
+p cnf 3 3
+a 1 2 0
+e 3 0
+1 2 -3 0
+-1 3 0
+-2 3 0

certtools/qbfcertprove.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+
+./../cadet -c tmp.aag --qbfcert $1
+
+# aigtoaig tmp.aag tmp.aig
+# abc -c "read tmp.aig; write tmp.aig; quit"
+# aigtoaig tmp.aig tmp.aag
+
+certcheck $1 tmp.aag | lingeling
+
+# picosat 
+
+# rm tmp.aag tmp.aig tmp.dimacs
+rm tmp.aag