projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Simplify reductions for set and bag choose (#8304)
[cvc5.git]
/
src
/
2022-03-15
Andrew Reynolds
Simplify reductions for set and bag choose (#8304)
tree
|
commitdiff
2022-03-15
Aina Niemetz
Rename TO_FP operator kinds. (#8285)
tree
|
commitdiff
2022-03-14
Andrew Reynolds
Fixes for skolem definition management (#8301)
tree
|
commitdiff
2022-03-14
Andrew Reynolds
Remove unecessary methods from the API (#8260)
tree
|
commitdiff
2022-03-14
Andrew Reynolds
Add rewrite for allchar beneath union + star (#8299)
tree
|
commitdiff
2022-03-14
Andrew Reynolds
Run preprocess rewrite on equalities until fixed point...
tree
|
commitdiff
2022-03-12
Andrew Reynolds
Introduce new splitting inference in sets + cardinality...
tree
|
commitdiff
2022-03-12
Andrew Reynolds
Add algorithm for finding pairs of paths in a node...
tree
|
commitdiff
2022-03-12
Andrew Reynolds
Improvements for sygus query generation (#8224)
tree
|
commitdiff
2022-03-12
Andrew Reynolds
Document type rules (#8248)
tree
|
commitdiff
2022-03-12
Andrew Reynolds
Always ensure literal when requiring phase via inferenc...
tree
|
commitdiff
2022-03-11
Andres Noetzli
[API/Python] Add support for `Solver::getModel()` ...
tree
|
commitdiff
2022-03-11
Aina Niemetz
api: Make checks header private. (#8283)
tree
|
commitdiff
2022-03-11
Andrew Reynolds
Remove old decision justification heurstic (#8275)
tree
|
commitdiff
2022-03-11
Andrew Reynolds
Update abduction and interpolation API to not use pass...
tree
|
commitdiff
2022-03-11
Andrew Reynolds
Fix maximum value for pedantic proof level (#8246)
tree
|
commitdiff
2022-03-11
Andrew Reynolds
Guard parametric datatypes instantiated by non-first...
tree
|
commitdiff
2022-03-11
Andrew Reynolds
Remove unecessary CEGQI options (#8281)
tree
|
commitdiff
2022-03-11
Andrew Reynolds
Consider APPLY_CONSTRUCTOR applied to values to be...
tree
|
commitdiff
2022-03-11
Andrew Reynolds
Fix reduction for arc trig functions (#8289)
tree
|
commitdiff
2022-03-11
Andres Noetzli
Refactor kinds parser (#8287)
tree
|
commitdiff
2022-03-10
Andrew Reynolds
Fix issue with subtyping from set membership in models...
tree
|
commitdiff
2022-03-10
Andrew Reynolds
Fix theoryOf call in get equality status (#8279)
tree
|
commitdiff
2022-03-10
Andrew Reynolds
Eliminate unecessary datatype options (#8280)
tree
|
commitdiff
2022-03-10
mudathirmahgoub
Fix cvc5-projects issue 475 (#8278)
tree
|
commitdiff
2022-03-10
Andrew Reynolds
Add output -o pre-asserts (#8270)
tree
|
commitdiff
2022-03-09
Gereon Kremer
Rename expert statistics to internal, add documentation...
tree
|
commitdiff
2022-03-09
Gereon Kremer
Clear obsolete pending lemmas in arithmetic (#8236)
tree
|
commitdiff
2022-03-09
Andrew Reynolds
Change interface for printing instantiations in the...
tree
|
commitdiff
2022-03-09
Andrew Reynolds
Use expression mining independent of whether sygus...
tree
|
commitdiff
2022-03-09
Andrew Reynolds
Add REGEXP_ALL kind to API (#8264)
tree
|
commitdiff
2022-03-09
Andrew Reynolds
Eliminate the APPLY_SELECTOR_TOTAL kind (#8266)
tree
|
commitdiff
2022-03-08
Andrew Reynolds
Do not expand APPLY_SELECTOR (#8174)
tree
|
commitdiff
2022-03-08
Andres Noetzli
[API/Python] Add support for `Solver::getProof()` ...
tree
|
commitdiff
2022-03-08
Andrew Reynolds
Guard another case of non-termination in quantifiers...
tree
|
commitdiff
2022-03-08
Andrew Reynolds
Fixes and additions to LFSC signature (#8205)
tree
|
commitdiff
2022-03-08
Andrew Reynolds
Eliminate shadowing in the quantifiers rewriter (#8244)
tree
|
commitdiff
2022-03-07
Andres Noetzli
Update documentation of `Solver::getUnsatCore()` (...
tree
|
commitdiff
2022-03-07
Gereon Kremer
Fix docs warnings (#8019)
tree
|
commitdiff
2022-03-07
Andrew Reynolds
Proper error message for non-first-class sets (#8245)
tree
|
commitdiff
2022-03-07
Gereon Kremer
Try harder to show that a RAN is rational (#8230)
tree
|
commitdiff
2022-03-06
Andres Noetzli
Disallow models with `--arrays-weak-equiv` (#8217)
tree
|
commitdiff
2022-03-05
Andrew Reynolds
Make seq.unit robust wrt subtyping (#8209)
tree
|
commitdiff
2022-03-05
Andrew Reynolds
Enable NL tangent planes by default (#8233)
tree
|
commitdiff
2022-03-04
mudathirmahgoub
Fix bag.map upwards inferences (#8232)
tree
|
commitdiff
2022-03-04
Gereon Kremer
Remove spurious assertion in linear solver (#8231)
tree
|
commitdiff
2022-03-04
Gereon Kremer
Guard recursion into terms during substitution in arith...
tree
|
commitdiff
2022-03-04
Andrew Reynolds
Fix rewrite rule synthesis for 0-ary operators (#8221)
tree
|
commitdiff
2022-03-04
Andrew Reynolds
Logic exception when using solution filtering for non...
tree
|
commitdiff
2022-03-04
Andrew Reynolds
Add support for get learned literals in the API (#8099)
tree
|
commitdiff
2022-03-03
Andrew Reynolds
Fix datatype declaration printing in LFSC printer ...
tree
|
commitdiff
2022-03-03
Andrew Reynolds
Generalize LFSC string signature to sequences (#8220)
tree
|
commitdiff
2022-03-03
Lachnitt
[proofs] Alethe: Removed Steps that are Double-Printed...
tree
|
commitdiff
2022-03-03
Andrew Reynolds
Throw logic exception if a transcendental function...
tree
|
commitdiff
2022-03-03
Andrew Reynolds
Improve error for higher-order logic (#8207)
tree
|
commitdiff
2022-03-03
Gereon Kremer
Integrate pythonic api (#8131)
tree
|
commitdiff
2022-03-03
Gereon Kremer
Fix rewriting of mixed-integer atoms (#8214)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Fix issue with dropping non-reduced sine terms (#8211)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Fix models involving cardinality of sets of finite...
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Always purify universe from set minus (#8201)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Eliminate CDHashMap::insertAtContextLevelZero (#8173)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Fix incorrect assertion in prop engine proofs (#8204)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Clean usage of options in regressions (#8190)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Improve error message when not using strings-exp (...
tree
|
commitdiff
2022-03-02
Gereon Kremer
Move libpoly <-> CoCoA conversion to new utility (...
tree
|
commitdiff
2022-03-02
Gereon Kremer
Refactor rewriting of arithmetic division (#8195)
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Add utility to access how to print floating point ...
tree
|
commitdiff
2022-03-02
Andrew Reynolds
Make blockModelValues robust to non-closed enumerable...
tree
|
commitdiff
2022-03-02
Gereon Kremer
Prune spurious roots in lazard evaluation of coverings...
tree
|
commitdiff
2022-03-01
Andrew Reynolds
Fix issue involving dropped purification lemmas for...
tree
|
commitdiff
2022-03-01
Andrew Reynolds
Do not use sygus evaluation functions in sygus-inst...
tree
|
commitdiff
2022-03-01
Andres Noetzli
[BV] Fix rewriter policy for `bvneg` (#8196)
tree
|
commitdiff
2022-03-01
Andrew Reynolds
Fix lambda lifting + proofs (#8152)
tree
|
commitdiff
2022-03-01
Andres Noetzli
Remove unused data members from `TheoryArrays` (#8197)
tree
|
commitdiff
2022-03-01
Gereon Kremer
Rename cad to coverings (#8187)
tree
|
commitdiff
2022-02-28
Andres Noetzli
[Seq/Model] Do not enumerate elements of constants...
tree
|
commitdiff
2022-02-28
Gereon Kremer
Refactor rewriting of arithmetic atoms (#8175)
tree
|
commitdiff
2022-02-28
Andrew Reynolds
Fix special casing for PI in model value (#8189)
tree
|
commitdiff
2022-02-28
Andrew Reynolds
Preserve model values for exact sine points (#8188)
tree
|
commitdiff
2022-02-28
Andrew Reynolds
Track names for witness terms in model (#8184)
tree
|
commitdiff
2022-02-28
Andrew Reynolds
Add two reduction schemas for sin terms (#8171)
tree
|
commitdiff
2022-02-28
Andres Noetzli
Remove broken/unused `--mmap` option (#8178)
tree
|
commitdiff
2022-02-28
Gereon Kremer
Add scripts to build python wheels (#8132)
tree
|
commitdiff
2022-02-28
Gereon Kremer
Refactor rewriting of arithmetic leafs (#8177)
tree
|
commitdiff
2022-02-28
Gereon Kremer
Refactor rewriting of arithmetic addition (#8180)
tree
|
commitdiff
2022-02-25
Andrew Reynolds
Consider PI to be a model value (#8176)
tree
|
commitdiff
2022-02-25
Gereon Kremer
Add utilities to rewrite atoms for the arithmetic rewri...
tree
|
commitdiff
2022-02-25
Gereon Kremer
Refactor rewriting of arithmetic negation and subtracti...
tree
|
commitdiff
2022-02-25
Gereon Kremer
Slightly refactor arithmetic rewriting for extended...
tree
|
commitdiff
2022-02-25
Andrew Reynolds
Fix non-termination in quantifiers rewriter (#8165)
tree
|
commitdiff
2022-02-25
Andrew Reynolds
Simplify and fix how purified terms are managed in...
tree
|
commitdiff
2022-02-25
Andrew Reynolds
Fix dropped bounds on PI (#8164)
tree
|
commitdiff
2022-02-25
Andrew Reynolds
Remove approximations infrastructure from model (#8166)
tree
|
commitdiff
2022-02-25
Andrew Reynolds
Remove spurious assertion involving constants for argum...
tree
|
commitdiff
2022-02-25
Andrew Reynolds
Make quantifiers terminate if it detects a (duplicate...
tree
|
commitdiff
2022-02-25
Andrew Reynolds
Consolidate extended rewrite preprocessing modes (...
tree
|
commitdiff
2022-02-25
Andres Noetzli
[Python API] Add support for blocking models (#8134)
tree
|
commitdiff
2022-02-24
Andrew Reynolds
Ensure variables are constrained in model when equal...
tree
|
commitdiff
2022-02-24
Andrew Reynolds
Make model builder robust to multiple value-like terms...
tree
|
commitdiff
2022-02-24
Gereon Kremer
Improve error message for missing options include ...
tree
|
commitdiff
next