chore: fix signature of functions that can produce null terms

cvc5.lean

@@ -3057,7 +3057,10 @@ Returns a formula `Φ` such that, given the current set of formulas `A` asserted
 - `(a ∧ Q)` and (A ∧ Φ) are equivalent, and
 - `Φ` is a quantifier-free formula containing only free variables in `y_1...y_n`.
 -/
-extern_def getQuantifierElimination : (solver : Solver) → (q : Term) → Env Term
+private extern_def getQuantifierEliminationOrNull : (solver : Solver) → (q : Term) → Env Term
+with getQuantifierElimination (solver : Solver) (q : Term) : Env (Option Term) := do
+  let term? ← solver.getQuantifierEliminationOrNull q
+  if term?.isNull then return none else return term?
 
 /-- Do partial quantifier elimination, which can be used for incrementally computing the result of a
   quantifier elimination.
@@ -3066,7 +3069,6 @@ extern_def getQuantifierElimination : (solver : Solver) → (q : Term) → Env T
 (get-qe-disjunct <q>)
 ```
 
-
 **NB:** Quantifier elimination is only complete for logics such as LRA, LIA, and BV.
 
 **Warning**: this function is experimental and may change in future versions.
@@ -3087,7 +3089,10 @@ Returns a formula `Φ` such that, given the current set of formulas `A` asserted
 
   In either case, we have that `Φ ∧ Q_j` will eventually be true or false, for some finite `j`.
 -/
-extern_def getQuantifierEliminationDisjunct : (solver : Solver) → (q : Term) → Env Term
+extern_def getQuantifierEliminationDisjunctOrNull : (solver : Solver) → (q : Term) → Env Term
+with getQuantifierEliminationDisjunct (solver : Solver) (q : Term) : Env (Option Term) := do
+  let term? ← solver.getQuantifierEliminationOrNull q
+  if term?.isNull then return none else return term?
 
 /-- When using separation logic, sets the location sort and the datatype sort to the given ones.
 
@@ -3173,7 +3178,7 @@ extern_def declareOracleFun :
 -/
 extern_def pop : (solver : Solver) → (nscopes : UInt32 := 1) → Env Unit
 
-/-- Get an interpolant if one exists, the null term otherwise.
+/-- Get an interpolant if one exists.
 
 Given that `A → B` is valid, this function determines a term `I` over the shared variables of `A` and `B`, such that `A → I` and `I → B` are valid. `A` is the current set of assertions and `B` is the conjecture, given as `conj`.
 
@@ -3189,9 +3194,12 @@ Given that `A → B` is valid, this function determines a term `I` over the shar
 
 - `conj`: The conjecture term.
 -/
-extern_def getInterpolantSimple : (solver : Solver) → (conj : Term) → Env Term
+private extern_def getInterpolantSimpleOrNull : (solver : Solver) → (conj : Term) → Env Term
+with getInterpolantSimple (solver : Solver) (conj : Term) : Env (Option Term) := do
+  let term? ← solver.getInterpolantSimpleOrNull conj
+  if term?.isNull then return none else return term?
 
-/-- Get an interpolant if one exists, the null term otherwise.
+/-- Get an interpolant if one exists.
 
 Given that `A → B` is valid, this function determines a term `I` over the shared variables of `A`
 and `B`, such that `A → I` and `I → B` are valid. `I` is constructed from the given grammar. `A` is
@@ -3210,10 +3218,15 @@ the current set of assertions and `B` is the conjecture, given as `conj`.
 - `conj`: The conjecture term.
 - `grammar`: The grammar for the interpolant `I`.
 -/
-extern_def getInterpolantOfGrammar :
+private extern_def getInterpolantOfGrammarOrNull :
   (solver : Solver) → (conj : Term) → (grammar : Grammar) → Env Term
+with
+  getInterpolantOfGrammar (solver : Solver) (conj : Term) (grammar : Grammar)
+  : Env (Option Term) := do
+    let term? ← solver.getInterpolantOfGrammarOrNull conj grammar
+    if term?.isNull then return none else return term?
 
-/-- Get an interpolant if one exists, the null term otherwise.
+/-- Get an interpolant if one exists.
 
 Given that `A → B` is valid, this function determines a term `I` over the shared variables of `A`
 and `B`, such that `A → I` and `I → B` are valid. If a grammar `G` is provided, `I` is constructed
@@ -3235,12 +3248,12 @@ from `G`. `A` is the current set of assertions and `B` is the conjecture, given
 -/
 def getInterpolant
   (solver : Solver) (conj : Term) (grammar : Option Grammar := none)
-: Env Term :=
+: Env (Option Term) :=
   if let some grammar := grammar
   then solver.getInterpolantOfGrammar conj grammar
   else solver.getInterpolantSimple conj
 
-/-- Get the next interpolant if any, the null term otherwise.
+/-- Get the next interpolant if any.
 
 Can only be called immediately after a successful call to `getInterpolant`,
 `getInterpolantOfGrammar`, `getInterpolant?`, `getInterpolantNext`, or `getInterpolantNext`. It is
@@ -3259,7 +3272,10 @@ from `none`.
 Returns a term `I` such that `A → I` and `I → B` and valid, where `A` is the current set of
 assertions and `B` is given in the input by `conj`, or the null term if such a term cannot be found.
 -/
-extern_def getInterpolantNext : (solver : Solver) → Env Term
+private extern_def getInterpolantNextOrNull : (solver : Solver) → Env Term
+with getInterpolantNext (solver : Solver) : Env (Option Term) := do
+  let term? ← solver.getInterpolantNextOrNull
+  if term?.isNull then return none else return term?
 
 /-- Get an abduct if one exists, the null term otherwise.
 
@@ -3277,9 +3293,12 @@ Returns a term `C` such that `A ∧ C` is satisfiable, and `A ∧ ¬B ∧ C` is
 the current set of assertions and `B` is given in the input by `conj`, or the null term if such a
 term cannot be found.
 -/
-private extern_def getAbductSimple : (solver : Solver) → (conj : Term) → Env Term
+private extern_def getAbductSimpleOrNull : (solver : Solver) → (conj : Term) → Env Term
+with getAbductSimple (solver : Solver) (conj : Term) : Env (Option Term) := do
+  let term? ← solver.getAbductSimpleOrNull conj
+  if term?.isNull then return none else return term?
 
-/-- Get an abduct if one exists, the null term otherwise.
+/-- Get an abduct if one exists.
 
 ```smtlib
 (get-abduct <conj> <grammar>)
