mirror of
https://github.com/radareorg/radius2.git
synced 2026-11-07 06:36:03 -10:00
Import and update boolector to fix the Windows build
* Boolector project it's no longer maintained * So we just keep a copy with fixes for Windows
This commit is contained in:
pancake authored and pancake committed
1 parent
b55bce5b8c
commit
9a67eeefae
11 files changed
+3027
-1
No files matched your search
@@ -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" }
|
||||
+7
-1
@@ -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
|
||||
+170
@@ -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"
|
||||
Vendored
+29
@@ -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 <[email protected]>"]
|
||||
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"]
|
||||
Vendored
+21
@@ -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.
|
||||
Vendored
+797
@@ -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<Box<timeout::TimeoutState>>, // 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, "<btor {:?}>", 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<R: Borrow<Btor> + Clone>(btor: R, bv: &BV<R>) -> Option<BV<R>> {
|
||||
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<R: Borrow<Btor> + Clone>(
|
||||
btor: R,
|
||||
array: &Array<R>,
|
||||
) -> Option<Array<R>> {
|
||||
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<R: Borrow<Btor> + Clone>(btor: R, symbol: &str) -> Option<BV<R>> {
|
||||
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<R: Borrow<Btor> + Clone>(btor: R, symbol: &str) -> Option<Array<R>> {
|
||||
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,
|
||||
}
|
||||
Vendored
+13
@@ -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;
|
||||
Vendored
+1476
File diff suppressed because it is too large.
Load diff
Vendored
+364
@@ -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<std::time::Duration>),
|
||||
/// 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,
|
||||
}
|
||||
Vendored
+81
@@ -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<R: Borrow<Btor> + 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<R: Borrow<Btor> + Clone + Send> Send for Sort<R> {}
|
||||
unsafe impl<R: Borrow<Btor> + Clone + Sync> Sync for Sort<R> {}
|
||||
|
||||
impl<R: Borrow<Btor> + Clone> Sort<R> {
|
||||
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<R>, element: &Sort<R>) -> 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<R: Borrow<Btor> + Clone> Drop for Sort<R> {
|
||||
fn drop(&mut self) {
|
||||
unsafe { boolector_release_sort(self.btor.borrow().as_raw(), self.as_raw()) }
|
||||
}
|
||||
}
|
||||
Vendored
+64
@@ -0,0 +1,64 @@
|
||||
use std::sync::RwLock;
|
||||
use std::time::{Duration, Instant};
|
||||
|
||||
#[derive(Debug)]
|
||||
pub struct TimeoutState {
|
||||
timeout_duration: RwLock<Option<Duration>>,
|
||||
current_operation_start_time: RwLock<Instant>,
|
||||
}
|
||||
|
||||
impl TimeoutState {
|
||||
pub fn new() -> Self {
|
||||
Self::with_timeout_duration(None)
|
||||
}
|
||||
|
||||
pub fn with_timeout_duration(timeout_duration: Option<Duration>) -> Self {
|
||||
Self {
|
||||
timeout_duration: RwLock::new(timeout_duration),
|
||||
current_operation_start_time: RwLock::new(Instant::now()),
|
||||
}
|
||||
}
|
||||
|
||||
pub fn get_timeout_duration(&self) -> Option<Duration> {
|
||||
let guard = self.timeout_duration.read().unwrap();
|
||||
*guard
|
||||
}
|
||||
|
||||
pub fn set_timeout_duration(&self, timeout_duration: Option<Duration>) {
|
||||
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
|
||||
}
|
||||
},
|
||||
}
|
||||
},
|
||||
}
|
||||
}
|
||||
Reference in new issue
Block a user