introduce notion of auxiliary constraints created by nla_solver lemmas

notes: auxiliary constraints could extend to Gomory and B&B.

src/math/lp/lar_constraints.h

@@ -41,14 +41,15 @@ class lar_base_constraint {
     lconstraint_kind m_kind;
     mpq              m_right_side;
     bool             m_active;
+    bool             m_is_auxiliary;
     unsigned         m_j;
     u_dependency*    m_dep;
 
-   public:
+public:
 
     virtual vector<std::pair<mpq, lpvar>> coeffs() const = 0;
     lar_base_constraint(unsigned j, lconstraint_kind kind, u_dependency* dep, const mpq& right_side) :
-        m_kind(kind), m_right_side(right_side), m_active(false), m_j(j), m_dep(dep) {}
+        m_kind(kind), m_right_side(right_side), m_active(false), m_is_auxiliary(false), m_j(j), m_dep(dep) {}
     virtual ~lar_base_constraint() = default;
 
     lconstraint_kind kind() const { return m_kind; }
@@ -60,6 +61,9 @@ class lar_base_constraint {
     void deactivate() { m_active = false; }
     bool is_active() const { return m_active; }
 
+    bool is_auxiliary() const { return m_is_auxiliary; }
+    void set_auxiliary() { m_is_auxiliary = true; }
+
     virtual unsigned size() const = 0;
     virtual mpq get_free_coeff_of_left_side() const { return zero_of_type<mpq>();}
 };
@@ -96,10 +100,13 @@ class constraint_set {
     stacked_value<unsigned>        m_constraint_count;
     unsigned_vector                m_active;
     stacked_value<unsigned>        m_active_lim;    
+    bool                           m_is_auxiliary_mode = false;
 
     constraint_index add(lar_base_constraint* c) {
         constraint_index ci = m_constraints.size();
         m_constraints.push_back(c);
+        if (m_is_auxiliary_mode)
+            c->set_auxiliary();
         return ci;
     }
 
@@ -146,6 +153,8 @@ public:
             c->~lar_base_constraint();
     }
 
+    void set_auxiliary(bool m) { m_is_auxiliary_mode = m; }
+
     void push() {
         m_constraint_count = m_constraints.size();
         m_constraint_count.push();

src/math/lp/lar_solver.cpp

@@ -1744,6 +1744,14 @@ namespace lp {
         A_r().m_columns.pop_back();
     }
 
+    lar_solver::scoped_auxiliary::scoped_auxiliary(lar_solver& s) : s(s) {
+        s.m_imp->m_constraints.set_auxiliary(true);
+    }
+
+    lar_solver::scoped_auxiliary::~scoped_auxiliary() {
+        s.m_imp->m_constraints.set_auxiliary(false);
+    }
+
     void lar_solver::remove_last_column_from_basis_tableau(unsigned j) {
         auto& rslv = get_core_solver().m_r_solver;
         int i = rslv.m_basis_heading[j];

src/math/lp/lar_solver.h

@@ -319,6 +319,12 @@ public:
     bool compare_values(lpvar j, lconstraint_kind kind, const mpq& right_side);
     lpvar add_term(const vector<std::pair<mpq, lpvar>>& coeffs, unsigned ext_i);
     void register_existing_terms();
+    class scoped_auxiliary {
+        lar_solver& s;
+    public:
+        scoped_auxiliary(lar_solver& s);
+        ~scoped_auxiliary();
+    };
     constraint_index add_var_bound(lpvar, lconstraint_kind, const mpq&);
     constraint_index add_var_bound_check_on_equal(lpvar, lconstraint_kind, const mpq&, lpvar&);
 

src/math/lp/nra_solver.cpp

@@ -63,6 +63,8 @@ struct solver::imp {
 
         for (auto ci : lra.constraints().indices()) {
             auto const& c = lra.constraints()[ci];
+            if (c.is_auxiliary())
+                continue;
             for (auto const& [coeff, v] : c.coeffs()) {
                 var2occurs.reserve(v + 1);
                 var2occurs[v].constraints.push_back(ci);

src/smt/theory_lra.cpp

@@ -2040,6 +2040,8 @@ public:
     }
 
     final_check_status check_nla() {
+        // TODO - enable or remove if found useful internals are corrected:
+        // lp::lar_solver::scoped_auxiliary _sa(lp()); // new atoms are auxilairy and are not used in nra_solver
         if (!m.inc()) {
             TRACE(arith, tout << "canceled\n";);
             return FC_GIVEUP;