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

[P4_Symbolic] Remove disjointness check on set of tables that get evaluate in each branch of a conditional. #769

Merged
merged 7 commits into from
Nov 27, 2024
Merged

[P4_Symbolic] Remove disjointness check on set of tables that get evaluate in each branch of a conditional. #769

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
e83312e
Extend BMv2 proto with error codes.
kishanps Jun 2, 2023
0b6c934
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins…
VSuryaprasad-HCL Nov 26, 2024
e281ac4
[P4_Symbolic] Adding p4_symbolic/symbolic/expected/conditional_nonlat…
VSuryaprasad-HCL Nov 25, 2024
78d0ac3
Merge branch 'main' of https://github.com/VSuryaprasad-HCL/sonic-pins…
VSuryaprasad-HCL Nov 26, 2024
788fcdd
[P4_Symbolic] Adding p4_symbolic/testdata/conditional/conditional_non…
VSuryaprasad-HCL Nov 25, 2024
b6b0d62
[P4-Symbolic] Remove disjointness check on set of tables that get eva…
kheradmandG Jun 6, 2023
3d2d02c
Merge branch 'main' into symbolic_import_branch_115
kishanps Nov 27, 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
8 changes: 4 additions & 4 deletions p4_symbolic/symbolic/conditional.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,10 +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. 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));
// Now we have two traces that need merging.
ASSIGN_OR_RETURN(
SymbolicTableMatches merged_matches,
util::MergeMatchesOnCondition(condition, if_matches, else_matches));

if (!conditional.optimized_symbolic_execution_info()
.continue_to_merge_point()) {
Expand Down
47 changes: 26 additions & 21 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 (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123)))
(let (($x125 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125)))
(assert
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
Expand Down Expand Up @@ -34,7 +34,8 @@
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
(let (($x60 (and $x42 $x46)))
(let ((?x112 (ite $x60 1 ?x102)))
(let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
(let (($x119 (ite ipv4.$valid$ $x42 false)))
(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 @@ -46,7 +47,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) $x42) (= ?x112 (- 1)))))))))))))))))))))))
(and (and (not $x41) $x119) (= ?x120 (- 1))))))))))))))))))))))))
(check-sat)

;
Expand All @@ -56,8 +57,8 @@
(declare-fun ipv4.dstAddr () (_ BitVec 32))
(declare-fun ipv4.$valid$ () Bool)
(assert
(let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123)))
(let (($x125 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125)))
(assert
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
Expand Down Expand Up @@ -85,7 +86,8 @@
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
(let (($x60 (and $x42 $x46)))
(let ((?x112 (ite $x60 1 ?x102)))
(let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
(let (($x119 (ite ipv4.$valid$ $x42 false)))
(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 @@ -97,8 +99,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) $x42)))
(and $x244 (= ?x112 0)))))))))))))))))))))))
(let (($x246 (and (not $x41) $x119)))
(and $x246 (= ?x120 0))))))))))))))))))))))))
(check-sat)

;
Expand All @@ -108,8 +110,8 @@
(declare-fun ipv4.dstAddr () (_ BitVec 32))
(declare-fun ipv4.$valid$ () Bool)
(assert
(let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123)))
(let (($x125 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125)))
(assert
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
Expand Down Expand Up @@ -137,7 +139,8 @@
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
(let (($x60 (and $x42 $x46)))
(let ((?x112 (ite $x60 1 ?x102)))
(let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
(let (($x119 (ite ipv4.$valid$ $x42 false)))
(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 @@ -149,7 +152,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) $x42) (= ?x112 1))))))))))))))))))))))
(and (and (not $x41) $x119) (= ?x120 1)))))))))))))))))))))))
(check-sat)

;
Expand All @@ -159,8 +162,8 @@
(declare-fun ipv4.dstAddr () (_ BitVec 32))
(declare-fun ipv4.$valid$ () Bool)
(assert
(let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123)))
(let (($x125 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125)))
(assert
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
Expand Down Expand Up @@ -188,7 +191,8 @@
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
(let (($x60 (and $x42 $x46)))
(let ((?x112 (ite $x60 1 ?x102)))
(let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
(let (($x119 (ite ipv4.$valid$ $x42 false)))
(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 @@ -200,7 +204,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) $x42) (= ?x112 2))))))))))))))))))))))
(and (and (not $x41) $x119) (= ?x120 2)))))))))))))))))))))))
(check-sat)

;
Expand All @@ -210,8 +214,8 @@
(declare-fun ipv4.dstAddr () (_ BitVec 32))
(declare-fun ipv4.$valid$ () Bool)
(assert
(let (($x123 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x123)))
(let (($x125 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x125)))
(assert
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
Expand Down Expand Up @@ -239,7 +243,8 @@
(let (($x45 (= ipv4.dstAddr (_ bv168427520 32))))
(let (($x46 (and true $x45)))
(let (($x60 (and $x42 $x46)))
(let ((?x112 (ite $x60 1 ?x102)))
(let ((?x120 (ite ipv4.$valid$ (ite $x60 1 ?x102) (- 1))))
(let (($x119 (ite ipv4.$valid$ $x42 false)))
(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 @@ -251,6 +256,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) $x42) (= ?x112 3))))))))))))))))))))))
(and (and (not $x41) $x119) (= ?x120 3)))))))))))))))))))))))
(check-sat)

138 changes: 70 additions & 68 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,30 +4,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x59 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59)))
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $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))))
(or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))))))))))))))
(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))))))))))))))
(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 ((?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)))))))))))))
(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))))))))))))))
(check-sat)

;
Expand All @@ -36,30 +37,31 @@
(declare-fun standard_metadata.egress_spec () (_ BitVec 9))
(declare-fun ethernet.dst_addr () (_ BitVec 48))
(assert
(let (($x59 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x59)))
(let (($x61 (= standard_metadata.ingress_port (_ bv1 9))))
(or (or false (= standard_metadata.ingress_port (_ bv0 9))) $x61)))
(assert
(let (($x31 (= standard_metadata.ingress_port (concat (_ bv0 8) (_ bv0 1)))))
(let (($x33 (and true $x31)))
(let (($x34 (and true (not $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))))
(or $x52 (or (or false (= ?x50 (_ bv0 9))) (= ?x50 (_ bv1 9))))))))))))))
(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))))))))))))))
(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 (($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)))))))))))))
(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))))))))))))))
(check-sat)

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

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

Loading
Loading