Searched refs:letOrder (Results 1 – 1 of 1) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/proof/ |
| H A D | proof_manager.cpp | 1005 void bind(Expr term, ProofLetMap& map, Bindings& letOrder) { in bind() argument
1011 bind(term[i], map, letOrder); in bind()
1023 bind(currentExpression.toExpr(), map, letOrder); in bind()
1029 letOrder.push_back(LetOrderElement(term, newId)); in bind()
1037 Bindings letOrder; in printGlobalLetMap() local
1040 bind(atom->toExpr(), letMap, letOrder); in printGlobalLetMap()
1046 bind(atom->toExpr(), letMap, letOrder); in printGlobalLetMap()
1049 for (unsigned i = 0; i < letOrder.size(); ++i) { in printGlobalLetMap()
1050 Expr currentExpr = letOrder[i].expr; in printGlobalLetMap()
1051 unsigned letId = letOrder[i].id; in printGlobalLetMap()
|