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
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])
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 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
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",[]),
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