From 5565ad35587c2dbcdb026db27f04789bffb95213 Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Tue, 31 Oct 2017 18:43:40 +0200 Subject: [PATCH 1/3] Tmp --- src/main/scala/org/kframework/km/rewrite.scala | 3 ++- src/main/scala/org/kframework/km/z3.scala | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/main/scala/org/kframework/km/rewrite.scala b/src/main/scala/org/kframework/km/rewrite.scala index 8f964fe..c6dca9b 100644 --- a/src/main/scala/org/kframework/km/rewrite.scala +++ b/src/main/scala/org/kframework/km/rewrite.scala @@ -11,7 +11,8 @@ class rewrite(val symbols: Seq[Seq[term.Symbol]]) { val z3 = new z3(symbols) - def applyRule(rule: SimpleRewrite, term: SimplePattern): Seq[SimplePattern] = { val cntRename = term.counter + 1 + def applyRule(rule: SimpleRewrite, term: SimplePattern): Seq[SimplePattern] = { + val cntRename = term.counter + 1 // rule: l => r if c lazy val l = rule.l.rename(cntRename) lazy val r = rule.r.rename(cntRename) diff --git a/src/main/scala/org/kframework/km/z3.scala b/src/main/scala/org/kframework/km/z3.scala index 2d368d9..0332f4f 100644 --- a/src/main/scala/org/kframework/km/z3.scala +++ b/src/main/scala/org/kframework/km/z3.scala @@ -87,7 +87,7 @@ class z3(val symbolsSeq: Seq[Seq[term.Symbol]]) { object z3 { // TODO: set proper z3 path - private val z3 = "./z3/bin/z3" // "z3-4.5.0-x64-osx-10.11.6/bin/z3" + private val z3 = "/home/virgil/runtime-verification/z3/build/z3" // "/usr/bin/z3" // "./z3/bin/z3" // "z3-4.5.0-x64-osx-10.11.6/bin/z3" val cmd = Seq(z3, "-smt2", "-in") From b3897acfb264b8d61be2c3a5b92a56011d573a6c Mon Sep 17 00:00:00 2001 From: Virgil Serbanuta Date: Fri, 3 Nov 2017 23:06:07 +0200 Subject: [PATCH 2/3] tmp --- .../kframework/kale/SubstitutionApply.scala | 6 + .../org/kframework/kale/builtin/MAP.scala | 5 +- .../org/kframework/kale/builtin/SET.scala | 5 +- .../org/kframework/kale/context/pattern.scala | 3 +- .../scala/org/kframework/kale/function.scala | 65 +++++++++-- .../org/kframework/kale/highcats/Free.scala | 8 +- .../org/kframework/kale/highcats/UpDown.scala | 10 +- .../kframework/kale/highcats/liftedCats.scala | 10 +- .../org/kframework/kale/matchingLogic.scala | 50 +++++++- .../org/kframework/kale/standard/ac.scala | 4 +- .../kframework/kale/standard/function.scala | 5 +- .../kale/standard/matchingLogic.scala | 35 +++++- .../kale/symbolic/IntegrationTest.scala | 108 ++++++++++++++++++ 13 files changed, 291 insertions(+), 23 deletions(-) create mode 100644 src/test/scala/org/kframework/kale/symbolic/IntegrationTest.scala diff --git a/src/main/scala/org/kframework/kale/SubstitutionApply.scala b/src/main/scala/org/kframework/kale/SubstitutionApply.scala index 6ddcd97..4881621 100644 --- a/src/main/scala/org/kframework/kale/SubstitutionApply.scala +++ b/src/main/scala/org/kframework/kale/SubstitutionApply.scala @@ -1,6 +1,7 @@ package org.kframework.kale import org.kframework.kale.transformer.Unary +import org.kframework.kale.transformer.Unary.Apply object Var { def apply(solver: SubstitutionApply)(v: Variable): Term = solver.substitution.get(v).getOrElse(v) @@ -13,9 +14,14 @@ class SubstitutionApply(val substitution: Substitution)(implicit penv: Environme def ExistsSub(solver: SubstitutionApply)(v: Exists): Term = substitutionMaker(solver.substitution.remove(v.v))(v.p) + def HLPF(solver: SubstitutionApply)(t: FreeNode1): Term = { + t.copy(solver(t._1)) + } + override def processingFunctions = definePartialFunction[Term, this.type]({ case `Variable` => Var.apply _ case Exists => ExistsSub _ + case l: HasLabelPredicateFunction => HLPF _ }) orElse env.unaryProcessingFunctions override def apply(t: Term): Term = { diff --git a/src/main/scala/org/kframework/kale/builtin/MAP.scala b/src/main/scala/org/kframework/kale/builtin/MAP.scala index 2758a62..a216532 100644 --- a/src/main/scala/org/kframework/kale/builtin/MAP.scala +++ b/src/main/scala/org/kframework/kale/builtin/MAP.scala @@ -99,7 +99,10 @@ trait MapMixin extends Mixin { } -case class MapLabel(name: String, indexFunction: Term => Term, identity: Term)(implicit val env: Environment) extends NonPrimitiveMonoidLabel with Constructor { +case class MapLabel(name: String, indexFunction: Term => Term, identity: Term) + (implicit val env: Environment) + extends NonPrimitiveMonoidLabel with Constructor { + override val isPredicate: Option[Boolean] = Some(false) def isIndexable(t: Term) = diff --git a/src/main/scala/org/kframework/kale/builtin/SET.scala b/src/main/scala/org/kframework/kale/builtin/SET.scala index c5b43ac..d000975 100644 --- a/src/main/scala/org/kframework/kale/builtin/SET.scala +++ b/src/main/scala/org/kframework/kale/builtin/SET.scala @@ -4,7 +4,10 @@ import org.kframework.kale._ import scala.collection.{Iterable, Set} -case class SetLabel(name: String, identity: Term)(implicit val env: Environment with BooleanMixin) extends NonPrimitiveMonoidLabel with Constructor { +case class SetLabel(name: String, identity: Term) + (implicit val env: Environment with BooleanMixin) + extends NonPrimitiveMonoidLabel with Constructor { + override val isPredicate: Option[Boolean] = Some(false) override def construct(l: Iterable[Term]): Term = SET(this, l.toSet) diff --git a/src/main/scala/org/kframework/kale/context/pattern.scala b/src/main/scala/org/kframework/kale/context/pattern.scala index febc5e1..e912261 100644 --- a/src/main/scala/org/kframework/kale/context/pattern.scala +++ b/src/main/scala/org/kframework/kale/context/pattern.scala @@ -12,7 +12,8 @@ import scala.collection.Set trait PatternContextMixin extends Mixin { _: Environment with standard.MatchingLogicMixin with HasMatcher with HolesMixin => - case class PatternContextApplicationLabel(name: String)(implicit val env: Environment with standard.MatchingLogicMixin) + case class PatternContextApplicationLabel(name: String) + (implicit val env: Environment with standard.MatchingLogicMixin) extends Context1ApplicationLabel with CluelessRoaring { // val C = env.Variable("GENERIC_CONTEXT_VAR") diff --git a/src/main/scala/org/kframework/kale/function.scala b/src/main/scala/org/kframework/kale/function.scala index 8c168b1..153de7e 100644 --- a/src/main/scala/org/kframework/kale/function.scala +++ b/src/main/scala/org/kframework/kale/function.scala @@ -3,9 +3,6 @@ package org.kframework.kale import cats.Monoid import org.kframework.kale.highcats._ import org.kframework.kale.standard.AssocWithIdList -import org.roaringbitmap.RoaringBitmap - -import scala.annotation.switch trait FunctionLabel extends NodeLabel with CluelessRoaring { val name: String @@ -17,6 +14,12 @@ trait PureFunctionLabel { override lazy val isPredicate = Some(false) } +trait PredicateFunctionLabel { + self: FunctionLabel => + + override lazy val isPredicate = Some(true) +} + trait FunctionLabel0 extends Label0 with FunctionLabel { def f(): Option[Term] @@ -37,6 +40,10 @@ trait FunctionLabel2 extends Label2 with FunctionLabel { override def apply(_1: Term, _2: Term): Term = env.bottomize(_1, _2) { f(_1, _2) getOrElse FreeNode2(this, _1, _2) } + // testing only + def applyBuild(_1: Term, _2: Term): Term = env.bottomize(_1, _2) { + FreeNode2(this, _1, _2) + } } trait FunctionLabel3 extends Label3 with FunctionLabel { @@ -55,7 +62,9 @@ trait FunctionLabel4 extends Label4 with FunctionLabel { } } -case class PrimitiveFunction1[A, R](name: String, aLabel: UpDown[A], rLabel: Up[R], primitiveF: A => R)(implicit val env: Environment) extends FunctionLabel1 with PureFunctionLabel { +case class PrimitiveFunction1[A, R] +(name: String, aLabel: UpDown[A], rLabel: Up[R], primitiveF: A => R) +(implicit val env: Environment) extends FunctionLabel1 with PureFunctionLabel { def f(_1: Term): Option[Term] = _1 match { case aLabel.extract(a) => Some(rLabel.up(primitiveF(a))) case _ => None @@ -67,11 +76,51 @@ object PrimitiveFunction1 { PrimitiveFunction1(name, aLabel, aLabel, f) } -case class PrimitiveFunction2[A, B, R](name: String, aLabel: UpDown[A], bLabel: UpDown[B], rLabel: Up[R], primitiveF: (A, B) => R)(implicit val env: Environment) +case class HasLabelPredicateFunction(name: String, label: Label) + (implicit val env: Environment) + extends FunctionLabel1 with PredicateFunctionLabel { + + def f(_1: Term): Option[Term] = { + if (_1.label.isInstanceOf[VariableLabel]) { + None + } else if (_1.label == label) { + Some(env.Top) + } else _1 match { + case v: SymbolicVariable if v.givenLabel == label => + Some(env.Top) + case _ => + Some(env.Bottom) + } + } +} + +case class PredicateFunction1(functionLabel: FunctionLabel1) + (implicit val env: Environment) + extends FunctionLabel1 with PredicateFunctionLabel { + override def f(_1: Term) = { + if (_1.label.isInstanceOf[VariableLabel]) { + None + } else { + functionLabel.f(_1) + } + } + + override val name = "pred" + functionLabel.name +} + +case class PrimitiveFunction2[A, B, R](name: String, + aLabel: UpDown[A], bLabel: UpDown[B], rLabel: Up[R], + primitiveF: (A, B) => R) + (implicit val env: Environment) extends FunctionLabel2 with PureFunctionLabel { def f(_1: Term, _2: Term): Option[Term] = (_1, _2) match { case (aLabel.extract(a), bLabel.extract(b)) => Some(rLabel.up(primitiveF(a, b))) + case (_: SymbolicVariable, bLabel.extract(_)) + |(aLabel.extract(_), _: SymbolicVariable) + | (_: SymbolicVariable, _: SymbolicVariable) => + val newVar: SymbolicVariable = env.SymbolicVariable.freshVariable(rLabel.label) + Some(env.And(newVar, env.Equality(newVar, FreeNode2(this, _1, _2)))) case _ => None } } @@ -149,10 +198,12 @@ case class PrimitiveMonoid[O: Monoid : UpDown](name: String)(implicit val env: E object PrimitiveFunction2 { - def apply[A, R](name: String, aLabel: UpDown[A], rLabel: Up[R], f: (A, A) => R)(implicit env: Environment): PrimitiveFunction2[A, A, R] = + def apply[A, R](name: String, aLabel: UpDown[A], rLabel: Up[R], f: (A, A) => R) + (implicit env: Environment): PrimitiveFunction2[A, A, R] = PrimitiveFunction2(name, aLabel, aLabel, rLabel, f) - def apply[A](name: String, aLabel: UpDown[A], f: (A, A) => A)(implicit env: Environment): PrimitiveFunction2[A, A, A] = + def apply[A](name: String, aLabel: UpDown[A], f: (A, A) => A) + (implicit env: Environment): PrimitiveFunction2[A, A, A] = PrimitiveFunction2(name, aLabel, aLabel, aLabel, f) } diff --git a/src/main/scala/org/kframework/kale/highcats/Free.scala b/src/main/scala/org/kframework/kale/highcats/Free.scala index 9b7fb8c..be9ac98 100644 --- a/src/main/scala/org/kframework/kale/highcats/Free.scala +++ b/src/main/scala/org/kframework/kale/highcats/Free.scala @@ -4,7 +4,7 @@ import cats._ import cats.implicits._ import cats.{Apply, Eq} import org.kframework.kale.util.LabelNamed -import org.kframework.kale.{Environment, FreeLabel1, FreeLabel2, FreeLabel3, Term} +import org.kframework.kale.{Environment, FreeLabel1, FreeLabel2, FreeLabel3, Label, Term} trait Free { _: Environment => @@ -21,6 +21,8 @@ trait Free { case (a) => a.down[A] map companionObject } override def up(o: R): Term = apply(split(o)) + + override def label: Label = this } def free2[A: UpDown, B: UpDown, R <: Product](companionObject: (A, B) => R) = @@ -35,6 +37,8 @@ trait Free { override def up(o: R) = split(o) match { case (a, b) => apply(a, b) } + + override def label: Label = this } def free3[A: UpDown, B: UpDown, C: UpDown, R <: Product](companionObject: (A, B, C) => R) = @@ -51,6 +55,8 @@ trait Free { case (a, b, c) => apply(a, b, c) } } + + override def label: Label = this } } diff --git a/src/main/scala/org/kframework/kale/highcats/UpDown.scala b/src/main/scala/org/kframework/kale/highcats/UpDown.scala index dffff21..acc3f68 100644 --- a/src/main/scala/org/kframework/kale/highcats/UpDown.scala +++ b/src/main/scala/org/kframework/kale/highcats/UpDown.scala @@ -1,9 +1,10 @@ package org.kframework.kale.highcats -import org.kframework.kale.{LeafLabel, Term} +import org.kframework.kale.{Label, LeafLabel, Term} trait Up[O] { def up(o: O): Term + def label: Label } trait Down[O] { @@ -17,12 +18,17 @@ trait Down[O] { object UpDown { final def apply[O](implicit instance: Up[O]): Up[O] = instance - final def apply[O](f: O => Term): Up[O] = (o: O) => f(o) + final def apply[O](f: O => Term, l: LeafLabel[O]): Up[O] = new Up[O] { + override def up(o: O) = f(o) + override def label: LeafLabel[O] = l + } final implicit def updownFromLeafLabel[O](implicit l: LeafLabel[O]): UpDown[O] = new UpDown[O] { override def down(t: Term) = l.unapply(t) override def up(o: O) = l.apply(o) + + override def label: LeafLabel[O] = l } } diff --git a/src/main/scala/org/kframework/kale/highcats/liftedCats.scala b/src/main/scala/org/kframework/kale/highcats/liftedCats.scala index 9fc024a..915d164 100644 --- a/src/main/scala/org/kframework/kale/highcats/liftedCats.scala +++ b/src/main/scala/org/kframework/kale/highcats/liftedCats.scala @@ -4,7 +4,7 @@ import cats._ import cats.implicits._ import org.kframework.kale.standard.ReferenceLabel import org.kframework.kale.util.LabelNamed -import org.kframework.kale.{Environment, FunctionLabel, FunctionLabel1, Label1, Label2, Mixin, MonoidLabel, PrimitiveFunction1, PrimitiveFunction2, PrimitiveFunction3, PrimitiveMonoid, Term, highcats} +import org.kframework.kale.{Environment, FunctionLabel, FunctionLabel1, Label, Label1, Label2, LeafLabel, Mixin, MonoidLabel, PrimitiveFunction1, PrimitiveFunction2, PrimitiveFunction3, PrimitiveMonoid, Term, highcats} trait Convert[A, B] { def convert(a: A): B @@ -58,16 +58,18 @@ trait LiftedCatsMixin extends Mixin with highcats.Free { implicit def upMonoidLabeled[O[_] : MonoidLabeled : Traverse : Applicative : MonoidK, E: UpDown]: UpDown[O[E]] = new UpDown[O[E]] { val eUpDown = implicitly[UpDown[E]] val fTraverse = implicitly[Traverse[O]] - val label = implicitly[MonoidLabeled[O]].monoidLabel + val mLabel = implicitly[MonoidLabeled[O]].monoidLabel val oMonoid = implicitly[MonoidK[O]].algebra[E] val oApplicative = implicitly[Applicative[O]] + override def label: Label = mLabel + override def up(o: O[E]): Term = { - fTraverse.foldMap(o)(eUpDown.up)(label) + fTraverse.foldMap(o)(eUpDown.up)(mLabel) } override def down(t: Term): Option[O[E]] = t match { - case label.iterable(seq: Iterable[Term]) => + case mLabel.iterable(seq: Iterable[Term]) => def ff(t: Term) = oApplicative.pure(eUpDown.down(t).get) Some(implicitly[Traverse[scala.List]].foldMap(seq.toList)(ff)(oMonoid)) diff --git a/src/main/scala/org/kframework/kale/matchingLogic.scala b/src/main/scala/org/kframework/kale/matchingLogic.scala index c96647e..e8fa8cd 100644 --- a/src/main/scala/org/kframework/kale/matchingLogic.scala +++ b/src/main/scala/org/kframework/kale/matchingLogic.scala @@ -1,6 +1,6 @@ package org.kframework.kale -import org.kframework.kale.standard.{MightBeSolved} +import org.kframework.kale.standard.MightBeSolved import org.kframework.kore.implementation.DefaultBuilders import org.kframework.{kale, kore} @@ -15,6 +15,7 @@ trait MatchingLogicMixin extends Mixin { // Labels val Variable: VariableLabel + val SymbolicVariable: SymbolicVariableLabel val And: AndLabel val Or: OrLabel val Rewrite: RewriteLabel @@ -79,6 +80,28 @@ trait VariableLabel extends LeafLabel[(Name, Sort)] { def apply(name: kale.Name): Variable = apply((name, standard.Sort.K)) } +trait SymbolicVariableLabel extends LeafLabel[(Name, Sort, Label)] { + def apply(name: String, givenLabel: Label): SymbolicVariable = + apply((standard.Name(name), standard.Sort.K, givenLabel)) + + def apply(name: String, sort: kale.Sort, givenLabel: Label): SymbolicVariable = + apply((standard.Name(name), sort, givenLabel)) + + def apply(v: (Name, Sort, Label)): SymbolicVariable + + def apply(name: kale.Name, givenLabel: Label): SymbolicVariable = + apply((name, standard.Sort.K, givenLabel)) + + private var counter = 0 + + def freshVariable(givenLabel: Label): SymbolicVariable = { + counter += 1 + generatedVariable(givenLabel, counter) + } + + def generatedVariable(givenLabel: Label, count: Int): SymbolicVariable +} + trait Name extends kore.Name { override def toString = str } @@ -108,6 +131,31 @@ trait Variable extends Leaf[(Name, Sort)] with kore.SortedVariable { override val variables: Set[Variable] = Set(this) } +trait SymbolicVariable extends Leaf[(Name, Sort, Label)] { + val name: Name + val givenLabel: Label // TODO: Should use the sort instead. + + val label: SymbolicVariableLabel + override val isGround = true + override val sort: Sort + override lazy val data: (Name, Sort, Label) = (name, sort, givenLabel) + override lazy val isPredicate: Boolean = false + + override def toString: String = name.str + ( + if (sort.name == "K") + "" + else + ":" + sort.name + ) + ":" + givenLabel.name + + override def canEqual(o: Any): Boolean = o.isInstanceOf[SymbolicVariable] + + override def equals(o: Any): Boolean = o match { + case v: SymbolicVariable => v.name == this.name + case _ => false + } +} + trait TruthLabel extends LeafLabel[Boolean] { override protected[this] def internalInterpret(s: String): Boolean = s.toBoolean } diff --git a/src/main/scala/org/kframework/kale/standard/ac.scala b/src/main/scala/org/kframework/kale/standard/ac.scala index e8caa07..4336759 100644 --- a/src/main/scala/org/kframework/kale/standard/ac.scala +++ b/src/main/scala/org/kframework/kale/standard/ac.scala @@ -141,7 +141,9 @@ case class CollectionSize(collectionLabel: CollectionLabel)(implicit env: Enviro override val isPredicate: Option[Boolean] = Some(false) } -private[standard] class MonoidListLabel(val name: String, val identity: Term)(implicit val env: Environment with IntMixin) extends NonPrimitiveMonoidLabel with Constructor { +private[standard] class MonoidListLabel(val name: String, val identity: Term) + (implicit val env: Environment with IntMixin) + extends NonPrimitiveMonoidLabel with Constructor { val size = CollectionSize(this) diff --git a/src/main/scala/org/kframework/kale/standard/function.scala b/src/main/scala/org/kframework/kale/standard/function.scala index be4721b..f2e141c 100644 --- a/src/main/scala/org/kframework/kale/standard/function.scala +++ b/src/main/scala/org/kframework/kale/standard/function.scala @@ -83,7 +83,10 @@ trait FunctionDefinedByRewriting extends FunctionLabel with PureFunctionLabel wi } } -case class FunctionDefinedByRewritingLabel0(name: String)(implicit val env: StandardEnvironment) extends FunctionDefinedByRewriting with FunctionLabel0 { +case class FunctionDefinedByRewritingLabel0(name: String) + (implicit val env: StandardEnvironment) + extends FunctionDefinedByRewriting with FunctionLabel0 { + def f(): Option[Term] = tryToApply(FreeNode0(this)) } diff --git a/src/main/scala/org/kframework/kale/standard/matchingLogic.scala b/src/main/scala/org/kframework/kale/standard/matchingLogic.scala index c346c8c..00e6117 100644 --- a/src/main/scala/org/kframework/kale/standard/matchingLogic.scala +++ b/src/main/scala/org/kframework/kale/standard/matchingLogic.scala @@ -21,6 +21,7 @@ trait MatchingLogicMixin extends Mixin { override val Or: DNFOrLabel = DNFOrLabel() override val Not: NotLabel = NotLabel() override val Variable: StandardVariableLabel = standard.StandardVariableLabel() + override val SymbolicVariable: StandardSymbolicVariableLabel = standard.StandardSymbolicVariableLabel() override val Equality: EqualityLabel = standard.StandardEqualityLabel() override val Exists: ExistsLabel = standard.SimpleExistsLabel() @@ -203,13 +204,40 @@ private[standard] case class StandardVariableLabel()(implicit override val env: override val isPredicate: Option[Boolean] = Some(false) } +private[standard] case class StandardSymbolicVariableLabel()(implicit override val env: Environment) + extends LabelNamed("#SymbolicVariable") with SymbolicVariableLabel with CluelessRoaring { // TODO: Is is really CluelessRoaring? + override def apply(nameSortLabel: (kale.Name, kale.Sort, Label)): SymbolicVariable = + StandardSymbolicVariable(nameSortLabel._1, nameSortLabel._2, nameSortLabel._3) + + override protected[this] def internalInterpret(s: String): (kale.Name, kale.Sort, Label) = ??? + + override def generatedVariable(givenLabel: Label, counter: Int): SymbolicVariable = { + this ((Name("_" + counter), Sort("K"), givenLabel)) + } + + override val isPredicate: Option[Boolean] = Some(false) +} + private[standard] case class StandardVariable(name: kale.Name, givenSort: kale.Sort)(implicit env: Environment) extends Variable with kore.Variable { override lazy val sort = givenSort val label = env.Variable } -private[standard] case class StandardTruthLabel()(implicit val env: Environment) extends NameFromObject with TruthLabel with RoaringLabelsFromTerm { +private[standard] case class StandardSymbolicVariable(override val name: kale.Name, + givenSort: kale.Sort, + override val givenLabel: Label) + (implicit env: Environment) + extends SymbolicVariable with kore.Variable { + + override lazy val sort: kale.Sort = givenSort + override val label: SymbolicVariableLabel = env.SymbolicVariable +} + +private[standard] case class StandardTruthLabel() + (implicit val env: Environment) + extends NameFromObject with TruthLabel with RoaringLabelsFromTerm { + def apply(v: Boolean) = if (v) env.Top else env.Bottom override val isPredicate: Option[Boolean] = Some(true) @@ -291,7 +319,8 @@ private[kale] class Matches(val _1: Term, val _2: Term)(implicit env: StandardEn val label = env.Match } -private[standard] case class StandardEqualityLabel()(implicit override val env: Environment with MatchingLogicMixin) extends LabelNamed("=") with EqualityLabel { +private[standard] case class StandardEqualityLabel()(implicit override val env: Environment with MatchingLogicMixin) + extends LabelNamed("=") with EqualityLabel { override def apply(_1: Term, _2: Term): Term = { val lhsOrElements = env.Or.asSet(_1) val rhsOrElements = env.Or.asSet(_2) @@ -307,7 +336,7 @@ private[standard] case class StandardEqualityLabel()(implicit override val env: if (_1 == _2) env.Top else if (_1.isGround && _2.isGround) { - if (env.isSealed) { + if (env.isSealed && !_1.isInstanceOf[SymbolicVariable] && !_2.isInstanceOf[SymbolicVariable]) { env.And.onlyPredicate(env.unify(_1, _2)) } else new Equals(_1, _2) diff --git a/src/test/scala/org/kframework/kale/symbolic/IntegrationTest.scala b/src/test/scala/org/kframework/kale/symbolic/IntegrationTest.scala new file mode 100644 index 0000000..6001ec5 --- /dev/null +++ b/src/test/scala/org/kframework/kale/symbolic/IntegrationTest.scala @@ -0,0 +1,108 @@ +package org.kframework.kale.symbolic + +import org.kframework.kale.standard.{NotLabel, StandardEnvironment, StandardSymbolicVariable} +import org.kframework.kale.{AndLabel, EqualityLabel, FreeNode1, HasLabelPredicateFunction, IMPCommonSignature, NonPrimitiveMonoidLabel, RewriteLabel, Rewriter, SymbolicVariableLabel, Term, VariableLabel} +import org.scalatest.{FlatSpec, Matchers} + +class IntegrationTest extends FlatSpec with Matchers { + private val env : StandardEnvironment = StandardEnvironment() + private val signature = new IMPCommonSignature()(env) + import signature._ + + private val Rewrite: RewriteLabel = env.Rewrite + private val And: AndLabel = env.And + private val Not: NotLabel = env.Not + private val Equality: EqualityLabel = env.Equality + + private val INT = env.INT + private val Variable: VariableLabel = env.Variable + private val SymbolicVariable: SymbolicVariableLabel = env.SymbolicVariable + + private val isIntLabel: HasLabelPredicateFunction = HasLabelPredicateFunction("is" + INT.Int, INT.Int)(env) + private val isInt = (x:Term) => FreeNode1(isIntLabel, x) + + private val SymbI = SymbolicVariable("I", INT.Int) + private val I1 = Variable("I1") + private val I2 = Variable("I2") + private val S = Variable("S") + private val R = Variable("R") + private val kseq: NonPrimitiveMonoidLabel = env.AssocWithIdLabel("_~>_", emptyk()) + + "Rewriting" should "match label predicate functions" in { + + + val rules: Set[Term] = Set( + T(k(kseq( + Rewrite( + plus(And(I1, isInt(I1)), And(I2, isInt(I2))), + INT.plus(I1, I2)), + R)), S) + ) map (t => Rewrite(lhs(t), rhs(t))) + + env.seal() + + val rewrite = Rewriter(env)(rules) + + val term = T(k(kseq(plus(INT.Int(1), INT.Int(2)))), state(statesMap())) + + val result = rewrite.searchStep(term) + result should equal (T(k(kseq(INT.Int(3))), state(statesMap()))) + } + + "Rewriting" should "use functions over variables." in { + val rules: Set[Term] = Set( + T(k(kseq( + Rewrite( + plus(And(I1, isInt(I1)), And(I2, isInt(I2))), + INT.plus(I1, I2)), + R)), S) + ) map (t => Rewrite(lhs(t), rhs(t))) + + env.seal() + + val rewrite = Rewriter(env)(rules) + + val term = T(k(kseq(plus(INT.Int(1), SymbI))), state(statesMap())) + + val result = rewrite.searchStep(term) + val v1 = SymbolicVariable.generatedVariable(INT.Int, 1) + val equalPred = Equality(v1, INT.plus.applyBuild(INT.Int(1), SymbI)) + // result should equal (And(T(k(kseq(v1)), state(statesMap())), equalPred) + result should equal (T(k(kseq(And(v1, equalPred))), state(statesMap()))) + } + + "Rewriting" should "evaluate complex expressions with variables." in { + + val rules: Set[Term] = Set( + /* + T(k(kseq( + Rewrite( + plus(And(I1, isInt(I1)), And(I2, isInt(I2))), + INT.plus(I1, I2)), + R)), S), + */ + T(k(kseq( + Rewrite( + plus(And(I1, isInt(I1)), And(I2, Not(isInt(I2)))), + kseq(I2, plus(I1, env.Hole))), + R)), S), + /* + T(k(kseq( + Rewrite( + kseq(And(I2, isInt(I2)), plus(I1, env.Hole)), + kseq(plus(I1, I2))), + R)), S), + */ + ) map (t => Rewrite(lhs(t), rhs(t))) + + env.seal() + + val rewrite = Rewriter(env)(rules) + + val term = T(k(kseq(plus(INT.Int(1), plus(INT.Int(1), And(SymbI, isInt(SymbI)))))), state(statesMap())) + // statesMap( + + val result = rewrite.searchStep(term) + result should equal (And(T(k(kseq(INT.plus(INT.Int(1), SymbI))), state(statesMap())), isInt(SymbI))) + } +} From 7cfde37596034e60a8697ade4b2e4a4ea3a93d03 Mon Sep 17 00:00:00 2001 From: cos Date: Sun, 5 Nov 2017 12:24:41 -0600 Subject: [PATCH 3/3] using regular Variables --- .../kale/standard/matchingLogic.scala | 8 ++- .../kale/symbolic/IntegrationTest.scala | 64 +++++++++++++------ 2 files changed, 50 insertions(+), 22 deletions(-) diff --git a/src/main/scala/org/kframework/kale/standard/matchingLogic.scala b/src/main/scala/org/kframework/kale/standard/matchingLogic.scala index 00e6117..8902607 100644 --- a/src/main/scala/org/kframework/kale/standard/matchingLogic.scala +++ b/src/main/scala/org/kframework/kale/standard/matchingLogic.scala @@ -196,16 +196,18 @@ private[standard] case class StandardVariableLabel()(implicit override val env: var counter = 0 - def freshVariable() = { + def freshVariable(): Variable = freshVariable(Sort.K) + + def freshVariable(sort: Sort): Variable = { counter += 1 - this ((Name("_" + counter), Sort("K"))) + this ((Name("_" + counter), sort)) } override val isPredicate: Option[Boolean] = Some(false) } private[standard] case class StandardSymbolicVariableLabel()(implicit override val env: Environment) - extends LabelNamed("#SymbolicVariable") with SymbolicVariableLabel with CluelessRoaring { // TODO: Is is really CluelessRoaring? + extends LabelNamed("#SymbolicVariable") with SymbolicVariableLabel with CluelessRoaring { // TODO: Is is really CluelessRoaring? override def apply(nameSortLabel: (kale.Name, kale.Sort, Label)): SymbolicVariable = StandardSymbolicVariable(nameSortLabel._1, nameSortLabel._2, nameSortLabel._3) diff --git a/src/test/scala/org/kframework/kale/symbolic/IntegrationTest.scala b/src/test/scala/org/kframework/kale/symbolic/IntegrationTest.scala index 6001ec5..daa5408 100644 --- a/src/test/scala/org/kframework/kale/symbolic/IntegrationTest.scala +++ b/src/test/scala/org/kframework/kale/symbolic/IntegrationTest.scala @@ -1,12 +1,37 @@ package org.kframework.kale.symbolic -import org.kframework.kale.standard.{NotLabel, StandardEnvironment, StandardSymbolicVariable} -import org.kframework.kale.{AndLabel, EqualityLabel, FreeNode1, HasLabelPredicateFunction, IMPCommonSignature, NonPrimitiveMonoidLabel, RewriteLabel, Rewriter, SymbolicVariableLabel, Term, VariableLabel} +import org.kframework.kale +import org.kframework.kale.standard.{NotLabel, Sort, StandardEnvironment, StandardSymbolicVariable} +import org.kframework.kale.{AndLabel, Environment, EqualityLabel, FreeNode1, HasLabelPredicateFunction, IMPCommonSignature, Label, NonPrimitiveMonoidLabel, RewriteLabel, Rewriter, SymbolicVariableLabel, Term, VariableLabel} import org.scalatest.{FlatSpec, Matchers} +import scala.collection.Seq + class IntegrationTest extends FlatSpec with Matchers { - private val env : StandardEnvironment = StandardEnvironment() + + val intSort = Sort("Int") + + trait ABitOfSortingSortingMixin extends Environment { + def sort(l: Label, children: Seq[Term]): kale.Sort = sort(l) + + def sort(l: Label): Sort = l match { + case INT.Int => intSort + case INT.plus => intSort + case plus => intSort + case _ => Sort.Top + } + + override def isSort(left: org.kframework.kore.Sort, term: Term): Boolean = + if (left == Sort.Top) { + true + } else { + term.sort == left + } + } + + private val env: StandardEnvironment = new StandardEnvironment with ABitOfSortingSortingMixin private val signature = new IMPCommonSignature()(env) + import signature._ private val Rewrite: RewriteLabel = env.Rewrite @@ -15,15 +40,11 @@ class IntegrationTest extends FlatSpec with Matchers { private val Equality: EqualityLabel = env.Equality private val INT = env.INT - private val Variable: VariableLabel = env.Variable - private val SymbolicVariable: SymbolicVariableLabel = env.SymbolicVariable - - private val isIntLabel: HasLabelPredicateFunction = HasLabelPredicateFunction("is" + INT.Int, INT.Int)(env) - private val isInt = (x:Term) => FreeNode1(isIntLabel, x) + private val Variable = env.Variable - private val SymbI = SymbolicVariable("I", INT.Int) - private val I1 = Variable("I1") - private val I2 = Variable("I2") + private val SymbI = Variable("I", intSort) + private val I1 = Variable("I1", intSort) + private val I2 = Variable("I2", intSort) private val S = Variable("S") private val R = Variable("R") private val kseq: NonPrimitiveMonoidLabel = env.AssocWithIdLabel("_~>_", emptyk()) @@ -34,7 +55,7 @@ class IntegrationTest extends FlatSpec with Matchers { val rules: Set[Term] = Set( T(k(kseq( Rewrite( - plus(And(I1, isInt(I1)), And(I2, isInt(I2))), + plus(I1, I2), INT.plus(I1, I2)), R)), S) ) map (t => Rewrite(lhs(t), rhs(t))) @@ -46,14 +67,14 @@ class IntegrationTest extends FlatSpec with Matchers { val term = T(k(kseq(plus(INT.Int(1), INT.Int(2)))), state(statesMap())) val result = rewrite.searchStep(term) - result should equal (T(k(kseq(INT.Int(3))), state(statesMap()))) + result should equal(T(k(kseq(INT.Int(3))), state(statesMap()))) } "Rewriting" should "use functions over variables." in { val rules: Set[Term] = Set( T(k(kseq( Rewrite( - plus(And(I1, isInt(I1)), And(I2, isInt(I2))), + plus(I1, I2), INT.plus(I1, I2)), R)), S) ) map (t => Rewrite(lhs(t), rhs(t))) @@ -65,10 +86,11 @@ class IntegrationTest extends FlatSpec with Matchers { val term = T(k(kseq(plus(INT.Int(1), SymbI))), state(statesMap())) val result = rewrite.searchStep(term) - val v1 = SymbolicVariable.generatedVariable(INT.Int, 1) + val v1 = Variable.freshVariable(intSort) val equalPred = Equality(v1, INT.plus.applyBuild(INT.Int(1), SymbI)) // result should equal (And(T(k(kseq(v1)), state(statesMap())), equalPred) - result should equal (T(k(kseq(And(v1, equalPred))), state(statesMap()))) +// result should equal(T(k(kseq(And(v1, equalPred))), state(statesMap()))) + result should equal(T(k(INT.plus(INT.Int(1), SymbI)), state(statesMap()))) } "Rewriting" should "evaluate complex expressions with variables." in { @@ -83,7 +105,7 @@ class IntegrationTest extends FlatSpec with Matchers { */ T(k(kseq( Rewrite( - plus(And(I1, isInt(I1)), And(I2, Not(isInt(I2)))), + plus(I1, I2), kseq(I2, plus(I1, env.Hole))), R)), S), /* @@ -99,10 +121,14 @@ class IntegrationTest extends FlatSpec with Matchers { val rewrite = Rewriter(env)(rules) - val term = T(k(kseq(plus(INT.Int(1), plus(INT.Int(1), And(SymbI, isInt(SymbI)))))), state(statesMap())) + val term = T(k(kseq(plus(INT.Int(1), plus(INT.Int(1), SymbI)))), state(statesMap())) // statesMap( val result = rewrite.searchStep(term) - result should equal (And(T(k(kseq(INT.plus(INT.Int(1), SymbI))), state(statesMap())), isInt(SymbI))) + // all rules have an implicit forall for all variables wrapping the entire rule + // as many variables get bounded, most of the forall dissapear + // as the Hole is free, the forall remains and is lowered to the smallest context + // hm, not sure if forall is correct here or we should wrap it explicitly into an exists, or maybe leave it free + result should equal(T(k(kseq(plus(INT.Int(1), SymbI), plus(INT.Int(1), env.ForAll(env.Hole, env.Hole)))), state(statesMap()))) } }