Update tests to new unsat assumptions tree

Author: samarion

src/test/scala/smtlib/parser/CommandsResponsesParserTests.scala

@@ -287,13 +287,15 @@ class CommandsResponsesParserTests extends FunSuite {
       GetUnsatAssumptionsResponseSuccess(Seq()))
   }
 
-  test("get-unsat-assumptions response is a list of symbols") {
+  test("get-unsat-assumptions response is a list of prop literals") {
     assert(Parser.fromString("(x)").parseGetUnsatAssumptionsResponse === 
-      GetUnsatAssumptionsResponseSuccess(Seq(SSymbol("x"))))
-    assert(Parser.fromString("(a c)").parseGetUnsatAssumptionsResponse === 
-      GetUnsatAssumptionsResponseSuccess(Seq(SSymbol("a"), SSymbol("c"))))
-    assert(Parser.fromString("(a b c d)").parseGetUnsatAssumptionsResponse === 
-      GetUnsatAssumptionsResponseSuccess(Seq(SSymbol("a"), SSymbol("b"), SSymbol("c"), SSymbol("d"))))
+      GetUnsatAssumptionsResponseSuccess(Seq(PropLiteral(SSymbol("x"), true))))
+    assert(Parser.fromString("((not a) c)").parseGetUnsatAssumptionsResponse === 
+      GetUnsatAssumptionsResponseSuccess(Seq(PropLiteral(SSymbol("a"), false), PropLiteral(SSymbol("c"), true))))
+    assert(Parser.fromString("(a b (not c) d)").parseGetUnsatAssumptionsResponse === 
+      GetUnsatAssumptionsResponseSuccess(Seq(
+        PropLiteral(SSymbol("a"), true), PropLiteral(SSymbol("b"), true),
+        PropLiteral(SSymbol("c"), false), PropLiteral(SSymbol("d"), true))))
   }
 
   /*

src/test/scala/smtlib/printer/PrinterTests.scala

@@ -450,10 +450,10 @@ It spans a couple lines""")))))
 
     def printGetUnsatAssumptions(res: GetUnsatAssumptionsResponse): String = printer.toString(res)
     def parseGetUnsatAssumptions(in: String): GetUnsatAssumptionsResponse = Parser.fromString(in).parseGetUnsatAssumptionsResponse
-    check(GetUnsatAssumptionsResponseSuccess(Seq(SSymbol("a"))),
+    check(GetUnsatAssumptionsResponseSuccess(Seq(PropLiteral(SSymbol("a"), true))),
           printGetUnsatAssumptions, parseGetUnsatAssumptions)
     check(GetUnsatAssumptionsResponseSuccess(
-            Seq(SSymbol("a"), SSymbol("b"))), 
+            Seq(PropLiteral(SSymbol("a"), true), PropLiteral(SSymbol("b"), false))), 
           printGetUnsatAssumptions, parseGetUnsatAssumptions)
 
     def printGetUnsatCore(res: GetUnsatCoreResponse): String = printer.toString(res)