@@ -3296,8 +3315,12 @@ Returns a term `C` such that `A ∧ C` is satisfiable, and `A ∧ ¬B ∧ C` is
 the current set of assertions and `B` is given in the input by `conj`, or the null term if such a
 term cannot be found.
 -/
-extern_def getAbductOfGrammar :
+private extern_def getAbductOfGrammarOrNull :
   (solver : Solver) → (conj : Term) → (grammar : Grammar) → Env Term
+with
+  getAbductOfGrammar (solver : Solver) (conj : Term) (grammar : Grammar) : Env (Option Term) := do
+    let term? ← solver.getAbductOfGrammarOrNull conj grammar
+    if term?.isNull then return none else return term?
 
 /-- Get an abduct if one exists.
 
@@ -3319,12 +3342,12 @@ term cannot be found.
 -/
 def getAbduct
   (solver : Solver) (conj : Term) (grammar : Option Grammar := none)
-: Env Term :=
+: Env (Option Term) :=
   if let some grammar := grammar
   then solver.getAbductOfGrammar conj grammar
   else solver.getAbductSimple conj
 
-/-- Get the next interpolant if any, the null term otherwise.
+/-- Get the next interpolant if any.
 
 Can only be called immediately after a successful call to `getAbduct`, `getAbductOfGrammar`,
 `getAbduct?`, `getAbductNext`, or `getAbductNext?`. It is guaranteed to produce a syntactically
@@ -3342,7 +3365,10 @@ Returns a term `C` such that `A ∧ C` is satisfiable, and `A ∧ ¬B ∧ C` is
 the current set of assertions and `B` is given in the input by the last call to a `getAbduct`-like
 function, or the null term if such a term cannot be found.
 -/
