Installing the System

Take the following steps

• cd <saturate_ install_ dir>/saturate/sources
• Replace in the file sat.pl the lines

          assert(saturate_directory( '/HG/local/provers/saturate' ) .
          davis_putnam( yes ).
  

  by

          saturate_directory( '<saturate_install_dir>/saturate' ) .
          davis_putnam( <yes/no> ).
  

  You may also want to adjust the configuration of the web browser to be used for displaying the help files. With netscape (Unix) or explorer (Windows) it should just work fine as is. Even if those settings are not correct that's not a problem, the Saturate system will function in any case.

  The flag for davis_ putnam indicates as to whether the optional incremental Davis-Putnam-like satisfiability checker should be included in the system. The flag has no effect for Quintus- and SICStus 2.1-Prolog. The module only works under SICStus 3.x.

  For SICStus 3.x users it is possible that on your computer system ``yes'' will produce errors due to incompatibilities on the C-compiler and C-libraries level. In that case change the default to ``no'' and run the generation again. Saturate will function without that module, too, but will perform much worse in medium to large examples of near-propositional nature and in certain knowledge representation applications. If you want that module, you may obtain it via ftp. You will then have to re-compile them on your system, using the same C-compiler that was used for installing SICStus 3.0. Then move the resulting modules into directory <saturate_ install_ dir>/saturate/sources/CLPPB and say davis_ putnam( yes ). before generating Saturate again.

• For SICStus Prolog users only: You need to have patch level #3 or higher for SICStus 3.0 and patch level #8 or higher for SICStus 2.1 (patch level #9 recommended). For later versions of SICStus 3.x any patch level should be fine.
  • On SPARC architectures include

            :- prolog_flag(compiling,_,fastcode).
    

    into your .sicstusrc file (or execute that query on top level) before installing the system if you want native code generation (the preferred mode).

  • Include

            setenv SP_COMPRESS_SAVE 1
    

    into your .cshrc file to save space when saving Saturate.
• cd to the sources subdirectory.

• Call Quintus Prolog or SICStus Prolog.

• Execute

          | ?- compile(sat), genSystem.
  

  (don't forget the dot at the end). Then, on demand, enter the name of a file to save the Saturate system on. Use that name on shell level to call Saturate lateron, or when restoring that state.

• Exit the Prolog system or start using Saturate right away.
• Don't remove the source files after system generation. Some of them will be needed and linked dynamically at runtime.
• If you would like to check as to whether the system operates correctly, execute

          | ?- cd('<saturate_install_dir>/saturate/examples'), 
               hgstuff:testsuite.
  

  As of November 2001 this runs for about 180 sec under SICStus 3.x on a 600Mhz Pentium IIII. The resulting behaviour should look like the one that is documented in the log-file <saturate_ install_ dir>/saturate/testsuite.log*.

Imprint | Data Protection