public class EProver extends FolTheoremProver
Modifier and Type | Field and Description |
---|---|
private java.lang.String |
additionalArguments
Additional arguments for the call to the eprover binary
(Default value is "--auto-schedule" which seems to be working
best in general)
|
private Shell |
bash
Shell to run eprover
|
private java.lang.String |
binaryLocation
String representation of the E binary path,
directory, where the temporary files are stored
|
defaultProver
Constructor and Description |
---|
EProver(java.lang.String binaryLocation)
Constructs a new instance pointing to a specific eprover
|
EProver(java.lang.String binaryLocation,
Shell bash)
Constructs a new instance pointing to a specific eprover
|
Modifier and Type | Method and Description |
---|---|
boolean |
equivalent(FolBeliefSet kb,
FolFormula a,
FolFormula b) |
java.lang.String |
getAdditionalArguments()
Returns the additional arguments given to the call of the
eprover binary (Default value is "--auto-schedule")
|
java.lang.String |
getBinaryLocation()
returns the path of the provers binary
|
boolean |
query(FolBeliefSet kb,
FolFormula query)
This method determines the answer of the given query
wrt.
|
void |
setAdditionalArguments(java.lang.String s)
Sets the additional arguments given to the call of the
eprover binary (Default value is "--auto-schedule")
|
void |
setBinaryLocation(java.lang.String binaryLocation)
Change path of the binary
|
getDefaultProver, setDefaultProver
private java.lang.String binaryLocation
private java.lang.String additionalArguments
private Shell bash
public EProver(java.lang.String binaryLocation, Shell bash)
binaryLocation
- of the eprover executable on the hard drivebash
- shell to run commandspublic EProver(java.lang.String binaryLocation)
binaryLocation
- of the eprover executable on the hard drivepublic void setAdditionalArguments(java.lang.String s)
s
- some stringpublic java.lang.String getAdditionalArguments()
public boolean query(FolBeliefSet kb, FolFormula query)
FolTheoremProver
query
in class FolTheoremProver
kb
- the knowledge basequery
- a query.public boolean equivalent(FolBeliefSet kb, FolFormula a, FolFormula b)
equivalent
in class FolTheoremProver
public java.lang.String getBinaryLocation()
public void setBinaryLocation(java.lang.String binaryLocation)
binaryLocation
- the new path of the E binary