clasplayer.cpp
No OneTemporary

File Metadata

Created
Thu, Jul 9, 1:27 AM

clasplayer.cpp

#include "clasplayer.h"
#include <clasp/program_builder.h> // for defining logic programs
#include <clasp/unfounded_check.h> // unfounded set checkers
#include <clasp/model_enumerators.h> // for enumerating answer sets
#include <clasp/clasp_facade.h>
#include <clingocontrol.hh>
#include <iostream>
#include <clingo_lib.hh>
#include <QString>
#include <QStringList>
using namespace std;
bool
ClaspLayer::onModel(Gringo::Model const & model)
{
cout << "Model: " << endl;
for (Gringo::Value atom : model.atoms(Gringo::Model::ATOMS))
{
atom.print(cout);
cout << endl;
}
}
QStringList multiplyLists(std::list<QStringList>&& lists)
{
QStringList&& result = lists.front();
lists.pop_front();
for (QStringList& list: lists)
{
QStringList::const_iterator end = result.end();
for (QStringList::iterator expr1I=result.begin(); expr1I<end; ++expr1I)
{
if (list.size() == 0 ) continue;
StringList::const_iterator expr2I=list.begin();
for(int expr2No=0, size = list.size()-1; expr2No < size; ++expr2No, ++expr1I)
result.append(QString("%1, %2").arg(*expr1I).arg(*expr2I));
*expr1I = QString("%1, %2").arg(*expr1I).arg(*expr2I);
}
}
return result;
}
void
ClaspLayer::addCFGData(CFGraph &&graph)
{
ostream& cout = __partGeneral;
cout <<endl<< "%\t\tStatic analysis: CFG" << endl;
for (const std::pair<FID, FID>& relation: graph.__relations)
{
const string& tagFrom = graph.__nodes.at(relation.first);
const string& tagTo = graph.__nodes.at(relation.second);
cout << (QString("call(%1, %2) .").arg(tagFrom.c_str()).arg(tagTo.c_str())).toStdString()<<endl;
}
}
void
ClaspLayer::addFunctionTags(const std::string& function, const std::vector<Tag>& tags)
{
ostream& cout = __partTags;
cout << (QString("function(%1) .").arg(function.c_str())).toStdString()<<std::endl;
int tagsCount=0;
for(Tag tag: tags)
{
cout << QString("tag(%1, %2).").arg(function.c_str()).arg(tag.first.c_str()).toStdString() << endl;
++tagsCount;
}
if (tagsCount == 0)
{
cout << "%no tags at all" << endl;
}
}
void
ClaspLayer::addRuleWarning(RuleWarning* rule)
{
//__partGeneral << rule << endl;
std::QStringList domains;
std::transform(rule->__args.begin(), rule->__args.end(), std::inserter(domains, domains.begin()),
[](const auto& argument) {
char* domain;
switch (argument.second)
{ case DomainAnnotation::FUNCTION:
domain = "function";
break;
case DomainAnnotation::VARIABLE:
domain = "variable";
break;
}
return QString("%1(%2)").arg(domain).arg(argument.first.c_str());
});
std::QStringList vars;
std::transform(rule->__args.begin(), rule->__args.end(), std::inserter(vars, vars.begin()),
[](const auto& argument) {
return argument.first.c_str();
});
std::QStringList guards;
std::transform(rule->__guards.begin(), rule->__guards.end(), std::inserter(guards, guards.begin()),
[](const MetaExpression& guard) {
return compile(guard)._c_str();
});
QStringList&& branches = compileNeg(rule->__condition);
for(const std::string& branch: branches)
{
std::string listener = registerListener(rule->__message);
result = QString("%1(%2):-%3, %4, %5")
.arg(listener.c_str())
.arg(vars.join(", "))
.arg(branch.c_str())
.arg(guards.join(", "))
.arg(domains.join(", "));
__partGeneral<< result << endl;
}
}
QStringList
ClaspLayer::compile(const Expression& e) const
{
QStringList result;
switch(e.__op)
{
case Operator::CALL:
assert(e.__state == COMPOUND);
std::list<QStringList> operands;
std::transform(e.operands.begin(), e.operands.end(), std::inserter(operands, operands().begin()),
[](const Expression& e) {return compile(e);});
QStringList&& operands_ = multiplyLists(operands);
result.append(QString("%1(%2)").arg(e.__valueS.c_str()).arg(operands_.join(", ")));
break;
case Operator::NONE:
switch (e.__state)
{
case Expression::IDENT:
result.append(e.__valueS);
break;
case Expression::NUMBER:
result.append(e.__valueD);
break;
default:
assert(true);
}
break;
}
return result;
}
QStringList compileNeg(const Expression& e) const
{
QStringList result;
switch(__op)
{
case Operator::IMPL:
assert(e.__state == COMPOUND);
assert(e.operands.size() == 2);
QStringList operands1 = compile(e.operands.at(0));
QStringList operands2 = compile(e.operands.at(1));
for (const auto& op1: operands1)
for (const auto& op2: operands2)
{
result.append(QString("%1, not %2").arg(op1).arg(op2));
}
break;
default:
assert(true);
}
return result;
}
void
ClaspLayer::run()
{
ostringstream program;
program << __partTags.str() << __partGeneral.str();
cout << program.str() << endl;
const char* argv[] = {nullptr, nullptr};
ClingoLib ctl(2, argv);
//prg.add("p", ["t"], "q(t).")
Gringo::FWStringVec vars{};
ctl.add("base", vars, program.str());
//prg.ground([("p", [2])])
Gringo::Control::GroundVec vals{std::make_pair("base", Gringo::FWValVec {})};
ctl.ground(vals, Gringo::Any());
//solve
Gringo::Control::Assumptions as;
Gringo::SolveResult result = ctl.solve(Gringo::Control::ModelHandler([&](Gringo::Model const &model){return this->onModel(model);}), std::move(as));
if (result == Gringo::SolveResult::SAT)
{
cout << "SUCCESSFULLY" << endl;
} else {
cout << "UNSUCCESSFULLY" << endl;
}
}
ClaspLayer::ClaspLayer()
{}
/*
void AspOutPrinter::reportSolution(const Clasp::Solver&, const Clasp::Enumerator&, bool complete) {
if (complete) std::cout << "No more models!" << std::endl;
else std::cout << "More models possible!" << std::endl;
}
void AspOutPrinter::reportModel(const Clasp::Solver& s, const Clasp::Enumerator&) {
std::cout << "Model " << s.stats.solve.models << ": \n";
// get the symbol table from the solver
const Clasp::AtomIndex& symTab = *s.strategies().symTab;
for (Clasp::AtomIndex::const_iterator it = symTab.begin(); it != symTab.end(); ++it)
{
// print each named atom that is true w.r.t the current assignment
}
std::cout << std::endl;
}
*/
/*****************************************
* CFGraph
*****************************************
*/
void
CFGraph::addNode(FID function, std::string&& tag)
{
__nodes.insert(make_pair(function, move(tag)));
}
bool
CFGraph::existsNode(FID function) const
{
return __nodes.count(function);
}
void
CFGraph::addLink(FID nodeFrom, FID nodeTo)
{
assert(__nodes.count(nodeFrom));
assert(__nodes.count(nodeTo));
__relations.insert(std::make_pair(nodeFrom, nodeTo));
}

Event Timeline