2:- ensure_loaded(ccalc).    3
    4solver_test :-
    5   initialize,
    6   format("Testing all SAT solvers and utility programs.~n~n",[]),
    7   value(ccalc_dir,CCDir),
    8   determine_os(OS),
    9
   10% There's a problem with checking the usage of pipes so the section below
   11% has been commented out.  (Pipes are not used by default, anyway.)
   12%
   13% Actually, it seems that this will work correctly in swipl, if we replace
   14%    make_pipe(P1),make_pipe(P2),format_to_atom(...),system(...),
   15% by
   16%    pipe(P2,P1)
   17% and remove
   18%    common_file_delete(P1),common_file_delete(P2)
   19% later on.
   20%
   21% However, I didn't do this because 
   22% a) we should also fix all places in ccalc.pl where pipes are used,
   23% b) sicstus (version 3.11.2, in the department) doesn't have pipe/2.
   24%
   25% -- Selim T. Erdogan, 23 May 2012
   26/*
   27   format("Testing whether CCalc can create and use pipes...",[]),
   28   flush_output,
   29   ( make_pipe(P1),
   30     make_pipe(P2),
   31     format_to_atom(Call1,"cat ~w > ~w &",[P1,P2]),
   32     system(Call1),
   33     see(P2),
   34     tell(P1),
   35     write('This is a test'), nl,
   36     told,
   37     read_line("This is a test"),
   38     seen,
   39     common_file_delete(P1),
   40     common_file_delete(P2),
   41     set(file_io,false),
   42     format(" successful.~n~n",[])
   43   ; format("Error using pipes for I/O.  The system utilities called by CCalc might not be~n",[]),
   44     format("portable.  Please contact ccalc-help@cs.utexas.edu for assistance.  In the~n",[]),
   45     format("meantime, please use the command 'set(file_io,true)' to use files instead of~n",[]),
   46     format("pipes for I/O.  You may add this line to the options.std file to make this the~n",[]),
   47     format("default.",[]) ),
   48   flush_output,
   49   !,
   50*/
   51
   52   format("Checking for existence of solvers directory...",[]),
   53   flush_output,
   54   format_to_atom(D,"~wsolvers/~s",[CCDir,OS]),
   55   ( common_file_exists(D)
   56     ->  format(" successful.~n~n",[]),
   57         format("SAT solvers executables for this operating system are stored in:~n",[]),
   58         format("~w~n~n",[D])
   59/*
   60   ; format("Directory does not exist.~nCreating ~w.~n~n ",[D]),
   61     flush_output,
   62     format_to_atom(Call2,"mkdir ~w",[D]),
   63     system(Call2)
   64*/
   65   ; format("Error: cannot create solvers directory.~n~n",[]),
   66     write('All of the SAT solvers and utility programs for CCalc must reside in'),nl,
   67     write('the directory <CCalc base dir>/solvers/<OS>, where <CCalc base dir> is the'),nl,
   68     write('directory in which ccalc.pl is located and <OS> is the name of the operating'),nl,
   69     write('system being used, as returned by the Unix system function \'uname\'.  (There'),nl,
   70     write('may be multiple subdirectories of the solvers directory if your CCalc'),nl,
   71     write('installation is shared by multiple operating systems.)  This directory does'),nl,
   72     write('not currently exist, and an attempt to create it has failed.  Please ask'),nl,
   73     write('your system administrator to create this directory and ensure that the'),nl,
   74     write('SAT solver executables are located therein.'),nl,nl,
   75     fail ),
   76   flush_output,
   77   !,
   78
   79   /* Test all the SAT solvers */
   80
   81   iset(compact,false),
   82   iset(num,1),
   83   iset(mode,basic),
   84   iset(atom_count,2),
   85   iset(clause_count,2),
   86   iset(query_clause_count,0),
   87   iset(timed,false),
   88   iset(verbose,false),
   89   iset(file_io,true),
   90   iset(noabort,true),
   91   assertz(clause([1,2])),
   92   assertz(clause([-2])),
   93
   94% SAT solver "sato_old" only exists as a binary for SunOS.  So no need
   95% to test it when we're running on Linux.
   96% -- Selim T. Erdogan, 22 May 2012
   97%
   98%   ( member(S,[mchaff,relsat,relsat_old,grasp,sato,sato_old,satz,satz-rand,
   99%	       walksat,zchaff]),
  100   ( ( OS == "Linux" 
  101       -> member(S,[mchaff,relsat,relsat_old,grasp,sato,satz,satz-rand,
  102	          walksat,zchaff])
  103     ; member(S,[mchaff,relsat,relsat_old,grasp,sato,sato_old,satz,satz-rand,
  104                 walksat,zchaff])), 
  105
  106     format("~nTesting solver ~w...",[S]),
  107     flush_output,
  108     system_value('sh rm ccsat.* mchaff-opts.smj 2> /dev/null'),
  109     format_to_atom(FullName,"~wsolvers/~s/~w",[CCDir,OS,S]),
  110     ( \+ common_file_exists(FullName)
  111       -> format("~nExecutable ~w is missing.~n",[FullName]),
  112          display_note(S), nl, fail
  113     ; ( iset(solver,S),
  114         call_sat(no_notify,Out1,Out2,VT,_),
  115         extract_info(Out1,Out2,VT,A,M,_,_),
  116         A == "SAT",
  117         M == [[1]] )
  118       -> format(" successful.~n",[]),
  119          fail
  120     ; format("~n",[]), display_note(S), nl, fail )
  121   ; format("~nIf you have any problems running CCalc, please contact the development~n",[]),
  122     format("team at ccalc-help@cs.utexas.edu.  Thanks for using CCalc!~n~n",[]),
  123     iset(noabort,false) ).
  124
  125
  126display_note(grasp) :- 
  127   format("There was an error invoking GRASP.  You may need to obtain the correct~n",[]),
  128   format("executable or recompile this solver for your system.  Source code and~n",[]),
  129   format("executables for the Feb/2000 version of GRASP are available at:~n",[]),
  130   format("http://sat.inesc.pt/grasp/~n",[]),
  131   format("Please rename the executable from 'sat-grasp' to 'grasp' and copy it to the SAT~n",[]),
  132   format("solver directory listed above.~n",[]).
  133
  134display_note(mchaff) :-
  135   format("There was an error invoking mChaff.  You may need to obtain the correct~n",[]),
  136   format("executable or recompile this solver for your system.  Source code and~n",[]),
  137   format("executables for the spelt3 distribution of mChaff used to be available from~n",[]),
  138   format("http://www.princeton.edu/~~chaff/ but they are not supported anymore.~n",[]),
  139   format("Contact us by e-mailing ccalc-help@cs.utexas.edu for a copy of the code.~n",[]),
  140   format("After you get mchaff's code, please rename the executable from 'Chaff2'~n",[]),
  141   format("to 'mchaff' and copy it to the SAT solver directory listed above.~n",[]).
  142
  143display_note(relsat) :-
  144   format("There was an error invoking relsat version 2.02.  You may need to obtain the~n",[]),
  145   format("correct executable and recompile this solver for your system.  Source code for~n",[]),
  146   format("relsat version 2.02 is available at http://www.bayardo.org/resources.html~n",[]),
  147   format("Please copy the executable 'relsat' to the SAT solver directory listed above.~n",[]).
  148
  149display_note(relsat_old) :-
  150   format("There was an error invoking relsat version 1.1.2 (called 'relsat_old' within~n",[]),
  151   format("CCalc).  You may need to recompile this solver for your system.~n",[]),
  152%   format("Source code for relsat version 1.1.2 is be available at:~n",[]),
  153%   format("http://www.almaden.ibm.com/cs/people/bayardo/resources.html~n",[]),
  154   format("Contact us by e-mailing ccalc-help@cs.utexas.edu for a copy of the code.~n",[]),
  155   format("After you get relsat_old's code, please rename the executable from 'relsat'~n",[]),
  156   format("to 'relsat_old' and copy it to the SAT solver directory listed above.~n",[]).
  157
  158display_note(sato) :-
  159   format("There was an error invoking SATO version 3.2.1.  You may need to recompile this~n",[]),
  160   format("solver for your system.  Source code for SATO version 3.2.1 is available at:~n",[]),
  161   format("http://www.cs.uiowa.edu/~~hzhang/sato.html~n",[]),
  162   format("Please copy the executable 'sato' to the SAT solver directory listed above.~n",[]).
  163
  164display_note(sato_old) :-
  165   format("There was an error invoking SATO version 3.1.2 (called 'sato_old' within~n",[]),
  166   format("CCalc).  Source code for this version is no longer available, though some~n",[]),
  167   format("executables (for SunOS) are included with CCalc for backwards compatibility~n",[]),
  168   format("with previous versions of CCalc.  Please use another solver (such as the more~n",[]),
  169   format("recent SATO version 3.2.1).~n",[]).
  170
  171display_note(satz) :-
  172   format("There was an error invoking Satz.  You may need to recompile this solver for~n",[]),
  173   format("your system.  Source code for Satz215.2 is available at:~n",[]),
  174   format("http://www.laria.u-picardie.fr/~~cli/EnglishPage.html~n",[]),
  175   format("Please name the executable 'satz' and copy it to the SAT solver directory~n",[]),
  176   format("listed above.~n",[]).
  177
  178display_note(satz-rand) :-
  179   format("There was an error invoking Satz-rand.  You may need to recompile this solver~n",[]),
  180   format("for your system.  Source code for Satz-rand version 4.9 is available at:~n",[]),
  181   format("http://www.cs.washington.edu/homes/kautz/satz-rand/~n",[]),
  182   format("Please copy the executable 'satz-rand' to the SAT solver directory listed~n",[]),
  183   format("above.~n",[]).
  184
  185display_note(walksat) :-
  186   format("There was an error invoking Walksat.  You may need to obtain the correct~n",[]),
  187   format("executables or recompile this solver for your system.  Executables and source~n",[]),
  188   format("code for Walksat version 41 are available at:~n",[]),
  189   format("http://www.cs.washington.edu/homes/kautz/walksat/~n",[]),
  190   format("Please copy the executable 'walksat' to the SAT solver directory listed above.~n",[]).
  191
  192display_note(zchaff) :-
  193   format("There was an error invoking zChaff.  You may need to obtain the correct~n",[]),
  194   format("executable or recompile this solver for your system.  Executables and source~n",[]),
  195   format("code for zChaff are available at:~n",[]),
  196   format("http://www.ee.princeton.edu/~~chaff/zchaff.php~n",[]),
  197   format("Please rename the executable to 'zchaff' and copy it to the SAT solver~n",[]),
  198   format("directory listed above.~n",[]).
  199
  200% For some odd reason, when we load/consult solver_test.pl, calling
  201% solver_test at the very end leads to failure (i.e. "false").  
  202% So, to avoid confusion, I'm commenting it out.
  203%
  204% -- Selim T. Erdogan, 28 May 2012
  205%:- solver_test.