From 26ddf7fb90ea62509bb235286024fc7f76319591 Mon Sep 17 00:00:00 2001
From: Patrick LaFontaine <32135464+Pat-Lafon@users.noreply.github.com>
Date: Tue, 7 Nov 2023 18:17:08 -0500
Subject: [PATCH] Implement += for Solver

---
 z3/src/solver.rs | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)

diff --git a/z3/src/solver.rs b/z3/src/solver.rs
index f27a8039..13923d55 100644
--- a/z3/src/solver.rs
+++ b/z3/src/solver.rs
@@ -4,6 +4,8 @@ use std::fmt;
 
 use z3_sys::*;
 
+use std::ops::AddAssign;
+
 use crate::{ast, ast::Ast, Context, Model, Params, SatResult, Solver, Statistics, Symbol};
 
 impl<'ctx> Solver<'ctx> {
@@ -89,6 +91,19 @@ impl<'ctx> Solver<'ctx> {
     /// should be used to check whether the logical context is consistent
     /// or not.
     ///
+    /// ```rust
+    /// use z3::{Config, Context, Solver, ast, SatResult, ast::Bool};
+    /// let cfg = Config::new();
+    /// let ctx = Context::new(&cfg);
+    /// let mut solver = Solver::new(&ctx);
+    ///
+    /// solver.assert(&Bool::from_bool(&ctx, true));
+    /// solver += &Bool::from_bool(&ctx, false);
+    /// solver += Bool::fresh_const(&ctx, "");
+    ///
+    /// assert_eq!(solver.check(), SatResult::Unsat);
+    /// ````
+    ///
     /// # See also:
     ///
     /// - [`Solver::assert_and_track()`]
@@ -385,3 +400,15 @@ impl<'ctx> Clone for Solver<'ctx> {
         new_solver
     }
 }
+
+impl<'ctx> AddAssign<&ast::Bool<'ctx>> for Solver<'ctx> {
+    fn add_assign(&mut self, rhs: &ast::Bool<'ctx>) {
+        self.assert(rhs);
+    }
+}
+
+impl<'ctx> AddAssign<ast::Bool<'ctx>> for Solver<'ctx> {
+    fn add_assign(&mut self, rhs: ast::Bool<'ctx>) {
+        self.assert(&rhs);
+    }
+}