Use separate methods for configuring the solver program and its args (#44)

Note: this is a breaking change.

Fixes #43

Author: fitzgen

README.md

@@ -33,7 +33,8 @@ use easy_smt::{ContextBuilder, Response};
 fn main() -> std::io::Result<()> {
     // Create a new context, backed by a Z3 subprocess.
     let mut ctx = ContextBuilder::new()
-        .solver("z3", ["-smt2", "-in"])
+        .solver("z3")
+        .solver_args(["-smt2", "-in"])
         .build()?;
 
     // Declare `x` and `y` variables that are bitvectors of width 32.
@@ -147,7 +148,8 @@ fn main() -> std::io::Result<()> {
         // Everything needed to replay the solver session will be written
         // to `replay.smt2`.
         .replay_file(Some(std::fs::File::create("replay.smt2")?))
-        .solver("z3", ["-smt2", "-in"])
+        .solver("z3")
+        .solver_args(["-smt2", "-in"])
         .build()?;
 
     // ...

examples/quantifiers.rs

@@ -4,7 +4,8 @@
 fn main() -> std::io::Result<()> {
     env_logger::init();
     let mut ctx = easy_smt::ContextBuilder::new()
-        .solver("z3", ["-smt2", "-in"])
+        .solver("z3")
+        .solver_args(["-smt2", "-in"])
         .build()?;
 
     // Declare an uninterpreted representation for sets.
@@ -14,11 +15,7 @@ fn main() -> std::io::Result<()> {
 
     // Our sets have a simple interface of predicates: empty(s),
     // member(x,s), and subset(s1,s2).
-    ctx.declare_fun(
-        "empty",
-        vec![ctx.atom("MySet")],
-        ctx.bool_sort(),
-    )?;
+    ctx.declare_fun("empty", vec![ctx.atom("MySet")], ctx.bool_sort())?;
     ctx.declare_fun(
         "member",
         vec![ctx.atom("MyElement"), ctx.atom("MySet")],
@@ -41,30 +38,18 @@ fn main() -> std::io::Result<()> {
             // One of the following is true:
             ctx.or(
                 // (1) s1 is a subset of s2, or
-                ctx.list(vec![
-                    ctx.atom("subset"),
-                    ctx.atom("s1"),
-                    ctx.atom("s2"),
-                ]),
+                ctx.list(vec![ctx.atom("subset"), ctx.atom("s1"), ctx.atom("s2")]),
                 // (2) an element exists which is a member of s1, and
                 // not a member of s2.
                 ctx.exists(
                     [("x", ctx.atom("MyElement"))],
                     ctx.and(
-                        ctx.list(vec![
-                            ctx.atom("member"),
-                            ctx.atom("x"),
-                            ctx.atom("s1"),
-                        ]),
-                        ctx.not(ctx.list(vec![
-                            ctx.atom("member"),
-                            ctx.atom("x"),
-                            ctx.atom("s2"),
-                        ])),
+                        ctx.list(vec![ctx.atom("member"), ctx.atom("x"), ctx.atom("s1")]),
+                        ctx.not(ctx.list(vec![ctx.atom("member"), ctx.atom("x"), ctx.atom("s2")])),
                     ),
                 ),
             ),
-        )
+        ),
     )?;
 
     // Second, a set is empty iff no member exists.
@@ -79,11 +64,7 @@ fn main() -> std::io::Result<()> {
                 // (2) an element exists that is a member of the set.
                 ctx.exists(
                     [("x", ctx.atom("MyElement"))],
-                    ctx.list(vec![
-                        ctx.atom("member"),
-                        ctx.atom("x"),
-                        ctx.atom("s1"),
-                    ]),
+                    ctx.list(vec![ctx.atom("member"), ctx.atom("x"), ctx.atom("s1")]),
                 ),
             ),
         ),
@@ -95,31 +76,21 @@ fn main() -> std::io::Result<()> {
     ctx.declare_const("s2", ctx.atom("MySet"))?;
 
     // Is it possible for s1 to be empty,
-    ctx.assert(
-        ctx.list(vec![ctx.atom("empty"), ctx.atom("s1")])
-    )?;
+    ctx.assert(ctx.list(vec![ctx.atom("empty"), ctx.atom("s1")]))?;
     // while also s1 is not a subset of s2?
-    ctx.assert(
-        ctx.not(
-            ctx.list(vec![
-                ctx.atom("subset"),
-                ctx.atom("s1"),
-                ctx.atom("s2"),
-            ])
-        )
-    )?;
+    ctx.assert(ctx.not(ctx.list(vec![ctx.atom("subset"), ctx.atom("s1"), ctx.atom("s2")])))?;
 
     // We expect the answer to be no (UNSAT).
     match ctx.check()? {
         easy_smt::Response::Sat => {
             println!("Solver returned SAT. This is unexpected!");
-        },
+        }
         easy_smt::Response::Unsat => {
             println!("Solver returned UNSAT. This is expected.");
-        },
+        }
         easy_smt::Response::Unknown => {
             println!("Solver returned UNKNOWN. This is unexpected!");
-        },
+        }
     }
     Ok(())
 }

