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

2020-06-25	Andrew Reynolds	Update option --nl-ext to enable/disable incremental...	commit \| commitdiff \| tree
2020-06-24	Andres Noetzli	Fix CVC4_EXTRAVERSION variable (#4653)	commit \| commitdiff \| tree
2020-06-24	Andres Noetzli	[unconstrained] Fix gathering of visited-once vars...	commit \| commitdiff \| tree
2020-06-23	Andrew Reynolds	(proof-new) Updates to proof node manager (#4617)	commit \| commitdiff \| tree
2020-06-23	Aina Niemetz	New C++ API: Remove examples for old API. (#4650)	commit \| commitdiff \| tree
2020-06-23	Mathias Preiner	Add support for eqrange predicate (#4562)	commit \| commitdiff \| tree
2020-06-22	Andrew Reynolds	(proof-new) Add REWRITE trust node kind. (#4624)	commit \| commitdiff \| tree
2020-06-22	Aina Niemetz	get-authors: Add alias for nafur. (#4646)	commit \| commitdiff \| tree
2020-06-22	nafur	Allow for better interaction of Integer/Rational with...	commit \| commitdiff \| tree
2020-06-22	Andrew Reynolds	(proof-new) Add proof-new to options file (#4641)	commit \| commitdiff \| tree
2020-06-22	Andrew Reynolds	Add trascendental function kinds to list of unevaluated...	commit \| commitdiff \| tree
2020-06-22	yoni206	fix (#4637)	commit \| commitdiff \| tree
2020-06-20	Alex Ozdemir	Use traversal iterators in IntToBv (#4169)	commit \| commitdiff \| tree
2020-06-20	Abdalrhman Mohamed	Add Match utility function. (#4632)	commit \| commitdiff \| tree
2020-06-20	Andrew Reynolds	(proof-new) Make static methods in re-elim (#4623)	commit \| commitdiff \| tree
2020-06-19	Andrew Reynolds	(proof-new) CDProof inherits from ProofGenerator (...	commit \| commitdiff \| tree
2020-06-19	Andrew Reynolds	Add casc j10 scripts (#4621)	commit \| commitdiff \| tree
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) ...assertion error [here](https://github.com/CVC4/CVC4/blob/8236d7f9bff3aef4f7b3...	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... ...simply recursive datatypes (https://github.com/ajreynol/CVC4/tree/dtNonSimpleRec...	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
next

RSS Atom