|
|
|
@ -22,26 +22,28 @@ namespace detail
|
|
|
|
|
// Forward Declarations
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AndPointer<ast::Precondition> &and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AtomicFormula &, normalizedAST::DerivedPredicateDeclarations &);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ExistsPointer<ast::Precondition> &exists, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ForAllPointer<ast::Precondition> &forAll, normalizedAST::DerivedPredicateDeclarations &);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ImplyPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::NotPointer<ast::Precondition> ¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::OrPointer<ast::Precondition> &or_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::AndPointer<normalizedAST::Literal> normalizeTopLevel(ast::AndPointer<ast::Precondition> &and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::AtomicFormula normalizeTopLevel(ast::AtomicFormula &, normalizedAST::DerivedPredicateDeclarations &);
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ExistsPointer<ast::Precondition> &exists, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ForAllPointer<ast::Precondition> &forAll, normalizedAST::DerivedPredicateDeclarations &);
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ImplyPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &);
|
|
|
|
|
normalizedAST::NotPointer<normalizedAST::AtomicFormula> normalizeTopLevel(ast::NotPointer<ast::Precondition> ¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::OrPointer<normalizedAST::Literal> normalizeTopLevel(ast::OrPointer<ast::Precondition> &or_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AndPointer<ast::Precondition> &and_, detail::NormalizationContext &normalizationContext);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AtomicFormula &, detail::NormalizationContext &);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ExistsPointer<ast::Precondition> &exists, detail::NormalizationContext &normalizationContext);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ForAllPointer<ast::Precondition> &forAll, detail::NormalizationContext &);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ImplyPointer<ast::Precondition> &, detail::NormalizationContext &);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::NotPointer<ast::Precondition> ¬_, detail::NormalizationContext &normalizationContext);
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::OrPointer<ast::Precondition> &or_, detail::NormalizationContext &normalizationContext);
|
|
|
|
|
normalizedAST::AndPointer<normalizedAST::Literal> normalizeTopLevel(ast::AndPointer<ast::Precondition> &and_, detail::NormalizationContext &normalizationContext);
|
|
|
|
|
normalizedAST::AtomicFormula normalizeTopLevel(ast::AtomicFormula &, detail::NormalizationContext &);
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ExistsPointer<ast::Precondition> &exists, detail::NormalizationContext &normalizationContext);
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ForAllPointer<ast::Precondition> &forAll, detail::NormalizationContext &);
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ImplyPointer<ast::Precondition> &, detail::NormalizationContext &);
|
|
|
|
|
normalizedAST::NotPointer<normalizedAST::AtomicFormula> normalizeTopLevel(ast::NotPointer<ast::Precondition> ¬_, detail::NormalizationContext &normalizationContext);
|
|
|
|
|
normalizedAST::OrPointer<normalizedAST::Literal> normalizeTopLevel(ast::OrPointer<ast::Precondition> &or_, detail::NormalizationContext &normalizationContext);
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::DerivedPredicatePointer addDerivedPredicate(const std::vector<normalizedAST::VariableDeclaration *> ¶meters, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
normalizedAST::DerivedPredicatePointer addDerivedPredicate(const std::vector<normalizedAST::VariableDeclaration *> ¶meters, detail::NormalizationContext &normalizationContext)
|
|
|
|
|
{
|
|
|
|
|
auto name = "derived-predicate-" + std::to_string(derivedPredicates.size() + 1);
|
|
|
|
|
auto &derivedPredicates = normalizationContext.derivedPredicates;
|
|
|
|
|
const auto derivedPredicateID = normalizationContext.derivedPredicateIDStart + derivedPredicates.size() + 1;
|
|
|
|
|
auto name = "derived-predicate-" + std::to_string(derivedPredicateID);
|
|
|
|
|
|
|
|
|
|
normalizedAST::DerivedPredicate::Arguments arguments;
|
|
|
|
|
arguments.reserve(parameters.size());
|
|
|
|
@ -60,14 +62,14 @@ normalizedAST::DerivedPredicatePointer addDerivedPredicate(const std::vector<nor
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AndPointer<ast::Precondition> &and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AndPointer<ast::Precondition> &and_, detail::NormalizationContext &normalizationContext)
|
|
|
|
|
{
|
|
|
|
|
std::vector<normalizedAST::VariableDeclaration *> parameters;
|
|
|
|
|
VariableStack variableStack;
|
|
|
|
|
|
|
|
|
|
collectFreeVariables(and_, parameters, variableStack);
|
|
|
|
|
|
|
|
|
|
auto derivedPredicate = addDerivedPredicate(parameters, derivedPredicates);
|
|
|
|
|
auto derivedPredicate = addDerivedPredicate(parameters, normalizationContext);
|
|
|
|
|
|
|
|
|
|
normalizedAST::And<normalizedAST::Literal>::Arguments normalizedArguments;
|
|
|
|
|
normalizedArguments.reserve(and_->arguments.size());
|
|
|
|
@ -76,7 +78,7 @@ normalizedAST::Literal normalizeNested(ast::AndPointer<ast::Precondition> &and_,
|
|
|
|
|
normalizedArguments.emplace_back(argument.match(
|
|
|
|
|
[&](auto &x) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalizeNested(x, derivedPredicates);
|
|
|
|
|
return normalizeNested(x, normalizationContext);
|
|
|
|
|
}));
|
|
|
|
|
|
|
|
|
|
derivedPredicate->declaration->precondition = std::make_unique<normalizedAST::And<normalizedAST::Literal>>(std::move(normalizedArguments));
|
|
|
|
@ -87,27 +89,27 @@ normalizedAST::Literal normalizeNested(ast::AndPointer<ast::Precondition> &and_,
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AtomicFormula &atomicFormula, normalizedAST::DerivedPredicateDeclarations &)
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::AtomicFormula &atomicFormula, detail::NormalizationContext &)
|
|
|
|
|
{
|
|
|
|
|
return normalize(std::move(atomicFormula));
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ExistsPointer<ast::Precondition> &exists, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ExistsPointer<ast::Precondition> &exists, detail::NormalizationContext &normalizationContext)
|
|
|
|
|
{
|
|
|
|
|
std::vector<normalizedAST::VariableDeclaration *> parameters;
|
|
|
|
|
VariableStack variableStack;
|
|
|
|
|
|
|
|
|
|
collectFreeVariables(exists, parameters, variableStack);
|
|
|
|
|
|
|
|
|
|
auto derivedPredicate = addDerivedPredicate(parameters, derivedPredicates);
|
|
|
|
|
auto derivedPredicate = addDerivedPredicate(parameters, normalizationContext);
|
|
|
|
|
|
|
|
|
|
derivedPredicate->declaration->existentialParameters = std::move(exists->parameters);
|
|
|
|
|
derivedPredicate->declaration->precondition = exists->argument.match(
|
|
|
|
|
[&](auto &x) -> normalizedAST::DerivedPredicatePrecondition
|
|
|
|
|
{
|
|
|
|
|
return normalizeTopLevel(x, derivedPredicates);
|
|
|
|
|
return normalizeTopLevel(x, normalizationContext);
|
|
|
|
|
});
|
|
|
|
|
|
|
|
|
|
// TODO: investigate, could be a compiler bug
|
|
|
|
@ -116,7 +118,7 @@ normalizedAST::Literal normalizeNested(ast::ExistsPointer<ast::Precondition> &ex
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ForAllPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &)
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ForAllPointer<ast::Precondition> &, detail::NormalizationContext &)
|
|
|
|
|
{
|
|
|
|
|
// “forall” expressions should be reduced to negated “exists” statements at this point
|
|
|
|
|
throw std::logic_error("precondition not in normal form (forall), please report to the bug tracker");
|
|
|
|
@ -124,7 +126,7 @@ normalizedAST::Literal normalizeNested(ast::ForAllPointer<ast::Precondition> &,
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ImplyPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &)
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::ImplyPointer<ast::Precondition> &, detail::NormalizationContext &)
|
|
|
|
|
{
|
|
|
|
|
// “imply” expressions should be reduced to disjunctions at this point
|
|
|
|
|
throw std::logic_error("precondition not in normal form (imply), please report to the bug tracker");
|
|
|
|
@ -132,12 +134,12 @@ normalizedAST::Literal normalizeNested(ast::ImplyPointer<ast::Precondition> &, n
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::NotPointer<ast::Precondition> ¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::NotPointer<ast::Precondition> ¬_, detail::NormalizationContext &normalizationContext)
|
|
|
|
|
{
|
|
|
|
|
auto normalizedArgumentLiteral = not_->argument.match(
|
|
|
|
|
[&](auto &x) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalizeNested(x, derivedPredicates);
|
|
|
|
|
return normalizeNested(x, normalizationContext);
|
|
|
|
|
});
|
|
|
|
|
|
|
|
|
|
// Multiple negations should be eliminated at this point
|
|
|
|
@ -151,14 +153,14 @@ normalizedAST::Literal normalizeNested(ast::NotPointer<ast::Precondition> ¬_,
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::OrPointer<ast::Precondition> &or_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
normalizedAST::Literal normalizeNested(ast::OrPointer<ast::Precondition> &or_, detail::NormalizationContext &normalizationContext)
|
|
|
|
|
{
|
|
|
|
|
std::vector<normalizedAST::VariableDeclaration *> parameters;
|
|
|
|
|
VariableStack variableStack;
|
|
|
|
|
|
|
|
|
|
collectFreeVariables(or_, parameters, variableStack);
|
|
|
|
|
|
|
|
|
|
auto derivedPredicate = addDerivedPredicate(parameters, derivedPredicates);
|
|
|
|
|
auto derivedPredicate = addDerivedPredicate(parameters, normalizationContext);
|
|
|
|
|
|
|
|
|
|
normalizedAST::Or<normalizedAST::Literal>::Arguments normalizedArguments;
|
|
|
|
|
normalizedArguments.reserve(or_->arguments.size());
|
|
|
|
@ -167,7 +169,7 @@ normalizedAST::Literal normalizeNested(ast::OrPointer<ast::Precondition> &or_, n
|
|
|
|
|
normalizedArguments.emplace_back(argument.match(
|
|
|
|
|
[&](auto &x) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalizeNested(x, derivedPredicates);
|
|
|
|
|
return normalizeNested(x, normalizationContext);
|
|
|
|
|
}));
|
|
|
|
|
|
|
|
|
|
derivedPredicate->declaration->precondition = std::make_unique<normalizedAST::Or<normalizedAST::Literal>>(std::move(normalizedArguments));
|
|
|
|
@ -178,7 +180,7 @@ normalizedAST::Literal normalizeNested(ast::OrPointer<ast::Precondition> &or_, n
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::AtomicFormula normalizeTopLevel(ast::AtomicFormula &atomicFormula, normalizedAST::DerivedPredicateDeclarations &)
|
|
|
|
|
normalizedAST::AtomicFormula normalizeTopLevel(ast::AtomicFormula &atomicFormula, detail::NormalizationContext &)
|
|
|
|
|
{
|
|
|
|
|
return normalize(std::move(atomicFormula));
|
|
|
|
|
}
|
|
|
|
@ -186,7 +188,7 @@ normalizedAST::AtomicFormula normalizeTopLevel(ast::AtomicFormula &atomicFormula
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
// Normalize top-level conjunctions
|
|
|
|
|
normalizedAST::AndPointer<normalizedAST::Literal> normalizeTopLevel(ast::AndPointer<ast::Precondition> &and_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
normalizedAST::AndPointer<normalizedAST::Literal> normalizeTopLevel(ast::AndPointer<ast::Precondition> &and_, detail::NormalizationContext &normalizationContext)
|
|
|
|
|
{
|
|
|
|
|
normalizedAST::And<normalizedAST::Literal>::Arguments arguments;
|
|
|
|
|
|
|
|
|
@ -201,13 +203,13 @@ normalizedAST::AndPointer<normalizedAST::Literal> normalizeTopLevel(ast::AndPoin
|
|
|
|
|
const auto handleNot =
|
|
|
|
|
[&](ast::NotPointer<ast::Precondition> ¬_) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalizeTopLevel(not_, derivedPredicates);
|
|
|
|
|
return normalizeTopLevel(not_, normalizationContext);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
const auto handleNested =
|
|
|
|
|
[&](auto &nested) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalizeNested(nested, derivedPredicates);
|
|
|
|
|
return normalizeNested(nested, normalizationContext);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
for (auto &argument : and_->arguments)
|
|
|
|
@ -222,21 +224,21 @@ normalizedAST::AndPointer<normalizedAST::Literal> normalizeTopLevel(ast::AndPoin
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ExistsPointer<ast::Precondition> &exists, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ExistsPointer<ast::Precondition> &exists, detail::NormalizationContext &normalizationContext)
|
|
|
|
|
{
|
|
|
|
|
return normalizeNested(exists, derivedPredicates);
|
|
|
|
|
return normalizeNested(exists, normalizationContext);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ForAllPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &)
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ForAllPointer<ast::Precondition> &, detail::NormalizationContext &)
|
|
|
|
|
{
|
|
|
|
|
throw std::logic_error("precondition not in normal form (forall), please report to the bug tracker");
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ImplyPointer<ast::Precondition> &, normalizedAST::DerivedPredicateDeclarations &)
|
|
|
|
|
normalizedAST::Literal normalizeTopLevel(ast::ImplyPointer<ast::Precondition> &, detail::NormalizationContext &)
|
|
|
|
|
{
|
|
|
|
|
throw std::logic_error("precondition not in normal form (imply), please report to the bug tracker");
|
|
|
|
|
}
|
|
|
|
@ -244,7 +246,7 @@ normalizedAST::Literal normalizeTopLevel(ast::ImplyPointer<ast::Precondition> &,
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
// Normalize top-level negations
|
|
|
|
|
normalizedAST::NotPointer<normalizedAST::AtomicFormula> normalizeTopLevel(ast::NotPointer<ast::Precondition> ¬_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
normalizedAST::NotPointer<normalizedAST::AtomicFormula> normalizeTopLevel(ast::NotPointer<ast::Precondition> ¬_, detail::NormalizationContext &normalizationContext)
|
|
|
|
|
{
|
|
|
|
|
// “not” expressions may be nested one time to form simple literals
|
|
|
|
|
if (not_->argument.is<ast::AtomicFormula>())
|
|
|
|
@ -253,7 +255,7 @@ normalizedAST::NotPointer<normalizedAST::AtomicFormula> normalizeTopLevel(ast::N
|
|
|
|
|
auto normalizedArgument = not_->argument.match(
|
|
|
|
|
[&](auto &nested) -> normalizedAST::AtomicFormula
|
|
|
|
|
{
|
|
|
|
|
auto normalizedLiteral = normalizeNested(nested, derivedPredicates);
|
|
|
|
|
auto normalizedLiteral = normalizeNested(nested, normalizationContext);
|
|
|
|
|
|
|
|
|
|
// Multiple negations should be eliminated at this point
|
|
|
|
|
if (normalizedLiteral.template is<normalizedAST::NotPointer<normalizedAST::AtomicFormula>>())
|
|
|
|
@ -268,7 +270,7 @@ normalizedAST::NotPointer<normalizedAST::AtomicFormula> normalizeTopLevel(ast::N
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
// TODO: refactor to avoid code duplication
|
|
|
|
|
normalizedAST::OrPointer<normalizedAST::Literal> normalizeTopLevel(ast::OrPointer<ast::Precondition> &or_, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
normalizedAST::OrPointer<normalizedAST::Literal> normalizeTopLevel(ast::OrPointer<ast::Precondition> &or_, detail::NormalizationContext &normalizationContext)
|
|
|
|
|
{
|
|
|
|
|
normalizedAST::Or<normalizedAST::Literal>::Arguments arguments;
|
|
|
|
|
|
|
|
|
@ -283,13 +285,13 @@ normalizedAST::OrPointer<normalizedAST::Literal> normalizeTopLevel(ast::OrPointe
|
|
|
|
|
const auto handleNot =
|
|
|
|
|
[&](ast::NotPointer<ast::Precondition> ¬_) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalizeTopLevel(not_, derivedPredicates);
|
|
|
|
|
return normalizeTopLevel(not_, normalizationContext);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
const auto handleNested =
|
|
|
|
|
[&](auto &nested) -> normalizedAST::Literal
|
|
|
|
|
{
|
|
|
|
|
return normalizeNested(nested, derivedPredicates);
|
|
|
|
|
return normalizeNested(nested, normalizationContext);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
for (auto &argument : or_->arguments)
|
|
|
|
@ -304,7 +306,7 @@ normalizedAST::OrPointer<normalizedAST::Literal> normalizeTopLevel(ast::OrPointe
|
|
|
|
|
|
|
|
|
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
|
|
|
|
|
|
|
|
|
normalizedAST::Precondition normalize(ast::Precondition &&precondition, normalizedAST::DerivedPredicateDeclarations &derivedPredicates)
|
|
|
|
|
normalizedAST::Precondition normalize(ast::Precondition &&precondition, detail::NormalizationContext &normalizationContext)
|
|
|
|
|
{
|
|
|
|
|
// Bring precondition to normal form
|
|
|
|
|
reduce(precondition);
|
|
|
|
@ -312,43 +314,43 @@ normalizedAST::Precondition normalize(ast::Precondition &&precondition, normaliz
|
|
|
|
|
const auto handleAtomicFormula =
|
|
|
|
|
[&](ast::AtomicFormula &atomicFormula) -> normalizedAST::Precondition
|
|
|
|
|
{
|
|
|
|
|
return normalizeTopLevel(atomicFormula, derivedPredicates);
|
|
|
|
|
return normalizeTopLevel(atomicFormula, normalizationContext);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
const auto handleAnd =
|
|
|
|
|
[&](ast::AndPointer<ast::Precondition> &and_) -> normalizedAST::Precondition
|
|
|
|
|
{
|
|
|
|
|
return normalizeTopLevel(and_, derivedPredicates);
|
|
|
|
|
return normalizeTopLevel(and_, normalizationContext);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
const auto handleExists =
|
|
|
|
|
[&](ast::ExistsPointer<ast::Precondition> &exists) -> normalizedAST::Precondition
|
|
|
|
|
{
|
|
|
|
|
return normalizeTopLevel(exists, derivedPredicates);
|
|
|
|
|
return normalizeTopLevel(exists, normalizationContext);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
const auto handleForAll =
|
|
|
|
|
[&](ast::ForAllPointer<ast::Precondition> &forAll) -> normalizedAST::Precondition
|
|
|
|
|
{
|
|
|
|
|
return normalizeTopLevel(forAll, derivedPredicates);
|
|
|
|
|
return normalizeTopLevel(forAll, normalizationContext);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
const auto handleImply =
|
|
|
|
|
[&](ast::ImplyPointer<ast::Precondition> &imply) -> normalizedAST::Precondition
|
|
|
|
|
{
|
|
|
|
|
return normalizeTopLevel(imply, derivedPredicates);
|
|
|
|
|
return normalizeTopLevel(imply, normalizationContext);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
const auto handleNot =
|
|
|
|
|
[&](ast::NotPointer<ast::Precondition> ¬_) -> normalizedAST::Precondition
|
|
|
|
|
{
|
|
|
|
|
return normalizeTopLevel(not_, derivedPredicates);
|
|
|
|
|
return normalizeTopLevel(not_, normalizationContext);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
const auto handleOr =
|
|
|
|
|
[&](ast::OrPointer<ast::Precondition> &or_) -> normalizedAST::Precondition
|
|
|
|
|
{
|
|
|
|
|
return normalizeNested(or_, derivedPredicates);
|
|
|
|
|
return normalizeNested(or_, normalizationContext);
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
return precondition.match(handleAtomicFormula, handleAnd, handleExists, handleForAll, handleImply, handleNot, handleOr);
|
|
|
|
|