Extend integer variable detection
If making a variable noninteger turns the entire formula obtained from completion true, we can drop that statement and conclude that the variable is integer.
This commit is contained in:
parent
9c792ff079
commit
28dbd407e2
@ -565,6 +565,39 @@ struct CheckIfQuantifiedFormulaFalseFunctor
|
|||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
struct CheckIfCompletedFormulaTrueFunctor
|
||||||
|
{
|
||||||
|
OperationResult operator()(ast::VariableDeclaration &variableDeclaration,
|
||||||
|
ast::Formula &, ast::Formula &completedFormula, VariableDomainMap &variableDomainMap)
|
||||||
|
{
|
||||||
|
if (variableDeclaration.domain != ast::Domain::Unknown)
|
||||||
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
|
clearVariableDomainMap(variableDomainMap);
|
||||||
|
|
||||||
|
auto result = evaluate(completedFormula, variableDomainMap);
|
||||||
|
|
||||||
|
if (result == EvaluationResult::Error || result == EvaluationResult::True)
|
||||||
|
return OperationResult::Unchanged;
|
||||||
|
|
||||||
|
// As a hypothesis, make the parameter’s domain noninteger
|
||||||
|
variableDomainMap[&variableDeclaration] = ast::Domain::General;
|
||||||
|
|
||||||
|
result = evaluate(completedFormula, variableDomainMap);
|
||||||
|
|
||||||
|
if (result == EvaluationResult::Error || result == EvaluationResult::True)
|
||||||
|
{
|
||||||
|
// 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.
|
||||||
// That is, completed formulas are either variable-free or universally quantified
|
// That is, completed formulas are either variable-free or universally quantified
|
||||||
void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
|
void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
|
||||||
@ -581,6 +614,9 @@ void detectIntegerVariables(std::vector<ast::Formula> &completedFormulas)
|
|||||||
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfQuantifiedFormulaFalseFunctor>(), variableDomainMap) == OperationResult::Changed)
|
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfQuantifiedFormulaFalseFunctor>(), variableDomainMap) == OperationResult::Changed)
|
||||||
operationResult = OperationResult::Changed;
|
operationResult = OperationResult::Changed;
|
||||||
|
|
||||||
|
if (completedFormula.accept(ForEachVariableDeclarationVisitor<CheckIfCompletedFormulaTrueFunctor>(), completedFormula, variableDomainMap) == OperationResult::Changed)
|
||||||
|
operationResult = OperationResult::Changed;
|
||||||
|
|
||||||
if (!completedFormula.is<ast::ForAll>())
|
if (!completedFormula.is<ast::ForAll>())
|
||||||
continue;
|
continue;
|
||||||
|
|
||||||
|
Loading…
x
Reference in New Issue
Block a user