Interface to SULFA System for use by users and theorem proving tools:  
Uses of this interface can be seen in:

books/clause-processors/sat-clause-processor.lisp
books/sat-tests/test-incremental.lisp
books/sat-tests/test-abstract-refine.lisp


------------------------ ACL2 Interface -------------------------

These commands are defined in the file sat.lisp and are intended
to be used by theorem proving tools.  All of the interface functions 
are in the ACL2 package, along with the $sat stobj.  Note that almost
every function here inputs at least $sat and state; and outputs at least 
erp, $sat, and state.  Here $sat is the $sat stobj, which is created
by the book and is initialized by the command sat-new-problem.  
The argument state is the current ACL2 state.  And the return value 
erp is nil if the function has no error or an error string otherwise.
You can safely ignore the erp output, since we always use hard
ACL2 errors anyway.  The reason for the erp is output is just to 
make the output to the ACL2 command line more pretty.


---Control Commands---

(sat-new-problem $sat state) => (erp $sat state):
Remove all data from the current satisfiability problem so that we can 
start a new one.  This function must be called before calling ANY other 
functions.


(sat-new-problem! $sat state) => (erp $sat state):
Same as sat-new-problem, but also resets the uninterpreted function markers 
(see sat-mark-uninterpreted).


(sat-end-problem $sat state) => (erp $sat state):
Remove all data from the current problem, but do not make room for a new 
one.  This should be used when you are done with the SAT solver if you 
want to save memory.


(sat-end-problem! $sat state) => (erp $sat state):
Same as sat-end-problem, but also removes the uninterpreted function markers
(see sat-mark-uninterpreted) and all state related to the SULFA recognizer,
which otherwise persists from one problem to the next.


(sat-set-verbosity x $sat state) => (erp $sat state):
Set the level of verbosity in the messages printed out to the ACL2 screen.
The verbosity level "x" is an integer from 0 to 4, with 0 meaning no
output and 4 meaning as much as possible.


(sat-mark-uninterpreted fn $sat state) => (erp $sat state):
Mark an ACL2 function to be treated as uninterpreted.  This
can be used as a means of abstracting recursive functions that
otherwise would not be in SULFA.  

NOTE: Uninterpreted markers persist from one SAT problem to
another.  If you want to reset them, you need to use the
sat-new-problem!.


(sat-unmark-uninterpreted fn $sat state) => (erp $sat state):
Unmark function fn as uninterpreted.  Now fn will only be 
treated as uninterpreted if it is a defstub (an encapsulated
function with no constraints).


--- Utility Functions ---

(sat-update-external-value $sat) => (erp $sat state):
Update the "external-value" of $sat.  This value will not be modified
internally, and is given simply for the use of tools built on top
of the SULFA system.  I use it in the "sat" clause processor so that
the end user can see that status of my theorem prover (whether
it returned VALID, INVALID, or SPURIOUS).

(sat-external-value $sat) => (erp value $sat state):
Read the "external-value" entry of $sat (see sat-update-status).


--- Main Functionality ---

(sat-in-SULFA expr $sat state) => (erp in-SULFA sat-package-symbols $sat state):
The return value "in-SULFA" is non-nil if and only if "expr" is in the 
Subclass of Unrollable SAT Formulas in ACL2 (SULFA).  SULFA is 
a decidable subclass including the primitives if, equal, car, cdr,
cons, and consp.  We restict SULFA to include only symbols in the SAT package,
so that these symbols can be reserved for internal use.  If this is the
reason expr wasn't in SULFA, sat-package-symbols is high.  


(sat-add-expr negate expr $sat state) => (erp $sat state):
Add a new ACL2 expression "expr" to the SAT conjunction. 
If sat-solve later returns satisfiable then there exists an instance
to the free variable that satisfies this "expr" along with the
rest of the SAT problem.  If "negate" is non-nil then the negation
of "expr" must be satisfied rather than the expression itself.
For example, to determine whether (implies (and a b) (or c d)) is
valid one could use the sequence:

(sat-add-expr nil a $sat state)
(sat-add-expr nil b $sat state)
(sat-add-expr t c $sat state)
(sat-add-expr t d $sat state)
(sat-solve $sat state)

Now we're asking the question is there an instance such that
a and b, but not c or d?  If there is then this instance is
a counter-example to (implies (and a b) (or c d)).  Otherwise,
(implies (and a b) (or c d)) is valid.


(sat-solve $sat state) => (erp soln $sat state):
Solve the current SAT problem, returning as soln either the symbol
'acl2::sat or 'acl2::unsat corresponding to the SAT problem being 
satisfiable or unsatisfiable respectively.  


(sat-generate-satisfying-instance $sat state) => (erp $sat state)
Generate a satifying instance to the current satisfiable problem.


(sat-si-input-alist $sat state) => (erp si-alist $sat state):
Returns an alist "si-alist" mapping the variables in the SAT problem to
values in a satisfying instance.  Note that you do not need to 


(sat-un-fn-list $sat state) => (erp fn-list $sat state):
Return a list of all the uninterpreted function symbols fn-list that
have been encountered by the system.  This may be less than the
number of relevant uninterpreted functions, if new expressions
have been added since the last call to sat-solve.


(sat-si-un-fn-alist fn $sat state) => (erp un-fn-alist $sat state):
Return an alist mapping argument values to return values for the
uninterpreted function fn.


---Commands for "Exploring" the Satisfying Instance---

The following functionality allows users to explore multiple instances
of the current problem.  It can be particularly useful for discovering 
what part of the current problem needs to be refined.

