WIP: Symbolic abstraction 2

src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/Interval.scala

@@ -2,6 +2,14 @@ package edu.colorado.plv.cuanto
 package abstracting.tc
 package domains
 
+import smtlib.Interpreter
+import smtlib.parser.Commands.{Command, DeclareConst}
+import smtlib.parser.Terms._
+import smtlib.theories.Core._
+import smtlib.theories.Ints._
+
+import symbolic._
+
 /** A domain representing an integer constrained by an upper and/or
   * lower bound
   *
@@ -45,7 +53,39 @@ package object interval {
     reduce(Btw(g,l))
   }
 
+  case class IntSMT(int1: SSymbol)
+
   object instances {
+    implicit val intSMTSymbol: Symbol[IntSMT] = new Symbol[IntSMT] {
+      override def draw(name: String): (IntSMT,Traversable[Command]) = {
+        val s: SSymbol = SSymbol(name)
+
+        (IntSMT(s),Seq(DeclareConst(s,IntSort())))
+      }
+    }
+
+    implicit val intSMTVal: SMTVal[Int] = new SMTVal[Int] {
+      override def interpret(value: Term): Option[Int] = value match {
+        case NumeralLit(v) => Some(v.intValue())
+        case _ => None
+      }
+    }
+
+    implicit val intModel: Model[Int] {type Schema = IntSMT} = new Model[Int] {
+      override type Schema = IntSMT
+      override def getModel(name: String, i: Interpreter): Option[Int] = {
+        for {
+          intResults <- getModelMap(i)
+          int <- intResults get SSymbol(name)
+        } yield int
+      }
+    }
+
+    implicit val intervalSym: SymAbstract[Interval,IntSMT] =
+      new SymAbstract[Interval,IntSMT] {
+        override def gammaHat(a: Interval): Constraint[IntSMT] = ???
+      }
+
     implicit val latticeInterval: Lattice[Interval] = new Lattice[I] {
       val bot: Interval = Bot
       val top: Interval = Top
@@ -110,4 +150,29 @@ package object interval {
 
   }
 
+  object symbolic {
+    def add(a: Int): Transformer[IntSMT] = {
+      case (IntSMT(i1),IntSMT(i2)) => 
+        Equals(Add(sTerm(i1),NumeralLit(BigInt(a))), sTerm(i2))
+    }
+    def sub(a: Int): Transformer[IntSMT] = {
+      case (IntSMT(i1),IntSMT(i2)) => 
+        Equals(Sub(sTerm(i1),NumeralLit(BigInt(a))), sTerm(i2))
+    }
+  }
+
+  def add(n: Int)(a: Interval): Interval = a match {
+    case Btw(g1,l1) => Btw(g1 + n, l1 + n)
+    case Lte(l) => Lte(l + n)
+    case Gte(g) => Gte(g + n)
+    case i => i // Bottom or Top will remain the same
+  }
+
+  def sub(n: Int)(a: Interval): Interval = a match {
+    case Btw(g1,l1) => Btw(g1 - n, l1 - n)
+    case Lte(l) => Lte(l - n)
+    case Gte(g) => Gte(g - n)
+    case i => i
+  }
+
 }

src/main/scala/edu/colorado/plv/cuanto/abstracting/tc/symbolic/package.scala

@@ -0,0 +1,128 @@
+package edu.colorado.plv.cuanto
+package abstracting.tc
+
+import smtlib.Interpreter
+import smtlib.interpreters.Z3Interpreter
+import smtlib.parser.Commands._
+import smtlib.parser.CommandsResponses.GetModelResponseSuccess
+import smtlib.parser.Terms._
+import smtlib.theories.Core.Not
+
+import Semilattice._
+import Abstraction._
+
+package object symbolic {
+
+  type Constraint[S] = S => Term
+  type Transformer[S] = (S,S) => Term
+
+  trait Symbol[S] {
+    def draw(s: String): (S,Traversable[Command])
+  }
+  object Symbol {
+    def apply[A : Symbol]: Symbol[A] = implicitly[Symbol[A]]
+  }
+
+  /** Create a [[smtlib.parser.terms.Term `Term`]] from a
+    * [[smtlib.parser.terms.SSymbol `SSymbol`]] */
+  val sTerm: SSymbol => QualifiedIdentifier =
+    s => QualifiedIdentifier(SimpleIdentifier(s))
+
+  trait SMTVal[V] {
+    def interpret(value: Term): Option[V]
+  }
+  object SMTVal {
+    def apply[A : SMTVal]: SMTVal[A] = implicitly[SMTVal[A]]
+  }
+
+  trait Model[C] {
+    type Schema
+    def getModel(name: String, interpreter: Interpreter): Option[C]
+  }
+  object Model {
+    def apply[A : Model]: Model[A] = implicitly[Model[A]]
+  }
+
+  def model[C,S : Symbol](
+    name: String, s: Constraint[S]
+  )(
+    implicit iM: Model[C] {type Schema = S}
+  ): Option[C] = {
+    val (schemaVal,decl) = Symbol[S].draw(name)
+    val z3 = Z3Interpreter.buildDefault
+    val assertion = Seq(Assert(s(schemaVal)))
+
+    (decl ++ assertion ++ Seq(CheckSat())).map(z3.eval)
+
+    Model[C].getModel(name, z3)
+  }
+
+  trait SymAbstract[A,S] {
+    def gammaHat(a: A): Constraint[S]
+  }
+  object SymAbstract {
+    def apply[A,S](implicit inst: SymAbstract[A,S]): SymAbstract[A,S] =
+      implicitly[SymAbstract[A,S]]
+  }
+
+  def modelT[C,S : Symbol](
+    t: Transformer[S]
+  )(
+    pre: Constraint[S],
+    post: Constraint[S]
+  )(
+    implicit iM: Model[C] {type Schema = S}
+  ): Option[(C,C)] = {
+    val baseName = "modelT"
+    val preName = baseName + "-pre"
+    val postName = baseName + "-post"
+    val (schemaValPre,declPre) = Symbol[S].draw(preName)
+    val (schemaValPost,declPost) = Symbol[S].draw(postName)
+
+    val z3 = Z3Interpreter.buildDefault
+
+    val assertion = Seq(
+      Assert(pre(schemaValPre)),
+      Assert(post(schemaValPost)),
+      Assert(t(schemaValPre,schemaValPost))
+    )
+
+    (declPre ++ declPost ++ assertion ++ Seq(CheckSat())).map(z3.eval)
+
+    for {
+      mPre <- Model[C].getModel(preName, z3)
+      mPost <- Model[C].getModel(postName, z3)
+    } yield (mPre,mPost)
+  }
+
+  def postHatUp[C,A : Semilattice,S : Symbol](t: Transformer[S])(v: A)(
+    implicit iM: Model[C] {type Schema = S}, iS: SymAbstract[A,S], iA: Abstraction[C,A]
+  ): A = {
+    val notGammaHat = (e: A) => (l: S) => Not(iS.gammaHat(e)(l))
+    def recur(low: A): A =
+      modelT(t)(iS.gammaHat(v),notGammaHat(low)) match {
+        case Some((s1,s2)) => recur(join(low,beta(s2)))
+        case None => low
+      }
+    recur(bot[A])
+  }
+
+  private[this] def comprehend[V : SMTVal](m: List[SExpr]): Map[SSymbol,V] = {
+    val p: (Map[SSymbol,V],SExpr) => Map[SSymbol,V] = {
+      (acc,i) => i match {
+        case DefineFun(FunDef(id,_,_,v)) => SMTVal[V].interpret(v) match {
+          case Some(v) => acc + (id -> v)
+          case None => acc
+        }
+        case _ => acc
+      }
+    }
+    m.foldLeft[Map[SSymbol,V]](Map.empty)(p)
+  }
+
+  def getModelMap[V : SMTVal](i: Interpreter): Option[Map[SSymbol,V]] =
+    i.eval(GetModel()) match {
+      case GetModelResponseSuccess(m) => Some(comprehend(m))
+      case _ => None
+    }
+}

