University of California at Berkeley
           Department of Electrical Engineering & Computer Sciences
                          Instructional Support Group

/share/b/pub/stp.help

								  Apr 10 2009

CONTENTS

	STP
	Documentation

STP
---
  STP (http://people.csail.mit.edu/vganesh/STP_files/stp.html) is the 
  Simple Theorem Prover, a constraint solver/decision procedure.  It was 
  developed primarily at Stanford.

  It is installed for Linux in 
  
	/home/ff/cs170/stp/bin/stp
	/home/ff/cs170/stp/lib/libstp.a

  For example:

	/share/b/bin/stp -s ~cs170/stp/sample-tests/long-by-hand.cvc

  For names and locations of the computers, please see 
  http://inst.eecs.berkeley.edu/connecting.html#labs

  The STP WEB page says: "WARNING: PLEASE DO `ulimit -s unlimited` BEFORE 
  RUNNING STP. OTHERWISE, THE YACC PARSER WILL SEGFAULT ON BIG EXAMPLES"

  More information is under /home/ff/cs170/stp.


Documentation
-------------

  Documentation is on-line at

   http://people.csail.mit.edu/vganesh/STP_files/stp-docs.html
   firefox file:///home/ff/cs170/stp/web



						Instructional Support Group
						378 & 386 Cory, 333 Soda
						inst@eecs.berkeley.edu