Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Hide statements #5562

Open
wants to merge 48 commits into
base: master
Choose a base branch
from
Open

Hide statements #5562

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
48 commits
Select commit Hold shift + click to select a range
a9d1b80
Add Boogie as a submodule
keyboardDrummer Jun 12, 2024
7bded0a
Use Boogie submodule
keyboardDrummer Jun 12, 2024
e7be101
Added reveal test
keyboardDrummer Jun 13, 2024
d34a4fa
Move resolve code for revealStmt to RevealStmt class
keyboardDrummer Jun 13, 2024
b7ae5a5
reveal.dfy test passes
keyboardDrummer Jun 13, 2024
f354052
Update reveal test
keyboardDrummer Jun 13, 2024
23f82c6
Progress towards blind functions
keyboardDrummer Jun 15, 2024
dcc4a89
Simplification
keyboardDrummer Jun 15, 2024
5bbc32e
Reveal.dfy passes
keyboardDrummer Jun 15, 2024
10d4a0f
Refactoring for readability
keyboardDrummer Jun 15, 2024
8f5940a
Add hidden function ensure clause test case to reveal.dfy
keyboardDrummer Jun 16, 2024
37f9462
Refactor TrPredicateStmt
keyboardDrummer Jun 16, 2024
608a6ab
Fix test
keyboardDrummer Jun 16, 2024
fca4526
Reveal now had a passing test for combining blind, opaque and reveal
keyboardDrummer Jun 17, 2024
8c0b90d
Update reveal.dfy test
keyboardDrummer Jun 20, 2024
97c4910
Add scratch test for playing around with
keyboardDrummer Jun 24, 2024
653c776
Make functions in Prelude revealed
keyboardDrummer Jun 24, 2024
3d7e01c
Make more generated function always revealed
keyboardDrummer Jun 24, 2024
5a65cb8
Let axioms decide if they can be hidden
keyboardDrummer Jun 27, 2024
af8b397
Update tests
keyboardDrummer Jun 27, 2024
f8bf900
Update test
keyboardDrummer Jun 27, 2024
84021fb
Update tests
keyboardDrummer Jun 27, 2024
eba67ca
Draft
keyboardDrummer Jul 1, 2024
f4da59c
Replace blind with hide statement
keyboardDrummer Jul 1, 2024
ee98116
Some success on revealFunctions.dfy
keyboardDrummer Jul 1, 2024
64f1c3d
revealFunctions.dfy works except for scoping now
keyboardDrummer Jul 1, 2024
28a2483
Scoping for if now works for revealFunctions.dfy
keyboardDrummer Jul 1, 2024
f4e3658
revealFunctions passes
keyboardDrummer Jul 1, 2024
b755a61
Reveal functions passes
keyboardDrummer Jul 2, 2024
0c2f5a0
Finished draft of revealInBlock test
keyboardDrummer Jul 2, 2024
10db663
Fix printing and cloning of hide reveal statements
keyboardDrummer Jul 2, 2024
18fb8fb
revealInBlock test passes
keyboardDrummer Jul 2, 2024
dd9fd67
Fixed revealInExpression test
keyboardDrummer Jul 2, 2024
f5afce8
Refactoring
keyboardDrummer Jul 2, 2024
a6e65d2
Progress in isolating expression wellformedness checks
keyboardDrummer Jul 3, 2024
c46ff52
revealInExpression test now passes
keyboardDrummer Jul 3, 2024
7861efa
Some cleanup
keyboardDrummer Jul 3, 2024
5664a6f
Adapt to Boogie changes and fix tests
keyboardDrummer Jul 3, 2024
64c5b4c
Refactoring and fixes
keyboardDrummer Jul 3, 2024
b5ad048
Remove comment
keyboardDrummer Jul 4, 2024
eca25fb
Merge commit 'origin/master~1' into alwaysOpaque
keyboardDrummer Jul 4, 2024
c60e66f
Merge remote-tracking branch 'origin/master' into alwaysOpaque
keyboardDrummer Jul 4, 2024
c33ffb1
Refactoring
keyboardDrummer Jul 4, 2024
fbe6356
Update documentation
keyboardDrummer Jul 4, 2024
a8670a9
Add release note
keyboardDrummer Jul 4, 2024
a2a6541
Revert "Use Boogie submodule"
keyboardDrummer Jul 4, 2024
b0b6350
Revert "Add Boogie as a submodule"
keyboardDrummer Jul 4, 2024
915659d
Update Boogie version
keyboardDrummer Jul 4, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Use Boogie submodule
  • Loading branch information
