From: Clark Barrett Date: Mon, 3 Dec 2012 04:35:27 +0000 (+0000) Subject: Fix for fuzzer-found model bug X-Git-Tag: cvc5-1.0.0~7485 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25c6e1331d338c6ba8d60224711343986e11cf79;p=cvc5.git Fix for fuzzer-found model bug --- diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 826e729fc..3880aaad9 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -210,7 +210,7 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ } /** add term */ -void TheoryModel::addTerm( Node n ){ +void TheoryModel::addTerm(TNode n ){ Assert(d_equalityEngine.hasTerm(n)); //must collect UF terms if (n.getKind()==APPLY_UF) { @@ -223,7 +223,7 @@ void TheoryModel::addTerm( Node n ){ } /** assert equality */ -void TheoryModel::assertEquality( Node a, Node b, bool polarity ){ +void TheoryModel::assertEquality(TNode a, TNode b, bool polarity ){ if (a == b && polarity) { return; } @@ -233,7 +233,7 @@ void TheoryModel::assertEquality( Node a, Node b, bool polarity ){ } /** assert predicate */ -void TheoryModel::assertPredicate( Node a, bool polarity ){ +void TheoryModel::assertPredicate(TNode a, bool polarity ){ if ((a == d_true && polarity) || (a == d_false && (!polarity))) { return; @@ -263,6 +263,8 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set* predFalse = ee->areEqual(eqc, d_false); } eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee); + bool first = true; + Node rep; for (; !eqc_i.isFinished(); ++eqc_i) { if (termSet != NULL && termSet->find(*eqc_i) == termSet->end()) { continue; @@ -274,28 +276,43 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set* else if (predFalse) { assertPredicate(*eqc_i, false); } - else if (eqc != (*eqc_i)) { - Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << eqc << "));" << endl; - d_equalityEngine.mergePredicates(*eqc_i, eqc, Node::null()); - Assert(d_equalityEngine.consistent()); + else { + if (first) { + rep = (*eqc_i); + first = false; + } + else { + Trace("model-builder-assertions") << "(assert (= " << *eqc_i << " " << rep << "));" << endl; + d_equalityEngine.mergePredicates(*eqc_i, rep, Node::null()); + Assert(d_equalityEngine.consistent()); + } } } else { - assertEquality(*eqc_i, eqc, true); + if (first) { + rep = (*eqc_i); + first = false; + } + else { + assertEquality(*eqc_i, rep, true); + } } } } } -void TheoryModel::assertRepresentative( Node n ){ +void TheoryModel::assertRepresentative(TNode n ) +{ Trace("model-builder-reps") << "Assert rep : " << n << std::endl; d_reps[ n ] = n; } -bool TheoryModel::hasTerm( Node a ){ +bool TheoryModel::hasTerm(TNode a) +{ return d_equalityEngine.hasTerm( a ); } -Node TheoryModel::getRepresentative( Node a ){ +Node TheoryModel::getRepresentative(TNode a) +{ if( d_equalityEngine.hasTerm( a ) ){ Node r = d_equalityEngine.getRepresentative( a ); if( d_reps.find( r )!=d_reps.end() ){ @@ -308,7 +325,8 @@ Node TheoryModel::getRepresentative( Node a ){ } } -bool TheoryModel::areEqual( Node a, Node b ){ +bool TheoryModel::areEqual(TNode a, TNode b) +{ if( a==b ){ return true; }else if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ @@ -318,7 +336,8 @@ bool TheoryModel::areEqual( Node a, Node b ){ } } -bool TheoryModel::areDisequal( Node a, Node b ){ +bool TheoryModel::areDisequal(TNode a, TNode b) +{ if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){ return d_equalityEngine.areDisequal( a, b, false ); }else{ diff --git a/src/theory/model.h b/src/theory/model.h index 7ccbe2fc3..e283ee183 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -90,11 +90,11 @@ public: * such as contraining the interpretation of uninterpretted functions, * and adding n to the equality engine of this model */ - virtual void addTerm( Node n ); + virtual void addTerm(TNode n); /** assert equality holds in the model */ - void assertEquality( Node a, Node b, bool polarity ); + void assertEquality(TNode a, TNode b, bool polarity); /** assert predicate holds in the model */ - void assertPredicate( Node a, bool polarity ); + void assertPredicate(TNode a, bool polarity); /** assert all equalities/predicates in equality engine hold in the model */ void assertEqualityEngine(const eq::EqualityEngine* ee, std::set* termSet = NULL); /** assert representative @@ -103,13 +103,13 @@ public: * case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... ) * functions where fullModel = true. */ - void assertRepresentative( Node n ); + void assertRepresentative(TNode n); public: /** general queries */ - bool hasTerm( Node a ); - Node getRepresentative( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); + bool hasTerm(TNode a); + Node getRepresentative(TNode a); + bool areEqual(TNode a, TNode b); + bool areDisequal(TNode a, TNode b); public: /** get value function for Exprs. */ Expr getValue( Expr expr ) const; diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index cc4a1556f..8ed9096c4 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -20,6 +20,7 @@ TESTS = \ fuzz03.smt \ fuzz04.smt \ fuzz05.smt \ + fuzz06.smt \ a17.smt \ error72.delta2.smt \ x2.smt diff --git a/test/regress/regress0/auflia/fuzz06.smt b/test/regress/regress0/auflia/fuzz06.smt new file mode 100644 index 000000000..88c2a9d5c --- /dev/null +++ b/test/regress/regress0/auflia/fuzz06.smt @@ -0,0 +1,349 @@ +(benchmark fuzzsmt +:logic QF_AUFLIA +:status sat +:extrafuns ((f0 Int Int)) +:extrafuns ((f1 Array Array Array)) +:extrapreds ((p0 Int)) +:extrapreds ((p1 Array Array Array)) +:extrafuns ((v0 Int)) +:extrafuns ((v1 Array)) +:formula +(let (?e2 0) +(let (?e3 (ite (p0 v0) 1 0)) +(let (?e4 (ite (p0 v0) 1 0)) +(let (?e5 (~ ?e4)) +(let (?e6 (ite (p0 ?e3) 1 0)) +(let (?e7 (f0 ?e3)) +(let (?e8 (* ?e4 (~ ?e2))) +(let (?e9 (store v1 ?e5 ?e8)) +(let (?e10 (select ?e9 ?e4)) +(let (?e11 (store ?e9 ?e8 ?e7)) +(let (?e12 (select ?e11 ?e10)) +(let (?e13 (f1 ?e11 ?e11)) +(let (?e14 (f1 v1 ?e13)) +(let (?e15 (f1 ?e9 ?e13)) +(flet ($e16 (p1 ?e14 ?e11 ?e15)) +(flet ($e17 (p1 ?e13 ?e15 v1)) +(flet ($e18 (p1 ?e9 ?e9 ?e14)) +(flet ($e19 (p0 ?e7)) +(flet ($e20 (<= v0 ?e4)) +(flet ($e21 (> ?e7 ?e12)) +(flet ($e22 (= ?e7 ?e12)) +(flet ($e23 (distinct ?e6 ?e5)) +(flet ($e24 (p0 ?e7)) +(flet ($e25 (>= ?e3 ?e8)) +(flet ($e26 (< ?e3 ?e7)) +(flet ($e27 (<= ?e7 v0)) +(flet ($e28 (p0 ?e10)) +(let (?e29 (ite $e27 ?e15 ?e13)) +(let (?e30 (ite $e28 ?e14 ?e14)) +(let (?e31 (ite $e26 ?e9 v1)) +(let (?e32 (ite $e17 ?e11 ?e13)) +(let (?e33 (ite $e23 ?e13 ?e13)) +(let (?e34 (ite $e25 ?e14 ?e30)) +(let (?e35 (ite $e22 ?e30 ?e30)) +(let (?e36 (ite $e25 ?e11 ?e31)) +(let (?e37 (ite $e22 ?e14 ?e35)) +(let (?e38 (ite $e19 ?e36 ?e35)) +(let (?e39 (ite $e21 ?e36 ?e9)) +(let (?e40 (ite $e16 ?e39 ?e11)) +(let (?e41 (ite $e28 ?e29 v1)) +(let (?e42 (ite $e25 ?e33 ?e36)) +(let (?e43 (ite $e21 ?e29 ?e9)) +(let (?e44 (ite $e18 ?e30 ?e13)) +(let (?e45 (ite $e18 ?e11 ?e41)) +(let (?e46 (ite $e20 ?e15 ?e34)) +(let (?e47 (ite $e24 ?e40 ?e13)) +(let (?e48 (ite $e26 ?e7 ?e6)) +(let (?e49 (ite $e21 ?e10 ?e6)) +(let (?e50 (ite $e22 v0 ?e8)) +(let (?e51 (ite $e19 ?e5 ?e4)) +(let (?e52 (ite $e16 ?e12 ?e10)) +(let (?e53 (ite $e16 ?e49 ?e8)) +(let (?e54 (ite $e21 ?e3 v0)) +(let (?e55 (ite $e24 ?e51 ?e52)) +(let (?e56 (ite $e23 ?e10 ?e5)) +(let (?e57 (ite $e18 ?e50 ?e49)) +(let (?e58 (ite $e17 ?e10 ?e4)) +(let (?e59 (ite $e27 ?e57 ?e12)) +(let (?e60 (ite $e21 ?e10 ?e3)) +(let (?e61 (ite $e28 ?e7 ?e55)) +(let (?e62 (ite $e20 ?e53 ?e53)) +(let (?e63 (ite $e25 ?e48 ?e8)) +(let (?e64 (store ?e45 ?e49 ?e8)) +(let (?e65 (store ?e43 ?e55 ?e57)) +(let (?e66 (select ?e34 v0)) +(let (?e67 (store ?e9 ?e66 ?e54)) +(let (?e68 (select ?e64 ?e56)) +(let (?e69 (f1 ?e11 ?e30)) +(let (?e70 (f1 ?e34 ?e36)) +(let (?e71 (f1 ?e38 ?e39)) +(let (?e72 (f1 ?e31 ?e45)) +(let (?e73 (f1 ?e43 ?e43)) +(let (?e74 (f1 ?e37 ?e65)) +(let (?e75 (f1 ?e9 ?e38)) +(let (?e76 (f1 ?e37 ?e14)) +(let (?e77 (f1 ?e13 ?e39)) +(let (?e78 (f1 ?e34 ?e39)) +(let (?e79 (f1 ?e64 ?e64)) +(let (?e80 (f1 ?e15 ?e15)) +(let (?e81 (f1 v1 v1)) +(let (?e82 (f1 ?e47 ?e71)) +(let (?e83 (f1 ?e77 ?e13)) +(let (?e84 (f1 ?e32 ?e32)) +(let (?e85 (f1 ?e46 ?e46)) +(let (?e86 (f1 ?e36 ?e72)) +(let (?e87 (f1 ?e81 ?e65)) +(let (?e88 (f1 ?e29 ?e45)) +(let (?e89 (f1 ?e44 ?e31)) +(let (?e90 (f1 ?e41 ?e41)) +(let (?e91 (f1 ?e34 ?e42)) +(let (?e92 (f1 ?e35 ?e35)) +(let (?e93 (f1 ?e33 ?e33)) +(let (?e94 (f1 ?e11 ?e14)) +(let (?e95 (f1 ?e67 ?e34)) +(let (?e96 (f1 ?e86 ?e37)) +(let (?e97 (f1 ?e40 ?e40)) +(let (?e98 (- ?e56 ?e5)) +(let (?e99 (+ ?e52 ?e57)) +(let (?e100 (ite (p0 ?e51) 1 0)) +(let (?e101 (ite (p0 ?e12) 1 0)) +(let (?e102 (ite (p0 ?e58) 1 0)) +(let (?e103 (+ v0 ?e10)) +(let (?e104 (~ ?e48)) +(let (?e105 (* ?e2 ?e12)) +(let (?e106 (- ?e3 ?e101)) +(let (?e107 (- ?e59 ?e100)) +(let (?e108 (ite (p0 ?e10) 1 0)) +(let (?e109 (* ?e2 ?e102)) +(let (?e110 (ite (p0 ?e7) 1 0)) +(let (?e111 (* ?e53 (~ ?e2))) +(let (?e112 (* ?e2 ?e4)) +(let (?e113 (~ ?e106)) +(let (?e114 (~ ?e57)) +(let (?e115 (* ?e68 (~ ?e2))) +(let (?e116 (- ?e4 ?e50)) +(let (?e117 (* ?e2 ?e49)) +(let (?e118 (ite (p0 ?e61) 1 0)) +(let (?e119 (ite (p0 ?e62) 1 0)) +(let (?e120 (* ?e10 ?e2)) +(let (?e121 (ite (p0 ?e119) 1 0)) +(let (?e122 (f0 ?e55)) +(let (?e123 (* (~ ?e2) ?e66)) +(let (?e124 (* ?e2 ?e63)) +(let (?e125 (ite (p0 ?e106) 1 0)) +(let (?e126 (f0 ?e102)) +(let (?e127 (f0 ?e55)) +(let (?e128 (f0 ?e103)) +(let (?e129 (~ ?e8)) +(let (?e130 (- ?e126 ?e6)) +(let (?e131 (* (~ ?e2) ?e60)) +(let (?e132 (* (~ ?e2) ?e54)) +(flet ($e133 (p1 ?e15 ?e73 ?e14)) +(flet ($e134 (p1 ?e47 ?e78 ?e81)) +(flet ($e135 (p1 ?e44 ?e80 ?e37)) +(flet ($e136 (p1 ?e42 ?e73 ?e91)) +(flet ($e137 (p1 ?e43 ?e37 ?e14)) +(flet ($e138 (p1 ?e73 ?e87 ?e34)) +(flet ($e139 (p1 ?e75 ?e46 ?e75)) +(flet ($e140 (p1 ?e96 ?e96 ?e88)) +(flet ($e141 (p1 ?e89 ?e78 ?e87)) +(flet ($e142 (p1 ?e70 ?e95 ?e47)) +(flet ($e143 (p1 ?e39 ?e96 ?e74)) +(flet ($e144 (p1 ?e91 ?e72 ?e70)) +(flet ($e145 (p1 v1 ?e65 ?e44)) +(flet ($e146 (p1 ?e90 ?e70 ?e79)) +(flet ($e147 (p1 ?e94 ?e91 ?e13)) +(flet ($e148 (p1 ?e41 ?e93 ?e32)) +(flet ($e149 (p1 ?e40 ?e91 ?e93)) +(flet ($e150 (p1 ?e92 ?e34 ?e80)) +(flet ($e151 (p1 ?e71 ?e44 ?e78)) +(flet ($e152 (p1 ?e43 ?e34 ?e73)) +(flet ($e153 (p1 ?e81 ?e73 ?e70)) +(flet ($e154 (p1 ?e86 ?e86 ?e38)) +(flet ($e155 (p1 ?e45 v1 ?e36)) +(flet ($e156 (p1 ?e43 ?e30 ?e37)) +(flet ($e157 (p1 ?e84 ?e78 ?e45)) +(flet ($e158 (p1 ?e67 ?e38 ?e90)) +(flet ($e159 (p1 ?e31 ?e81 ?e13)) +(flet ($e160 (p1 ?e64 ?e47 ?e94)) +(flet ($e161 (p1 ?e29 ?e75 ?e76)) +(flet ($e162 (p1 ?e85 ?e96 ?e82)) +(flet ($e163 (p1 ?e33 ?e29 ?e38)) +(flet ($e164 (p1 ?e31 ?e78 ?e69)) +(flet ($e165 (p1 ?e97 ?e9 ?e35)) +(flet ($e166 (p1 ?e83 ?e71 ?e79)) +(flet ($e167 (p1 ?e11 ?e67 ?e31)) +(flet ($e168 (p1 ?e39 ?e93 ?e96)) +(flet ($e169 (p1 ?e65 ?e85 ?e44)) +(flet ($e170 (p1 ?e76 ?e40 ?e15)) +(flet ($e171 (p1 ?e77 ?e34 ?e14)) +(flet ($e172 (distinct ?e129 ?e62)) +(flet ($e173 (p0 ?e116)) +(flet ($e174 (> ?e120 ?e10)) +(flet ($e175 (p0 ?e102)) +(flet ($e176 (> ?e50 ?e53)) +(flet ($e177 (> ?e119 ?e127)) +(flet ($e178 (distinct ?e117 ?e55)) +(flet ($e179 (= ?e122 ?e102)) +(flet ($e180 (< ?e123 ?e52)) +(flet ($e181 (> ?e66 ?e51)) +(flet ($e182 (= ?e121 ?e4)) +(flet ($e183 (distinct ?e130 ?e102)) +(flet ($e184 (< ?e111 ?e4)) +(flet ($e185 (p0 ?e68)) +(flet ($e186 (distinct ?e3 ?e3)) +(flet ($e187 (>= ?e66 ?e59)) +(flet ($e188 (< ?e10 ?e48)) +(flet ($e189 (distinct ?e5 ?e52)) +(flet ($e190 (= ?e101 ?e54)) +(flet ($e191 (>= ?e8 ?e116)) +(flet ($e192 (<= ?e62 ?e12)) +(flet ($e193 (< ?e131 ?e114)) +(flet ($e194 (>= ?e49 ?e125)) +(flet ($e195 (> ?e100 ?e7)) +(flet ($e196 (p0 ?e101)) +(flet ($e197 (distinct ?e118 ?e52)) +(flet ($e198 (<= v0 ?e60)) +(flet ($e199 (p0 ?e128)) +(flet ($e200 (>= ?e6 ?e106)) +(flet ($e201 (= ?e50 ?e61)) +(flet ($e202 (> ?e115 ?e132)) +(flet ($e203 (distinct ?e57 ?e102)) +(flet ($e204 (>= ?e102 ?e55)) +(flet ($e205 (p0 ?e55)) +(flet ($e206 (<= ?e113 ?e132)) +(flet ($e207 (<= ?e124 ?e106)) +(flet ($e208 (> ?e68 ?e117)) +(flet ($e209 (p0 ?e56)) +(flet ($e210 (<= ?e63 ?e112)) +(flet ($e211 (<= ?e119 ?e5)) +(flet ($e212 (= ?e105 ?e51)) +(flet ($e213 (< ?e6 ?e118)) +(flet ($e214 (p0 ?e66)) +(flet ($e215 (>= ?e58 ?e101)) +(flet ($e216 (distinct ?e109 ?e57)) +(flet ($e217 (distinct ?e99 ?e103)) +(flet ($e218 (<= ?e126 ?e58)) +(flet ($e219 (>= ?e107 ?e120)) +(flet ($e220 (< ?e125 ?e124)) +(flet ($e221 (> ?e98 ?e105)) +(flet ($e222 (p0 ?e118)) +(flet ($e223 (= ?e108 ?e4)) +(flet ($e224 (= ?e58 ?e114)) +(flet ($e225 (< ?e110 ?e123)) +(flet ($e226 (distinct ?e104 ?e111)) +(flet ($e227 (iff $e179 $e21)) +(flet ($e228 (if_then_else $e185 $e171 $e141)) +(flet ($e229 (and $e152 $e216)) +(flet ($e230 (and $e133 $e165)) +(flet ($e231 (and $e155 $e217)) +(flet ($e232 (iff $e16 $e180)) +(flet ($e233 (if_then_else $e168 $e191 $e153)) +(flet ($e234 (implies $e159 $e147)) +(flet ($e235 (not $e203)) +(flet ($e236 (xor $e28 $e223)) +(flet ($e237 (and $e174 $e172)) +(flet ($e238 (or $e194 $e197)) +(flet ($e239 (iff $e149 $e201)) +(flet ($e240 (not $e181)) +(flet ($e241 (or $e238 $e157)) +(flet ($e242 (and $e190 $e225)) +(flet ($e243 (implies $e140 $e215)) +(flet ($e244 (xor $e176 $e20)) +(flet ($e245 (not $e241)) +(flet ($e246 (iff $e243 $e158)) +(flet ($e247 (iff $e18 $e169)) +(flet ($e248 (xor $e173 $e210)) +(flet ($e249 (if_then_else $e212 $e143 $e218)) +(flet ($e250 (not $e177)) +(flet ($e251 (or $e207 $e163)) +(flet ($e252 (implies $e214 $e156)) +(flet ($e253 (or $e170 $e166)) +(flet ($e254 (iff $e206 $e209)) +(flet ($e255 (and $e231 $e189)) +(flet ($e256 (or $e148 $e167)) +(flet ($e257 (if_then_else $e237 $e248 $e235)) +(flet ($e258 (or $e138 $e142)) +(flet ($e259 (or $e249 $e164)) +(flet ($e260 (and $e208 $e204)) +(flet ($e261 (xor $e260 $e202)) +(flet ($e262 (xor $e193 $e136)) +(flet ($e263 (if_then_else $e184 $e219 $e227)) +(flet ($e264 (not $e145)) +(flet ($e265 (or $e256 $e187)) +(flet ($e266 (implies $e160 $e205)) +(flet ($e267 (iff $e178 $e134)) +(flet ($e268 (or $e220 $e27)) +(flet ($e269 (and $e265 $e25)) +(flet ($e270 (not $e242)) +(flet ($e271 (or $e270 $e255)) +(flet ($e272 (not $e199)) +(flet ($e273 (xor $e239 $e154)) +(flet ($e274 (or $e144 $e144)) +(flet ($e275 (if_then_else $e267 $e230 $e258)) +(flet ($e276 (not $e22)) +(flet ($e277 (and $e17 $e192)) +(flet ($e278 (and $e246 $e135)) +(flet ($e279 (and $e228 $e234)) +(flet ($e280 (and $e232 $e263)) +(flet ($e281 (and $e268 $e269)) +(flet ($e282 (if_then_else $e188 $e229 $e183)) +(flet ($e283 (if_then_else $e150 $e276 $e236)) +(flet ($e284 (if_then_else $e252 $e24 $e211)) +(flet ($e285 (iff $e264 $e151)) +(flet ($e286 (xor $e200 $e175)) +(flet ($e287 (or $e281 $e250)) +(flet ($e288 (if_then_else $e262 $e262 $e280)) +(flet ($e289 (not $e26)) +(flet ($e290 (if_then_else $e245 $e259 $e245)) +(flet ($e291 (not $e162)) +(flet ($e292 (if_then_else $e266 $e251 $e289)) +(flet ($e293 (implies $e254 $e275)) +(flet ($e294 (or $e273 $e293)) +(flet ($e295 (xor $e272 $e224)) +(flet ($e296 (implies $e257 $e240)) +(flet ($e297 (iff $e253 $e23)) +(flet ($e298 (iff $e19 $e292)) +(flet ($e299 (implies $e282 $e196)) +(flet ($e300 (iff $e284 $e139)) +(flet ($e301 (implies $e297 $e283)) +(flet ($e302 (and $e291 $e221)) +(flet ($e303 (not $e247)) +(flet ($e304 (xor $e294 $e161)) +(flet ($e305 (not $e244)) +(flet ($e306 (iff $e290 $e279)) +(flet ($e307 (and $e300 $e182)) +(flet ($e308 (implies $e288 $e195)) +(flet ($e309 (if_then_else $e304 $e299 $e186)) +(flet ($e310 (if_then_else $e261 $e222 $e213)) +(flet ($e311 (or $e286 $e301)) +(flet ($e312 (and $e311 $e298)) +(flet ($e313 (and $e295 $e302)) +(flet ($e314 (if_then_else $e305 $e278 $e278)) +(flet ($e315 (not $e226)) +(flet ($e316 (not $e303)) +(flet ($e317 (not $e315)) +(flet ($e318 (and $e296 $e137)) +(flet ($e319 (if_then_else $e307 $e308 $e313)) +(flet ($e320 (xor $e233 $e319)) +(flet ($e321 (if_then_else $e317 $e310 $e274)) +(flet ($e322 (not $e146)) +(flet ($e323 (xor $e198 $e321)) +(flet ($e324 (implies $e316 $e271)) +(flet ($e325 (xor $e312 $e314)) +(flet ($e326 (implies $e285 $e306)) +(flet ($e327 (if_then_else $e324 $e325 $e325)) +(flet ($e328 (if_then_else $e322 $e287 $e326)) +(flet ($e329 (implies $e323 $e309)) +(flet ($e330 (if_then_else $e327 $e329 $e318)) +(flet ($e331 (if_then_else $e277 $e330 $e277)) +(flet ($e332 (not $e328)) +(flet ($e333 (implies $e332 $e332)) +(flet ($e334 (not $e320)) +(flet ($e335 (implies $e333 $e334)) +(flet ($e336 (xor $e335 $e335)) +(flet ($e337 (iff $e331 $e336)) +$e337 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +