add single-shot solving option

potassco · Feb 14, 2021 · 98580d5 · 98580d5
1 parent 635b1cb
commit 98580d5
Show file tree

Hide file tree

Showing 5 changed files with 17 additions and 11 deletions.
diff --git a/clasp b/clasp
diff --git a/libclingo/clingo/clingocontrol.hh b/libclingo/clingo/clingocontrol.hh
@@ -97,6 +97,7 @@ struct ClingoOptions {
     bool                          wNoOther              = false;
     bool                          rewriteMinimize       = false;
     bool                          keepFacts             = false;
+    bool                          singleShot            = false;
     Foobar                        foobar;
 };
 
@@ -386,7 +387,6 @@ public:
     bool                                                       verbose_               = false;
     bool                                                       parsed                 = false;
     bool                                                       grounded               = false;
-    bool                                                       incremental_           = true;
     bool                                                       configUpdate_          = false;
     bool                                                       initialized_           = false;
     bool                                                       incmode_               = false;

diff --git a/libclingo/src/clingo_app.cc b/libclingo/src/clingo_app.cc
@@ -85,6 +85,7 @@ void ClingoApp::initOptions(Potassco::ProgramOptions::OptionContext& root) {
         ("keep-facts,@1"            , flag(grOpts_.keepFacts = false), "Do not remove facts from normal rules")
         ("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")
+        ("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
@@ -203,7 +203,7 @@ bool ClingoControl::update() {
     }
     if (!grounded) {
         if (!initialized_) {
-            out_->init(incremental_);
+            out_->init(clasp_->incremental());
             initialized_ = true;
         }
         out_->beginStep();
@@ -241,24 +241,25 @@ void ClingoControl::ground(Control::GroundVec const &parts, Context *context) {
 }
 
 void ClingoControl::main(IClingoApp &app, StringVec const &files, const ClingoOptions& opts, Clasp::Asp::LogicProgram* out) {
-    incremental_ = true;
     if (app.has_main()) {
         parse({}, opts, out, false);
-        clasp_->enableProgramUpdates();
+        if (opts.singleShot) { clasp_->keepProgram(); }
+        else { clasp_->enableProgramUpdates(); }
         app.main(*this, files);
     }
     else {
         parse(files, opts, out);
         if (scripts_.callable("main")) {
-            clasp_->enableProgramUpdates();
+            if (opts.singleShot) { clasp_->keepProgram(); }
+            else { clasp_->enableProgramUpdates(); }
             scripts_.main(*this);
         }
         else if (incmode_) {
-            clasp_->enableProgramUpdates();
+            if (opts.singleShot) { clasp_->keepProgram(); }
+            else { clasp_->enableProgramUpdates(); }
             incmode(*this);
         }
         else {
-            incremental_ = false;
             claspConfig_.releaseOptions();
             Control::GroundVec parts;
             parts.emplace_back("base", SymVec{});
@@ -848,7 +849,8 @@ ClingoLib::ClingoLib(Scripts &scripts, int argc, char const * const *argv, Logge
     allOpts.assignDefaults(parsed);
     claspConfig_.finalize(parsed, Clasp::Problem_t::Asp, true);
     clasp_.ctx.setEventHandler(this);
-    Clasp::Asp::LogicProgram* lp = &clasp_.startAsp(claspConfig_, true);
+    Clasp::Asp::LogicProgram* lp = &clasp_.startAsp(claspConfig_, !grOpts_.singleShot);
+    if (grOpts_.singleShot) { clasp_.keepProgram(); }
     parse({}, grOpts_, lp, false);
 }
 
@@ -886,6 +888,7 @@ void ClingoLib::initOptions(Potassco::ProgramOptions::OptionContext& root) {
          "      [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")
         ;
     root.add(gringo);
     claspConfig_.addOptions(root);

diff --git a/libclingo/src/gringo_app.cc b/libclingo/src/gringo_app.cc
@@ -60,6 +60,7 @@ struct GringoOptions {
     bool                          wNoOther              = false;
     bool                          rewriteMinimize       = false;
     bool                          keepFacts             = false;
+    bool                          singleShot            = false;
     Foobar                        foobar;
 };
 
@@ -364,6 +365,7 @@ struct GringoApp : public Potassco::Application {
             ("keep-facts,@1", flag(grOpts_.keepFacts = false), "Do not remove facts from normal rules")
             ("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")
+            ("single-shot,@2", flag(grOpts_.singleShot = false), "Force single-shot grounding mode")
             ("foobar,@4", storeTo(grOpts_.foobar, parseFoobar), "Foobar")
             ;
         root.add(gringo);
@@ -408,11 +410,11 @@ struct GringoApp : public Potassco::Application {
         using namespace Gringo;
         IncrementalControl inc(out, input_, grOpts_);
         if (inc.scripts.callable("main")) {
-            inc.incremental_ = true;
+            inc.incremental_ = !grOpts_.singleShot;
             inc.scripts.main(inc);
         }
         else if (inc.incmode) {
-            inc.incremental_ = true;
+            inc.incremental_ = !grOpts_.singleShot;
             incmode(inc);
         }
         else {
+5 −0		clasp/clasp_facade.h
+11 −3		src/clasp_facade.cpp
+1 −1		src/logic_program.cpp
+33 −0		tests/facade_test.cpp