Skip to content

Commit

Permalink
Dont include readme.md in doc
Browse files Browse the repository at this point in the history
  • Loading branch information
@novafacing
novafacing committed Aug 25, 2023
1 parent 08c7188 commit 191f1d0
Showing 1 changed file with 103 additions and 11 deletions.
114 changes: 103 additions & 11 deletions yices2/src/lib.rs
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,96 @@
#![doc = include_str!("../../README.md")]
//! # Yices2
//!
//! High level bindings to the Yices2 SMT solver.
//!
//! ## Examples
//!
//! Some examples to demonstrate usage of this library.
//!
//! ### Linear Real Arithmetic
//!
//! ```rust,no_run
//! use yices2::prelude::*;
//!
//! fn main() -> Result<(), Error> {
//! let config = Config::with_defaults_for_logics([Logic::QF_LRA])?;
//! let ctx = Context::with_config(&config)?;
//! let x = Uninterpreted::with_name(RealType::new()?.into(), "x")?;
//! let y = Uninterpreted::with_name(RealType::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()?.get_double(&x.into())?;
//! let yv = ctx.model()?.get_double(&y.into())?;
//! assert_eq!(xv, 2.0);
//! assert_eq!(yv, -1.0);
//!
//! Ok(())
//! }
//! ```
//!
//! ### BitVectors
//!
//! ```rust,no_run
//! use yices2::prelude::*;
//!
//! fn main() -> Result<(), Error> {
//! let config = Config::with_defaults_for_logics([Logic::QF_BV])?;
//! let ctx = Context::with_config(&config)?;
//! let bv = BitVectorType::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);
//!
//! Ok(())
//! }
//! ```
//!
//! ## 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 }
//! ```
//!
//! ## Notes
//!
//! This library is not thread safe, because the underlying `Yices2` library is not thread
//! safe. Do not use this library in multithreaded code. To use in multi-threaded code,
//! create a separate process and submit requests to the solver running in that process or
//! disable the `ctor` feature and manage state yourself.

// Allow unused unsafe because the yices! macro is sometimes not unsafe but having two
// versions of it would be silly
#![allow(unused_unsafe)]
Expand Down Expand Up @@ -90,14 +182,14 @@ mod ctor_test {
BitVectorSignedLessThanAtom, Equal, GcTerm, IfThenElse, IntegerDivision, Mul,
NamedTerm, Or, Power, Square, Sub, Term, Uninterpreted,
},
typ::{BitVectorType, BoolType, IntegerType, RealType},
typ::{BitVector, Bool, Integer, Real},
};
use anyhow::Result;

#[test]
/// mcsat_example.c test case
fn test_example_mcsat() -> Result<()> {
let x = Uninterpreted::new(RealType::new()?.into())?;
let x = Uninterpreted::new(Real::new()?.into())?;
x.set_name("x")?;
let p: Term = "(= (* x x) 2)".parse()?;
let config = Config::with_defaults_for_logics([Logic::QF_NRA])?;
Expand All @@ -120,7 +212,7 @@ mod ctor_test {
let config = Config::with_defaults_for_logics([Logic::QF_NIA])?;
let ctx = Context::with_config(&config)?;

let x = Uninterpreted::new(IntegerType::new()?.into())?;
let x = Uninterpreted::new(Integer::new()?.into())?;
x.set_name("x")?;

let t1 = IfThenElse::new(
Expand Down Expand Up @@ -166,7 +258,7 @@ mod ctor_test {
let config = Config::with_defaults_for_logics([Logic::QF_NIA])?;
let ctx = Context::with_config(&config)?;

let x = Uninterpreted::new(IntegerType::new()?.into())?;
let x = Uninterpreted::new(Integer::new()?.into())?;
x.set_name("x")?;

let one = ArithmeticConstant::from_i32(1)?;
Expand All @@ -190,7 +282,7 @@ mod ctor_test {
fn refcount_issue() -> Result<()> {
reset();

let bool_type = BoolType::new()?;
let bool_type = Bool::new()?;

for _ in 0..255 {
let t = Uninterpreted::new(bool_type.into())?;
Expand All @@ -206,7 +298,7 @@ mod ctor_test {

let config = Config::with_defaults_for_logics([Logic::QF_NIA])?;
let ctx = Context::with_config(&config)?;
let x = Uninterpreted::new(IntegerType::new()?.into())?;
let x = Uninterpreted::new(Integer::new()?.into())?;
x.set_name("x")?;

let power_term = Power::new(Square::new(x.into())?.into(), 2)?;
Expand Down Expand Up @@ -239,7 +331,7 @@ mod ctor_test {

let config = Config::with_defaults_for_logics([Logic::QF_LIA])?;
let ctx = Context::with_config(&config)?;
let x = Uninterpreted::new(IntegerType::new()?.into())?;
let x = Uninterpreted::new(Integer::new()?.into())?;
x.set_name("x")?;
let r_1 = IntegerDivision::new(x.into(), ArithmeticConstant::from_i32(2)?.into())?;
let check_zero_t1 =
Expand All @@ -260,8 +352,8 @@ mod ctor_test {

let config = Config::with_defaults_for_logics([Logic::QF_LRA])?;
let ctx = Context::with_config(&config)?;
let x = Uninterpreted::with_name(RealType::new()?.into(), "x")?;
let y = Uninterpreted::with_name(RealType::new()?.into(), "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())?;
let t2 = ArithmeticGreaterThanAtom::new(t1.into(), ArithmeticConstant::zero()?.into())?;
let t3 = Or::new([
Expand All @@ -284,7 +376,7 @@ mod ctor_test {

let config = Config::with_defaults_for_logics([Logic::QF_BV])?;
let ctx = Context::with_config(&config)?;
let bv = BitVectorType::new(32)?;
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")?;
Expand Down

0 comments on commit 191f1d0

Please sign in to comment.