remove disjunctive lemma feature

src/math/polysat/constraint.cpp

@@ -196,6 +196,7 @@ namespace polysat {
     }
 
     bool constraint_manager::should_gc() {
+        return false;
         // TODO control gc decay rate
         return m_constraints.size() > m_num_external + 100;
     }

src/math/polysat/solver.cpp

@@ -59,7 +59,6 @@ namespace polysat {
    
     lbool solver::check_sat() { 
         LOG("Starting");
-        m_disjunctive_lemma.reset();
         while (inc()) {
             m_stats.m_num_iterations++;
             LOG_H1("Next solving loop iteration (#" << m_stats.m_num_iterations << ")");
@@ -68,7 +67,6 @@ namespace polysat {
             COND_LOG(is_conflict(), "Conflict:       " << m_conflict);
             IF_LOGGING(m_viable.log());
             if (!is_conflict() && m_constraints.should_gc()) m_constraints.gc(*this);
-            if (pending_disjunctive_lemma()) { LOG_H2("UNDEF (handle lemma externally)"); return l_undef; }
             else if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
             else if (is_conflict()) resolve_conflict();
             else if (can_propagate()) propagate();

src/math/polysat/solver.h

@@ -86,8 +86,6 @@ namespace polysat {
         // Per constraint state
         constraint_manager       m_constraints;
 
-        svector<sat::bool_var>   m_disjunctive_lemma;
-
         // Per variable information
         vector<rational>         m_value;         // assigned value
         vector<justification>    m_justification; // justification for variable assignment
@@ -252,12 +250,6 @@ namespace polysat {
          */
         lbool check_sat();
 
-        /**
-         * Returns the disjunctive lemma that should be learned,
-         * or an empty vector if check_sat() terminated for a different reason.
-         */
-        svector<sat::bool_var> get_lemma() { return m_disjunctive_lemma; }
-        bool pending_disjunctive_lemma() { return !m_disjunctive_lemma.empty(); }
 
         /**
          * retrieve unsat core dependencies

src/test/polysat.cpp

@@ -16,31 +16,6 @@ namespace polysat {
         std::string m_name;
         lbool m_last_result = l_undef;
 
-        lbool check_rec() {
-            lbool result = check_sat();
-            if (result != l_undef)
-                return result;
-            auto const new_lemma = get_lemma();
-            // Empty lemma => check_sat() terminated for another reason, e.g., resource limits
-            if (new_lemma.empty())
-                return l_undef;
-            for (auto lit : new_lemma) {
-                push();
-                assign_eh(lit, true);
-                result = check_rec();
-                pop();
-                // Found a model => done
-                if (result == l_true)
-                    return l_true;
-                if (result == l_undef)
-                    return l_undef;
-                // Unsat => try next literal
-                SASSERT(result == l_false);
-            }
-            // No literal worked? unsat
-            return l_false;
-        }
-
     public:
         scoped_solver(std::string name): solver(lim), m_name(name) {
             std::cout << "\n\n\n" << std::string(78, '#') << "\n";
@@ -48,7 +23,7 @@ namespace polysat {
         }
 
         void check() {
-            m_last_result = check_rec();
+            m_last_result = check_sat();
             std::cout << m_name << ": " << m_last_result << "\n";
             statistics st;
             collect_statistics(st);