Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add option to preserve facts in symbol table #457

Merged
merged 1 commit into from
Oct 2, 2023
Merged

add option to preserve facts in symbol table #457

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,13 @@
* add function to change undo mode (#409)
* add function to access priorities to API (#406)
* add `Model::is_consequence` to API (#423)
* add option to preserve facts (#457)
* improve hash table performance (#441)
* fix `add_theory_atom_with_guard` in Python API
* fix AST bugs (#403)
* fix parsing of hexadecimal numbers (#421)
* fix assignment aggregates (#436)
* fix build scripts for Python 3.12 (#452)
* make sure `clingo_control_ground` is re-entrant (#418)
* update clasp and dependencies

Expand Down
16 changes: 12 additions & 4 deletions libclingo/clingo/clingocontrol.hh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ private:
// {{{1 declaration of ClingoOptions

struct ClingoOptions {
using Foobar = std::vector<Sig>;
using SigVec = std::vector<Sig>;
std::vector<std::string> defines;
Output::OutputOptions outputOptions;
Output::OutputFormat outputFormat = Output::OutputFormat::INTERMEDIATE;
Expand All @@ -97,7 +97,7 @@ struct ClingoOptions {
bool rewriteMinimize = false;
bool keepFacts = false;
bool singleShot = false;
Foobar foobar;
SigVec sigvec;
};

inline void enableAll(ClingoOptions& out, bool enable) {
Expand All @@ -124,6 +124,14 @@ inline bool parseWarning(const std::string& str, ClingoOptions& out) {
return false;
}

inline bool parsePreserveFacts(const std::string& str, ClingoOptions& out) {
if (str == "none") { out.keepFacts = false; out.outputOptions.preserveFacts = false; return true; }
if (str == "body") { out.keepFacts = true; out.outputOptions.preserveFacts = false; return true; }
if (str == "symtab") { out.keepFacts = false; out.outputOptions.preserveFacts = true; return true; }
if (str == "all") { out.keepFacts = true; out.outputOptions.preserveFacts = true; return true; }
return false;
}

inline std::vector<std::string> split(std::string const &source, char const *delimiter = " ", bool keepEmpty = false) {
std::vector<std::string> results;
size_t prev = 0;
Expand All @@ -136,15 +144,15 @@ inline std::vector<std::string> split(std::string const &source, char const *del
return results;
}

inline bool parseFoobar(const std::string& str, ClingoOptions::Foobar& foobar) {
inline bool parseSigVec(const std::string& str, ClingoOptions::SigVec& sigvec) {
for (auto &x : split(str, ",")) {
auto y = split(x, "/");
if (y.size() != 2) { return false; }
unsigned a;
if (!Potassco::string_cast<unsigned>(y[1], a)) { return false; }
bool sign = !y[0].empty() && y[0][0] == '-';
if (sign) { y[0] = y[0].substr(1); }
foobar.emplace_back(y[0].c_str(), a, sign);
sigvec.emplace_back(y[0].c_str(), a, sign);
}
return true;
}
Expand Down
23 changes: 15 additions & 8 deletions libclingo/src/clingo_app.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,19 +72,26 @@ void ClingoApp::initOptions(Potassco::ProgramOptions::OptionContext& root) {
" translate: print translated rules as plain text (prefix %%%%)\n"
" all : combines text and translate")
("warn,W,@1" , storeTo(grOpts_, parseWarning)->arg("<warn>")->composing(), "Enable/disable warnings:\n"
" none: disable all warnings\n"
" all: enable all warnings\n"
" [no-]atom-undefined: a :- b.\n"
" [no-]file-included: #include \"a.lp\". #include \"a.lp\".\n"
" none : disable all warnings\n"
" all : enable all warnings\n"
" [no-]atom-undefined : a :- b.\n"
" [no-]file-included : #include \"a.lp\". #include \"a.lp\".\n"
" [no-]operation-undefined: p(1/0).\n"
" [no-]global-variable: :- #count { X } = 1, X = 1.\n"
" [no-]other: clasp related and uncategorized warnings")
" [no-]global-variable : :- #count { X } = 1, X = 1.\n"
" [no-]other : clasp related and uncategorized warnings")
("rewrite-minimize,@1" , flag(grOpts_.rewriteMinimize = false), "Rewrite minimize constraints into rules")
("keep-facts,@1" , flag(grOpts_.keepFacts = false), "Do not remove facts from normal rules")
// for backward compatibility
("keep-facts,@3" , flag(grOpts_.keepFacts = false), "Do not remove facts from normal rules")
("preserve-facts,@1" , storeTo(grOpts_, parsePreserveFacts),
"Preserve facts in output:\n"
" none : do not preserve\n"
" body : do not preserve\n"
" symtab: do not preserve\n"
" all : preserve all facts")
("reify-sccs,@1" , flag(grOpts_.outputOptions.reifySCCs = false), "Calculate SCCs for reified output")
("reify-steps,@1" , flag(grOpts_.outputOptions.reifySteps = false), "Add step numbers to reified output")
("show-preds,@1" , storeTo(grOpts_.sigvec, parseSigVec), "Show the given signatures")
("single-shot,@2" , flag(grOpts_.singleShot = false), "Force single-shot solving mode")
("foobar,@4" , storeTo(grOpts_.foobar, parseFoobar) , "Foobar")
;
root.add(gringo);

Expand Down
34 changes: 22 additions & 12 deletions libclingo/src/clingocontrol.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,7 @@ void ClingoControl::parse(const StringVec& files, const ClingoOptions& opts, Cla
logger_.enable(Warnings::Other, !opts.wNoOther);
verbose_ = opts.verbose;
Output::OutputPredicates outPreds;
for (auto const &x : opts.foobar) {
for (auto const &x : opts.sigvec) {
outPreds.add(Location("<cmd>",1,1,"<cmd>", 1,1), x, false);
}
if (claspOut != nullptr) {
Expand Down Expand Up @@ -913,26 +913,36 @@ void ClingoLib::initOptions(Potassco::ProgramOptions::OptionContext& root) {
gringo.addOptions()
("verbose,V" , flag(grOpts_.verbose = false), "Enable verbose output")
("const,c" , storeTo(grOpts_.defines, parseConst)->composing()->arg("<id>=<term>"), "Replace term occurrences of <id> with <term>")
("output-debug", storeTo(grOpts_.outputOptions.debug = Output::OutputDebug::NONE, values<Output::OutputDebug>()
("output-debug" , storeTo(grOpts_.outputOptions.debug = Output::OutputDebug::NONE, values<Output::OutputDebug>()
("none", Output::OutputDebug::NONE)
("text", Output::OutputDebug::TEXT)
("translate", Output::OutputDebug::TRANSLATE)
("all", Output::OutputDebug::ALL)), "Print debug information during output:\n"
("all", Output::OutputDebug::ALL)),
"Print debug information during output:\n"
" none : no additional info\n"
" text : print rules as plain text (prefix %%)\n"
" translate: print translated rules as plain text (prefix %%%%)\n"
" all : combines text and translate")
("warn,W" , storeTo(grOpts_, parseWarning)->arg("<warn>")->composing(), "Enable/disable warnings:\n"
" none: disable all warnings\n"
" all: enable all warnings\n"
" [no-]atom-undefined: a :- b.\n"
" [no-]file-included: #include \"a.lp\". #include \"a.lp\".\n"
("warn,W" , storeTo(grOpts_, parseWarning)->arg("<warn>")->composing(),
"Enable/disable warnings:\n"
" none : disable all warnings\n"
" all : enable all warnings\n"
" [no-]atom-undefined : a :- b.\n"
" [no-]file-included : #include \"a.lp\". #include \"a.lp\".\n"
" [no-]operation-undefined: p(1/0).\n"
" [no-]global-variable: :- #count { X } = 1, X = 1.\n"
" [no-]other: clasp related and uncategorized warnings")
" [no-]global-variable : :- #count { X } = 1, X = 1.\n"
" [no-]other : clasp related and uncategorized warnings")
("rewrite-minimize" , flag(grOpts_.rewriteMinimize = false), "Rewrite minimize constraints into rules")
("keep-facts" , flag(grOpts_.keepFacts = false), "Do not remove facts from normal rules")
("single-shot,@2" , flag(grOpts_.singleShot = false), "Force single-shot solving mode")
// for backward compatibility
("keep-facts" , flag(grOpts_.keepFacts = false), "Preserve facts in rule bodies")
("preserve-facts" , storeTo(grOpts_, parsePreserveFacts),
"Preserve facts in output:\n"
" none : do not preserve\n"
" body : do not preserve\n"
" symtab: do not preserve\n"
" all : preserve all facts")
("single-shot" , flag(grOpts_.singleShot = false), "Force single-shot solving mode")
("show-preds" , storeTo(grOpts_.sigvec, parseSigVec), "Show the given signatures")
;
root.add(gringo);
claspConfig_.addOptions(root);
Expand Down
41 changes: 28 additions & 13 deletions libclingo/src/gringo_app.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ namespace Gringo {
using StrVec = std::vector<std::string>;

struct GringoOptions {
using Foobar = std::vector<Sig>;
using SigVec = std::vector<Sig>;
StrVec defines;
Output::OutputOptions outputOptions;
Output::OutputFormat outputFormat = Output::OutputFormat::INTERMEDIATE;
Expand All @@ -59,7 +59,7 @@ struct GringoOptions {
bool rewriteMinimize = false;
bool keepFacts = false;
bool singleShot = false;
Foobar foobar;
SigVec sigvec;
};

static inline std::vector<std::string> split(std::string const &source, char const *delimiter = " ", bool keepEmpty = false) {
Expand All @@ -74,15 +74,15 @@ static inline std::vector<std::string> split(std::string const &source, char con
return results;
}

static inline bool parseFoobar(const std::string& str, GringoOptions::Foobar& foobar) {
static inline bool parseSigVec(const std::string& str, GringoOptions::SigVec& sigvec) {
for (auto &x : split(str, ",")) {
auto y = split(x, "/");
if (y.size() != 2) { return false; }
unsigned a;
if (!Potassco::string_cast<unsigned>(y[1], a)) { return false; }
bool sign = !y[0].empty() && y[0][0] == '-';
if (sign) { y[0] = y[0].substr(1); }
foobar.emplace_back(y[0].c_str(), a, sign);
sigvec.emplace_back(y[0].c_str(), a, sign);
}
return true;
}
Expand Down Expand Up @@ -341,6 +341,14 @@ inline bool parseWarning(const std::string& str, GringoOptions& out) {
return false;
}

inline bool parsePreserveFacts(const std::string& str, GringoOptions& out) {
if (str == "none") { out.keepFacts = false; out.outputOptions.preserveFacts = false; return true; }
if (str == "body") { out.keepFacts = true; out.outputOptions.preserveFacts = false; return true; }
if (str == "symtab") { out.keepFacts = false; out.outputOptions.preserveFacts = true; return true; }
if (str == "all") { out.keepFacts = true; out.outputOptions.preserveFacts = true; return true; }
return false;
}

static bool parseText(const std::string&, GringoOptions& out) {
out.outputFormat = Output::OutputFormat::TEXT;
return true;
Expand Down Expand Up @@ -379,19 +387,26 @@ struct GringoApp : public Potassco::Application {
" translate: print translated rules as plain text (prefix %%%%)\n"
" all : combines text and translate")
("warn,W,@1", storeTo(grOpts_, parseWarning)->arg("<warn>")->composing(), "Enable/disable warnings:\n"
" none: disable all warnings\n"
" all: enable all warnings\n"
" [no-]atom-undefined: a :- b.\n"
" [no-]file-included: #include \"a.lp\". #include \"a.lp\".\n"
" none : disable all warnings\n"
" all : enable all warnings\n"
" [no-]atom-undefined : a :- b.\n"
" [no-]file-included : #include \"a.lp\". #include \"a.lp\".\n"
" [no-]operation-undefined: p(1/0).\n"
" [no-]global-variable: :- #count { X } = 1, X = 1.\n"
" [no-]other: uncategorized warnings")
" [no-]global-variable : :- #count { X } = 1, X = 1.\n"
" [no-]other : uncategorized warnings")
("rewrite-minimize,@1", flag(grOpts_.rewriteMinimize = false), "Rewrite minimize constraints into rules")
("keep-facts,@1", flag(grOpts_.keepFacts = false), "Do not remove facts from normal rules")
// for backward compatibility
("keep-facts,@4", flag(grOpts_.keepFacts = false), "Preserve facts in rule bodies.")
("preserve-facts,@1", storeTo(grOpts_, parsePreserveFacts),
"Preserve facts in output:\n"
" none : do not preserve\n"
" body : do not preserve\n"
" symtab: do not preserve\n"
" all : preserve all facts")
("reify-sccs,@1", flag(grOpts_.outputOptions.reifySCCs = false), "Calculate SCCs for reified output")
("reify-steps,@1", flag(grOpts_.outputOptions.reifySteps = false), "Add step numbers to reified output")
("show-preds,@1", storeTo(grOpts_.sigvec, parseSigVec), "Show the given signatures")
("single-shot,@2", flag(grOpts_.singleShot = false), "Force single-shot grounding mode")
("foobar,@4", storeTo(grOpts_.foobar, parseFoobar), "Foobar")
;
root.add(gringo);
OptionGroup basic("Basic Options");
Expand Down Expand Up @@ -456,7 +471,7 @@ struct GringoApp : public Potassco::Application {
using namespace Gringo;
grOpts_.verbose = verbose() == UINT_MAX;
Output::OutputPredicates outPreds;
for (auto &x : grOpts_.foobar) {
for (auto &x : grOpts_.sigvec) {
outPreds.add(Location("<cmd>",1,1,"<cmd>", 1,1), x, false);
}
Potassco::TheoryData data;
Expand Down
9 changes: 5 additions & 4 deletions libgringo/gringo/output/output.hh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ namespace Gringo { namespace Output {

class TranslatorOutput : public AbstractOutput {
public:
TranslatorOutput(UAbstractOutput out);
TranslatorOutput(UAbstractOutput out, bool preserveFacts);
void output(DomainData &data, Statement &stm) override;
private:
Translator trans_;
Expand All @@ -60,9 +60,10 @@ private:
};

struct OutputOptions {
OutputDebug debug = OutputDebug::NONE;
bool reifySCCs = false;
bool reifySteps = false;
OutputDebug debug = OutputDebug::NONE;
bool reifySCCs = false;
bool reifySteps = false;
bool preserveFacts = false;
};

class OutputPredicates {
Expand Down
3 changes: 2 additions & 1 deletion libgringo/gringo/output/statements.hh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,7 @@ public:
using ProjectionVec = std::vector<std::pair<Potassco::Id_t, Potassco::Id_t>>;
using TupleLitMap = ordered_map<TupleId, LiteralId>;

Translator(UAbstractOutput out);
Translator(UAbstractOutput out, bool preserveFacts);

void addMinimize(TupleId tuple, LiteralId cond);
void atoms(DomainData &data, unsigned atomset, IsTrueLookup const &isTrue, SymVec &atoms, OutputPredicates const &outPreds);
Expand Down Expand Up @@ -282,6 +282,7 @@ private:
static constexpr ClauseKey deleted = { 0xffffffff, 0x3fffffff, 1, 1, std::numeric_limits<uint64_t>::max() - 1 };
};
hash_set<ClauseKey, CallHash> clauses_;
bool preserveFacts_;
};

// {{{1 declaration of Minimize
Expand Down
7 changes: 4 additions & 3 deletions libgringo/src/output/output.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -398,8 +398,8 @@ class BackendTee : public Backend {

// {{{1 definition of TranslatorOutput

TranslatorOutput::TranslatorOutput(UAbstractOutput out)
: trans_(std::move(out)) { }
TranslatorOutput::TranslatorOutput(UAbstractOutput out, bool preserveFacts)
: trans_(std::move(out), preserveFacts) { }

void TranslatorOutput::output(DomainData &data, Statement &stm) {
stm.translate(data, trans_);
Expand Down Expand Up @@ -484,7 +484,7 @@ UAbstractOutput OutputBase::fromBackend(UBackend out, OutputOptions opts) {
if (opts.debug == OutputDebug::TRANSLATE || opts.debug == OutputDebug::ALL) {
output = gringo_make_unique<TextOutput>("%% ", std::cerr, std::move(output));
}
output = gringo_make_unique<TranslatorOutput>(std::move(output));
output = gringo_make_unique<TranslatorOutput>(std::move(output), opts.preserveFacts);
if (opts.debug == OutputDebug::TEXT || opts.debug == OutputDebug::ALL) {
output = gringo_make_unique<TextOutput>("% ", std::cerr, std::move(output));
}
Expand Down Expand Up @@ -641,6 +641,7 @@ void OutputBase::registerObserver(UBackend prg, bool replace) {
void ASPIFOutBackend::initProgram(bool incremental) {
static_cast<void>(incremental);
}

void ASPIFOutBackend::beginStep() {
out_ = &beginOutput();
bck_ = out_->backend();
Expand Down
12 changes: 7 additions & 5 deletions libgringo/src/output/statements.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -429,8 +429,9 @@ void WeakConstraint::replaceDelayed(DomainData &data, LitVec &delayed) {

// {{{1 definition of Translator

Translator::Translator(UAbstractOutput out)
Translator::Translator(UAbstractOutput out, bool preserveFacts)
: out_(std::move(out))
, preserveFacts_{preserveFacts}
{ }

void Translator::addMinimize(TupleId tuple, LiteralId cond) {
Expand Down Expand Up @@ -548,12 +549,12 @@ namespace {

class Atomtab : public Statement {
public:
Atomtab(PredicateDomain::Iterator atom)
: atom_(atom) { }
Atomtab(PredicateDomain::Iterator atom, bool preserveFacts)
: atom_(atom), preserveFacts_{preserveFacts} { }

void output(DomainData &data, UBackend &out) const override {
static_cast<void>(data);
out->output(*atom_, atom_->fact() ? 0 : atom_->uid());
out->output(*atom_, !preserveFacts_ && atom_->fact() ? 0 : atom_->uid());
}

void print(PrintPlain out, char const *prefix) const override {
Expand All @@ -578,14 +579,15 @@ class Atomtab : public Statement {

private:
PredicateDomain::Iterator atom_;
bool preserveFacts_;
};

} // namespace

void Translator::showAtom(DomainData &data, PredDomMap::iterator it) {
for (auto jt = (*it)->begin() + (*it)->showOffset(), je = (*it)->end(); jt != je; ++jt) {
if (jt->defined()) {
Atomtab(jt).translate(data, *this);
Atomtab{jt, preserveFacts_}.translate(data, *this);
}
}
(*it)->showNext();
Expand Down