diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-04 18:27:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-04 18:27:27 -0500 |
| commit | 64a8b1b205ccc793865bacf2b4388c534dc2f16d (patch) | |
| tree | 7ca259b5124eb1d657abc16f091aaaa57d97135d /src/smt/smt_engine.h | |
| parent | 99640a4dc014177ed3b205b7186254933e7c5566 (diff) | |
Fixes for getInterpolant and getAbduct API methods (#4846)
This fixes three issues in the getInterpolant method in the API, which was also copied to the getAbduct method:
(1) Use Node not Expr
(2) Must set up ExprManager scope
(3) The wrong solver pointer was passed to the returned term, which was causing segfaults on all abduction regressions.
We should also consider changing the interface of this method to return the term instead of a Boolean. This could be done as future work.
This fixes regress1.
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f51b6759b..5a8c41652 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -648,10 +648,12 @@ class CVC4_PUBLIC SmtEngine * This method invokes a separate copy of the SMT engine for solving the * corresponding sygus problem for generating such a solution. */ - bool getInterpol(const Expr& conj, const Type& grammarType, Expr& interpol); + bool getInterpol(const Node& conj, + const TypeNode& grammarType, + Node& interpol); /** Same as above, but without user-provided grammar restrictions */ - bool getInterpol(const Expr& conj, Expr& interpol); + bool getInterpol(const Node& conj, Node& interpol); /** * This method asks this SMT engine to find an abduct with respect to the |