Merge pull request #457 from potassco/feature/preserve-facts

add option to preserve facts in symbol table

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
 

libclingo/clingo/clingocontrol.hh

@@ -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;
@@ -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<std::string> split(std::string const &source, char const *delimiter = " ", bool keepEmpty = false) {
     std::vector<std::string> results;
     size_t prev = 0;
@@ -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;
 }

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("<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);
 

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("<cmd>",1,1,"<cmd>", 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("<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);

libclingo/src/gringo_app.cc

@@ -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;
@@ -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) {
@@ -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;
 }
@@ -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("<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");
@@ -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;

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 {

libgringo/gringo/output/statements.hh

@@ -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);
@@ -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

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<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));
     }
@@ -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();

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<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 {
@@ -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();