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

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
2018-09-26	Haniel Barbosa	Makes SyGuS parsing more robust in invariant problems...	commit \| commitdiff \| tree
2018-09-18	Haniel Barbosa	fix assertion error (#2487)	commit \| commitdiff \| tree
2018-09-13	Haniel Barbosa	Uses information gain heuristic for building better...	commit \| commitdiff \| tree
2018-09-11	Haniel Barbosa	fix (#2446)	commit \| commitdiff \| tree
2018-09-11	Haniel Barbosa	Using a single condition enumerator in sygus-unif ...	commit \| commitdiff \| tree
2018-08-31	Haniel Barbosa	Allows SAT checks of repair const to have different...	commit \| commitdiff \| tree
2018-08-31	Haniel Barbosa	Fix export of bound variables (#2409)	commit \| commitdiff \| tree
2018-08-29	Haniel Barbosa	fix bv total ops printing (#2365)	commit \| commitdiff \| tree
2018-08-25	Haniel Barbosa	Refactor nlExtPurify preprocessing pass (#1963)	commit \| commitdiff \| tree
2018-08-23	Haniel Barbosa	Makes the filename be set in the SMT engine by default...	commit \| commitdiff \| tree
2018-08-22	Haniel Barbosa	Adds regression test for automatic generation of SyGuS...	commit \| commitdiff \| tree
2018-08-21	Haniel Barbosa	Makes the new row propagation system default (#2335)	commit \| commitdiff \| tree
next

RSS Atom