Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
I
inox
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
LARA
inox
Commits
2daefa84
Commit
2daefa84
authored
10 years ago
by
Emmanouil (Manos) Koukoutos
Committed by
Etienne Kneuss
10 years ago
Browse files
Options
Downloads
Patches
Plain Diff
Generators from subexpressions with placeholders
parent
9c0b26bf
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+93
-0
93 additions, 0 deletions
src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
with
93 additions
and
0 deletions
src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+
93
−
0
View file @
2daefa84
...
...
@@ -170,6 +170,99 @@ class ExpressionGrammar(ctx: LeonContext, prog: Program, inputs: Seq[Expr], curr
}
}
def
computeSubexpressionGenerators
(
canPlacehold
:
Expr
=>
Boolean
)(
e
:
Expr
)
:
Seq
[
Gen
]
=
{
/** A simple Generator API **/
def
gen
(
tps
:
Seq
[
TypeTree
],
f
:
Seq
[
Expr
]
=>
Expr
)
:
Gen
=
Generator
[
TypeTree
,
Expr
](
tps
,
f
)
// A generator that accepts a single type, and always regenerates its input
// (simple placeholder of 1 position)
def
wildcardGen
(
tp
:
TypeTree
)
=
gen
(
Seq
(
tp
),
{
case
Seq
(
x
)
=>
x
})
// A generator that always regenerates its input
def
const
(
e
:
Expr
)
:
Gen
=
gen
(
Seq
(),
_
=>
e
)
// Creates a new generator by applying f on the result of g.builder
def
map
(
f
:
Expr
=>
Expr
)(
g
:
Gen
)
:
Gen
=
{
gen
(
g
.
subTrees
,
es
=>
f
(
g
.
builder
(
es
))
)
}
// Concatenate a sequence of generators into a generator.
// The arity of the resulting generator is the total arity of the constituting generators.
// builder is the function combining the results of the partial generators
def
concat
(
gens
:
Seq
[
Gen
],
builder
:
Seq
[
Expr
]
=>
Expr
)
:
Gen
=
{
val
types
=
gens
flatMap
{
_
.
subTrees
}
gen
(
types
,
exprs
=>
{
assert
(
exprs
.
length
==
types
.
length
)
// Total arity is arity of subgenerators
var
remaining
=
exprs
val
fromSubGens
=
for
(
gen
<-
gens
)
yield
{
val
(
current
,
rem
)
=
remaining
splitAt
gen
.
arity
remaining
=
rem
gen
.
builder
(
current
)
}
builder
(
fromSubGens
)
}
)
}
def
rec
(
e
:
Expr
)
:
Seq
[
Gen
]
=
{
// Add an additional wildcard generator, if current expression passes the filter
def
optWild
(
gens
:
Seq
[
Gen
])
:
Seq
[
Gen
]
=
if
(
canPlacehold
(
e
))
{
wildcardGen
(
e
.
getType
)
+:
gens
}
else
gens
e
match
{
case
t
:
Terminal
=>
// In case of Terminal, we either return the terminal itself, or the input expression
optWild
(
Seq
(
const
(
t
)))
case
UnaryOperator
(
sub
,
builder
)
=>
val
fromSub
=
for
(
subGen
<-
rec
(
sub
))
yield
map
(
builder
)(
subGen
)
optWild
(
fromSub
)
case
BinaryOperator
(
e1
,
e2
,
builder
)
=>
val
fromSub
=
for
{
subGen1
<-
rec
(
e1
)
subGen2
<-
rec
(
e2
)
}
yield
concat
(
Seq
(
subGen1
,
subGen2
),
{
case
Seq
(
e1
,
e2
)
=>
builder
(
e1
,
e2
)
})
optWild
(
fromSub
)
case
NAryOperator
(
subExpressions
,
builder
)
=>
def
combinations
[
A
](
seqs
:
Seq
[
Seq
[
A
]])
:
Seq
[
Seq
[
A
]]
=
{
if
(
seqs
.
isEmpty
)
Seq
(
Seq
())
else
for
{
hd
<-
seqs
.
head
tl
<-
combinations
(
seqs
.
tail
)
}
yield
hd
+:
tl
}
val
combos
=
combinations
(
subExpressions
map
rec
)
val
fromSub
=
combos
map
{
concat
(
_
,
builder
)
}
optWild
(
fromSub
)
}
}
rec
(
e
)
}
def
computeCompleteSubexpressionGenerators
=
inputs
flatMap
computeSubexpressionGenerators
{
_
=>
true
}
def
printGrammar
(
printer
:
String
=>
Unit
)
{
for
((
t
,
gs
)
<-
cache
;
g
<-
gs
)
{
val
subs
=
g
.
subTrees
.
map
{
tpe
=>
FreshIdentifier
(
tpe
.
toString
).
setType
(
tpe
).
toVariable
}
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment