Propositional Schemas

---------------------------------------------------------------------------
Informal Description
---------------------------------------------------------------------------

Clause schemas compactly encode a set of ground clauses.

A file begins with definitions of variable domains, e.g.:

(define people (mary john sam))
(define squares (range 1 8))

Schemas extend clauses with "forall" and "forsome":


(forall VARIABLE VALUES TEST BODY)
    Expand the BODY into a set of clauses, where in each clause the
    VARIABLE is replaced with one of VALUES.  Ground clause(s) are
    only included for a particular value if the TEST is true for
    that value.

	E.g.: (forall x people (ne x john) (or (likes john x)))
	expands to:
		(or (likes john mary))
		(or (likes john sam))

	This means "John likes everybody".  Note that the innermost "or"
	just indicates the start of the BODY of the clause schema: when
	"or" has a single argument, it is logically equivalent to that argument.

(forsome VARIABLE VALUES TEST BODY)
    Expand the BODY into a single clause, where any literals
    containing the VARIABLE are duplicated, once for each VALUE.
    Literals are only included for a particular value if the TEST is true for
    that value.

	E.g.: (forsome x people (ne x john) (or (likes john x)))
	expands to:
		(or (likes john mary) (likes john sam))

The parts of each clause schema must be nested as follows:

(forall .... (and ... (forsome ... (or ....))))

Thus, "forall" can apply to several clause bodys, but "forsome" must apply to
only a single clause body.

Arithmetic expressions involving constants and schema variables may appear 
as arguments to predicates in the body of a schema.  In an arithmetic expression,
"false" is represented by 0 and true by 1.  For example,

(forall x (range 1 4) t
	(or (foo x (eq 1 (mod x 2)))))

instantiates as the set of clauses:

(foo 1 1)
(foo 2 0)
(foo 3 1)
(foo 4 0)

---------------------------------------------------------------------------
BNF Syntax
---------------------------------------------------------------------------

SCHEMA_LIST = (SCHEMA)

SCHEMA = DEFINITION* CLAUSE_SCHEMA*

DEFINITION = (define DOMAIN_NAME DOMAIN_RANGE)

DOMAIN_RANGE = (CONSTANT*) | (range EXPR EXPR)

CLAUSE_SCHEMA = CLAUSE_CONJ | (forall VARIABLE DOMAIN EXPR CLAUSE_SCHEMA)

CLAUSE_CONJ = INNER_CLAUSE | (and INNTER_CLAUSE*)

INNER_CLAUSE = CLAUSE | (forsome VARIABLE DOMAIN EXPR INNER_CLAUSE)

CLAUSE = (or LIT*)

DOMAIN = DOMAIN_NAME | DOMAIN_RANGE

LIT = ATOM | (not ATOM) 

ATOM = PROPOSITION | (PREDICATE EXPR*)

EXPR = CONSTANT | VARIABLE | (OPERATOR2 EXPR EXPR) | (OPERATOR1 EXPR) | (member EXPR DOMAIN)

OPERATOR2 = eq | neq | = | < | > | <= | >= | and | or | + | - | * | / | mod

OPERATOR1 = not

PROPOSITION = LISP_SYMBOL

PREDICATE = LISP_SYMBOL

VARIABLE = LISP_SYMBOL

CONSTANT = LISP_SYMBOL | INTEGER | t

---------------------------------------------------------------------------
Examples
---------------------------------------------------------------------------

(define person (jim jack john))

# everyone either loves or hates each other

(forall x person t
  (forall y person (neq x y)
     (or (loves x y) (hates x y))))

# result:

