Added scaffold for implementing completion.
This commit is contained in:
parent
838a68e230
commit
27b46ceee1
21
include/anthem/Completion.h
Normal file
21
include/anthem/Completion.h
Normal file
@ -0,0 +1,21 @@
|
|||||||
|
#ifndef __ANTHEM__COMPLETION_H
|
||||||
|
#define __ANTHEM__COMPLETION_H
|
||||||
|
|
||||||
|
#include <anthem/AST.h>
|
||||||
|
|
||||||
|
namespace anthem
|
||||||
|
{
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
//
|
||||||
|
// Completion
|
||||||
|
//
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
void complete(std::vector<ast::Formula> &formulas);
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
#endif
|
30
src/anthem/Completion.cpp
Normal file
30
src/anthem/Completion.cpp
Normal file
@ -0,0 +1,30 @@
|
|||||||
|
#include <anthem/Completion.h>
|
||||||
|
|
||||||
|
#include <anthem/ASTVisitors.h>
|
||||||
|
|
||||||
|
namespace anthem
|
||||||
|
{
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
//
|
||||||
|
// Completion
|
||||||
|
//
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
void complete(std::vector<ast::Formula> &formulas)
|
||||||
|
{
|
||||||
|
for (auto &formula : formulas)
|
||||||
|
{
|
||||||
|
if (!formula.is<ast::Implies>())
|
||||||
|
throw std::runtime_error("cannot perform completion, formula not in normal form");
|
||||||
|
|
||||||
|
auto &implies = formula.get<ast::Implies>();
|
||||||
|
|
||||||
|
if (!implies.consequent.is<ast::Predicate>())
|
||||||
|
throw std::runtime_error("cannot perform completion, only single predicates supported as formula consequent currently");
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
////////////////////////////////////////////////////////////////////////////////////////////////////
|
||||||
|
|
||||||
|
}
|
@ -6,6 +6,7 @@
|
|||||||
|
|
||||||
#include <clingo.hh>
|
#include <clingo.hh>
|
||||||
|
|
||||||
|
#include <anthem/Completion.h>
|
||||||
#include <anthem/Context.h>
|
#include <anthem/Context.h>
|
||||||
#include <anthem/Simplification.h>
|
#include <anthem/Simplification.h>
|
||||||
#include <anthem/StatementVisitor.h>
|
#include <anthem/StatementVisitor.h>
|
||||||
@ -55,6 +56,9 @@ void translate(const char *fileName, std::istream &stream, Context &context)
|
|||||||
|
|
||||||
Clingo::parse_program(fileContent.c_str(), translateStatement, logger);
|
Clingo::parse_program(fileContent.c_str(), translateStatement, logger);
|
||||||
|
|
||||||
|
if (context.complete)
|
||||||
|
complete(formulas);
|
||||||
|
|
||||||
for (auto i = formulas.begin(); i != formulas.end(); i++)
|
for (auto i = formulas.begin(); i != formulas.end(); i++)
|
||||||
{
|
{
|
||||||
auto &formula = *i;
|
auto &formula = *i;
|
||||||
|
Loading…
Reference in New Issue
Block a user