Note: None of these functions should be called unless sat-solve has 
been applied first and its last return value was "sat".  

(sat-instance-exploration-begin $sat state) => (erp $sat state):
Begin exploring the current satisfying instance.  No new problems
can be considered until the exploration has been ended.


(sat-instance-exploration-end $sat state) => (erp $sat state):
End the exploration of the current satisfying instance.  You are
now free to start a new problem or add new expressions to the current 
problem.


(sat-ie-current-expr $sat state) => (erp expr $sat state):
Return an ACL2 expression representing the part of the problem we are 
currently exploring.  This expression will always either be a 
variable in the current satisfiability problem or the value of an
uninterpreted function, given concrete arguments.  For examplem,
given a problem "(equal a (f a x))" the current expression might
be "a", "x", (f '1 '2), etc..


(sat-ie-set val $sat state) => (erp soln $sat state):
Set the current ACL2 expression to the value "val".  The return value
soln is equal to 'acl2::SAT if this value leads to at least one
satisfying insance and 'acl2::UNSAT otherwise.  You can set the
current expression multiple times in order to explore which values lead
to satisfying instances.


(sat-ie-find-val $sat state) => (erp val $sat state):
Find a value for the current expression that can lead to at least one
satisfying instance.


(sat-ie-next $sat state) => (erp $sat state):
Move on to the next ACL2 expression that needs a value.  The current
value must be set before calling this function and afterward it is
permanently set to that value until exploration is ended.  For example,
say that you set "x" to 5 and the next expression is "y".  If "y" is
defined to be less than "x" then setting "y" to 6 will lead to an
"UNSAT" result.


(sat-ie-emptyp $sat state) => (erp empty $sat state):
Returns whether there is no current expression because all expressions
have been set.


(sat-ie-set! val $sat state) => (erp $sat state):
Set the current value without checking whether this value can be satisfied.


(sat-ie-check $sat state) => (erp soln $sat state):
Check whether the problem is still satisfiable (after using set!).


--- Commands for Refinement after Exploration ---

Instance exploration often leads to the discovery that certain abstracted
function applications need to be refined in order to prove a property 
unsatisfiable or find a more interesting satisfying instance.  However
the expression returned by sat-ie-current-expr is merely a concretization
of a function application---instead of (f x) it yields (f '1).  To
get at the refine the true function applications we provide the following
functions:


(sat-ie-current-entry $sat state) => (erp entry $sat state): 
Returns an internal representation of the current expression
being explored.  


(sat-ie-unique-id $sat state) => (erp id $sat state):
Returns a unique number from 1 to 'ACL2::*SAT-MAX-ENTRY-ID* representing 
the current entry.  This number will persist after instance exploration ends 
and the current SAT problem is refined.  In this way the user can remember 
which expressions have been refined in the past and what old instances have 
been explored.


(sat-ie-current-entry-type $sat state) => (erp entry-type $sat state):
Returns either 'acl2::variable or 'acl2::uninterpreted-function,
representing whether the current expression during instance exploration
is a variable or an uninterpreted function.

NOTE: An uninterpreted function application really represents a call
under some context---i.e. 
(implies <condition> (equal (<fn-name> . <args>) <expr>)), where
<fn-name> is the name of an uninterpreted function.  We do not currently provide
any method getting the original ACL2 expression.  Instead, we can only 
give the values of its components under the current counter-example.


(sat-un-fn-condition-val un-fn-entry $sat state) => (erp imp-true $sat state):
The Boolean "imp-true" is true iff the conditions on an uninterpreted
function entry "un-fn-entry" are met under the current counter-example.  


(sat-un-fn-fn un-fn-entry $sat state) => (erp fn $sat state):
Returns the function name "fn" of an uninterpreted function entry.


(sat-un-fn-val un-fn-entry $sat state) => (erp val $sat state):
Returns the return value of an uninterpreted function application in a given
uninterpreted function entry.  Note that this uninterpreted faction isn't 
actually required to be equal to this value unless all its conditions are met.


(sat-un-fn-arg-entry-list un-fn-entry $sat state) => (erp arg-entry-list $sat state):
Returns the arguments of an uninterpreted function in internal form.
The list "arg-entry-list" corresponds, in order, to the arguments of 
this uninterpreted function application as the internal form "arg-entry".


(sat-arg-entry-val arg-entry $sat state) => (erp val $sat state):
Returns the value of an argument, given in its internal "arg-entry" form.


(sat-add-expr-alist negate expr alist $sat state) => (erp $sat state):
This function is a more general version of sat-add-expr.  Every free
variable in the ACL2 expression "expr" must occur as a key in the 
alist "alist".  The value of the alist entry must be in internal form---
meaning it can be either a variable entry (given by sat-var-entry or 
sat-ie-current-entry), an uninterpreted function entry (given by 
sat-un-fn-entry-list or sat-ie-current-entry), or an argument entry 
(given by sat-si-un-fn-arg-entry-list).  The idea is that this function 
can be used to refine a formula in which the uninterpreted
functions are a means of abstraction.  

NOTE:  This expression implicitly acquires the conjunction of the
conditions in all of the uninterpreted function entries in the alist 
(but not the arg-entries).


(sat-un-fn-entry-list fn $sat state) => (erp un-fn-entry-list $sat state):
Return a list of all the uninterpreted function entries currently 
associated with the uninterpreted function fn.  


(sat-var-entry var $sat state) => (erp var-entry $sat state):
Return the internal representation, or "variable entry", associated with 
the ACL2 symbol "var".  One is created if it does not already exist.