001 package escjava.prover;
002
003 import java.util.Properties;
004 import org.apache.xmlrpc.*;
005 import java.util.Vector;
006 import java.util.Enumeration;
007 import java.util.Iterator;
008 import java.lang.Thread;
009 import escjava.prover.jniw.Cvc3Wrapper;
010 import escjava.prover.jniw.Cvc3WrapperException;
011
012 public class Cvc3 extends NewProver {
013
014 /*
015 * README
016 * This class and the new other ones like NewProver, ProverResponse
017 * have been specified with jml. Even if we cannot use jmlc and jmlrac for
018 * the whole escjava2 program, these new classes have been tested
019 * apart from the rest of the program. Using jmlrac on a few test seems
020 * to show that these classes are respecting there specification.
021 * Anyway nothing has been done with escjava2.
022 */
023
024 //@ public invariant started ==> wrapper != null;
025
026 private /*@ spec_public non_null @*/ static Cvc3Wrapper wrapper = new Cvc3Wrapper();
027
028 static boolean debug = false;
029
030 // special constructor for debugging
031 public Cvc3(boolean debug){
032 Cvc3.debug = debug;
033 }
034
035 /** Starts a new instance of CVC3. This is necessary in order to redefine
036 * any functions or variables used.
037 *
038 * @return OK (or exit)
039 */
040 /*@
041 @ also
042 @ assignable wrapper;
043 @*/
044 public /*@non_null*/ProverResponse start_prover() {
045
046 //++
047 if(debug) System.out.println("Cvc3::start_prover");
048 //++
049
050 try { wrapper.startSolver(); }
051 catch (Exception e) {
052 System.err.println("Cvc3Wrapper::"+e);
053 System.exit(0);
054 }
055
056 ProverResponse res = ProverResponse.OK;
057
058 //++
059 if(debug)
060 if( res != ProverResponse.OK )
061 System.out.println("Failed to init cvc");
062 //++
063
064 started = true;
065
066 return res;
067
068 }
069
070 /**
071 * Sets command line flags for CVC3. Flag are currently just strings in
072 * the properties.
073 *
074 * @param properties is a table of the flags. Keys and entries are strings,
075 * and are concatenated together to form each flag (so there is no
076 * functional difference between ["a b",""] and ["a","b"]).
077 *
078 * @return OK or SYNTAX_ERROR, as appropriate.
079 *
080 */
081 public /*@non_null*/ProverResponse set_prover_resource_flags(/*@non_null*/Properties properties) {
082
083 //++
084 if(debug) System.out.println("Cvc3::set_prover_resource_flags");
085 //++
086
087 /* we have to create a big string containing
088 * all the flags ( = key in the hashtable of Properties)
089 * and their values ( = value)
090 */
091 Enumeration flags = properties.keys();
092
093 String value = ""; // command string
094 String currentFlag = null;
095
096 for ( ; flags.hasMoreElements() ;) {
097
098 try {
099 currentFlag = (String)flags.nextElement();
100 value += currentFlag+" "+properties.getProperty( currentFlag );
101 }
102
103 catch (Exception e) {
104 System.err.println("Cvc3::Failed to inspect properties");
105 System.exit(0);
106 }
107 }
108
109 ProverResponse res = ProverResponse.OK;
110
111 try {
112 wrapper.setFlags(value);
113 }
114 catch (Exception e) {
115 res = ProverResponse.SYNTAX_ERROR;
116 }
117
118 //++
119 if(debug)
120 if( res!= ProverResponse.OK )
121 System.out.println("Failed to set flags");
122 //++
123
124 return res;
125 }
126
127 /**
128 * Declares a signature to CVC3. The signature is assumed to be a string
129 * of a sequence of CVC-readable declaration commands (each
130 * terminated by a semicolon).
131 *
132 * @return ProverResponse.OK if no problems encountered, otherwise
133 * ProverResponse.FAIL.
134 */
135 public /*@non_null*/ProverResponse signature(/*@non_null*/Signature signature) {
136 //++
137 if(debug)
138 System.out.print("Cvc3::signature");
139 //++
140
141 /*
142 * This requires the signature be able to be transformed into a list
143 * (Vector) of strings for each declaration command (without the ;)
144 * res can only degrade from "OK".
145 */
146
147 // We first need to decompose the signature into commands
148
149 ProverResponse res = ProverResponse.OK;
150 String [] cmd = signature.toString().split(";");
151 int sz = cmd.length;
152
153 // now we cycle through each command (replacing the semicolon):
154 // this assumes a CVC presentation language format!
155
156 try {
157 for (int i = 0; i < sz; i++) {
158 if (cmd[i].indexOf("TYPE") > -1) {
159 // tyedefs
160 wrapper.declType(cmd[i]+";");
161 } else if (cmd[i].matches("BOOLEAN\\s*\\z")) {
162 // predicates must have BOOLEAN domain
163 wrapper.declPred(cmd[i]+";");
164 } else {
165 // everything else is a function
166 wrapper.declFun(cmd[i]+";");
167 }
168 }
169 } catch (Exception e) {
170 res = ProverResponse.FAIL;
171 }
172
173 //++
174 if(debug)
175 if( res!= ProverResponse.OK )
176 System.out.println("Failed to set signature definitions");
177
178 signature_defined = true;
179
180 return res;
181 }
182
183 /**
184 * Same as make_asumption.
185 */
186 public /*@non_null*/ProverResponse declare_axiom(/*@non_null*/Formula formula) {
187
188 /*
189 * This is currently treated tha same as make_assumption
190 */
191
192 return make_assumption(formula);
193 }
194
195 /**
196 * Asserts a formula to cvc3.
197 *
198 * @param The fomula to be asserted, as a string. (not a "command")
199 *
200 * @return OK, FAIL, or INCONSISTENCY_WARNING. INCONSISTENCY_WARNING will
201 * indicate the current (post-assertion) context has been detected as
202 * inconsistent.
203 */
204 public /*@non_null*/ProverResponse make_assumption(/*@non_null*/Formula formula) {
205
206 /*
207 * This is currently treated the same as declare_axiom.
208 * Assume the formula is just a formula, not a command.
209 * The assertion goes through even if the context becomes inconsistent
210 */
211
212 ProverResponse res = ProverResponse.OK;
213
214 String cmd = "ASSERT " + formula.toString() + ";";
215
216 try {
217 wrapper.assertFormula(cmd);
218 if (wrapper.contextInconsistent()) {
219 res = ProverResponse.INCONSISTENCY_WARNING;
220 res.info = new Properties();
221 res.formula = new Formula("");
222 }
223 } catch (Exception e) {
224 res = ProverResponse.FAIL;
225 }
226
227 return res;
228 }
229
230 /**
231 * Retracts some number of previous assumptions.
232 *
233 * @param count the number of undos. If count < = 0 then do nothing.
234 * If count > the number of assertions, all assertions will be undone.
235 *
236 * @return OK.
237 */
238 public /*@non_null*/ProverResponse retract_assumption(int count) {
239
240 wrapper.undoAssert(count);
241
242 return ProverResponse.OK;
243 }
244
245 /**
246 * Perform a query on a formula.
247 *
248 * @param formula the formula to be checked.
249 * @param properties not currently used
250 *
251 * @return YES (is valid), COUNTEREXAMPLE (possibly spurious), or TIMEOUT.
252 * Note is is possible to also distinguish truly invalid operations from
253 * invalid-but-possibly-incomplete ones, but there does not appear to be
254 * a ProverResponse for "don't know" responses that allows the (possible)
255 * counterexample.
256 */
257 public /*@non_null*/ProverResponse is_valid(/*@non_null*/Formula formula,
258 Properties properties) {
259
260 ProverResponse res = ProverResponse.OK;
261
262 /*
263 * assume the query is not in command form;
264 * Properties are currently ignored
265 * a "Don't know" response is returned as a timeout
266 */
267
268 try {
269 String cmd = "QUERY " + formula.toString() + ";";
270 String r = wrapper.queryFormula(cmd);
271 if (r.startsWith("Abort")) {
272 res = ProverResponse.TIMEOUT; //should this be something else?
273 } else if (r.startsWith("Valid")) {
274 res = ProverResponse.YES; // is VALID
275 } else { // is INVALID or DON'T KNOW
276 int colon = r.indexOf(":");
277 String counterex = r.substring(colon+1);
278 res = ProverResponse.COUNTER_EXAMPLE;
279 res.formula = new Formula(counterex);
280 }
281 } catch (Exception e) { // PROBLEM
282 res = ProverResponse.SYNTAX_ERROR;
283 res.info = new Properties();
284 res.info.setProperty("ERROR",e.toString());
285 }
286
287 return res;
288 }
289
290
291 /**
292 * Destroys the current instance of cvc3. It is necessary to call
293 * start_solver() to do further processing.
294 *
295 * Returns OK or FAIL.
296 */
297 //@ also
298 //@ assignable signature_defined, started;
299 public /*@non_null*/ProverResponse stop_prover() {
300
301 //++
302 if(debug) System.out.println("Cvc3::stop_prover");
303 //++
304
305 int result;
306
307 ProverResponse res = ProverResponse.OK;
308
309 try {
310 wrapper.stopSolver();
311 } catch (Exception e) {
312 res = ProverResponse.FAIL;
313 }
314
315 if(debug)
316 if( res != ProverResponse.OK )
317 System.out.println("Cvc3::Failed to stop");
318
319 started = false;
320 signature_defined = false;
321
322 return res;
323 }
324
325 /*
326 * Test
327 */
328 static void printResponse(ProverResponse r) {
329 String s;
330 System.out.println();
331 if (r.equals(ProverResponse.OK)) {s = "OK";}
332 else if (r.equals(ProverResponse.FAIL)) {s = "FAIL";}
333 else if (r.equals(ProverResponse.YES)) {s = "YES";}
334 else if (r.equals(ProverResponse.NO)) {s = "NO";}
335 else if (r.equals(ProverResponse.COUNTER_EXAMPLE)) {s = "COUNTER_EXAMPLE="+r.formula.toString();}
336 else if (r.equals(ProverResponse.SYNTAX_ERROR)) {s = "SYNTAX_ERROR";}
337 else if (r.equals(ProverResponse.PROGRESS_INFORMATION)) {s = "PROGRESS_INFORMATION";}
338 else if (r.equals(ProverResponse.TIMEOUT)) {s = "TIMEOUT";}
339 else if (r.equals(ProverResponse.INCONSISTENCY_WARNING)) {s = "INCONSISTENCY_WARNING";}
340 else {s = "UNKNOWN RESPONSE";}
341 System.out.println(s);
342 }
343
344
345 static public void main(String[] argv){
346
347 long startTime = java.lang.System.currentTimeMillis();
348 Cvc3 cvc = new Cvc3(true);
349
350 /* Test 1 */
351 cvc.start_prover();
352 Properties flags = new Properties();
353 Properties p = new Properties();
354 flags.setProperty(" ","-tcc");
355 ProverResponse r;
356 cvc.set_prover_resource_flags(flags);
357 cvc.signature(new Signature("f:(INT,INT)->INT;x,y,z:INT;a,b,c:BOOLEAN;"));
358 cvc.make_assumption(new Formula("a AND b AND NOT c"));
359 cvc.make_assumption(new Formula("x=y"));
360 cvc.make_assumption (new Formula("f(x,x)=y"));
361 cvc.make_assumption(new Formula("f(x,x)=z"));
362 r = cvc.is_valid(new Formula("x=z"),p);
363 printResponse(r);
364 cvc.retract_assumption(2);
365 r = cvc.is_valid(new Formula("f(x+1,x+1)=y"),p);
366 printResponse(r);
367 cvc.stop_prover();
368 flags = new Properties();
369 flags.setProperty(" ","-lang presentation -output-lang smtlib");
370 cvc.set_prover_resource_flags(flags);
371 cvc.start_prover();
372 cvc.signature(new Signature("f:(INT,INT)->INT;a,b,c:INT;x,y,z:BOOLEAN;"));
373 cvc.make_assumption(new Formula("NOT(x AND NOT y AND z)"));
374 cvc.make_assumption(new Formula("a/=b"));
375 cvc.make_assumption(new Formula("f(a+1,a+1)=b+1"));
376 cvc.make_assumption(new Formula("f(a,a)=c"));
377 r = cvc.is_valid(new Formula("NOT a=c"),p);
378 printResponse(r);
379 r = cvc.is_valid(new Formula("f(a,b)=b"),p);
380 printResponse(r);
381 r = cvc.is_valid(new Formula("EXISTS(c:INT):f(a,c)=b"),p);
382 printResponse(r);
383 cvc.start_prover();
384
385 long endTime = java.lang.System.currentTimeMillis();
386
387 long totalTime = endTime - startTime;
388
389 System.out.println("Time spend : "+totalTime+" milliseconds");
390
391 }
392
393 }