projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
fix incorrect 64-bit detection -- powerpc64le doesn't end in 64 but is 64-bit
2022-04-05
Andrew Reynolds
Make inst constant attribute robust to purification...
commit
|
commitdiff
|
tree
2022-04-05
Andrew Reynolds
Be permissive for subtyping in function definitions...
commit
|
commitdiff
|
tree
2022-04-04
Andrew Reynolds
Rename getInstantiatedConstructorTerm to getInstantiatedTerm...
commit
|
commitdiff
|
tree
2022-04-04
Andrew Reynolds
Use raw symbols in proofs (#8550)
commit
|
commitdiff
|
tree
2022-04-04
Andrew Reynolds
Fix for get-value with empty uninterpreted sort domain...
commit
|
commitdiff
|
tree
2022-04-02
Andrew Reynolds
Rename mkSygusGrammar to mkGrammar (#8544)
commit
|
commitdiff
|
tree
2022-04-02
Andrew Reynolds
Remove variant of mkDatatypeDecl with one sort parameter...
commit
|
commitdiff
|
tree
2022-04-02
Andrew Reynolds
Ignore irrelevant exponential terms (#8534)
commit
|
commitdiff
|
tree
2022-04-02
Andrew Reynolds
Require that used model values are constant in CEGQI...
commit
|
commitdiff
|
tree
2022-04-02
Andrew Reynolds
Add a few miscellaneous pieces of documentation (#8533)
commit
|
commitdiff
|
tree
2022-04-02
Andrew Reynolds
Add more explanations in the API (#8493)
commit
|
commitdiff
|
tree
2022-04-01
Andrew Reynolds
Simplifications to the datatypes API (#8511)
commit
|
commitdiff
|
tree
2022-04-01
Andrew Reynolds
Internal simplifications to constructing datatypes...
commit
|
commitdiff
|
tree
2022-04-01
Andrew Reynolds
Fix sygus-inst when combined with bounded string quantifiers...
commit
|
commitdiff
|
tree
2022-03-31
Andrew Reynolds
Handled quoted symbols in indexed operators (#8491)
commit
|
commitdiff
|
tree
2022-03-31
Andrew Reynolds
Disable minisat variable elimination when a parametric...
commit
|
commitdiff
|
tree
2022-03-31
Andrew Reynolds
Do not export dt.size (#8483)
commit
|
commitdiff
|
tree
2022-03-31
Andrew Reynolds
Fix check for whether PI is reduced (#8485)
commit
|
commitdiff
|
tree
2022-03-31
Andrew Reynolds
Fix lower vs upper bound issue for eager RE conflicts...
commit
|
commitdiff
|
tree
2022-03-31
Andrew Reynolds
Fix non-termination in the strings rewriter (#8438)
commit
|
commitdiff
|
tree
2022-03-31
Andrew Reynolds
Fix case of Boolean skolem for ground term E-matching...
commit
|
commitdiff
|
tree
2022-03-30
Andrew Reynolds
Fix policy for purifying arguments of exp (#8416)
commit
|
commitdiff
|
tree
2022-03-30
Andrew Reynolds
Fixes for sygus-inst (#8448)
commit
|
commitdiff
|
tree
2022-03-30
Andrew Reynolds
Fix subtype issue in cegqi arithmetic (#8440)
commit
|
commitdiff
|
tree
2022-03-30
Andrew Reynolds
Change tuple tokens and update datatypes theory ref...
commit
|
commitdiff
|
tree
2022-03-30
Andrew Reynolds
Add LFSC to internal proof checker (#8442)
commit
|
commitdiff
|
tree
2022-03-29
Andrew Reynolds
Make ensureTermSort private (#8436)
commit
|
commitdiff
|
tree
2022-03-29
Andrew Reynolds
Add information for cardinality constraint to the API...
commit
|
commitdiff
|
tree
2022-03-29
Andrew Reynolds
Make ProofNodeManager mkScope more robust (#8435)
commit
|
commitdiff
|
tree
2022-03-29
Andrew Reynolds
Fix issue related to use of Boolean term variable for...
commit
|
commitdiff
|
tree
2022-03-28
Andrew Reynolds
Mark more methods as experimental (#8426)
commit
|
commitdiff
|
tree
2022-03-28
Andrew Reynolds
Fix synth result python unit test (#8418)
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
Fix spurious assertion failure (#8404)
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
Throw logic exception for set.map (#8403)
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
More minor cleaning of options (#8401)
commit
|
commitdiff
|
tree
2022-03-26
Andrew Reynolds
Fixes for API kind documentation (#8397)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Update checkSynth and checkSynthNext to return SynthResult...
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Change output of abduction/interpolation for failed...
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Fixes related to set defaults for sygus/proofs (#8395)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Properly guard commands in the SyGuS API (#8390)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Recategorize options (#8386)
commit
|
commitdiff
|
tree
2022-03-25
Andrew Reynolds
Fixes for theory reference for datatypes (#8380)
commit
|
commitdiff
|
tree
2022-03-24
Andrew Reynolds
Minor updates for quantifiers options (#8385)
commit
|
commitdiff
|
tree
2022-03-24
Andrew Reynolds
Standardize more instances of skolems (#8351)
commit
|
commitdiff
|
tree
2022-03-24
Andrew Reynolds
Fix a couple of parse error messages for sygus (#8381)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Clean options (#8309)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Add SynthResult to the API (#8370)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Make IDOF_MAX rewrite only apply when all children...
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Add internal synth result class (#8352)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Initial documentation on LFSC (#8365)
commit
|
commitdiff
|
tree
2022-03-23
Andrew Reynolds
Fix non-termination issue in sygus enumerator (#8340)
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Change null terminator for regular expression intersection...
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Updates for the theory reference for separation logic...
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Fixes for witness terms appearing in CEGQI instantiations...
commit
|
commitdiff
|
tree
2022-03-22
Andrew Reynolds
Refactor result class (#8313)
commit
|
commitdiff
|
tree
2022-03-21
Andrew Reynolds
Fix return value for candidate rewrite database (#8354)
commit
|
commitdiff
|
tree
2022-03-21
Andrew Reynolds
Fix LFSC conversion for seq unit (#8353)
commit
|
commitdiff
|
tree
2022-03-21
Andrew Reynolds
Fix learned literals for top-level AND (#8336)
commit
|
commitdiff
|
tree
2022-03-17
Andrew Reynolds
Update care graph computations to use standard node...
commit
|
commitdiff
|
tree
2022-03-16
Andrew Reynolds
Fix getModelValue for arithmetic (#8316)
commit
|
commitdiff
|
tree
2022-03-16
Andrew Reynolds
Ensure trusted steps are given for skolem lemmas when...
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Make learned literal computation more robust (#8308)
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Add unit test involving seq concat term (#8257)
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Fix issues involving multiple sources of model substitutions...
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Properly guard sort instantiate (#8247)
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Remove unecessary separation logic options (#8269)
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Fix to consider leafs of theory sets to be variables...
commit
|
commitdiff
|
tree
2022-03-15
Andrew Reynolds
Simplify reductions for set and bag choose (#8304)
commit
|
commitdiff
|
tree
2022-03-14
Andrew Reynolds
Fixes for skolem definition management (#8301)
commit
|
commitdiff
|
tree
2022-03-14
Andrew Reynolds
Remove unecessary methods from the API (#8260)
commit
|
commitdiff
|
tree
2022-03-14
Andrew Reynolds
Add rewrite for allchar beneath union + star (#8299)
commit
|
commitdiff
|
tree
2022-03-14
Andrew Reynolds
Run preprocess rewrite on equalities until fixed point...
commit
|
commitdiff
|
tree
2022-03-13
Andrew Reynolds
Minor sync from proof-new (#8293)
commit
|
commitdiff
|
tree
2022-03-12
Andrew Reynolds
Introduce new splitting inference in sets + cardinality...
commit
|
commitdiff
|
tree
2022-03-12
Andrew Reynolds
Add algorithm for finding pairs of paths in a node...
commit
|
commitdiff
|
tree
2022-03-12
Andrew Reynolds
Improvements for sygus query generation (#8224)
commit
|
commitdiff
|
tree
2022-03-12
Andrew Reynolds
Document type rules (#8248)
commit
|
commitdiff
|
tree
2022-03-12
Andrew Reynolds
Always ensure literal when requiring phase via inference...
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Remove old decision justification heurstic (#8275)
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Update abduction and interpolation API to not use pass...
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Fix maximum value for pedantic proof level (#8246)
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Guard parametric datatypes instantiated by non-first...
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Remove unecessary CEGQI options (#8281)
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Consider APPLY_CONSTRUCTOR applied to values to be...
commit
|
commitdiff
|
tree
2022-03-11
Andrew Reynolds
Fix reduction for arc trig functions (#8289)
commit
|
commitdiff
|
tree
2022-03-10
Andrew Reynolds
Fix issue with subtyping from set membership in models...
commit
|
commitdiff
|
tree
2022-03-10
Andrew Reynolds
Fix theoryOf call in get equality status (#8279)
commit
|
commitdiff
|
tree
2022-03-10
Andrew Reynolds
Eliminate unecessary datatype options (#8280)
commit
|
commitdiff
|
tree
2022-03-10
Andrew Reynolds
Add output -o pre-asserts (#8270)
commit
|
commitdiff
|
tree
2022-03-10
Andrew Reynolds
Disable timing out regressions (#8273)
commit
|
commitdiff
|
tree
2022-03-09
Andrew Reynolds
Change interface for printing instantiations in the...
commit
|
commitdiff
|
tree
2022-03-09
Andrew Reynolds
Use expression mining independent of whether sygus...
commit
|
commitdiff
|
tree
2022-03-09
Andrew Reynolds
Add REGEXP_ALL kind to API (#8264)
commit
|
commitdiff
|
tree
2022-03-09
Andrew Reynolds
Add regression for fixed issue 6700 (#8265)
commit
|
commitdiff
|
tree
2022-03-09
Andrew Reynolds
Eliminate the APPLY_SELECTOR_TOTAL kind (#8266)
commit
|
commitdiff
|
tree
2022-03-08
Andrew Reynolds
Do not expand APPLY_SELECTOR (#8174)
commit
|
commitdiff
|
tree
2022-03-08
Andrew Reynolds
Guard another case of non-termination in quantifiers...
commit
|
commitdiff
|
tree
2022-03-08
Andrew Reynolds
Fixes and additions to LFSC signature (#8205)
commit
|
commitdiff
|
tree
2022-03-08
Andrew Reynolds
Eliminate shadowing in the quantifiers rewriter (#8244)
commit
|
commitdiff
|
tree
2022-03-08
Andrew Reynolds
Add unit for fixed project issue (#8253)
commit
|
commitdiff
|
tree
next