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

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
2021-03-10	Mathias Preiner	Use Assert instead of assert. (#6095)	commit \| commitdiff \| tree
2021-03-10	Aina Niemetz	New C++ Api: Add missing argument checks in Solver...	commit \| commitdiff \| tree
2021-03-10	Andrew Reynolds	Add Env class (#6093)	commit \| commitdiff \| tree
2021-03-10	Andrew V. Jones	Improved handing of 'lib64' vs. 'lib' for glpk-cut...	commit \| commitdiff \| tree
2021-03-10	Haniel Barbosa	[proof-new] Clarifying doc (#6108)	commit \| commitdiff \| tree
2021-03-10	Aina Niemetz	Move ExprManager::isNAryKind to NodeManager. (#6107)	commit \| commitdiff \| tree
2021-03-10	Gereon Kremer	Improve arithmetic proofs (#6106)	commit \| commitdiff \| tree
2021-03-10	Mathias Preiner	cmake: Fix optimization level for debug builds. (#6097)	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-10	Mathias Preiner	test: Fix missing std::. (#6096)	commit \| commitdiff \| tree
2021-03-09	Aina Niemetz	New C++ Api: Use const ref for arguments when possible...	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	Aina Niemetz	New C++ Api: Migrate stats collection for consts, vars...	commit \| commitdiff \| tree
next

RSS Atom