diff options
Diffstat (limited to 'src/api/cvc4cpp.h')
| -rw-r--r-- | src/api/cvc4cpp.h | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 828dc6f65..76306d443 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -3023,6 +3023,29 @@ class CVC4_PUBLIC Solver void pop(uint32_t nscopes = 1) const; /** + * Get an interpolant + * SMT-LIB: ( get-interpol <term> ) + * Requires to enable option 'produce-interpols'. + * @param conj the conjecture term + * @param output a Term I such that A->I and I->B are valid, where A is the + * current set of assertions and B is given in the input by conj. + * @return true if it gets I successfully, false otherwise. + */ + bool getInterpolant(Term conj, Term& output) const; + + /** + * Get an interpolant + * SMT-LIB: ( get-interpol <term> ) + * Requires to enable option 'produce-interpols'. + * @param conj the conjecture term + * @param gtype the grammar for the interpolant I + * @param output a Term I such that A->I and I->B are valid, where A is the + * current set of assertions and B is given in the input by conj. + * @return true if it gets I successfully, false otherwise. + */ + bool getInterpolant(Term conj, const Type& gtype, Term& output) const; + + /** * Print the model of a satisfiable query to the given output stream. * Requires to enable option 'produce-models'. * @param out the output stream |