inox-tutorial-log.scala

scala> :paste
// Entering paste mode (ctrl-D to finish)

import inox._
import inox.trees._
import inox.trees.dsl._
import inox.solvers._

// Exiting paste mode, now interpreting.

import inox._
import inox.trees._
import inox.trees.dsl._
import inox.solvers._

scala>

scala> :paste
// Entering paste mode (ctrl-D to finish)

val list: Identifier = FreshIdentifier("List")
val cons: Identifier = FreshIdentifier("Cons")
val nil: Identifier = FreshIdentifier("Nil")

// Exiting paste mode, now interpreting.

list: inox.Identifier = List
cons: inox.Identifier = Cons
nil: inox.Identifier = Nil

scala> :paste
// Entering paste mode (ctrl-D to finish)

val head: Identifier = FreshIdentifier("head")
val tail: Identifier = FreshIdentifier("tail")

// Exiting paste mode, now interpreting.

head: inox.Identifier = head
tail: inox.Identifier = tail

scala> :paste
// Entering paste mode (ctrl-D to finish)

val listSort = mkSort(list)("T")(Seq(cons, nil))
val consConstructor = mkConstructor(cons)("T")(Some(list)) {
  case Seq(tp) => /* `tp` is the type parameter required by the "T" argument to `mkConstructor`. */
    /* We use the previously defined `head` and `tail` identifiers for the fields' symbols.
     * The type `T(list)(tp)` is a shorthand for `ADTType(list, Seq(tp))`. */
    Seq(ValDef(head, tp), ValDef(tail, T(list)(tp)))
}
val nilConstructor = mkConstructor(nil)("T")(Some(list))(tps => Seq.empty)

// Exiting paste mode, now interpreting.

listSort: inox.trees.dsl.trees.ADTSort = abstract class List[T]
consConstructor: inox.trees.dsl.trees.ADTConstructor = case class Cons[T](head: T, tail: List[T]) extends List[T]
nilConstructor: inox.trees.dsl.trees.ADTConstructor = case class Nil[T]() extends List[T]

scala> val size: Identifier = FreshIdentifier("size")
size: inox.Identifier = size

scala>

scala> :paste
// Entering paste mode (ctrl-D to finish)

val sizeFunction = mkFunDef(size)("T") { case Seq(tp) => (
  /* We now define the argument list of the size function.
   * Note that `"ls" :: T(list)(tp)` is a shorthand for the definition
   * `ValDef(FreshIdentifier("ls"), ADTType(list, Seq(tp)))`. */
  Seq("ls" :: T(list)(tp)),
  /* Now comes the return type of the size function (a mathematical integer). */
  IntegerType,
  /* And finally, the body constructor.
   * The function we pass in here will receive instances of `Variable` corresponding
   * to the `ValDef` parameters specified above. */
  { case Seq(ls) =>
    let("res" :: IntegerType, if_ (ls.isInstOf(T(cons)(tp))) {
      E(BigInt(1)) + E(size)(tp)(ls.asInstOf(T(cons)(tp)).getField(tail))
    } else_ {
      E(BigInt(0))
    }) (res => Assume(res >= E(BigInt(0)), res))
  })
}

// Exiting paste mode, now interpreting.

sizeFunction: inox.trees.dsl.trees.FunDef =
def size[T](ls$0: List[T]): BigInt = {
  val res$0: BigInt = if (ls$0.isInstanceOf[Cons[T]]) {
    1 + size[T](ls$0.asInstanceOf[Cons[T]].tail)
  } else {
    0
  }
  assume((res$0 >= 0))
  res$0
}

scala> :paste
// Entering paste mode (ctrl-D to finish)

implicit val symbols = NoSymbols
  .withFunctions(Seq(sizeFunction))
  .withADTs(Seq(listSort, consConstructor, nilConstructor))

// Exiting paste mode, now interpreting.

symbols: inox.trees.Symbols =
abstract class List[T]

case class Cons[T](head: T, tail: List[T]) extends List[T]

case class Nil[T]() extends List[T]

-----------

def size[T](ls$0: List[T]): BigInt = {
  val res$0: BigInt = if (ls$0.isInstanceOf[Cons[T]]) {
    1 + size[T](ls$0.asInstanceOf[Cons[T]].tail)
  } else {
    0
  }
  assume((res$0 >= 0))
  res$0
}

scala> :paste
// Entering paste mode (ctrl-D to finish)

