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

2021-12-21	Andrew Reynolds	Support get-abduct-next (#7850)	commit \| commitdiff \| tree
2021-12-21	Andrew Reynolds	Eliminate remaining calls to callExtendedRewrite (...	commit \| commitdiff \| tree
2021-12-21	yoni206	Rewrite (pow2 x) to (pow 2 x) when x is a constant... Fixes https://github.com/cvc5/cvc5-projects/issues... Fixes https://github.com/cvc5/cvc5-projects/issues... Fixes https://github.com/cvc5/cvc5-projects/issues...	commit \| commitdiff \| tree
2021-12-21	Gereon Kremer	Disable unit tests without poly (#7844)	commit \| commitdiff \| tree
2021-12-21	Andrew Reynolds	Connect sequences array solver to strategy in theory...	commit \| commitdiff \| tree
2021-12-20	Andrew Reynolds	Eliminating some uses of const rational in arithmetic...	commit \| commitdiff \| tree
2021-12-20	Andrew Reynolds	Updates to LFSC signatures (#7840)	commit \| commitdiff \| tree
2021-12-20	Andrew Reynolds	Allow SyGuS subsolver to be reused in incremental mode...	commit \| commitdiff \| tree
2021-12-20	Andres Noetzli	[Sequences/Array Solver] Minor refactoring (#7843)	commit \| commitdiff \| tree
2021-12-20	Haniel Barbosa	[proofs] Fix helper LFSC script (#7845)	commit \| commitdiff \| tree
2021-12-17	Aina Niemetz	api: java: Support default arity for Solver::mkUnresolvedSor...	commit \| commitdiff \| tree
2021-12-17	Andres Noetzli	[Strings] Minor fixes/improvements (#7837)	commit \| commitdiff \| tree
2021-12-17	Ying Sheng	Array-inspired Sequence Solver - Fixing several issues...	commit \| commitdiff \| tree
2021-12-17	Andrew Reynolds	Simplify contrib/get-lfsc-checker and use cvc5 repo...	commit \| commitdiff \| tree
2021-12-17	Andres Noetzli	Fix rewrite for `str.update(str.rev(s), n, t))` (#7838) Fixes https://github.com/cvc5/cvc5-projects/issues...	commit \| commitdiff \| tree
2021-12-17	Andrew Reynolds	Minor refactoring of API for eliminating arithmetic...	commit \| commitdiff \| tree
2021-12-17	Gereon Kremer	Fix tracker in SubstitutionMap (#7829)	commit \| commitdiff \| tree
2021-12-17	mudathirmahgoub	Remove Rewriter::rewrite from bags type enumerator...	commit \| commitdiff \| tree
2021-12-17	Andrew Reynolds	Refactoring initialization of proofs (#7834)	commit \| commitdiff \| tree
2021-12-17	mudathirmahgoub	Add relations.cpp, relations.py examples (#7801)	commit \| commitdiff \| tree
2021-12-17	Alex Ozdemir	More documentation for idiomatic python API (#7798)	commit \| commitdiff \| tree
2021-12-17	Andrew Reynolds	Get getRealOrIntegerValueSign to the API (#7832)	commit \| commitdiff \| tree
2021-12-17	Andrew Reynolds	Implement model construction for the array extension...	commit \| commitdiff \| tree
2021-12-17	Aina Niemetz	api: Rename DatatypeSelector::getRangeSort() to getCodomainS...	commit \| commitdiff \| tree
2021-12-17	Aina Niemetz	api: Add Solver::mkUnresolvedSort(). (#7817)	commit \| commitdiff \| tree
2021-12-17	Andrew Reynolds	Eliminate more uses of CONST_RATIONAL (#7816)	commit \| commitdiff \| tree
2021-12-17	Mathias Preiner	Disable unsat cores for quaternion_ds1_symm_0428.fof...	commit \| commitdiff \| tree
2021-12-16	Andrew Reynolds	Eliminate most static calls to rewrite in quantifiers...	commit \| commitdiff \| tree
2021-12-16	Andrew Reynolds	Fix get-model when sort constructors are present (...	commit \| commitdiff \| tree
2021-12-16	Haniel Barbosa	[proofs] Simplifying and adding new utils to SAT proof...	commit \| commitdiff \| tree
2021-12-16	Aina Niemetz	api: Add Sort::hasSymbol() and Sort::getSymbol(). ...	commit \| commitdiff \| tree
2021-12-16	Andrew Reynolds	Minor fix for print benchmark. (#7821)	commit \| commitdiff \| tree
2021-12-16	yoni206	bv-to-int: use pow2 operator (#7812)	commit \| commitdiff \| tree
2021-12-16	yoni206	int-to-bv: fail if one of the arguments has type real...	commit \| commitdiff \| tree
2021-12-16	mudathirmahgoub	Add regression bags-of-bags-subtypes.smt2 (#7814)	commit \| commitdiff \| tree
2021-12-16	Andres Noetzli	Explicitly disallow `mkConst(Rational)` (#7818)	commit \| commitdiff \| tree
2021-12-15	Andrew Reynolds	Ensure match terms are exhaustive in its type rule...	commit \| commitdiff \| tree
2021-12-15	Aina Niemetz	api: Fix smt-lib code blocks and math in C++ docs....	commit \| commitdiff \| tree
2021-12-15	Andrew Reynolds	Add trace to see inferences in final proof (#7813)	commit \| commitdiff \| tree
2021-12-14	Andrew Reynolds	Eliminate static calls to rewrite in strings (#7803)	commit \| commitdiff \| tree
2021-12-14	mudathirmahgoub	Fix cvc5-projects issue 358 (#7804)	commit \| commitdiff \| tree
2021-12-14	Abdalrhman Mohamed	Add a random Sygus enumerator. (#7782)	commit \| commitdiff \| tree
2021-12-14	Gereon Kremer	Make some undocumented options regular/expert (#7805)	commit \| commitdiff \| tree
2021-12-14	Gereon Kremer	Fix issues with tracing builds (#7809)	commit \| commitdiff \| tree
2021-12-14	Andres Noetzli	Add switches to toggle eager and inclusion solvers...	commit \| commitdiff \| tree
2021-12-14	Andrew Reynolds	Connecting the core array solver in strings (#7800)	commit \| commitdiff \| tree
2021-12-14	Andrew Reynolds	Minor fix for sygus unsat query generator (#7811)	commit \| commitdiff \| tree
2021-12-14	Andrew Reynolds	Throw exception for getting value of non-well-founded...	commit \| commitdiff \| tree
2021-12-14	Andrew Reynolds	Eliminate use of rewrite, CONST_RATIONAL in ArithMSum...	commit \| commitdiff \| tree
2021-12-14	Aina Niemetz	api: Add note to Solver::mkDatatypeSorts. (#7799)	commit \| commitdiff \| tree
2021-12-13	Andrew Reynolds	Distinguishing more uses of CONST_RATIONAL (#7802)	commit \| commitdiff \| tree
2021-12-13	mudathirmahgoub	A more efficient implementation for bag.card operator...	commit \| commitdiff \| tree
2021-12-13	Andrew Reynolds	Initial cut at distinguishing uses of CONST_RATIONAL...	commit \| commitdiff \| tree
2021-12-13	Andrew Reynolds	Fixes and additions for API for parametric datatypes...	commit \| commitdiff \| tree
2021-12-13	mudathirmahgoub	Update Relations.java (#7796)	commit \| commitdiff \| tree
2021-12-13	Gereon Kremer	Improve nonlinear solver (#7787)	commit \| commitdiff \| tree
2021-12-13	yoni206	Integrate new int-blaster (#7781)	commit \| commitdiff \| tree
2021-12-13	mudathirmahgoub	Fix cvc5-projects issues #358 and #375 (#7743)	commit \| commitdiff \| tree
2021-12-10	Aina Niemetz	api: Use 'note' constructs for API documentation. ...	commit \| commitdiff \| tree
2021-12-10	Aina Niemetz	Reorganize declareDatatype unit tests. (#7767)	commit \| commitdiff \| tree
2021-12-10	Andrew Reynolds	Refactor and fixes related to getSpecializedConstructorTerm...	commit \| commitdiff \| tree
2021-12-10	Ying Sheng	Array-inspired Sequence Solver - Adding the ArrayCoreSolver...	commit \| commitdiff \| tree
2021-12-10	Gereon Kremer	Eliminate more static rewrites (#7786)	commit \| commitdiff \| tree
2021-12-10	Gereon Kremer	Some cleanup around trace and debug (#7792)	commit \| commitdiff \| tree
2021-12-10	Abdalrhman Mohamed	Mute `define-fun` command generated for named terms...	commit \| commitdiff \| tree
2021-12-10	Gereon Kremer	Allow for wildcards in `-t` (#7791)	commit \| commitdiff \| tree
2021-12-10	Haniel Barbosa	[proofs] Make LazyCDProofChain extend CDProof (#7726)	commit \| commitdiff \| tree
2021-12-10	Haniel Barbosa	[proofs] Add option to prune inputs from final proof...	commit \| commitdiff \| tree
2021-12-09	Andrew Reynolds	Consider polarity in relevance manager (#7768)	commit \| commitdiff \| tree
2021-12-09	Gereon Kremer	Fix sine symmetry proof (#7783)	commit \| commitdiff \| tree
2021-12-09	Andrew Reynolds	Remove a few static access to options in proof code...	commit \| commitdiff \| tree
2021-12-09	Andrew Reynolds	Do not make SyGuS subsolver in unsat state after solving...	commit \| commitdiff \| tree
2021-12-09	Aina Niemetz	api: Add note to Sort::getTesterCodomainSort(). (#7776)	commit \| commitdiff \| tree
2021-12-09	Mathias Preiner	test: Remove CDList memory limit test. (#7777)	commit \| commitdiff \| tree
2021-12-08	Andrew Reynolds	Return bool for lemmaTheoryInference (#7773)	commit \| commitdiff \| tree
2021-12-08	Gereon Kremer	Remove rewrites from iand and pow2 solvers (#7775)	commit \| commitdiff \| tree
2021-12-08	Gereon Kremer	Eliminate rewriter from transcendental solver (#7772)	commit \| commitdiff \| tree
2021-12-08	Gereon Kremer	Static options acceses again (#7771)	commit \| commitdiff \| tree
2021-12-08	Andrew Reynolds	Make several regressions faster (#7769)	commit \| commitdiff \| tree
2021-12-08	Andrew Reynolds	Fix type rule for datatype updater for parametric sorts...	commit \| commitdiff \| tree
2021-12-08	Gereon Kremer	Turn kinds in python API into a proper Enum (#7686)	commit \| commitdiff \| tree
2021-12-08	Aina Niemetz	api: Improve documentation for getDatatypeParamSorts...	commit \| commitdiff \| tree
2021-12-08	Aina Niemetz	api: Fix Sort::getDatatypeArity() for non-parametric...	commit \| commitdiff \| tree
2021-12-08	Aina Niemetz	FP: Remove static call to Rewriter. (#7765)	commit \| commitdiff \| tree
2021-12-08	Gereon Kremer	Improve options tests (#7761)	commit \| commitdiff \| tree
2021-12-07	Gereon Kremer	Remove more static accesses to options (#7764)	commit \| commitdiff \| tree
2021-12-07	Gereon Kremer	Simpler versioning if release flag is set (#7758)	commit \| commitdiff \| tree
2021-12-07	Andrew Reynolds	Add proof annotation option (#7750)	commit \| commitdiff \| tree
2021-12-07	mudathirmahgoub	Fix some java documentation links (#7757)	commit \| commitdiff \| tree
2021-12-07	Lachnitt	[proofs] Alethe: Add ARITH_TRICHOTOMY to updater (...	commit \| commitdiff \| tree
2021-12-07	Lachnitt	[proofs] Alethe: Fix Bug in Finalize (#7746)	commit \| commitdiff \| tree
2021-12-07	Andrew Reynolds	Allow sygus in incremental mode (#7756)	commit \| commitdiff \| tree
2021-12-07	Andrew Reynolds	Make data structures in relevance manager SAT-context...	commit \| commitdiff \| tree
2021-12-07	Andrew Reynolds	Eliminate more static calls to Rewriter::rewrite (...	commit \| commitdiff \| tree
2021-12-07	Andrew Reynolds	Towards support for incremental sygus (#7736)	commit \| commitdiff \| tree
2021-12-07	Andrew Reynolds	Eliminate more static calls to Rewriter::rewrite (...	commit \| commitdiff \| tree
2021-12-07	makaimann	Add bitwise option to IntBlaster (#7721)	commit \| commitdiff \| tree
2021-12-07	Gereon Kremer	Fix 32bit issue in sep_log_api test (#7752)	commit \| commitdiff \| tree
2021-12-07	mudathirmahgoub	Add documentation for QuickStart.java (#7730)	commit \| commitdiff \| tree
2021-12-06	Gereon Kremer	Disable option regression for competition build (#7751)	commit \| commitdiff \| tree
next

RSS Atom