-extern_def getAbductNext : (solver : Solver) → Env Term
+private extern_def getAbductNextOrNull : (solver : Solver) → Env Term
+with getAbductNext (solver : Solver) : Env (Option Term) := do
+  let term? ← solver.getAbductNextOrNull
+  if term?.isNull then return none else return term?
 
 /-- Block the current model. Can be called only if immediately preceded by a SAT or INVALID query.
 

cvc5Test/Init.lean

@@ -34,6 +34,20 @@ def assertTrue (b : Bool) (hint := "") : IO Unit :=
 def assertFalse (b : Bool) (hint := "") : IO Unit :=
   assertEq false b hint
 
+def assertNone [ToString α] (a? : Option α) (hint := "") : IO Unit := do
+  if let some a := a? then
+    IO.eprintln s!"{Test.pref hint}expected none, got {a}"
+    fail "assertion failed"
+
+def assertSome (a? : Option α) (hint := "") : IO α := do
+  let some a := a?
+    | IO.eprintln s!"{Test.pref hint}expected non-none value, got none"
+      fail "assertion failed"
+  return a
+
+def assertSomeDiscard (a? : Option α) (hint := "") : IO Unit := do
+  let _ ← assertSome a? (hint := hint)
+
 def assertNe [ToString α] [BEq α] (lft rgt : α) (hint := "") : IO Unit := do
   if lft == rgt then
     IO.eprintln s!"{Test.pref hint}comparison failed: `{lft}` is the same as `{rgt}`"

cvc5Test/Unit/ApiSolver.lean

@@ -731,9 +731,10 @@ test![TestApiBlackSolver, getAbduct] tm solver => do
   -- conjecture for abduction `y > 0`
   let conj ← tm.mkTerm Kind.GT #[y, zero]
   -- call the abduction api, while the resulting abduct is the output
-  let output ← solver.getAbduct conj
+  let output? ← solver.getAbduct conj
   -- we expect the resulting output to be a boolean formula
-  assertTrue (¬ output.isNull ∧ (← output.getSort).isBoolean)
+  let output ← assertSome output?
+  assertTrue (← output.getSort).isBoolean
 
   -- try with a grammar, a simple grammar admitting true
   let truen ← tm.mkBoolean true
@@ -744,8 +745,9 @@ test![TestApiBlackSolver, getAbduct] tm solver => do
     "invalid grammar, must have at least one rule for each non-terminal symbol"
   g ← g.addRule start truen
   -- call the abduction api, while the resulting abduct is the output
-  let output2 ← solver.getAbduct conj2 g
+  let output2? ← solver.getAbduct conj2 g
   -- abduct must be true
+  let output2 ← assertSome output2?
   assertEq truen output2
 
   let tm' ← TermManager.new
@@ -820,8 +822,9 @@ test![TestApiBlackSolver, getInterpolant] tm solver => do
     ← tm.mkTerm Kind.LT #[z, zero],
   ]
   -- call the interpolation api, while the resulting interpolant is the output
-  let output ← solver.getInterpolant conj
+  let output? ← solver.getInterpolant conj
   -- we expect the resulting output to be a boolean formula
+  let output ← assertSome output?
   assertTrue (← output.getSort).isBoolean
 
   -- try with a grammar, a simple grammar admitting true
@@ -833,8 +836,9 @@ test![TestApiBlackSolver, getInterpolant] tm solver => do
     "invalid grammar, must have at least one rule for each non-terminal symbol"
   g ← g.addRule start truen |> assertOk
   -- call the interpolation api, while the resulting interpolant is the output
-  let output2 ← solver.getInterpolant conj2 g
+  let output2? ← solver.getInterpolant conj2 g
   -- interpolant must be true
+  let output2 ← assertSome output2?
   assertEq truen output2
 
   let tm' ← TermManager.new

ffi/ffi.cpp

@@ -3923,7 +3923,7 @@ LEAN_EXPORT lean_obj_res solver_getModel(lean_obj_arg solver,
   CVC5_LEAN_API_TRY_CATCH_ENV_END;
 }
 
