projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2022-03-05
Gereon Kremer
Add regressions for fixed issue (#8237)
commit
|
commitdiff
|
tree
2022-03-05
Andrew Reynolds
Enable NL tangent planes by default (#8233)
commit
|
commitdiff
|
tree
2022-03-04
mudathirmahgoub
Fix bag.map upwards inferences (#8232)
commit
|
commitdiff
|
tree
2022-03-04
Gereon Kremer
Add unit test for fixed issue (#8235)
commit
|
commitdiff
|
tree
2022-03-04
Gereon Kremer
Remove spurious assertion in linear solver (#8231)
commit
|
commitdiff
|
tree
2022-03-04
Gereon Kremer
Guard recursion into terms during substitution in arith...
commit
|
commitdiff
|
tree
2022-03-04
Andrew Reynolds
Fix rewrite rule synthesis for 0-ary operators (#8221)
commit
|
commitdiff
|
tree
2022-03-04
Andrew Reynolds
Logic exception when using solution filtering for non...
commit
|
commitdiff
|
tree
2022-03-04
Gereon Kremer
Only build wheels nightly and for releases (#8223)
commit
|
commitdiff
|
tree
2022-03-04
Andrew Reynolds
Add regressions for fixed projects issues (#8228)
commit
|
commitdiff
|
tree
2022-03-04
Andrew Reynolds
Add support for get learned literals in the API (#8099)
commit
|
commitdiff
|
tree
2022-03-03
Andrew Reynolds
Fix datatype declaration printing in LFSC printer ...
commit
|
commitdiff
|
tree
2022-03-03
Gereon Kremer
Build python wheels in our CI (#8087)
commit
|
commitdiff
|
tree
2022-03-03
Andrew Reynolds
Generalize LFSC string signature to sequences (#8220)
commit
|
commitdiff
|
tree
2022-03-03
Lachnitt
[proofs] Alethe: Removed Steps that are Double-Printed...
commit
|
commitdiff
|
tree
2022-03-03
Andrew Reynolds
Throw logic exception if a transcendental function...
commit
|
commitdiff
|
tree
2022-03-03
Andrew Reynolds
Add regression for fixed issue (#8213)
commit
|
commitdiff
|
tree
2022-03-03
Andrew Reynolds
Improve error for higher-order logic (#8207)
commit
|
commitdiff
|
tree
2022-03-03
Mathias Preiner
cmake: Fix murxla setup. (#8215)
commit
|
commitdiff
|
tree
2022-03-03
Gereon Kremer
Integrate pythonic api (#8131)
commit
|
commitdiff
|
tree
2022-03-03
Gereon Kremer
Fix rewriting of mixed-integer atoms (#8214)
commit
|
commitdiff
|
tree
2022-03-02
Andrew Reynolds
Fix issue with dropping non-reduced sine terms (#8211)
commit
|
commitdiff
|
tree
2022-03-02
Andrew Reynolds
Fix models involving cardinality of sets of finite...
commit
|
commitdiff
|
tree
2022-03-02
Andrew Reynolds
Always purify universe from set minus (#8201)
commit
|
commitdiff
|
tree
2022-03-02
Andrew Reynolds
Eliminate CDHashMap::insertAtContextLevelZero (#8173)
commit
|
commitdiff
|
tree
2022-03-02
Andrew Reynolds
Fix incorrect assertion in prop engine proofs (#8204)
commit
|
commitdiff
|
tree
2022-03-02
Andrew Reynolds
Clean usage of options in regressions (#8190)
commit
|
commitdiff
|
tree
2022-03-02
Andrew Reynolds
Improve error message when not using strings-exp (...
commit
|
commitdiff
|
tree
2022-03-02
Gereon Kremer
Move libpoly <-> CoCoA conversion to new utility (...
commit
|
commitdiff
|
tree
2022-03-02
Gereon Kremer
Refactor rewriting of arithmetic division (#8195)
commit
|
commitdiff
|
tree
2022-03-02
Andrew Reynolds
Add utility to access how to print floating point ...
commit
|
commitdiff
|
tree
2022-03-02
Andrew Reynolds
Make blockModelValues robust to non-closed enumerable...
commit
|
commitdiff
|
tree
2022-03-02
Andrew Reynolds
Add regressions for fixed issues (#8202)
commit
|
commitdiff
|
tree
2022-03-02
Gereon Kremer
Prune spurious roots in lazard evaluation of coverings...
commit
|
commitdiff
|
tree
2022-03-02
Gereon Kremer
Add standard theories to documentation (#8192)
commit
|
commitdiff
|
tree
2022-03-01
Andrew Reynolds
Fix issue involving dropped purification lemmas for...
commit
|
commitdiff
|
tree
2022-03-01
Andrew Reynolds
Do not use sygus evaluation functions in sygus-inst...
commit
|
commitdiff
|
tree
2022-03-01
Andrew Reynolds
Disable regression (#8191)
commit
|
commitdiff
|
tree
2022-03-01
Andres Noetzli
[BV] Fix rewriter policy for `bvneg` (#8196)
commit
|
commitdiff
|
tree
2022-03-01
Andrew Reynolds
Fix lambda lifting + proofs (#8152)
commit
|
commitdiff
|
tree
2022-03-01
Andres Noetzli
Remove unused data members from `TheoryArrays` (#8197)
commit
|
commitdiff
|
tree
2022-03-01
Gereon Kremer
Rename cad to coverings (#8187)
commit
|
commitdiff
|
tree
2022-02-28
Andres Noetzli
[Seq/Model] Do not enumerate elements of constants...
commit
|
commitdiff
|
tree
2022-02-28
Gereon Kremer
Refactor rewriting of arithmetic atoms (#8175)
commit
|
commitdiff
|
tree
2022-02-28
Andrew Reynolds
Fix special casing for PI in model value (#8189)
commit
|
commitdiff
|
tree
2022-02-28
Andrew Reynolds
Preserve model values for exact sine points (#8188)
commit
|
commitdiff
|
tree
2022-02-28
Andrew Reynolds
Track names for witness terms in model (#8184)
commit
|
commitdiff
|
tree
2022-02-28
Andrew Reynolds
Add two reduction schemas for sin terms (#8171)
commit
|
commitdiff
|
tree
2022-02-28
Andres Noetzli
Remove broken/unused `--mmap` option (#8178)
commit
|
commitdiff
|
tree
2022-02-28
Gereon Kremer
Add scripts to build python wheels (#8132)
commit
|
commitdiff
|
tree
2022-02-28
Gereon Kremer
Refactor rewriting of arithmetic leafs (#8177)
commit
|
commitdiff
|
tree
2022-02-28
Gereon Kremer
Refactor rewriting of arithmetic addition (#8180)
commit
|
commitdiff
|
tree
2022-02-25
Andrew Reynolds
Consider PI to be a model value (#8176)
commit
|
commitdiff
|
tree
2022-02-25
Andrew Reynolds
Syntax fixes for LFSC signature (#8172)
commit
|
commitdiff
|
tree
2022-02-25
Gereon Kremer
Add utilities to rewrite atoms for the arithmetic rewri...
commit
|
commitdiff
|
tree
2022-02-25
Gereon Kremer
Refactor rewriting of arithmetic negation and subtracti...
commit
|
commitdiff
|
tree
2022-02-25
Gereon Kremer
Slightly refactor arithmetic rewriting for extended...
commit
|
commitdiff
|
tree
2022-02-25
Andrew Reynolds
Fix non-termination in quantifiers rewriter (#8165)
commit
|
commitdiff
|
tree
2022-02-25
Andrew Reynolds
Simplify and fix how purified terms are managed in...
commit
|
commitdiff
|
tree
2022-02-25
Andrew Reynolds
Fix dropped bounds on PI (#8164)
commit
|
commitdiff
|
tree
2022-02-25
Andrew Reynolds
Remove approximations infrastructure from model (#8166)
commit
|
commitdiff
|
tree
2022-02-25
Andrew Reynolds
Remove spurious assertion involving constants for argum...
commit
|
commitdiff
|
tree
2022-02-25
Andrew Reynolds
Make quantifiers terminate if it detects a (duplicate...
commit
|
commitdiff
|
tree
2022-02-25
Andrew Reynolds
Add regression for fixed transcendental regression...
commit
|
commitdiff
|
tree
2022-02-25
Andrew Reynolds
Consolidate extended rewrite preprocessing modes (...
commit
|
commitdiff
|
tree
2022-02-25
Andres Noetzli
[Python API] Add support for blocking models (#8134)
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Ensure variables are constrained in model when equal...
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Make model builder robust to multiple value-like terms...
commit
|
commitdiff
|
tree
2022-02-24
Gereon Kremer
Improve error message for missing options include ...
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Make sine solver sound with respect to region boundarie...
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Check for free variables in several SolverEngine calls...
commit
|
commitdiff
|
tree
2022-02-24
Gereon Kremer
Get rid of some static objects in arithmetic theory...
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Make uninterpreted sort owner non-static (#8144)
commit
|
commitdiff
|
tree
2022-02-24
Andrew Reynolds
Add regression for some fixed array issues (#8145)
commit
|
commitdiff
|
tree
2022-02-23
Gereon Kremer
Add two regressions related to RAN models (#8142)
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Allow elimination of unevaluated terms by default ...
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Further relax what is considered a value in the model...
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Do not insist that entries for UF are constant in FMF...
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Eliminate match from LFSC proofs (#8090)
commit
|
commitdiff
|
tree
2022-02-23
Gereon Kremer
Remove long obsolete unsafe interrupt exception (#8139)
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Option exception when incompatible with proofs (#8064)
commit
|
commitdiff
|
tree
2022-02-23
Gereon Kremer
Fix creation of RAN from non-dyadic rational (#8138)
commit
|
commitdiff
|
tree
2022-02-23
Gereon Kremer
Fix icp candidate parsing (#8137)
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Properly sanatize user names in LFSC (#8080)
commit
|
commitdiff
|
tree
2022-02-23
Andres Noetzli
[Rewriter] Do not attempt to rewrite constants (#8061)
commit
|
commitdiff
|
tree
2022-02-23
Gereon Kremer
Fix pruning of covering intervals in proofs (#8084)
commit
|
commitdiff
|
tree
2022-02-23
Gereon Kremer
Refactor multiplication in arithmetic rewriter (#7965)
commit
|
commitdiff
|
tree
2022-02-23
Andrew Reynolds
Fix issue in datatypes care graph computation involving...
commit
|
commitdiff
|
tree
2022-02-22
Andrew Reynolds
Support some cases of isConst for regular expressions...
commit
|
commitdiff
|
tree
2022-02-22
Andrew Reynolds
Remove refineConflicts option (#8129)
commit
|
commitdiff
|
tree
2022-02-22
Andrew Reynolds
Change inference scheme in transcendentals to rewrite...
commit
|
commitdiff
|
tree
2022-02-22
Andrew Reynolds
Relax what is generated in the model from NL (#8113)
commit
|
commitdiff
|
tree
2022-02-22
vinciusb
[proofs] [dot] Enable DAG and tree printing with dot...
commit
|
commitdiff
|
tree
2022-02-21
Andrew Reynolds
Fixes and additions for LFSC signatures (#8120)
commit
|
commitdiff
|
tree
2022-02-18
Andrew Reynolds
Add unit test for fixed issue with get-difficulty ...
commit
|
commitdiff
|
tree
2022-02-18
Andrew Reynolds
Throw option exceptions when combining input conversion...
commit
|
commitdiff
|
tree
2022-02-18
Andrew Reynolds
Add well formed term check to solver engine (#8056)
commit
|
commitdiff
|
tree
2022-02-18
Andres Noetzli
Improve `STRINGS_ARRAY_UPDATE_BOUND` inference (#8123)
commit
|
commitdiff
|
tree
2022-02-18
Andrew Reynolds
Make spurious assertion into warning (#8051)
commit
|
commitdiff
|
tree
2022-02-18
Andres Noetzli
Fix `STRINGS_ARRAY_NTH_UPDATE` inference (#8121)
commit
|
commitdiff
|
tree
next