@keyboardDrummer
keyboardDrummer committed Jun 12, 2024
commit 7bded0a12767ef7ef7c7e33eda897082414b193a
38 changes: 38 additions & 0 deletions Source/Dafny.sln
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,32 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
EndProject
Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Boogie", "Boogie", "{60332269-9C5D-465E-8582-01F9B738BD90}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "BaseTypes", "..\boogie\Source\BaseTypes\BaseTypes.csproj", "{68721962-0D91-4355-BC94-BE1CCBD30E47}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AbstractInterpretation", "..\boogie\Source\AbstractInterpretation\AbstractInterpretation.csproj", "{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "CodeContractsExtender", "..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj", "{09662044-5640-4785-92E3-2F7CDBA4DDB2}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Concurrency", "..\boogie\Source\Concurrency\Concurrency.csproj", "{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Core", "..\boogie\Source\Core\Core.csproj", "{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ExecutionEngine", "..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj", "{0145DC89-7243-41F8-AB3E-F716F04E9BFF}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Graph", "..\boogie\Source\Graph\Graph.csproj", "{05DE24BB-D639-40C4-894F-701652F51559}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Houdini", "..\boogie\Source\Houdini\Houdini.csproj", "{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "..\boogie\Source\Model\Model.csproj", "{D97C23B6-FB4A-4450-930E-58EC83D308A0}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}"
EndProject
EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Expand Down Expand Up @@ -138,5 +164,17 @@ Global
SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187}
EndGlobalSection
GlobalSection(NestedProjects) = preSolution
{68721962-0D91-4355-BC94-BE1CCBD30E47} = {60332269-9C5D-465E-8582-01F9B738BD90}
{2A6B36F4-9F15-459A-8EDB-5BAEED98FE17} = {60332269-9C5D-465E-8582-01F9B738BD90}
{09662044-5640-4785-92E3-2F7CDBA4DDB2} = {60332269-9C5D-465E-8582-01F9B738BD90}
{DA8A9BA8-9BBA-4C64-9736-FD967517DCA9} = {60332269-9C5D-465E-8582-01F9B738BD90}
{2BF5ECCA-24B2-4A4B-86B6-D0DB17331109} = {60332269-9C5D-465E-8582-01F9B738BD90}
{0145DC89-7243-41F8-AB3E-F716F04E9BFF} = {60332269-9C5D-465E-8582-01F9B738BD90}
{05DE24BB-D639-40C4-894F-701652F51559} = {60332269-9C5D-465E-8582-01F9B738BD90}
{51D6B0D1-2D15-40A3-80F4-E32A5C07B0A6} = {60332269-9C5D-465E-8582-01F9B738BD90}
{D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90}
{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90}
{E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90}
{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90}
EndGlobalSection
EndGlobal
12 changes: 11 additions & 1 deletion Source/DafnyCore/DafnyCore.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,17 @@
<PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
<PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
<PackageReference Include="System.Collections.Immutable" Version="1.7.1" />
<PackageReference Include="Boogie.ExecutionEngine" Version="3.1.6" />
<ProjectReference Include="..\..\boogie\Source\ExecutionEngine\ExecutionEngine.csproj" />
<ProjectReference Include="..\..\boogie\Source\BaseTypes\BaseTypes.csproj" />
<ProjectReference Include="..\..\boogie\Source\Core\Core.csproj" />
<ProjectReference Include="..\..\boogie\Source\Graph\Graph.csproj" />
<ProjectReference Include="..\..\boogie\Source\Model\Model.csproj" />
<ProjectReference Include="..\..\boogie\Source\CodeContractsExtender\CodeContractsExtender.csproj" />
<ProjectReference Include="..\..\boogie\Source\VCExpr\VCExpr.csproj" />
<ProjectReference Include="..\..\boogie\Source\VCGeneration\VCGeneration.csproj" />
<ProjectReference Include="..\..\boogie\Source\Provers\SMTLib\SMTLib.csproj" />
<ProjectReference Include="..\..\boogie\Source\Houdini\Houdini.csproj" />
<ProjectReference Include="..\..\boogie\Source\Concurrency\Concurrency.csproj" />
<PackageReference Include="Tomlyn" Version="0.16.2" />
</ItemGroup>

Expand Down