001 package escjava.prover; 002 003 import java.util.Properties; 004 005 public class ProverResponse 006 { 007 /** 008 * A singleton response code to indicate everything is fine. 009 */ 010 public /*@ non_null @*/ static ProverResponse OK = 011 new ProverResponse(); 012 013 /** 014 * A singleton response code to indicate that something is seriously 015 * wrong with the corresponding call and/or the prover and a failure 016 * has taken place. A response code of FAIL typically indicates a 017 * non-correctable situation. The {@link #info} field should be 018 * consulted for additional information, and no further calls, but 019 * for {@link ProverInterface#stop_prover()} should be made. 020 */ 021 public /*@ non_null @*/ static ProverResponse FAIL = 022 new ProverResponse(); 023 024 /** 025 * A singleton response code to indicate a positive response to the 026 * last command. 027 */ 028 public /*@ non_null @*/ static ProverResponse YES = 029 new ProverResponse(); 030 031 /** 032 * A singleton response code to indicate a negative response to the 033 * last command. 034 */ 035 public /*@ non_null @*/ static ProverResponse NO = 036 new ProverResponse(); 037 038 /** 039 * A singleton response code to indicate a counter-example is 040 * available. The counter-example is contained in the {@link 041 * #formula} field of this response object. 042 */ 043 public /*@ non_null @*/ static ProverResponse COUNTER_EXAMPLE = 044 new ProverResponse(); 045 046 /** 047 * A singleton response code to indicate a syntax error in the 048 * corresponding prover call. The {@link #info} field should be 049 * consulted for additional information. 050 */ 051 public /*@ non_null @*/ static ProverResponse SYNTAX_ERROR = 052 new ProverResponse(); 053 054 /** 055 * A singleton response code to indicate that some progress 056 * information is available from the prover. The {@link #info} 057 * field should be consulted for additional information. 058 */ 059 public /*@ non_null @*/ static ProverResponse PROGRESS_INFORMATION = 060 new ProverResponse(); 061 062 /** 063 * A singleton response code to indicate that the prover has timed 064 * out on the corresponding prover call. The {@link #info} and/or 065 * {@link #formula} fields should be consulted for additional 066 * information. 067 */ 068 public /*@ non_null @*/ static ProverResponse TIMEOUT = 069 new ProverResponse(); 070 071 /** 072 * A singleton response code to indicate an inconsistency warning 073 * from the prover for one or more of the previous {@link 074 * ProverInterface#declare_axiom(Formula)} and {@link 075 * ProverInterface#make_assumption(Formula)} calls. The {@link 076 * #info} and/or {@link #formula} fields should be consulted for 077 * additional information. 078 */ 079 public /*@ non_null @*/ static ProverResponse INCONSISTENCY_WARNING = 080 new ProverResponse(); 081 082 /** 083 * A formula. Typically, this field is used to represent a 084 * counter-example in response to a call to {@link 085 * ProverInterface#is_valid(Formula)}. 086 */ 087 public Formula formula; 088 089 /** 090 * A set of properties. Typically, this field is used to represent 091 * property/value pairs specific to reporting prover progress, 092 * state, resource utilization, etc. 093 */ 094 public Properties info; 095 096 /** 097 * A private constructor that is only to be used during static 098 * initialization. 099 */ 100 protected ProverResponse() { 101 ; // skip 102 } 103 104 // placeholder for factory for building ProverResponses 105 /*@ ensures \result == ProverResponse.OK || 106 @ \result == ProverResponse.FAIL || 107 @ \result == ProverResponse.YES || 108 @ \result == ProverResponse.NO || 109 @ \result == ProverResponse.COUNTER_EXAMPLE || 110 @ \result == ProverResponse.SYNTAX_ERROR || 111 @ \result == ProverResponse.PROGRESS_INFORMATION || 112 @ \result == ProverResponse.TIMEOUT || 113 @ \result == ProverResponse.INCONSISTENCY_WARNING; 114 @*/ 115 static public /*@ pure non_null @*/ ProverResponse factory(int return_code) { 116 117 /* 118 * Naive implementation, should be redefined in subclasses 119 */ 120 121 if( return_code >= 0 ) 122 return ProverResponse.OK; 123 else 124 return ProverResponse.FAIL; 125 126 } 127 }