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

2021-07-29	Andrew Reynolds	Integrate central equality engine approach into theory...	commit \| commitdiff \| tree
2021-07-29	Andrew Reynolds	Minor updates to shared terms database for central...	commit \| commitdiff \| tree
2021-07-28	Andrew Reynolds	Minor changes to arrays in preparation for central...	commit \| commitdiff \| tree
2021-07-28	Andrew Reynolds	Make extended rewriter methods const (#6948)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Track instantiation reasons in proofs (#6935)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add basic LFSC utilities (#6879)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Move enum value generator to own file (#6941)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Minor fix for term database + central equality engine...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Revert change to regression (#6940)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Make all dependencies in the fast enumerator optional...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add print expression utility (#6880)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Minor changes from proof-new (#6937)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Miscellaneous fixes from proof-new (#6914)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add proof letify utility (#6881)	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Fix eq proof conversion for constant merged parameterized...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Default equality proofs for bags and separation logic...	commit \| commitdiff \| tree
2021-07-27	Andrew Reynolds	Add sygus enumerator callback (#6923)	commit \| commitdiff \| tree
2021-07-26	Andrew Reynolds	Enable default equality proofs for sets (#6931)	commit \| commitdiff \| tree
2021-07-26	Andrew Reynolds	More updates to arithmetic in preparation for central...	commit \| commitdiff \| tree
2021-07-25	Andrew Reynolds	Changes to datatypes in preparation for central equality...	commit \| commitdiff \| tree
2021-07-25	Andrew Reynolds	Refactor equality engine setup for arithmetic congruence...	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Simplify computation of relevant terms in datatypes...	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Add the central equality engine manager (#6893)	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Miscellaneous changes in preparation for central equality...	commit \| commitdiff \| tree
2021-07-22	Andrew Reynolds	Preparation for carry the rewrite rule database in...	commit \| commitdiff \| tree
2021-07-18	Andrew Reynolds	Add n-ary term utilities (#6896)	commit \| commitdiff \| tree
2021-07-16	Andrew Reynolds	Do not exhaustive instantiation when FMF is disabled...	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Fix context for proofs of instantiations (#6890)	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Distinguish quantifiers preprocess as its own proof...	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Connect the equality solver to theory arith (#6894)	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Arithmetic equality solver (#6876)	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Move master equality engine notification to own file...	commit \| commitdiff \| tree
2021-07-15	Andrew Reynolds	Add node converter utility (#6878)	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Fix for context on input proof generator (#6873)	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Move synthesis verification check to own file (#6882)	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Refactor setup of proof equality engine for central...	commit \| commitdiff \| tree
2021-07-14	Andrew Reynolds	Fix models for sequences of infinite element type ...	commit \| commitdiff \| tree
2021-07-13	Andrew Reynolds	Add branch and bound lemma if linear arithmetic generates...	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Add branch and bound (#6865)	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Fix for learned rewrite pass, add regression (#6850)	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Add arithmetic preprocess rewrite equality module ...	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Add trace for combination splits (#6862)	commit \| commitdiff \| tree
2021-07-12	Andrew Reynolds	Improvements to debug check model (#6861)	commit \| commitdiff \| tree
2021-07-09	Andrew Reynolds	Fix sets cardinality inference involving equivalent...	commit \| commitdiff \| tree
2021-07-09	Andrew Reynolds	Implement stop-only for new justification heuristic...	commit \| commitdiff \| tree
2021-07-08	Andrew Reynolds	Disable ordering heuristic for justification by default...	commit \| commitdiff \| tree
2021-07-07	Andrew Reynolds	Fix regressions for competition build (#6846)	commit \| commitdiff \| tree
2021-07-07	Andrew Reynolds	Standard output for trigger selection (#6841)	commit \| commitdiff \| tree
2021-07-06	Andrew Reynolds	Integrate learned rewrite preprocessing pass (#6840)	commit \| commitdiff \| tree
2021-07-06	Andrew Reynolds	Add implementation of learned rewrite pass (#6843)	commit \| commitdiff \| tree
2021-07-06	Andrew Reynolds	Add learned rewrite preprocessing pass (#6842)	commit \| commitdiff \| tree
2021-07-05	Andrew Reynolds	Make buffered inference manager more robust to backtracking...	commit \| commitdiff \| tree
2021-07-02	Andrew Reynolds	Fix rewriter for negative constant seq.nth (#6827)	commit \| commitdiff \| tree
2021-07-01	Andrew Reynolds	Add recursive function definitions to subsolver in...	commit \| commitdiff \| tree
2021-07-01	Andrew Reynolds	Add option to limit the number of instantiation rounds...	commit \| commitdiff \| tree
2021-06-30	Andrew Reynolds	Do not notify during equality engine initialization...	commit \| commitdiff \| tree
2021-06-30	Andrew Reynolds	Do not apply fmfBound to standard quantifiers when...	commit \| commitdiff \| tree
2021-06-30	Andrew Reynolds	Fix pre vs. post-rewrite in proofs for theory preprocessor...	commit \| commitdiff \| tree
2021-06-28	Andrew Reynolds	Rename internal string kinds to match API (#6797)	commit \| commitdiff \| tree
2021-06-24	Andrew Reynolds	Fix linear arithmetic for duplicate lemmas in incremental...	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Avoid full normalization of lambdas in getValue (#6787)	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Minor simplification to equality engine notifications...	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Always check legal eliminations in quantified logics...	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Fix type enumeration for non first-class sorts in FMF...	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Fix cases of ITE within regular expressions (#6783)	commit \| commitdiff \| tree
2021-06-22	Andrew Reynolds	Set up fine grained equality notifications (#6734)	commit \| commitdiff \| tree
2021-06-13	Andrew Reynolds	Minor simplifications to LogicInfo (#6737)	commit \| commitdiff \| tree
2021-06-11	Andrew Reynolds	Remove support for lazy BV extended function reductions...	commit \| commitdiff \| tree
2021-06-10	Andrew Reynolds	Ensure bv2nat and int2bv are not rewritten when using...	commit \| commitdiff \| tree
2021-06-09	Andrew Reynolds	Integrate learned literal manager into preprocessing...	commit \| commitdiff \| tree
2021-06-09	Andrew Reynolds	Fixes related to printing tuples, define-fun commands...	commit \| commitdiff \| tree
2021-06-08	Andrew Reynolds	Fix for 2 dimensional dependent bounded quantifiers...	commit \| commitdiff \| tree
2021-06-08	Andrew Reynolds	Add learned literal manager utility (#6709)	commit \| commitdiff \| tree
2021-06-08	Andrew Reynolds	Make TheoryUF compatible with central equality engine...	commit \| commitdiff \| tree
2021-06-08	Andrew Reynolds	Fix str.update reduction (#6696)	commit \| commitdiff \| tree
2021-06-07	Andrew Reynolds	(proof-new) Fix missing connection in trust substitution...	commit \| commitdiff \| tree
2021-06-07	Andrew Reynolds	(proof-new) Lazy proof chain debug names (#6680)	commit \| commitdiff \| tree
2021-06-04	Andrew Reynolds	Miscellaneous changes from central ee branch (#6687)	commit \| commitdiff \| tree
2021-06-03	Andrew Reynolds	Simplify automatic set-logic in smt2 parser (#6678)	commit \| commitdiff \| tree
2021-06-02	Andrew Reynolds	Fixes for printing define-fun-rec (#6673)	commit \| commitdiff \| tree
2021-06-02	Andrew Reynolds	Fix unsat core proofs (#6655)	commit \| commitdiff \| tree
2021-06-01	Andrew Reynolds	Use top-level substitutions in ITE simp (#6651)	commit \| commitdiff \| tree
2021-06-01	Andrew Reynolds	Disable timeout regressions (#6650)	commit \| commitdiff \| tree
2021-05-27	Andrew Reynolds	Fix regular expression aggressive elim (#6627)	commit \| commitdiff \| tree
2021-05-27	Andrew Reynolds	Update proof namespaces (#6614)	commit \| commitdiff \| tree
2021-05-27	Andrew Reynolds	Fix CEGQI for datatypes with Boolean subfields (#6630)	commit \| commitdiff \| tree
2021-05-27	Andrew Reynolds	Fix spurious assertion for trivial abduction (#6629)	commit \| commitdiff \| tree
2021-05-27	Andrew Reynolds	Enable new justification heuristic by default (#6613)	commit \| commitdiff \| tree
2021-05-24	Andrew Reynolds	Fix non-fixed length case in re-elim (#6612)	commit \| commitdiff \| tree
2021-05-24	Andrew Reynolds	Implementation of the new justification heuristic ...	commit \| commitdiff \| tree
2021-05-24	Andrew Reynolds	Move proof utilities to src/proof/ (#6611)	commit \| commitdiff \| tree
2021-05-24	Andrew Reynolds	Fix re-elim length requirement for symbolic RE memberships...	commit \| commitdiff \| tree
2021-05-24	Andrew Reynolds	Fix instance of no rewrite in extended rewriter (#6610)	commit \| commitdiff \| tree
2021-05-24	Andrew Reynolds	Better formalization of regular expression unfolding...	commit \| commitdiff \| tree
2021-05-21	Andrew Reynolds	Fix tests of unsat cores (#6593)	commit \| commitdiff \| tree
2021-05-21	Andrew Reynolds	Fix and refactor relevant domain (#6528)	commit \| commitdiff \| tree
2021-05-21	Andrew Reynolds	Formalize shared selectors as skolem functions (#6591)	commit \| commitdiff \| tree
2021-05-21	Andrew Reynolds	Minor simplification to boolean proof checker (#6590)	commit \| commitdiff \| tree
2021-05-21	Andrew Reynolds	(proof-new) Minor documentation sync (#6592)	commit \| commitdiff \| tree
2021-05-21	Andrew Reynolds	Add utility to get all types occurring in a term (...	commit \| commitdiff \| tree
next

RSS Atom