Java Doc for DecisionProcedureSmtAuflia.java in  » Testing » KeY » de » uka » ilkd » key » proof » decproc » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.proof.decproc 
Source Cross Reference  Class Diagram Java Document (Java Doc) 


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) )




Constructor Summary
public  DecisionProcedureSmtAuflia(Goal goal, DecisionProcedureTranslationFactory dptf, Services services)
    

Method Summary
public static  voidconfigureLogger(Level level)
     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.

abstract protected  DecisionProcedureResultexecDecProc()
     This method provides a hook for subclasses.
It must be implemented by subclasses which execute a concrete decision procedure.
public static  voidfireNewProblemLoaded(File problemFile, Proof proof)
     Informs this class that a new problem has been loaded in KeY.
public static  voidfireSelectedProofChanged(Proof proof)
     Informs this class the another Proof has been selected in the prover.
protected  BenchmarkgetResultBenchmark()
    
protected  FilegetTempFile()
    
public  DecisionProcedureResultrun(boolean lightweight)
    
final protected  DecisionProcedureResultrunInternal(ConstraintSet constraintSet, boolean lightWeight)
    


Constructor Detail
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




Method Detail
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



run
public DecisionProcedureResult run(boolean lightweight)(Code)



runInternal
final protected DecisionProcedureResult runInternal(ConstraintSet constraintSet, boolean lightWeight)(Code)



Fields inherited from de.uka.ilkd.key.proof.decproc.AbstractDecisionProcedure
final protected DecisionProcedureTranslationFactory dptf(Code)(Java Doc)
final protected Goal goal(Code)(Java Doc)
final protected Node node(Code)(Java Doc)
final protected Services services(Code)(Java Doc)
final protected Constraint userConstraint(Code)(Java Doc)

Methods inherited from de.uka.ilkd.key.proof.decproc.AbstractDecisionProcedure
protected static String getCurrentDateString()(Code)(Java Doc)
protected static String read(InputStream in) throws IOException(Code)(Java Doc)
public DecisionProcedureResult run(boolean lightWeight)(Code)(Java Doc)
public DecisionProcedureResult run()(Code)(Java Doc)
abstract protected DecisionProcedureResult runInternal(ConstraintSet constraintSet, boolean lightWeight)(Code)(Java Doc)

Methods inherited from java.lang.Object
protected Object clone() throws CloneNotSupportedException(Code)(Java Doc)
public boolean equals(Object o)(Code)(Java Doc)
protected void finalize() throws Throwable(Code)(Java Doc)
final native public Class getClass()(Code)(Java Doc)
public int hashCode()(Code)(Java Doc)
final public void notify() throws IllegalMonitorStateException(Code)(Java Doc)
final public void notifyAll() throws IllegalMonitorStateException(Code)(Java Doc)
public String toString()(Code)(Java Doc)
final public void wait() throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc)
final public void wait(long ms) throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc)
final public void wait(long ms, int ns) throws IllegalMonitorStateException, InterruptedException(Code)(Java Doc)

www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.