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
8e7d4aeb
Commit
8e7d4aeb
authored
9 years ago
by
Manos Koukoutos
Browse files
Options
Downloads
Patches
Plain Diff
CEGIS now returns all non-validable solutions on the same level
Also, limit validateFrom to 100 programs
parent
93ccaa93
Branches
Branches containing commit
Tags
Tags containing commit
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/main/scala/leon/synthesis/rules/CEGISLike.scala
+15
-14
15 additions, 14 deletions
src/main/scala/leon/synthesis/rules/CEGISLike.scala
with
15 additions
and
14 deletions
src/main/scala/leon/synthesis/rules/CEGISLike.scala
+
15
−
14
View file @
8e7d4aeb
...
@@ -507,12 +507,12 @@ abstract class CEGISLike(name: String) extends Rule(name) {
...
@@ -507,12 +507,12 @@ abstract class CEGISLike(name: String) extends Rule(name) {
* Here we check the validity of a (small) number of programs in isolation.
* Here we check the validity of a (small) number of programs in isolation.
* We keep track of CEXs generated by invalid programs and preemptively filter the rest of the programs with them.
* We keep track of CEXs generated by invalid programs and preemptively filter the rest of the programs with them.
*/
*/
def
validatePrograms
(
bss
:
Set
[
Set
[
Identifier
]])
:
Either
[
Seq
[
Seq
[
Expr
]]
,
Solution
]
=
{
def
validatePrograms
(
bss
:
Set
[
Set
[
Identifier
]])
:
Either
[
Seq
[
Seq
[
Expr
]]
,
Stream
[
Solution
]
]
=
{
val
origImpl
=
cTreeFd
.
fullBody
val
origImpl
=
cTreeFd
.
fullBody
var
cexs
=
Seq
[
Seq
[
Expr
]]()
var
cexs
=
Seq
[
Seq
[
Expr
]]()
var
best
:
Option
[
Solution
]
=
N
one
var
best
:
List
[
Solution
]
=
N
il
for
(
bs
<-
bss
.
toSeq
)
{
for
(
bs
<-
bss
.
toSeq
)
{
// We compute the corresponding expr and replace it in place of the C-tree
// We compute the corresponding expr and replace it in place of the C-tree
...
@@ -537,6 +537,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
...
@@ -537,6 +537,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
val
solver
=
solverf
.
getNewSolver
()
val
solver
=
solverf
.
getNewSolver
()
try
{
try
{
debug
(
"Sending candidate to solver..."
)
debug
(
"Sending candidate to solver..."
)
def
currentSolution
(
trusted
:
Boolean
)
=
Solution
(
BooleanLiteral
(
true
),
Set
(),
outerSol
,
isTrusted
=
trusted
)
solver
.
assertCnstr
(
cnstr
)
solver
.
assertCnstr
(
cnstr
)
solver
.
check
match
{
solver
.
check
match
{
case
Some
(
true
)
=>
case
Some
(
true
)
=>
...
@@ -556,14 +557,12 @@ abstract class CEGISLike(name: String) extends Rule(name) {
...
@@ -556,14 +557,12 @@ abstract class CEGISLike(name: String) extends Rule(name) {
case
Some
(
false
)
=>
case
Some
(
false
)
=>
// UNSAT, valid program
// UNSAT, valid program
debug
(
"Found valid program!"
)
debug
(
"Found valid program!"
)
return
Right
(
S
olution
(
BooleanLiteral
(
true
),
Set
(),
outerSol
,
true
))
return
Right
(
S
tream
(
currentSolution
(
true
))
)
case
None
=>
case
None
=>
debug
(
"Found a non-verifiable solution..."
)
debug
(
"Found a non-verifiable solution..."
)
if
(
useOptTimeout
)
{
// Optimistic valid solution
// Optimistic valid solution
best
+:=
currentSolution
(
false
)
best
=
Some
(
Solution
(
BooleanLiteral
(
true
),
Set
(),
outerSol
,
false
))
}
}
}
}
finally
{
}
finally
{
solverf
.
reclaim
(
solver
)
solverf
.
reclaim
(
solver
)
...
@@ -573,11 +572,13 @@ abstract class CEGISLike(name: String) extends Rule(name) {
...
@@ -573,11 +572,13 @@ abstract class CEGISLike(name: String) extends Rule(name) {
}
}
}
}
best
.
map
{
sol
=>
if
(
useOptTimeout
&&
best
.
nonEmpty
)
{
// Interpret timeout in CE search as "the candidate is valid"
// Interpret timeout in CE search as "the candidate is valid"
info
(
"CEGIS could not prove the validity of the resulting expression"
)
info
(
s
"CEGIS could not prove the validity of the resulting ${best.size} expression(s)"
)
Right
(
sol
)
Right
(
best
.
toStream
)
}.
getOrElse
(
Left
(
cexs
))
}
else
{
Left
(
cexs
)
}
}
}
def
allProgramsClosed
=
prunedPrograms
.
isEmpty
def
allProgramsClosed
=
prunedPrograms
.
isEmpty
...
@@ -825,7 +826,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
...
@@ -825,7 +826,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
def
nPassing
=
ndProgram
.
prunedPrograms
.
size
def
nPassing
=
ndProgram
.
prunedPrograms
.
size
def
programsReduced
()
=
nPassing
<=
10
||
nInitial
/
nPassing
>
testReductionRatio
def
programsReduced
()
=
nPassing
<=
10
||
(
nPassing
<=
100
&&
nInitial
/
nPassing
>
testReductionRatio
)
gi
.
canGrow
=
programsReduced
gi
.
canGrow
=
programsReduced
def
allInputExamples
()
=
{
def
allInputExamples
()
=
{
...
@@ -904,9 +905,9 @@ abstract class CEGISLike(name: String) extends Rule(name) {
...
@@ -904,9 +905,9 @@ abstract class CEGISLike(name: String) extends Rule(name) {
val
programsToValidate
=
ndProgram
.
prunedPrograms
val
programsToValidate
=
ndProgram
.
prunedPrograms
debug
(
s
"Will send ${programsToValidate.size} program(s) to validate individually"
)
debug
(
s
"Will send ${programsToValidate.size} program(s) to validate individually"
)
ndProgram
.
validatePrograms
(
programsToValidate
)
match
{
ndProgram
.
validatePrograms
(
programsToValidate
)
match
{
case
Right
(
sol
)
=>
case
Right
(
sol
s
)
=>
// Found solution! Exit CEGIS
// Found solution! Exit CEGIS
result
=
Some
(
RuleClosed
(
sol
))
result
=
Some
(
RuleClosed
(
sol
s
))
case
Left
(
cexs
)
=>
case
Left
(
cexs
)
=>
debug
(
s
"Found cexs! $cexs"
)
debug
(
s
"Found cexs! $cexs"
)
// Found some counterexamples
// Found some counterexamples
...
...
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