modify default solver parametersmaster
authorUtz-Uwe Haus <lisp@uuhaus.de>
Fri, 13 May 2011 10:20:30 +0000 (13 12:20 +0200)
committerUtz-Uwe Haus <lisp@uuhaus.de>
Fri, 13 May 2011 10:20:30 +0000 (13 12:20 +0200)
Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>
cuddsat.lisp

index 72d9eea..b31df5c 100644 (file)
                            :vars vars)))
     (cuddapi:cudd-ref truevar) ;; it is used as inital cnf
     (cuddapi:cudd-enable-reordering-reporting manager)
-    (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift)
-    ;    (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift-conv)
     ;    (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift)
+    ;    (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift-conv)
+    ;    (cuddapi:cudd-autodyn-enable manager :cudd-reorder-sift)
+    (cuddapi:cudd-autodyn-enable manager :cudd-reorder-symm-sift)
+    (cuddapi:cudd-autodyn-enable manager :cudd-reorder-window-4)
+    (cuddapi:cudd-set-max-growth manager 12d0)
+    (format T ";; cudd: max sift growth ~D, max number of variables sifted: ~D~%"
+           (cuddapi:cudd-read-max-growth manager)
+           (cuddapi:cudd-read-sift-max-var manager))
     (loop :for c :in clauses
-       :do (sat-env-add-clause env c))
+       :with numclauses := (length clauses)
+       :for counter :downfrom numclauses
+       :do (sat-env-add-clause env c)
+       :when (= 0 (mod counter 10))
+       :do (format T "~&;; ~D clauses to go~%" counter))
     env))