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

2021-03-30	Andrew Reynolds	Eliminate use of rational from tptp parser (#6239)	commit \| commitdiff \| tree
2021-03-30	Andrew Reynolds	Miscellaneous elimination of dependencies on quantifiers...	commit \| commitdiff \| tree
2021-03-29	Andrew Reynolds	Eliminate the use of quantifiers engine in sygus solver...	commit \| commitdiff \| tree
2021-03-29	Andrew Reynolds	Eliminate use of quantifiers engine in enumerative...	commit \| commitdiff \| tree
2021-03-29	Andrew Reynolds	Move decision manager into theory inference manager...	commit \| commitdiff \| tree
2021-03-26	Andrew Reynolds	Pass term registry to quantifiers modules (#6216)	commit \| commitdiff \| tree
2021-03-25	Andrew Reynolds	Refactor construction of triggers (#6209)	commit \| commitdiff \| tree
2021-03-24	Andrew Reynolds	Use inference manager to access intantiate utility...	commit \| commitdiff \| tree
2021-03-23	Andrew Reynolds	Remove unused code for axioms (#6197)	commit \| commitdiff \| tree
2021-03-23	Andrew Reynolds	Passing term registry to ematching utilities (#6190)	commit \| commitdiff \| tree
2021-03-23	Andrew Reynolds	Moving instantiate and skolemize into quantifiers inference...	commit \| commitdiff \| tree
2021-03-22	Andrew Reynolds	Move equality query utility into quantifiers model...	commit \| commitdiff \| tree
2021-03-22	Andrew Reynolds	Function types are always first-class (#6167)	commit \| commitdiff \| tree
2021-03-22	Andrew Reynolds	Add skolem definition manager (#6187)	commit \| commitdiff \| tree
2021-03-22	Andrew Reynolds	Guard for non-unique skolems in term formula removal...	commit \| commitdiff \| tree
2021-03-21	Andrew Reynolds	Simplify strings term registration (#6174)	commit \| commitdiff \| tree
2021-03-21	Andrew Reynolds	Clean up remaining raw uses of output channel (#6161)	commit \| commitdiff \| tree
2021-03-20	Andrew Reynolds	Improved tracing for equivalence classes of EE (#6169)	commit \| commitdiff \| tree
2021-03-19	Andrew Reynolds	Refactor initialization of quantifiers model and builder...	commit \| commitdiff \| tree
2021-03-18	Andrew Reynolds	Eliminate dependency on quantifiers engine in quantifiers...	commit \| commitdiff \| tree
2021-03-17	Andrew Reynolds	(proof-new) Fixes to set defaults (#6163)	commit \| commitdiff \| tree
2021-03-17	Andrew Reynolds	Move utilities for inferred bounds on quantifers to...	commit \| commitdiff \| tree
2021-03-16	Andrew Reynolds	Further standardization of strings statistics (#6128)	commit \| commitdiff \| tree
2021-03-15	Andrew Reynolds	Fix rewrite for double replace (#6152)	commit \| commitdiff \| tree
2021-03-15	Andrew Reynolds	Make nonlinear extension account for relevant term...	commit \| commitdiff \| tree
2021-03-15	Andrew Reynolds	Split inst match generator class to own file (#6125)	commit \| commitdiff \| tree
2021-03-15	Andrew Reynolds	Letify quantifier bodies independently (#6112)	commit \| commitdiff \| tree
2021-03-15	Andrew Reynolds	Reorganizing initialization of term registry in quantifiers...	commit \| commitdiff \| tree
2021-03-12	Andrew Reynolds	(proof-new) Miscellaneous sync to master (#6129)	commit \| commitdiff \| tree
2021-03-12	Andrew Reynolds	Simplify instantiation match generator interface (...	commit \| commitdiff \| tree
2021-03-11	Andrew Reynolds	Introduce inference ids for quantifier instantiation...	commit \| commitdiff \| tree
2021-03-11	Andrew Reynolds	(proof-new) Clean up uses of witness with skolem lemmas...	commit \| commitdiff \| tree
2021-03-11	Andrew Reynolds	Direct lemmas and inference ids for sygus extension...	commit \| commitdiff \| tree
2021-03-10	Andrew Reynolds	Add Env class (#6093)	commit \| commitdiff \| tree
2021-03-10	Andrew Reynolds	(proof-new) Update ppRewrite to use skolem lemmas ...	commit \| commitdiff \| tree
2021-03-10	Andrew Reynolds	Fix extended equality rewrite involving replace. (...	commit \| commitdiff \| tree
2021-03-10	Andrew Reynolds	Fix term registration and non-theory-preprocessed terms...	commit \| commitdiff \| tree
2021-03-10	Andrew Reynolds	Add quant elim regression (#6103)	commit \| commitdiff \| tree
2021-03-10	Andrew Reynolds	(proof-new) Replace witness form by original form in...	commit \| commitdiff \| tree
2021-03-09	Andrew Reynolds	Merge initialization steps in TheoryModelBuilder (...	commit \| commitdiff \| tree
2021-03-09	Andrew Reynolds	Remove logic request (#6089)	commit \| commitdiff \| tree
2021-03-09	Andrew Reynolds	(proof-new) Minor fix and allow proof option (#6085)	commit \| commitdiff \| tree
2021-03-08	Andrew Reynolds	Fix handling of negation of Boolean bound variables...	commit \| commitdiff \| tree
2021-03-08	Andrew Reynolds	(proof-new) Separating optimizations for strings skolem...	commit \| commitdiff \| tree
2021-03-08	Andrew Reynolds	(proof-new) Prepare arithmetic for changes to ppRewrite...	commit \| commitdiff \| tree
2021-03-08	Andrew Reynolds	Simplify theory preprocessing (#6058)	commit \| commitdiff \| tree
2021-03-08	Andrew Reynolds	Do not process conjunctions as facts in strings (#6065)	commit \| commitdiff \| tree
2021-03-03	Andrew Reynolds	(proof-new) Simplifications to arithmetic operator...	commit \| commitdiff \| tree
2021-03-02	Andrew Reynolds	Introduce quantifiers term registry (#5983)	commit \| commitdiff \| tree
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
next

RSS Atom