Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[P4-Symbolic] Add MergeDisjointTableMatches. #684

Merged
merged 12 commits into from
Nov 7, 2024
Merged

[P4-Symbolic] Add MergeDisjointTableMatches. #684

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
5f6315b
[P4_Symbolic] Add golden test for packet synthesis for conditional.p4…
VSuryaprasad-HCL Oct 28, 2024
85eb99c
[P4_Symbolic] Add golden test for packet synthesis for conditional.p4…
VSuryaprasad-HCL Oct 29, 2024
cdb04af
[P4_Symbolic] Adding conditional_sequence.txt in p4_symbolic/ir/expec…
VSuryaprasad-HCL Oct 29, 2024
6c44915
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins…
VSuryaprasad-HCL Oct 30, 2024
6d65294
[P4_Symbolic] Modified conditional_sequence.smt2
VSuryaprasad-HCL Oct 30, 2024
5d4e5d9
[P4_Symbolic] Adding complex_conditional.p4
VSuryaprasad-HCL Oct 30, 2024
163a872
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins…
VSuryaprasad-HCL Nov 1, 2024
4824730
[P4_Symbolic] Adding complex_conditional.txt
VSuryaprasad-HCL Oct 30, 2024
bfa41b6
[p4_symbolic] Add control flow graph analysis.
kheradmandG Nov 18, 2022
b3ef71d
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins…
VSuryaprasad-HCL Nov 4, 2024
5d24bd4
[p4-symbolic] Add MergeDisjointTableMatches.
kheradmandG Nov 29, 2022
3c6bbfe
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins…
VSuryaprasad-HCL Nov 6, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 5 additions & 18 deletions p4_symbolic/symbolic/conditional.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,13 +66,10 @@ absl::StatusOr<SymbolicTableMatches> EvaluateConditional(
data_plane, get_next_control_for_branch(conditional.else_branch()),
state, translator, else_guard));

// Now we have two traces that need merging.
// We should merge in a way such that the value of a field in the trace is
// the one from the if branch if the condition is true, and the else branch
// otherwise.
ASSIGN_OR_RETURN(
SymbolicTableMatches merged_matches,
util::MergeMatchesOnCondition(condition, if_matches, else_matches));
// Now we have two traces that need merging. The two traces are guaranteed to
// contain different table matches (see go/optimized-symbolic-execution).
ASSIGN_OR_RETURN(SymbolicTableMatches merged_matches,
util::MergeDisjointTableMatches(if_matches, else_matches));

if (!conditional.optimized_symbolic_execution_info()
.continue_to_merge_point()) {
Expand All @@ -90,17 +87,7 @@ absl::StatusOr<SymbolicTableMatches> EvaluateConditional(

// Merge the result of execution from the merge point with the result of
// merged if/else branches.
for (const auto &[table_name, match] : merged_matches) {
auto [_, inserted] = result.insert({table_name, std::move(match)});
if (!inserted) {
return absl::InternalError(
absl::Substitute("Table '$0' is encountered in branches and after "
"the merge point of '$1'",
table_name, conditional.name()));
}
}

return result;
return util::MergeDisjointTableMatches(merged_matches, result);
}
}

Expand Down
47 changes: 21 additions & 26 deletions p4_symbolic/symbolic/expected/basic.smt2
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@
(declare-fun ipv4.dstAddr () (_ BitVec 32))
(declare-fun ipv4.$valid$ () Bool)
(assert
(let (($x124 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x124))))
(let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123))))
(assert
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
Expand Down Expand Up @@ -34,8 +34,7 @@
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
(let (($x60 (and $x42 $x46)))
(let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
(let (($x119 (ite ipv4.$valid$ $x42 false)))
(let ((?x112 (ite $x60 1 ?x102)))
(let (($x61 (not $x46)))
(let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32))))))))
(let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32))))))))
Expand All @@ -47,7 +46,7 @@
(let (($x63 (and (and $x42 $x61) $x50)))
(let ((?x113 (ite $x60 (_ bv1 9) (ite $x63 (_ bv0 9) (ite $x67 (_ bv1 9) (ite $x71 (_ bv1 9) ?x77))))))
(let (($x41 (= ?x113 (_ bv511 9))))
(and (and (not $x41) $x119) (= ?x120 (- 1))))))))))))))))))))))))
(and (and (not $x41) $x42) (= ?x112 (- 1)))))))))))))))))))))))
(check-sat)

