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

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
2021-03-16	Mathias Preiner	cmake: Generate cvc4_export.h and set visibility to...	commit \| commitdiff \| tree
2021-03-16	Haniel Barbosa	[proof-new] Renaming proof option to be in sync with...	commit \| commitdiff \| tree
2021-03-16	Haniel Barbosa	[proof-new] Disabling proofs on regressions with known...	commit \| commitdiff \| tree
2021-03-16	Aina Niemetz	New C++ Api: Comprehensive guards for member functions...	commit \| commitdiff \| tree
2021-03-15	Andrew Reynolds	Fix rewrite for double replace (#6152)	commit \| commitdiff \| tree
2021-03-15	Aina Niemetz	New C++ Api: Comprehensive guards for member functions...	commit \| commitdiff \| tree
2021-03-15	Gereon Kremer	Replace HistogramStat by IntegralHistogramStat (#6126)	commit \| commitdiff \| tree
2021-03-15	Gereon Kremer	Disable sqlite (#6145)	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-15	Aina Niemetz	New C++ Api: Comprehensive guards for member functions...	commit \| commitdiff \| tree
2021-03-15	Aina Niemetz	New C++ Api: Comprehensive guards for member functions...	commit \| commitdiff \| tree
2021-03-14	Diego Della Rocca...	[proof-new] Adding a dot printer for proof nodes (...	commit \| commitdiff \| tree
2021-03-12	Aina Niemetz	New C++ Api: Move checks to separate file. (#6138)	commit \| commitdiff \| tree
2021-03-12	Aina Niemetz	New C++ API: Rename TRY CATCH macros. (#6135)	commit \| commitdiff \| tree
2021-03-12	Andres Noetzli	Schedule preregistration lemmas to be satisfied after...	commit \| commitdiff \| tree
2021-03-12	Mathias Preiner	cmake: Remove install rules for old API headers. (...	commit \| commitdiff \| tree
2021-03-12	Andrew Reynolds	(proof-new) Miscellaneous sync to master (#6129)	commit \| commitdiff \| tree
2021-03-12	Haniel Barbosa	[proof-new] Fix arity check when building equality...	commit \| commitdiff \| tree
2021-03-12	Gereon Kremer	Add missing includes for statistics (#6124)	commit \| commitdiff \| tree
2021-03-12	Andrew Reynolds	Simplify instantiation match generator interface (...	commit \| commitdiff \| tree
2021-03-12	Aina Niemetz	Add more unit tests for api::Sort. (#6122)	commit \| commitdiff \| tree
2021-03-12	Mathias Preiner	ci: Replace debug builds with assertion enabled production...	commit \| commitdiff \| tree
2021-03-11	Gereon Kremer	Make linear arithmetic use its inference manager (...	commit \| commitdiff \| tree
2021-03-11	Alex Ozdemir	arith proof rules shuffle & add ARITH_SUM_UB (#6118)	commit \| commitdiff \| tree
2021-03-11	Andrew Reynolds	Introduce inference ids for quantifier instantiation...	commit \| commitdiff \| tree
2021-03-11	Gereon Kremer	First refactoring of statistics classes (#6105)	commit \| commitdiff \| tree
2021-03-11	Aina Niemetz	Delete Expr layer. (#6117)	commit \| commitdiff \| tree
2021-03-11	MikolasJanota	Improvements and refactoring for enumeratative strategy...	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-11	Mathias Preiner	Fix compile warnings when compiling with GLPK. (#6115)	commit \| commitdiff \| tree
2021-03-11	Aina Niemetz	Remove obsolete test/api/statistics.cpp. (#6116)	commit \| commitdiff \| tree
2021-03-11	Aina Niemetz	Clean up ownership of Datatypes in NodeManager. (#6113)	commit \| commitdiff \| tree
2021-03-11	Aina Niemetz	Refactor Node::getOperator() to fix compiler warning...	commit \| commitdiff \| tree
2021-03-11	Mathias Preiner	Use CVC4_ASSERTIONS instead of NDEBUG. (#6099)	commit \| commitdiff \| tree
2021-03-11	Mathias Preiner	Add GitHub action to automatically update approved... Add GitHub action to automatically update...	commit \| commitdiff \| tree
next

RSS Atom