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

2020-06-19	Andrew Reynolds	(proof-new) Updates to strings term registry (#4599)	commit \| commitdiff \| tree
2020-06-19	Andrew Reynolds	Convert more uses of strings to words (#4584)	commit \| commitdiff \| tree
2020-06-19	Andrew Reynolds	(proof-new) Split operator elimination from arithmetic...	commit \| commitdiff \| tree
2020-06-19	Andrew Reynolds	Clean the header file of TheoryStrings (#4272)	commit \| commitdiff \| tree
2020-06-19	Andres Noetzli	Update version information post 1.8 release (#4635)	commit \| commitdiff \| tree
2020-06-19	Haniel Barbosa	Always rewrite boolean ITEs with constant then/else...	commit \| commitdiff \| tree
2020-06-19	Andres Noetzli	Update info for 1.8 release (#4633)	commit \| commitdiff \| tree
2020-06-19	Andres Noetzli	Cleanup examples (#4634)	commit \| commitdiff \| tree
2020-06-19	Haniel Barbosa	Generalize atom collection in old proof code (#4626)	commit \| commitdiff \| tree
2020-06-19	yoni206	Bv to int elimination bugfix (#4435)	commit \| commitdiff \| tree
2020-06-19	Andres Noetzli	Add logic check for define-fun(s)-rec (#4577)	commit \| commitdiff \| tree
2020-06-19	Andrew V. Jones	Revert "[Python] Properly destroy CVC4 object (#3753...	commit \| commitdiff \| tree
2020-06-18	Andres Noetzli	Improve memory management in Java bindings (#4629)	commit \| commitdiff \| tree
2020-06-17	Andrew Reynolds	Do not traverse WITNESS for partial substitutions in...	commit \| commitdiff \| tree
2020-06-17	Haniel Barbosa	Improve polynomial anyterm grammar (#3566)	commit \| commitdiff \| tree
2020-06-16	Andrew Reynolds	Updates to NEWS. (#4628)	commit \| commitdiff \| tree
2020-06-16	Abdalrhman Mohamed	Simplify sygus conversion script. (#4627)	commit \| commitdiff \| tree
2020-06-16	Aina Niemetz	Add missing REQUIRES to new regressions. (#4625)	commit \| commitdiff \| tree
2020-06-16	Aina Niemetz	BV: Fix querying equality status in lazy bit-blaster...	commit \| commitdiff \| tree
2020-06-16	Aina Niemetz	Fix regressions in regress1 after #4613. (#4616)	commit \| commitdiff \| tree
2020-06-16	Andrew Reynolds	(proof-new) Add quantifiers proof checker (#4593)	commit \| commitdiff \| tree
2020-06-15	Andrew Reynolds	(proof-new) Update proof node, add proof node algorithm...	commit \| commitdiff \| tree
2020-06-15	Haniel Barbosa	Support AND/OR definitions in lambda to array rewriting...	commit \| commitdiff \| tree
2020-06-15	Aina Niemetz	BV: Add missing type check for BITVECTOR_REPEAT_OP...	commit \| commitdiff \| tree
2020-06-15	Aina Niemetz	BV: Add missing type check for INT_TO_BITVECTOR. (...	commit \| commitdiff \| tree
2020-06-15	Andrew Reynolds	Do RE derivation inference only for concrete constant...	commit \| commitdiff \| tree
2020-06-13	Andrew Reynolds	Move sygus datatype utility functions to their own...	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	Update to consistent policy for removed terms in quantifier...	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	(proof-new) Term conversion proof generator utility...	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	(proof-new) Minor updates to strings base solver (...	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	Cardinality-related inferences per type in theory of...	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	(proof-new) Split TheoryEngine (#4558)	commit \| commitdiff \| tree
2020-06-12	Andres Noetzli	Fix install of static builds (#4604)	commit \| commitdiff \| tree
2020-06-12	Andrew Reynolds	Add rewrite for str.replace_re. (#4601)	commit \| commitdiff \| tree
2020-06-11	Andrew Reynolds	(proof-new) Add lazy proof utility (#4589)	commit \| commitdiff \| tree
2020-06-11	Andrew Reynolds	(proof-new) Add eager proof generator utility. (#4592)	commit \| commitdiff \| tree
2020-06-11	Andrew Reynolds	(proof-new) Remove arith-snorm option. (#4591)	commit \| commitdiff \| tree
2020-06-10	Andrew Reynolds	(proof-new) Theory proof step buffer utility (#4580)	commit \| commitdiff \| tree
2020-06-10	Andres Noetzli	Add support for str.replace_re/str.replace_re_all ...	commit \| commitdiff \| tree
2020-06-10	makaimann	Fix getKind for Python bindings (#4496)	commit \| commitdiff \| tree
2020-06-09	Andrew Reynolds	(proof-new) Refactor skolemization (#4586)	commit \| commitdiff \| tree
2020-06-09	Andrew Reynolds	(proof-new) Add trust node utility (#4588)	commit \| commitdiff \| tree
2020-06-09	Andres Noetzli	Language bindings: Enable catching of exceptions (...	commit \| commitdiff \| tree
2020-06-09	Andrew V. Jones	Ensure correct CMake dependencies on Debug_tags.h/Trace_tags...	commit \| commitdiff \| tree
2020-06-09	Andres Noetzli	Fix Java target and Relations example (#4583)	commit \| commitdiff \| tree
2020-06-08	Andres Noetzli	Fix ambiguous overload in unit test (#4582)	commit \| commitdiff \| tree
2020-06-08	Andrew Reynolds	(proof-new) Add abstract proof generator class (#4574)	commit \| commitdiff \| tree
2020-06-08	Andres Noetzli	Fix Coverity issues (#4587)	commit \| commitdiff \| tree
2020-06-06	Andrew Reynolds	Use NlLemma utility for all lemmas in non-linear. ...	commit \| commitdiff \| tree
2020-06-06	Andres Noetzli	Fix destruction order in NodeManager (#4578)	commit \| commitdiff \| tree
2020-06-06	Andres Noetzli	Keep definitions when global-declarations enabled ...	commit \| commitdiff \| tree
2020-06-06	Andrew Reynolds	Smt2 parsing support for nested recursive datatypes...	commit \| commitdiff \| tree
2020-06-05	Andrew Reynolds	Datatypes with nested recursion are not handled in...	commit \| commitdiff \| tree
2020-06-05	Andrew Reynolds	(proof-new) Updates to CDProof (#4565)	commit \| commitdiff \| tree
2020-06-05	Andres Noetzli	Skip parse-error regression for comp builds (#4567)	commit \| commitdiff \| tree
2020-06-05	Andrew Reynolds	(proof-new) Rename ProofSkolemCache to SkolemManager...	commit \| commitdiff \| tree
2020-06-05	Haniel Barbosa	Changing default language (#4561)	commit \| commitdiff \| tree
2020-06-05	Haniel Barbosa	Printing FP values as binary or indexed BVs according...	commit \| commitdiff \| tree
2020-06-05	Andres Noetzli	Fix handling of Boolean term variables (#4550)	commit \| commitdiff \| tree
2020-06-05	Andres Noetzli	Fix lifetime and copy issues with NodeDfsIterable ...	commit \| commitdiff \| tree
2020-06-05	Andrew V. Jones	If using 'ninja', tell the user to run 'ninja' not...	commit \| commitdiff \| tree
2020-06-05	makaimann	Add a method for retrieving base of a constant array...	commit \| commitdiff \| tree
2020-06-05	Andres Noetzli	Update Java tests to match changes in API (#4535)	commit \| commitdiff \| tree
2020-06-04	makaimann	Wrap Result in Python API (#4473)	commit \| commitdiff \| tree
2020-06-04	Aina Niemetz	New C++ Api: Second and last batch of API guards. ...	commit \| commitdiff \| tree
2020-06-04	Andrew Reynolds	Add sygus datatype substitution utility method (#4390)	commit \| commitdiff \| tree
2020-06-04	Andrew Reynolds	Fix abduction with datatypes (#4566)	commit \| commitdiff \| tree
2020-06-04	Andrew Reynolds	Theory strings preprocess (#4534)	commit \| commitdiff \| tree
2020-06-04	Aina Niemetz	New C++ Api: First batch of API guards. (#4557)	commit \| commitdiff \| tree
2020-06-03	Haniel Barbosa	(proof-new) Adding rules and proof checker for EUF...	commit \| commitdiff \| tree
2020-06-03	Haniel Barbosa	(proof-new) Adding rules and proof checker for Boolean...	commit \| commitdiff \| tree
2020-06-03	Andrew Reynolds	(proof-new) Add builtin proof checker (#4537)	commit \| commitdiff \| tree
2020-06-03	Mathias Preiner	Fix normalization of author names in contrib/get-authors...	commit \| commitdiff \| tree
2020-06-03	Andrew Reynolds	Do not apply unconstrained simplification when quantifiers...	commit \| commitdiff \| tree
2020-06-03	Andrew Reynolds	Update CEGQI to use lemma status instead of forcing...	commit \| commitdiff \| tree
2020-06-03	Andrew Reynolds	Use prenex normal form when using cegqi-nested-qe ...	commit \| commitdiff \| tree
2020-06-03	makaimann	Add Term::substitute to Python bindings (#4499)	commit \| commitdiff \| tree
2020-06-02	makaimann	Add hash Op, Sort and Term in Python bindings (#4498)	commit \| commitdiff \| tree
2020-06-02	Andrew Reynolds	Fix scope issue with pulling ITEs in extended rewriter...	commit \| commitdiff \| tree
2020-06-02	Andrew Reynolds	Do not handle universal quantification on functions...	commit \| commitdiff \| tree
2020-06-02	Aina Niemetz	New C++ API: Keep reference to solver object in non...	commit \| commitdiff \| tree
2020-06-01	Andrew Reynolds	(proof-new) Proof step buffer utilities (#4533)	commit \| commitdiff \| tree
2020-06-01	Andrew Reynolds	Move non-linear files to src/theory/arith/nl (#4548)	commit \| commitdiff \| tree
2020-06-01	Andres Noetzli	Set theoryof-mode after theory widening (#4545)	commit \| commitdiff \| tree
2020-06-01	Andres Noetzli	Do not parse ->/lambda unless --uf-ho enabled (#4544)	commit \| commitdiff \| tree
2020-06-01	Andrew Reynolds	Incorporate sequences into the word interface (#4543)	commit \| commitdiff \| tree
2020-05-31	Andres Noetzli	Do not cache operator eliminations in arith (#4542)	commit \| commitdiff \| tree
2020-05-31	yoni206	update example in README to use ctest. (#4540)	commit \| commitdiff \| tree
2020-05-30	Andrew Reynolds	Add the sequence type (#4539)	commit \| commitdiff \| tree
2020-05-28	Andrew Reynolds	Fix term registry for constant case, simplify. (#4538)	commit \| commitdiff \| tree
2020-05-27	Andrew Reynolds	Add the Expr-level sequence datatype (#4526)	commit \| commitdiff \| tree
2020-05-27	Martin	Tweak the use of static_assert to support older compilers...	commit \| commitdiff \| tree
2020-05-26	Martin	Fix an incorrect limit in conversion from real to float...	commit \| commitdiff \| tree
2020-05-26	Andrew Reynolds	Convert more uses of strings to words (#4527)	commit \| commitdiff \| tree
2020-05-26	Mathias Preiner	Fix mismatched iterators (CID 1493892). (#4531)	commit \| commitdiff \| tree
2020-05-26	Andrew Reynolds	(proof-new) Update proof checker. (#4511)	commit \| commitdiff \| tree
2020-05-26	Andrew Reynolds	(proof-new) Updates to strings skolem cache. (#4524)	commit \| commitdiff \| tree
2020-05-26	Mathias Preiner	Update to CaDiCaL version 1.2.1. (#4530)	commit \| commitdiff \| tree
2020-05-24	Andres Noetzli	[SMT-COMP] Redirect non-answers to /dev/null (#4528)	commit \| commitdiff \| tree
2020-05-23	mudathirmahgoub	remove unused field d_emp_exp in TheorySetsPrivate...	commit \| commitdiff \| tree
next

RSS Atom