val tp: TypeParameter = TypeParameter.fresh("T")
val ls: Variable = Variable.fresh("ls", T(list)(tp))
val prop = if_ (ls.isInstOf(T(cons)(tp))) {
  E(BigInt(1)) + E(size)(tp)(ls.asInstOf(T(cons)(tp)).getField(tail))
} else_ {
  E(BigInt(0))
}

// Exiting paste mode, now interpreting.

tp: inox.trees.TypeParameter = T
ls: inox.trees.Variable = ls
prop: inox.trees.dsl.trees.IfExpr =
if (ls.isInstanceOf[Cons[T]]) {
  1 + size[T](ls.asInstanceOf[Cons[T]].tail)
} else {
  0
}

scala> :paste
// Entering paste mode (ctrl-D to finish)

val program = InoxProgram(Context.empty, symbols)
val solver = solvers.SolverFactory.default(program).getNewSolver
solver.assertCnstr(Not(prop))
solver.check(SolverResponses.Simple) /* Should return `Unsat` */

// Exiting paste mode, now interpreting.

[Warning ] The Z3 native interface is not available. Falling back onto smt-z3.
inox.solvers.AbstractSolver$SolverUnsupportedError: <untyped>@?:? (of class inox.ast.Types$Untyped$) is unsupported by solver smt-z3:
  Could not transform <untyped> into an SMT sort
  at inox.solvers.AbstractSolver$class.unsupported(Solver.scala:46)
  at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$4$underlying$.unsupported(SolverFactory.scala:158)
  at inox.solvers.smtlib.SMTLIBTarget$class.computeSort(SMTLIBTarget.scala:156)
  at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$4$underlying$.inox$solvers$smtlib$Z3Target$$super$computeSort(SolverFactory.scala:158)
  at inox.solvers.smtlib.Z3Target$class.computeSort(Z3Target.scala:52)
  at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$4$underlying$.computeSort(SolverFactory.scala:158)
  at inox.solvers.smtlib.SMTLIBTarget$$anonfun$declareSort$1.apply(SMTLIBTarget.scala:136)
  at inox.solvers.smtlib.SMTLIBTarget$$anonfun$declareSort$1.apply(SMTLIBTarget.scala:136)
  at inox.utils.Bijection$$anonfun$cachedB$1.apply(Bijection.scala:68)
  at scala.Option.getOrElse(Option.scala:121)
  at inox.utils.Bijection.cachedB(Bijection.scala:67)
  at inox.solvers.smtlib.SMTLIBTarget$class.declareSort(SMTLIBTarget.scala:136)
  at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$4$underlying$.declareSort(SolverFactory.scala:158)
  at inox.solvers.smtlib.SMTLIBTarget$$anonfun$declareVariable$1.apply(SMTLIBTarget.scala:196)
  at inox.solvers.smtlib.SMTLIBTarget$$anonfun$declareVariable$1.apply(SMTLIBTarget.scala:194)
  at inox.utils.Bijection$$anonfun$cachedB$1.apply(Bijection.scala:68)
  at scala.Option.getOrElse(Option.scala:121)
  at inox.utils.Bijection.cachedB(Bijection.scala:67)
  at inox.solvers.smtlib.SMTLIBTarget$class.declareVariable(SMTLIBTarget.scala:194)
  at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$4$underlying$.declareVariable(SolverFactory.scala:158)
  at inox.solvers.smtlib.SMTLIBSolver$$anonfun$assertCnstr$1.apply(SMTLIBSolver.scala:32)
  at inox.solvers.smtlib.SMTLIBSolver$$anonfun$assertCnstr$1.apply(SMTLIBSolver.scala:32)
  at scala.collection.immutable.Set$Set2.foreach(Set.scala:128)
  at inox.solvers.smtlib.SMTLIBSolver$class.assertCnstr(SMTLIBSolver.scala:32)
  at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$4$underlying$.assertCnstr(SolverFactory.scala:158)
  at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$4$underlying$.assertCnstr(SolverFactory.scala:158)
  at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$assertCnstr$1.apply(UnrollingSolver.scala:150)
  at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$assertCnstr$1.apply(UnrollingSolver.scala:149)
  at scala.collection.immutable.List.foreach(List.scala:381)
  at inox.solvers.unrolling.AbstractUnrollingSolver$class.assertCnstr(UnrollingSolver.scala:149)
  at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$4.inox$tip$TipDebugger$$super$assertCnstr(SolverFactory.scala:150)
  at inox.tip.TipDebugger$class.assertCnstr(TipDebugger.scala:52)
  at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$4.assertCnstr(SolverFactory.scala:150)
  at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$4.assertCnstr(SolverFactory.scala:150)
  ... 47 elided

scala>