Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
929 commits
Select commit Hold shift + click to select a range
ed15af8
More preparation for eliminating nested calls to rewriter in strings …
ajreynol Jan 27, 2025
83e92c2
Add several new RARE rules for strings (#11514)
ajreynol Jan 27, 2025
4007720
ci: Add manual trigger for wheel publication (#11568)
daniel-larraz Jan 27, 2025
c251365
ci: Add option to choose the Python versions to build (#11571)
daniel-larraz Jan 28, 2025
fbed8f8
Use Cython's definition of libcpp.optional. (#11572)
robertwb Jan 28, 2025
27e184d
Demote more string rewrites to the extended rewriter (#11570)
ajreynol Jan 28, 2025
503cadf
Regression tests for the conjecture generator (#11519)
kartik-sabharwal Jan 30, 2025
eb6ccba
Introduce a primative string utility `Word::hasOverlap` (#11579)
ajreynol Jan 31, 2025
68bf6fb
Add default proof logger to log cpc proofs (#11511)
ajreynol Jan 31, 2025
a352c69
Add Eunoia definitions of extended RE evaluation (#11581)
ajreynol Feb 3, 2025
4180a07
Add support for `str.replace_all` in evaluator (#11334)
ajreynol Feb 3, 2025
c638460
Add proof support for arithmetic static learning (#11494)
ajreynol Feb 3, 2025
c1ad0f4
Split expert portions of Cpc.eo to own subdirectory (#11583)
ajreynol Feb 3, 2025
cbb647b
resolve dependency issues in rules/Uf.eo and programs/Nary.eo (#11543)
ciaran-matthew-dunne Feb 3, 2025
93a6469
Eunoia definition of arith BV conversions (#11584)
ajreynol Feb 3, 2025
470bfc7
moved conjecture generator eqc collection code into new function (#11…
kartik-sabharwal Feb 3, 2025
89e01fc
Add more cases of STRING_REDUCTION in Eunoia (#11586)
ajreynol Feb 4, 2025
fb422d0
Fix corner case in Eo signature for replace_re_all (#11585)
ajreynol Feb 4, 2025
70229a1
Add CPC and Eunoia definitions for string theory rewrites involving o…
ajreynol Feb 5, 2025
4953ad3
ci: Update Ubuntu runners to 22.04 (#11573)
daniel-larraz Feb 5, 2025
f784f98
Simplify CPC and Eunoia definition of ARITH_POLY_NORM_REL (#11578)
ajreynol Feb 5, 2025
acd6995
Add proof elaboration for MACRO_ARRAYS_NORMALIZE_OP (#11530)
ajreynol Feb 5, 2025
30bc237
Make RE_INTER_UNION_INCLUSION a macro, elaborate to simpler version (…
ajreynol Feb 6, 2025
6836398
More updates to classifications of options (#11576)
ajreynol Feb 6, 2025
87fd92a
Two fixes for quantifiers prenex proofs (#11487)
ajreynol Feb 7, 2025
4f3d959
Add Eunoia definitions of ARITH_MULT_SIGN and ARITH_MULT_ABS_COMPARIS…
ajreynol Feb 7, 2025
f7d323c
Refactor proof post processor DSL to avoid subgoal tracking (#11442)
ajreynol Feb 8, 2025
c79e20e
Add missing `const`s to iterator members (#11575)
eric-wieser Feb 10, 2025
4fbf9ed
Add more regressions demonstrating tricky proof cases (#11574)
ajreynol Feb 10, 2025
b38c29b
Add macros and elaboration for arithmetic integer relation rewrites (…
ajreynol Feb 10, 2025
e59c1e4
[proofs] Remove eager check for SAT proof closedness (#11613)
HanielB Feb 10, 2025
fb0b8e8
Update CPC signature and output to fully support parametric datatypes…
ajreynol Feb 10, 2025
e067b52
Make unit tests for proofs more robust wrt rewrite rules (#11601)
ajreynol Feb 10, 2025
dbb3c25
bitblast_utils: Refactor to not use NodeManager::currentNM() (#11529)
daniel-larraz Feb 10, 2025
b0cff18
Add Eunoia definition for more cases of STRING_REDUCTION (#11587)
ajreynol Feb 11, 2025
cbc0bd0
Fix printer for user patterns and annotations (#11598)
ajreynol Feb 11, 2025
c5fd700
Updates for string entail utility (#11607)
ajreynol Feb 11, 2025
637d166
Handle more cases in arith string pred entail (#11610)
ajreynol Feb 11, 2025
2b3a4be
Minor modifications to expert signature (#11611)
ajreynol Feb 11, 2025
fbf4750
Guard more cases of constant arrays in assertions (#11602)
ajreynol Feb 11, 2025
2ffe9f3
ci: Use the minimum required CMake version on Linux runners (#11595)
daniel-larraz Feb 11, 2025
1d83f8c
Update policy on options exceptions (#11566)
ajreynol Feb 11, 2025
ed3f78c
NodeBuilder: Assert that NodeManagers match. (#11620)
aniemetz Feb 11, 2025
9880318
Add ProofRule::RE_CONCAT (#11600)
ajreynol Feb 11, 2025
24b2d5a
Split RARE rewrites for expert extensions to own files (#11619)
ajreynol Feb 11, 2025
056ada5
Adding all Mbqi-Enum options and renaming the method from Mbqi-Fast-S…
kondylidou Feb 12, 2025
13f7a91
Splice constants in strings infer proof cons (#11593)
ajreynol Feb 12, 2025
53560b9
Fix documentation for transcendentals, make proof checker more pedant…
ajreynol Feb 12, 2025
669004e
Add proof elaboration for diamonds preprocessing (#11447)
ajreynol Feb 12, 2025
584111c
Split proof rules ARITH_POLY_NORM(_REL) to BV_POLY_NORM(_EQ) (#11609)
ajreynol Feb 12, 2025
2f076ba
Add ProofRule::DISTINCT_VALUES (#11596)
ajreynol Feb 12, 2025
8e2d145
Add remaining cases of STRING_REDUCTION in Eunoia (#11630)
ajreynol Feb 12, 2025
8cda341
Add unused variables to RARE preprocess tactic (#11467)
ajreynol Feb 12, 2025
ed4a464
Simplify quantifiers variable elimination inequality rewrite (#11605)
ajreynol Feb 13, 2025
25ab3e0
Generalize BV poly norm eq to odd coefficients (#11632)
ajreynol Feb 13, 2025
af8e321
Miscellaneous refactoring of arithmetic RARE rewrites (#11478)
ajreynol Feb 13, 2025
b4356ff
Add regressions for fixed issues (#11627)
ajreynol Feb 13, 2025
9fc7fa5
Add regressions for proofs (#11634)
ajreynol Feb 13, 2025
0311e55
Add macro rewrite MACRO_BV_EQ_SOLVE (#11466)
ajreynol Feb 14, 2025
3ff8ea3
Ensure only canonized terms are added to theorem index (#11635)
kartik-sabharwal Feb 14, 2025
9dbabd2
fix type errors in proofs/eo/programs/Nary.eo (#11640)
ciaran-matthew-dunne Feb 14, 2025
368a34f
Moved computation of irrelevant equivalence classes to separate funct…
kartik-sabharwal Feb 14, 2025
10cc6d5
Add rewrite level (normal/expert for rewrite rules) (#11646)
lenianiva Feb 17, 2025
92e99e7
Add Eunoia signature defining translation from sequences to strings (…
ajreynol Feb 17, 2025
72be5c8
Add macros for (non-splitting) string overlap rules (#11618)
ajreynol Feb 17, 2025
5efa79f
Add Eunoia definition for ProofRewriteRule::DISTINCT_CARD_CONFLICT (#…
ajreynol Feb 17, 2025
339a304
Add macros for string contains split overlap rule (#11591)
ajreynol Feb 18, 2025
16d644b
Add -o rare-db-expert, partition eo rewrite signatures (#11648)
ajreynol Feb 18, 2025
ac2b8b8
Fix several Eunoia rules for sequences (#11649)
ajreynol Feb 18, 2025
6983538
arith: Refactor to not use NodeManager::currentNM() (#11496)
daniel-larraz Feb 18, 2025
3e88ebd
Move BV ppAssert to its own utility, add proofs (#11427)
ajreynol Feb 18, 2025
bb7099f
Add distinct values to RARE reconstruction strategy (#11636)
ajreynol Feb 18, 2025
9de62f6
Do not include expert Eunoia signature from main signature (#11653)
ajreynol Feb 18, 2025
3759dab
Simplify internal proof checker for strings to not splice constants (…
ajreynol Feb 18, 2025
6eaadbc
Add helper functions to proof elaborator (#11652)
ajreynol Feb 19, 2025
69ba034
Simplifications to the core rules of the strings calculus (#11594)
ajreynol Feb 19, 2025
228f749
Add proof elaboration for string overlap macro rules (#11650)
ajreynol Feb 19, 2025
d0e7209
Fixes for BV RARE rules (#11642)
ajreynol Feb 19, 2025
2dcbe61
Improvements and optimizations for Eunoia quantifiers signature (#11603)
ajreynol Feb 20, 2025
a09cf82
Add elaboration for MACRO_STR_EQ_LEN_UNIFY (#11659)
ajreynol Feb 20, 2025
cecff59
Add proof rewrite rule SEQ_EVAL_OP (#11657)
ajreynol Feb 20, 2025
348845e
Documentation for OpArgIndex in conjecture generator (#11665)
kartik-sabharwal Feb 20, 2025
0ab0f2d
Add elaboration for MACRO_STR_EQ_LEN_UNIFY_PREFIX (#11658)
ajreynol Feb 20, 2025
a69fba7
Do not purify ground Boolean subterms in quantifier bodies (#11654)
ajreynol Feb 20, 2025
e2d2cfd
Small Cosmetic Changes to RARE rules (#11666)
Lachnitt Feb 24, 2025
76b59f0
separate function for debugging irrelevant eqc computation (#11669)
kartik-sabharwal Feb 24, 2025
b936ead
Add support for datatypes updater elimination rules in Eunoia (#11625)
ajreynol Feb 24, 2025
9dbba0f
Do not use array constants in sygus grammars unless arraysExp is true…
ajreynol Feb 24, 2025
2e06222
Miscellaneous changes from proof dev branch (#11668)
ajreynol Feb 24, 2025
116c288
Minor fix for quantifiers preprocessing pass (#11672)
ajreynol Feb 24, 2025
ae3442b
ci: Use separate GitHub Action to set up CMake (#11673)
daniel-larraz Feb 24, 2025
c67d35b
Add bitvector concat and xor to ACI_NORM (#11674)
ajreynol Feb 25, 2025
934876f
Add regressions for fixed issues (#11671)
ajreynol Feb 25, 2025
1596859
Fix corner case of elaboration of quantifiers merge prenex (#11661)
ajreynol Feb 25, 2025
3b7111d
Add getGeneralizedConstRegExp utility in RegExp entail (#11608)
ajreynol Feb 25, 2025
67595f8
Add macro and elaboration for MACRO_STR_COMPONENT_CTN (#11681)
ajreynol Feb 26, 2025
9826a0e
Add RARE rule for divisible (#11677)
ajreynol Feb 26, 2025
c4e55cc
Introduce MACRO_QUANT_DT_VAR_EXPAND and its elaboration (#11604)
ajreynol Feb 26, 2025
3cf3f1c
Refactor RE inter/union rewriter, add macro rewrite for RE inter/unio…
ajreynol Feb 26, 2025
e9704d4
Add proof elaboration for MACRO_STR_CONST_NCTN_CONCAT (#11679)
ajreynol Feb 26, 2025
ec4c678
Disable LFSC on regression (#11682)
ajreynol Feb 26, 2025
fb7e904
Add proof elaboration for MACRO_STR_IN_RE_INCLUSION (#11680)
ajreynol Feb 26, 2025
d9d228f
More fixes for LFSC + nightlies (#11684)
ajreynol Feb 27, 2025
84d755c
Eliminate use of LinearRewriteStrategy in cases where proofs can not …
ajreynol Feb 27, 2025
685fa7d
Only support datatype match if datatypesExp is true (#11444)
ajreynol Feb 27, 2025
06d065a
theory_bv_utils: Refactor to not use NodeManager::currentNM() (#11617)
daniel-larraz Feb 27, 2025
e1aecfb
cmake: Introduce max version check for CaDiCaL. (#11691)
aniemetz Feb 28, 2025
3ba0cf3
cmake: Remove workaround that got addressed on CMS side. (#11692)
aniemetz Feb 28, 2025
5e6dae4
Guard another case where variable elimination is not equivalence pres…
ajreynol Feb 28, 2025
2668938
cadical: Make modelValue more robust. (#11695)
aniemetz Feb 28, 2025
bbf701c
java: Remove reference to non-existent API function. (#11694)
aniemetz Feb 28, 2025
2f92bba
Take remaining minor changes to strings rewriter from proof branch (#…
ajreynol Mar 1, 2025
0232cd8
Guard another case of expert extensions of arithmetic (#11686)
ajreynol Mar 1, 2025
d287860
Add proof rewrite rule MACRO_BOOL_BV_INVERT_SOLVE (#11687)
ajreynol Mar 1, 2025
44b9ba8
Add proof elaboration for MACRO_RE_INTER_UNION_CONST_ELIM (#11685)
ajreynol Mar 1, 2025
f00cb40
Add regressions for fixed issues. (#11697)
ajreynol Mar 1, 2025
335a4e4
Fix elaboration of MACRO_SR_PRED_TRANSFORM (#11688)
ajreynol Mar 1, 2025
ac06198
Add regressions for more proof holes (#11663)
ajreynol Mar 1, 2025
0173102
Improve recursion limit heuristic in RARE (#11683)
ajreynol Mar 3, 2025
28c14d6
Improve warnings and errors for sygus-inference (#11690)
ajreynol Mar 3, 2025
1539ae5
Add proof rule ABSORB (#11637)
ajreynol Mar 3, 2025
8288af5
Address nondeterminism in quantifiers rewriter (#11700)
ajreynol Mar 4, 2025
802460d
Add proof elaboration for MACRO_BOOL_BV_INVERT_SOLVE (#11701)
ajreynol Mar 4, 2025
0d835cc
Print the result to the most recent solver's output stream (#11702)
daniel-larraz Mar 4, 2025
0337042
Fix JNI string conversion to handle Unicode surrogate pairs (#11693)
daniel-larraz Mar 4, 2025
704bd37
Add more regressions for proof holes (#11706)
ajreynol Mar 5, 2025
263e434
Setup infrastructure for necessary BV macro rewrites (#11707)
ajreynol Mar 5, 2025
cb8ccdd
Fix check for whether a regular expression is constant, guard cases o…
ajreynol Mar 5, 2025
de91651
Add necessary BV rewrites (#11662)
ajreynol Mar 6, 2025
acff956
quantifiers: Eliminate calls to NodeManager::currentNM() (#11711)
daniel-larraz Mar 6, 2025
c7d2d3c
Remove CONCAT_CONFLICT(_DEQ) rules (#11660)
ajreynol Mar 7, 2025
f97ed68
Simple fixes for projects issues (#11714)
ajreynol Mar 7, 2025
ff31255
Consolidate sets evaluation rules, implement in Eunoia (#11614)
ajreynol Mar 7, 2025
3f110c0
bv: Eliminate calls to NodeManager::currentNM() (#11712)
daniel-larraz Mar 7, 2025
3a8a70f
Fix numeric overflow case in strings rewriter (#11713)
ajreynol Mar 7, 2025
1cb2845
Remove DT_CLASH proof rule (#11629)
ajreynol Mar 7, 2025
94950d9
Add proof elaboration for And/Or/Xor simplify rules (#11720)
ajreynol Mar 10, 2025
8f8c70b
Avoid deadlock in HO model construction (#11723)
ajreynol Mar 10, 2025
4b5a522
Minor fixes and improvements for CPC Eunoia signature (#11719)
ajreynol Mar 10, 2025
fdce0c1
More updates to safe options (#11664)
ajreynol Mar 10, 2025
eccd313
Add elaboration for BV concat merge rules (#11727)
ajreynol Mar 11, 2025
ea756fb
Moved computation of relevant equivalence classes into a separate fun…
kartik-sabharwal Mar 11, 2025
576182a
strings: Refactor to not use NodeManager::currentNM() (#11717)
daniel-larraz Mar 11, 2025
74e6fa4
Move bitblasting to its own file in Eunoia signature (#11729)
ajreynol Mar 12, 2025
aba5d87
Add proof elaboration for BV concat extract rule (#11728)
ajreynol Mar 12, 2025
5ab6ba0
Do not throw an assertion failure when arithmetic model construction …
ajreynol Mar 12, 2025
057f782
Use arith substitution context for case of congruence manager conflic…
ajreynol Mar 12, 2025
d79b39e
Bump CaDiCaL to version 2.1.3. (#11716)
aniemetz Mar 12, 2025
1f2237a
cmake: Add JNI_HOME variable to specify the path to JNI libraries (#1…
daniel-larraz Mar 13, 2025
dc24c31
moved code that builds the theorem index to a separate function (#11731)
kartik-sabharwal Mar 13, 2025
4c64a77
Add proof elaboration for MultSltMult BV rewrite (#11732)
ajreynol Mar 13, 2025
743eaf6
Fix type rule for nested lambda, add regression (#11735)
ajreynol Mar 13, 2025
8cbd580
Refactor bound variable manager to use identifiers instead of attribu…
ajreynol Mar 13, 2025
c1bdfd3
Disable proof tester for regression. (#11741)
aniemetz Mar 14, 2025
497e984
Allow quoted symbols in indexed operators (#11738)
ajreynol Mar 17, 2025
b50dd17
Add more regressions from proof branch (#11739)
ajreynol Mar 17, 2025
b949f81
Add a static build option for the JNI library (#11730)
daniel-larraz Mar 17, 2025
82ff0f2
cmake: Compute absolute path to toolchain files (#11743)
daniel-larraz Mar 18, 2025
ab64642
Improve documentation of SatSolver interface. (#11745)
aniemetz Mar 18, 2025
4384596
cadical: Add more trace messages. (#11746)
aniemetz Mar 21, 2025
7bf5d3e
cadical: Add more stats. (#11747)
aniemetz Mar 21, 2025
46d49e4
Add macro elaboration for MACRO_BV_AND_OR_XOR_CONCAT_PULLUP (#11676)
ajreynol Mar 24, 2025
760e695
moved code that prints unproven conjectures to a separate function (#…
kartik-sabharwal Mar 24, 2025
5b954df
Fix prenex quant norm (#11755)
ajreynol Mar 26, 2025
81eb2b2
Add bitblasting utils to Eunoia signature (#11754)
ajreynol Mar 26, 2025
93e3ce3
More minor changes to BV rewriter for proofs (#11704)
ajreynol Mar 26, 2025
8594a8e
Include MinGW-w64 libraries in static JNI library (#11757)
daniel-larraz Mar 26, 2025
ba649b7
Add bv (un)signed inequality to bitblasting signature (#11759)
ajreynol Mar 27, 2025
a4f1c91
Miscellaneous remaining changes to strings signature (#11762)
ajreynol Mar 28, 2025
54148e5
Add side conditions for bitblasting addition and bitwise operators (#…
ajreynol Mar 31, 2025
3cb56d4
Treat higher-order equality as define-fun in non-incremental (#11766)
daniel-larraz Mar 31, 2025
34518c3
arith: Refactor to not use NodeManager::currentNM() (#11748)
daniel-larraz Mar 31, 2025
f82d140
Set CMAKE_POLICY_VERSION_MINIMUM for libpoly (#11768)
daniel-larraz Apr 1, 2025
3e9d3f2
Add Eunoia side conditions for bitblasting multiplication (#11765)
ajreynol Apr 1, 2025
05b0173
moved code that prints theorem index to a separate function (#11767)
kartik-sabharwal Apr 1, 2025
ff8459d
Add Eunoia definitions for bitblasting udiv/urem (#11770)
ajreynol Apr 1, 2025
3887500
[proofs] [alethe] Fix handling of Alethe skolem definitions (#11753)
HanielB Apr 1, 2025
fe6d0cc
Add remaining RARE rewrites for strings (#11569)
ajreynol Apr 2, 2025
3f84ac1
Disable unsat core on regression (#11775)
ajreynol Apr 2, 2025
6ec69ca
bags/sets/datatypes: Eliminate calls to NodeManager::currentNM() (#11…
daniel-larraz Apr 2, 2025
6826042
Add NodeManager pointer to SkolemManager (#11773)
daniel-larraz Apr 2, 2025
6ec5fb7
[proof log] Make sure we log lemmas from presolve() (#11631)
HanielB Apr 2, 2025
268f4fd
expr: Refactor to not use NodeManager::currentNM() (#11777)
daniel-larraz Apr 2, 2025
0e4aaa4
Add fine grained proof support for quantifiers variable eliminations …
ajreynol Apr 2, 2025
f086362
rewriter: Refactor to not use NodeManager::currentNM() (#11778)
daniel-larraz Apr 2, 2025
210436e
Add Eunoia definitions for BV multiplication overflow predicates (#11…
ajreynol Apr 2, 2025
19d1c1d
Add Eunoia bitblast signature for bvite, refactor constant (#11774)
ajreynol Apr 2, 2025
8bee87b
Minor changes and fixes to RARE rules (#11776)
ajreynol Apr 2, 2025
1267afa
preprocessing/printer/proof: Refactor to not use NodeManager::current…
daniel-larraz Apr 2, 2025
0c31f7b
Pass NodeManager pointer to getNullTerminator (#11781)
daniel-larraz Apr 3, 2025
9d99200
Miscellaneous changes to string rewriter (#11779)
ajreynol Apr 3, 2025
ee76c36
Add Eunoia signature for bitblasting shifts (#11783)
ajreynol Apr 3, 2025
9b8ccc5
Extend evaluator for applications of symbolic indexed operators (#11641)
ajreynol Apr 4, 2025
6dbf4a1
Finish Eunoia bitblasting signature and enable (#11785)
ajreynol Apr 4, 2025
0310120
Add Eunoia signature for (forthcoming) rule exists string length (#11…
ajreynol Apr 7, 2025
de09de5
Infrastructure and proof rules involving witness terms (#11536)
ajreynol Apr 7, 2025
1dd45a4
Refactor and minor improvements to MBQI (#11722)
ajreynol Apr 7, 2025
2ff1e17
More updates to safe options (#11761)
ajreynol Apr 7, 2025
87f0a8c
Add two rewrites to the string rewriter (#11794)
ajreynol Apr 8, 2025
e84b22e
Minor fixes for API proof include (#11795)
ajreynol Apr 8, 2025
7dfae14
Minor fix and addition to theory rewrite reconstruction (#11791)
ajreynol Apr 8, 2025
abce90d
Add Eunoia signature for (forthcoming) proof rule for invertibility c…
ajreynol Apr 8, 2025
9de6d5c
Ensure BV inequality mode is uniformly handled in CEGQI (#11784)
ajreynol Apr 8, 2025
ca7c8ef
Add simple missing BV rewrite rules (#11782)
ajreynol Apr 8, 2025
03ccb55
Add more proof regressions, focused on RARE coverage (#11793)
ajreynol Apr 8, 2025
f1557e1
Drop outdated LibPoly patch addressing a Clang warning (#11789)
daniel-larraz Apr 8, 2025
809fd63
smt driver: Terminate early if --preprocess-only enabled. (#11797)
mpreiner Apr 8, 2025
28f261c
Fix use of EVALUATE in proof elaboration (#11798)
ajreynol Apr 8, 2025
4a4ae29
[proofs] [alethe] Support symbolic indexed operators (#11804)
HanielB Apr 9, 2025
f3061f2
Fix a few missing cases of EVALUATE and ABSORB (#11787)
ajreynol Apr 10, 2025
480e465
Use standard Eunoia list in CPC utils (#11803)
ajreynol Apr 10, 2025
ed10fc9
Fully support standard SMT-LIB syntax for bitvector conversions (#11801)
ajreynol Apr 10, 2025
4218233
fp_word_blaster: Refactor to not use NodeManager::currentNM() (#11802)
daniel-larraz Apr 10, 2025
b75ba98
type_properties: Refactor to not use NodeManager::currentNM() (#11799)
daniel-larraz Apr 10, 2025
ae7d71d
theory: Eliminate calls to NodeManager::currentNM() (#11805)
daniel-larraz Apr 11, 2025
2ab8207
Add bag.some and bag.all (#11800)
mudathirmahgoub Apr 11, 2025
9ffcde2
smt: Refactor to not use NodeManager::currentNM() (#11806)
daniel-larraz Apr 11, 2025
4c1c4d4
[proofs] [alethe] Generalize ALPHA_EQUIV translation (#11236)
HanielB Apr 11, 2025
2545c1d
moved code that builds conjectures into a separate function (#11772)
kartik-sabharwal Apr 14, 2025
2777d65
Refactor arithmetic rewriter for ADD (#11764)
ajreynol Apr 14, 2025
59a6c1d
Clean up uses of quantifiers TermUtil (#11807)
ajreynol Apr 14, 2025
c47a96d
Mkexpr script conversion (#11176)
netolcc06 Apr 15, 2025
0f666c2
Remove obsolete fixmes. (#11813)
aniemetz Apr 15, 2025
c56a15e
Add missing check in oracle checker. (#11815)
aniemetz Apr 15, 2025
b1a267b
api: Add missing/refactor API checks. (#11814)
aniemetz Apr 15, 2025
cf8c5f3
NodeManager as a static thread_local singleton is no more. (#11816)
aniemetz Apr 16, 2025
8b63df8
Fix declarePool test in api_solver_black (#11818)
daniel-larraz Apr 16, 2025
881c037
Add arithmetic lemma proof reconstruction utility (#11453)
ajreynol Apr 17, 2025
5383729
Update Eunoia/CPC to new interface for declare-parameterized-const (#…
ajreynol Apr 17, 2025
80c7890
Eliminate singleton_elim from heads of RARE rules (#11589)
ajreynol Apr 17, 2025
31e4b60
Fix evaluator for BV repeat (#11822)
ajreynol Apr 18, 2025
86b529a
skeleton structure
limpa105 Apr 24, 2025
9d4770b
Remove workflow file to bypass PAT scope issue
limpa105 Apr 24, 2025
de1351b
Remove docs_cleanup.yml workflow to bypass PAT issue
limpa105 Apr 24, 2025
f7b5952
removing worklfows
limpa105 Apr 24, 2025
6923533
integer gb
limpa105 May 8, 2025
22e4682
reduction disequalities
limpa105 May 8, 2025
d19115f
tighten bounds
limpa105 May 8, 2025
f3181c9
added skolems
limpa105 May 8, 2025
cd87347
no split diseq
limpa105 May 8, 2025
71bb7ba
unsat due to bds
limpa105 May 8, 2025
d0ccae1
qf_nia fall back
limpa105 May 8, 2025
7acd0e0
eliminating segfault in bds
limpa105 May 13, 2025
7a2844d
better diseq encoding
limpa105 May 13, 2025
7a3f482
no order in integers
limpa105 May 13, 2025
87d69e1
trying unweighted
limpa105 May 13, 2025
cabbbf6
no print
limpa105 May 13, 2025
af2849c
set up for conflicts
limpa105 May 22, 2025
7534a45
removed print statments + put mm mod lower in pre processing
limpa105 May 30, 2025
bb02e6f
fixed interaction with simplex
limpa105 Jul 2, 2025
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
The diff you're trying to view is too large. We only load the first 3000 changed files.
2 changes: 1 addition & 1 deletion .github/ISSUE_TEMPLATE/bug_report.md
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ A clear and concise description of what the bug is.
**Operating system**: Name/version of the operating system.

**`configure.sh` options**
Paste `configure.sh` here.
Paste the options passed to `configure.sh` here.

**`configure.sh` output**
Paste the output of `configure.sh` here.
82 changes: 82 additions & 0 deletions .github/actions/add-jar/action.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,82 @@
name: Add self-contained JAR with the cvc5 Java bindings
description: |
Creates a JAR that includes the cvc5 Java bindings
along with the necessary native libraries.
inputs:
install-path:
description: path to the directory with installed artifacts
jar-libs-dir:
description: name of the directory that will contain the libraries within the JAR
jar-name:
description: target name of the JAR
github-token-latest:
description: token to upload JAR to latest
github-token-release:
description: token to upload JAR to release
shell:
default: bash
runs:
using: composite
steps:
- name: Create JAR contents (Linux)
if: runner.os == 'Linux'
shell: ${{ inputs.shell }}
run: |
echo "::group::Create JAR contents (Linux)"
mkdir ${{ inputs.jar-libs-dir }}
cd ${{ inputs.jar-libs-dir }}
cp ${{ inputs.install-path }}/lib/libcvc5jni.so .
echo "::endgroup::"

- name: Create JAR contents (macOS)
if: runner.os == 'macOS'
shell: ${{ inputs.shell }}
run: |
echo "::group::Create JAR contents (macOS)"
mkdir ${{ inputs.jar-libs-dir }}
cd ${{ inputs.jar-libs-dir }}
cp ${{ inputs.install-path }}/lib/libcvc5jni.dylib .
echo "::endgroup::"

- name: Create JAR contents (Windows)
if: runner.os == 'Windows'
shell: ${{ inputs.shell }}
run: |
echo "::group::Create JAR contents (Windows)"
mkdir ${{ inputs.jar-libs-dir }}
cd ${{ inputs.jar-libs-dir }}
cp ${{ inputs.install-path }}/bin/cvc5jni.dll .
echo "::endgroup::"

- name: Create JAR
shell: ${{ inputs.shell }}
run: |
echo "::group::Create JAR"
unzip ${{ inputs.install-path }}/share/java/cvc5.jar
jar cf ${{ inputs.jar-name }}.jar AUTHORS COPYING licenses io ${{ inputs.jar-libs-dir }}
echo "::endgroup::"

- name: Test JAR
shell: ${{ inputs.shell }}
run: |
javac -cp "${{ inputs.jar-name }}.jar" ./examples/api/java/QuickStart.java -d .
if [[ "$RUNNER_OS" == "Windows" ]]; then
java -cp "${{ inputs.jar-name }}.jar;." QuickStart
else
java -cp "${{ inputs.jar-name }}.jar:." QuickStart
fi
rm QuickStart.class

- name: Store to latest
if: github.ref == 'refs/heads/main'
uses: ./.github/actions/store-to-latest
with:
asset-filename: ${{ inputs.jar-name }}.jar
github-token: ${{ inputs.github-token-latest }}

- name: Store to release
if: startsWith(github.ref, 'refs/tags/')
uses: ./.github/actions/store-to-release
with:
asset-filename: ${{ inputs.jar-name }}.jar
github-token: ${{ inputs.github-token-release }}
109 changes: 29 additions & 80 deletions .github/actions/add-package/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -11,10 +11,15 @@ inputs:
description: token to upload package to release
shell:
default: bash
outputs:
install-path:
description: path to the installation directory
value: ${{ steps.create-zip.outputs.install-path }}
runs:
using: composite
steps:
- name: Create ZIP file
id: create-zip
shell: ${{ inputs.shell }}
run: |
echo "::group::Create ZIP file"
Expand All @@ -27,22 +32,34 @@ runs:
# They are built for testing purposes, but
# only work for the specific CI Python version.
rm -rf ${{ inputs.build-dir }}/install/lib/python*

# Copy COPYING file and licenses directory to install directory
cp COPYING ${{ inputs.build-dir }}/install/
rm -rf ${{ inputs.build-dir }}/install/lib/site-packages

if [[ "$RUNNER_OS" == "Windows" ]]; then
if [ -f ${{ inputs.build-dir }}/install/bin/libcvc5.dll ]; then
cp /mingw64/bin/libgcc_s_seh-1.dll ${{ inputs.build-dir }}/install/bin/
cp /mingw64/bin/libstdc++-6.dll ${{ inputs.build-dir }}/install/bin/
cp /mingw64/bin/libwinpthread-1.dll ${{ inputs.build-dir }}/install/bin/
else
cp /mingw64/lib/libgmp.a ${{ inputs.build-dir }}/install/lib/
fi
fi

# Copy AUTHORS and COPYING files and licenses directory to install directory
cp AUTHORS COPYING ${{ inputs.build-dir }}/install/
cp -r licenses ${{ inputs.build-dir }}/install/

# Create ZIP file
pushd ${{ inputs.build-dir }}
mv install ${{ inputs.package-name }}
echo "install-path=${{ inputs.build-dir }}/${{ inputs.package-name }}" >> $GITHUB_OUTPUT
zip -r ${{ inputs.package-name }} ${{ inputs.package-name }}
popd

# Move package to root directory
mv ${{ inputs.build-dir }}/${{ inputs.package-name }}.zip .
echo "::endgroup::"

- name: install pyGithub
- name: Install pyGithub
shell: ${{ inputs.shell }}
run: |
# Upgrading pyopenssl resolves the following error:
Expand All @@ -53,82 +70,14 @@ runs:

- name: Store to latest
if: github.ref == 'refs/heads/main'
shell: 'python3 {0}'
env:
GITHUB_TOKEN: ${{ inputs.github-token-latest }}
PACKAGE: ${{ inputs.package-name }}.zip
run: |
import datetime
import os
from github import Github

sha = os.getenv('GITHUB_SHA')

gh = Github(os.getenv('GITHUB_TOKEN'))
repo = gh.get_repo(os.getenv('GITHUB_REPOSITORY'))

try:
ref = repo.get_git_ref('tags/latest')
# update "latest" to current commit if sha changed
if ref.object.sha != sha:
ref.edit(sha)
except:
print('tag `latest` does not exist.')
exit

try:
rel = repo.get_release('latest')
except:
print('New `latest` release')
rel = repo.create_git_release('latest', 'latest', 'Latest builds')

# generate new filename
package = os.getenv('PACKAGE')
name,ext = os.path.splitext(package)
curtime = repo.get_git_commit(sha).committer.date.strftime('%Y-%m-%d')
samedayprefix = '{}-{}-'.format(name, curtime)
filename = '{}-{}-{}{}'.format(name, curtime, sha[:7], ext)

# prune old commits
assets = list(rel.get_assets())
assets.sort(key=lambda x: x.created_at, reverse=True)

for cnt,asset in enumerate(assets):
delete = False
# We generate 10 artifacts per build:
# {Linux, Linux-arm64, macOS, macOS-arm64, Windows} * {static, shared}
if cnt >= 20: # Keep at most 2 builds
delete = True
if asset.name.startswith(samedayprefix):
delete = True
# convert to timezone-aware datetime
age = datetime.datetime.now().replace(tzinfo=datetime.timezone.utc) - asset.created_at
if age.days > 7:
delete = True
if delete:
asset.delete_asset()

# upload as asset with proper name
rel.upload_asset(package, name=filename)
uses: ./.github/actions/store-to-latest
with:
asset-filename: ${{ inputs.package-name }}.zip
github-token: ${{ inputs.github-token-latest }}

- name: Store to release
if: startsWith(github.ref, 'refs/tags/')
shell: 'python3 {0}'
env:
GITHUB_TOKEN: ${{ inputs.github-token-release }}
PACKAGE: ${{ inputs.package-name }}.zip
run: |
import os
from github import Github

refname = os.getenv('GITHUB_REF_NAME')
gh = Github(os.getenv('GITHUB_TOKEN'))
repo = gh.get_repo(os.getenv('GITHUB_REPOSITORY'))
try:
rel = repo.get_release(refname)
except:
print("New release from " + refname)
ref = repo.get_git_ref('tags/' + refname)
commit = repo.get_git_commit(ref.object.sha)
rel = repo.create_git_release(refname, refname, commit.message)
rel.upload_asset(os.getenv('PACKAGE'))
uses: ./.github/actions/store-to-release
with:
asset-filename: ${{ inputs.package-name }}.zip
github-token: ${{ inputs.github-token-release }}
22 changes: 4 additions & 18 deletions .github/actions/configure-and-build/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -45,12 +45,7 @@ runs:
-DCMAKE_CXX_COMPILER_LAUNCHER=ccache -DCMAKE_C_COMPILER_LAUNCHER=ccache

cd build-shared/ && pwd=$(pwd)
if [[ "$RUNNER_OS" == "Windows" ]]; then
ccache --set-config="base_dir=$pwd"
else
# can not use `ccache --set-config=base_dir=` due to ccache bug, fixed with 3.7.10
$SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir = $pwd" $CCACHE_CONFIGPATH
fi
ccache --set-config="base_dir=$pwd"

make -j${{ env.num_proc }}

Expand All @@ -66,16 +61,11 @@ runs:
run: |
echo "::group::Static build"
${{ inputs.configure-env }} ./configure.sh ${{ inputs.configure-config }} \
--prefix=$(pwd)/build-static/install --werror --static --name=build-static --no-java-bindings \
--prefix=$(pwd)/build-static/install --werror --static --name=build-static \
-DCMAKE_CXX_COMPILER_LAUNCHER=ccache -DCMAKE_C_COMPILER_LAUNCHER=ccache

cd build-static/ && pwd=$(pwd)
if [[ "$RUNNER_OS" == "Windows" ]]; then
ccache --set-config="base_dir=$pwd"
else
# can not use `ccache --set-config=base_dir=` due to ccache bug, fixed with 3.7.10
$SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir = $pwd" $CCACHE_CONFIGPATH
fi
ccache --set-config="base_dir=$pwd"

make -j${{ env.num_proc }}

Expand All @@ -90,11 +80,7 @@ runs:
shell: ${{ inputs.shell }}
run: |
echo "::group::Reset ccache base_dir"
if [[ "$RUNNER_OS" == "Windows" ]]; then
ccache --set-config="base_dir="
else
$SED -i.orig -n -e '/^base_dir = /!p' -e "\$abase_dir =" $CCACHE_CONFIGPATH
fi
ccache --set-config="base_dir="
echo "::endgroup::"

- name: ccache Statistics
Expand Down
40 changes: 34 additions & 6 deletions .github/actions/install-dependencies/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,12 @@ inputs:
windows-build:
default: false
type: boolean
wasm-build:
default: false
type: boolean
shell:
default: bash

runs:
using: composite
steps:
Expand All @@ -27,7 +31,6 @@ runs:
libtinfo-dev \
libfl-dev
echo "SED=sed" >> $GITHUB_ENV
echo "CCACHE_CONFIGPATH=/home/runner/.ccache/ccache.conf" >> $GITHUB_ENV
echo "::endgroup::"

- name: Install software for cross-compiling for arm64 Linux
Expand Down Expand Up @@ -57,6 +60,21 @@ runs:
sudo update-alternatives --set x86_64-w64-mingw32-g++ /usr/bin/x86_64-w64-mingw32-g++-posix
echo "::endgroup::"

- name: Install software for WebAssembly compilation
# Boolean inputs are actually strings:
# https://github.com/actions/runner/issues/1483
if: inputs.wasm-build == 'true'
shell: bash
run: |
echo "::group::Install software for WebAssembly compilation"
sudo apt-get update
git clone https://github.com/emscripten-core/emsdk.git
cd emsdk/
./emsdk install '3.1.18'
./emsdk activate '3.1.18'
echo "$(pwd)" >> $GITHUB_PATH
echo "$(pwd)/upstream/emscripten" >> $GITHUB_PATH

- name: Install Windows software
if: runner.os == 'Windows' && inputs.windows-build == 'true'
uses: msys2/setup-msys2@v2
Expand All @@ -66,6 +84,7 @@ runs:
path-type: inherit
install: |
make
mingw-w64-x86_64-autotools
mingw-w64-x86_64-ccache
mingw-w64-x86_64-cmake
mingw-w64-x86_64-gcc
Expand All @@ -89,13 +108,14 @@ runs:
brew config
brew untap homebrew/core homebrew/cask
brew config

brew install \
if [[ $RUNNER_ARCH == "ARM64" ]]; then
AUTOTOOLS="autoconf libtool"
fi
brew install $AUTOTOOLS \
automake \
ccache \
pkgconfig \
gnu-sed
echo "SED=gsed" >> $GITHUB_ENV
echo "CCACHE_CONFIGPATH=/Users/runner/Library/Preferences/ccache/ccache.conf" >> $GITHUB_ENV
echo "num_proc=$(( $(sysctl -n hw.logicalcpu) + 1 ))" >> $GITHUB_ENV
echo "::endgroup::"

Expand All @@ -109,6 +129,14 @@ runs:
echo "$HOME/.venv/bin" >> $GITHUB_PATH
echo "::endgroup::"

# Required for the installation of Python bindings
- name: Upgrade Python pip
shell: ${{ inputs.shell }}
run: |
echo "::group::Upgrade Python pip"
python3 -m pip install --upgrade pip
echo "::endgroup::"

- name: Install software for documentation
if: inputs.with-documentation == 'true'
shell: ${{ inputs.shell }}
Expand All @@ -118,5 +146,5 @@ runs:
python3 -m pip install \
sphinx==7.1.2 \
sphinxcontrib-bibtex==2.5.0 sphinx-tabs==3.4.1 sphinx-rtd-theme==1.3.0 breathe==4.35.0 \
sphinxcontrib-programoutput==0.17
sphinxcontrib-programoutput==0.17 sphinxcontrib-googleanalytics==0.4
echo "::endgroup::"
9 changes: 8 additions & 1 deletion .github/actions/run-tests/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,12 @@ runs:
shell: ${{ inputs.shell }}
run: |
if [[ "${{ inputs.check-python-bindings }}" != "true" ]]; then exit 0; fi
export PYTHONPATH="$PYTHONPATH:$(dirname $(dirname $(find ${{ inputs.build-dir }}/install -name 'cvc5_python_base*')))"
PYTHON_MODULE_PATH="$(dirname $(dirname $(find ${{ inputs.build-dir }}/install -name 'cvc5_python_base*')))"
if [[ "$RUNNER_OS" == "Windows" ]]; then
export PYTHONPATH="$PYTHONPATH;$(cygpath -w $PYTHON_MODULE_PATH)"
else
export PYTHONPATH="$PYTHONPATH:$PYTHON_MODULE_PATH"
fi
python3 -c "import cvc5"

- name: Check Examples
Expand All @@ -59,6 +64,8 @@ runs:
export PATH="${{ inputs.build-dir }}/install/bin:$PATH"
export CMAKE_GENERATOR="MSYS Makefiles"
fi
export CFLAGS=-Werror
export CXXFLAGS=-Werror
cmake .. -DCMAKE_PREFIX_PATH=${{ inputs.build-dir }}/install/lib/cmake \
-DPython_EXECUTABLE=$(command -v python3)
make -j${{ env.num_proc }}
Expand Down
Loading