taco_model_checker/internal_spec/
upwards_closed_set.rs

1//! Module for implementing atomic proposition types for model checking of
2//! threshold automata
3//!
4//! This module implements the basic specification types for parameterized model
5//! checking of threshold automata, as well as some helper functions that are
6//! useful when translating form a specification language.
7
8use core::fmt;
9use std::{
10    borrow::Borrow,
11    cmp::max,
12    collections::{HashMap, HashSet},
13};
14
15use taco_display_utils::join_iterator;
16use taco_smt_encoder::expression_encoding::{EncodeToSMT, SMTSolverError, SMTVariableContext};
17use taco_threshold_automaton::{
18    VariableConstraint,
19    expressions::{And, BooleanConnective, Location, Or, Parameter, Variable, fraction::Fraction},
20    impl_bitand, impl_bitor,
21    lia_threshold_automaton::{
22        ConstraintRewriteError, LIAVariableConstraint,
23        integer_thresholds::{DeriveFromIntegerComp, ThresholdCompOp, ThresholdConstraint},
24    },
25};
26
27use crate::{TASpecification, internal_spec::Disjunction};
28
29/// Type representing an upwards closed set of configurations
30///
31/// This type represents an upwards closed set of configurations symbolically.
32/// Therefore, it can be seen as disjunction over [UpwardsClosedClause]
33/// (i.e., since the clauses build a disjunction, it can be seen as a formula in
34/// DNF). Its purpose is to serve as the low-level characterization of an error
35/// state when model checking.
36///
37/// To create a new [UpwardsClosedSet] use the `new` methods and combine them
38/// using the [And] and [Or] implementations. For an [UpwardsClosedSet] they can
39/// also be thought of as taking the intersection or the union.
40#[derive(Debug, Clone, PartialEq)]
41pub struct UpwardsClosedSet {
42    /// Set of clauses treated as a disjunction over all clauses
43    clauses: Disjunction<UpwardsClosedClause>,
44}
45
46impl UpwardsClosedSet {
47    /// Create a new [UpwardsClosedSet] which is unconstrained, i.e., contains
48    /// all possible configurations
49    pub fn new_top() -> Self {
50        Self {
51            clauses: [UpwardsClosedClause::new_top()].into(),
52        }
53    }
54
55    /// Check whether this set contains all possible configurations / is a
56    /// tautology
57    pub fn is_top(&self) -> bool {
58        self.clauses.iter().any(|c| c.is_top())
59    }
60
61    /// Create a new [UpwardsClosedSet] that is not inhabited, i.e., it contains
62    /// no configurations
63    pub fn new_bot() -> Self {
64        Self { clauses: [].into() }
65    }
66
67    /// Check whether the current set of constraints is unsatisfiable
68    pub fn is_bot(&self) -> bool {
69        self.clauses.is_empty()
70    }
71
72    /// Create new [UpwardsClosedSet] which contains all configurations
73    /// satisfying given constrain
74    pub fn new_var_constraint(var_constr: LIAVariableConstraint) -> Self {
75        let apc = UpwardsClosedClause::new().with_variable_constraint(var_constr);
76
77        Self::new_from_clause(apc)
78    }
79
80    /// Create a new [UpwardsClosedSet] which contains all configurations for
81    /// which all locations given in `cover` are occupied by at least one
82    /// process
83    pub fn new_cover<L: Borrow<Location>, I: IntoIterator<Item = L>>(cover: I) -> Self {
84        let apc = UpwardsClosedClause::new().with_locs_to_cover(cover);
85
86        Self::new_from_clause(apc)
87    }
88
89    /// Create a new [UpwardsClosedSet] requiring each location in `cover` to
90    /// contain at least the given number of processes
91    pub fn new_cover_int<L: Borrow<Location>, I: IntoIterator<Item = (L, u32)>>(cover: I) -> Self {
92        let apc = UpwardsClosedClause::new().with_lower_bounds(cover);
93
94        Self::new_from_clause(apc)
95    }
96
97    /// Create a new [UpwardsClosedSet] requiring each location in `cover` to
98    /// contain at least the given number of processes, and each location in
99    /// `empty` to contain no processes
100    pub fn new_reach<
101        L: Borrow<Location>,
102        I: IntoIterator<Item = (L, u32)>,
103        II: IntoIterator<Item = L>,
104    >(
105        cover: I,
106        empty: II,
107    ) -> Self {
108        let apc = UpwardsClosedClause::new()
109            .with_lower_bounds(cover)
110            .with_locs_to_empty(empty);
111
112        Self::new_from_clause(apc)
113    }
114
115    /// Create a new [UpwardsClosedSet] from a single clause
116    fn new_from_clause(clause: UpwardsClosedClause) -> Self {
117        Self {
118            clauses: [clause].into(),
119        }
120    }
121
122    /// Check whether this constraint contains a reachability constraint
123    ///
124    /// A reachability constraint requires at least one location to be empty,
125    /// this function checks whether any of the clauses (see
126    /// [UpwardsClosedClause]) contains a reachability specification.
127    pub fn contains_reachability_constraint(&self) -> bool {
128        self.clauses
129            .iter()
130            .any(|a| a.contains_reachability_constraint())
131    }
132
133    /// Iterator over the individual upwards closed clauses
134    pub fn upwards_closed_clauses(&self) -> impl Iterator<Item = &UpwardsClosedClause> {
135        self.clauses.iter()
136    }
137}
138
139impl TASpecification for UpwardsClosedSet {
140    fn locs_appearing(&self) -> impl IntoIterator<Item = &Location> {
141        self.clauses.iter().flat_map(|a| a.locs_appearing())
142    }
143
144    fn var_constraint(&self) -> impl IntoIterator<Item = &LIAVariableConstraint> {
145        self.clauses.iter().flat_map(|a| a.var_constraint())
146    }
147}
148
149impl DeriveFromIntegerComp<Location, UpwardsClosedSetExtractionError> for UpwardsClosedSet {
150    fn form_ordered_constr(
151        scaled_t: HashMap<Location, Fraction>,
152        mut thr_constr: ThresholdConstraint,
153    ) -> Result<Self, UpwardsClosedSetExtractionError> {
154        if scaled_t.len() != 1 {
155            return Err(
156                UpwardsClosedSetExtractionError::LocationConstraintMultiLocation(Box::new((
157                    scaled_t, thr_constr,
158                ))),
159            );
160        }
161
162        let (loc, scale) = scaled_t.into_iter().next().unwrap();
163        if scale.is_zero() {
164            unreachable!(
165                "Invalid target constraint constructed containing only parameters (locations are multiplied by zero)."
166            );
167        }
168        thr_constr.scale(scale.inverse());
169
170        if !thr_constr.get_threshold().is_constant() {
171            return Err(
172                UpwardsClosedSetExtractionError::LocationConstraintWithParameters(Box::new((
173                    loc, thr_constr,
174                ))),
175            );
176        }
177        let mut c = thr_constr.get_threshold().get_const().unwrap();
178
179        match thr_constr.get_op() {
180            ThresholdCompOp::Geq | ThresholdCompOp::Gt => {
181                // For >: add one if ceil does not increase
182                if ThresholdCompOp::Gt == thr_constr.get_op() && c.is_integer() {
183                    c += Fraction::from(1);
184                }
185
186                if c.is_negative() || c.is_zero() {
187                    return Ok(UpwardsClosedSet::new_top());
188                }
189
190                let c = c.get_ceil().unwrap();
191                Ok(UpwardsClosedSet::new_from_clause(
192                    UpwardsClosedClause::new().with_lower_bounds([(loc, c)]),
193                ))
194            }
195            ThresholdCompOp::Lt | ThresholdCompOp::Leq => {
196                // For <=: If the floor count does not
197                if ThresholdCompOp::Leq == thr_constr.get_op() && c.is_integer() {
198                    c += Fraction::from(1);
199                }
200
201                // Since we are treating integers, this constraint is equivalent
202                // to \bot
203                if c.is_zero() || c.is_negative() {
204                    return Ok(UpwardsClosedSet::new_bot());
205                }
206
207                // < 1 --> Can be translated to 0
208                if c.get_ceil() == Some(1) {
209                    return Ok(UpwardsClosedSet::new_from_clause(
210                        UpwardsClosedClause::new().with_locs_to_empty([loc]),
211                    ));
212                }
213
214                Err(
215                    UpwardsClosedSetExtractionError::LocationConstraintNotUpwardsClosed(Box::new(
216                        (loc, thr_constr),
217                    )),
218                )
219            }
220        }
221    }
222}
223
224impl Or for UpwardsClosedSet {
225    fn or(mut self, other: Self) -> Self {
226        if self.is_top() || other.is_top() {
227            return Self::new_top();
228        }
229
230        if self.is_bot() {
231            return other;
232        }
233        if other.is_bot() {
234            return self;
235        }
236
237        self.clauses = self.clauses.or(other.clauses);
238        self
239    }
240}
241impl_bitor!(UpwardsClosedSet);
242
243impl And for UpwardsClosedSet {
244    fn and(self, other: Self) -> Self {
245        if self.is_bot() || other.is_bot() {
246            return UpwardsClosedSet::new_bot();
247        }
248
249        if self.is_top() {
250            return other;
251        }
252        if other.is_top() {
253            return self;
254        }
255
256        let aps = self
257            .clauses
258            .into_iter()
259            .flat_map(|s_apc| {
260                other
261                    .clauses
262                    .iter()
263                    .map(move |o_apc| s_apc.clone() & o_apc.clone())
264            })
265            .collect();
266
267        Self { clauses: aps }
268    }
269}
270impl_bitand!(UpwardsClosedSet);
271
272impl<C: SMTVariableContext<Location> + SMTVariableContext<Variable> + SMTVariableContext<Parameter>>
273    EncodeToSMT<UpwardsClosedSet, C> for UpwardsClosedSet
274{
275    fn encode_to_smt_with_ctx(
276        &self,
277        solver: &taco_smt_encoder::SMTSolver,
278        ctx: &C,
279    ) -> Result<taco_smt_encoder::SMTExpr, SMTSolverError> {
280        if self.clauses.is_empty() {
281            return Ok(solver.false_());
282        }
283
284        let disjuncts = self
285            .clauses
286            .iter()
287            .map(|c| c.encode_to_smt_with_ctx(solver, ctx))
288            .collect::<Result<Vec<_>, SMTSolverError>>()?;
289
290        Ok(solver.or_many(disjuncts))
291    }
292}
293
294impl fmt::Display for UpwardsClosedSet {
295    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
296        write!(f, "{}", join_iterator(self.clauses.iter(), " || "))
297    }
298}
299
300/// Errors that can occur when attempting to extract an upwards closed set of
301/// configurations
302#[derive(Debug, Clone, PartialEq)]
303pub enum UpwardsClosedSetExtractionError {
304    /// Found a constraint involving multiple locations, which is unsupported
305    LocationConstraintMultiLocation(Box<(HashMap<Location, Fraction>, ThresholdConstraint)>),
306    /// Specification uses non-linear expressions, therefore not upwards closed set can be extracted
307    LIARewriteError(Box<ConstraintRewriteError>),
308    /// Constraint on process in a specific location is not upwards closed
309    /// (this can stem from constraints of the form `l < 42`)
310    LocationConstraintNotUpwardsClosed(Box<(Location, ThresholdConstraint)>),
311    /// Constraints on locations contain parameters
312    LocationConstraintWithParameters(Box<(Location, ThresholdConstraint)>),
313    /// Expression contains the temporal operator that is not being collapsed
314    /// during extraction of the upwards closed set (e.g. a `<>` inside an
315    /// `[]`-specification)
316    NestedTemporalOperator,
317}
318
319impl From<ConstraintRewriteError> for UpwardsClosedSetExtractionError {
320    fn from(err: ConstraintRewriteError) -> Self {
321        Self::LIARewriteError(Box::new(err))
322    }
323}
324
325impl fmt::Display for UpwardsClosedSetExtractionError {
326    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
327        match self {
328            UpwardsClosedSetExtractionError::LocationConstraintMultiLocation(cstr) => {
329                write!(
330                    f,
331                    "Multiple locations referenced in constraint: {} {}",
332                    join_iterator(cstr.0.iter().map(|(l, f)| format!("{f} * {l}")), "+ "),
333                    cstr.1
334                )
335            }
336            UpwardsClosedSetExtractionError::LIARewriteError(err) => {
337                write!(f, "Failed to rewrite to linear arithmetic: {}", err)
338            }
339            UpwardsClosedSetExtractionError::LocationConstraintNotUpwardsClosed(x) => {
340                write!(
341                    f,
342                    "Constraint on location '{}' not upwards closed. Constraint: {}{}",
343                    x.0, x.0, x.1
344                )
345            }
346            UpwardsClosedSetExtractionError::LocationConstraintWithParameters(x) => write!(
347                f,
348                "Constraint on location '{}' uses parameters. Constraint: {}{}",
349                x.0, x.0, x.1
350            ),
351            UpwardsClosedSetExtractionError::NestedTemporalOperator => write!(
352                f,
353                "Expression contains the other temporal operator, which cannot be transformed into an upwards closed set"
354            ),
355        }
356    }
357}
358
359impl std::error::Error for UpwardsClosedSetExtractionError {}
360
361/// Description of an upwards closed set of configurations of a threshold
362/// automaton
363///
364/// An upwards closed set of configurations can be seen as the conjunction of
365/// three different types of constraints:
366/// - a set of locations which are not allowed to contain any processes
367/// - a map of locations to integer bounds, where the bounds represent minimal
368///   the number of processes that need to be present in the respective location
369/// - constraints on the shared variable evaluations
370///
371/// Any configuration of a threshold automaton that fulfills the constraints is
372/// then said to be in the set.
373///
374/// This type should usually not be created directly. Instead, use the
375/// [UpwardsClosedSet] type (with a single clause).
376#[derive(Clone, Debug, PartialEq)]
377pub struct UpwardsClosedClause {
378    /// Location should not be covered by any processes
379    locs_no_procs: HashSet<Location>,
380    /// Map with location + number of processes at least in there
381    locs_lower_bounds: HashMap<Location, u32>,
382    /// conjunct of variable constraints
383    variable_constr: LIAVariableConstraint,
384}
385
386impl UpwardsClosedClause {
387    /// Get the constraint over the shared variable valuations
388    pub fn variable_constr(&self) -> &LIAVariableConstraint {
389        &self.variable_constr
390    }
391
392    /// Returns an iterator over locations and the respective lower bound on how
393    /// many processes need to be in the location to be in the set
394    pub fn locs_to_cover(&self) -> impl Iterator<Item = (&Location, &u32)> {
395        self.locs_lower_bounds.iter()
396    }
397
398    /// Returns the locations where no process is allowed to be in
399    pub fn locs_to_uncover(&self) -> impl Iterator<Item = &Location> {
400        self.locs_no_procs.iter()
401    }
402
403    /// Create a new upwards closed set that contains all possible configurations
404    pub fn new_top() -> Self {
405        Self::new()
406    }
407
408    /// Check whether this clause is a tautology, i.e., contains all possible
409    /// configurations
410    pub fn is_top(&self) -> bool {
411        self.locs_lower_bounds.is_empty()
412            && self.locs_no_procs.is_empty()
413            && self.variable_constr == LIAVariableConstraint::True
414    }
415
416    /// Creates a new empty set of atomic propositions
417    ///
418    /// Such an upwards closed set is equivalent to a constraint `true` or the
419    /// set of all configurations
420    fn new() -> Self {
421        Self {
422            locs_lower_bounds: HashMap::new(),
423            locs_no_procs: HashSet::new(),
424            variable_constr: LIAVariableConstraint::True,
425        }
426    }
427
428    /// Add a locations where at least one process must be present
429    ///
430    /// If a lower bound constraint for a specific location has been previously
431    /// added, this function will merge the constraints by taking the maximum of
432    /// the lower bounds
433    fn with_locs_to_cover<I: Borrow<Location>, L: IntoIterator<Item = I>>(
434        mut self,
435        cover: L,
436    ) -> Self {
437        cover.into_iter().for_each(|l| {
438            if let Some(bound) = self.locs_lower_bounds.get_mut(l.borrow()) {
439                *bound = max(*bound, 1);
440                return;
441            }
442
443            self.locs_lower_bounds.insert(l.borrow().clone(), 1);
444        });
445
446        self
447    }
448
449    /// Add lower bounds for a set of locations
450    ///
451    /// If a lower bound constraint for a specific location has been previously
452    /// added, this function will merge the constraints by taking the maximum of
453    /// the lower bounds
454    fn with_lower_bounds<I: Borrow<Location>, N: Into<u32>, L: IntoIterator<Item = (I, N)>>(
455        mut self,
456        cover: L,
457    ) -> Self {
458        cover.into_iter().for_each(|(l, n)| {
459            if let Some(bound) = self.locs_lower_bounds.get_mut(l.borrow()) {
460                *bound = max(*bound, n.into());
461                return;
462            }
463
464            self.locs_lower_bounds.insert(l.borrow().clone(), n.into());
465        });
466
467        self
468    }
469
470    /// Add locations which are not allowed to be covered
471    fn with_locs_to_empty<I: Borrow<Location>, L: IntoIterator<Item = I>>(
472        mut self,
473        locs: L,
474    ) -> Self {
475        locs.into_iter().for_each(|l| {
476            self.locs_no_procs.insert(l.borrow().clone());
477        });
478        self
479    }
480
481    /// Add a constraint on the shared variable valuation
482    ///
483    /// If a constraint has been previously added, the resulting variable
484    /// constraint will be the conjunction of the previous and the new one
485    fn with_variable_constraint(mut self, constr: LIAVariableConstraint) -> Self {
486        if constr == LIAVariableConstraint::True {
487            return self;
488        }
489
490        if self.variable_constr == LIAVariableConstraint::True {
491            self.variable_constr = constr;
492            return self;
493        }
494
495        self.variable_constr = LIAVariableConstraint::BinaryGuard(
496            Box::new(self.variable_constr),
497            BooleanConnective::And,
498            Box::new(constr),
499        );
500
501        self
502    }
503
504    /// Check whether the upwards closed set contains a reachability constraint,
505    /// i.e., a constraint where at least one location is not allowed to be
506    /// covered
507    fn contains_reachability_constraint(&self) -> bool {
508        !self.locs_no_procs.is_empty()
509    }
510}
511
512impl TASpecification for UpwardsClosedClause {
513    fn locs_appearing(&self) -> impl IntoIterator<Item = &Location> {
514        self.locs_lower_bounds
515            .keys()
516            .chain(self.locs_no_procs.iter())
517    }
518
519    fn var_constraint(&self) -> impl IntoIterator<Item = &LIAVariableConstraint> {
520        [&self.variable_constr]
521    }
522}
523
524impl_bitand!(UpwardsClosedClause);
525
526impl And for UpwardsClosedClause {
527    fn and(self, other: Self) -> Self {
528        self.with_lower_bounds(other.locs_lower_bounds.iter().map(|(l, n)| (l, *n)))
529            .with_locs_to_empty(other.locs_no_procs)
530            .with_variable_constraint(other.variable_constr)
531    }
532}
533
534impl fmt::Display for UpwardsClosedClause {
535    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
536        let lower_bounds = join_iterator(
537            self.locs_lower_bounds
538                .iter()
539                .map(|(loc, n)| format!("({loc} >= {n})"))
540                .chain(self.locs_no_procs.iter().map(|loc| format!("({loc} == 0)"))),
541            " && ",
542        );
543
544        write!(f, "{lower_bounds}")?;
545
546        if self.variable_constr != LIAVariableConstraint::True {
547            if !lower_bounds.is_empty() {
548                write!(f, " && ")?;
549            }
550            write!(f, "{}", self.variable_constr)?;
551        }
552
553        Ok(())
554    }
555}
556
557impl<C: SMTVariableContext<Location> + SMTVariableContext<Variable> + SMTVariableContext<Parameter>>
558    EncodeToSMT<UpwardsClosedClause, C> for UpwardsClosedClause
559{
560    fn encode_to_smt_with_ctx(
561        &self,
562        solver: &taco_smt_encoder::SMTSolver,
563        ctx: &C,
564    ) -> Result<taco_smt_encoder::SMTExpr, SMTSolverError> {
565        // lower bounds
566        let lower_bounds = self
567            .locs_lower_bounds
568            .iter()
569            .map(|(loc, n)| {
570                let loc = ctx.get_expr_for(loc)?;
571                let n = solver.numeral(*n);
572
573                Ok(solver.gte(loc, n))
574            })
575            .collect::<Result<Vec<_>, SMTSolverError>>()?;
576
577        // locations that should not be covered
578        let loc_uncover = self
579            .locs_no_procs
580            .iter()
581            .map(|loc| {
582                let loc = ctx.get_expr_for(loc)?;
583                let zero = solver.numeral(0);
584
585                Ok(solver.eq(loc, zero))
586            })
587            .collect::<Result<Vec<_>, SMTSolverError>>()?;
588
589        // constraint on variable evaluation
590        let var_constr = self
591            .variable_constr
592            .as_boolean_expr()
593            .encode_to_smt_with_ctx(solver, ctx)?;
594
595        let res = solver.and_many(
596            lower_bounds
597                .into_iter()
598                .chain(loc_uncover)
599                .chain([var_constr]),
600        );
601
602        Ok(res)
603    }
604}
605
606#[cfg(test)]
607mod tests {
608    use std::collections::{HashMap, HashSet};
609
610    use taco_smt_encoder::{
611        SMTSolverBuilder, SMTSolverContext,
612        expression_encoding::{EncodeToSMT, SMTVariableContext, StaticSMTContext},
613    };
614    use taco_threshold_automaton::{
615        BooleanVarConstraint,
616        expressions::{ComparisonOp, IntegerExpression, IntegerOp, Location, Parameter, Variable},
617        lia_threshold_automaton::{
618            LIAVariableConstraint, integer_thresholds::DeriveFromIntegerComp,
619        },
620    };
621
622    use crate::{
623        TASpecification,
624        internal_spec::upwards_closed_set::{
625            UpwardsClosedClause, UpwardsClosedSet, UpwardsClosedSetExtractionError,
626        },
627    };
628
629    #[test]
630    fn test_target_config_new_cover() {
631        let cover = UpwardsClosedSet::new_cover([
632            Location::new("l1"),
633            Location::new("l2"),
634            Location::new("l3"),
635        ]);
636
637        let expected = UpwardsClosedSet {
638            clauses: [UpwardsClosedClause {
639                locs_lower_bounds: HashMap::from([
640                    (Location::new("l1"), 1),
641                    (Location::new("l2"), 1),
642                    (Location::new("l3"), 1),
643                ]),
644                locs_no_procs: HashSet::new(),
645                variable_constr: LIAVariableConstraint::True,
646            }]
647            .into(),
648        };
649
650        assert_eq!(cover, expected);
651    }
652
653    #[test]
654    fn test_target_config_new_reach() {
655        let reach = UpwardsClosedSet::new_reach(
656            [
657                (Location::new("l1"), 1),
658                (Location::new("l2"), 1),
659                (Location::new("l3"), 1),
660            ],
661            [
662                Location::new("l4"),
663                Location::new("l5"),
664                Location::new("l6"),
665            ],
666        );
667
668        let expected = UpwardsClosedSet {
669            clauses: [UpwardsClosedClause {
670                locs_lower_bounds: HashMap::from([
671                    (Location::new("l1"), 1),
672                    (Location::new("l2"), 1),
673                    (Location::new("l3"), 1),
674                ]),
675                locs_no_procs: HashSet::from([
676                    Location::new("l4"),
677                    Location::new("l5"),
678                    Location::new("l6"),
679                ]),
680                variable_constr: LIAVariableConstraint::True,
681            }]
682            .into(),
683        };
684
685        assert_eq!(reach, expected);
686    }
687
688    // This test tests a private method but this method is crucial for correctness
689    #[test]
690    fn test_disjunct_from_integer() {
691        // l == 0
692        let got = UpwardsClosedSet::from_integer_expr(
693            IntegerExpression::Atom(Location::new("l")),
694            ComparisonOp::Eq,
695            IntegerExpression::Const(0),
696        );
697        assert!(got.is_ok());
698
699        let expected = UpwardsClosedSet {
700            clauses: [UpwardsClosedClause {
701                locs_lower_bounds: HashMap::new(),
702                locs_no_procs: HashSet::from([Location::new("l")]),
703                variable_constr: LIAVariableConstraint::True,
704            }]
705            .into(),
706        };
707
708        assert_eq!(got.unwrap(), expected);
709
710        // l != 0
711        let got = UpwardsClosedSet::from_integer_expr(
712            IntegerExpression::Atom(Location::new("l")),
713            ComparisonOp::Neq,
714            IntegerExpression::Const(0),
715        );
716        assert!(got.is_ok());
717
718        let expected = UpwardsClosedSet {
719            clauses: [UpwardsClosedClause {
720                locs_lower_bounds: HashMap::from([(Location::new("l"), 1)]),
721                locs_no_procs: HashSet::new(),
722                variable_constr: LIAVariableConstraint::True,
723            }]
724            .into(),
725        };
726
727        assert_eq!(got.unwrap(), expected);
728
729        // l > 0
730        let got = UpwardsClosedSet::from_integer_expr(
731            IntegerExpression::Atom(Location::new("l")),
732            ComparisonOp::Gt,
733            IntegerExpression::Const(0),
734        );
735        assert!(got.is_ok());
736
737        let expected = UpwardsClosedSet {
738            clauses: [UpwardsClosedClause {
739                locs_lower_bounds: HashMap::from([(Location::new("l"), 1)]),
740                locs_no_procs: HashSet::new(),
741                variable_constr: LIAVariableConstraint::True,
742            }]
743            .into(),
744        };
745
746        assert_eq!(got.unwrap(), expected);
747
748        // l > 42
749        let got = UpwardsClosedSet::from_integer_expr(
750            IntegerExpression::Atom(Location::new("l")),
751            ComparisonOp::Gt,
752            IntegerExpression::Const(42),
753        );
754        assert!(got.is_ok());
755
756        let expected = UpwardsClosedSet {
757            clauses: [UpwardsClosedClause {
758                locs_lower_bounds: HashMap::from([(Location::new("l"), 43)]),
759                locs_no_procs: HashSet::new(),
760                variable_constr: LIAVariableConstraint::True,
761            }]
762            .into(),
763        };
764
765        assert_eq!(got.unwrap(), expected);
766
767        // l >= 42
768        let got = UpwardsClosedSet::from_integer_expr(
769            IntegerExpression::Atom(Location::new("l")),
770            ComparisonOp::Geq,
771            IntegerExpression::Const(42),
772        );
773        assert!(got.is_ok());
774
775        let expected = UpwardsClosedSet {
776            clauses: [UpwardsClosedClause {
777                locs_lower_bounds: HashMap::from([(Location::new("l"), 42)]),
778                locs_no_procs: HashSet::new(),
779                variable_constr: LIAVariableConstraint::True,
780            }]
781            .into(),
782        };
783
784        assert_eq!(got.unwrap(), expected);
785
786        // l > 2/3
787        let got = UpwardsClosedSet::from_integer_expr(
788            IntegerExpression::Atom(Location::new("l")),
789            ComparisonOp::Gt,
790            IntegerExpression::BinaryExpr(
791                Box::new(IntegerExpression::Const(2)),
792                IntegerOp::Div,
793                Box::new(IntegerExpression::Const(3)),
794            ),
795        );
796        assert!(got.is_ok());
797
798        let expected = UpwardsClosedSet {
799            clauses: [UpwardsClosedClause {
800                locs_lower_bounds: HashMap::from([(Location::new("l"), 1)]),
801                locs_no_procs: HashSet::new(),
802                variable_constr: LIAVariableConstraint::True,
803            }]
804            .into(),
805        };
806
807        assert_eq!(got.unwrap(), expected);
808
809        // l >= 2/3
810        let got = UpwardsClosedSet::from_integer_expr(
811            IntegerExpression::Atom(Location::new("l")),
812            ComparisonOp::Geq,
813            IntegerExpression::BinaryExpr(
814                Box::new(IntegerExpression::Const(2)),
815                IntegerOp::Div,
816                Box::new(IntegerExpression::Const(3)),
817            ),
818        );
819        assert!(got.is_ok());
820
821        let expected = UpwardsClosedSet {
822            clauses: [UpwardsClosedClause {
823                locs_lower_bounds: HashMap::from([(Location::new("l"), 1)]),
824                locs_no_procs: HashSet::new(),
825                variable_constr: LIAVariableConstraint::True,
826            }]
827            .into(),
828        };
829
830        assert_eq!(got.unwrap(), expected);
831
832        //  42 < l --> l > 42
833        let got = UpwardsClosedSet::from_integer_expr(
834            IntegerExpression::Const(42),
835            ComparisonOp::Lt,
836            IntegerExpression::Atom(Location::new("l")),
837        );
838        assert!(got.is_ok(), "{:#?}", got);
839
840        let expected = UpwardsClosedSet {
841            clauses: [UpwardsClosedClause {
842                locs_lower_bounds: HashMap::from([(Location::new("l"), 43)]),
843                locs_no_procs: HashSet::new(),
844                variable_constr: LIAVariableConstraint::True,
845            }]
846            .into(),
847        };
848
849        assert_eq!(got.unwrap(), expected);
850
851        // l > 0 + 1 + 2
852        let got = UpwardsClosedSet::from_integer_expr(
853            IntegerExpression::Atom(Location::new("l")),
854            ComparisonOp::Gt,
855            IntegerExpression::BinaryExpr(
856                Box::new(IntegerExpression::Const(0)),
857                IntegerOp::Add,
858                Box::new(IntegerExpression::BinaryExpr(
859                    Box::new(IntegerExpression::Const(1)),
860                    IntegerOp::Add,
861                    Box::new(IntegerExpression::Const(2)),
862                )),
863            ),
864        );
865        assert!(got.is_ok());
866
867        let expected = UpwardsClosedSet {
868            clauses: [UpwardsClosedClause {
869                locs_lower_bounds: HashMap::from([(Location::new("l"), 4)]),
870                locs_no_procs: HashSet::new(),
871                variable_constr: LIAVariableConstraint::True,
872            }]
873            .into(),
874        };
875
876        assert_eq!(got.unwrap(), expected);
877
878        // l < 1
879        let got = UpwardsClosedSet::from_integer_expr(
880            IntegerExpression::Atom(Location::new("l")),
881            ComparisonOp::Lt,
882            IntegerExpression::Const(1),
883        );
884        assert!(got.is_ok());
885
886        let expected = UpwardsClosedSet {
887            clauses: [UpwardsClosedClause {
888                locs_lower_bounds: HashMap::new(),
889                locs_no_procs: HashSet::from([Location::new("l")]),
890                variable_constr: LIAVariableConstraint::True,
891            }]
892            .into(),
893        };
894
895        assert_eq!(got.unwrap(), expected);
896
897        // l <= 0
898        let got = UpwardsClosedSet::from_integer_expr(
899            IntegerExpression::Atom(Location::new("l")),
900            ComparisonOp::Leq,
901            IntegerExpression::Const(0),
902        );
903        assert!(got.is_ok());
904
905        let expected = UpwardsClosedSet {
906            clauses: [UpwardsClosedClause {
907                locs_lower_bounds: HashMap::new(),
908                locs_no_procs: HashSet::from([Location::new("l")]),
909                variable_constr: LIAVariableConstraint::True,
910            }]
911            .into(),
912        };
913
914        assert_eq!(got.unwrap(), expected);
915    }
916
917    // This test tests a private method but this method is crucial for correctness
918    #[test]
919    fn test_target_config_try_loc_constr_error_cases() {
920        // l1 + l2 == 0
921        let got = UpwardsClosedSet::from_integer_expr(
922            IntegerExpression::BinaryExpr(
923                Box::new(IntegerExpression::Atom(Location::new("l1"))),
924                IntegerOp::Add,
925                Box::new(IntegerExpression::Atom(Location::new("l2"))),
926            ),
927            ComparisonOp::Eq,
928            IntegerExpression::Const(0),
929        );
930        assert!(got.is_err(), "{:#?}", got);
931
932        assert!(matches!(
933            got.unwrap_err(),
934            UpwardsClosedSetExtractionError::LocationConstraintMultiLocation(_)
935        ));
936
937        // l * l == 0
938        let got = UpwardsClosedSet::from_integer_expr(
939            IntegerExpression::BinaryExpr(
940                Box::new(IntegerExpression::Atom(Location::new("l"))),
941                IntegerOp::Mul,
942                Box::new(IntegerExpression::Atom(Location::new("l"))),
943            ),
944            ComparisonOp::Eq,
945            IntegerExpression::Const(0),
946        );
947        assert!(got.is_err(), "{:#?}", got);
948
949        assert!(matches!(
950            got.unwrap_err(),
951            UpwardsClosedSetExtractionError::LIARewriteError(_)
952        ));
953
954        // l + n == 0
955        let got = UpwardsClosedSet::from_integer_expr(
956            IntegerExpression::BinaryExpr(
957                Box::new(IntegerExpression::Atom(Location::new("l"))),
958                IntegerOp::Add,
959                Box::new(IntegerExpression::Param(Parameter::new("n"))),
960            ),
961            ComparisonOp::Eq,
962            IntegerExpression::Const(0),
963        );
964        assert!(got.is_err(), "{:#?}", got);
965
966        assert!(matches!(
967            got.unwrap_err(),
968            UpwardsClosedSetExtractionError::LocationConstraintWithParameters(_)
969        ));
970
971        // l < 3
972        let got = UpwardsClosedSet::from_integer_expr(
973            IntegerExpression::Atom(Location::new("l")),
974            ComparisonOp::Lt,
975            IntegerExpression::Const(3),
976        );
977        assert!(got.is_err(), "{:#?}", got);
978
979        assert!(matches!(
980            got.unwrap_err(),
981            UpwardsClosedSetExtractionError::LocationConstraintNotUpwardsClosed(_)
982        ));
983
984        // l <= 3
985        let got = UpwardsClosedSet::from_integer_expr(
986            IntegerExpression::Atom(Location::new("l")),
987            ComparisonOp::Leq,
988            IntegerExpression::Const(3),
989        );
990        assert!(got.is_err(), "{:#?}", got);
991
992        assert!(matches!(
993            got.unwrap_err(),
994            UpwardsClosedSetExtractionError::LocationConstraintNotUpwardsClosed(_)
995        ));
996
997        // l == 3
998        let got = UpwardsClosedSet::from_integer_expr(
999            IntegerExpression::Atom(Location::new("l")),
1000            ComparisonOp::Eq,
1001            IntegerExpression::Const(3),
1002        );
1003        assert!(got.is_err(), "{:#?}", got);
1004
1005        assert!(matches!(
1006            got.unwrap_err(),
1007            UpwardsClosedSetExtractionError::LocationConstraintNotUpwardsClosed(_)
1008        ));
1009
1010        // l != 3
1011        let got = UpwardsClosedSet::from_integer_expr(
1012            IntegerExpression::Atom(Location::new("l")),
1013            ComparisonOp::Neq,
1014            IntegerExpression::Const(3),
1015        );
1016        assert!(got.is_err(), "{:#?}", got);
1017
1018        assert!(matches!(
1019            got.unwrap_err(),
1020            UpwardsClosedSetExtractionError::LocationConstraintNotUpwardsClosed(_)
1021        ));
1022    }
1023
1024    #[test]
1025    fn test_target_config_encode_target_config_unconstrained() {
1026        let solver_builder = SMTSolverBuilder::default();
1027
1028        let ctx = StaticSMTContext::new(solver_builder, [], [], []).unwrap();
1029
1030        let config = UpwardsClosedSet::new_top();
1031
1032        let got_expr = config
1033            .encode_to_smt_with_ctx(ctx.get_smt_solver(), &ctx)
1034            .unwrap();
1035
1036        let expected_expr = ctx.get_true();
1037        assert_eq!(got_expr, expected_expr)
1038    }
1039
1040    #[test]
1041    fn test_target_config_encode_target_config_single_loc_cov() {
1042        let solver_builder = SMTSolverBuilder::default();
1043
1044        let ctx = StaticSMTContext::new(solver_builder, [], [Location::new("l")], []).unwrap();
1045
1046        let config = UpwardsClosedSet::new_cover([Location::new("l")]);
1047
1048        let got_expr = config
1049            .encode_to_smt_with_ctx(ctx.get_smt_solver(), &ctx)
1050            .unwrap();
1051
1052        let solver = ctx.get_smt_solver();
1053
1054        let expected_expr = solver.and(
1055            solver.gte(
1056                ctx.get_expr_for(&Location::new("l")).unwrap(),
1057                solver.numeral(1),
1058            ),
1059            solver.true_(),
1060        );
1061
1062        assert_eq!(
1063            got_expr,
1064            expected_expr,
1065            "got: {}, expected: {}",
1066            solver.display(got_expr),
1067            solver.display(expected_expr)
1068        )
1069    }
1070
1071    #[test]
1072    fn test_target_config_encode_target_config_single_loc_uncover() {
1073        let solver_builder = SMTSolverBuilder::default();
1074
1075        let ctx = StaticSMTContext::new(solver_builder, [], [Location::new("l")], []).unwrap();
1076
1077        let config = UpwardsClosedSet::new_reach([], [Location::new("l")]);
1078
1079        let got_expr = config
1080            .encode_to_smt_with_ctx(ctx.get_smt_solver(), &ctx)
1081            .unwrap();
1082
1083        let solver = ctx.get_smt_solver();
1084
1085        let expected_expr = solver.and(
1086            solver.eq(
1087                ctx.get_expr_for(&Location::new("l")).unwrap(),
1088                solver.numeral(0),
1089            ),
1090            solver.true_(),
1091        );
1092
1093        assert_eq!(
1094            got_expr,
1095            expected_expr,
1096            "got: {}, expected: {}",
1097            solver.display(got_expr),
1098            solver.display(expected_expr)
1099        )
1100    }
1101
1102    #[test]
1103    fn test_target_config_encode_target_config_var_constr() {
1104        let solver_builder = SMTSolverBuilder::default();
1105
1106        let ctx = StaticSMTContext::new(
1107            solver_builder,
1108            [],
1109            [Location::new("l")],
1110            [Variable::new("v")],
1111        )
1112        .unwrap();
1113
1114        let config = UpwardsClosedSet::new_var_constraint(
1115            BooleanVarConstraint::ComparisonExpression(
1116                Box::new(IntegerExpression::Atom(Variable::new("v"))),
1117                ComparisonOp::Eq,
1118                Box::new(IntegerExpression::Const(1)),
1119            )
1120            .try_into()
1121            .unwrap(),
1122        );
1123
1124        let got_expr = config
1125            .encode_to_smt_with_ctx(ctx.get_smt_solver(), &ctx)
1126            .unwrap();
1127
1128        let solver = ctx.get_smt_solver();
1129
1130        let expected_expr = solver.and(
1131            solver.lte(
1132                ctx.get_expr_for(&Variable::new("v")).unwrap(),
1133                solver.numeral(1),
1134            ),
1135            solver.gte(
1136                ctx.get_expr_for(&Variable::new("v")).unwrap(),
1137                solver.numeral(1),
1138            ),
1139        );
1140
1141        assert_eq!(
1142            got_expr,
1143            expected_expr,
1144            "got: {}, expected: {}",
1145            solver.display(got_expr),
1146            solver.display(expected_expr)
1147        )
1148    }
1149
1150    #[test]
1151    fn test_target_config_encode_target_config_all_constr() {
1152        let solver_builder = SMTSolverBuilder::default();
1153
1154        let ctx = StaticSMTContext::new(
1155            solver_builder,
1156            [],
1157            [Location::new("l1"), Location::new("l2")],
1158            [Variable::new("v")],
1159        )
1160        .unwrap();
1161
1162        let config =
1163            UpwardsClosedSet::new_reach([(Location::new("l1"), 42)], [Location::new("l2")])
1164                & UpwardsClosedSet::new_var_constraint(
1165                    BooleanVarConstraint::ComparisonExpression(
1166                        Box::new(IntegerExpression::Atom(Variable::new("v"))),
1167                        ComparisonOp::Eq,
1168                        Box::new(IntegerExpression::Const(1)),
1169                    )
1170                    .try_into()
1171                    .unwrap(),
1172                );
1173        let got_expr = config
1174            .encode_to_smt_with_ctx(ctx.get_smt_solver(), &ctx)
1175            .unwrap();
1176
1177        let solver = ctx.get_smt_solver();
1178
1179        let expected_expr = solver.and_many([
1180            solver.gte(
1181                ctx.get_expr_for(&Location::new("l1")).unwrap(),
1182                solver.numeral(42),
1183            ),
1184            solver.eq(
1185                ctx.get_expr_for(&Location::new("l2")).unwrap(),
1186                solver.numeral(0),
1187            ),
1188            solver.and(
1189                solver.lte(
1190                    ctx.get_expr_for(&Variable::new("v")).unwrap(),
1191                    solver.numeral(1),
1192                ),
1193                solver.gte(
1194                    ctx.get_expr_for(&Variable::new("v")).unwrap(),
1195                    solver.numeral(1),
1196                ),
1197            ),
1198        ]);
1199
1200        assert_eq!(
1201            got_expr,
1202            expected_expr,
1203            "got: {}, expected: {}",
1204            solver.display(got_expr),
1205            solver.display(expected_expr)
1206        )
1207    }
1208
1209    #[test]
1210    fn test_target_config_locations_appearing() {
1211        let config =
1212            UpwardsClosedSet::new_reach([(Location::new("l1"), 42)], [Location::new("l2")])
1213                & UpwardsClosedSet::new_var_constraint(
1214                    BooleanVarConstraint::ComparisonExpression(
1215                        Box::new(IntegerExpression::Atom(Variable::new("v"))),
1216                        ComparisonOp::Eq,
1217                        Box::new(IntegerExpression::Const(1)),
1218                    )
1219                    .try_into()
1220                    .unwrap(),
1221                );
1222
1223        let got_expr: HashSet<Location> = config.locs_appearing().into_iter().cloned().collect();
1224
1225        let expected_locs = HashSet::from([Location::new("l1"), Location::new("l2")]);
1226
1227        assert_eq!(got_expr, expected_locs)
1228    }
1229
1230    #[test]
1231    fn test_target_config_is_reachability_constr() {
1232        let config =
1233            UpwardsClosedSet::new_reach([(Location::new("l1"), 42)], [Location::new("l2")])
1234                & UpwardsClosedSet::new_var_constraint(
1235                    BooleanVarConstraint::ComparisonExpression(
1236                        Box::new(IntegerExpression::Atom(Variable::new("v"))),
1237                        ComparisonOp::Eq,
1238                        Box::new(IntegerExpression::Const(1)),
1239                    )
1240                    .try_into()
1241                    .unwrap(),
1242                );
1243
1244        assert!(config.contains_reachability_constraint());
1245
1246        let config = UpwardsClosedSet::new_reach([(Location::new("l1"), 42)], [])
1247            & UpwardsClosedSet::new_var_constraint(
1248                BooleanVarConstraint::ComparisonExpression(
1249                    Box::new(IntegerExpression::Atom(Variable::new("v"))),
1250                    ComparisonOp::Eq,
1251                    Box::new(IntegerExpression::Const(1)),
1252                )
1253                .try_into()
1254                .unwrap(),
1255            );
1256
1257        assert!(!config.contains_reachability_constraint());
1258    }
1259
1260    #[test]
1261    fn test_disjunction_target_config_get_locations_in_target() {
1262        let config1 =
1263            UpwardsClosedSet::new_reach([(Location::new("l1"), 42)], [Location::new("l2")])
1264                & UpwardsClosedSet::new_var_constraint(
1265                    BooleanVarConstraint::ComparisonExpression(
1266                        Box::new(IntegerExpression::Atom(Variable::new("v"))),
1267                        ComparisonOp::Eq,
1268                        Box::new(IntegerExpression::Const(1)),
1269                    )
1270                    .try_into()
1271                    .unwrap(),
1272                );
1273
1274        let config2 =
1275            UpwardsClosedSet::new_reach([(Location::new("l3"), 42)], [Location::new("l4")])
1276                & UpwardsClosedSet::new_var_constraint(
1277                    BooleanVarConstraint::ComparisonExpression(
1278                        Box::new(IntegerExpression::Atom(Variable::new("v"))),
1279                        ComparisonOp::Eq,
1280                        Box::new(IntegerExpression::Const(1)),
1281                    )
1282                    .try_into()
1283                    .unwrap(),
1284                );
1285
1286        let dis = config1 | config2;
1287
1288        let got_set_locations: HashSet<Location> =
1289            dis.locs_appearing().into_iter().cloned().collect();
1290
1291        let expected_set_locations = HashSet::from([
1292            Location::new("l1"),
1293            Location::new("l2"),
1294            Location::new("l3"),
1295            Location::new("l4"),
1296        ]);
1297
1298        assert_eq!(got_set_locations, expected_set_locations);
1299
1300        let dis = UpwardsClosedSet::new_bot();
1301
1302        let got_set_locations: HashSet<_> = dis.locs_appearing().into_iter().collect();
1303
1304        let expected_set_locations = HashSet::from([]);
1305
1306        assert_eq!(got_set_locations, expected_set_locations);
1307    }
1308
1309    #[test]
1310    fn test_disj_target_config_contains_reachability_constraint() {
1311        let config1 = UpwardsClosedSet::new_reach([(Location::new("l1"), 42)], [])
1312            & UpwardsClosedSet::new_var_constraint(
1313                BooleanVarConstraint::ComparisonExpression(
1314                    Box::new(IntegerExpression::Atom(Variable::new("v"))),
1315                    ComparisonOp::Eq,
1316                    Box::new(IntegerExpression::Const(1)),
1317                )
1318                .try_into()
1319                .unwrap(),
1320            );
1321
1322        let config2 =
1323            UpwardsClosedSet::new_reach([(Location::new("l3"), 42)], [Location::new("l4")])
1324                & UpwardsClosedSet::new_var_constraint(
1325                    BooleanVarConstraint::ComparisonExpression(
1326                        Box::new(IntegerExpression::Atom(Variable::new("v"))),
1327                        ComparisonOp::Eq,
1328                        Box::new(IntegerExpression::Const(1)),
1329                    )
1330                    .try_into()
1331                    .unwrap(),
1332                );
1333
1334        let dis = config1 | config2;
1335
1336        assert!(dis.contains_reachability_constraint());
1337
1338        let disj = UpwardsClosedSet::new_bot();
1339
1340        assert!(!disj.contains_reachability_constraint())
1341    }
1342
1343    #[test]
1344    fn test_disj_target_config_encode_to_smt_empty() {
1345        let solver_builder = SMTSolverBuilder::default();
1346
1347        let ctx = StaticSMTContext::new(solver_builder, [], [], []).unwrap();
1348
1349        let solver = ctx.get_smt_solver();
1350
1351        let disj = UpwardsClosedSet::new_bot();
1352
1353        let got_expr = disj.encode_to_smt_with_ctx(solver, &ctx).unwrap();
1354
1355        let expected_expr = solver.false_();
1356
1357        assert_eq!(
1358            got_expr,
1359            expected_expr,
1360            "got: {}, expected: {}",
1361            solver.display(got_expr),
1362            solver.display(expected_expr)
1363        )
1364    }
1365
1366    #[test]
1367    fn test_disj_target_config_encode_smt() {
1368        let solver_builder = SMTSolverBuilder::default();
1369
1370        let ctx = StaticSMTContext::new(
1371            solver_builder,
1372            [],
1373            [
1374                Location::new("l1"),
1375                Location::new("l2"),
1376                Location::new("l3"),
1377                Location::new("l4"),
1378            ],
1379            [Variable::new("v")],
1380        )
1381        .unwrap();
1382
1383        let solver = ctx.get_smt_solver();
1384
1385        let config1 =
1386            UpwardsClosedSet::new_reach([(Location::new("l1"), 42)], [Location::new("l2")])
1387                & UpwardsClosedSet::new_var_constraint(
1388                    BooleanVarConstraint::ComparisonExpression(
1389                        Box::new(IntegerExpression::Atom(Variable::new("v"))),
1390                        ComparisonOp::Eq,
1391                        Box::new(IntegerExpression::Const(1)),
1392                    )
1393                    .try_into()
1394                    .unwrap(),
1395                );
1396
1397        let config2 =
1398            UpwardsClosedSet::new_reach([(Location::new("l3"), 42)], [Location::new("l4")])
1399                & UpwardsClosedSet::new_var_constraint(
1400                    BooleanVarConstraint::ComparisonExpression(
1401                        Box::new(IntegerExpression::Atom(Variable::new("v"))),
1402                        ComparisonOp::Eq,
1403                        Box::new(IntegerExpression::Const(1)),
1404                    )
1405                    .try_into()
1406                    .unwrap(),
1407                );
1408
1409        let disj = config1 | config2;
1410
1411        let got_expr = disj.encode_to_smt_with_ctx(solver, &ctx).unwrap();
1412
1413        let expected_expr = solver.or_many([
1414            solver.and_many([
1415                solver.gte(
1416                    ctx.get_expr_for(&Location::new("l1")).unwrap(),
1417                    solver.numeral(42),
1418                ),
1419                solver.eq(
1420                    ctx.get_expr_for(&Location::new("l2")).unwrap(),
1421                    solver.numeral(0),
1422                ),
1423                solver.and(
1424                    solver.lte(
1425                        ctx.get_expr_for(&Variable::new("v")).unwrap(),
1426                        solver.numeral(1),
1427                    ),
1428                    solver.gte(
1429                        ctx.get_expr_for(&Variable::new("v")).unwrap(),
1430                        solver.numeral(1),
1431                    ),
1432                ),
1433            ]),
1434            solver.and_many([
1435                solver.gte(
1436                    ctx.get_expr_for(&Location::new("l3")).unwrap(),
1437                    solver.numeral(42),
1438                ),
1439                solver.eq(
1440                    ctx.get_expr_for(&Location::new("l4")).unwrap(),
1441                    solver.numeral(0),
1442                ),
1443                solver.and(
1444                    solver.lte(
1445                        ctx.get_expr_for(&Variable::new("v")).unwrap(),
1446                        solver.numeral(1),
1447                    ),
1448                    solver.gte(
1449                        ctx.get_expr_for(&Variable::new("v")).unwrap(),
1450                        solver.numeral(1),
1451                    ),
1452                ),
1453            ]),
1454        ]);
1455
1456        assert_eq!(
1457            got_expr,
1458            expected_expr,
1459            "got: {}, expected: {}",
1460            solver.display(got_expr),
1461            solver.display(expected_expr)
1462        )
1463    }
1464
1465    #[test]
1466    fn test_or_with_top_and_bot() {
1467        let cover = UpwardsClosedSet::new_cover([Location::new("l1")]);
1468
1469        // `top || x` is `top`
1470        assert_eq!(
1471            UpwardsClosedSet::new_top() | cover.clone(),
1472            UpwardsClosedSet::new_top()
1473        );
1474        assert_eq!(
1475            cover.clone() | UpwardsClosedSet::new_top(),
1476            UpwardsClosedSet::new_top()
1477        );
1478
1479        // `bot || x` is `x`
1480        assert_eq!(UpwardsClosedSet::new_bot() | cover.clone(), cover);
1481        assert_eq!(cover.clone() | UpwardsClosedSet::new_bot(), cover);
1482    }
1483
1484    #[test]
1485    fn test_and_with_top_and_bot() {
1486        let cover = UpwardsClosedSet::new_cover([Location::new("l1")]);
1487
1488        // `bot && x` is `bot`
1489        assert_eq!(
1490            UpwardsClosedSet::new_bot() & cover.clone(),
1491            UpwardsClosedSet::new_bot()
1492        );
1493        assert_eq!(
1494            cover.clone() & UpwardsClosedSet::new_bot(),
1495            UpwardsClosedSet::new_bot()
1496        );
1497
1498        // `top && x` is `x`
1499        assert_eq!(UpwardsClosedSet::new_top() & cover.clone(), cover);
1500        assert_eq!(cover.clone() & UpwardsClosedSet::new_top(), cover);
1501    }
1502
1503    #[test]
1504    fn test_from_integer_expr_rounding() {
1505        let l = Location::new("l");
1506        // `k * l <op> c`
1507        let mk = |k: u32, op: ComparisonOp, c: u32| {
1508            UpwardsClosedSet::from_integer_expr(
1509                IntegerExpression::Const(k) * IntegerExpression::Atom(l.clone()),
1510                op,
1511                IntegerExpression::Const(c),
1512            )
1513        };
1514        let empty = UpwardsClosedSet::new_from_clause(
1515            UpwardsClosedClause::new().with_locs_to_empty([l.clone()]),
1516        );
1517
1518        // 2*l < 1, 2*l <= 1, 2*l < 2, l <= 0  ==>  l == 0
1519        assert_eq!(mk(2, ComparisonOp::Lt, 1), Ok(empty.clone()));
1520        assert_eq!(mk(2, ComparisonOp::Leq, 1), Ok(empty.clone()));
1521        assert_eq!(mk(2, ComparisonOp::Lt, 2), Ok(empty.clone()));
1522        assert_eq!(mk(1, ComparisonOp::Leq, 0), Ok(empty.clone()));
1523
1524        // 2*l < 3 ==> l <= 1, which is not upwards closed
1525        assert!(matches!(
1526            mk(2, ComparisonOp::Lt, 3),
1527            Err(UpwardsClosedSetExtractionError::LocationConstraintNotUpwardsClosed(_))
1528        ));
1529        // 2*l <= 2 ==> l <= 1, which is not upwards closed
1530        assert!(matches!(
1531            mk(2, ComparisonOp::Leq, 2),
1532            Err(UpwardsClosedSetExtractionError::LocationConstraintNotUpwardsClosed(_))
1533        ));
1534
1535        // l < 0 ==> bot
1536        assert_eq!(mk(1, ComparisonOp::Lt, 0), Ok(UpwardsClosedSet::new_bot()));
1537
1538        // 2*l > 3, 2*l >= 3 ==> l >= 2
1539        let geq2 = UpwardsClosedSet::new_cover_int([(l.clone(), 2)]);
1540        assert_eq!(mk(2, ComparisonOp::Gt, 3), Ok(geq2.clone()));
1541        assert_eq!(mk(2, ComparisonOp::Geq, 3), Ok(geq2.clone()));
1542        // l > 1 ==> l >= 2
1543        assert_eq!(mk(1, ComparisonOp::Gt, 1), Ok(geq2));
1544        // l >= 0 ==> top
1545        assert_eq!(mk(1, ComparisonOp::Geq, 0), Ok(UpwardsClosedSet::new_top()));
1546    }
1547}
taco_model_checker/internal_spec/upwards_closed_set.rs

taco_model_checker/internal_spec/
upwards_closed_set.rs
