@@ -496,58 +496,6 @@ abstract_object_pointert intervals_expression_transform(
496
496
497
497
// ///////////////////////////////////////////////////////
498
498
// value_set expression transform
499
- static exprt rewrite_expression (
500
- const exprt &expr,
501
- const std::vector<abstract_object_pointert> &ops);
502
-
503
- // / Recursively construct a combination \p sub_con from \p super_con and once
504
- // / constructed call \p f.
505
- // / \param super_con: vector of some containers storing the values
506
- // / \param sub_con: the one combination being currently constructed
507
- // / \param f: callable with side-effects
508
- void apply_comb (
509
- abstract_object_sett &results,
510
- const std::vector<value_ranget> &super_con,
511
- std::vector<abstract_object_pointert> &sub_con,
512
- const exprt &expr,
513
- const abstract_environmentt &environment,
514
- const namespacet &ns)
515
- {
516
- size_t n = sub_con.size ();
517
- if (n == super_con.size ())
518
- {
519
- auto rewritten_expr = rewrite_expression (expr, sub_con);
520
- auto combination = transform (rewritten_expr, sub_con, environment, ns);
521
- results.insert (combination);
522
- }
523
- else
524
- {
525
- for (const auto &value : super_con[n])
526
- {
527
- sub_con.push_back (value);
528
- apply_comb (results, super_con, sub_con, expr, environment, ns);
529
- sub_con.pop_back ();
530
- }
531
- }
532
- }
533
-
534
- // / Call the function \p f on every combination of elements in \p super_con.
535
- // / Hence the arity of \p f is `super_con.size()`. <{1,2},{1},{1,2,3}> ->
536
- // / f(1,1,1), f(1,1,2), f(1,1,3), f(2,1,1), f(2,1,2), f(2,1,3).
537
- // / \param super_con: vector of some containers storing the values
538
- // / \param f: callable with side-effects
539
- abstract_object_sett evaluate_each_combination (
540
- const std::vector<value_ranget> &super_con,
541
- const exprt &expr,
542
- const abstract_environmentt &environment,
543
- const namespacet &ns)
544
- {
545
- abstract_object_sett results;
546
- std::vector<abstract_object_pointert> sub_con;
547
- apply_comb (results, super_con, sub_con, expr, environment, ns);
548
- return results;
549
- }
550
-
551
499
class value_set_evaluator
552
500
{
553
501
public:
@@ -574,12 +522,57 @@ class value_set_evaluator
574
522
if (expression.id () == ID_if)
575
523
return value_set_evaluate_conditional (collective_operands);
576
524
577
- auto resulting_objects = evaluate_each_combination (
578
- collective_operands, expression, environment, ns);
525
+ auto resulting_objects = evaluate_each_combination (collective_operands);
579
526
580
527
return resolve_new_values (resulting_objects);
581
528
}
582
529
530
+ // / Evaluate expression for every combination of values in \p value_ranges.
531
+ // / <{1,2},{1},{1,2,3}> ->
532
+ // / eval(1,1,1), eval(1,1,2), eval(1,1,3), eval(2,1,1), eval(2,1,2), eval(2,1,3).
533
+ abstract_object_sett
534
+ evaluate_each_combination (const std::vector<value_ranget> &value_ranges) const
535
+ {
536
+ abstract_object_sett results;
537
+ std::vector<abstract_object_pointert> combination;
538
+ evaluate_combination (results, value_ranges, combination);
539
+ return results;
540
+ }
541
+
542
+ void evaluate_combination (
543
+ abstract_object_sett &results,
544
+ const std::vector<value_ranget> &value_ranges,
545
+ std::vector<abstract_object_pointert> &combination) const
546
+ {
547
+ size_t n = combination.size ();
548
+ if (n == value_ranges.size ())
549
+ {
550
+ auto rewritten_expr = rewrite_expression (combination);
551
+ auto result = ::transform (rewritten_expr, combination, environment, ns);
552
+ results.insert (result);
553
+ }
554
+ else
555
+ {
556
+ for (const auto &value : value_ranges[n])
557
+ {
558
+ combination.push_back (value);
559
+ evaluate_combination (results, value_ranges, combination);
560
+ combination.pop_back ();
561
+ }
562
+ }
563
+ }
564
+
565
+ exprt
566
+ rewrite_expression (const std::vector<abstract_object_pointert> &ops) const
567
+ {
568
+ auto operands_expr = exprt::operandst{};
569
+ for (auto v : ops)
570
+ operands_expr.push_back (v->to_constant ());
571
+ auto rewritten_expr =
572
+ exprt (expression.id (), expression.type (), std::move (operands_expr));
573
+ return rewritten_expr;
574
+ }
575
+
583
576
std::vector<value_ranget> unwrap_operands () const
584
577
{
585
578
auto unwrapped = std::vector<value_ranget>{};
@@ -689,14 +682,3 @@ static abstract_object_pointert value_set_expression_transform(
689
682
auto evaluator = value_set_evaluator (expr, operands, environment, ns);
690
683
return evaluator ();
691
684
}
692
-
693
- static exprt rewrite_expression (
694
- const exprt &expr,
695
- const std::vector<abstract_object_pointert> &ops)
696
- {
697
- auto operands_expr = exprt::operandst{};
698
- for (auto v : ops)
699
- operands_expr.push_back (v->to_constant ());
700
- auto rewritten_expr = exprt (expr.id (), expr.type (), std::move (operands_expr));
701
- return rewritten_expr;
702
- }
0 commit comments