Skip to content

Commit 16bb7e9

Browse files
committed
Fix GetUnsatAssumptionResponseSuccess tree with props
1 parent 91e7214 commit 16bb7e9

File tree

3 files changed

+17
-14
lines changed

3 files changed

+17
-14
lines changed

src/main/scala/smtlib/parser/ParserCommandsResponses.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -257,8 +257,8 @@ trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserC
257257
peekToken match {
258258
case Tokens.SymbolLit("error") => parseErrorResponse
259259
case t => {
260-
val syms = parseUntil(Tokens.CParen)(parseSymbol _)
261-
GetUnsatAssumptionsResponseSuccess(syms)
260+
val props = parseUntil(Tokens.CParen)(parsePropLit _)
261+
GetUnsatAssumptionsResponseSuccess(props)
262262
}
263263
}
264264
}

src/main/scala/smtlib/printer/PrintingContext.scala

Lines changed: 13 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -112,6 +112,16 @@ class PrintingContext(writer: Writer) {
112112
print(keyword.name)
113113
}
114114

115+
def printPropLit(prop: PropLiteral): Unit = {
116+
if (prop.polarity) {
117+
print(prop.symbol)
118+
} else {
119+
print("(not ")
120+
print(prop.symbol)
121+
print(")")
122+
}
123+
}
124+
115125
private def printTerm(term: Term): Unit = term match {
116126
case Let(vb, vbs, t) =>
117127
print("(let (")
@@ -180,15 +190,7 @@ class PrintingContext(writer: Writer) {
180190

181191
case CheckSatAssuming(props) =>
182192
print("(check-sat-assuming ")
183-
printNary(props, (prop: PropLiteral) => {
184-
if (prop.polarity) {
185-
print(prop.symbol)
186-
} else {
187-
print("(not ")
188-
print(prop.symbol)
189-
print(")")
190-
}
191-
}, "(", " ", ")")
193+
printNary(props, (pl: PropLiteral) => printPropLit(pl), "(", " ", ")")
192194
print(")\n")
193195

194196
case DeclareConst(name, sort) =>
@@ -390,8 +392,8 @@ class PrintingContext(writer: Writer) {
390392
case GetProofResponseSuccess(proof) =>
391393
print(proof)
392394

393-
case GetUnsatAssumptionsResponseSuccess(symbols) =>
394-
printNary(symbols, "(", " ", ")")
395+
case GetUnsatAssumptionsResponseSuccess(props) =>
396+
printNary(props, (pl: PropLiteral) => printPropLit(pl), "(", " ", ")")
395397

396398
case GetUnsatCoreResponseSuccess(symbols) =>
397399
printNary(symbols, "(", " ", ")")

src/main/scala/smtlib/trees/Trees.scala

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -412,6 +412,7 @@ object Commands {
412412

413413
object CommandsResponses {
414414
import Terms._
415+
import Commands.PropLiteral
415416

416417
sealed abstract class CommandResponse extends Positioned with SExpr {
417418
override def toString: String = printer.RecursivePrinter.toString(this)
@@ -497,7 +498,7 @@ object CommandsResponses {
497498
case class GetProofResponseSuccess(proof: SExpr) extends
498499
GetProofResponse with SuccessfulResponse
499500

500-
case class GetUnsatAssumptionsResponseSuccess(symbols: Seq[SSymbol]) extends
501+
case class GetUnsatAssumptionsResponseSuccess(props: Seq[PropLiteral]) extends
501502
GetUnsatAssumptionsResponse with SuccessfulResponse
502503

503504
case class GetUnsatCoreResponseSuccess(symbols: Seq[SSymbol]) extends

0 commit comments

Comments
 (0)