diff --git a/include/anthem/Completion.h b/include/anthem/Completion.h new file mode 100644 index 0000000..b777a48 --- /dev/null +++ b/include/anthem/Completion.h @@ -0,0 +1,21 @@ +#ifndef __ANTHEM__COMPLETION_H +#define __ANTHEM__COMPLETION_H + +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Completion +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void complete(std::vector &formulas); + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} + +#endif diff --git a/src/anthem/Completion.cpp b/src/anthem/Completion.cpp new file mode 100644 index 0000000..dce67bb --- /dev/null +++ b/src/anthem/Completion.cpp @@ -0,0 +1,30 @@ +#include + +#include + +namespace anthem +{ + +//////////////////////////////////////////////////////////////////////////////////////////////////// +// +// Completion +// +//////////////////////////////////////////////////////////////////////////////////////////////////// + +void complete(std::vector &formulas) +{ + for (auto &formula : formulas) + { + if (!formula.is()) + throw std::runtime_error("cannot perform completion, formula not in normal form"); + + auto &implies = formula.get(); + + if (!implies.consequent.is()) + throw std::runtime_error("cannot perform completion, only single predicates supported as formula consequent currently"); + } +} + +//////////////////////////////////////////////////////////////////////////////////////////////////// + +} diff --git a/src/anthem/Translation.cpp b/src/anthem/Translation.cpp index 432eb52..7537962 100644 --- a/src/anthem/Translation.cpp +++ b/src/anthem/Translation.cpp @@ -6,6 +6,7 @@ #include +#include #include #include #include @@ -55,6 +56,9 @@ void translate(const char *fileName, std::istream &stream, Context &context) Clingo::parse_program(fileContent.c_str(), translateStatement, logger); + if (context.complete) + complete(formulas); + for (auto i = formulas.begin(); i != formulas.end(); i++) { auto &formula = *i;