ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

Uses of Class
escjava.prover.ProverResponse

Packages that use ProverResponse
escjava.prover   
 

Uses of ProverResponse in escjava.prover
 

Subclasses of ProverResponse in escjava.prover
 class HarveyResponse
           
 class SammyResponse
           
 

Fields in escjava.prover declared as ProverResponse
static ProverResponse ProverResponse.OK
          A singleton response code to indicate everything is fine.
static ProverResponse ProverResponse.FAIL
          A singleton response code to indicate that something is seriously wrong with the corresponding call and/or the prover and a failure has taken place.
static ProverResponse ProverResponse.YES
          A singleton response code to indicate a positive response to the last command.
static ProverResponse ProverResponse.NO
          A singleton response code to indicate a negative response to the last command.
static ProverResponse ProverResponse.COUNTER_EXAMPLE
          A singleton response code to indicate a counter-example is available.
static ProverResponse ProverResponse.SYNTAX_ERROR
          A singleton response code to indicate a syntax error in the corresponding prover call.
static ProverResponse ProverResponse.PROGRESS_INFORMATION
          A singleton response code to indicate that some progress information is available from the prover.
static ProverResponse ProverResponse.TIMEOUT
          A singleton response code to indicate that the prover has timed out on the corresponding prover call.
static ProverResponse ProverResponse.INCONSISTENCY_WARNING
          A singleton response code to indicate an inconsistency warning from the prover for one or more of the previous ProverInterface#declare_axiom(Formula) and ProverInterface#make_assumption(Formula) calls.
 

Methods in escjava.prover that return ProverResponse
static ProverResponse SammyResponse.factory(int return_code)
           
 ProverResponse Sammy.start_prover()
           
 ProverResponse Sammy.set_prover_resource_flags(java.util.Properties properties)
           
 ProverResponse Sammy.signature(Signature signature)
           
 ProverResponse Sammy.declare_axiom(Formula formula)
           
 ProverResponse Sammy.make_assumption(Formula formula)
           
 ProverResponse Sammy.retract_assumption(int count)
           
 ProverResponse Sammy.is_valid(Formula formula, java.util.Properties properties)
           
 ProverResponse Sammy.stop_prover()
           
private  ProverResponse Sammy.execute(java.lang.String cmd)
          call to sammy using xml rpc commands available : start_solver set_flags type_declaration func_declaration add_assertion query backtrack stop_solver See sammy's cvcl/smt/README.TXT for further informations
static ProverResponse ProverResponse.factory(int return_code)
           
abstract  ProverResponse NewProver.start_prover()
          Start up the prover.
abstract  ProverResponse NewProver.set_prover_resource_flags(java.util.Properties properties)
          Send arbitrary information to the prover.
abstract  ProverResponse NewProver.signature(Signature signature)
          Send the signature of a new theory to the prover.
abstract  ProverResponse NewProver.declare_axiom(Formula formula)
          Declare a new axiom in the current theory.
abstract  ProverResponse NewProver.make_assumption(Formula formula)
          Make an assumption.
abstract  ProverResponse NewProver.retract_assumption(int count)
          Retract some assumptions.
abstract  ProverResponse NewProver.is_valid(Formula formula, java.util.Properties properties)
          Check the validity of the given formula given the current theory, its axioms, and the current set of assumptions.
abstract  ProverResponse NewProver.stop_prover()
          Stop the prover.
static ProverResponse HarveyResponse.factory(int return_code)
           
 ProverResponse Harvey.start_prover()
           
 ProverResponse Harvey.set_prover_resource_flags(java.util.Properties properties)
           
 ProverResponse Harvey.signature(Signature signature)
           
 ProverResponse Harvey.declare_axiom(Formula formula)
           
 ProverResponse Harvey.make_assumption(Formula formula)
           
 ProverResponse Harvey.retract_assumption(int count)
           
 ProverResponse Harvey.is_valid(Formula formula, java.util.Properties properties)
           
 ProverResponse Harvey.stop_prover()
           
 


ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

The ESC/Java2 Project Homepage