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.

1 files changed, 4 insertions, 4 deletions

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;