Add example to readme

Cargo.toml

@@ -8,11 +8,10 @@ license = "GPL-3.0"
 publish = true
 readme = "README.md"
 repository = "https://github.com/novafacing/yices2-rs"
-version = "0.1.0"
 
 [workspace]
 members = ["yices2-sys", "yices2"]
 default-members = ["yices2-sys", "yices2"]
 
 [workspace.dependencies]
-yices2-sys = { version = "0.1.0", path = "yices2-sys" }
+yices2-sys = { version = "2.6.4", path = "yices2-sys" }

README.md

@@ -1,3 +1,78 @@
 # Yices2
 
-This package is under construction :) check back in two weeks!
+Low and high-level Rust bindings to the [Yices2](https://yices.csl.sri.com) SMT solver.
+
+- [Yices2](#yices2)
+  - [Example](#example)
+    - [Linear Real Arithmetic](#linear-real-arithmetic)
+    - [BitVectors](#bitvectors)
+  - [Usage](#usage)
+  - [Features](#features)
+
+## Example
+
+### Linear Real Arithmetic
+
+```rust
+let config = Config::with_defaults_for_logics([Logic::QF_LRA])?;
+let ctx = Context::with_config(&config)?;
+let x = Uninterpreted::with_name(Real::new()?.into(), "x")?;
+let y = Uninterpreted::with_name(Real::new()?.into(), "y")?;
+let t1 = Add::new(x.into(), y.into())?;
+let t2 = ArithmeticGreaterThanAtom::new(t1.into(), ArithmeticConstant::zero()?.into())?;
+let t3 = Or::new([
+    ArithmeticLessThanAtom::new(x.into(), ArithmeticConstant::zero()?.into())?.into(),
+    ArithmeticLessThanAtom::new(y.into(), ArithmeticConstant::zero()?.into())?.into(),
+])?;
+ctx.assert([t2.into(), t3.into()])?;
+let status = ctx.check()?;
+assert_eq!(status, Status::STATUS_SAT);
+let xv = ctx.model()?.double(&x.into())?;
+let yv = ctx.model()?.double(&y.into())?;
+assert_eq!(xv, 2.0);
+assert_eq!(yv, -1.0);
+```
+
+### BitVectors
+
+```rust
+let config = Config::with_defaults_for_logics([Logic::QF_BV])?;
+let ctx = Context::with_config(&config)?;
+let bv = BitVector::new(32)?;
+let bvc = BitVectorConstant::from_hex_with_name("00000000", "c")?;
+let x = Uninterpreted::with_name(bv.into(), "x")?;
+let y = Uninterpreted::with_name(bv.into(), "y")?;
+let a1 = BitVectorSignedGreaterThanAtom::new(x.into(), bvc.into())?;
+let a2 = BitVectorSignedGreaterThanAtom::new(y.into(), bvc.into())?;
+let a3 = BitVectorSignedLessThanAtom::new(
+    BitVectorAdd::new(x.into(), y.into())?.into(),
+    x.into(),
+)?;
+ctx.assert([a1.into(), a2.into(), a3.into()])?;
+
+assert_eq!(ctx.check()?, Status::STATUS_SAT);
+```
+
+## Usage
+
+You can add this crate to your project by running:
+
+```sh
+cargo add yices2
+```
+
+Or by adding this line to your `Cargo.toml`:
+
+```toml
+yices2 = { version = "2.6.4" }
+```
+
+## Features
+
+By default, `yices2` enables the `ctor` feature, which calls `yices_init` at program
+initialization and `yices_exit` at program exit. If you'd like to disable this behavior,
+you can use the `default-features = false` flag in your `Cargo.toml`.
+
+```toml
+yices2 = { version = "2.6.4", default-features = false }
+```

yices2-sys/Cargo.toml

@@ -9,7 +9,7 @@ license.workspace = true
 publish.workspace = true
 readme.workspace = true
 repository.workspace = true
-version.workspace = true
+version = "2.6.4"
 
 [lib]
 doctest = false

yices2/Cargo.toml

@@ -9,7 +9,7 @@ license.workspace = true
 publish.workspace = true
 readme.workspace = true
 repository.workspace = true
-version.workspace = true
+version = "0.1.1"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 

yices2/src/lib.rs

@@ -250,12 +250,9 @@ mod ctor_test {
 
         let config = Config::with_defaults_for_logics([Logic::QF_LRA])?;
         let ctx = Context::with_config(&config)?;
-        let x = Uninterpreted::new(Real::new()?.into())?;
-        x.set_name("x")?;
-        let y = Uninterpreted::new(Real::new()?.into())?;
-        y.set_name("y")?;
+        let x = Uninterpreted::with_name(Real::new()?.into(), "x")?;
+        let y = Uninterpreted::with_name(Real::new()?.into(), "y")?;
         let t1 = Add::new(x.into(), y.into())?;
-        println!("t1: {:?}", t1);
         let t2 = ArithmeticGreaterThanAtom::new(t1.into(), ArithmeticConstant::zero()?.into())?;
         let t3 = Or::new([
             ArithmeticLessThanAtom::new(x.into(), ArithmeticConstant::zero()?.into())?.into(),
@@ -264,7 +261,6 @@ mod ctor_test {
         ctx.assert([t2.into(), t3.into()])?;
         let status = ctx.check()?;
         assert_eq!(status, Status::STATUS_SAT);
-        println!("status: {:?}", status);
         let xv = ctx.model()?.double(&x.into())?;
         let yv = ctx.model()?.double(&y.into())?;
         assert_eq!(xv, 2.0);
@@ -276,19 +272,12 @@ mod ctor_test {
     fn readme_bv() -> Result<()> {
         reset();
 
-        let config = Config::new()?;
-        config.set_defaults_for_logic(&Logic::QF_BV)?;
-        println!("Got config");
-
+        let config = Config::with_defaults_for_logics([Logic::QF_BV])?;
         let ctx = Context::with_config(&config)?;
-        println!("Got context");
         let bv = BitVector::new(32)?;
-        let bvc = BitVectorConstant::from_hex("00000000")?;
-
-        let x = Uninterpreted::new(bv.into())?;
-        x.set_name("x")?;
-        let y = Uninterpreted::new(bv.into())?;
-        y.set_name("y")?;
+        let bvc = BitVectorConstant::from_hex_with_name("00000000", "c")?;
+        let x = Uninterpreted::with_name(bv.into(), "x")?;
+        let y = Uninterpreted::with_name(bv.into(), "y")?;
         let a1 = BitVectorSignedGreaterThanAtom::new(x.into(), bvc.into())?;
         let a2 = BitVectorSignedGreaterThanAtom::new(y.into(), bvc.into())?;
         let a3 = BitVectorSignedLessThanAtom::new(