src/test/scala/edu/colorado/plv/cuanto/abstracting/tc/domains/SymbolicIntervalSpec.scala

@@ -0,0 +1,67 @@
+package edu.colorado.plv.cuanto
+package abstracting.tc
+package domains.interval
+
+import smtlib.theories.Core._
+import smtlib.theories.Ints._
+
+import abstracting.tc.symbolic._
+
+import instances._
+
+/**
+  * @author Nicholas V. Lewchenko
+  */
+class SymbolicIntervalSpec extends CuantoSpec {
+
+  val gteSpec: Int => Constraint[IntSMT] =
+    i => { case IntSMT(t) => GreaterThan(sTerm(t),NumeralLit(BigInt(i))) }
+
+  val btwSpec: (Int,Int) => Constraint[IntSMT] = {
+    case (g,l) => {
+      case IntSMT(t) => And(
+        GreaterThan(sTerm(t),NumeralLit(BigInt(g))),
+        LessThan(sTerm(t),NumeralLit(BigInt(l)))
+      )
+    }
+  }
+
+  val modelTests = Table[Constraint[IntSMT],Int => Boolean](
+    "SMT constraint" -> "Int predicate",
+    gteSpec(4) -> { i => i > 4 },
+    btwSpec(1,9) -> { i => i > 1 && i < 9 }
+  )
+
+  val modelInst: Model[Int] {type Schema = IntSMT} = intModel
+
+  "The Int symbolic representation" should "produce models" in {
+    forAll (modelTests) {
+      (smt,p) => model("asdf",smt).map(p) should equal (Some(true))
+    }
+
+    model("asdf",btwSpec(2,1)) should equal (None)
+  }
+
+
+  val addSpec: Int => Transformer[IntSMT] =
+    n => {
+      case (IntSMT(a1),IntSMT(a2)) => Equals(
+        Add(sTerm(a1),NumeralLit(BigInt(n))),
+        sTerm(a2)
+      )
+    }
+
+  val transformerTests = Table[
+    (Transformer[IntSMT],Constraint[IntSMT],Constraint[IntSMT]),
+    ((Int,Int)) => Boolean
+  ](
+    "SMT Transformer and constraints" -> "Int pair predicate",
+    (addSpec(1),gteSpec(1),gteSpec(5)) -> { case ((i1,i2)) => (i1 + 1) == i2 }
+  )
+
+  "The Int symbolic representation" should "produce transformer models" in {
+    forAll (transformerTests) {
+      case ((t,pre,post),p) => modelT(t)(pre,post).map(p) should equal (Some(true))
+    }
+  }
+}