;
Expand All @@ -57,8 +56,8 @@
(declare-fun ipv4.dstAddr () (_ BitVec 32))
(declare-fun ipv4.$valid$ () Bool)
(assert
(let (($x124 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x124))))
(let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123))))
(assert
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
Expand Down Expand Up @@ -86,8 +85,7 @@
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
(let (($x60 (and $x42 $x46)))
(let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
(let (($x119 (ite ipv4.$valid$ $x42 false)))
(let ((?x112 (ite $x60 1 ?x102)))
(let (($x61 (not $x46)))
(let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32))))))))
(let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32))))))))
Expand All @@ -99,8 +97,8 @@
(let (($x63 (and (and $x42 $x61) $x50)))
(let ((?x113 (ite $x60 (_ bv1 9) (ite $x63 (_ bv0 9) (ite $x67 (_ bv1 9) (ite $x71 (_ bv1 9) ?x77))))))
(let (($x41 (= ?x113 (_ bv511 9))))
(let (($x244 (and (not $x41) $x119)))
(and $x244 (= ?x120 0))))))))))))))))))))))))
(let (($x243 (and (not $x41) $x42)))
(and $x243 (= ?x112 0)))))))))))))))))))))))
(check-sat)

;
Expand All @@ -110,8 +108,8 @@
(declare-fun ipv4.dstAddr () (_ BitVec 32))
(declare-fun ipv4.$valid$ () Bool)
(assert
(let (($x124 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x124))))
(let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123))))
(assert
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
Expand Down Expand Up @@ -139,8 +137,7 @@
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
(let (($x60 (and $x42 $x46)))
(let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
(let (($x119 (ite ipv4.$valid$ $x42 false)))
(let ((?x112 (ite $x60 1 ?x102)))
(let (($x61 (not $x46)))
(let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32))))))))
(let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32))))))))
Expand All @@ -152,7 +149,7 @@
(let (($x63 (and (and $x42 $x61) $x50)))
(let ((?x113 (ite $x60 (_ bv1 9) (ite $x63 (_ bv0 9) (ite $x67 (_ bv1 9) (ite $x71 (_ bv1 9) ?x77))))))
(let (($x41 (= ?x113 (_ bv511 9))))
(and (and (not $x41) $x119) (= ?x120 1)))))))))))))))))))))))
(and (and (not $x41) $x42) (= ?x112 1))))))))))))))))))))))
(check-sat)

;
Expand All @@ -162,8 +159,8 @@
(declare-fun ipv4.dstAddr () (_ BitVec 32))
(declare-fun ipv4.$valid$ () Bool)
(assert
(let (($x124 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x124))))
(let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123))))
(assert
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
Expand Down Expand Up @@ -191,8 +188,7 @@
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
(let (($x60 (and $x42 $x46)))
(let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
(let (($x119 (ite ipv4.$valid$ $x42 false)))
(let ((?x112 (ite $x60 1 ?x102)))
(let (($x61 (not $x46)))
(let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32))))))))
(let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32))))))))
Expand All @@ -204,7 +200,7 @@
(let (($x63 (and (and $x42 $x61) $x50)))
(let ((?x113 (ite $x60 (_ bv1 9) (ite $x63 (_ bv0 9) (ite $x67 (_ bv1 9) (ite $x71 (_ bv1 9) ?x77))))))
(let (($x41 (= ?x113 (_ bv511 9))))
(and (and (not $x41) $x119) (= ?x120 2)))))))))))))))))))))))
(and (and (not $x41) $x42) (= ?x112 2))))))))))))))))))))))
(check-sat)

;
Expand All @@ -214,8 +210,8 @@
(declare-fun ipv4.dstAddr () (_ BitVec 32))
(declare-fun ipv4.$valid$ () Bool)
(assert
(let (($x124 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x124))))
(let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123))))
(assert
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
Expand Down Expand Up @@ -243,8 +239,7 @@
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
(let (($x60 (and $x42 $x46)))
(let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
(let (($x119 (ite ipv4.$valid$ $x42 false)))
(let ((?x112 (ite $x60 1 ?x102)))
(let (($x61 (not $x46)))
(let (($x65 (and $x61 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv168427520 32))))))))
(let (($x69 (and $x65 (not (and true (= ((_ extract 31 16) ipv4.dstAddr) ((_ extract 31 16) (_ bv336855040 32))))))))
Expand All @@ -256,6 +251,6 @@
(let (($x63 (and (and $x42 $x61) $x50)))
(let ((?x113 (ite $x60 (_ bv1 9) (ite $x63 (_ bv0 9) (ite $x67 (_ bv1 9) (ite $x71 (_ bv1 9) ?x77))))))
(let (($x41 (= ?x113 (_ bv511 9))))
(and (and (not $x41) $x119) (= ?x120 3)))))))))))))))))))))))
(and (and (not $x41) $x42) (= ?x112 3))))))))))))))))))))))
(check-sat)

