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

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
2020-12-14	Andrew Reynolds	Fix SAT-context dependent issue in strings preregistration...	commit \| commitdiff \| tree
2020-12-12	Andrew Reynolds	Flush statistics through NodeManager in SmtEngine ...	commit \| commitdiff \| tree
2020-12-11	Andrew Reynolds	Fix length assumption for deq norm emp rule (#5623)	commit \| commitdiff \| tree
2020-12-10	Andrew Reynolds	Refactor regressions (#5639)	commit \| commitdiff \| tree
2020-12-09	Andrew Reynolds	(proof-new) Make theory preprocessor proofs self contained...	commit \| commitdiff \| tree
2020-12-09	Andrew Reynolds	Make decision engine independent of AssertionsPipeline...	commit \| commitdiff \| tree
2020-12-09	Andrew Reynolds	Remove obsolete regressions (#5633)	commit \| commitdiff \| tree
2020-12-09	Andrew Reynolds	Ensure CEGQI is applied for parametric datatypes when...	commit \| commitdiff \| tree
2020-12-09	Andrew Reynolds	Do not check FP at last call if not necessary (#5627)	commit \| commitdiff \| tree
2020-12-08	Andrew Reynolds	Make term indices in the strings base solver aware...	commit \| commitdiff \| tree
2020-12-08	Andrew Reynolds	Proper implementation of expand definitions for sequences...	commit \| commitdiff \| tree
2020-12-08	Andrew Reynolds	Fix collect model values for sequences of sequences...	commit \| commitdiff \| tree
2020-12-07	Andrew Reynolds	Fix and reenable fact vs lemma optimization in datatypes...	commit \| commitdiff \| tree
2020-12-07	Andrew Reynolds	Fix issue with free variables introduced by quantifier...	commit \| commitdiff \| tree
2020-12-07	Andrew Reynolds	Do not expand theory definitions at the beginning of...	commit \| commitdiff \| tree
2020-12-07	Andrew Reynolds	(proof-new) Split proof ensure closed checks to own...	commit \| commitdiff \| tree
2020-12-07	Andrew Reynolds	Fix bugs in getFreeVariables (#5601)	commit \| commitdiff \| tree
2020-12-04	Andrew Reynolds	Fix bug in hasBoundVar (#5600)	commit \| commitdiff \| tree
2020-12-03	Andrew Reynolds	(proof-new) Updates to SMT proof manager and SmtEngine...	commit \| commitdiff \| tree
2020-12-03	Andrew Reynolds	Refactor handling of global declarations (#5577)	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	Remove Record object and convert to Node-level API...	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	Remove dagification visitor (#5574)	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	Add associative utilities to node manager (#5530)	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	Use new let binding for cvc printer (#5561)	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	(proof-new) Proofs for expand definitions (#5562)	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	Remove assertion related to CEGQI dependency lemmas...	commit \| commitdiff \| tree
2020-12-02	Andrew Reynolds	Fix issues related to model declarations (#5560)	commit \| commitdiff \| tree
2020-12-01	Andrew Reynolds	More fixes for quantifier elimination (#5533)	commit \| commitdiff \| tree
2020-11-30	Andrew Reynolds	Use new let binding in AST printer (#5529)	commit \| commitdiff \| tree
2020-11-30	Andrew Reynolds	Remove includes for old API from internal code (#5536)	commit \| commitdiff \| tree
2020-11-30	Andrew Reynolds	(proof-new) Proofs for regular expression elimination...	commit \| commitdiff \| tree
2020-11-26	Andrew Reynolds	Removing infrastructure related to SMT model (#5527)	commit \| commitdiff \| tree
2020-11-26	Andrew Reynolds	Move expand definitions to its own file (#5528)	commit \| commitdiff \| tree
2020-11-26	Andrew Reynolds	Fully decouple SmtEngine and the Expr layer (#5532)	commit \| commitdiff \| tree
2020-11-26	Andrew Reynolds	Fix missed case of theory preprocessing (#5531)	commit \| commitdiff \| tree
2020-11-26	Andrew Reynolds	Disable fact vs lemma optimization in datatypes for...	commit \| commitdiff \| tree
2020-11-25	Andrew Reynolds	Add regressions for closed issues (#5526)	commit \| commitdiff \| tree
2020-11-25	Andrew Reynolds	Use symbol manager for printing responses get-model...	commit \| commitdiff \| tree
2020-11-25	Andrew Reynolds	Allow printing of null node in let binder (#5523)	commit \| commitdiff \| tree
2020-11-23	Andrew Reynolds	Fix regular expression consume for nested star (#5518)	commit \| commitdiff \| tree
2020-11-23	Andrew Reynolds	Change UF ho to ppRewrite instead of expand definition...	commit \| commitdiff \| tree
2020-11-23	Andrew Reynolds	Fix for sygusToBuiltinEval for non-ground composite...	commit \| commitdiff \| tree
2020-11-23	Andrew Reynolds	(proof-new) Miscellaneous changes from proof-new (...	commit \| commitdiff \| tree
2020-11-23	Andrew Reynolds	Add declare model symbol methods to SymbolManager and...	commit \| commitdiff \| tree
next

RSS Atom