diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2020-08-12 15:17:18 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-12 08:17:18 -0500 |
commit | 558ceb2f64877fa2cc5f1cd448147e529b5c1c02 (patch) | |
tree | 31beed1c4b0b792bf6328b25a5e576e48b118970 /src/theory | |
parent | 0e39025474cb32a3b96ebc93afd8a761ca0ec9ef (diff) |
Fix infinite loop in arith_ite_simp (#4805)
We have an open issue with an infinite loop with --ite-simp for a long time in #789 , for example on
(declare-fun a () Int)
(declare-fun b () Int)
(assert
(and
(= 1 (+ a b))
(or (= 0 a) (= 0 b))
(or (= 0 b) (>= b 8))
(or (= 0 a) (not (>= b 8)))
)
)
(check-sat)
The problem goes back to arith_ite_utils.cpp and roughly is as follows:
The method solveBinOr looks for patterns like (or (= b 0) (= b 1)). It introduces a new Boolean variable deor_1 and substitutes b -> (ite deor_1 1 0).
The method also stores another mapping in d_skolems: deor_1 -> (>= b 8) here which is also used in selectForCmp. However, these skolems are also used to add even more substitutions here after applying the already added substitutions to it. Eventually, we have a substitution deor_1 -> (>= (ite deor_1 1 0) 8) which inevitably leads to an infinite loop.
I have found no reason for the second mapping (deor_1 -> (>= b 8)) to be added as a substitution, and thus this PR removes it.
Benchmarks are running to check whether there are further issues with this, and whether this simplification is beneficial.
Fixes #789.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/arith_ite_utils.cpp | 11 | ||||
-rw-r--r-- | src/theory/arith/arith_ite_utils.h | 2 |
2 files changed, 0 insertions, 13 deletions
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp index 4892389f2..15fd7af6c 100644 --- a/src/theory/arith/arith_ite_utils.cpp +++ b/src/theory/arith/arith_ite_utils.cpp @@ -151,7 +151,6 @@ ArithIteUtils::ArithIteUtils( d_subcount(uc, 0), d_skolems(uc), d_implies(), - d_skolemsAdded(), d_orBinEqs() { d_subs = new SubstitutionMap(uc); @@ -313,16 +312,7 @@ void ArithIteUtils::learnSubstitutions(const std::vector<Node>& assertions){ d_orBinEqs.resize(writePos); }while(solvedSomething); - for(size_t i = 0, N=d_skolemsAdded.size(); i<N; ++i){ - Node sk = d_skolemsAdded[i]; - Node to = d_skolems[sk]; - if(!to.isNull()){ - Node fp = applySubstitutions(to); - addSubstitution(sk, fp); - } - } d_implies.clear(); - d_skolemsAdded.clear(); d_orBinEqs.clear(); } @@ -457,7 +447,6 @@ bool ArithIteUtils::solveBinOr(TNode binor){ Node sk = nm->mkSkolem("deor", nm->booleanType()); Node ite = sk.iteNode(otherL, otherR); d_skolems.insert(sk, cnd); - d_skolemsAdded.push_back(sk); addSubstitution(sel, ite); return true; } diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h index f86328d5d..d03b0795f 100644 --- a/src/theory/arith/arith_ite_utils.h +++ b/src/theory/arith/arith_ite_utils.h @@ -69,8 +69,6 @@ class ArithIteUtils { typedef std::map<Node, std::set<Node> > ImpMap; ImpMap d_implies; - std::vector<Node> d_skolemsAdded; - std::vector<Node> d_orBinEqs; public: |