patrick/anthem
1
0
Fork 0
Code Issues 15 Releases 21 Activity

Refactor integer variable detection

Browse Source 
This reimplements integer variable detection as two parts. The first one
is a visitor class that recursively searches for all declared variables
in a formula and applies the second part, a custom functor.

Two such functors are implemented. The first one checks whether a
predicate definition is falsified by making a variable noninteger, in
which case it can be concluded that the variable in question is integer.
The second functor checks whether bound variables in a quantified
formula turn the quantified part false, again to conclude that variables
are integer.
This commit is contained in:
Patrick Lühne 2018-04-21 16:54:08 +02:00
parent 8f3ff23f38
commit f65d4dbbd8
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 102 additions and 111 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

211
src/anthem/IntegerVariableDetection.cpp
View File

@ -381,163 +381,117 @@ EvaluationResult evaluate(const ast::Formula &formula, VariableDomainMap &variab
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap); template <class Functor>
struct ForEachVariableDeclarationVisitor
////////////////////////////////////////////////////////////////////////////////////////////////////
struct DetectIntegerVariablesVisitor
{ {
static OperationResult visit(ast::And &and_, ast::Formula &definition, VariableDomainMap &variableDomainMap) template <class... Arguments>
static OperationResult visit(ast::And &and_, Arguments &&... arguments)
{ {
auto operationResult = OperationResult::Unchanged; auto operationResult = OperationResult::Unchanged;
for (auto &argument : and_.arguments) for (auto &argument : and_.arguments)
if (detectIntegerVariables(argument, definition, variableDomainMap) == OperationResult::Changed) if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
return operationResult; return operationResult;
} }
static OperationResult visit(ast::Biconditional &biconditional, ast::Formula &definition, VariableDomainMap &variableDomainMap) template <class... Arguments>
static OperationResult visit(ast::Biconditional &biconditional, Arguments &&... arguments)
{ {
auto operationResult = OperationResult::Unchanged; auto operationResult = OperationResult::Unchanged;
if (detectIntegerVariables(biconditional.left, definition, variableDomainMap) == OperationResult::Changed) if (biconditional.left.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
if (detectIntegerVariables(biconditional.right, definition, variableDomainMap) == OperationResult::Changed) if (biconditional.right.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
return operationResult; return operationResult;
} }
static OperationResult visit(ast::Boolean &, ast::Formula &, VariableDomainMap &) template <class... Arguments>
static OperationResult visit(ast::Boolean &, Arguments &&...)
{ {
return OperationResult::Unchanged; return OperationResult::Unchanged;
} }
static OperationResult visit(ast::Comparison &, ast::Formula &, VariableDomainMap &) template <class... Arguments>
static OperationResult visit(ast::Comparison &, Arguments &&...)
{ {
return OperationResult::Unchanged; return OperationResult::Unchanged;
} }
static OperationResult visit(ast::Exists &exists, ast::Formula &definition, VariableDomainMap &variableDomainMap) template <class... Arguments>
static OperationResult visit(ast::Exists &exists, Arguments &&... arguments)
{ {
auto operationResult = OperationResult::Unchanged; auto operationResult = OperationResult::Unchanged;
if (detectIntegerVariables(exists.argument, definition, variableDomainMap) == OperationResult::Changed) if (exists.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
for (auto &variableDeclaration : exists.variables) for (auto &variableDeclaration : exists.variables)
{ if (Functor()(*variableDeclaration, exists.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
if (variableDeclaration->domain != ast::Domain::Unknown)
continue;
clearVariableDomainMap(variableDomainMap);
auto argumentResult = evaluate(exists.argument, variableDomainMap);
auto definitionResult = evaluate(definition, variableDomainMap);
if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|| definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
{
continue;
}
// As a hypothesis, make the parameter’s domain noninteger
variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
argumentResult = evaluate(exists.argument, variableDomainMap);
definitionResult = evaluate(definition, variableDomainMap);
if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|| definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
{
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
variableDeclaration->domain = ast::Domain::Integer;
}
}
return operationResult; return operationResult;
} }
static OperationResult visit(ast::ForAll &forAll, ast::Formula &definition, VariableDomainMap &variableDomainMap) template <class... Arguments>
static OperationResult visit(ast::ForAll &forAll, Arguments &&... arguments)
{ {
auto operationResult = OperationResult::Unchanged; auto operationResult = OperationResult::Unchanged;
if (detectIntegerVariables(forAll.argument, definition, variableDomainMap) == OperationResult::Changed) if (forAll.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
for (auto &variableDeclaration : forAll.variables) for (auto &variableDeclaration : forAll.variables)
{ if (Functor()(*variableDeclaration, forAll.argument, std::forward<Arguments>(arguments)...) == OperationResult::Changed)
if (variableDeclaration->domain != ast::Domain::Unknown)
continue;
clearVariableDomainMap(variableDomainMap);
auto argumentResult = evaluate(forAll.argument, variableDomainMap);
auto definitionResult = evaluate(definition, variableDomainMap);
if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|| definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
{
continue;
}
// As a hypothesis, make the parameter’s domain noninteger
variableDomainMap[variableDeclaration.get()] = ast::Domain::General;
argumentResult = evaluate(forAll.argument, variableDomainMap);
definitionResult = evaluate(definition, variableDomainMap);
if (argumentResult == EvaluationResult::Error || argumentResult == EvaluationResult::False
|| definitionResult == EvaluationResult::Error || definitionResult == EvaluationResult::False)
{
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
variableDeclaration->domain = ast::Domain::Integer;
}
}
return operationResult; return operationResult;
} }
static OperationResult visit(ast::Implies &implies, ast::Formula &definition, VariableDomainMap &variableDomainMap) template <class... Arguments>
static OperationResult visit(ast::Implies &implies, Arguments &&... arguments)
{ {
auto operationResult = OperationResult::Unchanged; auto operationResult = OperationResult::Unchanged;
if (detectIntegerVariables(implies.antecedent, definition, variableDomainMap) == OperationResult::Changed) if (implies.antecedent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
if (detectIntegerVariables(implies.consequent, definition, variableDomainMap) == OperationResult::Changed) if (implies.consequent.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
return operationResult; return operationResult;
} }
static OperationResult visit(ast::In &, ast::Formula &, VariableDomainMap &) template <class... Arguments>
static OperationResult visit(ast::In &, Arguments &&...)
{ {
return OperationResult::Unchanged; return OperationResult::Unchanged;
} }
static OperationResult visit(ast::Not &not_, ast::Formula &definition, VariableDomainMap &variableDomainMap) template <class... Arguments>
static OperationResult visit(ast::Not &not_, Arguments &&... arguments)
{ {
return detectIntegerVariables(not_.argument, definition, variableDomainMap); return not_.argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...);
} }
static OperationResult visit(ast::Or &or_, ast::Formula &definition, VariableDomainMap &variableDomainMap) template <class... Arguments>
static OperationResult visit(ast::Or &or_, Arguments &&... arguments)
{ {
auto operationResult = OperationResult::Unchanged; auto operationResult = OperationResult::Unchanged;
for (auto &argument : or_.arguments) for (auto &argument : or_.arguments)
if (detectIntegerVariables(argument, definition, variableDomainMap) == OperationResult::Changed) if (argument.accept(ForEachVariableDeclarationVisitor(), std::forward<Arguments>(arguments)...) == OperationResult::Changed)
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
return operationResult; return operationResult;
} }
static OperationResult visit(ast::Predicate &, ast::Formula &, VariableDomainMap &) template <class... Arguments>
static OperationResult visit(ast::Predicate &, Arguments &&...)
{ {
return OperationResult::Unchanged; return OperationResult::Unchanged;
} }
@ -545,11 +499,70 @@ struct DetectIntegerVariablesVisitor
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
OperationResult detectIntegerVariables(ast::Formula &formula, ast::Formula &definition, VariableDomainMap &variableDomainMap) struct CheckIfDefinitionFalseFunctor
{ {
return formula.accept(DetectIntegerVariablesVisitor(), definition, variableDomainMap); OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
ast::Formula &, ast::Formula &definition, VariableDomainMap &variableDomainMap)
{
if (variableDeclaration.domain != ast::Domain::Unknown)
return OperationResult::Unchanged;
clearVariableDomainMap(variableDomainMap);
auto result = evaluate(definition, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
return OperationResult::Unchanged;
// As a hypothesis, make the parameter’s domain noninteger
variableDomainMap[&variableDeclaration] = ast::Domain::General;
result = evaluate(definition, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
{
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
variableDeclaration.domain = ast::Domain::Integer;
return OperationResult::Changed;
} }
return OperationResult::Unchanged;
}
};
////////////////////////////////////////////////////////////////////////////////////////////////////
struct CheckIfQuantifiedFormulaFalseFunctor
{
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
ast::Formula &quantifiedFormula, VariableDomainMap &variableDomainMap)
{
if (variableDeclaration.domain != ast::Domain::Unknown)
return OperationResult::Unchanged;
clearVariableDomainMap(variableDomainMap);
auto result = evaluate(quantifiedFormula, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
return OperationResult::Unchanged;
// As a hypothesis, make the parameter’s domain noninteger
variableDomainMap[&variableDeclaration] = ast::Domain::General;
result = evaluate(quantifiedFormula, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
{
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
variableDeclaration.domain = ast::Domain::Integer;
return OperationResult::Changed;
}
return OperationResult::Unchanged;
}
};
//////////////////////////////////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////////////////////////////////
// Assumes the completed formulas to be in translated but not simplified form. // Assumes the completed formulas to be in translated but not simplified form.
@ -565,7 +578,7 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
for (auto &completedFormula : completedFormulas) for (auto &completedFormula : completedFormulas)
{ {
if (detectIntegerVariables(completedFormula, completedFormula, variableDomainMap) == OperationResult::Changed) if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfQuantifiedFormulaFalseFunctor>(), variableDomainMap) == OperationResult::Changed)
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
if (!completedFormula.is<ast::ForAll>()) if (!completedFormula.is<ast::ForAll>())
@ -584,12 +597,11 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
auto &predicate = biconditional.left.get<ast::Predicate>(); auto &predicate = biconditional.left.get<ast::Predicate>();
auto &definition = biconditional.right; auto &definition = biconditional.right;
assert(predicate.arguments.size() == predicate.declaration->arity()); if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfDefinitionFalseFunctor>(), definition, variableDomainMap) == OperationResult::Changed)
// TODO: refactor
if (detectIntegerVariables(definition, definition, variableDomainMap) == OperationResult::Changed)
operationResult = OperationResult::Changed; operationResult = OperationResult::Changed;
assert(predicate.arguments.size() == predicate.declaration->arity());
for (size_t i = 0; i < predicate.arguments.size(); i++) for (size_t i = 0; i < predicate.arguments.size(); i++)
{ {
auto &variableArgument = predicate.arguments[i]; auto &variableArgument = predicate.arguments[i];
@ -599,28 +611,7 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
auto &variable = variableArgument.get<ast::Variable>(); auto &variable = variableArgument.get<ast::Variable>();
if (parameter.domain != ast::Domain::Unknown) parameter.domain = variable.declaration->domain;
continue;
clearVariableDomainMap(variableDomainMap);
auto result = evaluate(definition, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
continue;
// As a hypothesis, make the parameter’s domain noninteger
variableDomainMap[variable.declaration] = ast::Domain::General;
result = evaluate(definition, variableDomainMap);
if (result == EvaluationResult::Error || result == EvaluationResult::False)
{
// If making the variable noninteger leads to a false or erroneous result, it’s proven to be integer
operationResult = OperationResult::Changed;
variable.declaration->domain = ast::Domain::Integer;
parameter.domain = ast::Domain::Integer;
}
} }
} }
} }