Add argument to distinguish lemmas and input assertions (#7326)

Work towards virtual clause deletion, where lemmas will be SAT-context dependent.

This adds an argument to the decision engine so it can distinguish lemmas from input assertions.

6 files changed, 22 insertions, 14 deletions

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 3011ad6ec..88f8c6c50 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -42,8 +42,12 @@ prop::SatLiteral DecisionEngine::getNext(bool& stopSearch)
 
 DecisionEngineEmpty::DecisionEngineEmpty(Env& env) : DecisionEngine(env) {}
 bool DecisionEngineEmpty::isDone() { return false; }
-void DecisionEngineEmpty::addAssertion(TNode assertion) {}
-void DecisionEngineEmpty::addSkolemDefinition(TNode lem, TNode skolem) {}
+void DecisionEngineEmpty::addAssertion(TNode assertion, bool isLemma) {}
+void DecisionEngineEmpty::addSkolemDefinition(TNode lem,
+                                              TNode skolem,
+                                              bool isLemma)
+{
+}
 prop::SatLiteral DecisionEngineEmpty::getNextInternal(bool& stopSearch)
 {
   return undefSatLiteral;
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index d0092ab1c..3755509b8 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -54,12 +54,12 @@ class DecisionEngine : protected EnvObj
    * Notify this class that assertion is an (input) assertion, not corresponding
    * to a skolem definition.
    */
-  virtual void addAssertion(TNode assertion) = 0;
+  virtual void addAssertion(TNode assertion, bool isLemma) = 0;
   /**
    * Notify this class that lem is the skolem definition for skolem, which is
    * a part of the current assertions.
    */
-  virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0;
+  virtual void addSkolemDefinition(TNode lem, TNode skolem, bool isLemma) = 0;
   /**
    * Notify this class that the list of lemmas defs are now active in the
    * current SAT context.
@@ -93,8 +93,8 @@ class DecisionEngineEmpty : public DecisionEngine
  public:
   DecisionEngineEmpty(Env& env);
   bool isDone() override;
-  void addAssertion(TNode assertion) override;
-  void addSkolemDefinition(TNode lem, TNode skolem) override;
+  void addAssertion(TNode assertion, bool isLemma) override;
+  void addSkolemDefinition(TNode lem, TNode skolem, bool isLemma) override;
 
  protected:
   prop::SatLiteral getNextInternal(bool& stopSearch) override;
diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp
index c61069cae..120fc730b 100644
--- a/src/decision/decision_engine_old.cpp
+++ b/src/decision/decision_engine_old.cpp
@@ -72,7 +72,7 @@ SatLiteral DecisionEngineOld::getNextInternal(bool& stopSearch)
   return d_decisionStopOnly ? undefSatLiteral : ret;
 }
 
-void DecisionEngineOld::addAssertion(TNode assertion)
+void DecisionEngineOld::addAssertion(TNode assertion, bool isLemma)
 {
   // new assertions, reset whatever result we knew
   d_result = SAT_VALUE_UNKNOWN;
@@ -82,7 +82,9 @@ void DecisionEngineOld::addAssertion(TNode assertion)
   }
 }
 
-void DecisionEngineOld::addSkolemDefinition(TNode lem, TNode skolem)
+void DecisionEngineOld::addSkolemDefinition(TNode lem,
+                                            TNode skolem,
+                                            bool isLemma)
 {
   // new assertions, reset whatever result we knew
   d_result = SAT_VALUE_UNKNOWN;
diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h
index f1a340ca0..5f33a5ecc 100644
--- a/src/decision/decision_engine_old.h
+++ b/src/decision/decision_engine_old.h
@@ -92,12 +92,12 @@ class DecisionEngineOld : public decision::DecisionEngine
    * Notify this class that assertion is an (input) assertion, not corresponding
    * to a skolem definition.
    */
-  void addAssertion(TNode assertion) override;
+  void addAssertion(TNode assertion, bool isLemma) override;
   /**
    * Notify this class  that lem is the skolem definition for skolem, which is
    * a part of the current assertions.
    */
-  void addSkolemDefinition(TNode lem, TNode skolem) override;
+  void addSkolemDefinition(TNode lem, TNode skolem, bool isLemma) override;
 
   // Interface for Strategies to use stuff stored in Decision Engine
   // (which was possibly requested by them on initialization)
diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp
index e577e6912..d65936964 100644
--- a/src/decision/justification_strategy.cpp
+++ b/src/decision/justification_strategy.cpp
@@ -478,7 +478,7 @@ prop::SatValue JustificationStrategy::lookupValue(TNode n)
 
 bool JustificationStrategy::isDone() { return !refreshCurrentAssertion(); }
 
-void JustificationStrategy::addAssertion(TNode assertion)
+void JustificationStrategy::addAssertion(TNode assertion, bool isLemma)
 {
   Trace("jh-assert") << "addAssertion " << assertion << std::endl;
   std::vector<TNode> toProcess;
@@ -486,7 +486,9 @@ void JustificationStrategy::addAssertion(TNode assertion)
   insertToAssertionList(toProcess, false);
 }
 
-void JustificationStrategy::addSkolemDefinition(TNode lem, TNode skolem)
+void JustificationStrategy::addSkolemDefinition(TNode lem,
+                                                TNode skolem,
+                                                bool isLemma)
 {
   Trace("jh-assert") << "addSkolemDefinition " << lem << " / " << skolem
                      << std::endl;
diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h
index 366c26c22..60446a0e7 100644
--- a/src/decision/justification_strategy.h
+++ b/src/decision/justification_strategy.h
@@ -145,12 +145,12 @@ class JustificationStrategy : public DecisionEngine
    * Notify this class that assertion is an (input) assertion, not corresponding
    * to a skolem definition.
    */
-  void addAssertion(TNode assertion) override;
+  void addAssertion(TNode assertion, bool isLemma) override;
   /**
    * Notify this class that lem is the skolem definition for skolem, which is
    * a part of the current assertions.
    */
-  void addSkolemDefinition(TNode lem, TNode skolem) override;
+  void addSkolemDefinition(TNode lem, TNode skolem, bool isLemma) override;
   /**
    * Notify this class that the list of lemmas defs are now active in the
    * current SAT context. This is triggered when a literal lit is sent to