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

2021-04-30	Mathias Preiner	bv: Refactor ppAssert and move to TheoryBV. (#6470)	commit \| commitdiff \| tree
2021-04-30	Aina Niemetz	Add parameter name for argument `isPreRewrite` for...	commit \| commitdiff \| tree
2021-04-30	Ouyancheng	Refactor optimization result and objective classes...	commit \| commitdiff \| tree
2021-04-30	Andrew Reynolds	Use substitutions for implementing defined functions...	commit \| commitdiff \| tree
2021-04-29	Andrew Reynolds	Add assertion list utility for justification heuristic...	commit \| commitdiff \| tree
2021-04-29	Gereon Kremer	Simplify generated code for getOption() and setOption...	commit \| commitdiff \| tree
2021-04-29	Gereon Kremer	Add missing include. (#6463)	commit \| commitdiff \| tree
2021-04-29	Gereon Kremer	Avoid exponential explosion of small constant in CEGQI...	commit \| commitdiff \| tree
2021-04-28	Ouyancheng	Fix BV Optimization Boundary Condition when lower bound...	commit \| commitdiff \| tree
2021-04-28	Gereon Kremer	Refactor resource manager options (#6446)	commit \| commitdiff \| tree
2021-04-28	Gereon Kremer	Remove exception headers from options.h (#6456)	commit \| commitdiff \| tree
2021-04-28	Gereon Kremer	Make sure reference stats are reset properly (#6457)	commit \| commitdiff \| tree
2021-04-28	Gereon Kremer	Clean up options holder class (#6458)	commit \| commitdiff \| tree
2021-04-28	Gereon Kremer	Cleanup DidYouMean (#6454)	commit \| commitdiff \| tree
2021-04-27	Andrew Reynolds	Add internal support for datatype update (#6450)	commit \| commitdiff \| tree
2021-04-27	Andrew Reynolds	Move slow regression to regress3 (#6451)	commit \| commitdiff \| tree
2021-04-27	Andrew Reynolds	Fix refutational soundness bug in quantifier prenexing...	commit \| commitdiff \| tree
2021-04-27	Andrew Reynolds	Simplify making function types (#6447)	commit \| commitdiff \| tree
2021-04-27	Gereon Kremer	Initial setup for docs of python API (#6445)	commit \| commitdiff \| tree
2021-04-27	Gereon Kremer	Use std::hash for API types (#6432)	commit \| commitdiff \| tree
2021-04-27	Aina Niemetz	Bool: Move implementation of type rules to cpp. (#6420)	commit \| commitdiff \| tree
2021-04-26	Gereon Kremer	Generate docs conf.py by cmake (#6441)	commit \| commitdiff \| tree
2021-04-26	Gereon Kremer	Protect int stats methods (#6442)	commit \| commitdiff \| tree
2021-04-26	Gereon Kremer	First part of options refactoring (#6428)	commit \| commitdiff \| tree
2021-04-26	Andrew Reynolds	Fix theoryOf for Boolean equalities (#6444)	commit \| commitdiff \| tree
2021-04-26	Diego Della Rocca...	New design in DOT representation, nodes colored based...	commit \| commitdiff \| tree
2021-04-26	Andrew Reynolds	Ensure dependency is tracked for all substitutions...	commit \| commitdiff \| tree
2021-04-26	Andrew Reynolds	Enable print-inst-full by default (#6435)	commit \| commitdiff \| tree
2021-04-26	Haniel Barbosa	Fix assertions in SAT solver (#6443)	commit \| commitdiff \| tree
2021-04-26	Andrew Reynolds	Do not process looping word equations over sequences...	commit \| commitdiff \| tree
2021-04-25	Andrew Reynolds	Use fast enumeration by default for Boolean predicate...	commit \| commitdiff \| tree
2021-04-25	Andrew Reynolds	More check models (#6439)	commit \| commitdiff \| tree
2021-04-24	Andrew Reynolds	Improve getValue for non-evaluated operators (#6436)	commit \| commitdiff \| tree
2021-04-24	Mathias Preiner	Add assumption-based unsat cores. (#6427)	commit \| commitdiff \| tree
2021-04-23	Gereon Kremer	Add missing dependency for CaDiCaL (#6431)	commit \| commitdiff \| tree
2021-04-23	Andrew Reynolds	(proof-new) Proofs for sets purification lemmas (#6416)	commit \| commitdiff \| tree
2021-04-23	Andrew Reynolds	Add new substitution apply methods fixpoint, sequential...	commit \| commitdiff \| tree
2021-04-23	Gereon Kremer	Make sure a ReferenceStat is set to values of the correct...	commit \| commitdiff \| tree
2021-04-23	Andrew Reynolds	Enable strings exp by default for strings specific...	commit \| commitdiff \| tree
2021-04-23	Aina Niemetz	BV: Add proof logging for bit-blasting. (#6373)	commit \| commitdiff \| tree
2021-04-23	Andrew Reynolds	Move implementation of UF rewriter to cpp (#6393)	commit \| commitdiff \| tree
2021-04-22	Andrew Reynolds	Make trust substitution map generate proofs lazily...	commit \| commitdiff \| tree
2021-04-22	Andrew Reynolds	Minor improvements to substitutions (#6380)	commit \| commitdiff \| tree
2021-04-22	Andrew Reynolds	Minor changes to unsat core default setting (#6425)	commit \| commitdiff \| tree
2021-04-22	Mathias Preiner	cmake: Do not require --auto-download for already downloaded...	commit \| commitdiff \| tree
2021-04-22	Gereon Kremer	Update INSTALL.md (#6412)	commit \| commitdiff \| tree
2021-04-22	Gereon Kremer	Add API documentation for statistics (#6364)	commit \| commitdiff \| tree
2021-04-22	Gereon Kremer	Remove unused stuff from options setup (#6422)	commit \| commitdiff \| tree
2021-04-22	Andrew Reynolds	Reorganizing use of skolem definition manager in prop...	commit \| commitdiff \| tree
2021-04-22	Andrew Reynolds	Fix models for sygus-inference, bv2int, real2int (...	commit \| commitdiff \| tree
2021-04-22	Haniel Barbosa	Reconciling proofs and unsat cores (#6405)	commit \| commitdiff \| tree
2021-04-22	Andres Noetzli	Allow in-place construction of `CDList` items (#6409)	commit \| commitdiff \| tree
2021-04-22	Andrew Reynolds	Move expand definition from Theory to TheoryRewriter...	commit \| commitdiff \| tree
2021-04-21	Aina Niemetz	Arithmetic: Move implementation of type rules to cpp...	commit \| commitdiff \| tree
2021-04-21	Aina Niemetz	UF: Move implementation of type rules to cpp. (#6403)	commit \| commitdiff \| tree
2021-04-21	Gereon Kremer	Add explicit dependencies for base lib (#6410)	commit \| commitdiff \| tree
2021-04-21	Gereon Kremer	Pass GMP to libpoly (#6411)	commit \| commitdiff \| tree
2021-04-21	Aina Niemetz	Datatypes: Move implementation of type rules to cpp...	commit \| commitdiff \| tree
2021-04-21	Mathias Preiner	Goodbye CVC4, hello cvc5! (#6371)	commit \| commitdiff \| tree
2021-04-21	Mathias Preiner	cmake: Add optional module name argument for check_python_mo...	commit \| commitdiff \| tree
2021-04-21	Aina Niemetz	Sets: Move implementation of type rules to cpp. (#6401)	commit \| commitdiff \| tree
2021-04-21	Aina Niemetz	Arrays: Move implementation of type rules to cpp. ...	commit \| commitdiff \| tree
2021-04-21	Andrew Reynolds	Add unit test for abduction (#6400)	commit \| commitdiff \| tree
2021-04-21	Andrew Reynolds	Add basic utilities for new implementation of justification...	commit \| commitdiff \| tree
2021-04-21	mudathirmahgoub	Add getNumIndices to Op (#6386)	commit \| commitdiff \| tree
2021-04-20	Andrew Reynolds	Split FP expand definitions to own module (#6392)	commit \| commitdiff \| tree
2021-04-20	Aina Niemetz	BV: Move implementation of type rules from header to...	commit \| commitdiff \| tree
2021-04-20	Aina Niemetz	Sep: Move implementation of type rules to cpp. (#6402)	commit \| commitdiff \| tree
2021-04-20	Aina Niemetz	Quantifiers: Move implementation of type rules to cpp...	commit \| commitdiff \| tree
2021-04-20	Gereon Kremer	Add InferenceId as resources (#6339)	commit \| commitdiff \| tree
2021-04-20	Andrew Reynolds	Add instantiation pool feature to the API (#6358)	commit \| commitdiff \| tree
2021-04-20	Gereon Kremer	Split C++ API docs from general docs (#6365)	commit \| commitdiff \| tree
2021-04-20	Aina Niemetz	Remove support for CVC3 language. (#6369)	commit \| commitdiff \| tree
2021-04-20	Gereon Kremer	Basic setup for examples in documentation (#6383)	commit \| commitdiff \| tree
2021-04-20	Aina Niemetz	Add guards to disable clang-format around placeholders...	commit \| commitdiff \| tree
2021-04-20	Andres Noetzli	Fix `ANTLR3_COMMAND` for system ANTLR3 JAR (#6399)	commit \| commitdiff \| tree
2021-04-20	Gereon Kremer	Properly link Poly against GMP (#6398)	commit \| commitdiff \| tree
2021-04-20	yoni206	python API sorts: adding functions and tests (#6361)	commit \| commitdiff \| tree
2021-04-19	Andrew Reynolds	Fully incorporate quantifiers macros into ppAssert...	commit \| commitdiff \| tree
2021-04-19	Gereon Kremer	Remove linking against gmp and cln in tests and parser...	commit \| commitdiff \| tree
2021-04-16	Gereon Kremer	Fix dependencies for stats options (#6378)	commit \| commitdiff \| tree
2021-04-16	Andrew Reynolds	Fix ONCE for post-rewrite (#6372)	commit \| commitdiff \| tree
2021-04-16	Gereon Kremer	Refactor cmake: auto-download and default-on dependencies...	commit \| commitdiff \| tree
2021-04-16	Gereon Kremer	Replace SExpr class by simpler conversion routines...	commit \| commitdiff \| tree
2021-04-16	Mathias Preiner	cmake: Build object libraries for base and context...	commit \| commitdiff \| tree
2021-04-15	Aina Niemetz	preprocessing context: Add wrapper for model substitutions...	commit \| commitdiff \| tree
2021-04-15	Mathias Preiner	Build support library from base and context. (#6368)	commit \| commitdiff \| tree
2021-04-15	Gereon Kremer	Avoid options listener for resource manager. (#6366)	commit \| commitdiff \| tree
2021-04-15	Aina Niemetz	Rename occurrences of CVC4 to CVC5. (#6351)	commit \| commitdiff \| tree
2021-04-15	Gereon Kremer	Fix printing of stats when aborted. (#6362)	commit \| commitdiff \| tree
2021-04-15	Andrew Reynolds	Reenable regression for minimizing instantiations ...	commit \| commitdiff \| tree
2021-04-14	Andrew Reynolds	Fix type rule for relations join image (#6349)	commit \| commitdiff \| tree
2021-04-14	Gereon Kremer	Improve documentation for FP rounding mode, add bibliography...	commit \| commitdiff \| tree
2021-04-14	Gereon Kremer	Improve documentation of API kinds (#6341)	commit \| commitdiff \| tree
2021-04-14	Gereon Kremer	Improve documentation for API exceptions (#6340)	commit \| commitdiff \| tree
2021-04-14	Gereon Kremer	Refactor / reimplement statistics (#6162)	commit \| commitdiff \| tree
2021-04-14	Aina Niemetz	Rename public and private headers in src/include. ...	commit \| commitdiff \| tree
2021-04-14	Haniel Barbosa	[unsat-cores] Improving new unsat cores (#6356)	commit \| commitdiff \| tree
2021-04-14	Andrew Reynolds	Add internal API methods for pool-based instantiation...	commit \| commitdiff \| tree
2021-04-14	Andrew Reynolds	Add interface for getting relevant assertions (#5131)	commit \| commitdiff \| tree
next

RSS Atom