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

2021-04-05	Andrew Reynolds	Add benchmark for issue 4412 (#6287)	commit \| commitdiff \| tree
2021-04-05	Haniel Barbosa	[proof-new] Registering proof checkers uniformly from...	commit \| commitdiff \| tree
2021-04-05	Andrew Reynolds	Enable UF when pre-skolem nested option is enabled...	commit \| commitdiff \| tree
2021-04-05	NicolaasWeideman	python: Fix type casting in mkBitVector (#6261)	commit \| commitdiff \| tree
2021-04-05	Andrew Reynolds	Fix subtyping for sets care graph (#6278)	commit \| commitdiff \| tree
2021-04-05	Andrew Reynolds	Add interface for skolem functions in SkolemManager...	commit \| commitdiff \| tree
2021-04-05	yoni206	A proposal for python api unit tests (#6255)	commit \| commitdiff \| tree
2021-04-05	Yancheng Ou	Optimizer for BitVectors (#6213)	commit \| commitdiff \| tree
2021-04-03	Andrew Reynolds	Disable substring component contains in strip endpoints...	commit \| commitdiff \| tree
2021-04-02	Gereon Kremer	Add cache for new dependencies folder. (#6265)	commit \| commitdiff \| tree
2021-04-02	Mathias Preiner	cmake: Do not link against main object library. (#6269)	commit \| commitdiff \| tree
2021-04-02	Gereon Kremer	New statistics registry (#6210)	commit \| commitdiff \| tree
2021-04-02	Gereon Kremer	Minor refactoring (#6273)	commit \| commitdiff \| tree
2021-04-02	Andrew Reynolds	Cleaning up friend relationships for commands (#6254)	commit \| commitdiff \| tree
2021-04-02	Andrew Reynolds	Fix case where RE unfolding generates a trivially true...	commit \| commitdiff \| tree
2021-04-02	Gereon Kremer	FindCaDiCaL: Avoid redirect to file (#6272)	commit \| commitdiff \| tree
2021-04-01	Gereon Kremer	Add utility classes for new statistics (#6178)	commit \| commitdiff \| tree
2021-04-01	Andrew Reynolds	Simplify caching of regular expression unfolding (...	commit \| commitdiff \| tree
2021-04-01	Aina Niemetz	FP: Factor out symfpu traits. (#6246)	commit \| commitdiff \| tree
2021-04-01	Andrew Reynolds	Fix type rule for to_real (#6257)	commit \| commitdiff \| tree
2021-04-01	Andrew Reynolds	Add regression for issue 6191 (#6264)	commit \| commitdiff \| tree
2021-04-01	Aina Niemetz	Delete hashsmt example. (#6263)	commit \| commitdiff \| tree
2021-04-01	Gereon Kremer	Refactor CLN dependency & Cleanup (#6251)	commit \| commitdiff \| tree
2021-04-01	Aina Niemetz	Rename namespace CVC5 to cvc5. (#6258)	commit \| commitdiff \| tree
2021-04-01	Aina Niemetz	kinds: Remove non-existent properties. (#6253)	commit \| commitdiff \| tree
2021-04-01	Andrew Reynolds	Add debug traces to theory inference manager (#6250)	commit \| commitdiff \| tree
2021-04-01	Andrew Reynolds	Fix non-linear for unknown case (#6252)	commit \| commitdiff \| tree
2021-04-01	Gereon Kremer	Make ResetCommand go through APISolver (#6172)	commit \| commitdiff \| tree
2021-03-31	Aina Niemetz	Rename namespace CVC4 to CVC5. (#6249)	commit \| commitdiff \| tree
2021-03-31	Gereon Kremer	Refactor GMP and Poly dependencies (#6245)	commit \| commitdiff \| tree
2021-03-31	Gereon Kremer	Refactor dependencies for external SAT solvers (#6215)	commit \| commitdiff \| tree
2021-03-31	Gereon Kremer	Refactor SymFPU dependency (#6218)	commit \| commitdiff \| tree
2021-03-31	Aina Niemetz	Bags: Move implementation of type rules from header...	commit \| commitdiff \| tree
2021-03-31	Aina Niemetz	Fix years in COPYING. (#6248)	commit \| commitdiff \| tree
2021-03-31	Andrew Reynolds	Eliminate dependencies on quantifiers engine in internal...	commit \| commitdiff \| tree
2021-03-31	Andrew Reynolds	Add missing inference ids (#6242)	commit \| commitdiff \| tree
2021-03-31	Aina Niemetz	FP: Move implementation of type rules from header to...	commit \| commitdiff \| tree
2021-03-31	yoni206	Fix compilation of Python bindings for named build...	commit \| commitdiff \| tree
2021-03-30	Andrew Reynolds	Fix printing for double patterns (#6235)	commit \| commitdiff \| tree
2021-03-30	Andrew Reynolds	Make SEXPR simply typed (#6160)	commit \| commitdiff \| tree
2021-03-30	Andrew Reynolds	Implement simple tracking of instantiation lemmas ...	commit \| commitdiff \| tree
2021-03-30	Andrew Reynolds	Refactoring quantifier annotation kinds, add kinds...	commit \| commitdiff \| tree
2021-03-30	Andrew Reynolds	Eliminate use of rational from tptp parser (#6239)	commit \| commitdiff \| tree
2021-03-30	Abdalrhman Mohamed	Give a better error when sygus grammar rules contain...	commit \| commitdiff \| tree
2021-03-30	Gereon Kremer	Fix total time statistic (#6233)	commit \| commitdiff \| tree
2021-03-30	Andrew Reynolds	Miscellaneous elimination of dependencies on quantifiers...	commit \| commitdiff \| tree
2021-03-29	Gereon Kremer	Add external project to install gtest (#6229)	commit \| commitdiff \| tree
2021-03-29	Andrew Reynolds	Eliminate the use of quantifiers engine in sygus solver...	commit \| commitdiff \| tree
2021-03-29	Aina Niemetz	Fix configuration printing. (#6236)	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-29	yoni206	Modular bv2int part 1 (#6212)	commit \| commitdiff \| tree
2021-03-29	Aina Niemetz	FloatingPointLiteral: Constructor for special consts...	commit \| commitdiff \| tree
2021-03-27	Andrew V. Jones	When building ANTLR via CMake, do not require javac...	commit \| commitdiff \| tree
2021-03-27	Gereon Kremer	Refactor ANTLR3 dependency (#6202)	commit \| commitdiff \| tree
2021-03-27	Aina Niemetz	Use color output to print configuration. (#6219)	commit \| commitdiff \| tree
2021-03-26	Aina Niemetz	FloatingPointLiteral: Make constructors that shouldn...	commit \| commitdiff \| tree
2021-03-26	Andrew Reynolds	Pass term registry to quantifiers modules (#6216)	commit \| commitdiff \| tree
2021-03-25	Gereon Kremer	Ensure nonlinear extensions properly reconsiders its...	commit \| commitdiff \| tree
2021-03-25	Aina Niemetz	FP: Refactor FloatingPointLiteral in preparation for...	commit \| commitdiff \| tree
2021-03-25	Andrew Reynolds	Refactor construction of triggers (#6209)	commit \| commitdiff \| tree
2021-03-25	Mathias Preiner	Do not use Configuration class in API black tests....	commit \| commitdiff \| tree
2021-03-25	Gereon Kremer	Add missing includes. (#6207)	commit \| commitdiff \| tree
2021-03-25	Haniel Barbosa	Deleting old LFSC signatures (#6194)	commit \| commitdiff \| tree
2021-03-24	Andrew Reynolds	Use inference manager to access intantiate utility...	commit \| commitdiff \| tree
2021-03-24	Gereon Kremer	Only consider relevant terms for integer branches ...	commit \| commitdiff \| tree
2021-03-24	Gereon Kremer	Refactor our integration of LFSC (#6201)	commit \| commitdiff \| tree
2021-03-23	Andrew Reynolds	Remove unused code for axioms (#6197)	commit \| commitdiff \| tree
2021-03-23	Haniel Barbosa	Removing unused build options and deprecated proof...	commit \| commitdiff \| tree
2021-03-23	Andrew Reynolds	Passing term registry to ematching utilities (#6190)	commit \| commitdiff \| tree
2021-03-23	Aina Niemetz	Remove internal includes of Api header. (#6193)	commit \| commitdiff \| tree
2021-03-23	Abdalrhman Mohamed	Replace old sygus term reconstruction algorithm with...	commit \| commitdiff \| tree
2021-03-23	Andrew Reynolds	Moving instantiate and skolemize into quantifiers inference...	commit \| commitdiff \| tree
2021-03-22	Gereon Kremer	Move statistics from the driver into the SmtEngine...	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	Aina Niemetz	FP: Add documentation for FloatingPointLiteral constructors...	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-20	mudathirmahgoub	Generate cvc/Kind.java for the java API (#6143)	commit \| commitdiff \| tree
2021-03-19	Andrew Reynolds	Refactor initialization of quantifiers model and builder...	commit \| commitdiff \| tree
2021-03-19	Aina Niemetz	BitVector: Change setBit to set the bit in place. ...	commit \| commitdiff \| tree
2021-03-19	Aina Niemetz	FP: Use setBit instead of bv or in conversion from...	commit \| commitdiff \| tree
2021-03-18	Haniel Barbosa	When giving an SMT-LIB version, defaulting to SMT-LIB...	commit \| commitdiff \| tree
2021-03-18	Gereon Kremer	Move stats registry to env. (#6173)	commit \| commitdiff \| tree
2021-03-18	Andrew Reynolds	Eliminate dependency on quantifiers engine in quantifiers...	commit \| commitdiff \| tree
2021-03-18	Abdalrhman Mohamed	Eliminate more uses of SExpr. (#6149)	commit \| commitdiff \| tree
2021-03-18	Aina Niemetz	New C++ Api: Comprehensive guards for member functions...	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-17	Aina Niemetz	New C++ Api: Comprehensive guards for member functions...	commit \| commitdiff \| tree
2021-03-17	Aina Niemetz	Rename test/unit/expr to test/unit/node. (#6156)	commit \| commitdiff \| tree
2021-03-17	Aina Niemetz	Rename fixtures in test/unit/context to conform to...	commit \| commitdiff \| tree
2021-03-17	Aina Niemetz	Rename fixtures in test/unit/base to conform to naming...	commit \| commitdiff \| tree
2021-03-16	Mathias Preiner	ci: Enable checking of proofs + unsat cores. (#6088)	commit \| commitdiff \| tree
2021-03-16	Haniel Barbosa	[proof-new] Activating proofs when dumping proofs ...	commit \| commitdiff \| tree
2021-03-16	Andrew Reynolds	Further standardization of strings statistics (#6128)	commit \| commitdiff \| tree
next

RSS Atom