(or (loves jim jack) (hates jim jack)
(or (loves jim john) (hates jim john)
(or (loves jack jim)  (hates jack jim))
(or (loves jack john) (hates jack john))
(or (loves john jim)  (hates john jim))
(or (loves john jack) (hates john jack))

# jack loves everyone

(forall x person (neq x jack)
   (or (loves jack x))

# result:

(or (loves jack jim))
(or (loves jack john))

# jack loves someone
	
(forsome x person (neq x jack)
   (or (loves jack x)))

# result:

(or (loves jack jim) (loves jack john))

# everyone loves someone

(forall x person t
  (forsome y person (neq x y)
	     (or (loves x y))))

# result:

(or (loves jim jack) (loves jim john))
(or (loves jack jim) (loves jack john))
(or (loves john jim) (loves john jack))

# someone loves everyone

(forsome x person t
   (forall y person (neq x y)
       (or (loves x y))))

# result:

** PARSE ERROR **

# encoding the problem of arranging 3 castles on 3x3 chess board
# such that there are no attacks

# At least one castle in each row
(forall i (range 1 3) t
    (forsome j (range 1 3) t
        (or (castle i j))))

# result:

(or (castle 1 1) (castle 1 2) (castle 1 3))
(or (castle 2 1) (castle 2 2) (castle 2 3))
(or (castle 3 1) (castle 3 2) (castle 3 3))

# No attacks
(forall i (range 1 3) t
   (forall j (range 1 3) t
       (forall x (range 1 3) (ne i x)
           (forall y (range 1 3) (ne j y)
                (or (not (castle i j))
                    (not castle x y))))))

# encoding a STRIPS style "pick up block" operator

(define block (red blue green))

(forall i (range 0 9)
  (forall x block t
     (forall y block (neq x y)
        (and 
            (or (not (pickup x y i) (on x y i)))
            (or (not (pickup x y i) (handempty i)))
            (or (not (pickup x y i) (on x y i)))
            (or (not (pickup x y i) (clear x i)))
            (or (not (pickup x y i) (not handempty (+ i 1))))
            (or (not (pickup x y i) (hold x (+ i 1))))
            (or (not (pickup x y i) (clear y (+ i 1))))))))

---------------------------------------------------------------------------
LISP Functions
---------------------------------------------------------------------------

(expand_schema SCHEMA_LIST
   # instantiates the SCHEMA_LIST and
   # returns a list of ground clauses

(propositionalize GROUND_CLAUSE_LIST)
   # returns (NVAR NCLAUSE PROPOSITIONAL_CLAUSE_LIST MAPPING)
   #   NVAR is the number of Boolean variables (propositions)
   #   NCLAUSE is the number of clauses
   #   PROPOSITIONAL_CLAUSE_LIST is a list of clauses in a format
   #      where propositions are represented by integers and negative
   #     literals by negative integers.
   #   MAPPING is an association list from the integer to symbolic
   #   form of the propositions.

example:

(propositionalize '((or (loves jack mary) (loves jack jane) (loves jack jim))
                             (or (not loves jack mary))))

returns

(3 2 ((1 2 3) (-1)) ((1 . (loves jack mary)) (2 . (loves jack jane))
                     (3 . (loves jack jim))))

(print_cnf FILE_NAME NVAR NCLAUSE PROPOSITIONAL_CLAUSE_LIST MAPPING)
# prints to a file in the .cnf format used by many solvers.  Example:

c Lines beginning with c are comments and appear only at start of file.
c The p line specifies cnf format, number vars, number clauses
c Variables are numbered starting at 1
c Each clause ends with 0
c Comments beginning cm are used by convention to store the
c mapping from numeric propositions to named propositions
c
cm 1 (loves jack mary)
cm 2 (loves jack jane)
cm 3 (loves jack jim)
p cnf 3 2
1 2 3 0
-1 0

(read_schema FILE_NAME)
# reads a SCHEMA from the file and returns a SCHEMA_LIST

(process_schema IN_FILE OUT_FILE)
# performs
#    (apply 'print_cnf OUT_FILE (propositionalize (read_schema IN_FILE)))

(interpret_model PROPOSITION_LIST MAPPING)
# PROPOSITION_LIST is a list of integers representing a truth
#  assignment.  Positive integers indicate the proposition is true,
#  negative false.  Integers missing from the list also correspond
#  to false propositions.
# MAPPING is an association list from the integer to symbolic form
#  of propositions, as described above.
# Returns a list of the true propositions in symbolic form.

(interpret_cnf CNF_FILE_NAME SOLN_FILE_NAME OUTPUT_FILE_NAME)
# CNF_FILE_NAME should contain "cm" comments specifying a mapping
# SOLN_FILE_NAME is a file containing integers that specify the model.
#    Non-numeric characters in this file are ignored.
# OUTPUT_FILE_NAME receives the interpreted solution in symbolic
#    form, with one literal per line.  There is no initial or final
#    parenthesis in the file: it is a sequence, rather than a list, of
#    literals.  The propositions are sorted on their last argument.
#    The comparison function for sort should apply numeric order
#    if both arguments are numeric, otherwise it should apply
#    lexigraphic ordering.