diff options
Diffstat (limited to 'src/theory/arith/constraint.h')
| -rw-r--r-- | src/theory/arith/constraint.h | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h index d00f16c90..33e39a5f0 100644 --- a/src/theory/arith/constraint.h +++ b/src/theory/arith/constraint.h @@ -571,8 +571,7 @@ class Constraint { * This is not appropriate for propagation! * Use explainForPropagation() instead. */ - std::shared_ptr<ProofNode> externalExplainByAssertions( - NodeBuilder<>& nb) const + std::shared_ptr<ProofNode> externalExplainByAssertions(NodeBuilder& nb) const { return externalExplain(nb, AssertionOrderSentinel); } @@ -876,7 +875,7 @@ class Constraint { * This is the minimum fringe of the implication tree * s.t. every constraint is assertedBefore(order) or hasEqualityEngineProof(). */ - std::shared_ptr<ProofNode> externalExplain(NodeBuilder<>& nb, + std::shared_ptr<ProofNode> externalExplain(NodeBuilder& nb, AssertionOrder order) const; static Node externalExplain(const ConstraintCPVec& b, AssertionOrder order); @@ -1168,7 +1167,7 @@ private: */ TrustNode eeExplain(ConstraintCP c) const; /** Get an explanation for this constraint from the equality engine */ - void eeExplain(ConstraintCP c, NodeBuilder<>& nb) const; + void eeExplain(ConstraintCP c, NodeBuilder& nb) const; /** * Returns a constraint with the variable v, the constraint type t, and a value |