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

Omitting the universal quantifier for completion if predicate is 0-ary.

Browse Source
This commit is contained in:
Patrick Lühne 2017-04-08 14:51:16 +02:00
parent cc27ed7595
commit a23e248e7b
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
1 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/anthem/Completion.cpp
View File

@ -70,6 +70,15 @@ void completePredicate(const ast::Predicate &predicate, std::vector<ast::Formula
i++;
}
// Build the biconditional within the completed formula
auto biconditional = ast::Formula::make<ast::Biconditional>(ast::deepCopy(predicate), std::move(or_));
if (predicate.arguments.empty())
{
formulas[formulasBegin] = std::move(biconditional);
return;
}
// Copy the predicate’s arguments for the completed formula
std::vector<ast::Variable> variables;
variables.reserve(predicate.arguments.size());
@ -80,11 +89,8 @@ void completePredicate(const ast::Predicate &predicate, std::vector<ast::Formula
variables.emplace_back(ast::deepCopy(argument.get<ast::Variable>()));
}
// Build the completed formula
auto biconditional = ast::Formula::make<ast::Biconditional>(ast::deepCopy(predicate), std::move(or_));
auto completedFormula = ast::Formula::make<ast::ForAll>(std::move(variables), std::move(biconditional));
// TODO: reduce formula, for instance, if there are no variables in the for-all expression
formulas[formulasBegin] = std::move(completedFormula);
}