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

2021-02-26	Andrew Reynolds	Minor improvement and fix to smt2 printer (#6009)	commit \| commitdiff \| tree
2021-02-26	Andrew Reynolds	Optionally permit creation of non-flat function types...	commit \| commitdiff \| tree
2021-02-26	Andrew Reynolds	(proof-new) Fix regular expression unfolding under...	commit \| commitdiff \| tree
2021-02-25	Andrew Reynolds	Move slow regressions to regress1 (#5999)	commit \| commitdiff \| tree
2021-02-24	Andrew Reynolds	Add state and inference manager to inst match generator...	commit \| commitdiff \| tree
2021-02-24	Andrew Reynolds	Add interface to TheoryState for sort inference and...	commit \| commitdiff \| tree
2021-02-23	Andrew Reynolds	Explanation of failure for instantiate, use in enumerative...	commit \| commitdiff \| tree
2021-02-22	Andrew Reynolds	Eliminate raw use of output channel and valuation in...	commit \| commitdiff \| tree
2021-02-22	Andrew Reynolds	Move quantifiers attributes to quantifiers registry...	commit \| commitdiff \| tree
2021-02-22	Andrew Reynolds	(proof-new) Change proof-new option to proof (#5955)	commit \| commitdiff \| tree
2021-02-22	Andrew Reynolds	Require length-in-conclusion form for strings inferences...	commit \| commitdiff \| tree
2021-02-22	Andrew Reynolds	(proof-new) Option to automatically add SYMM steps...	commit \| commitdiff \| tree
2021-02-22	Andrew Reynolds	Fix datatypes inference manager when proofs are enabled...	commit \| commitdiff \| tree
2021-02-19	Andrew Reynolds	Simplify interface to instantiate (#5926)	commit \| commitdiff \| tree
2021-02-19	Andrew Reynolds	Fill in missing inference ids in datatypes theory ...	commit \| commitdiff \| tree
2021-02-19	Andrew Reynolds	Refactoring theory inference process (#5920)	commit \| commitdiff \| tree
2021-02-19	Andrew Reynolds	Fix rewrite for contains over replace (#5924)	commit \| commitdiff \| tree
2021-02-19	Andrew Reynolds	Remove string stat for inferences (#5932)	commit \| commitdiff \| tree
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
next

RSS Atom