examples/sudoku.rs

@@ -6,7 +6,8 @@ fn main() -> std::io::Result<()> {
     env_logger::init();
 
     let mut ctx = easy_smt::ContextBuilder::new()
-        .solver("z3", ["-smt2", "-in"])
+        .solver("z3")
+        .solver_args(["-smt2", "-in"])
         .build()?;
 
     // for helping diagnose unsolvable problems

src/context.rs

@@ -3,7 +3,7 @@ use crate::{
     sexpr::{Arena, DisplayExpr, SExpr, SExprData},
     solver::Solver,
 };
-use std::{ffi, io};
+use std::{ffi, io, mem};
 
 macro_rules! variadic {
     ($name:ident, $op:ident) => {
@@ -70,7 +70,8 @@ macro_rules! pairwise {
 
 #[derive(Default)]
 pub struct ContextBuilder {
-    solver_program_and_args: Option<(ffi::OsString, Vec<ffi::OsString>)>,
+    solver: Option<ffi::OsString>,
+    solver_args: Vec<ffi::OsString>,
     replay_file: Option<Box<dyn io::Write + Send>>,
 }
 
@@ -82,17 +83,29 @@ impl ContextBuilder {
 
     /// Configure the solver that will be used.
     ///
+    /// You can pass arguments to the underlying solver via the
+    /// [`solver_args`][Self::solver_args] method.
+    ///
     /// By default, no solver is configured, and any `Context` created will only
     /// be able to build and display expressions, not assert them or query for
     /// their satisfiability.
-    pub fn solver<P, A>(&mut self, program: P, args: A) -> &mut Self
+    pub fn solver<P>(&mut self, program: P) -> &mut Self
     where
         P: Into<ffi::OsString>,
+    {
+        self.solver = Some(program.into());
+        self
+    }
+
+    /// Configure the arguments that will be passed to the solver.
+    ///
+    /// By default, no arguments are passed to the solver.
+    pub fn solver_args<A>(&mut self, args: A) -> &mut Self
+    where
         A: IntoIterator,
         A::Item: Into<ffi::OsString>,
     {
-        self.solver_program_and_args =
-            Some((program.into(), args.into_iter().map(|a| a.into()).collect()));
+        self.solver_args = args.into_iter().map(|a| a.into()).collect();
         self
     }
 
@@ -102,7 +115,8 @@ impl ContextBuilder {
     /// `Context` created will only be able to build and display expressions,
     /// not assert them or query for their satisfiability.
     pub fn without_solver(&mut self) -> &mut Self {
-        self.solver_program_and_args = None;
+        self.solver = None;
+        self.solver_args.clear();
         self
     }
 
@@ -128,10 +142,10 @@ impl ContextBuilder {
         let arena = Arena::new();
         let atoms = KnownAtoms::new(&arena);
 
-        let solver = if let Some((program, args)) = self.solver_program_and_args.take() {
+        let solver = if let Some(program) = self.solver.take() {
             Some(Solver::new(
                 program,
-                args,
+                mem::take(&mut self.solver_args),
                 self.replay_file
                     .take()
                     .unwrap_or_else(|| Box::new(io::sink())),

tests/error.rs

@@ -1,18 +1,19 @@
-
 // This test ensures that we can handle `(error "...")` responses from z3.
 #[test]
 fn handles_errors_gracefully() -> std::io::Result<()> {
     let mut context = easy_smt::ContextBuilder::new()
-        .solver("z3", ["-smt2", "-in"])
+        .solver("z3")
+        .solver_args(["-smt2", "-in"])
         .build()?;
 
     let width = context.numeral(1);
     let sort = context.bit_vec_sort(width);
 
     // The name `foo:a` will cause a parse error, as z3 will parse it as the two atoms, `foo`
     // and `:a`, and then reject the invalid declaration.
-    context.declare_fun("foo:a", vec![], sort).expect_err("z3 should reject this declaration");
+    context
+        .declare_fun("foo:a", vec![], sort)
+        .expect_err("z3 should reject this declaration");
 
     Ok(())
 }
-