From 795ab3d4e6a2e75e4e6c6d795d78ef3ae3d17eeb Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 14 Dec 2010 01:04:00 +0000 Subject: [PATCH] fix to static learning application in UF, resolves bug# 239 --- src/theory/uf/morgan/theory_uf_morgan.cpp | 1 + test/regress/regress0/Makefile.am | 3 +- test/regress/regress0/bug239.smt | 185 ++++++++++++++++++++++ 3 files changed, 188 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/bug239.smt diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index ef00b5818..cd9ee79c3 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -647,6 +647,7 @@ void TheoryUFMorgan::staticLearning(TNode n, NodeBuilder<>& learned) { // binary OR of binary ANDs of EQUALities if(n.getKind() == kind::OR && n.getNumChildren() == 2 && n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 && + n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 && (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) && (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) && (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) && diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 73901c328..6ce2468b8 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -84,7 +84,8 @@ BUG_TESTS = \ bug168.smt \ bug187.smt2 \ bug216.smt2 \ - bug220.smt2 + bug220.smt2 \ + bug239.smt TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug239.smt b/test/regress/regress0/bug239.smt new file mode 100644 index 000000000..b80f56c44 --- /dev/null +++ b/test/regress/regress0/bug239.smt @@ -0,0 +1,185 @@ +(benchmark fuzzsmt +:logic QF_LRA +:status sat +:extrafuns ((v0 Real)) +:extrafuns ((v1 Real)) +:extrafuns ((v2 Real)) +:formula +(let (?e3 5) +(let (?e4 0) +(let (?e5 2) +(let (?e6 (+ v0 v1)) +(let (?e7 (* v1 ?e3)) +(let (?e8 (~ v0)) +(let (?e9 (- v2 v1)) +(let (?e10 (- v0 ?e9)) +(let (?e11 (* v0 (~ ?e3))) +(let (?e12 (/ ?e4 (~ ?e3))) +(let (?e13 (+ ?e8 ?e7)) +(let (?e14 (/ ?e4 (~ ?e5))) +(flet ($e15 (<= v2 ?e7)) +(flet ($e16 (<= ?e11 ?e11)) +(flet ($e17 (= ?e11 ?e13)) +(flet ($e18 (<= ?e7 ?e14)) +(flet ($e19 (> ?e14 v1)) +(flet ($e20 (< v0 ?e10)) +(flet ($e21 (= ?e8 ?e11)) +(flet ($e22 (>= ?e8 ?e13)) +(flet ($e23 (< ?e10 v2)) +(flet ($e24 (>= ?e10 ?e8)) +(flet ($e25 (= ?e6 ?e7)) +(flet ($e26 (distinct ?e12 ?e11)) +(flet ($e27 (distinct ?e10 ?e9)) +(let (?e28 (ite $e27 ?e13 ?e6)) +(let (?e29 (ite $e21 v2 ?e28)) +(let (?e30 (ite $e26 ?e12 ?e12)) +(let (?e31 (ite $e18 ?e28 v0)) +(let (?e32 (ite $e20 ?e9 ?e10)) +(let (?e33 (ite $e22 ?e11 ?e28)) +(let (?e34 (ite $e17 ?e8 ?e13)) +(let (?e35 (ite $e26 ?e14 v1)) +(let (?e36 (ite $e21 ?e14 ?e30)) +(let (?e37 (ite $e19 ?e7 ?e11)) +(let (?e38 (ite $e25 v1 ?e8)) +(let (?e39 (ite $e22 ?e28 ?e28)) +(let (?e40 (ite $e25 v0 ?e14)) +(let (?e41 (ite $e24 ?e37 v2)) +(let (?e42 (ite $e16 ?e6 v2)) +(let (?e43 (ite $e19 ?e11 ?e7)) +(let (?e44 (ite $e23 ?e36 v2)) +(let (?e45 (ite $e20 v1 ?e7)) +(let (?e46 (ite $e15 ?e45 ?e13)) +(flet ($e47 (= ?e32 ?e9)) +(flet ($e48 (< ?e41 v0)) +(flet ($e49 (distinct ?e14 ?e43)) +(flet ($e50 (distinct ?e8 ?e10)) +(flet ($e51 (> ?e8 ?e37)) +(flet ($e52 (< v1 ?e11)) +(flet ($e53 (< ?e30 ?e8)) +(flet ($e54 (< v2 ?e12)) +(flet ($e55 (>= ?e8 ?e31)) +(flet ($e56 (= ?e12 ?e44)) +(flet ($e57 (= ?e45 v0)) +(flet ($e58 (= ?e36 ?e39)) +(flet ($e59 (= ?e31 v0)) +(flet ($e60 (< ?e9 ?e43)) +(flet ($e61 (distinct ?e14 ?e44)) +(flet ($e62 (= ?e45 ?e29)) +(flet ($e63 (<= ?e12 ?e9)) +(flet ($e64 (>= ?e41 ?e28)) +(flet ($e65 (<= ?e11 v0)) +(flet ($e66 (< ?e29 ?e14)) +(flet ($e67 (< ?e44 v2)) +(flet ($e68 (< ?e40 ?e45)) +(flet ($e69 (> ?e34 ?e7)) +(flet ($e70 (= ?e38 ?e30)) +(flet ($e71 (>= ?e36 ?e31)) +(flet ($e72 (= ?e32 ?e38)) +(flet ($e73 (<= ?e30 ?e42)) +(flet ($e74 (= ?e11 ?e9)) +(flet ($e75 (> ?e40 ?e7)) +(flet ($e76 (distinct ?e39 ?e41)) +(flet ($e77 (< ?e11 ?e28)) +(flet ($e78 (distinct ?e31 ?e45)) +(flet ($e79 (= ?e45 ?e11)) +(flet ($e80 (>= ?e11 ?e42)) +(flet ($e81 (< ?e12 ?e7)) +(flet ($e82 (>= ?e11 ?e41)) +(flet ($e83 (<= ?e8 v0)) +(flet ($e84 (< ?e8 ?e8)) +(flet ($e85 (> ?e30 v2)) +(flet ($e86 (= ?e9 ?e30)) +(flet ($e87 (= ?e33 ?e7)) +(flet ($e88 (<= ?e32 ?e44)) +(flet ($e89 (<= ?e36 ?e33)) +(flet ($e90 (distinct ?e45 ?e45)) +(flet ($e91 (distinct ?e14 ?e44)) +(flet ($e92 (<= v1 ?e12)) +(flet ($e93 (>= v0 ?e12)) +(flet ($e94 (>= ?e46 ?e29)) +(flet ($e95 (> ?e14 ?e6)) +(flet ($e96 (>= v2 ?e14)) +(flet ($e97 (>= ?e39 ?e44)) +(flet ($e98 (>= ?e38 ?e28)) +(flet ($e99 (> v2 ?e9)) +(flet ($e100 (<= ?e42 ?e33)) +(flet ($e101 (= ?e30 ?e29)) +(flet ($e102 (= ?e9 v0)) +(flet ($e103 (distinct ?e37 ?e40)) +(flet ($e104 (= ?e43 ?e14)) +(flet ($e105 (<= ?e35 ?e13)) +(flet ($e106 (and $e102 $e70)) +(flet ($e107 (implies $e84 $e84)) +(flet ($e108 (implies $e69 $e60)) +(flet ($e109 (iff $e105 $e99)) +(flet ($e110 (iff $e100 $e80)) +(flet ($e111 (or $e52 $e86)) +(flet ($e112 (xor $e26 $e18)) +(flet ($e113 (or $e20 $e107)) +(flet ($e114 (not $e94)) +(flet ($e115 (or $e79 $e104)) +(flet ($e116 (not $e76)) +(flet ($e117 (if_then_else $e112 $e22 $e90)) +(flet ($e118 (xor $e77 $e57)) +(flet ($e119 (xor $e88 $e55)) +(flet ($e120 (and $e92 $e68)) +(flet ($e121 (or $e82 $e25)) +(flet ($e122 (implies $e19 $e119)) +(flet ($e123 (implies $e66 $e117)) +(flet ($e124 (if_then_else $e15 $e73 $e65)) +(flet ($e125 (iff $e64 $e103)) +(flet ($e126 (iff $e121 $e122)) +(flet ($e127 (if_then_else $e50 $e47 $e101)) +(flet ($e128 (iff $e81 $e127)) +(flet ($e129 (implies $e124 $e21)) +(flet ($e130 (iff $e87 $e129)) +(flet ($e131 (iff $e116 $e51)) +(flet ($e132 (implies $e72 $e97)) +(flet ($e133 (and $e56 $e98)) +(flet ($e134 (implies $e91 $e53)) +(flet ($e135 (xor $e133 $e114)) +(flet ($e136 (xor $e17 $e110)) +(flet ($e137 (iff $e96 $e128)) +(flet ($e138 (or $e125 $e59)) +(flet ($e139 (or $e23 $e48)) +(flet ($e140 (iff $e62 $e95)) +(flet ($e141 (not $e61)) +(flet ($e142 (and $e132 $e63)) +(flet ($e143 (xor $e109 $e131)) +(flet ($e144 (iff $e54 $e126)) +(flet ($e145 (xor $e74 $e67)) +(flet ($e146 (if_then_else $e89 $e93 $e140)) +(flet ($e147 (iff $e71 $e138)) +(flet ($e148 (and $e143 $e146)) +(flet ($e149 (xor $e147 $e142)) +(flet ($e150 (implies $e85 $e58)) +(flet ($e151 (or $e24 $e78)) +(flet ($e152 (if_then_else $e137 $e113 $e123)) +(flet ($e153 (and $e145 $e16)) +(flet ($e154 (not $e150)) +(flet ($e155 (implies $e151 $e154)) +(flet ($e156 (if_then_else $e118 $e136 $e75)) +(flet ($e157 (and $e108 $e108)) +(flet ($e158 (or $e83 $e141)) +(flet ($e159 (iff $e155 $e149)) +(flet ($e160 (iff $e158 $e156)) +(flet ($e161 (or $e115 $e130)) +(flet ($e162 (or $e157 $e160)) +(flet ($e163 (if_then_else $e152 $e153 $e139)) +(flet ($e164 (not $e144)) +(flet ($e165 (not $e27)) +(flet ($e166 (or $e148 $e162)) +(flet ($e167 (iff $e134 $e166)) +(flet ($e168 (or $e111 $e159)) +(flet ($e169 (or $e106 $e164)) +(flet ($e170 (xor $e161 $e120)) +(flet ($e171 (and $e168 $e165)) +(flet ($e172 (or $e170 $e135)) +(flet ($e173 (or $e169 $e163)) +(flet ($e174 (implies $e49 $e172)) +(flet ($e175 (xor $e174 $e173)) +(flet ($e176 (and $e171 $e175)) +(flet ($e177 (implies $e167 $e176)) +$e177 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + -- 2.30.2