Yet another hack to go around CVC4 regb#32

Author: regb

src/it/resources/regression/smtlib/solving/all/define_fun1.smt2

@@ -0,0 +1,10 @@
+(set-option :print-success true)
+(set-logic QF_UF)
+(declare-sort U 0)
+(declare-fun x0 () U)
+(declare-fun y0 () U)
+(define-fun x1 () U x0)
+(define-fun y1 () U y0)
+(assert (not (= x1 y1)))
+(check-sat)
+(exit)

src/it/resources/regression/smtlib/solving/cvc4/define_fun2.smt2

@@ -0,0 +1,8 @@
+(set-option :print-success true)
+(set-logic QF_UF)
+(declare-sort U 0)
+(declare-fun x0 () U)
+(declare-fun y0 () U)
+(define-fun-rec x1 ((z U)) U z)
+(define-fun-rec y1 ((z U)) U z)
+(exit)

src/it/resources/regression/smtlib/solving/cvc4/define_fun2.smt2.want

@@ -0,0 +1,8 @@
+success
+success
+success
+success
+success
+success
+success
+success

src/it/resources/regression/smtlib/solving/cvc4/define_fun3.smt2

@@ -0,0 +1,7 @@
+(set-option :print-success true)
+(set-logic QF_UF)
+(declare-sort U 0)
+(declare-fun x0 () U)
+(declare-fun y0 () U)
+(define-funs-rec ((x1 ((z U)) U)) (z))
+(exit)

src/it/resources/regression/smtlib/solving/cvc4/define_fun3.smt2.want

@@ -0,0 +1,7 @@
+success
+success
+success
+success
+success
+success
+success

src/it/scala/smtlib/it/SmtLibRunnerTests.scala

@@ -19,7 +19,7 @@ import interpreters._
   * Compare the result of running command by command with an interpreter against
   * running the corresponding executable directly on the .smt2 files.
   *
-  * TODO: proper way to display warning when not all tests are run because of not found exectuables
+  * TODO: proper way to display warning when not all tests are run because of not found executables.
   */
 class SmtLibRunnerTests extends FunSuite with TestHelpers {
 
@@ -47,23 +47,41 @@ class SmtLibRunnerTests extends FunSuite with TestHelpers {
   if(isCVC4Available) {
     filesInResourceDir("regression/smtlib/solving/cvc4", _.endsWith(".smt2")).foreach(file => {
       test("With CVC4: SMTLIB benchmark: " + file.getPath) {
-        compareWithInterpreter(executeCVC4)(getCVC4Interpreter, file)
+        compareWithWant(getCVC4Interpreter, file, new File(file.getPath + ".want"))
       }
     })
   }
 
 
   def compareWithInterpreter(executable: (File) => (String => Unit) => Unit)
                             (interpreter: Interpreter, file: File) = {
-
     val lexer = new Lexer(new FileReader(file))
     val parser = new Parser(lexer)
 
     executable(file) { (expected: String) =>
-      val res: String = interpreter.eval(parser.parseCommand).toString
+      val cmd = parser.parseCommand
+      assert(cmd !== null)
+      val res: String = interpreter.eval(cmd).toString
       assert(expected.trim === res.trim)
     }
     assert(parser.parseCommand === null)
   }
 
+  def compareWithWant(interpreter: Interpreter, file: File, want: File) = {
+
+    val lexer = new Lexer(new FileReader(file))
+    val parser = new Parser(lexer)
+
+    for(expected <- scala.io.Source.fromFile(want).getLines) {
+      val cmd = parser.parseCommand
+      assert(cmd !== null)
+      val res: String = interpreter.eval(cmd).toString
+      assert(expected.trim === res.trim)
+    }
+    assert(parser.parseCommand === null)
+    intercept[smtlib.parser.Parser.UnexpectedEOFException] {
+      // There shouldn't be anything left on the interpreter parser (the solver process).
+      interpreter.parser.parseSExpr
+    }
+  }
 }

src/main/scala/smtlib/interpreters/CVC4Interpreter.scala

@@ -14,15 +14,24 @@ class CVC4Interpreter(executable: String, args: Array[String], tailPrinter: Bool
   parser.parseGenResponse
 
   override def parseResponseOf(cmd: SExpr): SExpr = cmd match {
-    case DefineFunsRec(funs, bodies) =>
-      // CVC4 translates definefunsrec in three commands per function,
-      // and thus emits 3x (success)
+    case DefineFunsRec(funs, _) =>
+      // CVC4 translates define-funs-rec in three commands per function,
+      // and thus emits 3x success.
       val res = for (i <- 1 to funs.size*3) yield {
         parser.parseGenResponse
       }
 
       res.find(_ != Success).getOrElse(Success)
 
+    case DefineFunRec(_) =>
+      // CVC4 translates define-fun-rec in three commands,
+      // and thus emits 3x success.
+      val res = for (i <- 1 to 3) yield {
+        parser.parseGenResponse
+      }
+
+      res.find(_ != Success).getOrElse(Success)
+
     case _ =>
       super.parseResponseOf(cmd)
   }