Minor formatting.
This commit is contained in:
parent
4f003a8730
commit
957457939c
@ -15,9 +15,9 @@ namespace ast
|
|||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
// Terms are primitive (or arguments) if they are neither operations nor intervals
|
// Terms are primitive (or arguments) if they are neither operations nor intervals
|
||||||
inline bool isPrimitive(const ast::Term &term)
|
inline bool isPrimitive(const Term &term)
|
||||||
{
|
{
|
||||||
return (!term.is<ast::BinaryOperation>() && !term.is<ast::Interval>());
|
return (!term.is<BinaryOperation>() && !term.is<Interval>());
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
@ -362,7 +362,7 @@ struct Biconditional
|
|||||||
struct Exists
|
struct Exists
|
||||||
{
|
{
|
||||||
// TODO: rename “variables”
|
// TODO: rename “variables”
|
||||||
explicit Exists(std::vector<std::unique_ptr<VariableDeclaration>> &&variables, Formula &&argument)
|
explicit Exists(VariableDeclarationPointers &&variables, Formula &&argument)
|
||||||
: variables{std::move(variables)},
|
: variables{std::move(variables)},
|
||||||
argument{std::move(argument)}
|
argument{std::move(argument)}
|
||||||
{
|
{
|
||||||
@ -373,7 +373,7 @@ struct Exists
|
|||||||
Exists(Exists &&other) noexcept = default;
|
Exists(Exists &&other) noexcept = default;
|
||||||
Exists &operator=(Exists &&other) noexcept = default;
|
Exists &operator=(Exists &&other) noexcept = default;
|
||||||
|
|
||||||
std::vector<std::unique_ptr<VariableDeclaration>> variables;
|
VariableDeclarationPointers variables;
|
||||||
Formula argument;
|
Formula argument;
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -381,7 +381,7 @@ struct Exists
|
|||||||
|
|
||||||
struct ForAll
|
struct ForAll
|
||||||
{
|
{
|
||||||
explicit ForAll(std::vector<std::unique_ptr<VariableDeclaration>> &&variables, Formula &&argument)
|
explicit ForAll(VariableDeclarationPointers &&variables, Formula &&argument)
|
||||||
: variables{std::move(variables)},
|
: variables{std::move(variables)},
|
||||||
argument{std::move(argument)}
|
argument{std::move(argument)}
|
||||||
{
|
{
|
||||||
@ -392,7 +392,7 @@ struct ForAll
|
|||||||
ForAll(ForAll &&other) noexcept = default;
|
ForAll(ForAll &&other) noexcept = default;
|
||||||
ForAll &operator=(ForAll &&other) noexcept = default;
|
ForAll &operator=(ForAll &&other) noexcept = default;
|
||||||
|
|
||||||
std::vector<std::unique_ptr<VariableDeclaration>> variables;
|
VariableDeclarationPointers variables;
|
||||||
Formula argument;
|
Formula argument;
|
||||||
};
|
};
|
||||||
|
|
||||||
@ -457,14 +457,14 @@ struct Or
|
|||||||
|
|
||||||
struct ScopedFormula
|
struct ScopedFormula
|
||||||
{
|
{
|
||||||
explicit ScopedFormula(ast::Formula &&formula, std::vector<std::unique_ptr<ast::VariableDeclaration>> &&freeVariables)
|
explicit ScopedFormula(Formula &&formula, VariableDeclarationPointers &&freeVariables)
|
||||||
: formula{std::move(formula)},
|
: formula{std::move(formula)},
|
||||||
freeVariables{std::move(freeVariables)}
|
freeVariables{std::move(freeVariables)}
|
||||||
{
|
{
|
||||||
}
|
}
|
||||||
|
|
||||||
ast::Formula formula;
|
Formula formula;
|
||||||
std::vector<std::unique_ptr<ast::VariableDeclaration>> freeVariables;
|
VariableDeclarationPointers freeVariables;
|
||||||
};
|
};
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
@ -22,9 +22,9 @@ namespace ast
|
|||||||
|
|
||||||
struct PrintContext
|
struct PrintContext
|
||||||
{
|
{
|
||||||
std::map<const ast::VariableDeclaration *, size_t> userVariableIDs;
|
std::map<const VariableDeclaration *, size_t> userVariableIDs;
|
||||||
std::map<const ast::VariableDeclaration *, size_t> headVariableIDs;
|
std::map<const VariableDeclaration *, size_t> headVariableIDs;
|
||||||
std::map<const ast::VariableDeclaration *, size_t> bodyVariableIDs;
|
std::map<const VariableDeclaration *, size_t> bodyVariableIDs;
|
||||||
};
|
};
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
@ -425,14 +425,14 @@ struct VariantPrintVisitor
|
|||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext)
|
inline output::ColorStream &print(output::ColorStream &stream, const Formula &formula, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
return formula.accept(VariantPrintVisitor<ast::Formula>(), stream, printContext);
|
return formula.accept(VariantPrintVisitor<Formula>(), stream, printContext);
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext)
|
inline output::ColorStream &print(output::ColorStream &stream, const Term &term, PrintContext &printContext)
|
||||||
{
|
{
|
||||||
return term.accept(VariantPrintVisitor<ast::Term>(), stream, printContext);
|
return term.accept(VariantPrintVisitor<Term>(), stream, printContext);
|
||||||
}
|
}
|
||||||
|
|
||||||
////////////////////////////////////////////////////////////////////////////////////////////////////
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
Loading…
Reference in New Issue
Block a user