add ability to multiply term

Z3Prover · Jan 22, 2024 · 839b710 · 839b710
1 parent 0ebd8d6
commit 839b710
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/math/lp/lar_term.h b/src/math/lp/lar_term.h
@@ -138,6 +138,12 @@ class lar_term {
         }
         return ret;
     }
+
+    lar_term& operator*=(mpq const& k) {
+        for (auto & t : m_coeffs)
+            t.m_value *= k;
+        return *this;
+    }
 
     void clear() {
         m_coeffs.reset();