Skip to content

Commit c4c475f

Browse files
pleichfitzgen
pleich
and
fitzgen
authored
Add support for parsing negative solution values (#46)
## Description This PR would add support for solutions that contain negative integers. Currently, the problem with negative solutions is that the SMT solver will return for example `(x (- 2))` a solution to `x < 0` . When calling `get`, this solution will be parsed into an `SExprData::List` . Calling `try_from_int` will then return always return the error `NotAnAtom`. This PR introduces a new variant of `SExprData`, which is a special case of `SExprData::List`, which is returned for lists that contain exactly two atoms , where the first one is either `+` or `-`. Additionally it fixes typos in comments. ## Minimal Test ```rust use easy_smt::{ContextBuilder, Response}; #[test] fn test_negative_integers() { let mut ctx = ContextBuilder::new() .solver("z3") .solver_args(["-smt2", "-in"]) .build() .unwrap(); let x = ctx.declare_const("x", ctx.int_sort()).unwrap(); ctx.assert(ctx.lt(x, ctx.numeral(0))).unwrap(); assert_eq!(ctx.check().unwrap(), Response::Sat); let solution = ctx.get_value(vec![x]).unwrap(); let sol_x = ctx.get(solution[0].1); let sol = i64::try_from(sol_x).expect("Failed to parse"); assert!(sol < 0) } ``` --------- Co-authored-by: Nick Fitzgerald <[email protected]>
1 parent 8533979 commit c4c475f

File tree

2 files changed

+281
-4
lines changed

2 files changed

+281
-4
lines changed

‎src/context.rs‎

Lines changed: 180 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -659,6 +659,186 @@ impl Context {
659659
self.arena.get(expr)
660660
}
661661

662+
/// Get the atom data for the given s-expression.
663+
///
664+
/// This allows you to inspect s-expressions. If the s-expression is not an
665+
/// atom this function returns `None`.
666+
///
667+
/// You may only pass in `SExpr`s that were created by this
668+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
669+
/// invalid data.
670+
pub fn get_atom(&self, expr: SExpr) -> Option<&str> {
671+
self.arena.get_atom(expr)
672+
}
673+
674+
/// Get the string data for the given s-expression.
675+
///
676+
/// This allows you to inspect s-expressions. If the s-expression is not an
677+
/// string this function returns `None`.
678+
///
679+
/// You may only pass in `SExpr`s that were created by this
680+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
681+
/// invalid data.
682+
pub fn get_str(&self, expr: SExpr) -> Option<&str> {
683+
self.arena.get_str(expr)
684+
}
685+
686+
/// Get the list data for the given s-expression.
687+
///
688+
/// This allows you to inspect s-expressions.If the s-expression is not an
689+
/// list this function returns `None`.
690+
///
691+
/// You may only pass in `SExpr`s that were created by this
692+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
693+
/// invalid data.
694+
pub fn get_list(&self, expr: SExpr) -> Option<&[SExpr]> {
695+
self.arena.get_list(expr)
696+
}
697+
698+
/// Get the data for the given s-expression as an `u8`.
699+
///
700+
/// This allows you to inspect s-expressions. If the s-expression is not an
701+
/// cannot be parsed into an `u8` this function returns `None`.
702+
///
703+
/// You may only pass in `SExpr`s that were created by this
704+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
705+
/// invalid data.
706+
pub fn get_u8(&self, expr: SExpr) -> Option<u8> {
707+
self.arena.get_t(expr)
708+
}
709+
710+
/// Get the data for the given s-expression as an `u16`.
711+
///
712+
/// This allows you to inspect s-expressions. If the s-expression is not an
713+
/// cannot be parsed into an `u16` this function returns `None`.
714+
///
715+
/// You may only pass in `SExpr`s that were created by this
716+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
717+
/// invalid data.
718+
pub fn get_u16(&self, expr: SExpr) -> Option<u16> {
719+
self.arena.get_t(expr)
720+
}
721+
722+
/// Get the data for the given s-expression as an `u32`.
723+
///
724+
/// This allows you to inspect s-expressions. If the s-expression is not an
725+
/// cannot be parsed into an `u32` this function returns `None`.
726+
///
727+
/// You may only pass in `SExpr`s that were created by this
728+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
729+
/// invalid data.
730+
pub fn get_u32(&self, expr: SExpr) -> Option<u32> {
731+
self.arena.get_t(expr)
732+
}
733+
734+
/// Get the data for the given s-expression as an `u64`.
735+
///
736+
/// This allows you to inspect s-expressions. If the s-expression is not an
737+
/// cannot be parsed into an `u64` this function returns `None`.
738+
///
739+
/// You may only pass in `SExpr`s that were created by this
740+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
741+
/// invalid data.
742+
pub fn get_u64(&self, expr: SExpr) -> Option<u64> {
743+
self.arena.get_t(expr)
744+
}
745+
746+
/// Get the data for the given s-expression as an `u128`.
747+
///
748+
/// This allows you to inspect s-expressions. If the s-expression is not an
749+
/// cannot be parsed into an `u128` this function returns `None`.
750+
///
751+
/// You may only pass in `SExpr`s that were created by this
752+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
753+
/// invalid data.
754+
pub fn get_u128(&self, expr: SExpr) -> Option<u128> {
755+
self.arena.get_t(expr)
756+
}
757+
758+
/// Get the data for the given s-expression as an `usize`.
759+
///
760+
/// This allows you to inspect s-expressions. If the s-expression is not an
761+
/// cannot be parsed into an `usize` this function returns `None`.
762+
///
763+
/// You may only pass in `SExpr`s that were created by this
764+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
765+
/// invalid data.
766+
pub fn get_usize(&self, expr: SExpr) -> Option<usize> {
767+
self.arena.get_t(expr)
768+
}
769+
770+
/// Get the data for the given s-expression as an `i8`.
771+
///
772+
/// This allows you to inspect s-expressions. If the s-expression is not an
773+
/// cannot be parsed into an `i8` this function returns `None`.
774+
///
775+
/// You may only pass in `SExpr`s that were created by this
776+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
777+
/// invalid data.
778+
pub fn get_i8(&self, expr: SExpr) -> Option<i8> {
779+
self.arena.get_t(expr)
780+
}
781+
782+
/// Get the data for the given s-expression as an `i16`.
783+
///
784+
/// This allows you to inspect s-expressions. If the s-expression is not an
785+
/// cannot be parsed into an `i16` this function returns `None`.
786+
///
787+
/// You may only pass in `SExpr`s that were created by this
788+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
789+
/// invalid data.
790+
pub fn get_i16(&self, expr: SExpr) -> Option<i16> {
791+
self.arena.get_t(expr)
792+
}
793+
794+
/// Get the data for the given s-expression as an `i32`.
795+
///
796+
/// This allows you to inspect s-expressions. If the s-expression is not an
797+
/// cannot be parsed into an `i32` this function returns `None`.
798+
///
799+
/// You may only pass in `SExpr`s that were created by this
800+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
801+
/// invalid data.
802+
pub fn get_i32(&self, expr: SExpr) -> Option<i32> {
803+
self.arena.get_t(expr)
804+
}
805+
806+
/// Get the data for the given s-expression as an `i64`.
807+
///
808+
/// This allows you to inspect s-expressions. If the s-expression is not an
809+
/// cannot be parsed into an `i64` this function returns `None`.
810+
///
811+
/// You may only pass in `SExpr`s that were created by this
812+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
813+
/// invalid data.
814+
pub fn get_i64(&self, expr: SExpr) -> Option<i64> {
815+
self.arena.get_t(expr)
816+
}
817+
818+
/// Get the data for the given s-expression as an `i128`.
819+
///
820+
/// This allows you to inspect s-expressions. If the s-expression is not an
821+
/// cannot be parsed into an `i128` this function returns `None`.
822+
///
823+
/// You may only pass in `SExpr`s that were created by this
824+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
825+
/// invalid data.
826+
pub fn get_i128(&self, expr: SExpr) -> Option<i128> {
827+
self.arena.get_t(expr)
828+
}
829+
830+
/// Get the data for the given s-expression as an `isize`.
831+
///
832+
/// This allows you to inspect s-expressions. If the s-expression is not an
833+
/// cannot be parsed into an `isize` this function returns `None`.
834+
///
835+
/// You may only pass in `SExpr`s that were created by this
836+
/// `Context`. Failure to do so is safe, but may trigger a panic or return
837+
/// invalid data.
838+
pub fn get_isize(&self, expr: SExpr) -> Option<isize> {
839+
self.arena.get_t(expr)
840+
}
841+
662842
/// Access "known" atoms.
663843
///
664844
/// This lets you skip the is-it-already-interned-or-not checks and hash map

‎src/sexpr.rs‎

Lines changed: 101 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -213,22 +213,118 @@ impl Arena {
213213
unreachable!()
214214
}
215215
}
216+
217+
pub fn get_atom(&self, expr: SExpr) -> Option<&str> {
218+
if !expr.is_atom() {
219+
return None;
220+
}
221+
222+
let inner = self.0.borrow();
223+
// Safety argument: the data will live as long as the containing context, and is
224+
// immutable once it's inserted, so using the lifteime of the Arena is acceptable.
225+
let data = unsafe { std::mem::transmute(inner.strings[expr.index()].as_str()) };
226+
Some(data)
227+
}
228+
229+
pub fn get_str(&self, expr: SExpr) -> Option<&str> {
230+
if !expr.is_string() {
231+
return None;
232+
}
233+
234+
let inner = self.0.borrow();
235+
// Safety argument: the data will live as long as the containing context, and is
236+
// immutable once it's inserted, so using the lifteime of the Arena is acceptable.
237+
let data = unsafe { std::mem::transmute(inner.strings[expr.index()].as_str()) };
238+
Some(data)
239+
}
240+
241+
pub fn get_list(&self, expr: SExpr) -> Option<&[SExpr]> {
242+
if !expr.is_list() {
243+
return None;
244+
}
245+
246+
let inner = self.0.borrow();
247+
// Safety argument: the data will live as long as the containing context, and is
248+
// immutable once it's inserted, so using the lifteime of the Arena is acceptable.
249+
let data = unsafe { std::mem::transmute(inner.lists[expr.index()].as_slice()) };
250+
return Some(data);
251+
}
252+
253+
pub(crate) fn get_t<T: TryParseInt>(&self, expr: SExpr) -> Option<T> {
254+
let inner = self.0.borrow();
255+
256+
if expr.is_atom() {
257+
let data = inner.strings[expr.index()].as_str();
258+
return T::try_parse_t(data, false);
259+
}
260+
261+
if expr.is_list() {
262+
let data = inner.lists[expr.index()].as_slice();
263+
264+
if data.len() != 2 || data.iter().any(|expr| !expr.is_atom()) {
265+
return None;
266+
}
267+
268+
let is_negated = match inner.strings[data[0].index()].as_str() {
269+
"-" => true,
270+
"+" => false,
271+
_ => return None,
272+
};
273+
274+
let r_data = inner.strings[data[1].index()].as_str();
275+
276+
return T::try_parse_t(r_data, is_negated);
277+
}
278+
279+
None
280+
}
281+
}
282+
283+
pub(crate) trait TryParseInt: Sized {
284+
fn try_parse_t(a: &str, negate: bool) -> Option<Self>;
285+
}
286+
287+
macro_rules! impl_get_int {
288+
( $( $ty:ty )* ) => {
289+
$(
290+
impl TryParseInt for $ty {
291+
fn try_parse_t(a: &str, negate: bool) -> Option<Self> {
292+
let x = if let Some(a) = a.strip_prefix("#x") {
293+
<$ty>::from_str_radix(a, 16).ok()?
294+
} else if let Some(a) = a.strip_prefix("#b") {
295+
<$ty>::from_str_radix(a , 2).ok()?
296+
} else {
297+
a.parse::<$ty>().ok()?
298+
};
299+
300+
if negate {
301+
return x.checked_neg();
302+
}
303+
304+
Some(x)
305+
}
306+
}
307+
)*
308+
};
216309
}
217310

