backend.lisp

   1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
   2 ;;;
   3 ;;; backend.lisp --- SAT wrapper generic backend definition
   4
   5 ;; Copyright (C) 2010 Utz-Uwe Haus <lisp@uuhaus.de>
   6 ;; $Id:$
   7 ;; This code is free software; you can redistribute it and/or modify
   8 ;; it under the terms of the version 3 of the GNU General
   9 ;; Public License as published by the Free Software Foundation, as
  10 ;; clarified by the prequel found in LICENSE.Lisp-GPL-Preface.
  11 ;;
  12 ;; This code is distributed in the hope that it will be useful, but
  13 ;; without any warranty; without even the implied warranty of
  14 ;; merchantability or fitness for a particular purpose. See the GNU
  15 ;; Lesser General Public License for more details.
  16 ;;
  17 ;; Version 3 of the GNU General Public License is in the file
  18 ;; LICENSE.GPL that was distributed with this file. If it is not
  19 ;; present, you can access it from
  20 ;; http://www.gnu.org/copyleft/gpl.txt (until superseded by a
  21 ;; newer version) or write to the Free Software Foundation, Inc., 59
  22 ;; Temple Place, Suite 330, Boston, MA 02111-1307 USA
  23 ;;
  24 ;; Commentary:
  25
  26 ;;
  27
  28 ;;; Code:
  29
  30
  31 (eval-when (:compile-toplevel :load-toplevel)
  32   (declaim (optimize (speed 3) (debug 1) (safety 1))))
  33
  34 (in-package #:satwrap.backend)
  35 \f
  36 ;;; Backend:
  37 (defclass satwrap-backend ()
  38   ((name :accessor sat-backend-name :initarg :name)
  39    (version :accessor sat-backend-version :initarg :version))
  40   (:documentation "Superclass of all sat backends"))
  41
  42 \f
  43 ;; these generics need implementations for each backend:
  44 (defgeneric (setf numvars) (numvars backend)
  45   (:documentation "Declare number of variables used in backend."))
  46
  47 (defgeneric add-clause (backend clause)
  48   (:documentation "Add CLAUSE to CNF of BACKEND."))
  49
  50 (defgeneric satisfiablep (backend assumptions)
  51   (:documentation "Check BACKEND for satisfiability under ASSUMPTIONS.
  52 Returns T or NIL.")
  53   ;; no default implementation, but convert vector to list for dumb backends
  54   (:method ((be satwrap-backend) (assumptions vector))
  55     (satisfiablep be (coerce assumptions 'list))))
  56
  57 (defgeneric solution (backend interesting-vars)
  58   (:documentation "Return the values of INTERESTING-VARS in last SAT solution of BACKEND."))
  59
  60 \f
  61 ;; these generics do not need to be implemented as there are default implementations
  62 (defgeneric get-essential-variables (backend)
  63   (:documentation "Compute the variables that are essential, i.e. fixed in all solutions of SOLVER.
  64 Returns a list of literals fixed, sign according to phase."))
  65
  66 (defgeneric synchronize-backend (backend numvars new-clauses deleted-clauses old-clauses)
  67   (:documentation "Populate CNF with NUMVARS variables in BACKEND.
  68 NEW-CLAUSES are the clauses added since the last call to synchronize-backend,
  69 DELETED-CLAUSES are the clauses deleted since the last call to synchronize-backend,
  70 OLD-CLAUSES is the union of the NEW-CLAUSES and the OLD-CLAUSES minus the DELETED-CLAUSES when synchronize-backend was last called, including the DELETED-CLAUSES.")
  71   (:method ((backend satwrap-backend) numvars
  72             (new-clauses list)
  73             (deleted-clauses list)
  74             (old-clauses list))
  75     "Default implementation: Stuff everything into a possibly fresh solver."
  76     (reinitialize-instance backend)
  77     ;; declare proper number of variables
  78     (setf (numvars backend) numvars)
  79     ;; old clauses, including deletion
  80     (loop :for c :in old-clauses
  81        :unless (member c deleted-clauses :test #'equal)
  82        :do (add-clause backend c))
  83     ;; new clauses
  84     (dolist (c new-clauses)
  85       (add-clause backend c))))
  86
  87