| java.lang.Object
 de.uka.ilkd.key.proof.decproc.AbstractDecisionProcedure
de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAuflia
All known Subclasses: de.uka.ilkd.key.proof.decproc.DecisionProcedureDummyTranslation, de.uka.ilkd.key.proof.decproc.DecisionProcedureSVC, de.uka.ilkd.key.proof.decproc.DecisionProcedureYices, de.uka.ilkd.key.proof.decproc.DecisionProcedureCVCLite, de.uka.ilkd.key.proof.decproc.DecisionProcedureCVC3,
| DecisionProcedureSmtAuflia | | abstract public class DecisionProcedureSmtAuflia extends AbstractDecisionProcedure (Code) | | Represents a basic class for the invocation of decisison procedures accepting the SMT-LIB
format as input language on the translation of a KeY Goal.
An instance of this class takes a Goal, translates it in into a Benchmark
for the SMT logic (QF_)AUFLIA and stores this translation result in a temporary file.
This class is intended to be subclassed by classes which invoke a concrete decision procedure
supporting the SMT-LIB logic (QF_)AUFLIA. These subclasses must implement the provided hook method
execDecProc()
author:
akuwertz
version:
1.3, 10/02/2006 (Extended to support quantifiers (AUFLIA) ) |
| DecisionProcedureSmtAuflia | | public DecisionProcedureSmtAuflia(Goal goal, DecisionProcedureTranslationFactory dptf, Services services)(Code) | | Mere constructor, just creates a new DecisionProcedureSmtAuflia instance
Parameters:
goal - the Goal which should be translated
Parameters:
dptf - the DecisionProcedureTranslationFactory used for translation
Parameters:
services - the Services used during translation |
| configureLogger | | public static void configureLogger(Level level)(Code) | | Configures the Logger hierarchy used to log the process of translating
a Goal into SMT AUFLIA syntax.
If the specified Level is less or equal to INFO, a log file will be
created in a log directory for SMT under the ".key" directory. All logged information
will be stored in this file, and not go to any inherited Appenders.
Otherwise, no extra file will be created and all logged information output will go to
any inherited Appender.
If this method is not called before calling any of the other methods of this class, the
configuration of the Logger will be inherited from the rootlogger
Parameters:
level - the Level the Logger should be configured with
throws:
RuntimeException - if the specified Level is less or equal to INFOand the log file could not be created |
| execDecProc | | abstract protected DecisionProcedureResult execDecProc()(Code) | | This method provides a hook for subclasses.
It must be implemented by subclasses which execute a concrete decision procedure.
a DecisionProcedureResult representing the result of the execution ofthe decision procedure on the created and temporal stored Benchmark |
| fireNewProblemLoaded | | public static void fireNewProblemLoaded(File problemFile, Proof proof)(Code) | | Informs this class that a new problem has been loaded in KeY.
This method should be called every time when a new problem has been loaded to the KeY prover.
It delayedly sets up a new directory to store all benchmarks resulting from the loaded problem
Parameters:
problemFile - the problem File the has been loaded
Parameters:
proof - the Proof that has been created for the given problem |
| fireSelectedProofChanged | | public static void fireSelectedProofChanged(Proof proof)(Code) | | Informs this class the another Proof has been selected in the prover.
This method should be called every time when the selected Proof has changed.
It changes the directory in which the created SMT-Lib benchmarks will be archived so that
all benchmarks resulting from one loaded problem will be stored in the same directory
Parameters:
proof - the Proof that is currently selected in the prover |
| getResultBenchmark | | protected Benchmark getResultBenchmark()(Code) | | Returns the Benchmark that represents the translation result
the Benchmark representing the translation result |
| getTempFile | | protected File getTempFile()(Code) | | Returns the temporary File the translation result is stored in
the temporary File the translation result is stored in |
|
|