diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-12 11:14:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-12 11:14:08 -0500 |
| commit | 3ce6e00068c02286704143d82d5f044fdb356516 (patch) | |
| tree | 53d8403a8cc2c92db4cb815861f5c7cd56dee446 /src/smt/interpolation_solver.h | |
| parent | e93c443a0bfb1a66909e8467b24da399be3d01ac (diff) | |
Eliminate uses of Expr in SmtEngine interface (#5240)
This eliminates all use of Expr in the SmtEngine except in a few interfaces (setUserAttribute, getAssignment) whose signature is currently in question.
The next steps will be to (1) eliminate Expr from the smt/model.h interface, (2) replace Type by TypeNode in Sort.
Diffstat (limited to 'src/smt/interpolation_solver.h')
| -rw-r--r-- | src/smt/interpolation_solver.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h index 8e6d2cd14..096cf8983 100644 --- a/src/smt/interpolation_solver.h +++ b/src/smt/interpolation_solver.h @@ -71,8 +71,8 @@ class InterpolationSolver * the interpolation problem (interpol), and the solution implies the goal * (conj). If these criteria are not met, an internal error is thrown. */ - void checkInterpol(Expr interpol, - const std::vector<Expr>& easserts, + void checkInterpol(Node interpol, + const std::vector<Node>& easserts, const Node& conj); private: |