Skip to content
Snippets Groups Projects
Commit 3c4ef122 authored by Ali Sinan Köksal's avatar Ali Sinan Köksal
Browse files

ternary terms and increase stack size for runner script

parent dae2666c
No related branches found
No related tags found
No related merge requests found
...@@ -40,9 +40,10 @@ object FirstClassConstraints { ...@@ -40,9 +40,10 @@ object FirstClassConstraints {
val f5 = ((x : Int, y : Int) => x + y) compose0 ((x : Int) => x + 42) compose1 ((x: Int) => x + 43) val f5 = ((x : Int, y : Int) => x + y) compose0 ((x : Int) => x + 42) compose1 ((x: Int) => x + 43)
println("Composed f5: " + f5.expr) println("Composed f5: " + f5.expr)
// println("has size 3: " + hasSize(3).expr) // println("has size 5: " + hasSize(5).expr)
for (s <- hasSize(3).findAll) println(hasSize(5).solve)
println(s) // for (s <- hasSize(3).findAll)
// println(s)
} }
} }
#!/bin/bash #!/bin/bash
LD_LIBRARY_PATH=lib-bin \ LD_LIBRARY_PATH=lib-bin \
JAVA_OPTS="-Xmx512M -Xms512M -Xss256M" \
scala -classpath bin/purescala/purescala-definitions_2.8.1-1.0.jar:lib/z3.jar:bin/cp/constraint-programming-plugin_2.8.1-1.0.jar:out ${@} scala -classpath bin/purescala/purescala-definitions_2.8.1-1.0.jar:lib/z3.jar:bin/cp/constraint-programming-plugin_2.8.1-1.0.jar:out ${@}
...@@ -44,11 +44,6 @@ trait CodeGeneration { ...@@ -44,11 +44,6 @@ trait CodeGeneration {
private lazy val skipCounterFunction = definitions.getMember(runtimeMethodsModule, "skipCounter") private lazy val skipCounterFunction = definitions.getMember(runtimeMethodsModule, "skipCounter")
private lazy val copySettingsFunction = definitions.getMember(runtimeMethodsModule, "copySettings") private lazy val copySettingsFunction = definitions.getMember(runtimeMethodsModule, "copySettings")
private lazy val termModules = List(
definitions.getModule("cp.Terms.Term1"),
definitions.getModule("cp.Terms.Term2")
)
private lazy val converterClass = definitions.getClass("cp.Converter") private lazy val converterClass = definitions.getClass("cp.Converter")
private lazy val serializationModule = definitions.getModule("cp.Serialization") private lazy val serializationModule = definitions.getModule("cp.Serialization")
...@@ -79,6 +74,8 @@ trait CodeGeneration { ...@@ -79,6 +74,8 @@ trait CodeGeneration {
private lazy val andClass = definitions.getClass("purescala.Trees.And") private lazy val andClass = definitions.getClass("purescala.Trees.And")
private lazy val equalsClass = definitions.getClass("purescala.Trees.Equals") private lazy val equalsClass = definitions.getClass("purescala.Trees.Equals")
private def termModules(arity : Int) = definitions.getModule("cp.Terms.Term" + arity)
class CodeGenerator(unit : CompilationUnit, owner : Symbol, defaultPos : Position) { class CodeGenerator(unit : CompilationUnit, owner : Symbol, defaultPos : Position) {
private def newSerialized(serialized : Serialized) : Tree = { private def newSerialized(serialized : Serialized) : Tree = {
...@@ -233,7 +230,7 @@ trait CodeGeneration { ...@@ -233,7 +230,7 @@ trait CodeGeneration {
} }
def newBaseTerm(exprToScalaSym : Symbol, serializedProg : Serialized, serializedInputVarList : Serialized, serializedOutputVars : Serialized, serializedExpr : Serialized, inputVarValues : Tree, arity : Int) : Tree = { def newBaseTerm(exprToScalaSym : Symbol, serializedProg : Serialized, serializedInputVarList : Serialized, serializedOutputVars : Serialized, serializedExpr : Serialized, inputVarValues : Tree, arity : Int) : Tree = {
termModules(arity-1) APPLY ( termModules(arity) APPLY (
newConverter(exprToScalaSym), newConverter(exprToScalaSym),
newSerialized(serializedProg), newSerialized(serializedProg),
newSerialized(serializedInputVarList), newSerialized(serializedInputVarList),
......
...@@ -73,6 +73,21 @@ object Terms { ...@@ -73,6 +73,21 @@ object Terms {
def compose1[A](other : Term1[A, T2]) : Term2[T1,A,R] = compose_1_1_2(other, this) def compose1[A](other : Term1[A, T2]) : Term2[T1,A,R] = compose_1_1_2(other, this)
} }
/** Terms with three arguments */
sealed trait Term3[T1,T2,T3,R] extends Term[(T1,T2,T3),R] {
val convertingFunction = converterOf(this).exprSeq2scala3[T1,T2,T3] _
type t2c = (Term3[T1,T2,T3,R]) => Term3[T1,T2,T3,Boolean]
def minimizing(minFunc : IntTerm3[T1,T2,T3])(implicit asConstraint: t2c) : MinConstraint3[T1,T2,T3] =
MinConstraint3[T1,T2,T3](asConstraint(this), minFunc)
def ||(other : Constraint3[T1,T2,T3])(implicit asConstraint: t2c) : Constraint3[T1,T2,T3] = OrConstraint3[T1,T2,T3](this, other)
def &&(other : Constraint3[T1,T2,T3])(implicit asConstraint: t2c) : Constraint3[T1,T2,T3] = AndConstraint3[T1,T2,T3](this, other)
def unary_!(implicit asConstraint: t2c) : Constraint3[T1,T2,T3] = NotConstraint3[T1,T2,T3](this)
}
/* this is for Constraint2[A,B] /* this is for Constraint2[A,B]
def proj0 : Constraint1[A] = this.asInstanceOf[Constraint] match { def proj0 : Constraint1[A] = this.asInstanceOf[Constraint] match {
case BaseTerm(conv,pr,ex,ts) => { case BaseTerm(conv,pr,ex,ts) => {
...@@ -126,10 +141,21 @@ object Terms { ...@@ -126,10 +141,21 @@ object Terms {
new Term[(T1,T2),R](program, expr, types, converter) with Term2[T1,T2,R] new Term[(T1,T2),R](program, expr, types, converter) with Term2[T1,T2,R]
} }
object Term3 {
def apply[T1,T2,T3,R](conv : Converter, serializedProg : Serialized, serializedInputVars : Serialized, serializedOutputVars : Serialized, serializedExpr : Serialized, inputVarValues : Seq[Expr]) = {
val (converter, program, expr, types) = Term.processArgs(conv, serializedProg, serializedInputVars, serializedOutputVars, serializedExpr, inputVarValues)
new Term[(T1,T2,T3),R](program, expr, types, converter) with Term3[T1,T2,T3,R]
}
def apply[T1,T2,T3,R](program : Program, expr : Expr, types : Seq[TypeTree], converter : Converter) =
new Term[(T1,T2,T3),R](program, expr, types, converter) with Term3[T1,T2,T3,R]
}
/** A constraint is just a term with Boolean range */ /** A constraint is just a term with Boolean range */
type Constraint[T] = Term[T,Boolean] type Constraint[T] = Term[T,Boolean]
type Constraint1[T1] = Term1[T1,Boolean] type Constraint1[T1] = Term1[T1,Boolean]
type Constraint2[T1,T2] = Term2[T1,T2,Boolean] type Constraint2[T1,T2] = Term2[T1,T2,Boolean]
type Constraint3[T1,T2,T3] = Term3[T1,T2,T3,Boolean]
object OrConstraint1 { object OrConstraint1 {
def apply[A](l : Constraint[A], r : Constraint[A]) : Constraint1[A] = (l, r) match { def apply[A](l : Constraint[A], r : Constraint[A]) : Constraint1[A] = (l, r) match {
...@@ -151,6 +177,16 @@ object Terms { ...@@ -151,6 +177,16 @@ object Terms {
} }
} }
object OrConstraint3 {
def apply[A,B,C](l : Constraint[(A,B,C)], r : Constraint[(A,B,C)]) : Constraint3[A,B,C] = (l, r) match {
case (Term(p1,ex1,ts1,conv1), Term(p2,ex2,ts2,conv2)) => Term3(p1,Or(ex1,ex2),ts1,conv1)
}
def apply[A,B,C](cs : Seq[Constraint[(A,B,C)]]) : Constraint3[A,B,C] = cs match {
case s @ Seq(Term(p,ex,ts,conv), _*) => Term3(p, Or(s.map(_.expr)), ts, conv)
}
}
object AndConstraint1 { object AndConstraint1 {
def apply[A](l : Constraint[A], r : Constraint[A]) : Constraint1[A] = (l, r) match { def apply[A](l : Constraint[A], r : Constraint[A]) : Constraint1[A] = (l, r) match {
case (Term(p1,ex1,ts1,conv1), Term(p2,ex2,ts2,conv2)) => Term1(p1,And(ex1,ex2),ts1,conv1) case (Term(p1,ex1,ts1,conv1), Term(p2,ex2,ts2,conv2)) => Term1(p1,And(ex1,ex2),ts1,conv1)
...@@ -171,6 +207,16 @@ object Terms { ...@@ -171,6 +207,16 @@ object Terms {
} }
} }
object AndConstraint3 {
def apply[A,B,C](l : Constraint[(A,B,C)], r : Constraint[(A,B,C)]) : Constraint3[A,B,C] = (l, r) match {
case (Term(p1,ex1,ts1,conv1), Term(p2,ex2,ts2,conv2)) => Term3(p1,And(ex1,ex2),ts1,conv1)
}
def apply[A,B,C](cs : Seq[Constraint[(A,B,C)]]) : Constraint3[A,B,C] = cs match {
case s @ Seq(Term(p,ex,ts,conv), _*) => Term3(p, And(s.map(_.expr)), ts, conv)
}
}
object NotConstraint1 { object NotConstraint1 {
def apply[A](c : Constraint[A]) : Constraint1[A] = c match { def apply[A](c : Constraint[A]) : Constraint1[A] = c match {
case Term(p,ex,ts,conv) => Term1(p,Not(ex),ts,conv) case Term(p,ex,ts,conv) => Term1(p,Not(ex),ts,conv)
...@@ -183,9 +229,16 @@ object Terms { ...@@ -183,9 +229,16 @@ object Terms {
} }
} }
object NotConstraint3 {
def apply[A,B,C](c : Constraint[(A,B,C)]) : Constraint3[A,B,C] = c match {
case Term(p,ex,ts,conv) => Term3(p,Not(ex),ts,conv)
}
}
type IntTerm[T] = Term[T,Int] type IntTerm[T] = Term[T,Int]
type IntTerm1[T1] = Term1[T1,Int] type IntTerm1[T1] = Term1[T1,Int]
type IntTerm2[T1,T2] = Term2[T1,T2,Int] type IntTerm2[T1,T2] = Term2[T1,T2,Int]
type IntTerm3[T1,T2,T3] = Term3[T1,T2,T3,Int]
/** This construct represents a constraint with an expression to minimize */ /** This construct represents a constraint with an expression to minimize */
abstract class MinConstraint[T](cons : Constraint[_], minFunc : IntTerm[_]) { abstract class MinConstraint[T](cons : Constraint[_], minFunc : IntTerm[_]) {
...@@ -217,6 +270,10 @@ object Terms { ...@@ -217,6 +270,10 @@ object Terms {
val convertingFunction = converterOf(cons).exprSeq2scala2[T1,T2] _ val convertingFunction = converterOf(cons).exprSeq2scala2[T1,T2] _
} }
case class MinConstraint3[T1,T2,T3](cons : Constraint3[T1,T2,T3], minFunc : IntTerm3[T1,T2,T3]) extends MinConstraint[(T1,T2,T3)](cons, minFunc) {
val convertingFunction = converterOf(cons).exprSeq2scala3[T1,T2,T3] _
}
/********** TERM METHODS **********/ /********** TERM METHODS **********/
/** compose_i_j_k will compose f (of arity j) and g (of arity k) as "g∘f" by /** compose_i_j_k will compose f (of arity j) and g (of arity k) as "g∘f" by
* inserting arguments of f in place of argument i of g */ * inserting arguments of f in place of argument i of g */
...@@ -224,19 +281,52 @@ object Terms { ...@@ -224,19 +281,52 @@ object Terms {
val (newExpr, newTypes) = compose(f, g, 0, 1, 1) val (newExpr, newTypes) = compose(f, g, 0, 1, 1)
Term1(f.program, newExpr, newTypes, f.converter) Term1(f.program, newExpr, newTypes, f.converter)
} }
private def compose_0_2_1[A1,A2,R1,R2](f : Term[(A1,A2),R1], g : Term[(R1),R2]) : Term2[A1,A2,R2] = { private def compose_0_2_1[A1,A2,R1,R2](f : Term[(A1,A2),R1], g : Term[(R1),R2]) : Term2[A1,A2,R2] = {
val (newExpr, newTypes) = compose(f, g, 0, 2, 1) val (newExpr, newTypes) = compose(f, g, 0, 2, 1)
Term2(f.program, newExpr, newTypes, f.converter) Term2(f.program, newExpr, newTypes, f.converter)
} }
private def compose_0_3_1[A1,A2,A3,R1,R2](f : Term[(A1,A2,A3),R1], g : Term[(R1),R2]) : Term3[A1,A2,A3,R2] = {
val (newExpr, newTypes) = compose(f, g, 0, 3, 1)
Term3(f.program, newExpr, newTypes, f.converter)
}
private def compose_0_1_2[A1,R1,B2,R2](f : Term[(A1),R1], g : Term[(R1,B2),R2]) : Term2[A1,B2,R2] = { private def compose_0_1_2[A1,R1,B2,R2](f : Term[(A1),R1], g : Term[(R1,B2),R2]) : Term2[A1,B2,R2] = {
val (newExpr, newTypes) = compose(f, g, 0, 1, 2) val (newExpr, newTypes) = compose(f, g, 0, 1, 2)
Term2(f.program, newExpr, newTypes, f.converter) Term2(f.program, newExpr, newTypes, f.converter)
} }
private def compose_1_1_2[A1,R1,B1,R2](f : Term[(A1),R1], g : Term[(B1,R1),R2]) : Term2[B1,A1,R2] = { private def compose_1_1_2[A1,R1,B1,R2](f : Term[(A1),R1], g : Term[(B1,R1),R2]) : Term2[B1,A1,R2] = {
val (newExpr, newTypes) = compose(f, g, 1, 1, 2) val (newExpr, newTypes) = compose(f, g, 1, 1, 2)
Term2(f.program, newExpr, newTypes, f.converter) Term2(f.program, newExpr, newTypes, f.converter)
} }
private def compose_0_2_2[A1,A2,R1,B2,R2](f : Term[(A1,A2),R1], g : Term[(R1,B2),R2]) : Term3[A1,A2,B2,R2] = {
val (newExpr, newTypes) = compose(f, g, 0, 2, 2)
Term3(f.program, newExpr, newTypes, f.converter)
}
private def compose_1_2_2[A1,A2,R1,B1,R2](f : Term[(A1,A2),R1], g : Term[(B1,R1),R2]) : Term3[B1,A1,A2,R2] = {
val (newExpr, newTypes) = compose(f, g, 1, 2, 2)
Term3(f.program, newExpr, newTypes, f.converter)
}
private def compose_0_1_3[A1,R1,B2,B3,R2](f : Term[(A1),R1], g : Term[(R1,B2,B3),R2]) : Term3[A1,B2,B3,R2] = {
val (newExpr, newTypes) = compose(f, g, 0, 1, 3)
Term3(f.program, newExpr, newTypes, f.converter)
}
private def compose_1_1_3[A1,R1,B1,B3,R2](f : Term[(A1),R1], g : Term[(B1,R1,B3),R2]) : Term3[B1,A1,B3,R2] = {
val (newExpr, newTypes) = compose(f, g, 1, 1, 3)
Term3(f.program, newExpr, newTypes, f.converter)
}
private def compose_2_1_3[A1,R1,B1,B2,R2](f : Term[(A1),R1], g : Term[(B1,B2,R1),R2]) : Term3[B1,B2,A1,R2] = {
val (newExpr, newTypes) = compose(f, g, 2, 1, 3)
Term3(f.program, newExpr, newTypes, f.converter)
}
/** Compute composed expression for g∘f */ /** Compute composed expression for g∘f */
private def compose(f : Term[_,_], g : Term[_,_], index : Int, nf : Int, ng : Int) : (Expr, Seq[TypeTree]) = (f, g) match { private def compose(f : Term[_,_], g : Term[_,_], index : Int, nf : Int, ng : Int) : (Expr, Seq[TypeTree]) = (f, g) match {
case (Term(_,ef,tf,_),Term(_,eg,tg,_)) => { case (Term(_,ef,tf,_),Term(_,eg,tg,_)) => {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment