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

2021-02-18	Andrew Reynolds	Document UF inferences (#5917)	commit \| commitdiff \| tree
2021-02-18	Andrew Reynolds	Eliminate non-static members in term util (#5919)	commit \| commitdiff \| tree
2021-02-18	Andrew Reynolds	Move first order model for full model check to own...	commit \| commitdiff \| tree
2021-02-17	Andrew Reynolds	Move methods from term util to quantifiers registry...	commit \| commitdiff \| tree
2021-02-17	Andrew Reynolds	Compute fact or lemma in datatypes prior to buffering...	commit \| commitdiff \| tree
2021-02-13	Andrew Reynolds	Moving methods from quantifiers engine to quantifiers...	commit \| commitdiff \| tree
2021-02-12	Andrew Reynolds	Simplify and fix decision engine's handling of skolem...	commit \| commitdiff \| tree
2021-02-12	Andrew Reynolds	(proof-new) Option to not automatically consider symmetry...	commit \| commitdiff \| tree
2021-02-11	Andrew Reynolds	Fix spurious assertion failure in regexp normalization...	commit \| commitdiff \| tree
2021-02-11	Andrew Reynolds	Simplify interface for preprocessor (#5890)	commit \| commitdiff \| tree
2021-02-10	Andrew Reynolds	Refactor term registration visitors (#5875)	commit \| commitdiff \| tree
2021-02-10	Andrew Reynolds	Fix open proof for factoring lemma (#5885)	commit \| commitdiff \| tree
2021-02-10	Andrew Reynolds	Simplify method for inferring proxy lemmas in strings...	commit \| commitdiff \| tree
2021-02-10	Andrew Reynolds	Remove track instantiations infrastructure (#5883)	commit \| commitdiff \| tree
2021-02-10	Andrew Reynolds	Optimize get skolems method (#5876)	commit \| commitdiff \| tree
2021-02-10	Andrew Reynolds	Do not traverse quantifiers in term formula removal...	commit \| commitdiff \| tree
2021-02-09	Andrew Reynolds	Eliminating dependencies from inst utils (#5882)	commit \| commitdiff \| tree
2021-02-09	Andrew Reynolds	Make term database optionally SAT-context-dependent...	commit \| commitdiff \| tree
2021-02-08	Andrew Reynolds	Use quantifiers inference manager for lemma management...	commit \| commitdiff \| tree
2021-02-08	Andrew Reynolds	Fix disequality between seq.unit terms (#5880)	commit \| commitdiff \| tree
2021-02-08	Andrew Reynolds	Remove support for inst closure (#5874)	commit \| commitdiff \| tree
2021-02-08	Andrew Reynolds	Avoid spurious traversal of terms during preregistration...	commit \| commitdiff \| tree
2021-02-06	Andrew Reynolds	Do not combine theories if theory engine needs check...	commit \| commitdiff \| tree
2021-02-05	Andrew Reynolds	Minor cleaning of quantifiers engine (#5858)	commit \| commitdiff \| tree
2021-02-05	Andrew Reynolds	Miscellaneous cleaning in theory engine (#5854)	commit \| commitdiff \| tree
2021-02-04	Andrew Reynolds	Introduce quantifiers registry utility (#5829)	commit \| commitdiff \| tree
2021-02-04	Andrew Reynolds	Eliminate equality query dependence on quantifiers...	commit \| commitdiff \| tree
2021-02-02	Andrew Reynolds	(proof-new) Miscellaneous fixes and regressions (#5841)	commit \| commitdiff \| tree
2021-02-02	Andrew Reynolds	(proof-new) Refactor theory preprocessing (#5835)	commit \| commitdiff \| tree
2021-02-02	Andrew Reynolds	Remove quantifiers regression from decision folder...	commit \| commitdiff \| tree
2021-02-02	Andrew Reynolds	Cleanup some includes (#5847)	commit \| commitdiff \| tree
2021-02-02	Andrew Reynolds	Improvements for NL traces (#5846)	commit \| commitdiff \| tree
2021-02-01	Andrew Reynolds	Eliminate PREPROCESS lemma property (#5827)	commit \| commitdiff \| tree
2021-02-01	Andrew Reynolds	Simplify alpha equivalence module (#5839)	commit \| commitdiff \| tree
2021-01-30	Andrew Reynolds	Fix unguarded call to get representative (#5838)	commit \| commitdiff \| tree
2021-01-29	Andrew Reynolds	(proof-new) Distinguish pre vs post rewrites in term...	commit \| commitdiff \| tree
2021-01-28	Andrew Reynolds	Reorganize calls to quantifiers engine from SmtEngine...	commit \| commitdiff \| tree
2021-01-28	Andrew Reynolds	Simplify lemma interface (#5819)	commit \| commitdiff \| tree
2021-01-28	Andrew Reynolds	Use standard equality engine information in quantifiers...	commit \| commitdiff \| tree
2021-01-28	Andrew Reynolds	Always theory-preprocess lemmas (#5817)	commit \| commitdiff \| tree
2021-01-27	Andrew Reynolds	Add option for whether to filter candidate rewrite...	commit \| commitdiff \| tree
2021-01-27	Andrew Reynolds	Split pattern term selector from trigger (#5811)	commit \| commitdiff \| tree
2021-01-27	Andrew Reynolds	(proof-new) Improvements to quantifiers engine and...	commit \| commitdiff \| tree
2021-01-27	Andrew Reynolds	Use term canonizer utility locally in quantifiers ...	commit \| commitdiff \| tree
2021-01-27	Andrew Reynolds	Use standard conflict mechanism in quantifiers state...	commit \| commitdiff \| tree
2021-01-26	Andrew Reynolds	Introduce quantifiers inference manager (#5821)	commit \| commitdiff \| tree
2021-01-26	Andrew Reynolds	Remove deprecated quantifiers modules (#5820)	commit \| commitdiff \| tree
2021-01-26	Andrew Reynolds	Refactor quantifiers engine initialization (#5813)	commit \| commitdiff \| tree
2021-01-25	Andrew Reynolds	Ensure uses of ground terms in triggers are preprocessed...	commit \| commitdiff \| tree
2021-01-25	Andrew Reynolds	Split inst match generator into multiple files (#5805)	commit \| commitdiff \| tree
2021-01-25	Andrew Reynolds	Split E-matching strategies to own files (#5807)	commit \| commitdiff \| tree
2021-01-24	Andrew Reynolds	Initial cleaning of e-matching instantiation strategy...	commit \| commitdiff \| tree
2021-01-24	Andrew Reynolds	Initial cleaning of triggers (#5795)	commit \| commitdiff \| tree
2021-01-24	Andrew Reynolds	Initial cleaning of inst match generator (#5794)	commit \| commitdiff \| tree
2021-01-24	Andrew Reynolds	(proof-new) Instantiation list utility (#5768)	commit \| commitdiff \| tree
2021-01-24	Andrew Reynolds	Add interface for getting preprocessed term (#5798)	commit \| commitdiff \| tree
2021-01-21	Andrew Reynolds	Add div, mod, abs in non-strict parsing mode (#5793)	commit \| commitdiff \| tree
2021-01-20	Andrew Reynolds	Refactoring the single invocation solver (#5706)	commit \| commitdiff \| tree
2021-01-20	Andrew Reynolds	Fix type issues with relevant domain computation (...	commit \| commitdiff \| tree
2021-01-20	Andrew Reynolds	Fix corner case of wrongly applied selector as trigger...	commit \| commitdiff \| tree
2021-01-20	Andrew Reynolds	Do not track processed in remove term formulas loop...	commit \| commitdiff \| tree
2021-01-20	Andrew Reynolds	Use arbitrary ground term assignment for sorts where...	commit \| commitdiff \| tree
2021-01-15	Andrew Reynolds	Implement --no-strings-lazy-pp as a preprocessing pass...	commit \| commitdiff \| tree
2021-01-14	Andrew Reynolds	Updates to theory preprocess equality (#5776)	commit \| commitdiff \| tree
2021-01-13	Andrew Reynolds	Split eager solver from strings solver state (#5775)	commit \| commitdiff \| tree
2021-01-13	Andrew Reynolds	Do not call ppRewrite on Boolean equalities (#5762)	commit \| commitdiff \| tree
2021-01-11	Andrew Reynolds	Merge theory registrar and theory proxy (#5758)	commit \| commitdiff \| tree
2021-01-11	Andrew Reynolds	Further simplifications in preparation for removing...	commit \| commitdiff \| tree
2021-01-11	Andrew Reynolds	Remove extended rewrite for arithmetic (#5760)	commit \| commitdiff \| tree
2021-01-06	Andrew Reynolds	Add new interfaces to term formula removal and theory...	commit \| commitdiff \| tree
2021-01-05	Andrew Reynolds	Remove a few miscellaneous references to the expr layer...	commit \| commitdiff \| tree
2020-12-23	Andrew Reynolds	Add option to track and notify from CNF stream (#5708)	commit \| commitdiff \| tree
2020-12-23	Andrew Reynolds	Remove quant EPR option (#5716)	commit \| commitdiff \| tree
2020-12-23	Andrew Reynolds	(proof-new) Miscelleneous fixes from proof-new (#5714)	commit \| commitdiff \| tree
2020-12-23	Andrew Reynolds	Minor simplification to Theory::theoryOf (#5719)	commit \| commitdiff \| tree
2020-12-22	Andrew Reynolds	Move slow regression to regress3 (#5715)	commit \| commitdiff \| tree
2020-12-22	Andrew Reynolds	Make theory preprocess rewrite equalities a preprocessing...	commit \| commitdiff \| tree
2020-12-22	Andrew Reynolds	Remove preregister instantiation heuristic (#5713)	commit \| commitdiff \| tree
2020-12-21	Andrew Reynolds	Move ownership of theory preprocessor to TheoryProxy...	commit \| commitdiff \| tree
2020-12-21	Andrew Reynolds	Eliminate recursion from the internals of term formula...	commit \| commitdiff \| tree
2020-12-21	Andrew Reynolds	Fix issue with selector triggers (#5689)	commit \| commitdiff \| tree
2020-12-18	Andrew Reynolds	Simplify internal API for sygus (#5687)	commit \| commitdiff \| tree
2020-12-17	Andrew Reynolds	(proof-new) Minor updates to term conversion proof...	commit \| commitdiff \| tree
2020-12-17	Andrew Reynolds	Simplify term formula removal interface (#5695)	commit \| commitdiff \| tree
2020-12-17	Andrew Reynolds	Simplify and fix check models (#5685)	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	Simplify preprocessing (#5647)	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	Mark quantifier instantiations as needs justify (#5684)	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	Simplify synth-fun printer (#5682)	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	(proof-new) Use bound variable manager (#5679)	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	Move ownership of term formula removal to theory preprocesso...	commit \| commitdiff \| tree
2020-12-16	Andrew Reynolds	Use uint64 utility when parsing tuple selectors in...	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Move trigger trie to own file (#5680)	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Improvements related to quantifiers printing (#5678)	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Proper expand definitions for sets (#5676)	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Consolidate basic sygus utilities regarding sygus conjecture...	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Fix datatypes compute ground value (#5671)	commit \| commitdiff \| tree
2020-12-15	Andrew Reynolds	Remove bv divide by zero option (#5672)	commit \| commitdiff \| tree
2020-12-14	Andrew Reynolds	Properly implement datatype selector triggers (#5624)	commit \| commitdiff \| tree
2020-12-14	Andrew Reynolds	(proof-new) Add bound variable manager (#5655)	commit \| commitdiff \| tree
2020-12-14	Andrew Reynolds	Fix and improve evaluator (#5563)	commit \| commitdiff \| tree
next

RSS Atom