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.

diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 3011ad6ec4ebf3f4e1703b60712cd87b1e22c253..88f8c6c5043673eaa21edd64c7484ad072e3cbd2 100644 (file)
--- 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 d0092ab1ca62963e2e4aaa1f6ba129cdf789130c..3755509b8676517186dba6286369f56079989520 100644 (file)
--- 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 c61069cae494d7f97b1c349229be7f66fec17f8f..120fc730be8bbee152770a785be22a389cbabcd2 100644 (file)
--- 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 f1a340ca07949d6e5e01f5b1e6ed152d06fd5975..5f33a5ecc1f5ff8d9df50dd49791a217a11e0b01 100644 (file)
--- 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 e577e691200f9755522b6433ee40bdf41192c674..d659369642a97dc19c83d203ddf6e2ade3a77c71 100644 (file)
--- 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 366c26c22e8c181bc9cb3b3cdf875f6a1578b721..60446a0e73aaeea7d8cd21ce99f7baef45a90a25 100644 (file)
--- 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

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 6f8bbe997b9d593fba8d6eb5ba8373215fac482c..0e911a49544fc16e444884dab2e6a24ba203accf 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -194,7 +194,7 @@ void PropEngine::assertInputFormulas(
     {
       skolem = it->second;
     }
-    d_theoryProxy->notifyAssertion(assertions[i], skolem);
+    d_theoryProxy->notifyAssertion(assertions[i], skolem, false);
   }
   for (const Node& node : assertions)
   {
@@ -310,11 +310,11 @@ void PropEngine::assertLemmasInternal(
     if (!trn.isNull())
     {
       // notify the theory proxy of the lemma
-      d_theoryProxy->notifyAssertion(trn.getProven());
+      d_theoryProxy->notifyAssertion(trn.getProven(), TNode::null(), true);
     }
     for (const theory::SkolemLemma& lem : ppLemmas)
     {
-      d_theoryProxy->notifyAssertion(lem.getProven(), lem.d_skolem);
+      d_theoryProxy->notifyAssertion(lem.getProven(), lem.d_skolem, true);
     }
   }
 }

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 254388a496f3e6e791dcaa10b16877268ac01cc9..ff00acc517da0cbda61c9781032b8496b270b0ed 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -62,16 +62,16 @@ void TheoryProxy::presolve()
   d_theoryEngine->presolve();
 }
 
-void TheoryProxy::notifyAssertion(Node a, TNode skolem)
+void TheoryProxy::notifyAssertion(Node a, TNode skolem, bool isLemma)
 {
   if (skolem.isNull())
   {
-    d_decisionEngine->addAssertion(a);
+    d_decisionEngine->addAssertion(a, isLemma);
   }
   else
   {
     d_skdm->notifySkolemDefinition(skolem, a);
-    d_decisionEngine->addSkolemDefinition(a, skolem);
+    d_decisionEngine->addSkolemDefinition(a, skolem, isLemma);
   }
 }
 

diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 67d3c06682419ce2dd9dd5b4c46e087834e390f5..decae3f2abfc2f08176ba021d6b33d479a614fb6 100644 (file)
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -68,8 +68,13 @@ class TheoryProxy : public Registrar
   /** Presolve, which calls presolve for the modules managed by this class */
   void presolve();
 
-  /** Notify a lemma, possibly corresponding to a skolem definition */
-  void notifyAssertion(Node lem, TNode skolem = TNode::null());
+  /**
+   * Notify a lemma or input assertion, possibly corresponding to a skolem
+   * definition.
+   */
+  void notifyAssertion(Node lem,
+                       TNode skolem = TNode::null(),
+                       bool isLemma = false);
 
   void theoryCheck(theory::Theory::Effort effort);