Home
last modified time | relevance | path

Searched refs:toSumNode (Results 1 – 1 of 1) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/arith/
H A Dtheory_arith_private.cpp81 static Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum);
2338 Node sum = toSumNode(d_partialModel, lhs); in replayGetConstraint()
2454 Node toSumNode(const ArithVariables& vars, const DenseMap<Rational>& sum){ in toSumNode() function
2985 Node sum = toSumNode(d_partialModel, lhs); in cutToLiteral()