git.libre-soc.org Git - cvc5.git/search

2022-03-24	Gereon Kremer	Document proof rules for coverings solver (#8376)	commit \| commitdiff \| tree
2022-03-24	Andrew Reynolds	Minor updates for quantifiers options (#8385)	commit \| commitdiff \| tree
2022-03-24	Haniel Barbosa	[proofs] [sat] Handle resolution proofs for optimized...	commit \| commitdiff \| tree
2022-03-24	Gereon Kremer	Document arithmetic proof rules (#8373)	commit \| commitdiff \| tree
2022-03-24	Andrew Reynolds	Standardize more instances of skolems (#8351)	commit \| commitdiff \| tree
2022-03-24	Haniel Barbosa	[sat] Add option to disable Minisat simplifications...	commit \| commitdiff \| tree
2022-03-24	Andrew Reynolds	Fix a couple of parse error messages for sygus (#8381)	commit \| commitdiff \| tree
2022-03-24	Haniel Barbosa	[unsat-cores] [sat-proof] Fix open proofs due to theory...	commit \| commitdiff \| tree
2022-03-23	Andrew Reynolds	Clean options (#8309)	commit \| commitdiff \| tree
2022-03-23	Gereon Kremer	Add API unit tests for statistics (#8341)	commit \| commitdiff \| tree
2022-03-23	Andrew Reynolds	Add SynthResult to the API (#8370)	commit \| commitdiff \| tree
2022-03-23	Gereon Kremer	Add `getOptionInfo()` and `getOptionNames()` to python...	commit \| commitdiff \| tree
2022-03-23	Gereon Kremer	Document proof rules for transcendentals (#8375)	commit \| commitdiff \| tree
2022-03-23	Andrew Reynolds	Make IDOF_MAX rewrite only apply when all children...	commit \| commitdiff \| tree
2022-03-23	Mathias Preiner	Only update latest tag if commit changed. (#8379)	commit \| commitdiff \| tree
2022-03-23	Andrew Reynolds	Add internal synth result class (#8352)	commit \| commitdiff \| tree
2022-03-23	Gereon Kremer	Run gen-versioninfo unconditionally (#8368)	commit \| commitdiff \| tree
2022-03-23	Gereon Kremer	Store latest builds in a special release (#8337)	commit \| commitdiff \| tree
2022-03-23	Gereon Kremer	Remove dependency on build (#8367)	commit \| commitdiff \| tree
2022-03-23	mudathirmahgoub	update SET_COMPREHENSION documentation (#8372)	commit \| commitdiff \| tree
2022-03-23	Andrew Reynolds	Initial documentation on LFSC (#8365)	commit \| commitdiff \| tree
2022-03-23	mudathirmahgoub	Fix cvc5-projects issue 497 (#8331)	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	Gereon Kremer	Refactor proof rule documentation (#8303)	commit \| commitdiff \| tree
2022-03-22	Andrew Reynolds	Updates for the theory reference for separation logic...	commit \| commitdiff \| tree
2022-03-22	Gereon Kremer	Make uncovered-api-functions.py exit with 1 if something...	commit \| commitdiff \| tree
2022-03-22	Haniel Barbosa	[proofs] Alethe: fixing formatting and adding missing...	commit \| commitdiff \| tree
2022-03-22	mudathirmahgoub	update sets-and-relations.rst (#8364)	commit \| commitdiff \| tree
2022-03-22	Abdalrhman Mohamed	Add a timeout option for verification of synthesized...	commit \| commitdiff \| tree
2022-03-22	Andres Noetzli	[FP] Remove `FLOATINGPOINT_TO_FP_GENERIC` kind (#8334)	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-22	Mathias Preiner	api: Unify mkTerm variants. (#8357)	commit \| commitdiff \| tree
2022-03-22	Andres Noetzli	[API] Support `Op::operator[]` in Java and Python ...	commit \| commitdiff \| tree
2022-03-21	Andres Noetzli	Remove `Op::getIndices()` (#8355)	commit \| commitdiff \| tree
2022-03-21	Andrew Reynolds	Fix return value for candidate rewrite database (#8354)	commit \| commitdiff \| tree
2022-03-21	Gereon Kremer	Refactor documentation (#8288)	commit \| commitdiff \| tree
2022-03-21	Andrew Reynolds	Fix LFSC conversion for seq unit (#8353)	commit \| commitdiff \| tree
2022-03-21	Gereon Kremer	Fix names of unit tests (#8338)	commit \| commitdiff \| tree
2022-03-21	Andrew Reynolds	Fix learned literals for top-level AND (#8336)	commit \| commitdiff \| tree
2022-03-20	Gereon Kremer	Add `getStatistics()` to python API (#8343)	commit \| commitdiff \| tree
2022-03-17	Andres Noetzli	[Parser] Simplify `Smt2::addIndexedOperator()` (#8333)	commit \| commitdiff \| tree
2022-03-17	Aina Niemetz	ctest: Fix labels for python unit tests. (#8328)	commit \| commitdiff \| tree
2022-03-17	Andrew Reynolds	Update care graph computations to use standard node...	commit \| commitdiff \| tree
2022-03-17	Gereon Kremer	Replace `Debug` by `Trace` (#7793)	commit \| commitdiff \| tree
2022-03-17	Andres Noetzli	Remove unused options handler (#8335)	commit \| commitdiff \| tree
2022-03-17	Andres Noetzli	[CI] Use ccache for Windows builds (#8332)	commit \| commitdiff \| tree
2022-03-17	Aina Niemetz	api: Fix documentation for TO_FP kinds. (#8329)	commit \| commitdiff \| tree
2022-03-17	Aina Niemetz	api: Fix documentation for UNINTERPRETED_SORT_VALUE...	commit \| commitdiff \| tree
2022-03-17	Gereon Kremer	don't build gtest in CI (#8323)	commit \| commitdiff \| tree
2022-03-17	Andres Noetzli	[CI] Strip stored binaries (#8327)	commit \| commitdiff \| tree
2022-03-16	Aina Niemetz	Add unit test and assertion to test and catch cvc5...	commit \| commitdiff \| tree
2022-03-16	Andres Noetzli	Remove unused files in `regress0` (#8325)	commit \| commitdiff \| tree
2022-03-16	Andres Noetzli	[CI] Build and release Win64 binaries (#8321)	commit \| commitdiff \| tree
2022-03-16	Gereon Kremer	Use native cancellation mechanism (#8311)	commit \| commitdiff \| tree
2022-03-16	Mathias Preiner	unit: Add test for api::Kind. (#8322)	commit \| commitdiff \| tree
2022-03-16	Aina Niemetz	First step towards refactoring regression tests. (...	commit \| commitdiff \| tree
2022-03-16	mudathirmahgoub	Add regression for cvc5-projects issue 490 (#8317)	commit \| commitdiff \| tree
2022-03-16	Mathias Preiner	api: Print the correct string for external kinds. ...	commit \| commitdiff \| tree
2022-03-16	Mathias Preiner	run_regression: Make sure to strip trailing whitespaces...	commit \| commitdiff \| tree
2022-03-16	Mathias Preiner	api: Make mkDatatypeDecl argument const&. (#8315)	commit \| commitdiff \| tree
2022-03-16	Andres Noetzli	Fix shared library Windows builds with LibPoly (#8306)	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-16	Andres Noetzli	Ignore `CMAKE_SYSROOT` when cross-compiling (#8318)	commit \| commitdiff \| tree
2022-03-15	Andrew Reynolds	Make learned literal computation more robust (#8308)	commit \| commitdiff \| tree
2022-03-15	Aina Niemetz	api: Remove Sort::isFirstClass(). (#8312)	commit \| commitdiff \| tree
2022-03-15	Andres Noetzli	[BV] Fix strategy for rewriting `bvnot` (#8297)	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	mudathirmahgoub	Add skolem lemmas for bags card terms (#7995)	commit \| commitdiff \| tree
2022-03-15	Andrew Reynolds	Properly guard sort instantiate (#8247)	commit \| commitdiff \| tree
2022-03-15	Gereon Kremer	Enable nl-cov-var-elim by default, but disable with...	commit \| commitdiff \| tree
2022-03-15	Andrew Reynolds	Remove unecessary separation logic options (#8269)	commit \| commitdiff \| tree
2022-03-15	Andres Noetzli	Simplify `Scope` (#8307)	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-15	Aina Niemetz	Rename TO_FP operator kinds. (#8285)	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	Mathias Preiner	cmake: Do not require googletest if unit tests are...	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	Andres Noetzli	[API/Python] Add support for `Solver::getModel()` ...	commit \| commitdiff \| tree
2022-03-11	Aina Niemetz	api: Make checks header private. (#8283)	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	Gereon Kremer	Add first step for proofs documentation (#8193)	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
next

RSS Atom