311+
impl_get_int!(u8 u16 u32 u64 u128 usize i8 i16 i32 i64 i128 isize);
312+
218313
/// The data contents of an [`SExpr`][crate::SExpr].
219314
///
220315
/// ## Converting `SExprData` to an Integer
221316
///
222-
/// There are `TryFrom<SExprData>` implementations for common integer types that
223-
/// you can use:
317+
/// There are a variety of `Context::get_*` helper methods (such as for example
318+
/// [`Context::get_u8`] and [`Context::get_i64`]) to parse integers out of
319+
/// s-expressions. For example, you can use:
224320
///
225321
/// ```
226322
/// let mut ctx = easy_smt::ContextBuilder::new().build().unwrap();
227323
///
228324
/// let neg_one = ctx.binary(8, -1_i8);
229325
/// assert_eq!(ctx.display(neg_one).to_string(), "#b11111111");
230326
///
231-
/// let x = u8::try_from(ctx.get(neg_one)).unwrap();
327+
/// let x = ctx.get_u8(neg_one).unwrap();
232328
/// assert_eq!(x, 0xff);
233329
/// ```
234330
#[derive(Debug)]
@@ -652,7 +748,8 @@ mod tests {
652748
.expect_err("Single atom doesn't close a list")
653749
.expect_more();
654750

655-
let expr = p.parse(&arena, ")")
751+
let expr = p
752+
.parse(&arena, ")")
656753
.expect("Closing paren should finish the parse");
657754

658755
let SExprData::List(es) = arena.get(expr) else {

0 commit comments

Comments
 (0)