Modifier and Type | Field and Description |
---|---|
private Variable |
VarsNeqRequirement.first |
private Variable |
VarsNeqRequirement.second |
private Variable |
VarConstNeqRequirement.variable |
Modifier and Type | Method and Description |
---|---|
static java.util.Set<java.util.Map<Variable,Constant>> |
GroundingTools.getAllSubstitutions(java.util.Set<Variable> variables)
Calculates all possible substitutions in the given set of variables using
all possible constants of the same sort.
|
static java.util.Set<java.util.Map<Variable,Constant>> |
GroundingTools.getAllSubstitutions(java.util.Set<Variable> variables,
java.util.Set<Constant> constants)
Calculates all possible substitutions of variables for a given set of
constants
|
Modifier and Type | Method and Description |
---|---|
static java.util.Set<java.util.Map<Variable,Constant>> |
GroundingTools.getAllSubstitutions(java.util.Set<Variable> variables)
Calculates all possible substitutions in the given set of variables using
all possible constants of the same sort.
|
static java.util.Set<java.util.Map<Variable,Constant>> |
GroundingTools.getAllSubstitutions(java.util.Set<Variable> variables,
java.util.Set<Constant> constants)
Calculates all possible substitutions of variables for a given set of
constants
|
boolean |
GroundingRequirement.isValid(java.util.Map<Variable,Constant> assignment)
This method checks, if an assignment of constants to variables satisfies a
given grounding condition.
|
boolean |
VarConstNeqRequirement.isValid(java.util.Map<Variable,Constant> assignment) |
boolean |
VarsNeqRequirement.isValid(java.util.Map<Variable,Constant> assignment) |
static boolean |
GroundingTools.isValidGroundingApplication(java.util.Map<Variable,Constant> map,
java.util.Set<GroundingRequirement> requirements)
Checks a grounding application for compliance with the grounding
requirements.
|
Constructor and Description |
---|
VarConstNeqRequirement(Variable variable,
Constant constant)
Creates a new grounding requirement expressing, that the variable given may
not be set to the specific constant.
|
VarsNeqRequirement(Variable first,
Variable second)
Creates a new grounding requirement for the two given variables that are
not allowed to be set to the same constant in one ground instance.
|
Modifier and Type | Method and Description |
---|---|
GroundingRequirement |
GroundingRequirementsParser.parseRequirement(java.lang.String s,
java.util.Set<Variable> variables)
Parses a string of the following form:
(VARIABLENAME "<>" VARIABLENAME | VARIABLENAME "<>" CONSTANTNAME)
where the constant CONSTANTNAME has to be of the same sort as the
variable VARIABLENAME.
|
java.util.Set<GroundingRequirement> |
GroundingRequirementsParser.parseRequirements(java.lang.String s,
java.util.Set<Variable> variables)
Parses a string of the following form: REQUIREMENT ("," REQUIREMENT)*
|
Modifier and Type | Method and Description |
---|---|
java.util.Set<Variable> |
SActionQuery.getInnerVariables()
Returns all inner variables, which occur in state formulas and actions
in this action query.
|
abstract java.util.Set<Variable> |
QueryProposition.getVariables()
Returns all variables occuring in inner formulas and actions of this query
proposition.
|
java.util.Set<Variable> |
AlwaysQuery.getVariables() |
java.util.Set<Variable> |
NecessarilyQuery.getVariables() |
java.util.Set<Variable> |
HoldsQuery.getVariables() |
Modifier and Type | Method and Description |
---|---|
protected SActionQuery |
SActionQuery.substituteInnerFormulas(java.util.Map<Variable,Constant> map)
Returns a new action query in which all variables are mapped to constants
with regard to the given map.
|
private static PropositionalFormula |
SActionQuery.substitutePropositions(java.util.Map<Variable,Constant> map,
PropositionalFormula formula)
Utility function that walks through all parts of a propositional formula
with query propositions substituting all variables with constants according
to the given map.
|
Modifier and Type | Method and Description |
---|---|
java.util.Set<Variable> |
DelpRule.getQuantifierVariables() |
java.util.Set<Variable> |
DelpRule.getUnboundVariables() |
Modifier and Type | Method and Description |
---|---|
boolean |
DelpRule.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
DelpRule.isWellBound(java.util.Set<Variable> boundVariables) |
Modifier and Type | Field and Description |
---|---|
private java.util.Set<Variable> |
QuantifiedFormulaSupport.quantifier_variables
The variables of this quantified folFormula.
|
private java.util.Set<Variable> |
Sort.variables
The set of variables of this sort
|
Modifier and Type | Method and Description |
---|---|
Variable |
Variable.clone() |
Modifier and Type | Method and Description |
---|---|
java.util.Set<java.util.Map<Variable,Term<?>>> |
RelationalFormula.allSubstitutions(java.util.Collection<? extends Term<?>> terms)
Computes all possible substitutions, i.e.
|
java.util.Set<Variable> |
QuantifiedFormulaSupport.getQuantifierVariables()
Returns the variables of this quantified formula.
|
java.util.Set<Variable> |
QuantifiedFormulaSupport.getUnboundVariables() |
Modifier and Type | Method and Description |
---|---|
boolean |
QuantifiedFormulaSupport.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
QuantifiedFormulaSupport.isWellBound(java.util.Set<Variable> boundVariables) |
void |
QuantifiedFormulaSupport.setQuantifierVariables(java.util.Set<Variable> variables) |
Constructor and Description |
---|
Variable(Variable other)
Copy-Ctor: Creates a deep copy of the given Variable
|
Constructor and Description |
---|
QuantifiedFormulaSupport(T formula,
java.util.Set<Variable> variables) |
Modifier and Type | Method and Description |
---|---|
java.util.Set<Variable> |
QuantifiedFormula.getQuantifierVariables() |
java.util.Set<Variable> |
QuantifiedFormula.getUnboundVariables() |
Modifier and Type | Method and Description |
---|---|
boolean |
QuantifiedFormula.isClosed(java.util.Set<Variable> boundVariables)
Checks whether this formula is closed, i.e.
|
boolean |
QuantifiedFormula.isWellBound(java.util.Set<Variable> boundVariables)
Checks whether this formula is well-bound, i.e.
|
Modifier and Type | Field and Description |
---|---|
private java.util.Map<java.lang.String,Variable> |
TPTPParser.variables
Keeps track of variables defined.
|
private java.util.Map<java.lang.String,Variable> |
FolParser.variables
Keeps track of variables defined.
|
Modifier and Type | Method and Description |
---|---|
java.util.Map<java.lang.String,Variable> |
FolParser.getVariables() |
Modifier and Type | Method and Description |
---|---|
void |
FolParser.setVariables(java.util.Map<java.lang.String,Variable> variables) |
Modifier and Type | Method and Description |
---|---|
java.util.Set<Variable> |
AssociativeFOLFormula.getQuantifierVariables() |
java.util.Set<Variable> |
ForallQuantifiedFormula.getQuantifierVariables() |
java.util.Set<Variable> |
FolFormula.getQuantifierVariables() |
java.util.Set<Variable> |
ExistsQuantifiedFormula.getQuantifierVariables() |
java.util.Set<Variable> |
SpecialFormula.getUnboundVariables() |
java.util.Set<Variable> |
AssociativeFOLFormula.getUnboundVariables() |
java.util.Set<Variable> |
Equivalence.getUnboundVariables() |
java.util.Set<Variable> |
ForallQuantifiedFormula.getUnboundVariables() |
java.util.Set<Variable> |
ExistsQuantifiedFormula.getUnboundVariables() |
java.util.Set<Variable> |
FOLAtom.getUnboundVariables() |
java.util.Set<Variable> |
Implication.getUnboundVariables() |
java.util.Set<Variable> |
Negation.getUnboundVariables() |
abstract java.util.Set<Variable> |
LogicStructure.getVariables()
Returns all variables that appear in this structure.
|
Modifier and Type | Method and Description |
---|---|
boolean |
SpecialFormula.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
AssociativeFOLFormula.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
Equivalence.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
ForallQuantifiedFormula.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
ExistsQuantifiedFormula.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
FOLAtom.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
Implication.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
Negation.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
SpecialFormula.isWellBound(java.util.Set<Variable> boundVariables) |
boolean |
AssociativeFOLFormula.isWellBound(java.util.Set<Variable> boundVariables) |
boolean |
Equivalence.isWellBound(java.util.Set<Variable> boundVariables) |
boolean |
ForallQuantifiedFormula.isWellBound(java.util.Set<Variable> boundVariables) |
boolean |
ExistsQuantifiedFormula.isWellBound(java.util.Set<Variable> boundVariables) |
boolean |
FOLAtom.isWellBound(java.util.Set<Variable> boundVariables) |
boolean |
Implication.isWellBound(java.util.Set<Variable> boundVariables) |
boolean |
Negation.isWellBound(java.util.Set<Variable> boundVariables) |
void |
ForallQuantifiedFormula.setQuantifierVariables(java.util.Set<Variable> variables) |
void |
ExistsQuantifiedFormula.setQuantifierVariables(java.util.Set<Variable> variables) |
Constructor and Description |
---|
ExistsQuantifiedFormula(RelationalFormula folFormula,
Variable variable)
Creates a new quantified folFormula with the given folFormula and variable.
|
ForallQuantifiedFormula(RelationalFormula folFormula,
Variable variable)
Creates a new quantified folFormula with the given folFormula and variable.
|
Constructor and Description |
---|
ExistsQuantifiedFormula(RelationalFormula folFormula,
java.util.Set<Variable> variables)
Creates a new quantified folFormula with the given folFormula and variables.
|
ForallQuantifiedFormula(RelationalFormula folFormula,
java.util.Set<Variable> variables)
Creates a new quantified folFormula with the given folFormula and variables.
|
Modifier and Type | Method and Description |
---|---|
private java.lang.String |
Prover9Writer.printVar(Variable v)
Crates a type check or type def for a variable
|
private java.lang.String |
TPTPWriter.printVar(Variable v)
Crates a type check or type def for a variable
|
Modifier and Type | Method and Description |
---|---|
java.util.Set<Variable> |
ModalFormula.getQuantifierVariables() |
java.util.Set<Variable> |
ModalFormula.getUnboundVariables() |
Modifier and Type | Method and Description |
---|---|
boolean |
ModalFormula.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
ModalFormula.isWellBound(java.util.Set<Variable> boundVariables) |
Modifier and Type | Method and Description |
---|---|
java.util.Set<Variable> |
MlnFormula.getQuantifierVariables() |
java.util.Set<Variable> |
MlnFormula.getUnboundVariables() |
Modifier and Type | Method and Description |
---|---|
boolean |
MlnFormula.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
MlnFormula.isWellBound(java.util.Set<Variable> boundVariables) |
Modifier and Type | Method and Description |
---|---|
java.util.Set<Variable> |
RelationalConditional.getQuantifierVariables() |
java.util.Set<Variable> |
RelationalConditional.getUnboundVariables() |
Modifier and Type | Method and Description |
---|---|
boolean |
RelationalConditional.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
RelationalConditional.isWellBound(java.util.Set<Variable> boundVariables) |
Modifier and Type | Method and Description |
---|---|
java.util.Set<Variable> |
DefaultRule.getQuantifierVariables() |
java.util.Set<Variable> |
DefaultRule.getUnboundVariables() |
Modifier and Type | Method and Description |
---|---|
boolean |
DefaultRule.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
DefaultRule.isWellBound(java.util.Set<Variable> boundVariables) |
Modifier and Type | Field and Description |
---|---|
protected java.util.List<Variable> |
ASTSymbolicSet.variables |
Modifier and Type | Field and Description |
---|---|
protected java.util.Set<Variable> |
SymbolicSet.openVariables |
Modifier and Type | Method and Description |
---|---|
java.util.Set<Variable> |
SymbolicSet.getVariables() |
Constructor and Description |
---|
SymbolicSet(java.util.Collection<Variable> variables,
java.util.Collection<DLPElement> literals) |
Modifier and Type | Method and Description |
---|---|
java.util.Set<Variable> |
NLPNot.getUnboundVariables() |
Modifier and Type | Method and Description |
---|---|
boolean |
NLPNot.isClosed(java.util.Set<Variable> boundVariables) |
boolean |
NLPNot.isWellBound(java.util.Set<Variable> boundVariables) |