diff --git a/src/sat/sat_aig_simplifier.cpp b/src/sat/sat_aig_simplifier.cpp
index cbba29793..79b7b0b04 100644
--- a/src/sat/sat_aig_simplifier.cpp
+++ b/src/sat/sat_aig_simplifier.cpp
@@ -91,8 +91,6 @@ namespace sat {
         s(_s), 
         m_trail_size(0),
         m_validator(nullptr) {  
-        m_config.m_enable_dont_cares = true;
-        m_config.m_enable_units = true;
         if (s.get_config().m_drat) {
             std::function<void(literal_vector const& clause)> _on_add = 
                 [this](literal_vector const& clause) { s.m_drat.add(clause); };
@@ -101,7 +99,7 @@ namespace sat {
             m_aig_cuts.set_on_clause_add(_on_add);
             m_aig_cuts.set_on_clause_del(_on_del);
         }
-        else if (m_config.m_validate) {
+        else if (m_config.m_validate_cuts) {
             ensure_validator();
             std::function<void(literal_vector const& clause)> _on_add = 
                 [this](literal_vector const& clause) { 
@@ -193,7 +191,7 @@ namespace sat {
         af.set(on_and);
         af.set(on_ite);
         clause_vector clauses(s.clauses());
-        if (m_config.m_add_learned) clauses.append(s.learned());
+        if (m_config.m_learned2aig) clauses.append(s.learned());
         af(clauses);
 
         std::function<void (literal_vector const&)> on_xor = 
@@ -339,7 +337,7 @@ namespace sat {
      * that u implies v.
      */
     void aig_simplifier::cuts2implies(vector<cut_set> const& cuts) {
-        if (!m_config.m_enable_implies) return;
+        if (!m_config.m_learn_implies) return;
         vector<vector<std::pair<unsigned, cut const*>>> var_tables;
         map<cut const*, unsigned, cut::dom_hash_proc, cut::dom_eq_proc> cut2tables;
         unsigned j = 0;
@@ -631,13 +629,13 @@ namespace sat {
     }
 
     void aig_simplifier::validate_unit(literal lit) {
-        if (!m_config.m_validate_enabled) return;
+        if (!m_config.m_validate_lemmas) return;
         ensure_validator();
         m_validator->validate(1, &lit);
     }
 
     void aig_simplifier::validate_eq(literal a, literal b) {
-        if (!m_config.m_validate_enabled) return;
+        if (!m_config.m_validate_lemmas) return;
         ensure_validator();
         literal lits1[2] = { a, ~b };
         literal lits2[2] = { ~a, b };
diff --git a/src/sat/sat_aig_simplifier.h b/src/sat/sat_aig_simplifier.h
index c58f9aa25..74328f623 100644
--- a/src/sat/sat_aig_simplifier.h
+++ b/src/sat/sat_aig_simplifier.h
@@ -33,19 +33,19 @@ namespace sat {
             void reset() { memset(this, 0, sizeof(*this)); }
         };
         struct config {
-            bool m_validate;
-            bool m_enable_units;
-            bool m_enable_dont_cares;
-            bool m_enable_implies;
-            bool m_add_learned;
-            bool m_validate_enabled;
+            bool m_enable_units;            // enable learning units
+            bool m_enable_dont_cares;       // enable applying don't cares to LUTs
+            bool m_learn_implies;           // learn binary clauses
+            bool m_learned2aig;             // add learned clauses to AIGs used by cut-set enumeration
+            bool m_validate_cuts;           // enable direct validation of generated cuts
+            bool m_validate_lemmas;         // enable direct validation of learned lemmas 
             config():
-                m_validate(false), 
-                m_enable_units(false),
-                m_enable_dont_cares(false),
-                m_enable_implies(false),
-                m_add_learned(true),
-                m_validate_enabled(false) {}
+                m_enable_units(true),
+                m_enable_dont_cares(true),
+                m_learn_implies(false),
+                m_learned2aig(true),
+                m_validate_cuts(false), 
+                m_validate_lemmas(false) {}
         };
     private:
         struct report;
@@ -151,6 +151,13 @@ namespace sat {
         void operator()();
         void collect_statistics(statistics& st) const;
 
+        /**
+         * The clausifier may know that some literal is defined as a 
+         * function of other literals. This API is exposed so that 
+         * the clausifier can instrument the simplifier with an initial
+         * AIG.
+         * set_root is issued from the equivalence finder.
+         */
         void add_and(literal head, unsigned sz, literal const* args);
         void add_or(literal head, unsigned sz, literal const* args);
         void add_xor(literal head, unsigned sz, literal const* args);