Skip to content

Commit

Permalink
Adjust show handling in text output.
Browse files Browse the repository at this point in the history 
* Add "#show." whenever the output contains a generated atom name.
* Use (<s>:<a>) from an output statement as name for atom <a> only if
  <s> is not reserved (i.e. 'x_<id>') and the mapping is unique, i.e.
  there is no other output statement with <a> as condition.
* Require uniqueness of theory atoms.
  • Loading branch information
@BenKaufmann
BenKaufmann committed May 29, 2024
1 parent 33f38b2 commit 10ed000
Show file tree
Hide file tree
Showing 3 changed files with 230 additions and 43 deletions.
5 changes: 4 additions & 1 deletion potassco/aspif_text.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,7 +101,7 @@ class AspifTextOutput : public Potassco::AbstractProgram {

void addAtom(Atom_t id, const StringSpan& str);
private:
std::ostream& printName(std::ostream& os, Lit_t lit) const;
std::ostream& printName(std::ostream& os, Lit_t lit);
void writeDirectives();
void visitTheories();
AspifTextOutput& push(uint32_t x);
Expand All @@ -116,6 +116,9 @@ class AspifTextOutput : public Potassco::AbstractProgram {
TheoryData theory_;
Data* data_;
int step_;
int showAtoms_;
Atom_t startAtom_;
Atom_t maxAtom_;
};

//! Converts a given theory atom to a string.
Expand Down
77 changes: 63 additions & 14 deletions src/aspif_text.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -301,6 +301,7 @@ struct AspifTextOutput::Data {
typedef std::vector<Id_t> AtomMap;
typedef std::vector<Lit_t> LitVec;
typedef std::vector<uint32_t> RawVec;
enum { genNameId = idMax - 1 };
LitSpan getCondition(Id_t id) const {
return toSpan(&conditions[id + 1], static_cast<size_t>(conditions[id]));
}
Expand All @@ -317,14 +318,21 @@ struct AspifTextOutput::Data {
strings.push_back(std::string(Potassco::begin(str), Potassco::end(str)));
return id;
}
Id_t getAtomNameId(Atom_t atom) const {
return atom < atoms.size() ? atoms[atom] : idMax;
}
const std::string* getAtomName(Atom_t atom) const {
Id_t id = getAtomNameId(atom);
return id < strings.size() ? &strings[id] : 0;
}
RawVec directives;
StringVec strings;
AtomMap atoms; // maps into strings
LitVec conditions;
uint32_t readPos;
void reset() { directives.clear(); strings.clear(); atoms.clear(); conditions.clear(); readPos = 0; }
};
AspifTextOutput::AspifTextOutput(std::ostream& os) : os_(os), step_(-1) {
AspifTextOutput::AspifTextOutput(std::ostream& os) : os_(os), step_(-1), showAtoms_(0), startAtom_(0), maxAtom_(0) {
data_ = new Data();
}
AspifTextOutput::~AspifTextOutput() {
Expand All @@ -334,19 +342,26 @@ void AspifTextOutput::addAtom(Atom_t id, const StringSpan& str) {
if (id >= data_->atoms.size()) { data_->atoms.resize(id + 1, idMax); }
data_->atoms[id] = data_->addString(str);
}
std::ostream& AspifTextOutput::printName(std::ostream& os, Lit_t lit) const {
std::ostream& AspifTextOutput::printName(std::ostream& os, Lit_t lit) {
if (lit < 0) { os << "not "; }
Atom_t id = Potassco::atom(lit);
if (id < data_->atoms.size() && data_->atoms[id] < data_->strings.size()) {
os << data_->strings[data_->atoms[id]];
if (const std::string* name = data_->getAtomName(id)) {
os << *name;
}
else {
os << "x_" << id;
if (showAtoms_ == 0) {
showAtoms_ = 1;
}
}
maxAtom_ = std::max(maxAtom_, id);
return os;
}
void AspifTextOutput::initProgram(bool incremental) {
step_ = incremental ? 0 : -1;
step_ = incremental ? 0 : -1;
showAtoms_ = 0;
startAtom_ = 0;
maxAtom_ = 0;
data_->reset();
}
void AspifTextOutput::beginStep() {
Expand Down Expand Up @@ -386,6 +401,11 @@ void AspifTextOutput::minimize(Weight_t prio, const WeightLitSpan& lits) {
}
static bool isAtom(const StringSpan& s) {
std::size_t sz = size(s);
if (sz > 2 && s[0] == 'x' && s[1] == '_') {
const char* x = s.first + 2;
for (const char *end = Potassco::end(s); x != end && BufferedStream::isDigit(*x); ++x) { ; }
return x != Potassco::end(s);
}
char first = sz > 0 ? s[0] : char(0);
if (first == '-' && sz > 1) {
first = s[1];
Expand All @@ -394,12 +414,23 @@ static bool isAtom(const StringSpan& s) {
}

void AspifTextOutput::output(const StringSpan& str, const LitSpan& cond) {
if (size(cond) == 1 && lit(*begin(cond)) > 0 && isAtom(str)) {
addAtom(Potassco::atom(*begin(cond)), str);
}
else {
push(Directive_t::Output).push(data_->addString(str)).push(cond);
if (size(cond) == 1 && *begin(cond) > maxAtom_ && isAtom(str)) {
Atom_t atom = Potassco::atom(*begin(cond));
Id_t nameId = data_->getAtomNameId(atom);
if (nameId == idMax) {
addAtom(atom, str);
return;
}
if (nameId != Data::genNameId) {
const std::string& curr = data_->strings.at(nameId);
if (curr.size() == Potassco::size(str) && std::equal(curr.begin(), curr.end(), Potassco::begin(str))) {
return; // ignore duplicate string
}
data_->atoms[atom] = Data::genNameId;
push(Directive_t::Output).push(nameId).push(cond);
}
}
push(Directive_t::Output).push(data_->addString(str)).push(cond);
}
void AspifTextOutput::external(Atom_t a, Value_t v) {
push(Directive_t::External).push(a).push(static_cast<uint32_t>(v));
Expand Down Expand Up @@ -545,6 +576,21 @@ void AspifTextOutput::writeDirectives() {
}
os_ << term << "\n";
}
if (showAtoms_) {
if (showAtoms_ == 1) {
os_ << "#show.\n";
showAtoms_ = 2;
}
for (Atom_t a = startAtom_; a < data_->atoms.size(); ++a) {
if (const std::string* n = data_->getAtomName(a)) {
if (*n->c_str() != '&') {
os_ << "#show " << *n << " : " << *n << ".\n";
}
}
}
startAtom_ = data_->atoms.size();
}
os_ << std::flush;
}
void AspifTextOutput::visitTheories() {
struct BuildStr : public TheoryAtomStringBuilder {
Expand All @@ -553,8 +599,8 @@ void AspifTextOutput::visitTheories() {
return self->data_->getCondition(condId);
}
virtual std::string getName(Atom_t id) const {
if (id < self->data_->atoms.size() && self->data_->atoms[id] < self->data_->strings.size()) {
return self->data_->strings[self->data_->atoms[id]];
if (const std::string* name = self->data_->getAtomName(id)) {
return *name;
}
return std::string("x_").append(Potassco::toString(id));
}
Expand All @@ -567,8 +613,11 @@ void AspifTextOutput::visitTheories() {
os_ << name << ".\n";
}
else {
POTASSCO_REQUIRE(atom >= data_->atoms.size() || data_->atoms[atom] == idMax,
"Redefinition: theory atom '%u' already shown as '%s'", atom, data_->strings[data_->atoms[atom]].c_str());
POTASSCO_REQUIRE(atom > maxAtom_, "Redefinition: theory atom '%u:%s' already defined in a previous step", atom, name.c_str());
if (const std::string* p = data_->getAtomName(atom)) {
POTASSCO_REQUIRE(p->at(0) != '&', "Redefinition: theory atom '%u' already shown as '%s'", atom, p->c_str());
push(Directive_t::Output).push(data_->atoms[atom]).push(1).push(atom);
}
addAtom(atom, toSpan(name));
}
}
Expand Down
Loading

0 comments on commit 10ed000

Please sign in to comment.