diff options
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(); |