diff --git a/CHANGES.md b/CHANGES.md index 088e2e19b..52064a444 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -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 diff --git a/libclingo/clingo/clingocontrol.hh b/libclingo/clingo/clingocontrol.hh index ffb336ab6..324c055ca 100644 --- a/libclingo/clingo/clingocontrol.hh +++ b/libclingo/clingo/clingocontrol.hh @@ -84,7 +84,7 @@ private: // {{{1 declaration of ClingoOptions struct ClingoOptions { - using Foobar = std::vector; + using SigVec = std::vector; std::vector defines; Output::OutputOptions outputOptions; Output::OutputFormat outputFormat = Output::OutputFormat::INTERMEDIATE; @@ -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) { @@ -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 split(std::string const &source, char const *delimiter = " ", bool keepEmpty = false) { std::vector results; size_t prev = 0; @@ -136,7 +144,7 @@ inline std::vector 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; } @@ -144,7 +152,7 @@ inline bool parseFoobar(const std::string& str, ClingoOptions::Foobar& foobar) { if (!Potassco::string_cast(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; } diff --git a/libclingo/src/clingo_app.cc b/libclingo/src/clingo_app.cc index 13980efa6..2fa0d2dc4 100644 --- a/libclingo/src/clingo_app.cc +++ b/libclingo/src/clingo_app.cc @@ -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("")->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); diff --git a/libclingo/src/clingocontrol.cc b/libclingo/src/clingocontrol.cc index f6728fefc..43a6d6e5c 100644 --- a/libclingo/src/clingocontrol.cc +++ b/libclingo/src/clingocontrol.cc @@ -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("",1,1,"", 1,1), x, false); } if (claspOut != nullptr) { @@ -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("="), "Replace term occurrences of with ") - ("output-debug", storeTo(grOpts_.outputOptions.debug = Output::OutputDebug::NONE, values() + ("output-debug" , storeTo(grOpts_.outputOptions.debug = Output::OutputDebug::NONE, values() ("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("")->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("")->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); diff --git a/libclingo/src/gringo_app.cc b/libclingo/src/gringo_app.cc index 86ea81cbe..74eea9eb9 100644 --- a/libclingo/src/gringo_app.cc +++ b/libclingo/src/gringo_app.cc @@ -46,7 +46,7 @@ namespace Gringo { using StrVec = std::vector; struct GringoOptions { - using Foobar = std::vector; + using SigVec = std::vector; StrVec defines; Output::OutputOptions outputOptions; Output::OutputFormat outputFormat = Output::OutputFormat::INTERMEDIATE; @@ -59,7 +59,7 @@ struct GringoOptions { bool rewriteMinimize = false; bool keepFacts = false; bool singleShot = false; - Foobar foobar; + SigVec sigvec; }; static inline std::vector split(std::string const &source, char const *delimiter = " ", bool keepEmpty = false) { @@ -74,7 +74,7 @@ static inline std::vector 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; } @@ -82,7 +82,7 @@ static inline bool parseFoobar(const std::string& str, GringoOptions::Foobar& fo if (!Potassco::string_cast(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; } @@ -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; @@ -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("")->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"); @@ -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("",1,1,"", 1,1), x, false); } Potassco::TheoryData data; diff --git a/libgringo/gringo/output/output.hh b/libgringo/gringo/output/output.hh index f83b7907c..9bd64f3fb 100644 --- a/libgringo/gringo/output/output.hh +++ b/libgringo/gringo/output/output.hh @@ -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_; @@ -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 { diff --git a/libgringo/gringo/output/statements.hh b/libgringo/gringo/output/statements.hh index 8d898e97e..bd1e53551 100644 --- a/libgringo/gringo/output/statements.hh +++ b/libgringo/gringo/output/statements.hh @@ -228,7 +228,7 @@ public: using ProjectionVec = std::vector>; using TupleLitMap = ordered_map; - 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); @@ -282,6 +282,7 @@ private: static constexpr ClauseKey deleted = { 0xffffffff, 0x3fffffff, 1, 1, std::numeric_limits::max() - 1 }; }; hash_set clauses_; + bool preserveFacts_; }; // {{{1 declaration of Minimize diff --git a/libgringo/src/output/output.cc b/libgringo/src/output/output.cc index f479d8302..20ffd3bcc 100644 --- a/libgringo/src/output/output.cc +++ b/libgringo/src/output/output.cc @@ -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_); @@ -484,7 +484,7 @@ UAbstractOutput OutputBase::fromBackend(UBackend out, OutputOptions opts) { if (opts.debug == OutputDebug::TRANSLATE || opts.debug == OutputDebug::ALL) { output = gringo_make_unique("%% ", std::cerr, std::move(output)); } - output = gringo_make_unique(std::move(output)); + output = gringo_make_unique(std::move(output), opts.preserveFacts); if (opts.debug == OutputDebug::TEXT || opts.debug == OutputDebug::ALL) { output = gringo_make_unique("% ", std::cerr, std::move(output)); } @@ -641,6 +641,7 @@ void OutputBase::registerObserver(UBackend prg, bool replace) { void ASPIFOutBackend::initProgram(bool incremental) { static_cast(incremental); } + void ASPIFOutBackend::beginStep() { out_ = &beginOutput(); bck_ = out_->backend(); diff --git a/libgringo/src/output/statements.cc b/libgringo/src/output/statements.cc index d1213f2ac..342daba82 100644 --- a/libgringo/src/output/statements.cc +++ b/libgringo/src/output/statements.cc @@ -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) { @@ -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(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 { @@ -578,6 +579,7 @@ class Atomtab : public Statement { private: PredicateDomain::Iterator atom_; + bool preserveFacts_; }; } // namespace @@ -585,7 +587,7 @@ class Atomtab : public Statement { 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();