1 files changed, 14 insertions, 0 deletions
diff --git a/src/prop/sat.h b/src/prop/sat.h
index be3ed244b..e86443827 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -137,6 +137,12 @@ class SatSolver : public SatInputInterface {
   /** Context we will be using to synchronzie the sat solver */
   context::Context* d_context;
 
+  /**
+   * Set of all lemmas that have been "shared" in the portfolio---i.e.,
+   * all imported and exported lemmas.
+   */
+  std::hash_set<Node, NodeHashFunction> d_shared;
+
   /* Pointer to the concrete SAT solver. Including this via the
      preprocessor saves us a level of indirection vs, e.g., defining a
      sub-class for each solver. */
@@ -263,6 +269,8 @@ public:
 
   void notifyRestart();
 
+  void notifyNewLemma(SatClause& lemma);
+
   SatLiteral getNextReplayDecision();
 
   void logDecision(SatLiteral lit);
@@ -294,6 +302,12 @@ inline SatSolver::SatSolver(PropEngine* propEngine,
   d_minisat->random_var_freq = Options::current()->satRandomFreq;
   d_minisat->random_seed = Options::current()->satRandomSeed;
 
+  // Give access to all possible options in the sat solver
+  d_minisat->var_decay = Options::current()->satVarDecay;
+  d_minisat->clause_decay = Options::current()->satClauseDecay;
+  d_minisat->restart_first = Options::current()->satRestartFirst;
+  d_minisat->restart_inc = Options::current()->satRestartInc;
+
   d_statistics.init(d_minisat);
 }