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

2021-02-02	Haniel Barbosa	[proof-new] Fix bug in expansion of MACRO_RESOLUTION...	commit \| commitdiff \| tree
2021-01-29	Haniel Barbosa	[proof-new] Connecting new unsat cores (#5834)	commit \| commitdiff \| tree
2021-01-26	Haniel Barbosa	Reestablishing support for define-sort (#5810)	commit \| commitdiff \| tree
2021-01-22	Haniel Barbosa	[proof-new] Expanding MACRO_RESOLUTION in post-processing...	commit \| commitdiff \| tree
2021-01-08	Haniel Barbosa	[proof-new] Implementing getProof in the API and SMT...	commit \| commitdiff \| tree
2021-01-07	Haniel Barbosa	Remove dependency on expression layer in TPTP parser...	commit \| commitdiff \| tree
2021-01-07	Haniel Barbosa	Fix warning in TPTP parser (#5752)	commit \| commitdiff \| tree
2020-12-24	Haniel Barbosa	[proof-new] Only use old proofs for unsat cores if...	commit \| commitdiff \| tree
2020-12-23	Haniel Barbosa	Dumping unsat cores after check-sat-assuming/QUERY...	commit \| commitdiff \| tree
2020-12-23	Haniel Barbosa	[proof-new] Adding a manager for the new unsat cores...	commit \| commitdiff \| tree
2020-12-21	Haniel Barbosa	Have unsat core regression agnostic to number of assertions...	commit \| commitdiff \| tree
2020-12-17	Haniel Barbosa	[proof-new] Only use old proof code for unsat cores...	commit \| commitdiff \| tree
2020-12-14	Haniel Barbosa	[proof-new] Making the CDCL(T) Minisat proof producing...	commit \| commitdiff \| tree
2020-12-14	Haniel Barbosa	[proof-new] Make prop engine proof producing (#5667)	commit \| commitdiff \| tree
2020-12-14	Haniel Barbosa	[proof-new] Updating interfaces between prop engine...	commit \| commitdiff \| tree
2020-12-11	Haniel Barbosa	[proof-new] Updating theory proxy to new proof infrastructu...	commit \| commitdiff \| tree
2020-12-08	Haniel Barbosa	[proof-new] Updating SAT proof to use MACRO_RESOLUTION...	commit \| commitdiff \| tree
2020-12-08	Haniel Barbosa	[proof-new] Adding MACRO_RESOLUTION rule and updating...	commit \| commitdiff \| tree
2020-10-24	Haniel Barbosa	[proof-new] Fix n-ary kind handling in EqEngine explanations...	commit \| commitdiff \| tree
2020-10-19	Haniel Barbosa	[proof-new] Fixing resolution proof checker (#5262)	commit \| commitdiff \| tree
2020-10-19	Haniel Barbosa	[proof-new] Improving cycle checking in lazycdproofchain...	commit \| commitdiff \| tree
2020-10-14	Haniel Barbosa	using NOT_NOT_ELIM rather than macros to do double...	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Adds a proof manager for prop engine (...	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Adds a proof post processor for the Prop...	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Updates to proof node updater (#5156)	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Adds a proof-producing CNF converter (...	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Removing spurious forward declaration in...	commit \| commitdiff \| tree
2020-09-29	Haniel Barbosa	[proof-new] Adds a proof node hash function (#5154)	commit \| commitdiff \| tree
2020-09-28	Haniel Barbosa	[proof-new] Adds a proof manager for the SAT solver...	commit \| commitdiff \| tree
2020-09-25	Haniel Barbosa	Cleaning and documenting cnf stream (#5134)	commit \| commitdiff \| tree
2020-09-18	Haniel Barbosa	[proof-new] Proof utilities for normalizing clauses...	commit \| commitdiff \| tree
2020-09-17	Haniel Barbosa	[proof-new] Have mkScope agnostic to True assumptions...	commit \| commitdiff \| tree
2020-09-16	Haniel Barbosa	[proof-new] Adds Lazy CDProof chain data-structure...	commit \| commitdiff \| tree
2020-09-16	Haniel Barbosa	[proof-new] Extending eqproof conversion to HO congruence...	commit \| commitdiff \| tree
2020-09-16	Haniel Barbosa	[proof-new] Resolution rules and checkers (#5070)	commit \| commitdiff \| tree
2020-09-16	Haniel Barbosa	[proof-new] A simple proof generator for buffered proof...	commit \| commitdiff \| tree
2020-09-04	Haniel Barbosa	[Regressions] Fix regression issues related to BV proofs...	commit \| commitdiff \| tree
2020-09-04	Haniel Barbosa	Fix non-lib-poly-build issues (#5028)	commit \| commitdiff \| tree
2020-09-01	Haniel Barbosa	Removes old proof code (#4964)	commit \| commitdiff \| tree
2020-08-25	Haniel Barbosa	Eliminating spurious replay of commands for define...	commit \| commitdiff \| tree
2020-08-13	Haniel Barbosa	[proof-new] Adding support for corner case of transitivity...	commit \| commitdiff \| tree
2020-08-12	Haniel Barbosa	generalize handling MERGED_THROUGH_CONSTANST in EqProof...	commit \| commitdiff \| tree
2020-08-12	Haniel Barbosa	(proof-new) Improving proof-production in Equality...	commit \| commitdiff \| tree
2020-07-18	Haniel Barbosa	Improving equality engine tracing (#4770)	commit \| commitdiff \| tree
2020-07-17	Haniel Barbosa	Fix EqProof to ProofNode conversion (#4760)	commit \| commitdiff \| tree
2020-07-16	Haniel Barbosa	(proof-new) Implements the conversion between EqProof...	commit \| commitdiff \| tree
2020-07-16	Haniel Barbosa	(proof-new) Adding API for converting EqProof into...	commit \| commitdiff \| tree
2020-07-14	Haniel Barbosa	Fix options messages that were inverted (#4734)	commit \| commitdiff \| tree
2020-07-11	Haniel Barbosa	Adding test for whether a kind is n-ary (#4718)	commit \| commitdiff \| tree
2020-06-19	Haniel Barbosa	Always rewrite boolean ITEs with constant then/else...	commit \| commitdiff \| tree
2020-06-19	Haniel Barbosa	Generalize atom collection in old proof code (#4626)	commit \| commitdiff \| tree
2020-06-17	Haniel Barbosa	Improve polynomial anyterm grammar (#3566)	commit \| commitdiff \| tree
2020-06-15	Haniel Barbosa	Support AND/OR definitions in lambda to array rewriting...	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-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-04-28	Haniel Barbosa	update Haniel's affiliation (#4404)	commit \| commitdiff \| tree
2020-04-18	Haniel Barbosa	Improving EqProof printing (#4329)	commit \| commitdiff \| tree
2020-02-27	Haniel Barbosa	Changing TPTP parser to accomodate new API (#3837)	commit \| commitdiff \| tree
2020-02-17	Haniel Barbosa	Using ParseOp in TPTP (#3764)	commit \| commitdiff \| tree
2020-02-14	Haniel Barbosa	Forcing rewrite pass rather than asserting if formula...	commit \| commitdiff \| tree
2019-12-12	Haniel Barbosa	Fix Unif+PI algorithm with symbolic unfolding (#3558)	commit \| commitdiff \| tree
2019-12-10	Haniel Barbosa	Fix ufho issues (#3551)	commit \| commitdiff \| tree
2019-11-30	Haniel Barbosa	improving parsing error messages related to HOL (#3510)	commit \| commitdiff \| tree
2019-11-27	Haniel Barbosa	Enable sygusRecFun by default and fixes SyGuS+RecFun...	commit \| commitdiff \| tree
2019-11-22	Haniel Barbosa	fixing stupid typo (#3488)	commit \| commitdiff \| tree
2019-11-21	Haniel Barbosa	hard limit for rec-fun eval (#3485)	commit \| commitdiff \| tree
2019-11-20	Haniel Barbosa	Lazy evaluation via rec-funs of ITE expressions (...	commit \| commitdiff \| tree
2019-09-16	Haniel Barbosa	Adding new scripts for CASC/TPTP (#3291)	commit \| commitdiff \| tree
2019-08-06	Haniel Barbosa	Scripts for CASC-27 (#3163)	commit \| commitdiff \| tree
2019-08-03	Haniel Barbosa	Collapse @ chains in SMT2 printer (#3140)	commit \| commitdiff \| tree
2019-07-31	Haniel Barbosa	Parsing THF and adding several regressions (#3131)	commit \| commitdiff \| tree
2019-07-30	Haniel Barbosa	Code to activate hoelim preprocessing pass (#3129)	commit \| commitdiff \| tree
2019-07-30	Haniel Barbosa	Remove hard coded option for TPTP regressions in run_regress...	commit \| commitdiff \| tree
2019-07-24	Haniel Barbosa	adding runscripts for syguscomp2019 (#3118)	commit \| commitdiff \| tree
2019-06-13	Haniel Barbosa	Fix warning (#3053)	commit \| commitdiff \| tree
2019-04-12	Haniel Barbosa	Referring to prerelease 1.8 (#2943)	commit \| commitdiff \| tree
2019-04-09	Haniel Barbosa	Removing references to cvc4-bugs@... (#2945)	commit \| commitdiff \| tree
2019-04-09	Haniel Barbosa	"prerelease -> release" in INSTALL (#2944)	commit \| commitdiff \| tree
2019-04-08	Haniel Barbosa	fix copyright year in configuration file (#2942)	commit \| commitdiff \| tree
2019-04-05	Haniel Barbosa	prerelease -> release (#2941)	commit \| commitdiff \| tree
2019-04-05	Haniel Barbosa	fix fp issue (#2940)	commit \| commitdiff \| tree
2019-04-04	Haniel Barbosa	adding sygus news (#2934)	commit \| commitdiff \| tree
2019-04-04	Haniel Barbosa	Ignoring FP benchmarks with "unsafe" sizes unless option...	commit \| commitdiff \| tree
2019-04-04	Haniel Barbosa	Update release notes and lib version (#2933)	commit \| commitdiff \| tree
2019-03-29	Haniel Barbosa	removing deprecated rewriting signature / example ...	commit \| commitdiff \| tree
2019-03-28	Haniel Barbosa	fix ex_bv.plf (#2905)	commit \| commitdiff \| tree
2019-03-22	Haniel Barbosa	fix help information on TPTP parsing (#2884)	commit \| commitdiff \| tree
2019-03-15	Haniel Barbosa	New beta-reduction for HOL solving (#2869)	commit \| commitdiff \| tree
2019-03-15	Haniel Barbosa	Adding capture avoiding substitution (#2867)	commit \| commitdiff \| tree
2018-11-07	Haniel Barbosa	Adding default SyGuS grammar construction for arrays...	commit \| commitdiff \| tree
2018-11-03	Haniel Barbosa	Refactor default grammars construction (#2681)	commit \| commitdiff \| tree
2018-10-18	Haniel Barbosa	Introducing internal commands for SyGuS commands (...	commit \| commitdiff \| tree
2018-10-16	Haniel Barbosa	Option for shuffling condition pool in CegisUnif (...	commit \| commitdiff \| tree
2018-10-11	Haniel Barbosa	Fix default setting of CegisUnif options (#2605)	commit \| commitdiff \| tree
2018-10-05	Haniel Barbosa	Fix unif trace (#2550)	commit \| commitdiff \| tree
2018-10-03	Haniel Barbosa	Make CegisUnif with condition independent robust to...	commit \| commitdiff \| tree
2018-10-01	Haniel Barbosa	init scalar class members (coverity issues 1473720...	commit \| commitdiff \| tree
2018-09-29	Haniel Barbosa	Stream concrete values for variable agnostic enumerators...	commit \| commitdiff \| tree
next

RSS Atom