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

IC3IA with cvc5's SyGuS-based predicate generation #357

Draft
wants to merge 231 commits into
base: main
Choose a base branch
from
Draft

IC3IA with cvc5's SyGuS-based predicate generation #357

wants to merge 231 commits into from

Conversation

CyanoKobalamyne
Copy link
Collaborator

No description provided.

@makaimann
WIP: just starting on IC3Base
5b3d9ac
@makaimann
Some refactoring in IC3Base
9afbcd6
@makaimann
Work on moving more over to base class
305bad0
@makaimann
Temporarily change name of ProofGoal in IC3Base to avoid clashing
e67b1bb
@makaimann
Add a negate method to IC3Unit
bb4c039
@makaimann
WIP: start moving implementation to IC3Base
f911344
@makaimann
Don't make IC3Unit abstract
7165f11
@makaimann
Add an UnsatCoreReducer to IC3Base
7a07fba
@makaimann
Use UnsatCoreReduder for fixing initial - and add required make_and
7ed60bd
@makaimann
Fix includes
10a1cb5
@makaimann
WIP implementation of block_all -- changed from unique_ptr to shared_…
1818c9d 
…ptr for goals
@makaimann
Implement block_all
0a26f94
@makaimann
Implement step and step_0
a4fa591
@makaimann
Add intersects_bad
9ec0454
@makaimann
Implement initialize for IC3Base
8d6e579
@makaimann
Remove IC3UnitCreator and use a virtual function instead
a06e605
@makaimann
Implement get_predecessor
da1a40a
@makaimann
Add pure virtual function for checking TS
d3afcfa
@makaimann
Add a handler for creating / negating IC3Units
709044f
@makaimann
WIP on ClauseHandler for bit-level IC3
3827e51
@makaimann
Add IC3 constructors
882475d
@makaimann
WIP: implement pure virtual methods in IC3 and add necessary infrastr…
3a229f1 
…ucture
@makaimann
Several fixes from initial tests
0e1e045
@makaimann
More fixes related to solver context -- should be refactored so that …
a373279 
…virtual methods start at solver_context_ == 0
@makaimann
Fix call to generalize_predecessor
0a4c57b
@makaimann
Make sure to create Cube correctly
c309a9a
@makaimann
Bit-level IC3 is working
164a0fc
@makaimann
Minor comments
9274b05
@makaimann
More comments
43a7f00
@makaimann
Fix includes for Linux
d11792b
makaimann and others added 26 commits May 5, 2021 14:22
@makaimann
Use values in first grammar
676ca0e
@makaimann
Revert "Use values in first grammar"
e65bd88 
This reverts commit 676ca0e.
@makaimann
Use values from TS (not unrolling) first
c7ae688
@makaimann
Minor
2114e35
@makaimann
Add sign extend to multisort operators
64c4ab6
@makaimann
Allow unbounded size by passing 0
0747e30
@makaimann
Update smt-switch version
b4ac732
@makaimann
Some cvc4 -> cvc5 renaming
94787a6
@makaimann
cvc4->cvc5 renaming
508a07d
@makaimann
cvc4->cvc5 in tests directory
d43a59d
@makaimann
Update download script for cvc5
8839ecc
@makaimann
Fix CI for cvc5
d49726f
@makaimann
Temporarily pull branch of smt-switch
7db2188
@makaimann
Merge branch 'master' into ic3ia-cvc5-pred
74ec4ea
@makaimann
Update smt-switch building script
9c87e7d
@ahmed-irfan
Merge branch 'ic3ia-cvc4-pred' into ic3ia-cvc4-pred
4e3d7ac
@ahmed-irfan
Merge pull request stanford-centaur#1 from upscale-project/ic3ia-cvc4…
75706eb 
…-pred

Ic3ia cvc4 pred
@ahmed-irfan
merge ic3ia-cvc4-pred
18f155a
@ahmed-irfan
cvc5
e415838
@ahmed-irfan
Merge branch 'master' of github.com:upscale-project/pono into ic3ia-c…
58deeab 
…vc5-pred
@makaimann
Fix some compiler errors -- there are still more from the updated cvc…
7e002a0 
…5 api
@ahmed-irfan
fix more errors -- compiles now
3cc85ed
@ahmed-irfan
fix test
dd178f4
@ahmed-irfan
fix sygus option
ac9d40b
@ahmed-irfan
dump
21367ae
@CyanoKobalamyne
Merge branch 'main' into ic3ia-cvc5-pred-rebase
34fc00b
@CyanoKobalamyne CyanoKobalamyne changed the base branch from ic3ia-cvc5-pred to main October 9, 2024 03:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@CyanoKobalamyne @makaimann @ahmed-irfan @yoni206