diff --git a/Cargo.toml b/Cargo.toml index 8fd1675..28d5338 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,7 +14,12 @@ members = [ "examples/ollvm", "examples/statically-linked" ] +exclude = ["vendor/boolector"] [profile.release] lto = true opt-level=3 + +[patch.crates-io] +# boolector 0.4.3 compares ftell() output against an i64 constant, which fails on Windows. +boolector = { path = "vendor/boolector" } diff --git a/radius/Cargo.toml b/radius/Cargo.toml index a3b9c43..3f94ea0 100644 --- a/radius/Cargo.toml +++ b/radius/Cargo.toml @@ -19,7 +19,13 @@ rand = "0.8.4" colored = "2.0.0" [features] -default = ["boolector/vendor-lgl"] +default = [] + +[target.'cfg(not(windows))'.dependencies] +boolector = { version = "0.4.3", features = ["vendor-lgl"] } + +[target.'cfg(windows)'.dependencies] +boolector = "0.4.3" [package.metadata.docs.rs] no-default-features = true diff --git a/vendor/boolector/Cargo.lock b/vendor/boolector/Cargo.lock new file mode 100644 index 0000000..da4cc37 --- /dev/null +++ b/vendor/boolector/Cargo.lock @@ -0,0 +1,170 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 4 + +[[package]] +name = "boolector" +version = "0.4.3" +dependencies = [ + "boolector-sys", + "libc", +] + +[[package]] +name = "boolector-sys" +version = "0.7.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "17f0c2f69c37174fb92110f2949c79ad87f6ab48bf45e2e3220b669c10698093" +dependencies = [ + "cc", + "cmake", + "copy_dir", + "libc", +] + +[[package]] +name = "cc" +version = "1.2.56" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "aebf35691d1bfb0ac386a69bac2fde4dd276fb618cf8bf4f5318fe285e821bb2" +dependencies = [ + "find-msvc-tools", + "shlex", +] + +[[package]] +name = "cmake" +version = "0.1.57" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "75443c44cd6b379beb8c5b45d85d0773baf31cce901fe7bb252f4eff3008ef7d" +dependencies = [ + "cc", +] + +[[package]] +name = "copy_dir" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "543d1dd138ef086e2ff05e3a48cf9da045da2033d16f8538fd76b86cd49b2ca3" +dependencies = [ + "walkdir", +] + +[[package]] +name = "find-msvc-tools" +version = "0.1.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5baebc0774151f905a1a2cc41989300b1e6fbb29aff0ceffa1064fdd3088d582" + +[[package]] +name = "libc" +version = "0.2.182" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6800badb6cb2082ffd7b6a67e6125bb39f18782f793520caee8cb8846be06112" + +[[package]] +name = "same-file" +version = "1.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "93fc1dc3aaa9bfed95e02e6eadabb4baf7e3078b0bd1b4d7b6b0b68378900502" +dependencies = [ + "winapi-util", +] + +[[package]] +name = "shlex" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64" + +[[package]] +name = "walkdir" +version = "2.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29790946404f91d9c5d06f9874efddea1dc06c5efe94541a7d6863108e3a5e4b" +dependencies = [ + "same-file", + "winapi-util", +] + +[[package]] +name = "winapi-util" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22" +dependencies = [ + "windows-sys", +] + +[[package]] +name = "windows-sys" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" +dependencies = [ + "windows-targets", +] + +[[package]] +name = "windows-targets" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_gnullvm", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", +] + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" + +[[package]] +name = "windows_i686_gnu" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" + +[[package]] +name = "windows_i686_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" + +[[package]] +name = "windows_i686_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.52.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" diff --git a/vendor/boolector/Cargo.toml b/vendor/boolector/Cargo.toml new file mode 100644 index 0000000..9d8ffd7 --- /dev/null +++ b/vendor/boolector/Cargo.toml @@ -0,0 +1,29 @@ +# THIS FILE IS AUTOMATICALLY GENERATED BY CARGO +# +# When uploading crates to the registry Cargo will automatically +# "normalize" Cargo.toml files for maximal compatibility +# with all versions of Cargo and also rewrite `path` dependencies +# to registry (e.g., crates.io) dependencies. +# +# If you are reading this file be aware that the original Cargo.toml +# will likely look very different (and much more reasonable). +# See Cargo.toml.orig for the original contents. + +[package] +edition = "2018" +name = "boolector" +version = "0.4.3" +authors = ["Craig Disselkoen "] +description = "Safe high-level bindings for the Boolector SMT solver" +documentation = "https://docs.rs/boolector" +keywords = ["boolector", "smt", "ffi", "bindings"] +license = "MIT" +repository = "https://github.com/cdisselkoen/boolector-rs" +[dependencies.boolector-sys] +version = "0.7.1" + +[dependencies.libc] +version = "0.2.73" + +[features] +vendor-lgl = ["boolector-sys/vendor-lgl"] diff --git a/vendor/boolector/LICENSE b/vendor/boolector/LICENSE new file mode 100644 index 0000000..655e5ab --- /dev/null +++ b/vendor/boolector/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2019 Craig Disselkoen + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/vendor/boolector/src/btor.rs b/vendor/boolector/src/btor.rs new file mode 100644 index 0000000..ea4a2f8 --- /dev/null +++ b/vendor/boolector/src/btor.rs @@ -0,0 +1,797 @@ +use crate::node::{Array, BV}; +use crate::option::BtorOption; +use crate::option::*; +use crate::timeout::{self, TimeoutState}; +use boolector_sys::*; +use std::borrow::Borrow; +use std::ffi::{CStr, CString}; +use std::fmt; +use std::os::raw::{c_char, c_void}; +use std::pin::Pin; + +/// A `Btor` represents an instance of the Boolector solver. +/// Each `BV` and `Array` is created in a particular `Btor` instance. +pub struct Btor { + btor: *mut boolector_sys::Btor, + pub(crate) timeout_state: Pin>, // needs to be `Pin`, because the Boolector callback will expect to continue to find the `TimeoutState` at the same location +} + +// Two `Btor`s are equal if they have the same underlying Btor pointer. +// We disregard the `timeout_state` for this purpose. +impl PartialEq for Btor { + fn eq(&self, other: &Self) -> bool { + self.btor == other.btor + } +} + +impl Eq for Btor {} + +impl fmt::Debug for Btor { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + write!(f, "", self.btor) + } +} + +/// According to +/// https://groups.google.com/forum/#!msg/boolector/itYGgJxU3mY/AC2O0898BAAJ, +/// the Boolector library is thread-safe, so we make `Btor` both `Send` and +/// `Sync`. (Note that `TimeoutState` is also careful to be both `Send` and +/// `Sync`.) +unsafe impl Send for Btor {} +unsafe impl Sync for Btor {} + +impl Btor { + /// Create a new `Btor` instance with no variables and no constraints. + pub fn new() -> Self { + Self { + btor: unsafe { boolector_new() }, + timeout_state: Pin::new(Box::new(timeout::TimeoutState::new())), + } + } + + pub(crate) fn as_raw(&self) -> *mut boolector_sys::Btor { + self.btor + } + + /// Set an option to a particular value. + #[allow(clippy::cognitive_complexity)] + pub fn set_opt(&self, opt: BtorOption) { + match opt { + BtorOption::ModelGen(mg) => { + let val = match mg { + ModelGen::Disabled => 0, + ModelGen::Asserted => 1, + ModelGen::All => 2, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_MODEL_GEN, val) } + }, + BtorOption::Incremental(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_INCREMENTAL, if b { 1 } else { 0 }) + }, + BtorOption::IncrementalSMT1(ismt1) => { + let val = match ismt1 { + IncrementalSMT1::Basic => BTOR_INCREMENTAL_SMT1_BASIC, + IncrementalSMT1::Continue => BTOR_INCREMENTAL_SMT1_CONTINUE, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_INCREMENTAL_SMT1, val) } + }, + BtorOption::InputFileFormat(iff) => { + let val = match iff { + InputFileFormat::Autodetect => BTOR_INPUT_FORMAT_NONE, + InputFileFormat::Btor => BTOR_INPUT_FORMAT_BTOR, + InputFileFormat::Btor2 => BTOR_INPUT_FORMAT_BTOR2, + InputFileFormat::SMTLIBv1 => BTOR_INPUT_FORMAT_SMT1, + InputFileFormat::SMTLIBv2 => BTOR_INPUT_FORMAT_SMT2, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_INPUT_FORMAT, val) } + }, + BtorOption::OutputNumberFormat(nf) => { + let val = match nf { + NumberFormat::Binary => BTOR_OUTPUT_BASE_BIN, + NumberFormat::Decimal => BTOR_OUTPUT_BASE_DEC, + NumberFormat::Hexadecimal => BTOR_OUTPUT_BASE_HEX, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_OUTPUT_NUMBER_FORMAT, val) } + }, + BtorOption::OutputFileFormat(off) => { + let val = match off { + OutputFileFormat::BTOR => BTOR_OUTPUT_FORMAT_BTOR, + OutputFileFormat::SMTLIBv2 => BTOR_OUTPUT_FORMAT_SMT2, + OutputFileFormat::AigerASCII => BTOR_OUTPUT_FORMAT_AIGER_ASCII, + OutputFileFormat::AigerBinary => BTOR_OUTPUT_FORMAT_AIGER_BINARY, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_OUTPUT_FORMAT, val) } + }, + BtorOption::SolverTimeout(duration) => { + self.timeout_state.set_timeout_duration(duration); + match duration { + None => { + // remove any existing timeout + unsafe { boolector_set_term(self.as_raw(), None, std::ptr::null_mut()) } + }, + Some(_) => { + let ptr_to_ts: Pin<&TimeoutState> = (&self.timeout_state).as_ref(); + let raw_ptr_to_ts: *const TimeoutState = + Pin::into_inner(ptr_to_ts) as *const TimeoutState; + let void_ptr_to_ts: *mut c_void = raw_ptr_to_ts as *mut c_void; + unsafe { + boolector_set_term( + self.as_raw(), + Some(timeout::callback), + void_ptr_to_ts, + ) + } + }, + } + }, + BtorOption::SolverEngine(se) => { + let val = match se { + SolverEngine::Fun => BTOR_ENGINE_FUN, + SolverEngine::SLS => BTOR_ENGINE_SLS, + SolverEngine::Prop => BTOR_ENGINE_PROP, + SolverEngine::AIGProp => BTOR_ENGINE_AIGPROP, + SolverEngine::Quant => BTOR_ENGINE_QUANT, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_ENGINE, val) } + }, + BtorOption::SatEngine(se) => { + let val = match se { + SatEngine::CaDiCaL => BTOR_SAT_ENGINE_CADICAL, + SatEngine::CMS => BTOR_SAT_ENGINE_CMS, + SatEngine::Lingeling => BTOR_SAT_ENGINE_LINGELING, + SatEngine::MiniSAT => BTOR_SAT_ENGINE_MINISAT, + SatEngine::PicoSAT => BTOR_SAT_ENGINE_PICOSAT, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_SAT_ENGINE, val) } + }, + BtorOption::AutoCleanup(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_AUTO_CLEANUP, if b { 1 } else { 0 }) + }, + BtorOption::PrettyPrint(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PRETTY_PRINT, if b { 1 } else { 0 }) + }, + BtorOption::Seed(u) => unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_SEED, u) }, + BtorOption::RewriteLevel(rl) => { + let val = match rl { + RewriteLevel::None => 0, + RewriteLevel::TermLevel => 1, + RewriteLevel::More => 2, + RewriteLevel::Full => 3, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_REWRITE_LEVEL, val) } + }, + BtorOption::SkeletonPreproc(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_SKELETON_PREPROC, + if b { 1 } else { 0 }, + ) + }, + BtorOption::Ackermann(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_ACKERMANN, if b { 1 } else { 0 }) + }, + BtorOption::BetaReduce(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_BETA_REDUCE, if b { 1 } else { 0 }) + }, + BtorOption::EliminateSlices(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_ELIMINATE_SLICES, + if b { 1 } else { 0 }, + ) + }, + BtorOption::VariableSubst(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_VAR_SUBST, if b { 1 } else { 0 }) + }, + BtorOption::UnconstrainedOpt(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_UCOPT, if b { 1 } else { 0 }) + }, + BtorOption::MergeLambdas(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_MERGE_LAMBDAS, if b { 1 } else { 0 }) + }, + BtorOption::ExtractLambdas(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_EXTRACT_LAMBDAS, + if b { 1 } else { 0 }, + ) + }, + BtorOption::Normalize(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_NORMALIZE, if b { 1 } else { 0 }) + }, + BtorOption::NormalizeAdd(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_NORMALIZE_ADD, if b { 1 } else { 0 }) + }, + BtorOption::FunPreProp(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_PREPROP, if b { 1 } else { 0 }) + }, + BtorOption::FunPreSLS(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_PRESLS, if b { 1 } else { 0 }) + }, + BtorOption::FunDualProp(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_DUAL_PROP, if b { 1 } else { 0 }) + }, + BtorOption::FunDualPropQsortOrder(dpqo) => { + let val = match dpqo { + DualPropQsortOrder::Just => BTOR_DP_QSORT_JUST, + DualPropQsortOrder::Asc => BTOR_DP_QSORT_ASC, + DualPropQsortOrder::Desc => BTOR_DP_QSORT_DESC, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_DUAL_PROP_QSORT, val) } + }, + BtorOption::FunJustification(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_JUST, if b { 1 } else { 0 }) + }, + BtorOption::FunJustificationHeuristic(jh) => { + let val = match jh { + JustificationHeuristic::Left => BTOR_JUST_HEUR_BRANCH_LEFT, + JustificationHeuristic::MinApp => BTOR_JUST_HEUR_BRANCH_MIN_APP, + JustificationHeuristic::MinDepth => BTOR_JUST_HEUR_BRANCH_MIN_DEP, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_JUST_HEURISTIC, val) } + }, + BtorOption::FunLazySynthesize(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_FUN_LAZY_SYNTHESIZE, + if b { 1 } else { 0 }, + ) + }, + BtorOption::FunEagerLemmas(el) => { + let val = match el { + EagerLemmas::None => BTOR_FUN_EAGER_LEMMAS_NONE, + EagerLemmas::Conf => BTOR_FUN_EAGER_LEMMAS_CONF, + EagerLemmas::All => BTOR_FUN_EAGER_LEMMAS_ALL, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_FUN_EAGER_LEMMAS, val) } + }, + BtorOption::SLSNumFlips(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_NFLIPS, u) + }, + BtorOption::SLSMoveStrategy(sms) => { + let val = match sms { + SLSMoveStrategy::BestMove => 0, + SLSMoveStrategy::RandomWalk => 1, + SLSMoveStrategy::FirstBestMove => 2, + SLSMoveStrategy::BestSameMove => 3, + SLSMoveStrategy::AlwaysProp => 4, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_STRATEGY, val) } + }, + BtorOption::SLSJustification(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_JUST, if b { 1 } else { 0 }) + }, + BtorOption::SLSGroupWiseMoves(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_MOVE_GW, if b { 1 } else { 0 }) + }, + BtorOption::SLSRangeWiseMoves(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_SLS_MOVE_RANGE, + if b { 1 } else { 0 }, + ) + }, + BtorOption::SLSSegmentWiseMoves(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_SLS_MOVE_SEGMENT, + if b { 1 } else { 0 }, + ) + }, + BtorOption::SLSRandomWalkMoves(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_SLS_MOVE_RAND_WALK, + if b { 1 } else { 0 }, + ) + }, + BtorOption::SLSRandomWalkProbability(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_PROB_MOVE_RAND_WALK, u) + }, + BtorOption::SLSRandomizeAll(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_SLS_MOVE_RAND_ALL, + if b { 1 } else { 0 }, + ) + }, + BtorOption::SLSRandomizeRange(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_SLS_MOVE_RAND_RANGE, + if b { 1 } else { 0 }, + ) + }, + BtorOption::SLSPropagationMoves(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_MOVE_PROP, if b { 1 } else { 0 }) + }, + BtorOption::SLSPropagationMovesNumProp(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_MOVE_PROP_N_PROP, u) + }, + BtorOption::SLSPropagationMovesNumRegular(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_SLS_MOVE_PROP_N_SLS, u) + }, + BtorOption::SLSForceRandomWalks(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_SLS_MOVE_PROP_FORCE_RW, + if b { 1 } else { 0 }, + ) + }, + BtorOption::SLSIncMoveTest(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_SLS_MOVE_INC_MOVE_TEST, + if b { 1 } else { 0 }, + ) + }, + BtorOption::SLSRestarts(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_SLS_USE_RESTARTS, + if b { 1 } else { 0 }, + ) + }, + BtorOption::SLSBanditScheme(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_SLS_USE_BANDIT, + if b { 1 } else { 0 }, + ) + }, + BtorOption::PropNumSteps(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_NPROPS, u) + }, + BtorOption::PropRestarts(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_PROP_USE_RESTARTS, + if b { 1 } else { 0 }, + ) + }, + BtorOption::PropBanditScheme(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_PROP_USE_BANDIT, + if b { 1 } else { 0 }, + ) + }, + BtorOption::PropPathSelectionMode(pathsel) => { + let val = match pathsel { + PropPathSelection::Controlling => BTOR_PROP_PATH_SEL_CONTROLLING, + PropPathSelection::Essential => BTOR_PROP_PATH_SEL_ESSENTIAL, + PropPathSelection::Random => BTOR_PROP_PATH_SEL_RANDOM, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PATH_SEL, val) } + }, + BtorOption::PropInvValueProbability(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_USE_INV_VALUE, u) + }, + BtorOption::PropFlipConditionProbability(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_FLIP_COND, u) + }, + BtorOption::PropFlipConditionProbabilityConstant(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_FLIP_COND_CONST, u) + }, + BtorOption::PropFlipConditionNumPaths(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_FLIP_COND_CONST_NPATHSEL, u) + }, + BtorOption::PropFlipConditionProbabilityConstantDelta(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_FLIP_COND_CONST_DELTA, u) + }, + BtorOption::PropSliceKeepDCProbability(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_SLICE_KEEP_DC, u) + }, + BtorOption::PropConcatFlipProbability(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_CONC_FLIP, u) + }, + BtorOption::PropSliceFlipProbability(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_SLICE_FLIP, u) + }, + BtorOption::PropEqFlipProbability(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_EQ_FLIP, u) + }, + BtorOption::PropAndFlipProbability(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_PROP_PROB_AND_FLIP, u) + }, + BtorOption::AIGPropUseRestarts(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_AIGPROP_USE_RESTARTS, + if b { 1 } else { 0 }, + ) + }, + BtorOption::AIGPropQuantSynthesis(pqs) => { + let val = match pqs { + AIGPropQuantSynthesis::None => BTOR_QUANT_SYNTH_NONE, + AIGPropQuantSynthesis::EL => BTOR_QUANT_SYNTH_EL, + AIGPropQuantSynthesis::ELMC => BTOR_QUANT_SYNTH_ELMC, + AIGPropQuantSynthesis::ELELMC => BTOR_QUANT_SYNTH_EL_ELMC, + AIGPropQuantSynthesis::ELMR => BTOR_QUANT_SYNTH_ELMR, + }; + unsafe { boolector_set_opt(self.as_raw(), BTOR_OPT_QUANT_SYNTH, val) } + }, + BtorOption::AIGPropQuantDualSolver(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_QUANT_DUAL_SOLVER, + if b { 1 } else { 0 }, + ) + }, + BtorOption::AIGPropQuantSynthLimit(u) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_QUANT_SYNTH_LIMIT, u) + }, + BtorOption::AIGPropSynthQI(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_QUANT_SYNTH_QI, + if b { 1 } else { 0 }, + ) + }, + BtorOption::AIGPropQuantDER(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_QUANT_DER, if b { 1 } else { 0 }) + }, + BtorOption::AIGPropQuantCER(b) => unsafe { + boolector_set_opt(self.as_raw(), BTOR_OPT_QUANT_CER, if b { 1 } else { 0 }) + }, + BtorOption::AIGPropQuantMiniscope(b) => unsafe { + boolector_set_opt( + self.as_raw(), + BTOR_OPT_QUANT_MINISCOPE, + if b { 1 } else { 0 }, + ) + }, + } + } + + /// Solve the current input (defined by the constraints which have been added + /// via [`BV::assert()`](struct.BV.html#method.assert) and + /// [`BV::assume()`](struct.BV.html#method.assume)). All assertions and + /// assumptions are implicitly combined via Boolean `and`. + /// + /// Calling this function multiple times requires incremental usage to be + /// enabled via [`Btor::set_opt()`](struct.Btor.html#method.set_opt). + /// If incremental usage is not enabled, this function may only be called + /// once. + /// + /// ``` + /// # use boolector::{Btor, BV, SolverResult}; + /// # use boolector::option::{BtorOption, ModelGen}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// btor.set_opt(BtorOption::Incremental(true)); + /// + /// // An 8-bit unconstrained `BV` with the symbol "foo" + /// let foo = BV::new(btor.clone(), 8, Some("foo")); + /// + /// // Assert that "foo" must be greater than `3` + /// foo.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert(); + /// + /// // This state is satisfiable + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// + /// // Assert that "foo" must also be less than `2` + /// foo.ult(&BV::from_u32(btor.clone(), 2, 8)).assert(); + /// + /// // State is now unsatisfiable + /// assert_eq!(btor.sat(), SolverResult::Unsat); + /// + /// // Repeat the first step above with the solver timeout set to something + /// // extremely high (say, 200 sec) - should still be `Sat` + /// # use std::time::Duration; + /// let btor = Rc::new(Btor::new()); + /// btor.set_opt(BtorOption::Incremental(true)); + /// btor.set_opt(BtorOption::SolverTimeout(Some(Duration::from_secs(200)))); + /// let foo = BV::new(btor.clone(), 8, Some("foo")); + /// foo.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert(); + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// + /// // But, if we make the second assertion and then set the solver timeout to + /// // something extremely low (say, 2 ns), we'll get `SolverResult::Unknown` + /// foo.ugt(&BV::from_u32(btor.clone(), 5, 8)).assert(); + /// btor.set_opt(BtorOption::SolverTimeout(Some(Duration::from_nanos(2)))); + /// assert_eq!(btor.sat(), SolverResult::Unknown); + /// ``` + pub fn sat(&self) -> SolverResult { + self.timeout_state.restart_timer(); + #[allow(non_upper_case_globals)] + match unsafe { boolector_sat(self.as_raw()) } as u32 { + BtorSolverResult_BTOR_RESULT_SAT => SolverResult::Sat, + BtorSolverResult_BTOR_RESULT_UNSAT => SolverResult::Unsat, + BtorSolverResult_BTOR_RESULT_UNKNOWN => SolverResult::Unknown, + u => panic!("Unexpected return value from boolector_sat(): {}", u), + } + } + + /// Push `n` context levels. `n` must be at least 1. + pub fn push(&self, n: u32) { + unsafe { boolector_push(self.as_raw(), n) } + } + + /// Pop `n` context levels. `n` must be at least 1. + pub fn pop(&self, n: u32) { + unsafe { boolector_pop(self.as_raw(), n) } + } + + /// Duplicate a `Btor` instance. This will copy all variables, assertions, + /// etc into the new instance. + /// + /// Each `BV` or `Array` may only be used with the `Btor` it was originally + /// created for. If you have a `BV` for one `Btor` and want to find the + /// corresponding `BV` in another `Btor`, use + /// [`Btor::get_matching_bv()`](struct.Btor.html#method.get_matching_bv) or + /// [`Btor::get_bv_by_symbol()`](struct.Btor.html#method.get_bv_by_symbol). + /// + /// With [`SatEngine::Lingeling`](option/enum.SatEngine.html), this can be + /// called at any time; but with `SatEngine::PicoSAT` or + /// `SatEngine::MiniSAT`, this can only be called prior to the first + /// `Btor::sat()` call. + /// + /// The Boolector API docs refer to this operation as "clone", but we use + /// `duplicate()` to avoid confusion. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV, SolverResult}; + /// # use boolector::option::{BtorOption, ModelGen}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// btor.set_opt(BtorOption::ModelGen(ModelGen::All)); + /// + /// // `x` is an 8-bit `BV` less than `42` + /// let x = BV::new(btor.clone(), 8, Some("x")); + /// x.ult(&BV::from_u32(btor.clone(), 42, 8)).assert(); + /// + /// // `y` is equal to `x + 7` + /// let y = x.add(&BV::from_u32(btor.clone(), 7, 8)); + /// + /// // We duplicate the `Btor` instance + /// let btor_2 = Rc::new(btor.duplicate()); + /// + /// // The duplicated instance has copied versions of + /// // `x` and `y` which are distinct from the original + /// // `x` and `y` but still have the corresponding + /// // relationship (i.e., `y_2 = x_2 + 7`) + /// let x_2 = Btor::get_matching_bv(btor_2.clone(), &x).unwrap(); + /// let y_2 = Btor::get_matching_bv(btor_2.clone(), &y).unwrap(); + /// + /// // The instances are totally independent now. In the + /// // original instance, we'll assert that `x > 3`, while + /// // in the new instance, we'll assert that `x < 3`. + /// // Note that we're careful to create constants with the + /// // correct `Btor` instance. + /// x.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert(); + /// x_2.ult(&BV::from_u32(btor_2.clone(), 3, 8)).assert(); + /// + /// // Each instance is satisfiable by itself + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// assert_eq!(btor_2.sat(), SolverResult::Sat); + /// + /// // In the first instance, `y > 10`, while in the second, + /// // `y < 10` + /// let y_solution = y.get_a_solution().as_u64().unwrap(); + /// assert!(y_solution > 10); + /// let y_2_solution = y_2.get_a_solution().as_u64().unwrap(); + /// assert!(y_2_solution < 10); + /// ``` + pub fn duplicate(&self) -> Self { + let duplicated = Self { + btor: unsafe { boolector_clone(self.as_raw()) }, + timeout_state: Pin::new(Box::new(TimeoutState::with_timeout_duration( + self.timeout_state.get_timeout_duration(), + ))), + }; + // we need to inform the callback about the new location of the `TimeoutState` + let ptr_to_ts: Pin<&TimeoutState> = (&self.timeout_state).as_ref(); + let raw_ptr_to_ts: *const TimeoutState = Pin::into_inner(ptr_to_ts) as *const TimeoutState; + let void_ptr_to_ts: *mut c_void = raw_ptr_to_ts as *mut c_void; + unsafe { boolector_set_term(self.as_raw(), Some(timeout::callback), void_ptr_to_ts) } + duplicated + } + + /// Given a `BV` originally created for any `Btor`, get the corresponding + /// `BV` in the given `btor`. This only works if the `BV` was created before + /// the relevant `Btor::duplicate()` was called; that is, it is intended to + /// be used to find the copied version of a given `BV` in the new `Btor`. + /// + /// It's also fine to call this with a `BV` created for the given `Btor` + /// itself, in which case you'll just get back `Some(bv.clone())`. + /// + /// For a code example, see + /// [`Btor::duplicate()`](struct.Btor.html#method.duplicate). + #[allow(clippy::if_same_then_else)] + pub fn get_matching_bv + Clone>(btor: R, bv: &BV) -> Option> { + let node = unsafe { boolector_match_node(btor.borrow().as_raw(), bv.node) }; + if node.is_null() { + None + } else if unsafe { boolector_is_array(btor.borrow().as_raw(), node) } { + None + } else { + Some(BV { btor, node }) + } + } + + /// Given an `Array` originally created for any `Btor`, get the corresponding + /// `Array` in the given `btor`. This only works if the `Array` was created + /// before the relevant `Btor::duplicate()` was called; that is, it is + /// intended to be used to find the copied version of a given `Array` in the + /// new `Btor`. + /// + /// It's also fine to call this with an `Array` created for the given `Btor` + /// itself, in which case you'll just get back `Some(array.clone())`. + pub fn get_matching_array + Clone>( + btor: R, + array: &Array, + ) -> Option> { + let node = unsafe { boolector_match_node(btor.borrow().as_raw(), array.node) }; + if node.is_null() { + None + } else if unsafe { boolector_is_array(btor.borrow().as_raw(), node) } { + Some(Array { btor, node }) + } else { + None + } + } + + /// Given a symbol, find the `BV` in the given `Btor` which has that symbol. + /// + /// Since `Btor::duplicate()` copies all `BV`s to the new `Btor` including + /// their symbols, this can also be used to find the copied version of a + /// given `BV` in the new `Btor`. + #[allow(clippy::if_same_then_else)] + pub fn get_bv_by_symbol + Clone>(btor: R, symbol: &str) -> Option> { + let cstring = CString::new(symbol).unwrap(); + let symbol = cstring.as_ptr() as *const c_char; + let node = unsafe { boolector_match_node_by_symbol(btor.borrow().as_raw(), symbol) }; + if node.is_null() { + None + } else if unsafe { boolector_is_array(btor.borrow().as_raw(), node) } { + None + } else { + Some(BV { btor, node }) + } + } + + /// Given a symbol, find the `Array` in the given `Btor` which has that + /// symbol. + /// + /// Since `Btor::duplicate()` copies all `Array`s to the new `Btor` including + /// their symbols, this can also be used to find the copied version of a + /// given `Array` in the new `Btor`. + pub fn get_array_by_symbol + Clone>(btor: R, symbol: &str) -> Option> { + let cstring = CString::new(symbol).unwrap(); + let symbol = cstring.as_ptr() as *const c_char; + let node = unsafe { boolector_match_node_by_symbol(btor.borrow().as_raw(), symbol) }; + if node.is_null() { + None + } else if unsafe { boolector_is_array(btor.borrow().as_raw(), node) } { + Some(Array { btor, node }) + } else { + None + } + } + + /// Add all current assumptions as assertions + pub fn fixate_assumptions(&self) { + unsafe { boolector_fixate_assumptions(self.as_raw()) } + } + + /// Remove all added assumptions + pub fn reset_assumptions(&self) { + unsafe { boolector_reset_assumptions(self.as_raw()) } + } + + /// Reset all statistics other than time statistics + pub fn reset_stats(&self) { + unsafe { boolector_reset_stats(self.as_raw()) } + } + + /// Reset time statistics + pub fn reset_time(&self) { + unsafe { boolector_reset_time(self.as_raw()) } + } + + /// Get a `String` describing the current constraints + pub fn print_constraints(&self) -> String { + unsafe { + let tmpfile: *mut libc::FILE = libc::tmpfile(); + if tmpfile.is_null() { + panic!("Failed to create a temp file"); + } + // Write the data to `tmpfile` + boolector_dump_smt2(self.as_raw(), tmpfile); + // Seek to the end of `tmpfile` + assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_END), 0); + // Get the length of `tmpfile` + let length = libc::ftell(tmpfile); + if length < 0 { + panic!("ftell() returned a negative value"); + } + // Seek back to the beginning of `tmpfile` + assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_SET), 0); + let mut buffer = Vec::with_capacity(length as usize); + libc::fread( + buffer.as_mut_ptr() as *mut c_void, + 1, + length as usize, + tmpfile, + ); + libc::fclose(tmpfile); + buffer.set_len(length as usize); + String::from_utf8_unchecked(buffer) + } + } + + /// Get a `String` describing the current model, including a set of + /// satisfying assignments for all variables + pub fn print_model(&self) -> String { + unsafe { + let tmpfile: *mut libc::FILE = libc::tmpfile(); + if tmpfile.is_null() { + panic!("Failed to create a temp file"); + } + // Write the data to `tmpfile` + let format_cstring = CString::new("btor").unwrap(); + boolector_print_model( + self.as_raw(), + format_cstring.as_ptr() as *mut c_char, + tmpfile, + ); + // Seek to the end of `tmpfile` + assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_END), 0); + // Get the length of `tmpfile` + let length = libc::ftell(tmpfile); + if length < 0 { + panic!("ftell() returned a negative value"); + } + // Seek back to the beginning of `tmpfile` + assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_SET), 0); + let mut buffer = Vec::with_capacity(length as usize); + libc::fread( + buffer.as_mut_ptr() as *mut c_void, + 1, + length as usize, + tmpfile, + ); + libc::fclose(tmpfile); + buffer.set_len(length as usize); + String::from_utf8_unchecked(buffer) + } + } + + /// Get Boolector's version string + pub fn get_version(&self) -> String { + let cstr = unsafe { CStr::from_ptr(boolector_version(self.as_raw())) }; + cstr.to_str().unwrap().to_owned() + } + + /// Get Boolector's copyright notice + pub fn get_copyright(&self) -> String { + let cstr = unsafe { CStr::from_ptr(boolector_copyright(self.as_raw())) }; + cstr.to_str().unwrap().to_owned() + } +} + +impl Default for Btor { + fn default() -> Self { + Self::new() + } +} + +impl Drop for Btor { + fn drop(&mut self) { + unsafe { + boolector_release_all(self.as_raw()); + assert_eq!(boolector_get_refs(self.as_raw()) as i32, 0); + boolector_delete(self.as_raw()); + } + } +} + +#[derive(PartialEq, Eq, Clone, Copy, Debug)] +pub enum SolverResult { + Sat, + Unsat, + Unknown, +} diff --git a/vendor/boolector/src/lib.rs b/vendor/boolector/src/lib.rs new file mode 100644 index 0000000..b796740 --- /dev/null +++ b/vendor/boolector/src/lib.rs @@ -0,0 +1,13 @@ +// this ensures that crate users generating docs with --no-deps will still +// properly get links to the public docs for boolector's types +#![doc(html_root_url = "https://docs.rs/boolector/0.4.2")] + +mod btor; +pub use btor::{Btor, SolverResult}; +mod node; +pub use node::Array; +pub use node::BVSolution; +pub use node::BV; +pub mod option; +mod sort; +mod timeout; diff --git a/vendor/boolector/src/node.rs b/vendor/boolector/src/node.rs new file mode 100644 index 0000000..5872e1a --- /dev/null +++ b/vendor/boolector/src/node.rs @@ -0,0 +1,1476 @@ +use crate::btor::Btor; +use crate::sort::Sort; +use boolector_sys::*; +use std::borrow::Borrow; +use std::ffi::{CStr, CString}; +use std::fmt; +use std::os::raw::{c_char, c_void}; + +/// A bitvector object: that is, a single symbolic value, consisting of some +/// number of symbolic bits. +/// +/// This is generic in the `Btor` reference type. +/// For instance, you could use `BV>` for single-threaded applications, +/// or `BV>` for multi-threaded applications. +#[derive(PartialEq, Eq)] +pub struct BV + Clone> { + pub(crate) btor: R, + pub(crate) node: *mut BoolectorNode, +} + +// According to +// https://groups.google.com/forum/#!msg/boolector/itYGgJxU3mY/AC2O0898BAAJ, +// the Boolector library is thread-safe, meaning `*mut BoolectorNode` can be +// both `Send` and `Sync`. +// So as long as `R` is `Send` and/or `Sync`, we can mark `BV` as `Send` and/or +// `Sync` respectively. +unsafe impl + Clone + Send> Send for BV {} +unsafe impl + Clone + Sync> Sync for BV {} + +// The attr:meta stuff is so that doc comments work correctly. +// See https://stackoverflow.com/questions/41361897/documenting-a-function-created-with-a-macro-in-rust +macro_rules! unop { + ( $(#[$attr:meta])* => $f:ident, $rawfn:ident ) => { + $(#[$attr])* + pub fn $f(&self) -> Self { + Self { + btor: self.btor.clone(), + node: unsafe { $rawfn(self.btor.borrow().as_raw(), self.node) }, + } + } + }; +} + +// The attr:meta stuff is so that doc comments work correctly. +// See https://stackoverflow.com/questions/41361897/documenting-a-function-created-with-a-macro-in-rust +macro_rules! binop { + ( $(#[$attr:meta])* => $f:ident, $rawfn:ident ) => { + $(#[$attr])* + pub fn $f(&self, other: &Self) -> Self { + Self { + btor: self.btor.clone(), + node: unsafe { $rawfn(self.btor.borrow().as_raw(), self.node, other.node) }, + } + } + }; +} + +impl + Clone> BV { + /// Create a new unconstrained `BV` variable of the given `width`. + /// + /// The `symbol`, if present, will be used to identify the `BV` when printing + /// a model or dumping to file. It must be unique if it is present. + /// + /// `width` must not be 0. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV, SolverResult}; + /// # use boolector::option::{BtorOption, ModelGen}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// btor.set_opt(BtorOption::ModelGen(ModelGen::All)); + /// + /// // An 8-bit unconstrained `BV` with the symbol "foo" + /// let bv = BV::new(btor.clone(), 8, Some("foo")); + /// + /// // Assert that it must be greater than `3` + /// bv.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert(); + /// + /// // Now any solution must give it a value greater than `3` + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// let solution = bv.get_a_solution().as_u64().unwrap(); + /// assert!(solution > 3); + /// ``` + pub fn new(btor: R, width: u32, symbol: Option<&str>) -> Self { + let sort = Sort::bitvector(btor.clone(), width); + let node = match symbol { + None => unsafe { + boolector_var(btor.borrow().as_raw(), sort.as_raw(), std::ptr::null()) + }, + Some(symbol) => { + let cstring = CString::new(symbol).unwrap(); + let symbol = cstring.as_ptr() as *const c_char; + unsafe { boolector_var(btor.borrow().as_raw(), sort.as_raw(), symbol) } + }, + }; + Self { btor, node } + } + + /// Create a new constant `BV` representing the given `bool` (either constant + /// `true` or constant `false`). + /// + /// The resulting `BV` will be either constant `0` or constant `1`, and will + /// have bitwidth 1. + pub fn from_bool(btor: R, b: bool) -> Self { + Self { + node: { + if b { + unsafe { boolector_true(btor.borrow().as_raw()) } + } else { + unsafe { boolector_false(btor.borrow().as_raw()) } + } + }, + btor, // out of order so it can be used above but moved in here + } + } + + /// Create a new constant `BV` representing the given signed integer. + /// The new `BV` will have the width `width`, which must not be 0. + pub fn from_i32(btor: R, i: i32, width: u32) -> Self { + let sort = Sort::bitvector(btor.clone(), width); + Self { + node: unsafe { boolector_int(btor.borrow().as_raw(), i, sort.as_raw()) }, + btor, // out of order so it can be used above but moved in here + } + } + + /// Create a new constant `BV` representing the given unsigned integer. + /// The new `BV` will have the width `width`, which must not be 0. + /// + /// For a code example, see [`BV::new()`](struct.BV.html#method.new). + pub fn from_u32(btor: R, u: u32, width: u32) -> Self { + let sort = Sort::bitvector(btor.clone(), width); + Self { + node: unsafe { boolector_unsigned_int(btor.borrow().as_raw(), u, sort.as_raw()) }, + btor, // out of order so it can be used above but moved in here + } + } + + /// Create a new constant `BV` representing the given signed integer. + /// The new `BV` will have the width `width`, which must not be 0. + pub fn from_i64(btor: R, i: i64, width: u32) -> Self { + let low_bits = (i & 0xFFFF_FFFF) as i32; + let high_bits = (i >> 32) as i32; + if width <= 32 { + Self::from_i32(btor, low_bits, width) + } else { + let bv64 = Self::from_i32(btor.clone(), high_bits, 32) + .concat(&Self::from_i32(btor, low_bits, 32)); + if width < 64 { + bv64.slice(width - 1, 0) + } else if width == 64 { + bv64 + } else { + bv64.sext(width - 64) + } + } + } + + /// Create a new constant `BV` representing the given unsigned integer. + /// The new `BV` will have the width `width`, which must not be 0. + pub fn from_u64(btor: R, u: u64, width: u32) -> Self { + let low_bits = (u & 0xFFFF_FFFF) as u32; + let high_bits = (u >> 32) as u32; + if width <= 32 { + Self::from_u32(btor, low_bits, width) + } else { + let bv64 = Self::from_u32(btor.clone(), high_bits, 32) + .concat(&Self::from_u32(btor, low_bits, 32)); + if width < 64 { + bv64.slice(width - 1, 0) + } else if width == 64 { + bv64 + } else { + bv64.sext(width - 64) + } + } + } + + /// Create the constant `0` of the given width. + /// This is equivalent to `from_i32(btor, 0, width)`, but may be more efficient. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// let zero = BV::zero(btor.clone(), 8); + /// assert_eq!(zero.as_u64().unwrap(), 0); + /// ``` + pub fn zero(btor: R, width: u32) -> Self { + let sort = Sort::bitvector(btor.clone(), width); + Self { + node: unsafe { boolector_zero(btor.borrow().as_raw(), sort.as_raw()) }, + btor, // out of order so it can be used above but moved in here + } + } + + /// Create the constant `1` of the given width. + /// This is equivalent to `from_i32(btor, 1, width)`, but may be more efficient. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// let one = BV::one(btor.clone(), 8); + /// assert_eq!(one.as_u64().unwrap(), 1); + /// ``` + pub fn one(btor: R, width: u32) -> Self { + let sort = Sort::bitvector(btor.clone(), width); + Self { + node: unsafe { boolector_one(btor.borrow().as_raw(), sort.as_raw()) }, + btor, // out of order so it can be used above but moved in here + } + } + + /// Create a bitvector constant of the given width, where all bits are set to one. + /// This is equivalent to `from_i32(btor, -1, width)`, but may be more efficient. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// let ones = BV::ones(btor.clone(), 8); + /// assert_eq!(ones.as_binary_str().unwrap(), "11111111"); + /// ``` + pub fn ones(btor: R, width: u32) -> Self { + let sort = Sort::bitvector(btor.clone(), width); + Self { + node: unsafe { boolector_ones(btor.borrow().as_raw(), sort.as_raw()) }, + btor, // out of order so it can be used above but moved in here + } + } + + /// Create a new constant `BV` from the given string `bits` representing a + /// binary number. + /// + /// `bits` must be non-empty and consist only of '0' and/or '1' characters. + /// + /// The resulting `BV` will have bitwidth equal to the length of `bits`. + pub fn from_binary_str(btor: R, bits: &str) -> Self { + let cstring = CString::new(bits).unwrap(); + Self { + node: unsafe { + boolector_const(btor.borrow().as_raw(), cstring.as_ptr() as *const c_char) + }, + btor, // out of order so it can be used above but moved in here + } + } + + /// Create a new constant `BV` from the given string `num` representing a + /// (signed) decimal number. The new `BV` will have the width `width`, which + /// must not be 0. + pub fn from_dec_str(btor: R, num: &str, width: u32) -> Self { + let sort = Sort::bitvector(btor.clone(), width); + let cstring = CString::new(num).unwrap(); + Self { + node: unsafe { + boolector_constd( + btor.borrow().as_raw(), + sort.as_raw(), + cstring.as_ptr() as *const c_char, + ) + }, + btor, // out of order so it can be used above but moved in here + } + } + + /// Create a new constant `BV` from the given string `num` representing a + /// hexadecimal number. The new `BV` will have the width `width`, which must + /// not be 0. + pub fn from_hex_str(btor: R, num: &str, width: u32) -> Self { + let sort = Sort::bitvector(btor.clone(), width); + let cstring = CString::new(num).unwrap(); + Self { + node: unsafe { + boolector_consth( + btor.borrow().as_raw(), + sort.as_raw(), + cstring.as_ptr() as *const c_char, + ) + }, + btor, // out of order so it can be used above but moved in here + } + } + + /// Get the value of the `BV` as a string of '0's and '1's. This method is + /// only effective for `BV`s which are constant, as indicated by + /// [`BV::is_const()`](struct.BV.html#method.is_const). + /// + /// This method does not require the current state to be satisfiable. To get + /// the value of nonconstant `BV` objects given the current constraints, see + /// [`get_a_solution()`](struct.BV.html#method.get_a_solution), which does + /// require that the current state be satisfiable. + /// + /// Returns `None` if the `BV` is not constant. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// + /// // This `BV` is constant, so we get a `Some` + /// let five = BV::from_u32(btor.clone(), 5, 8); + /// assert_eq!(five.as_binary_str(), Some("00000101".to_owned())); + /// + /// // This `BV` is not constant, so we get `None` + /// let unconstrained = BV::new(btor.clone(), 8, Some("foo")); + /// assert_eq!(unconstrained.as_binary_str(), None); + /// ``` + pub fn as_binary_str(&self) -> Option { + if self.is_const() { + let raw = unsafe { boolector_get_bits(self.btor.borrow().as_raw(), self.node) }; + let cstr = unsafe { CStr::from_ptr(raw) }; + let string = cstr.to_str().unwrap().to_owned(); + unsafe { boolector_free_bits(self.btor.borrow().as_raw(), raw) }; + Some(string) + } else { + None + } + } + + /// Get the value of the `BV` as a `u64`. This method is only effective for + /// `BV`s which are constant, as indicated by + /// [`BV::is_const()`](struct.BV.html#method.is_const). + /// + /// This method does not require the current state to be satisfiable. To get + /// the value of nonconstant `BV` objects given the current constraints, see + /// [`get_a_solution()`](struct.BV.html#method.get_a_solution), which does + /// require that the current state be satisfiable. + /// + /// Returns `None` if the `BV` is not constant, or if the value does not fit + /// in 64 bits. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// + /// // This `BV` is constant, so we get a `Some` + /// let five = BV::from_u32(btor.clone(), 5, 8); + /// assert_eq!(five.as_u64(), Some(5)); + /// + /// // This `BV` is not constant, so we get `None` + /// let unconstrained = BV::new(btor.clone(), 8, Some("foo")); + /// assert_eq!(unconstrained.as_u64(), None); + /// ``` + pub fn as_u64(&self) -> Option { + if self.is_const() { + let binary_string = self.as_binary_str()?; + Some(u64::from_str_radix(&binary_string, 2).unwrap()) + } else { + None + } + } + + /// Get the value of the `BV` as a `bool`. This method is only effective for + /// `BV`s which are constant, as indicated by + /// [`BV::is_const()`](struct.BV.html#method.is_const). + /// + /// Returns `true` if the `BV` has a constant nonzero value, or `false` if + /// the `BV` has a constant zero value. + /// Returns `None` if the `BV` is not constant. + pub fn as_bool(&self) -> Option { + if self.is_const() { + let binary_string = self.as_binary_str()?; + for c in binary_string.chars() { + if c != '0' { + return Some(true); + } + } + Some(false) + } else { + None + } + } + + /// Get a solution for the `BV` according to the current model. + /// + /// This requires that model generation is enabled (see + /// [`Btor::set_opt`](struct.Btor.html#method.set_opt)), and that the most + /// recent call to [`Btor::sat()`](struct.Btor.html#method.sat) returned + /// `SolverResult::Sat`. + /// + /// Calling this multiple times on the same `BV` or different arbitrary `BV`s + /// (for the same `Btor` instance) will produce a consistent set of solutions + /// as long as the `Btor`'s state is not otherwise changed. That is, this + /// queries an underlying model which won't change unless the `Btor` state + /// changes. + /// + /// For a code example, see [`BV::new()`](struct.BV.html#method.new). + pub fn get_a_solution(&self) -> BVSolution { + let btor = self.btor.borrow(); + use crate::option::{BtorOption, NumberFormat}; + // Workaround for https://github.com/Boolector/boolector/issues/79: + // set OUTPUT_NUMBER_FORMAT to binary just for this call, restore old + // value on method exit + let old_output_format = + unsafe { boolector_get_opt(btor.as_raw(), BTOR_OPT_OUTPUT_NUMBER_FORMAT) }; + btor.set_opt(BtorOption::OutputNumberFormat(NumberFormat::Binary)); + + btor.timeout_state.restart_timer(); + + let solution = BVSolution::from_raw(btor, unsafe { + boolector_bv_assignment(self.btor.borrow().as_raw(), self.node) + }); + + // restore the old value of the OUTPUT_NUMBER_FORMAT setting + unsafe { + boolector_set_opt( + btor.as_raw(), + BTOR_OPT_OUTPUT_NUMBER_FORMAT, + old_output_format, + ) + }; + + solution + } + + /// Get the `Btor` which this `BV` belongs to + pub fn get_btor(&self) -> R { + self.btor.clone() + } + + /// Get the id of the `BV` + pub fn get_id(&self) -> i32 { + unsafe { boolector_get_node_id(self.btor.borrow().as_raw(), self.node) } + } + + /// Get the bitwidth of the `BV` + pub fn get_width(&self) -> u32 { + unsafe { boolector_get_width(self.btor.borrow().as_raw(), self.node) } + } + + /// Get the symbol of the `BV`, if one was assigned + pub fn get_symbol(&self) -> Option<&str> { + let raw = unsafe { boolector_get_symbol(self.btor.borrow().as_raw(), self.node) }; + if raw.is_null() { + None + } else { + let cstr = unsafe { CStr::from_ptr(raw) }; + Some(cstr.to_str().unwrap()) + } + } + + /// Set the symbol of the `BV`. See notes on + /// [`BV::new()`](struct.BV.html#method.new). + pub fn set_symbol(&mut self, symbol: Option<&str>) { + match symbol { + None => unsafe { + boolector_set_symbol(self.btor.borrow().as_raw(), self.node, std::ptr::null()) + }, + Some(symbol) => { + let cstring = CString::new(symbol).unwrap(); + let symbol = cstring.as_ptr() as *const c_char; + unsafe { boolector_set_symbol(self.btor.borrow().as_raw(), self.node, symbol) } + }, + } + } + + /// Does the `BV` have a constant value? + /// + /// # Examples + /// + /// ``` + /// # use boolector::{Btor, BV}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// + /// // This `BV` is constant + /// let five = BV::from_u32(btor.clone(), 5, 8); + /// assert!(five.is_const()); + /// + /// // This `BV` is not constant + /// let unconstrained = BV::new(btor.clone(), 8, Some("foo")); + /// assert!(!unconstrained.is_const()); + /// + /// // 5 + [unconstrained] is also not constant + /// let sum = five.add(&unconstrained); + /// assert!(!sum.is_const()); + /// + /// // But 5 + 5 is constant + /// let sum = five.add(&five); + /// assert!(sum.is_const()); + /// ``` + pub fn is_const(&self) -> bool { + unsafe { boolector_is_const(self.btor.borrow().as_raw(), self.node) } + } + + /// Does `self` have the same width as `other`? + pub fn has_same_width(&self, other: &Self) -> bool { + unsafe { boolector_is_equal_sort(self.btor.borrow().as_raw(), self.node, other.node) } + } + + /// Assert that `self == 1`. + /// + /// `self` must have bitwidth 1. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV, SolverResult}; + /// # use boolector::option::{BtorOption, ModelGen}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// btor.set_opt(BtorOption::Incremental(true)); + /// btor.set_opt(BtorOption::ModelGen(ModelGen::All)); + /// + /// // Create an unconstrained `BV` + /// let bv = BV::new(btor.clone(), 8, Some("foo")); + /// + /// // Assert that it must be greater than `3` + /// bv.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert(); + /// + /// // (you may prefer this alternate style for assertions) + /// BV::assert(&bv.ugt(&BV::from_u32(btor.clone(), 3, 8))); + /// + /// // The state is satisfiable, and any solution we get + /// // for `bv` must be greater than `3` + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// let solution = bv.get_a_solution().as_u64().unwrap(); + /// assert!(solution > 3); + /// + /// // Now we assert that `bv` must be less than `2` + /// bv.ult(&BV::from_u32(btor.clone(), 2, 8)).assert(); + /// + /// // The state is now unsatisfiable + /// assert_eq!(btor.sat(), SolverResult::Unsat); + /// ``` + pub fn assert(&self) { + unsafe { boolector_assert(self.btor.borrow().as_raw(), self.node) } + } + + /// Assume that the given node == 1. + /// Assumptions are identical to assertions except that they are discarded + /// after each call to `Btor::sat()`. + /// + /// Requires incremental usage to be enabled via + /// [`Btor::set_opt()`](struct.Btor.html#method.set_opt). + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV, SolverResult}; + /// # use boolector::option::{BtorOption, ModelGen}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// btor.set_opt(BtorOption::Incremental(true)); + /// + /// // Create an unconstrained `BV` + /// let bv = BV::new(btor.clone(), 8, Some("foo")); + /// + /// // Assert that it must be greater than `3` + /// bv.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert(); + /// + /// // The state is satisfiable + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// + /// // Temporarily assume that the `BV` is less than `2` + /// bv.ult(&BV::from_u32(btor.clone(), 2, 8)).assume(); + /// + /// // The state is now unsatisfiable + /// assert_eq!(btor.sat(), SolverResult::Unsat); + /// + /// // The assumption only lasts until the next `sat()` + /// // call, so it has been discarded now + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// ``` + pub fn assume(&self) { + unsafe { boolector_assume(self.btor.borrow().as_raw(), self.node) } + } + + /// Returns true if this node is an assumption that forced the input formula + /// to become unsatisfiable. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV, SolverResult}; + /// # use boolector::option::{BtorOption, ModelGen}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// btor.set_opt(BtorOption::Incremental(true)); + /// + /// // Create an unconstrained `BV` and assert that it is greater + /// // than `3`; the state is satisfiable + /// let bv = BV::new(btor.clone(), 8, Some("foo")); + /// bv.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert(); + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// + /// // Temporarily assume that the `BV` is less than `2` + /// let assumption = bv.ult(&BV::from_u32(btor.clone(), 2, 8)); + /// assumption.assume(); + /// + /// // The state is now unsatisfiable, and `assumption` is a + /// // failed assumption + /// assert_eq!(btor.sat(), SolverResult::Unsat); + /// assert!(assumption.is_failed_assumption()); + /// ``` + pub fn is_failed_assumption(&self) -> bool { + unsafe { boolector_failed(self.btor.borrow().as_raw(), self.node) } + } + + binop!( + /// Bitvector equality. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have bitwidth 1. + => _eq, boolector_eq + ); + binop!( + /// Bitvector inequality. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have bitwidth 1. + => _ne, boolector_ne + ); + + binop!( + /// Bitvector addition. `self` and `other` must have the same bitwidth. + => add, boolector_add + ); + binop!( + /// Bitvector subtraction. `self` and `other` must have the same bitwidth. + => sub, boolector_sub + ); + binop!( + /// Bitvector multiplication. `self` and `other` must have the same bitwidth. + => mul, boolector_mul + ); + binop!( + /// Unsigned division. `self` and `other` must have the same bitwidth. + /// Division by `0` produces `-1`. + => udiv, boolector_udiv + ); + binop!( + /// Signed division. `self` and `other` must have the same bitwidth. + => sdiv, boolector_sdiv + ); + binop!( + /// Unsigned remainder. `self` and `other` must have the same bitwidth. + /// If `other` is `0`, the result will be `self`. + => urem, boolector_urem + ); + binop!( + /// Signed remainder. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have positive sign. + => srem, boolector_srem + ); + binop!( + /// Signed remainder. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have sign matching the divisor. + => smod, boolector_smod + ); + unop!( + /// Increment operation + => inc, boolector_inc + ); + unop!( + /// Decrement operation + => dec, boolector_dec + ); + unop!( + /// Two's complement negation + => neg, boolector_neg + ); + + binop!( + /// Unsigned addition overflow detection. Resulting `BV` will have bitwidth + /// one, and be `true` if adding `self` and `other` would overflow when + /// interpreting both `self` and `other` as unsigned. + => uaddo, boolector_uaddo + ); + binop!( + /// Signed addition overflow detection. Resulting `BV` will have bitwidth + /// one, and be `true` if adding `self` and `other` would overflow when + /// interpreting both `self` and `other` as signed. + => saddo, boolector_saddo + ); + binop!( + /// Unsigned subtraction overflow detection. Resulting `BV` will have bitwidth + /// one, and be `true` if subtracting `self` and `other` would overflow when + /// interpreting both `self` and `other` as unsigned. + => usubo, boolector_usubo + ); + binop!( + /// Signed subtraction overflow detection. Resulting `BV` will have bitwidth + /// one, and be `true` if subtracting `self` and `other` would overflow when + /// interpreting both `self` and `other` as signed. + => ssubo, boolector_ssubo + ); + binop!( + /// Unsigned multiplication overflow detection. Resulting `BV` will have + /// bitwidth 1, and be `true` if multiplying `self` and `other` would + /// overflow when interpreting both `self` and `other` as unsigned. + => umulo, boolector_umulo + ); + binop!( + /// Signed multiplication overflow detection. Resulting `BV` will have + /// bitwidth 1, and be `true` if multiplying `self` and `other` would + /// overflow when interpreting both `self` and `other` as signed. + => smulo, boolector_smulo + ); + binop!( + /// Signed division overflow detection. Resulting `BV` will have bitwidth + /// one, and be `true` if dividing `self` by `other` would overflow when + /// interpreting both `self` and `other` as signed. + /// + /// Signed division can overflow if `self` is `INT_MIN` and `other` is `-1`. + /// Note that unsigned division cannot overflow. + => sdivo, boolector_sdivo + ); + + unop!( + /// Bitwise `not` operation (one's complement) + => not, boolector_not + ); + binop!( + /// Bitwise `and` operation. `self` and `other` must have the same bitwidth. + => and, boolector_and + ); + binop!( + /// Bitwise `or` operation. `self` and `other` must have the same bitwidth. + => or, boolector_or + ); + binop!( + /// Bitwise `xor` operation. `self` and `other` must have the same bitwidth. + => xor, boolector_xor + ); + binop!( + /// Bitwise `nand` operation. `self` and `other` must have the same bitwidth. + => nand, boolector_nand + ); + binop!( + /// Bitwise `nor` operation. `self` and `other` must have the same bitwidth. + => nor, boolector_nor + ); + binop!( + /// Bitwise `xnor` operation. `self` and `other` must have the same bitwidth. + => xnor, boolector_xnor + ); + + binop!( + /// Logical shift left: shift `self` left by `other` bits. + /// Either `self` and `other` must have the same bitwidth, or `self` must + /// have a bitwidth which is a power of two and the bitwidth of `other` must + /// be log2 of the bitwidth of `self`. + /// + /// Resulting `BV` will have the same bitwidth as `self`. + => sll, boolector_sll + ); + binop!( + /// Logical shift right: shift `self` right by `other` bits. + /// Either `self` and `other` must have the same bitwidth, or `self` must + /// have a bitwidth which is a power of two and the bitwidth of `other` must + /// be log2 of the bitwidth of `self`. + /// + /// Resulting `BV` will have the same bitwidth as `self`. + => srl, boolector_srl + ); + binop!( + /// Arithmetic shift right: shift `self` right by `other` bits. + /// Either `self` and `other` must have the same bitwidth, or `self` must + /// have a bitwidth which is a power of two and the bitwidth of `other` must + /// be log2 of the bitwidth of `self`. + /// + /// Resulting `BV` will have the same bitwidth as `self`. + => sra, boolector_sra + ); + binop!( + /// Rotate `self` left by `other` bits. + /// `self` must have a bitwidth which is a power of two, and the bitwidth of + /// `other` must be log2 of the bitwidth of `self`. + /// + /// Resulting `BV` will have the same bitwidth as `self`. + => rol, boolector_rol + ); + binop!( + /// Rotate `self` right by `other` bits. + /// `self` must have a bitwidth which is a power of two, and the bitwidth of + /// `other` must be log2 of the bitwidth of `self`. + /// + /// Resulting `BV` will have the same bitwidth as `self`. + => ror, boolector_ror + ); + + unop!( + /// `and` reduction operation: take the Boolean `and` of all bits in the `BV`. + /// Resulting `BV` will have bitwidth 1. + => redand, boolector_redand + ); + unop!( + /// `or` reduction operation: take the Boolean `or` of all bits in the `BV`. + /// Resulting `BV` will have bitwidth 1. + => redor, boolector_redor + ); + unop!( + /// `xor` reduction operation: take the Boolean `xor` of all bits in the `BV`. + /// Resulting `BV` will have bitwidth 1. + => redxor, boolector_redxor + ); + + binop!( + /// Unsigned greater than. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have bitwidth 1. + => ugt, boolector_ugt + ); + binop!( + /// Unsigned greater than or equal. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have bitwidth 1. + => ugte, boolector_ugte + ); + binop!( + /// Signed greater than. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have bitwidth 1. + => sgt, boolector_sgt + ); + binop!( + /// Signed greater than or equal. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have bitwidth 1. + => sgte, boolector_sgte + ); + binop!( + /// Unsigned less than. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have bitwidth 1. + => ult, boolector_ult + ); + binop!( + /// Unsigned less than or equal. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have bitwidth 1. + => ulte, boolector_ulte + ); + binop!( + /// Signed less than. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have bitwidth 1. + => slt, boolector_slt + ); + binop!( + /// Signed less than or equal. `self` and `other` must have the same bitwidth. + /// Resulting `BV` will have bitwidth 1. + => slte, boolector_slte + ); + + /// Unsigned extension (zero-extension), extending by `n` bits. Resulting + /// `BV` will have bitwidth equal to the bitwidth of `self` plus `n`. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// + /// // Create an 8-bit `BV` with value `3` + /// let bv = BV::from_u32(btor.clone(), 3, 8); + /// + /// // Zero-extend by 56 bits + /// let extended = bv.uext(56); + /// + /// // Resulting `BV` is 64 bits and has value `3` + /// assert_eq!(extended.get_width(), 64); + /// assert_eq!(extended.as_u64().unwrap(), 3); + /// ``` + pub fn uext(&self, n: u32) -> Self { + Self { + btor: self.btor.clone(), + node: unsafe { boolector_uext(self.btor.borrow().as_raw(), self.node, n) }, + } + } + + /// Sign-extension operation, extending by `n` bits. Resulting `BV` will have + /// bitwidth equal to the bitwidth of `self` plus `n`. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// + /// // Create an 8-bit `BV` with value `-3` + /// let bv = BV::from_i32(btor.clone(), -3, 8); + /// + /// // Sign-extend by 56 bits + /// let extended = bv.sext(56); + /// + /// // Resulting `BV` is 64 bits and has value `-3` + /// assert_eq!(extended.get_width(), 64); + /// assert_eq!(extended.as_u64().unwrap() as i64, -3); + /// ``` + pub fn sext(&self, n: u32) -> Self { + Self { + btor: self.btor.clone(), + node: unsafe { boolector_sext(self.btor.borrow().as_raw(), self.node, n) }, + } + } + + /// Slicing operation: obtain bits `high` through `low` (inclusive) of `self`. + /// Resulting `BV` will have bitwidth `high - low + 1`. + /// + /// Requires that `0 <= low <= high < self.get_width()`. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// + /// // Create an 8-bit `BV` with this constant value + /// let bv = BV::from_binary_str(btor.clone(), "01100101"); + /// + /// // Slice out bits 1 through 4, inclusive + /// let slice = bv.slice(4, 1); + /// + /// // Resulting slice has width `4` and value `"0010"` + /// assert_eq!(slice.get_width(), 4); + /// assert_eq!(slice.as_binary_str().unwrap(), "0010"); + pub fn slice(&self, high: u32, low: u32) -> Self { + assert!(low <= high, "slice: low must be <= high; got low = {}, high = {}", low, high); + assert!(high < self.get_width(), "slice: high must be < width; got high = {}, width = {}", high, self.get_width()); + Self { + btor: self.btor.clone(), + node: unsafe { boolector_slice(self.btor.borrow().as_raw(), self.node, high, low) }, + } + } + + binop!( + /// Concatenate two bitvectors. Resulting `BV` will have bitwidth equal to + /// the sum of `self` and `other`'s bitwidths. + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// + /// // Create an 8-bit `BV` with value `1` + /// let one = BV::one(btor.clone(), 8); + /// + /// // Create an 8-bit `BV` consisting of all ones + /// let ones = BV::ones(btor.clone(), 8); + /// + /// // The concatenation has length 16 and this value + /// let result = ones.concat(&one); + /// assert_eq!(result.get_width(), 16); + /// assert_eq!(result.as_binary_str().unwrap(), "1111111100000001"); + /// + /// // Concatenate in the other order + /// let result = one.concat(&ones); + /// assert_eq!(result.get_width(), 16); + /// assert_eq!(result.as_binary_str().unwrap(), "0000000111111111"); + /// ``` + => concat, boolector_concat + ); + + /// Concatenate the `BV` with itself `n` times + pub fn repeat(&self, n: u32) -> Self { + Self { + btor: self.btor.clone(), + node: unsafe { boolector_repeat(self.btor.borrow().as_raw(), self.node, n) }, + } + } + + binop!( + /// Returns the `BV` which is true if `self <=> other`, else false. + /// `self` and `other` must have bitwidth 1. + => iff, boolector_iff + ); + binop!( + /// Returns the `BV` which is true if `self` implies `other`, else false. + /// `self` and `other` must have bitwidth 1. + => implies, boolector_implies + ); + + /// Create an if-then-else `BV` node. + /// If `self` is true, then `truebv` is returned, else `falsebv` is returned. + /// + /// `self` must have bitwidth 1. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV, SolverResult}; + /// # use boolector::option::{BtorOption, ModelGen}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// btor.set_opt(BtorOption::ModelGen(ModelGen::All)); + /// + /// // Create an unconstrained `BV` `x` + /// let x = BV::new(btor.clone(), 8, Some("x")); + /// + /// // `y` will be `5` if `x > 10`, else it will be `1` + /// let five = BV::from_u32(btor.clone(), 5, 8); + /// let one = BV::one(btor.clone(), 8); + /// let cond = x.ugt(&BV::from_u32(btor.clone(), 10, 8)); + /// let y = cond.cond_bv(&five, &one); + /// // (you may prefer this alternate style) + /// let _y = BV::cond_bv(&cond, &five, &one); + /// + /// // Now assert that `x < 7` + /// x.ult(&BV::from_u32(btor.clone(), 7, 8)).assert(); + /// + /// // As a result, `y` must be `1` + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// assert_eq!(y.get_a_solution().as_u64().unwrap(), 1); + /// ``` + pub fn cond_bv(&self, truebv: &Self, falsebv: &Self) -> Self { + assert_eq!(self.get_width(), 1, "cond_bv: self must have bitwidth 1; got {}", self.get_width()); + Self { + btor: self.btor.clone(), + node: unsafe { + boolector_cond( + self.btor.borrow().as_raw(), + self.node, + truebv.node, + falsebv.node, + ) + }, + } + } + + /// Create an if-then-else `Array` node. + /// If `self` is true, then `true_array` is returned, else `false_array` is returned. + /// + /// `self` must have bitwidth 1. + pub fn cond_array(&self, true_array: &Array, false_array: &Array) -> Array { + assert_eq!(self.get_width(), 1, "cond_array: self must have bitwidth 1; got {}", self.get_width()); + Array { + btor: self.btor.clone(), + node: unsafe { + boolector_cond( + self.btor.borrow().as_raw(), + self.node, + true_array.node, + false_array.node, + ) + }, + } + } +} + +impl + Clone> Clone for BV { + fn clone(&self) -> Self { + Self { + btor: self.btor.clone(), + node: unsafe { + boolector_copy(self.btor.borrow().as_raw(), self.node) // not an actual copy, just incrementing the refcount properly + }, + } + } +} + +impl + Clone> Drop for BV { + fn drop(&mut self) { + // Actually releasing here seems to expose some UAF bugs in Boolector + // Instead, we just rely on release_all when dropping the Btor + // unsafe { boolector_release(self.btor.borrow().as_raw(), self.node) } + } +} + +impl + Clone> fmt::Debug for BV { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + const MAX_LENGTH: libc::c_long = 2000; // Match ftell()'s return type across platforms + unsafe { + let tmpfile: *mut libc::FILE = libc::tmpfile(); + if tmpfile.is_null() { + panic!("Failed to create a temp file"); + } + // Write the data to `tmpfile` + boolector_dump_smt2_node(self.btor.borrow().as_raw(), tmpfile, self.node); + // Seek to the end of `tmpfile` + assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_END), 0); + // Get the length of `tmpfile` + let length = libc::ftell(tmpfile); + if length < 0 { + panic!("ftell() returned a negative value"); + } + // Seek back to the beginning of `tmpfile` + assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_SET), 0); + let retval = if length > MAX_LENGTH { + write!(f, "") + } else { + let mut buffer = Vec::with_capacity(length as usize); + libc::fread( + buffer.as_mut_ptr() as *mut c_void, + 1, + length as usize, + tmpfile, + ); + buffer.set_len(length as usize); + let string = String::from_utf8_unchecked(buffer); + write!(f, "{}", string) + }; + libc::fclose(tmpfile); + retval + } + } +} + +/// An `Array` in Boolector is really just a map from `BV`s to `BV`s. +/// +/// Like `BV`, `Array` is generic in the `Btor` reference type. +/// For instance, you could use `Array>` for single-threaded applications, +/// or `Array>` for multi-threaded applications. +#[derive(PartialEq, Eq)] +pub struct Array + Clone> { + pub(crate) btor: R, + pub(crate) node: *mut BoolectorNode, +} + +// According to +// https://groups.google.com/forum/#!msg/boolector/itYGgJxU3mY/AC2O0898BAAJ, +// the Boolector library is thread-safe, meaning `*mut BoolectorNode` can be +// both `Send` and `Sync`. +// So as long as `R` is `Send` and/or `Sync`, we can mark `Array` as `Send` +// and/or `Sync` respectively. +unsafe impl + Clone + Send> Send for Array {} +unsafe impl + Clone + Sync> Sync for Array {} + +impl + Clone> Array { + /// Create a new `Array` which maps `BV`s of width `index_width` to `BV`s of + /// width `element_width`. All values in the `Array` will be unconstrained. + /// + /// The `symbol`, if present, will be used to identify the `Array` when printing + /// a model or dumping to file. It must be unique if it is present. + /// + /// Both `index_width` and `element_width` must not be 0. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Array, Btor, BV}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// + /// // `arr` is an `Array` which maps 8-bit values to 8-bit values + /// let arr = Array::new(btor.clone(), 8, 8, Some("arr")); + /// + /// // Write the value `3` to array index `7` + /// let three = BV::from_u32(btor.clone(), 3, 8); + /// let seven = BV::from_u32(btor.clone(), 7, 8); + /// let arr2 = arr.write(&seven, &three); + /// + /// // Read back out the resulting value + /// let read_bv = arr2.read(&seven); + /// + /// // should be the value `3` + /// assert_eq!(read_bv.as_u64().unwrap(), 3); + /// ``` + pub fn new(btor: R, index_width: u32, element_width: u32, symbol: Option<&str>) -> Self { + let index_sort = Sort::bitvector(btor.clone(), index_width); + let element_sort = Sort::bitvector(btor.clone(), element_width); + let array_sort = Sort::array(btor.clone(), &index_sort, &element_sort); + let node = match symbol { + None => unsafe { + boolector_array( + btor.borrow().as_raw(), + array_sort.as_raw(), + std::ptr::null(), + ) + }, + Some(symbol) => { + let cstring = CString::new(symbol).unwrap(); + let symbol = cstring.as_ptr() as *const c_char; + unsafe { boolector_array(btor.borrow().as_raw(), array_sort.as_raw(), symbol) } + }, + }; + Self { btor, node } + } + + /// Create a new `Array` which maps `BV`s of width `index_width` to `BV`s of + /// width `element_width`. The `Array` will be initialized so that all + /// indices map to the same constant value `val`. + /// + /// Both `index_width` and `element_width` must not be 0. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Array, Btor, BV, SolverResult}; + /// # use boolector::option::{BtorOption, ModelGen}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// btor.set_opt(BtorOption::ModelGen(ModelGen::All)); + /// btor.set_opt(BtorOption::Incremental(true)); + /// + /// // `arr` is an `Array` which maps 8-bit values to 8-bit values. + /// // It is initialized such that all entries are the constant `42`. + /// let fortytwo = BV::from_u32(btor.clone(), 42, 8); + /// let arr = Array::new_initialized(btor.clone(), 8, 8, &fortytwo); + /// + /// // Reading the value at any index should produce `42`. + /// let read_bv = arr.read(&BV::from_u32(btor.clone(), 61, 8)); + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// assert_eq!(read_bv.get_a_solution().as_u64().unwrap(), 42); + /// + /// // Write the value `3` to array index `7` + /// let three = BV::from_u32(btor.clone(), 3, 8); + /// let seven = BV::from_u32(btor.clone(), 7, 8); + /// let arr2 = arr.write(&seven, &three); + /// + /// // Read back out the value at index `7`. It should be `3`. + /// let read_bv = arr2.read(&seven); + /// assert_eq!(read_bv.as_u64().unwrap(), 3); + /// + /// // Reading the value at any other index should still produce `42`. + /// let read_bv = arr2.read(&BV::from_u32(btor.clone(), 99, 8)); + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// //assert_eq!(read_bv.get_a_solution().as_u64().unwrap(), 42); + /// ``` + pub fn new_initialized(btor: R, index_width: u32, element_width: u32, val: &BV) -> Self { + let index_sort = Sort::bitvector(btor.clone(), index_width); + let element_sort = Sort::bitvector(btor.clone(), element_width); + let array_sort = Sort::array(btor.clone(), &index_sort, &element_sort); + let node = + unsafe { boolector_const_array(btor.borrow().as_raw(), array_sort.as_raw(), val.node) }; + Self { btor, node } + } + + /// Get the bitwidth of the index type of the `Array` + pub fn get_index_width(&self) -> u32 { + unsafe { boolector_get_index_width(self.btor.borrow().as_raw(), self.node) } + } + + /// Get the bitwidth of the element type of the `Array` + pub fn get_element_width(&self) -> u32 { + unsafe { boolector_get_width(self.btor.borrow().as_raw(), self.node) } + } + + /// Get the symbol of the `Array`, if one was assigned + pub fn get_symbol(&self) -> Option<&str> { + let raw = unsafe { boolector_get_symbol(self.btor.borrow().as_raw(), self.node) }; + if raw.is_null() { + None + } else { + let cstr = unsafe { CStr::from_ptr(raw) }; + Some(cstr.to_str().unwrap()) + } + } + + /// Does the `Array` have a constant value? + pub fn is_const(&self) -> bool { + unsafe { boolector_is_const(self.btor.borrow().as_raw(), self.node) } + } + + /// Does `self` have the same index and element widths as `other`? + pub fn has_same_widths(&self, other: &Self) -> bool { + unsafe { boolector_is_equal_sort(self.btor.borrow().as_raw(), self.node, other.node) } + } + + binop!( + /// Array equality. `self` and `other` must have the same index and element widths. + => _eq, boolector_eq + ); + binop!( + /// Array inequality. `self` and `other` must have the same index and element widths. + => _ne, boolector_ne + ); + + /// Array read: get the value in the `Array` at the given `index` + pub fn read(&self, index: &BV) -> BV { + BV { + btor: self.btor.clone(), + node: unsafe { boolector_read(self.btor.borrow().as_raw(), self.node, index.node) }, + } + } + + /// Array write: return a new `Array` which has `value` at position `index`, + /// and all other elements unchanged. + pub fn write(&self, index: &BV, value: &BV) -> Self { + Self { + btor: self.btor.clone(), + node: unsafe { + boolector_write( + self.btor.borrow().as_raw(), + self.node, + index.node, + value.node, + ) + }, + } + } +} + +impl + Clone> Clone for Array { + fn clone(&self) -> Self { + Self { + btor: self.btor.clone(), + node: unsafe { + boolector_copy(self.btor.borrow().as_raw(), self.node) // not an actual copy, just incrementing the refcount properly + }, + } + } +} + +impl + Clone> Drop for Array { + fn drop(&mut self) { + // Actually releasing here seems to expose some UAF bugs in Boolector + // Instead, we just rely on release_all when dropping the Btor + // unsafe { boolector_release(self.btor.borrow().as_raw(), self.node) } + } +} + +impl + Clone> fmt::Debug for Array { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + const MAX_LENGTH: libc::c_long = 2000; // Match ftell()'s return type across platforms + unsafe { + let tmpfile: *mut libc::FILE = libc::tmpfile(); + if tmpfile.is_null() { + panic!("Failed to create a temp file"); + } + // Write the data to `tmpfile` + boolector_dump_smt2_node(self.btor.borrow().as_raw(), tmpfile, self.node); + // Seek to the end of `tmpfile` + assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_END), 0); + // Get the length of `tmpfile` + let length = libc::ftell(tmpfile); + if length < 0 { + panic!("ftell() returned a negative value"); + } + // Seek back to the beginning of `tmpfile` + assert_eq!(libc::fseek(tmpfile, 0, libc::SEEK_SET), 0); + let retval = if length > MAX_LENGTH { + write!(f, "") + } else { + let mut buffer = Vec::with_capacity(length as usize); + libc::fread( + buffer.as_mut_ptr() as *mut c_void, + 1, + length as usize, + tmpfile, + ); + buffer.set_len(length as usize); + let string = String::from_utf8_unchecked(buffer); + write!(f, "{}", string) + }; + libc::fclose(tmpfile); + retval + } + } +} + +/// A `BVSolution` represents a possible solution for one `BV` in a given model. +#[derive(PartialEq, Eq, Clone, Debug, Hash)] +pub struct BVSolution { + assignment: String, +} + +impl BVSolution { + /// expects an `assignment` in _binary_ (01x) format + /// + /// relevant: https://github.com/Boolector/boolector/issues/79 + fn from_raw(btor: &Btor, assignment: *const c_char) -> Self { + Self { + assignment: { + let cstr = unsafe { CStr::from_ptr(assignment) }; + let assign = cstr.to_str().unwrap().to_owned(); + unsafe { + boolector_free_bv_assignment(btor.as_raw(), cstr.as_ptr() as *const c_char) + }; + assign + }, + } + } + + /// Get a string of length equal to the bitwidth, where each character in the + /// string is either `0`, `1`, or `x`. An `x` indicates that, in this model, + /// the corresponding bit can be arbitrarily chosen to be `0` or `1` and all + /// constraints would still be satisfied. + /// + /// # Example + /// + /// ``` + /// # use boolector::{Btor, BV, SolverResult}; + /// # use boolector::option::{BtorOption, ModelGen}; + /// # use std::rc::Rc; + /// let btor = Rc::new(Btor::new()); + /// btor.set_opt(BtorOption::ModelGen(ModelGen::All)); + /// + /// // `bv` starts as an unconstrained 8-bit value + /// let bv = BV::new(btor.clone(), 8, Some("foo")); + /// + /// // assert that the first two digits of `bv` are 0 + /// let mask = BV::from_u32(btor.clone(), 0b11000000, 8); + /// let zero = BV::zero(btor.clone(), 8); + /// bv.and(&mask)._eq(&zero).assert(); + /// + /// // `as_01x_str()` gives an 8-character string whose first + /// // two digits are '0' + /// assert_eq!(btor.sat(), SolverResult::Sat); + /// let solution = bv.get_a_solution(); + /// assert_eq!(&solution.as_01x_str()[..2], "00"); + /// ``` + pub fn as_01x_str(&self) -> &str { + &self.assignment + } + + /// Turn a string of `0`, `1`, and/or `x` characters into a `BVSolution`. + /// See [`as_01x_str()`](struct.BVSolution.html#method.as_01x_str). + pub fn from_01x_str(s: impl Into) -> Self { + Self { + assignment: s.into(), + } + } + + /// Get a version of this `BVSolution` that is guaranteed to correspond to + /// exactly one possible value. For instance, + /// [`as_01x_str()`](struct.BVSolution.html#method.as_01x_str) on the + /// resulting `BVSolution` will contain no `x`s. + /// + /// In the event that the input `BVSolution` did represent multiple possible + /// values (see [`as_01x_str()`](struct.BVSolution.html#method.as_01x_str)), + /// this will simply choose one possible value arbitrarily. + pub fn disambiguate(&self) -> Self { + Self { + assignment: self + .as_01x_str() + .chars() + .map(|c| match c { + 'x' => '0', + c => c, + }) + .collect(), + } + } + + /// Get a `u64` value for the `BVSolution`. In the event that this + /// `BVSolution` represents multiple possible values (see + /// [`as_01x_str()`](struct.BVSolution.html#method.as_01x_str)), this will + /// simply choose one possible value arbitrarily. + /// + /// Returns `None` if the value does not fit in 64 bits. + /// + /// For a code example, see [`BV::new()`](struct.BV.html#method.new). + pub fn as_u64(&self) -> Option { + let disambiguated = self.disambiguate(); + let binary_string = disambiguated.as_01x_str(); + if binary_string.len() > 64 { + None + } else { + Some(u64::from_str_radix(&binary_string, 2).unwrap_or_else(|e| { + panic!( + "Got the following error while trying to parse {:?} as a binary string: {}", + binary_string, e + ) + })) + } + } + + /// Get a `bool` value for the `BVSolution`. In the event that this + /// `BVSolution` represents both `true` and `false` (see + /// [`as_01x_str()`](struct.BVSolution.html#method.as_01x_str)), this will + /// return `false`. + /// + /// Returns `None` if the `BVSolution` is not a 1-bit value. + pub fn as_bool(&self) -> Option { + let binary_string = self.as_01x_str(); + if binary_string.len() == 1 { + match binary_string.chars().nth(0).unwrap() { + '0' => Some(false), + '1' => Some(true), + 'x' => Some(false), + c => panic!("Unexpected solution character: {}", c), + } + } else { + None + } + } +} diff --git a/vendor/boolector/src/option.rs b/vendor/boolector/src/option.rs new file mode 100644 index 0000000..7c26426 --- /dev/null +++ b/vendor/boolector/src/option.rs @@ -0,0 +1,364 @@ +//! This module exposes options which can be set on a `Btor` instance. + +/// Documentation for individual options and their possible values are +/// more-or-less taken verbatim from the Boolector 3.0.0 docs. +pub enum BtorOption { + /// Whether to generate a model (set of concrete solution values) for + /// satisfiable instances + ModelGen(ModelGen), + /// Enable/disable incremental mode. Note that the Boolector 3.0.0 docs say + /// that "disabling incremental usage is currently not supported". + Incremental(bool), + /// Set incremental mode for SMT-LIB v1 input. The default is + /// `IncrementalSMT1::Basic`. + IncrementalSMT1(IncrementalSMT1), + /// Input file format. The default is `InputFileFormat::Autodetect`. + InputFileFormat(InputFileFormat), + /// Format to output numbers in. The default is `NumberFormat::Binary`. + OutputNumberFormat(NumberFormat), + /// Output file format. The default is `FileFormat::BTOR`. + OutputFileFormat(OutputFileFormat), + /// Solver timeout. If `Some`, then operations lasting longer than the given + /// `Duration` will be aborted and return `SolverResult::Unknown`. + /// + /// If `None`, then any previously set solver timeout will be removed, and + /// there will be no time limit to solver operations. + SolverTimeout(Option), + /// Solver engine. The default is `SolverEngine::Fun`. + SolverEngine(SolverEngine), + /// SAT solver. Each option requires that Boolector was compiled with support + /// for the corresponding solver. + SatEngine(SatEngine), + /// Enable/disable auto cleanup of all references held on exit. + AutoCleanup(bool), + /// Enable/disable pretty printing when dumping. + PrettyPrint(bool), + /// Seed for Boolector's internal random number generator. The default is 0. + Seed(u32), + /// Rewrite level. The default is `RewriteLevel::Full`. + /// + /// Boolector's docs say to not change this setting after creating expressions. + RewriteLevel(RewriteLevel), + /// Enable/disable skeleton preprocessing during simplification. + SkeletonPreproc(bool), + /// Enable/disable the eager addition of Ackermann constraints for function + /// applications. + Ackermann(bool), + /// Enable/disable the eager elimination of lambda expressions via beta + /// reduction. + BetaReduce(bool), + /// Enable/disable slice elimination on bit vector variables. + EliminateSlices(bool), + /// Enable/disable variable substitution during simplification. + VariableSubst(bool), + /// Enable/disable unconstrained optimization. + UnconstrainedOpt(bool), + /// Enable/disable merging of lambda expressions. + MergeLambdas(bool), + /// Enable/disable extraction of common array patterns as lambda terms. + ExtractLambdas(bool), + /// Enable/disable normalization of addition, multiplication, and bitwise + /// `and`. + Normalize(bool), + /// Enable/disable normalization of addition. + NormalizeAdd(bool), + /// For `SolverEngine::Fun`, enable/disable Prop engine preprocessing step + /// within sequential portfolio setting. + FunPreProp(bool), + /// For `SolverEngine::Fun`, enable/disable SLS engine preprocessing step + /// within sequential portfolio setting. + FunPreSLS(bool), + /// For `SolverEngine::Fun`, enable/disable dual propagation optimization. + FunDualProp(bool), + /// For `SolverEngine::Fun`, set the order in which inputs are assumed in + /// dual propagation clone. The default is `DualPropQsortOrder::Just`. + FunDualPropQsortOrder(DualPropQsortOrder), + /// For `SolverEngine::Fun`, enable/disable justification optimization. + FunJustification(bool), + /// For `SolverEngine::Fun`, set the path selection heuristic for + /// justification optimization. The default is + /// `JustificationHeuristic::MinApp`. + FunJustificationHeuristic(JustificationHeuristic), + /// For `SolverEngine::Fun`, enable/disable lazy synthesis of bitvector + /// expressions. + FunLazySynthesize(bool), + /// For `SolverEngine::Fun`, enable/disable eager generation of lemmas. + FunEagerLemmas(EagerLemmas), + /// For `SolverEngine::SLS`, set the number of bit flips used as a limit. + /// `0` indicates no limit. + SLSNumFlips(u32), + /// For `SolverEngine::SLS`, set the move strategy. The default is + /// `SLSMoveStrategy::BestMove`. + SLSMoveStrategy(SLSMoveStrategy), + /// For `SolverEngine::SLS`, enable/disable justification-based path + /// selection during candidate selection. + SLSJustification(bool), + /// For `SolverEngine::SLS`, enable/disable group-wise moves, where rather + /// than changing the assignment of one single candidate variable, all + /// candidate variables are set at the same time (using the same strategy). + SLSGroupWiseMoves(bool), + /// For `SolverEngine::SLS`, enable/disable range-wise bitflip moves, where + /// the bits within all ranges from 2 to the bitwidth (starting from the LSB) + /// are flipped at once. + SLSRangeWiseMoves(bool), + /// For `SolverEngine::SLS`, enable/disable segment-wise bitflip moves, where + /// the bits within segments of multiples of 2 are flipped at once. + SLSSegmentWiseMoves(bool), + /// For `SolverEngine::SLS`, enable/disable random walk moves, where one out + /// of all possible neighbors is randomly selected for a randomly selected + /// candidate variable. + SLSRandomWalkMoves(bool), + /// For `SolverEngine::SLS`, set the probability with which a random walk is + /// chosen if `SLSRandomWalkMoves` is enabled. + SLSRandomWalkProbability(u32), + /// For `SolverEngine::SLS`, enable/disable the randomization of all + /// candidate variables (rather than a single randomly selected candidate + /// variable) in case no best move has been found. + SLSRandomizeAll(bool), + /// For `SolverEngine::SLS`, enable/disable the randomization of bit ranges + /// (rather than all bits) of candidate variable(s) to be randomized in case + /// no best move has been found. + SLSRandomizeRange(bool), + /// For `SolverEngine::SLS`, enable/disable propagation moves. + SLSPropagationMoves(bool), + /// For `SolverEngine::SLS` when propagation moves are enabled, set the + /// number of propagation moves to be performed (this forms a ratio with + /// `SLSPropagationMovesNumRegular`). + SLSPropagationMovesNumProp(u32), + /// For `SolverEngine::SLS` when propagation moves are enabled, set the + /// number of regular moves to be performed (this forms a ratio with + /// `SLSPropagationMovesNumProp`). + SLSPropagationMovesNumRegular(u32), + /// For `SolverEngine::SLS`, enable/disable forcibly choosing random walks as + /// recovery moves when conflicts occur after a propagation move. + SLSForceRandomWalks(bool), + /// For `SolverEngine::SLS`, enable/disable that during best move selection, + /// if the current candidate variable with a previous neighbor yields the + /// currently best score, this neighbor assignment is used as a base for + /// further neighborhood exploration (rather than its current assignment). + SLSIncMoveTest(bool), + /// For `SolverEngine::SLS`, enable/disable restarts. + SLSRestarts(bool), + /// For `SolverEngine::SLS`, enable/disable the "bandit scheme" for selecting + /// root constraints. If disabled, candidate root constraints are selected + /// randomly. + SLSBanditScheme(bool), + /// For `SolverEngine::Prop`, set the number of propagation steps used as a + /// limit. `0` indicates no limit. + PropNumSteps(u32), + /// For `SolverEngine::Prop`, enable/disable restarts. + PropRestarts(bool), + /// For `SolverEngine::Prop`, enable/disable the "bandit scheme" for + /// selecting root constraints. If disabled, candidate root constraints are + /// selected randomly. + PropBanditScheme(bool), + /// For `SolverEngine::Prop`, choose the mode for path selection. + /// The default is `PropPathSelection::Essential`. + PropPathSelectionMode(PropPathSelection), + /// For `SolverEngine::Prop`, set the probability with which to choose + /// inverse values over consistent values. + PropInvValueProbability(u32), + /// For `SolverEngine::Prop`, set the probability with which to select the + /// path to the condition (in case of an if-then-else operation) rather than + /// the enabled branch during down propagation. + PropFlipConditionProbability(u32), + /// Like `PropFlipConditionProbability`, but for the case that either the + /// 'then' or 'else' branch is constant. + PropFlipConditionProbabilityConstant(u32), + /// For `SolverEngine::Prop`, set the limit for how often the path to the + /// condition may be selected before `PropFlipConditionProbabilityConstant` + /// is decreased or increased by `PropFlipConditionProbabilityConstantDelta`. + PropFlipConditionNumPaths(u32), + /// For `SolverEngine::Prop`, set the delta by which + /// `PropFlipConditionProbabilityConstant` is decreased or increased after + /// `PropFlipConditionNumPaths` is reached. + PropFlipConditionProbabilityConstantDelta(u32), + /// For `SolverEngine::Prop`, set the probability with which to keep the + /// current value of the don't care bits of a slice operation (rather than + /// fully randomizing all of them) when selecting an inverse or consistent + /// value. + PropSliceKeepDCProbability(u32), + /// For `SolverEngine::Prop`, set the probability with which to use the + /// corresponding slice of the current assignment with at most one of its + /// bits flipped as the result of consistent value selection for concats. + PropConcatFlipProbability(u32), + /// For `SolverEngine::Prop`, set the probability with which to use the + /// current assignment of the operand of a slice operation with one of the + /// don't care bits flipped, unless their current assignment is kept by + /// `PropSliceKeepDCProbability`. + PropSliceFlipProbability(u32), + /// For `SolverEngine::Prop`, set the probability with which the current + /// assignment of the selected node with one of its bits flipped (rather than + /// a fully randomized bitvector) is down-propagated in the case of an + /// inequality. + PropEqFlipProbability(u32), + /// For `SolverEngine::Prop`, set the probability with which the current + /// assignment of the don't care bits of the selected node with at most one + /// of its bits flipped in case of an `and` operation. + PropAndFlipProbability(u32), + /// For `SolverEngine::AIGProp`, enable/disable restarts. + AIGPropUseRestarts(bool), + /// For `SolverEngine::AIGProp`, select the synthesis mode for Skolem + /// functions. + AIGPropQuantSynthesis(AIGPropQuantSynthesis), + /// For `SolverEngine::AIGProp`, enable/disable solving the dual (negated) + /// version of the quantified bit-vector formula. + AIGPropQuantDualSolver(bool), + /// For `SolverEngine::AIGProp`, set the limit of enumerated expressions + /// for the enumerative learning synthesis algorithm. + AIGPropQuantSynthLimit(u32), + /// For `SolverEngine::AIGProp`, enable/disable generalization of + /// quantifier instantiations via enumerative learning. + AIGPropSynthQI(bool), + /// For `SolverEngine::AIGProp`, enable/disable destructive equality + /// resolution simplification. + AIGPropQuantDER(bool), + /// For `SolverEngine::AIGProp`, enable/disable constructive equality + /// resolution simplification. + AIGPropQuantCER(bool), + /// For `SolverEngine::AIGProp`, enable/disable miniscoping. + AIGPropQuantMiniscope(bool), +} + +pub enum ModelGen { + /// Do not generate models + Disabled, + /// Generate models for asserted expressions only + Asserted, + /// Generate models for all expressions + All, +} + +pub enum IncrementalSMT1 { + /// Stop after first satisfiable formula + Basic, + /// Solve all formulas + Continue, +} + +pub enum InputFileFormat { + Autodetect, + Btor, + Btor2, + SMTLIBv1, + SMTLIBv2, +} + +pub enum NumberFormat { + Binary, + Decimal, + Hexadecimal, +} + +pub enum OutputFileFormat { + BTOR, + SMTLIBv2, + AigerASCII, + AigerBinary, +} + +pub enum SolverEngine { + /// Default engine for all combinations of QF_AUFBV; uses lemmas on demand + /// for QF_AUFBV and eager bit-blasting for QF_BV + Fun, + /// Score-based local search QF_BV engine + SLS, + /// Propagation-based local search QF_BV engine + Prop, + /// Propagation-based local search QF_BV engine that operates on the bit-blasted formula (the AIG layer) + AIGProp, + /// Quantifier engine (BV only) + Quant, +} + +pub enum SatEngine { + /// CaDiCaL + CaDiCaL, + /// CryptoMiniSat + CMS, + /// Lingeling + Lingeling, + /// MiniSAT + MiniSAT, + /// PicoSAT + PicoSAT, +} + +pub enum RewriteLevel { + /// "no rewriting" + None, + /// "term level rewriting" + TermLevel, + /// "more simplification techniques" + More, + /// "full rewriting/simplification" + Full, +} + +pub enum DualPropQsortOrder { + /// Order by score, highest score first + Just, + /// Order by input id, ascending + Asc, + /// Order by input id, descending + Desc, +} + +pub enum JustificationHeuristic { + /// Always choose the left branch + Left, + /// Choose the branch with the minimum number of applies + MinApp, + /// Choose the branch with the minimum depth + MinDepth, +} + +pub enum EagerLemmas { + /// Do not generate lemmas eagerly (generate one single lemma per refinement + /// iteration) + None, + /// Only generate lemmas eagerly until the first conflict dependent on + /// another conflict is found + Conf, + /// In each refinement iterations, generate lemmas for all conflicts + All, +} + +pub enum SLSMoveStrategy { + /// Always choose the best score improving move + BestMove, + /// Perform a random walk weighted by score + RandomWalk, + /// Always choose the first best move, even if another move may be better + FirstBestMove, + /// Choose a move even if its score is not better but the same as the score + /// of the previous best move + BestSameMove, + /// Always choose propagation move, and recover with SLS move in case of + /// conflict + AlwaysProp, +} + +pub enum PropPathSelection { + /// Select path based on controlling inputs + Controlling, + /// Select path based on essential inputs + Essential, + /// Select path based on random inputs + Random, +} + +pub enum AIGPropQuantSynthesis { + /// Do not synthesize skolem functions (use model values for instantiation) + None, + /// Use enumerative learning to synthesize skolem functions + EL, + /// Use enumerative learning modulo the predicates in the cone of influence + /// of the existential variables to synthesize skolem functions + ELMC, + /// Chain the `EL` and `ELMC` approaches to synthesize skolem functions + ELELMC, + /// Use enumerative learning modulo the given root constraints to synthesize + /// skolem functions + ELMR, +} diff --git a/vendor/boolector/src/sort.rs b/vendor/boolector/src/sort.rs new file mode 100644 index 0000000..0daca67 --- /dev/null +++ b/vendor/boolector/src/sort.rs @@ -0,0 +1,81 @@ +// We have some methods on `Sort` that we don't use, but still make sense to +// have around for the future +#![allow(dead_code)] + +use crate::btor::Btor; +use boolector_sys::*; +use std::borrow::Borrow; + +pub struct Sort + Clone> { + btor: R, + sort: BoolectorSort, +} + +// According to +// https://groups.google.com/forum/#!msg/boolector/itYGgJxU3mY/AC2O0898BAAJ, +// the Boolector library is thread-safe, meaning `BoolectorSort` can be +// both `Send` and `Sync`. +// So as long as `R` is `Send` and/or `Sync`, we can mark `Sort` as `Send` +// and/or `Sync` respectively. +unsafe impl + Clone + Send> Send for Sort {} +unsafe impl + Clone + Sync> Sync for Sort {} + +impl + Clone> Sort { + pub(crate) fn from_raw(btor: R, sort: BoolectorSort) -> Self { + Self { btor, sort } + } + + pub(crate) fn as_raw(&self) -> BoolectorSort { + self.sort + } + + /// Create a bitvector sort for the given bitwidth. + /// `width` must not be `0`. + pub fn bitvector(btor: R, width: u32) -> Self { + assert!(width > 0, "boolector: cannot create 0-width bitvector sort"); + Self::from_raw(btor.clone(), unsafe { + boolector_bitvec_sort(btor.borrow().as_raw(), width) + }) + } + + /// Create the Boolean sort. + /// + /// In Boolector, there is no distinction between Booleans and bitvectors of + /// bitwidth one, so this is equivalent to `Sort::bitvector(btor, 1)`. + pub fn bool(btor: R) -> Self { + Self::from_raw(btor.clone(), unsafe { + boolector_bool_sort(btor.borrow().as_raw()) + }) + } + + /// Create an array sort. An `Array` in Boolector is really just a map + /// which maps items of the `index` sort to the `element` sort. + /// + /// Both the `index` and `element` sorts must be bitvector sorts. + pub fn array(btor: R, index: &Sort, element: &Sort) -> Self { + Self::from_raw(btor.clone(), unsafe { + boolector_array_sort(btor.borrow().as_raw(), index.as_raw(), element.as_raw()) + }) + } + + /// Is `self` an array sort? + pub fn is_array_sort(&self) -> bool { + unsafe { boolector_is_array_sort(self.btor.borrow().as_raw(), self.as_raw()) } + } + + /// Is `self` a bitvector sort? + pub fn is_bv_sort(&self) -> bool { + unsafe { boolector_is_bitvec_sort(self.btor.borrow().as_raw(), self.as_raw()) } + } + + /// Is `self` a function sort? + pub fn is_fun_sort(&self) -> bool { + unsafe { boolector_is_fun_sort(self.btor.borrow().as_raw(), self.as_raw()) } + } +} + +impl + Clone> Drop for Sort { + fn drop(&mut self) { + unsafe { boolector_release_sort(self.btor.borrow().as_raw(), self.as_raw()) } + } +} diff --git a/vendor/boolector/src/timeout.rs b/vendor/boolector/src/timeout.rs new file mode 100644 index 0000000..88bcd9f --- /dev/null +++ b/vendor/boolector/src/timeout.rs @@ -0,0 +1,64 @@ +use std::sync::RwLock; +use std::time::{Duration, Instant}; + +#[derive(Debug)] +pub struct TimeoutState { + timeout_duration: RwLock>, + current_operation_start_time: RwLock, +} + +impl TimeoutState { + pub fn new() -> Self { + Self::with_timeout_duration(None) + } + + pub fn with_timeout_duration(timeout_duration: Option) -> Self { + Self { + timeout_duration: RwLock::new(timeout_duration), + current_operation_start_time: RwLock::new(Instant::now()), + } + } + + pub fn get_timeout_duration(&self) -> Option { + let guard = self.timeout_duration.read().unwrap(); + *guard + } + + pub fn set_timeout_duration(&self, timeout_duration: Option) { + let mut guard = self.timeout_duration.write().unwrap(); + *guard = timeout_duration; + } + + pub fn get_current_operation_start_time(&self) -> Instant { + let guard = self.current_operation_start_time.read().unwrap(); + *guard + } + + pub fn restart_timer(&self) { + let mut guard = self.current_operation_start_time.write().unwrap(); + *guard = Instant::now(); + } +} + +pub extern "C" fn callback(void_ptr_to_ts: *mut std::os::raw::c_void) -> i32 { + let timeout_state = unsafe { &*(void_ptr_to_ts as *const TimeoutState) }; + match timeout_state.get_timeout_duration() { + None => 0, // no timeout set, keep going + Some(timeout_duration) => { + let current_operation_start_time = timeout_state.get_current_operation_start_time(); + match Instant::now().checked_duration_since(current_operation_start_time) { + None => { + // somehow negative time has elapsed since operation started? Keep going + 0 + }, + Some(duration) => { + if duration > timeout_duration { + 1 // terminate + } else { + 0 // keep going + } + }, + } + }, + } +}