Commit 89453b91 authored by Anastasiia's avatar Anastasiia

smt model for multiple vars - smtlib bug detected

parent 167b8b23
......@@ -194,13 +194,14 @@ object RelativeErrorPhase extends DaisyPhase with Taylor with ErrorFunctions{
inputValMap: Map[Identifier, Interval],
ctx: Context): Option[Seq[Map[Identifier, Interval]]] = {
val constrs = inputValMap.flatMap(x => {
val constrs = removeDeltasFromMap(inputValMap).flatMap(x => {
val (id, interval) = x
SMTRange.toConstraints(Variable(id), interval)
})
val condition = and(constrs.toSeq :_*)
val solverQuery = And(condition, Equals(zero, bodyReal))
val model = Solver.getModel(solverQuery)
reporter.debug(model)
model match {
case Some(tmp) =>
val exprs: Map[Identifier, Expr] = variablesOf(bodyReal).map(id => {(id -> model.get(id))}).toMap
......
......@@ -135,6 +135,7 @@ abstract class SMTLibSolver(val context: Context) {
commandBuffer.write("\n")
commandBuffer.flush()
System.out.println("CMD: "+cmd)
interpreter.eval(cmd) match {
case err @ ErrorResponse(msg) if !rawOut =>
reporter.warning(s"Unexpected error from $targetName solver: $msg")
......@@ -143,6 +144,7 @@ abstract class SMTLibSolver(val context: Context) {
addError()
err
case res =>
System.out.println(res)
res
}
}
......@@ -216,7 +218,7 @@ abstract class SMTLibSolver(val context: Context) {
emit(cmd) match {
case GetValueResponseSuccess(valuationPairs) =>
System.out.println("Val Pairs: "+valuationPairs)
new Model(valuationPairs.collect {
case (SimpleSymbol(sym), value) if variables.containsB(sym) =>
val id = variables.toA(sym)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment