Defaults for well known SMT solvers (#52)

This commit adds the methods `.with_z3_defaults()` and
`.with_cvc5_defaults()` to the `ContextBuilder`. These methods will add
the default arguments to start the respective SMT solver in REPL mode.

---------

Co-authored-by: Trevor Elliott <[email protected]>

Author: pleich

.github/workflows/ci.yml

@@ -2,27 +2,26 @@ name: CI
 
 on:
   push:
-    branches: [ "main" ]
+    branches: ["main"]
   pull_request:
-    branches: [ "main" ]
+    branches: ["main"]
 
 env:
   CARGO_TERM_COLOR: always
 
 jobs:
   build:
-
     runs-on: ubuntu-latest
 
     steps:
-    - uses: actions/checkout@v3
-    - name: Install Z3
-      run: sudo apt install -y z3
-    - name: Build
-      run: cargo build --verbose
-    - name: Run tests
-      run: cargo test --verbose
-    - name: Run Sudoku Example
-      run: |
-        cargo run --example sudoku
-        cargo run --example quantifiers
+      - uses: actions/checkout@v3
+      - name: Install Solvers
+        run: sudo apt install -y z3 cvc5
+      - name: Build
+        run: cargo build --verbose
+      - name: Run tests
+        run: cargo test --verbose
+      - name: Run Sudoku Example
+        run: |
+          cargo run --example sudoku
+          cargo run --example quantifiers

README.md

@@ -33,8 +33,7 @@ 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")
-        .solver_args(["-smt2", "-in"])
+        .with_z3_defaults()
         .build()?;
 
     // Declare `x` and `y` variables that are bitvectors of width 32.
@@ -148,8 +147,7 @@ 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")
-        .solver_args(["-smt2", "-in"])
+        .with_z3_defaults()
         .build()?;
 
     // ...

examples/quantifiers.rs

@@ -3,10 +3,7 @@
 
 fn main() -> std::io::Result<()> {
     env_logger::init();
-    let mut ctx = easy_smt::ContextBuilder::new()
-        .solver("z3")
-        .solver_args(["-smt2", "-in"])
-        .build()?;
+    let mut ctx = easy_smt::ContextBuilder::new().with_z3_defaults().build()?;
 
     // Declare an uninterpreted representation for sets.
     ctx.declare_sort("MySet", 0)?;

examples/sudoku.rs

@@ -5,10 +5,7 @@ use easy_smt::SExpr;
 fn main() -> std::io::Result<()> {
     env_logger::init();
 
-    let mut ctx = easy_smt::ContextBuilder::new()
-        .solver("z3")
-        .solver_args(["-smt2", "-in"])
-        .build()?;
+    let mut ctx = easy_smt::ContextBuilder::new().with_z3_defaults().build()?;
 
     // for helping diagnose unsolvable problems
     ctx.set_option(":produce-unsat-cores", ctx.true_())?;

src/context.rs

@@ -81,6 +81,16 @@ impl ContextBuilder {
         Self::default()
     }
 
+    /// Initialize the builder with Z3 defaults.
+    pub fn with_z3_defaults(&mut self) -> &mut Self {
+        self.solver("z3").solver_args(["-smt2", "-in", "-v:0"])
+    }
+
+    /// Initialize the builder with CVC5 defaults.
+    pub fn with_cvc5_defaults(&mut self) -> &mut Self {
+        self.solver("cvc5").solver_args(["--quiet", "--lang=smt2", "--incremental"])
+    }
+
     /// Configure the solver that will be used.
     ///
     /// You can pass arguments to the underlying solver via the

tests/error.rs

@@ -1,10 +1,7 @@
 // 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")
-        .solver_args(["-smt2", "-in"])
-        .build()?;
+    let mut context = easy_smt::ContextBuilder::new().with_z3_defaults().build()?;
 
     let width = context.numeral(1);
     let sort = context.bit_vec_sort(width);

tests/solvers.rs

@@ -0,0 +1,38 @@
+use easy_smt::{Context, Response};
+
+fn test_solver_interaction(solver: &mut Context) {
+    let int_sort = solver.int_sort();
+    let x = solver.declare_const("x", int_sort).unwrap();
+
+    // x <= 2 && x > 1
+    let constr = solver.and(
+        solver.lte(x, solver.numeral(2)),
+        solver.gt(x, solver.numeral(1)),
+    );
+    solver.assert(constr).unwrap();
+
+    assert_eq!(solver.check().unwrap(), Response::Sat);
+
+    let solution = solver.get_value(vec![x]).unwrap();
+    assert_eq!(solution.len(), 1);
+    assert_eq!(solution[0].0, x);
+    assert_eq!(solver.get_u64(solution[0].1).unwrap(), 2);
+}
+
+#[test]
+fn test_z3_solver() {
+    let mut context = easy_smt::ContextBuilder::new()
+        .with_z3_defaults()
+        .build()
+        .unwrap();
+    test_solver_interaction(&mut context);
+}
+
+#[test]
+fn test_cvc5_solver() {
+    let mut context = easy_smt::ContextBuilder::new()
+        .with_cvc5_defaults()
+        .build()
+        .unwrap();
+    test_solver_interaction(&mut context);
+}