Term api and io world (#38)

* chore: remove obsolete `ioWorld` parameters in FFI

* chore: catch more C++ exceptions, format C++

* feat: fix/augment `Term` api

* chore(test): add `Term` unit tests

* chore: improve test syntax-ext, simplify tests

* feat: finish lifting the `Term` api (except `getStringValue`), with tests

Author: AdrienChampion

cvc5.lean

@@ -129,7 +129,9 @@ scoped syntax
 macro_rules
 | `(command|
   $[ $outputComment:docComment ]?
-  test! $[ [ $fileId:ident , $testId:ident ] ]? $[$tmIdent?:ident =>]? $code:term
+  test! $[ [ $fileId:ident , $testId:ident ] ]?
+    $[$tmIdent?:ident $[$solverIdent?:ident]? =>]?
+    $code:term
 ) => do
   let errPrefStrLit :=
     match (fileId, testId) with
@@ -139,10 +141,25 @@ macro_rules
   let runFun ← `(term| cvc5.Env.run)
   let toRun ←
     if let some tmIdent := tmIdent? then
-      `(do
-          let $tmIdent:ident ← TermManager.new
-          $code:term
-      )
+      let boolIdent := `bool |> Lean.mkIdent
+      let intIdent := `int |> Lean.mkIdent
+      let realIdent := `real |> Lean.mkIdent
+      let uninterpretedIdent := `uninterpreted |> Lean.mkIdent
+      if let some (some solverIdent) := solverIdent? then
+        `(do
+            let $tmIdent:ident ← TermManager.new
+            let $solverIdent:ident ← Solver.new $tmIdent
+            let $boolIdent ← $tmIdent:ident |>.getBooleanSort
+            let $intIdent ← $tmIdent:ident |>.getIntegerSort
+            let $realIdent ← $tmIdent:ident |>.getRealSort
+            let $uninterpretedIdent ← $tmIdent:ident |>.mkUninterpretedSort "u"
+            $code:term
+        )
+      else
+        `(do
+            let $tmIdent:ident ← TermManager.new
+            $code:term
+        )
     else `(do $code:term)
 
   `(

cvc5Test/Init.lean

@@ -10,10 +10,10 @@ def mkTerms1 : IO Unit := Env.runIO do
     ← tm.mkBoolean true,
     ← tm.mkBoolean false,
   )
-  assertEq tru.getKind boolKind
-  assertEq tru.getSort.toString "Bool"
-  assertEq fls.getKind boolKind
-  assertEq fls.getSort.toString "Bool"
+  assertEq (← tru.getKind) boolKind
+  assertEq (← tru.getSort).toString "Bool"
+  assertEq (← fls.getKind) boolKind
+  assertEq (← fls.getSort).toString "Bool"
 
   let intKind := Kind.CONST_INTEGER
 
@@ -23,30 +23,30 @@ def mkTerms1 : IO Unit := Env.runIO do
     ← tm.mkInteger 7,
     ← tm.mkInteger 11,
   )
-  assertEq one.getKind intKind
-  assertEq one.getSort.toString "Int"
-  assertEq three.getKind intKind
-  assertEq three.getSort.toString "Int"
-  assertEq seven.getKind intKind
-  assertEq seven.getSort.toString "Int"
-  assertEq eleven.getKind intKind
-  assertEq eleven.getSort.toString "Int"
+  assertEq (← one.getKind) intKind
+  assertEq (← one.getSort).toString "Int"
+  assertEq (← three.getKind) intKind
+  assertEq (← three.getSort).toString "Int"
+  assertEq (← seven.getKind) intKind
+  assertEq (← seven.getSort).toString "Int"
+  assertEq (← eleven.getKind) intKind
+  assertEq (← eleven.getSort).toString "Int"
 
   let ite1 ← tm.mkTerm Kind.ITE #[fls, three, seven]
-  assertEq ite1.getKind Kind.ITE
-  assertEq ite1.getSort.toString "Int"
+  assertEq (← ite1.getKind) Kind.ITE
+  assertEq (← ite1.getSort).toString "Int"
 
   let eq1 ← tm.mkTerm Kind.EQUAL #[ite1, eleven]
-  assertEq eq1.getKind Kind.EQUAL
-  assertEq eq1.getSort.toString "Bool"
+  assertEq (← eq1.getKind) Kind.EQUAL
+  assertEq (← eq1.getSort).toString "Bool"
 
   let eq1' ← tm.mkTerm Kind.EQUAL #[ite1, eleven, one]
-  assertEq eq1'.getKind Kind.AND
-  assertEq eq1'.getSort.toString "Bool"
+  assertEq (← eq1'.getKind) Kind.AND
+  assertEq (← eq1'.getSort).toString "Bool"
 
   let ite2 ← tm.mkTerm Kind.ITE #[tru, eq1, fls]
-  assertEq ite2.getKind Kind.ITE
-  assertEq ite2.getSort.toString "Bool"
+  assertEq (← ite2.getKind) Kind.ITE
+  assertEq (← ite2.getSort).toString "Bool"
 
 #guard_msgs in
   #eval mkTerms1

cvc5Test/MkTerms1.lean

@@ -18,8 +18,7 @@ def parseCommand (parser : InputParser) (s : String) : Env Command := do
   parser.appendIncrementalStringInput s
   parser.nextCommand
 
-test![TestApiBlackCommand, invoke] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackCommand, invoke] tm solver => do
   let parser ← InputParser.new solver
   let sm ← parser.getSymbolManager
   parser.setIncrementalStringInput
@@ -34,16 +33,14 @@ test![TestApiBlackCommand, invoke] tm => do
   assertError "Only one set-logic is allowed." do
     parseCommand parser "(set-logic QF_LRA)"
 
-test![TestApiBlackCommand, toString] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackCommand, toString] tm solver => do
   let parser ← InputParser.new solver
   parser.setIncrementalStringInput
   let cmd ← parseCommand parser "(set-logic QF_LIA)"
   assertFalse cmd.isNull
   assertEq cmd.toString "(set-logic QF_LIA)"
 
-test![TestApiBlackCommand, getCommandName] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackCommand, getCommandName] tm solver => do
   -- not in original test, silences the stderr warnings since the logic is not set otherwise
   solver.setLogic "ALL"
   let parser ← InputParser.new solver

cvc5Test/Unit/ApiCommand.lean

@@ -22,14 +22,12 @@ def parseLogicCommand (parser : InputParser) (logic : String) : Env Command := d
 test![TestApiBlackInputParser, constructSymbolManager] tm => do
   let _ ← SymbolManager.new tm
 
-test![TestApiBlackInputParser, setFileInput] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, setFileInput] tm solver => do
   let parser ← InputParser.new solver
   assertError "Couldn't open file: nonexistent.smt2" do
     parser.setFileInput "nonexistent.smt2"
 
-test![TestApiBlackInputParser, setStreamInput] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, setStreamInput] tm solver => do
   let parser ← InputParser.new solver
   let symbols ← parser.getSymbolManager
   let s := "(set-logic QF_LIA)\n(declare-fun a () Bool)\n(declare-fun b () Bool)\n"
@@ -43,8 +41,7 @@ test![TestApiBlackInputParser, setStreamInput] tm => do
   loop ()
   assertTrue (← parser.isDone)
 
-test![TestApiBlackInputParser, setStreamInput'] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, setStreamInput'] tm solver => do
   let parser ← InputParser.new solver
   let symbols ← parser.getSymbolManager
   let s := "(set-logic QF_LIA)\n(declare-fun a () Bool)\n(declare-fun b () Bool)\n"
@@ -59,8 +56,7 @@ test![TestApiBlackInputParser, setStreamInput'] tm => do
   loop ()
   assertTrue (← parser.isDone)
 
-test![TestApiBlackInputParser, setAndAppendIncrementalStringInput] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, setAndAppendIncrementalStringInput] tm solver => do
   let parser ← InputParser.new solver
   let symbols ← parser.getSymbolManager
   parser.setIncrementalStringInput (name := "input_parser_black")
@@ -82,8 +78,7 @@ test![TestApiBlackInputParser, setAndAppendIncrementalStringInput] tm => do
   assertTrue cmd.isNull
   assertTrue (← parser.isDone)
 
-test![TestApiBlackInputParser, setAndAppendIncrementalStringInputInterleave] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, setAndAppendIncrementalStringInputInterleave] tm solver => do
   let parser ← InputParser.new solver
   let symbols ← parser.getSymbolManager
   parser.setIncrementalStringInput (name := "input_parser_black")
@@ -105,14 +100,12 @@ test![TestApiBlackInputParser, setAndAppendIncrementalStringInputInterleave] tm
   assertTrue cmd.isNull
   assertTrue (← parser.isDone)
 
-test![TestApiBlackInputParser, appendIncrementalNoSet] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, appendIncrementalNoSet] tm solver => do
   let parser ← InputParser.new solver
   assertError "Input to parser not initialized" do
     parser.appendIncrementalStringInput "(set-logic ALL)"
 
-test![TestApiBlackInputParser, setStringInput] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, setStringInput] tm solver => do
   let parser ← InputParser.new solver
   let symbols ← parser.getSymbolManager
   parser.setStringInput "(set-logic ALL)" (name := "input_parser_black")
@@ -122,32 +115,28 @@ test![TestApiBlackInputParser, setStringInput] tm => do
   let cmd ← parser.nextCommand
   assertTrue cmd.isNull
 
-test![TestApiBlackInputParser, nextCommandNoInput] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, nextCommandNoInput] tm solver => do
   let parser ← InputParser.new solver
   parser.setStringInput "" (name := "input_parser_black")
   let cmd ← parser.nextCommand
   assertTrue cmd.isNull
 
-test![TestApiBlackInputParser, nextCommandNoIncrementalInput] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, nextCommandNoIncrementalInput] tm solver => do
   let parser ← InputParser.new solver
   parser.setIncrementalStringInput (name := "input_parser_black")
   let cmd ← parser.nextCommand
   assertTrue cmd.isNull
   let term ← parser.nextTerm
   assertTrue term.isNull
 
-test![TestApiBlackInputParser, nextTerm] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, nextTerm] tm solver => do
   let parser ← InputParser.new solver
   assertError "Input to parser not initialized" parser.nextTerm
   parser.setStringInput "" (name := "input_parser_black")
   let term ← parser.nextTerm
   assertTrue term.isNull
 
-test![TestApiBlackInputParser, nextTerm2] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, nextTerm2] tm solver => do
   -- adding a set-logic compared to the original test to silence warnings
   solver.setLogic "ALL"
   let parser ← InputParser.new solver
@@ -166,7 +155,7 @@ test![TestApiBlackInputParser, nextTerm2] tm => do
   parser.appendIncrementalStringInput "(+ a 1)\n"
   let term ← assertOk parser.nextTerm
   assertFalse term.isNull
-  assertEq term.getKind Kind.ADD
+  assertEq (← term.getKind) Kind.ADD
   parser.appendIncrementalStringInput "(+ b 1)\n"
   assertError "Symbol 'b' not declared as a variable" parser.nextTerm
 
@@ -215,8 +204,7 @@ test![TestApiBlackInputParser, setAndAppendIncrementalStringInput] tm => do
     "Logic mismatch when initializing InputParser.\n\
     The solver's logic: QF_LRA\nThe symbol manager's logic: QF_LIA"
 
-test![TestApiBlackInputParser, incrementalSetString] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, incrementalSetString] tm solver => do
   let parser ← InputParser.new solver
   let symbols ← parser.getSymbolManager
   let mut out := ""
@@ -230,8 +218,7 @@ test![TestApiBlackInputParser, incrementalSetString] tm => do
     out := s!"{out}{output}"
   assertEq out ""
 
-test![TestApiBlackInputParser, getDeclaredTermsAndSorts] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackInputParser, getDeclaredTermsAndSorts] tm solver => do
   let parser ← InputParser.new solver
   let symbols ← parser.getSymbolManager
   parser.setIncrementalStringInput (name := "input_parser_black")
@@ -246,4 +233,4 @@ test![TestApiBlackInputParser, getDeclaredTermsAndSorts] tm => do
   let terms ← symbols.getDeclaredTerms
   assertEq sorts.size 1
   assertEq terms.size 1
-  assertEq terms[0]!.getSort sorts[0]!
+  assertEq (← terms[0]!.getSort) sorts[0]!

cvc5Test/Unit/ApiInputParser.lean

@@ -104,21 +104,21 @@ test![TestApiBlackProof, getRewriteRule] tm => do
 
   assertOkDiscard proof.getRewriteRule
 
-test![TestApiBlackProof, getResult] solver => do
-  let proof ← createProof solver
+test![TestApiBlackProof, getResult] tm => do
+  let proof ← createProof tm
   let _ := proof.getResult
 
-test![TestApiBlackProof, getChildren] solver => do
-  let proof ← createProof solver
+test![TestApiBlackProof, getChildren] tm => do
+  let proof ← createProof tm
   let children := proof.getChildren
   assertFalse children.isEmpty
 
-test![TestApiBlackProof, getArguments] solver => do
-  let proof ← createProof solver
+test![TestApiBlackProof, getArguments] tm => do
+  let proof ← createProof tm
   let _ := proof.getArguments
 
-test![TestApiBlackProof, equalhash] solver => do
-  let x ← createProof solver
+test![TestApiBlackProof, equalhash] tm => do
+  let x ← createProof tm
   let kids := x.getChildren
   if h : 0 < kids.size then
     let y := kids[0]

cvc5Test/Unit/ApiProof.lean

@@ -11,10 +11,8 @@ test![TestApiBlackResult, isNull] do
   -- lean API does not expose null results
   assertTrue true
 
-test![TestApiBlackResult, equalHash] tm => do
-  let solver ← Solver.new tm
-  let u ← tm.mkUninterpretedSort "u"
-  let x ← solver.declareFun "x" #[] u
+test![TestApiBlackResult, equalHash] tm solver => do
+  let x ← solver.declareFun "x" #[] uninterpreted
   let x_eq_x ← tm.mkTerm .EQUAL #[x, x]
   solver.assertFormula x_eq_x
   -- skipping null-result-related checks
@@ -32,10 +30,8 @@ test![TestApiBlackResult, equalHash] tm => do
   assertNe res1.hash res3.hash
   assertNe res2.hash res3.hash
 
-test![TestApiBlackResult, isSat] tm => do
-  let solver ← Solver.new tm
-  let u ← tm.mkUninterpretedSort "u"
-  let x ← solver.declareFun "x" #[] u
+test![TestApiBlackResult, isSat] tm solver => do
+  let x ← solver.declareFun "x" #[] uninterpreted
   solver.assertFormula (← tm.mkTerm .EQUAL #[x, x])
   let res ← solver.checkSat
   assertTrue res.isSat
@@ -47,10 +43,8 @@ test![TestApiBlackResult, isSat] tm => do
   assertEq ue.toString "UNKNOWN_REASON"
   assertEq res.getUnknownExplanation? none
 
-test![TestApiBlackResult, isUnsat] tm => do
-  let solver ← Solver.new tm
-  let u ← tm.mkUninterpretedSort "u"
-  let x ← solver.declareFun "x" #[] u
+test![TestApiBlackResult, isUnsat] tm solver => do
+  let x ← solver.declareFun "x" #[] uninterpreted
   solver.assertFormula (← tm.mkTerm .NOT #[← tm.mkTerm .EQUAL #[x, x]])
   let res ← solver.checkSat
   assertFalse res.isSat
@@ -62,13 +56,11 @@ test![TestApiBlackResult, isUnsat] tm => do
   assertEq ue.toString "UNKNOWN_REASON"
   assertEq res.getUnknownExplanation? none
 
-test![TestApiBlackResult, isUnknown] tm => do
-  let solver ← Solver.new tm
+test![TestApiBlackResult, isUnknown] tm solver => do
   solver.setLogic "QF_NIA"
   solver.setOption "incremental" "false"
   solver.setOption "solve-real-as-int" "true"
-  let realSort ← tm.getRealSort
-  let x ← solver.declareFun "x" #[] realSort
+  let x ← solver.declareFun "x" #[] real
   let zero := ← tm.mkReal 0
   let one := ← tm.mkReal 1
   solver.assertFormula (← tm.mkTerm .LT #[zero, x])