From 5698cef78260c13b9a127c631842ac65a44e5d95 Mon Sep 17 00:00:00 2001
From: Utz-Uwe Haus <lisp@uuhaus.de>
Date: Tue, 1 Jun 2010 13:08:17 +0200
Subject: [PATCH] Add get-essential-variables implementation.

Signed-off-by: Utz-Uwe Haus <lisp@uuhaus.de>
---
 backend.lisp |  8 +++++++-
 dimacs.lisp  |  3 ++-
 package.lisp |  4 ++++
 satwrap.lisp | 45 +++++++++++++++++++++++++++++++++++++--------
 4 files changed, 50 insertions(+), 10 deletions(-)

diff --git a/backend.lisp b/backend.lisp
index 8ca81ea..8cb925c 100644
--- a/backend.lisp
+++ b/backend.lisp
@@ -28,6 +28,8 @@
 ;;; Code:
 
 
+(eval-when (:compile-toplevel :load-toplevel)
+  (declaim (optimize (speed 3) (debug 1) (safety 1))))
 
 (in-package #:satwrap.backend)
 
@@ -53,4 +55,8 @@ Returns T or NIL."))
   (:documentation "Return the values of INTERESTING-VARS in last SAT solution of BACKEND."))
 
 
-
+
+;; these generics do not need to be implemented as there are default implementations
+(defgeneric get-essential-variables (backend)
+  (:documentation "Compute the variables that are essential, i.e. fixed in all solutions of SOLVER. 
+Returns a list of literals fixed, sign according to phase."))
\ No newline at end of file
diff --git a/dimacs.lisp b/dimacs.lisp
index 42c0fff..a6a381b 100644
--- a/dimacs.lisp
+++ b/dimacs.lisp
@@ -27,7 +27,8 @@
 
 ;;; Code:
 
-
+(eval-when (:compile-toplevel :load-toplevel)
+  (declaim (optimize (speed 3) (debug 1) (safety 1))))
 
 (in-package #:satwrap)
 
diff --git a/package.lisp b/package.lisp
index 60e27a7..a621d45 100644
--- a/package.lisp
+++ b/package.lisp
@@ -32,11 +32,14 @@
 
 (defpackage #:satwrap.backend
   (:use #:cl)
+  ;; required interface for each backend:
   (:export #:satwrap-backend
 	   #:numvars
 	   #:add-clause
 	   #:satisfiablep
 	   #:solution)
+  ;; optional interface:
+  (:export #:get-essential-variables)
   )
 
 
@@ -54,6 +57,7 @@
   (:export #:satwrap-condition #:invalid-clause)
   ;; interface:
   (:export #:add-variable #:add-clause #:satisfiablep #:solution
+	   #:get-essential-variables
 	   #:with-sat-solver #:with-index-hash)
   ;; input/output
   (:export #:read-dimacs #:write-dimacs)
diff --git a/satwrap.lisp b/satwrap.lisp
index 8aec8eb..ddf2ef7 100644
--- a/satwrap.lisp
+++ b/satwrap.lisp
@@ -27,11 +27,20 @@
 
 ;;; Code:
 
+(eval-when (:compile-toplevel :load-toplevel)
+  (declaim (optimize (speed 3) (debug 1) (safety 1))))
 
 
 (in-package #:satwrap)
 
+(defvar *default-sat-backend* :precosat 
+  "Name of the default backend to be used by make-sat-solver.")
+
+(defparameter *satwrap-backends* 
+  `((:precosat . ,(find-class 'satwrap.precosat:precosat-backend)))
+  "Alist of symbolic name to backend class name for all supported backends.")
 
+
 ;;; Frontend:
 (defclass sat-solver ()
   ((backend :initarg :backend :accessor sat-solver-backend)
@@ -99,17 +108,10 @@
     (satwrap.backend:add-clause (sat-solver-backend solver) c)))
 
 
-(defvar *default-sat-backend* :precosat 
-  "Name of the default backend to be used by make-sat-solver.")
-
-(defparameter *satwrap-backends* 
-  `((:precosat . ,(find-class 'satwrap.precosat:precosat-backend)))
-  "Alist of symbolic name to backend class name for all supported backends.")
-
 (defun make-sat-solver (&optional (backend *default-sat-backend*))
   "Return a new sat solver instance. Optional argument BACKEND can be used to
 specify which backend should be used. It defaults to *default-sat-backend*."
-  (let ((be (assoc backend *satwrap-backends*)))
+  (let ((be (assoc backend *satwrap-backends* :test #'eq)))
     (if be
 	(make-instance 'sat-solver :backend (make-instance (cdr be)))
 	(error 'invalid-backend :name backend))))
@@ -146,6 +148,33 @@ sequence of 0/1 values for variables [1...N]. Keyword argument INTERESTING-VARS
 	    &key (interesting-vars (iota (sat-solver-numvars solver))))
     (satwrap.backend:solution (sat-solver-backend solver) interesting-vars)))
 
+(defgeneric get-essential-variables (solver)
+  (:documentation "Compute the variables that are essential, i.e. fixed in all solutions of SOLVER. 
+Returns a list of literals fixed, sign according to phase.")
+  (:method ((solver sat-solver))
+    ;; The backend may define a specialized method, but then it has to
+    ;; work on the one copy of data flushed to the solver. Precosat for example
+    ;; does not allow that, so we define the universal implementation here instead of
+    ;; a default implementation in the backend.
+    (let ((have-specialized-method 
+	   (find-method #'satwrap.backend:get-essential-variables
+			'()
+			`(,(class-of (sat-solver-backend solver)))
+			nil)))
+      (if have-specialized-method
+	  (progn
+	    (flush-to-backend solver)
+	    (satwrap.backend:get-essential-variables (sat-solver-backend solver)))
+	  (let ((fixed '()))
+	    (loop :for var :of-type (integer 1) :in (iota (sat-solver-numvars solver))
+	       :as res-for-+ := (satisfiablep solver :assume `(,var ,@fixed))
+	       :as res-for-- := (satisfiablep solver :assume `(,(- var) ,@fixed))
+	       :do (cond
+		     ((and res-for-+ (not res-for--)) 
+		      (push var fixed))
+		     ((and (not res-for-+) res-for--)
+		      (push (- var) fixed))))
+	    fixed)))))
 
 
 (defmacro with-sat-solver ((name numatoms &key (backend *default-sat-backend*))
-- 
2.11.4.GIT