-LEAN_EXPORT lean_obj_res solver_getQuantifierElimination(lean_obj_arg solver,
+LEAN_EXPORT lean_obj_res solver_getQuantifierEliminationOrNull(lean_obj_arg solver,
                                                          lean_obj_arg term)
 {
   CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN;
@@ -3933,7 +3933,7 @@ LEAN_EXPORT lean_obj_res solver_getQuantifierElimination(lean_obj_arg solver,
 }
 
 LEAN_EXPORT lean_obj_res
-solver_getQuantifierEliminationDisjunct(lean_obj_arg solver, lean_obj_arg term)
+solver_getQuantifierEliminationDisjunctOrNull(lean_obj_arg solver, lean_obj_arg term)
 {
   CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN;
   return env_val(
@@ -4049,7 +4049,7 @@ LEAN_EXPORT lean_obj_res solver_pop(lean_obj_arg solver, uint32_t nscopes)
   CVC5_LEAN_API_TRY_CATCH_ENV_END;
 }
 
-LEAN_EXPORT lean_obj_res solver_getInterpolantSimple(lean_obj_arg solver,
+LEAN_EXPORT lean_obj_res solver_getInterpolantSimpleOrNull(lean_obj_arg solver,
                                                      lean_obj_arg conj)
 {
   CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN;
@@ -4058,7 +4058,7 @@ LEAN_EXPORT lean_obj_res solver_getInterpolantSimple(lean_obj_arg solver,
   CVC5_LEAN_API_TRY_CATCH_ENV_END;
 }
 
-LEAN_EXPORT lean_obj_res solver_getInterpolantOfGrammar(lean_obj_arg solver,
+LEAN_EXPORT lean_obj_res solver_getInterpolantOfGrammarOrNull(lean_obj_arg solver,
                                                         lean_obj_arg conj,
                                                         lean_obj_arg grammar)
 {
@@ -4068,15 +4068,15 @@ LEAN_EXPORT lean_obj_res solver_getInterpolantOfGrammar(lean_obj_arg solver,
   CVC5_LEAN_API_TRY_CATCH_ENV_END;
 }
 
-LEAN_EXPORT lean_obj_res solver_getInterpolantNext(lean_obj_arg solver)
+LEAN_EXPORT lean_obj_res solver_getInterpolantNextOrNull(lean_obj_arg solver)
 {
   CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN;
   return env_val(
       term_box(new Term(solver_unbox(solver)->getInterpolantNext())));
   CVC5_LEAN_API_TRY_CATCH_ENV_END;
 }
 
-LEAN_EXPORT lean_obj_res solver_getAbductSimple(lean_obj_arg solver,
+LEAN_EXPORT lean_obj_res solver_getAbductSimpleOrNull(lean_obj_arg solver,
                                                 lean_obj_arg conj)
 {
   CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN;
@@ -4085,7 +4085,7 @@ LEAN_EXPORT lean_obj_res solver_getAbductSimple(lean_obj_arg solver,
   CVC5_LEAN_API_TRY_CATCH_ENV_END;
 }
 
-LEAN_EXPORT lean_obj_res solver_getAbductOfGrammar(lean_obj_arg solver,
+LEAN_EXPORT lean_obj_res solver_getAbductOfGrammarOrNull(lean_obj_arg solver,
                                                    lean_obj_arg conj,
                                                    lean_obj_arg grammar)
 {
@@ -4095,7 +4095,7 @@ LEAN_EXPORT lean_obj_res solver_getAbductOfGrammar(lean_obj_arg solver,
   CVC5_LEAN_API_TRY_CATCH_ENV_END;
 }
 
-LEAN_EXPORT lean_obj_res solver_getAbductNext(lean_obj_arg solver)
+LEAN_EXPORT lean_obj_res solver_getAbductNextOrNull(lean_obj_arg solver)
 {
   CVC5_LEAN_API_TRY_CATCH_ENV_BEGIN;
   return env_val(term_box(new Term(solver_unbox(solver)->getAbductNext())));