Skip to content

Leiqi concrete simulator #260

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

Merged
polgreen merged 9 commits into from
Mar 24, 2025
Merged

Leiqi concrete simulator #260

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
22d1b32
add concrete Simulator
lichye Oct 9, 2024
cb0f0b7
change other file
lichye Oct 9, 2024
c5c474c
Added link to tutorial lectures
saseshia Nov 14, 2024
ba905f4
add ConcreteSimutalor with the same output result
lichye Feb 18, 2025
6cd8952
change cache to v4
lichye Feb 21, 2025
c59b39a
rewrite the codebase
lichye Mar 3, 2025
25d1348
debug
lichye Mar 5, 2025
951404f
modify test benchmark
lichye Mar 17, 2025
98321ef
fix up typo
lichye Mar 20, 2025
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
21 changes: 13 additions & 8 deletions .github/workflows/test.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ jobs:

- name: Cache Z3
id: cache-z3
uses: actions/cache@v1
uses: actions/cache@v4
with:
path: z3/
key: ${{ runner.os }}-z3-${{ hashFiles('get-z3-linux.sh') }}-1
Expand All @@ -35,7 +35,7 @@ jobs:

- name: Cache CVC5
id: cache-cvc5
uses: actions/cache@v1
uses: actions/cache@v4
with:
path: cvc5/
key: ${{ runner.os }}-cvc5-${{ hashFiles('get-cvc5-linux.sh') }}-1
Expand All @@ -54,7 +54,7 @@ jobs:

# - name: Cache Delphi
# id: cache-delphi
# uses: actions/cache@v1
# uses: actions/cache@v4
# with:
# path: delphi/
# key: ${{ runner.os }}-delphi-${{ hashFiles('get-delphi-linux.sh') }}-1
Expand All @@ -79,16 +79,21 @@ jobs:
java-version: 11

- name: Cache SBT ivy cache
uses: actions/cache@v1
uses: actions/cache@v4
with:
path: ~/.ivy2/cache
key: ${{ runner.os }}-sbt-ivy-cache-${{ hashFiles('**/build.sbt') }}

- name: Cache SBT
uses: actions/cache@v1
uses: actions/cache@v4
with:
path: ~/.sbt
key: ${{ runner.os }}-sbt-${{ hashFiles('**/build.sbt') }}

- name: Set up SBT
uses: coursier/setup-action@v1
with:
apps: sbt

- name: Compile
run: sbt compile
Expand All @@ -110,7 +115,7 @@ jobs:

- name: Cache Z3
id: cache-z3
uses: actions/cache@v1
uses: actions/cache@v4
with:
path: z3/
key: ${{ runner.os }}-z3-${{ hashFiles('get-z3-macos.sh') }}-1
Expand All @@ -133,7 +138,7 @@ jobs:

- name: Cache CVC5
id: cache-cvc5
uses: actions/cache@v1
uses: actions/cache@v4
with:
path: cvc5/
key: ${{ runner.os }}-cvc5-${{ hashFiles('get-cvc5-macos.sh') }}-1
Expand All @@ -152,7 +157,7 @@ jobs:

# - name: Cache delphi
# id: cache-delphi
# uses: actions/cache@v1
# uses: actions/cache@v4
# with:
# path: delphi/
# key: ${{ runner.os }}-delphi-${{ hashFiles('get-delphi-macos.sh') }}-1
Expand Down
4 changes: 3 additions & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,9 @@ For bug reports, first preference is for you to file a GitHub issue. For help us

## UCLID5 Tutorial/Publication

The [tutorial](https://github.com/uclid-org/uclid/blob/master/tutorial/tutorial.pdf) has a gentle introduction to using UCLID5.
The [tutorial document](https://github.com/uclid-org/uclid/blob/master/tutorial/tutorial.pdf) has a gentle introduction to using UCLID5.

A set of tutorial lectures on UCLID5 can be found [here](https://people.eecs.berkeley.edu/~sseshia/uclid5-tutorial/).


## Versions
Expand Down
1 change: 1 addition & 0 deletions src/main/resources/logback.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@
<logger name="uclid.Utils.schedule" level="OFF"/>
<logger name="uclid.Utils.topoSort" level="OFF"/>
<logger name="uclid.smt.SynthLibInterface" level="OFF"/>
<logger name="ConcreteSimulator" level="OFF"/>


<root level="debug">
Expand Down
Loading