| 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 | 
VarsNeqRequirement.isValid(java.util.Map<Variable,Constant> assignment)  | 
boolean | 
VarConstNeqRequirement.isValid(java.util.Map<Variable,Constant> assignment)  | 
boolean | 
GroundingRequirement.isValid(java.util.Map<Variable,Constant> assignment)
This method checks, if an assignment of constants to variables satisfies a
 given grounding condition. 
 | 
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> | 
NecessarilyQuery.getVariables()  | 
java.util.Set<Variable> | 
HoldsQuery.getVariables()  | 
java.util.Set<Variable> | 
AlwaysQuery.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> | 
Sort.variables
The set of variables of this sort 
 | 
| Modifier and Type | Method and Description | 
|---|---|
Variable | 
Variable.clone()  | 
| Constructor and Description | 
|---|
Variable(Variable other)
Copy-Ctor: Creates a deep copy of the given Variable 
 | 
| 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 | 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 | Field and Description | 
|---|---|
private java.util.Map<java.lang.String,Variable> | 
FolParser.variables
Keeps track of variables defined. 
 | 
| Modifier and Type | Field and Description | 
|---|---|
private java.util.Set<Variable> | 
QuantifiedFormula.quantifier_variables
The variables of this quantified folFormula. 
 | 
| 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> | 
QuantifiedFormula.getQuantifierVariables()
Returns the variables of this quantified folFormula. 
 | 
java.util.Set<Variable> | 
FolFormula.getQuantifierVariables()  | 
java.util.Set<Variable> | 
AssociativeFOLFormula.getQuantifierVariables()  | 
java.util.Set<Variable> | 
SpecialFormula.getUnboundVariables()  | 
java.util.Set<Variable> | 
QuantifiedFormula.getUnboundVariables()  | 
java.util.Set<Variable> | 
Negation.getUnboundVariables()  | 
java.util.Set<Variable> | 
FOLAtom.getUnboundVariables()  | 
java.util.Set<Variable> | 
AssociativeFOLFormula.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 | 
QuantifiedFormula.isClosed(java.util.Set<Variable> boundVariables)  | 
boolean | 
Negation.isClosed(java.util.Set<Variable> boundVariables)  | 
boolean | 
FOLAtom.isClosed(java.util.Set<Variable> boundVariables)  | 
boolean | 
AssociativeFOLFormula.isClosed(java.util.Set<Variable> boundVariables)  | 
boolean | 
SpecialFormula.isWellBound(java.util.Set<Variable> boundVariables)  | 
boolean | 
QuantifiedFormula.isWellBound(java.util.Set<Variable> boundVariables)  | 
boolean | 
Negation.isWellBound(java.util.Set<Variable> boundVariables)  | 
boolean | 
FOLAtom.isWellBound(java.util.Set<Variable> boundVariables)  | 
boolean | 
AssociativeFOLFormula.isWellBound(java.util.Set<Variable> boundVariables)  | 
| Constructor and Description | 
|---|
ExistsQuantifiedFormula(FolFormula folFormula,
                       Variable variable)
Creates a new exists-quantified formula with the given formula and variable. 
 | 
ForallQuantifiedFormula(FolFormula folFormula,
                       Variable variable)
Creates a new for-all-quantified formula with the given formula and variable. 
 | 
QuantifiedFormula(FolFormula 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 exists-quantified formula with the given formula and variables. 
 | 
ForallQuantifiedFormula(RelationalFormula folFormula,
                       java.util.Set<Variable> variables)
Creates a new for-all-quantified formula with the given formula and variables. 
 | 
QuantifiedFormula(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 | 
TptpWriter.printVar(Variable v)
Crates a type check or type def for a variable 
 | 
private java.lang.String | 
Prover9Writer.printVar(Variable v)
Crates a type check or type def for a variable 
 | 
| 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)  |