138 changes: 68 additions & 70 deletions p4_symbolic/symbolic/expected/conditional.smt2
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,31 +4,30 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61))))
(let (($x59 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x40 (= ethernet.dst_addr (_ bv1 48))))
(let (($x41 (and true $x40)))
(let (($x42 (and true $x41)))
(let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
(let (($x52 (= ?x50 (_ bv511 9))))
(or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))))))))))))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x39 (ite $x31 $x33 false)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(and (and (not $x54) $x39) (= (- 1) (- 1))))))))))))))
(let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x40 (= ethernet.dst_addr (_ bv1 48))))
(let (($x41 (and true $x40)))
(let (($x42 (and true $x41)))
(let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
(let (($x52 (= ?x50 (_ bv511 9))))
(and (and (not $x52) $x33) (= (- 1) (- 1)))))))))))))
(check-sat)

;
Expand All @@ -37,31 +36,30 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61))))
(let (($x59 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x40 (= ethernet.dst_addr (_ bv1 48))))
(let (($x41 (and true $x40)))
(let (($x42 (and true $x41)))
(let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
(let (($x52 (= ?x50 (_ bv511 9))))
(or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))))))))))))))
(assert
(let (($x34 (and true (not (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))))
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x40 (ite $x31 false $x34)))
(let ((?x38 (ite $x34 (_ bv511 9) (ite (and true $x31) (_ bv511 9) standard_metadata.egress_spec))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) ?x38)))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(and (and (not $x54) $x40) (= (- 1) (- 1))))))))))))))
(let (($x33 (and true $x31)))
(let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x40 (= ethernet.dst_addr (_ bv1 48))))
(let (($x41 (and true $x40)))
(let (($x42 (and true $x41)))
(let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
(let (($x52 (= ?x50 (_ bv511 9))))
(and (and (not $x52) $x34) (= (- 1) (- 1)))))))))))))
(check-sat)

;
Expand All @@ -70,31 +68,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61))))
(let (($x59 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x40 (= ethernet.dst_addr (_ bv1 48))))
(let (($x41 (and true $x40)))
(let (($x42 (and true $x41)))
(let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
(let (($x52 (= ?x50 (_ bv511 9))))
(or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))))))))))))))
(assert
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x49 (ite $x44 0 (- 1))))
(let (($x40 (= ethernet.dst_addr (_ bv1 48))))
(let (($x41 (and true $x40)))
(let (($x42 (and true $x41)))
(let ((?x47 (ite $x42 0 (- 1))))
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not $x43)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(and (and (not $x54) true) (= ?x49 (- 1))))))))))))))
(let ((?x45 (ite (and true (not $x41)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
(let (($x52 (= ?x50 (_ bv511 9))))
(and (and (not $x52) true) (= ?x47 (- 1))))))))))))))
(check-sat)

;
Expand All @@ -103,31 +101,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61))))
(let (($x59 (= standard_metadata.ingress_port (_ bv1 9))))
(and (and (distinct standard_metadata.ingress_port (_ bv511 9)) true) (or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59))))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(or $x54 (or (or false (= ?x52 (_ bv0 9))) (= ?x52 (_ bv1 9))))))))))))))
(let ((?x45 (ite (and true (not (and true (= ethernet.dst_addr (_ bv1 48))))) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let (($x40 (= ethernet.dst_addr (_ bv1 48))))
(let (($x41 (and true $x40)))
(let (($x42 (and true $x41)))
(let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
(let (($x52 (= ?x50 (_ bv511 9))))
(or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))))))))))))))
(assert
(let (($x42 (= ethernet.dst_addr (_ bv1 48))))
(let (($x43 (and true $x42)))
(let (($x44 (and true $x43)))
(let ((?x49 (ite $x44 0 (- 1))))
(let (($x40 (= ethernet.dst_addr (_ bv1 48))))
(let (($x41 (and true $x40)))
(let (($x42 (and true $x41)))
(let ((?x47 (ite $x42 0 (- 1))))
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $x31))))
(let ((?x47 (ite (and true (not $x43)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x52 (ite $x44 (_ bv1 9) ?x47)))
(let (($x54 (= ?x52 (_ bv511 9))))
(let (($x159 (and (not $x54) true)))
(and $x159 (= ?x49 0))))))))))))))
(let ((?x45 (ite (and true (not $x41)) (_ bv511 9) (ite $x34 (_ bv511 9) (ite $x33 (_ bv511 9) standard_metadata.egress_spec)))))
(let ((?x50 (ite $x42 (_ bv1 9) ?x45)))
(let (($x52 (= ?x50 (_ bv511 9))))
(let (($x157 (and (not $x52) true)))
(and $x157 (= ?x47 0))))))))))))))
(check-sat)

Loading
Loading