diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-26 17:30:44 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-26 17:30:44 +0000 |
commit | c3ca3d8c58cc9954f8ad190e1e2dedbcbb5372f0 (patch) | |
tree | 4830fb02118a499da8cb62aaec06b16919e0d05a /src | |
parent | 2a731b9164bb178f1232a9af0babc7dd84450cea (diff) |
Removing DioSolver::acceptableOriginalNodes(). This assertion was too strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/dio_solver.cpp | 20 | ||||
-rw-r--r-- | src/theory/arith/dio_solver.h | 5 |
2 files changed, 2 insertions, 23 deletions
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 46ca717bf..4d9d66cec 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -132,27 +132,11 @@ bool DioSolver::debugEqualityInInputEquations(Node eq){ return false; } -bool DioSolver::acceptableOriginalNodes(Node n){ - Kind k = n.getKind(); - if(k == kind::EQUAL){ - return true; - }else if(k == kind::AND){ - Node ub = n[0]; - Node lb = n[1]; - Kind kub = Comparison::comparisonKind(ub); - Kind klb = Comparison::comparisonKind(lb); - Debug("nf::tmp") << n << endl; - return (kub == kind::GEQ || kub==kind::LT) && (klb == kind::GEQ || klb == kind::LT); - }else{ - return false; - } -} void DioSolver::pushInputConstraint(const Comparison& eq, Node reason){ Assert(!debugEqualityInInputEquations(reason)); Assert(eq.debugIsIntegral()); Assert(eq.getNode().getKind() == kind::EQUAL); - Assert(acceptableOriginalNodes(reason)); SumPair sp = eq.toSumPair(); uint32_t length = sp.maxLength(); @@ -209,7 +193,6 @@ Node DioSolver::proveIndex(TrailIndex i){ Variable v = vl.getHead(); Node input = proofVariableToReason(v); - Assert(acceptableOriginalNodes(input)); if(input.getKind() == kind::AND){ for(Node::iterator input_iter = input.begin(), input_end = input.end(); input_iter != input_end; ++input_iter){ Node inputChild = *input_iter; @@ -689,9 +672,10 @@ std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::decomposeIndex( TrailIndex ci = d_trail.size(); d_trail.push_back(Constraint(newSI, Polynomial::mkZero())); + // no longer reference av safely! Debug("arith::dio") << "Decompose ci(" << ci <<":" << d_trail[ci].d_eq.getNode() - << ") for " << av.getNode() << endl; + << ") for " << d_trail[i].d_minimalMonomial.getNode() << endl; Assert(d_trail[ci].d_eq.getPolynomial().getCoefficient(vl) == Constant::mkConstant(-1)); SumPair newFact = r + fresh_a; diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 7d1faed86..bfcd19021 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -237,11 +237,6 @@ private: */ size_t allocateVariableInPool(); - /** - * Returns true if the node can be accepted as a reason according to the - * kinds. - */ - bool acceptableOriginalNodes(Node n); /** Empties the unproccessed input constraints into the queue. */ void enqueueInputConstraints(); |