projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
[Win64] Link LibPoly statically for static builds (#7891)
[cvc5.git] / src /
2022-01-10 Andrew ReynoldsFix internal type error when printing lambdas with... tree | commitdiff
2022-01-10 Andrew ReynoldsCheck arity in Sort::instantiate (#7897) tree | commitdiff
2022-01-10 Gereon KremerAdd new methods for RealAlgebraicNumber (#7907) tree | commitdiff
2022-01-10 Aina Niemetzapi: Remove Sort::isComparableTo(). (#7903) tree | commitdiff
2022-01-10 Matthew SotoudehAvoid gcc/10.1.0 bug by moving some configuration into... tree | commitdiff
2022-01-07 Matthew SotoudehRemove CDDenseSet data structure (#7890) tree | commitdiff
2022-01-07 Andrew ReynoldsFix eager string preprocessing in incremental mode... tree | commitdiff
2022-01-06 Andrew ReynoldsMake alpha equivalence user context dependent (#7889) tree | commitdiff
2022-01-06 Andrew ReynoldsDisallow separation logic in incremental mode (#7888) tree | commitdiff
2022-01-06 Gereon KremerImprove theory combination in the presence of real... tree | commitdiff
2022-01-06 Andrew ReynoldsFix non-idempotent rewrite in arrays (#7887) tree | commitdiff
2022-01-06 Andrew ReynoldsMinor cleaning of non-clausal simplification (#7886) tree | commitdiff
2022-01-05 Aina Niemetzcppapi: Remove Datatype::hasNestedRecursion(). (#7878) tree | commitdiff
2022-01-05 Aina Niemetzapi: Add missing guard for Datatype::isFinite(). (... tree | commitdiff
2022-01-05 Andrew ReynoldsProperly parse arithmetic values (#7876) tree | commitdiff
2022-01-05 Andrew ReynoldsTrack input list for atoms in difficulty manager (... tree | commitdiff
2022-01-05 Alex OzdemirDon't use python's collections.Set (#7875) tree | commitdiff
2022-01-05 yoni206Properly set __file__ in python bindings (#7867) tree | commitdiff
2022-01-04 Andrew ReynoldsFix proofs for datatype purify (#7841) tree | commitdiff
2022-01-04 Andrew ReynoldsChange default granularity of proofs to macro (#7855) tree | commitdiff
2022-01-04 Aina NiemetzReorder NodeManager class according to code guidelines... tree | commitdiff
2022-01-04 Andrew ReynoldsAdd utility expr::isBooleanConnective (#7869) tree | commitdiff
2022-01-04 Andrew ReynoldsRemove spurious call to applySubs (#7871) tree | commitdiff
2022-01-04 Andrew ReynoldsRemove unused shutdown infrastructure (#7872) tree | commitdiff
2022-01-04 Andrew ReynoldsFix int blaster (#7856) tree | commitdiff
2022-01-04 mudathirmahgoubAdd bag.member operator to theory of bags (#7857) tree | commitdiff
2022-01-04 Haniel Barbosa[proofs] [sat] Add manager for optimized clauses and... tree | commitdiff
2022-01-04 mudathirmahgoubRefactor bag solver (#7770) tree | commitdiff
2022-01-04 yoni206Adding interpolation and abduction to the python API... tree | commitdiff
2022-01-04 Aina Niemetzapi: Remove redundant check in Term::toString(). (... tree | commitdiff
2022-01-03 Andrew ReynoldsUpdate quantifiers compute elim symbols to be iterative... tree | commitdiff
2022-01-03 Andres Noetzli[BV] Remove non-existent `friend` class (#7864) tree | commitdiff
2022-01-03 Aina Niemetzapi: Remove redundant check in Sort::toString(). (... tree | commitdiff
2022-01-03 Gereon KremerRemove static options from sat solver. (#7790) tree | commitdiff
2022-01-03 Andres NoetzliExecute `(reset)` command in parse-only mode (#7862) tree | commitdiff
2021-12-22 Andrew ReynoldsRemove most uses of mkRationalNode (#7854) tree | commitdiff
2021-12-22 Andrew ReynoldsAdd support for incremental + interpolants (#7853) tree | commitdiff
2021-12-21 Andrew ReynoldsSupport get-abduct-next (#7850) tree | commitdiff
2021-12-21 Andrew ReynoldsEliminate remaining calls to callExtendedRewrite (... tree | commitdiff
2021-12-21 yoni206Rewrite (pow2 x) to (pow 2 x) when x is a constant... tree | commitdiff
2021-12-21 Andrew ReynoldsConnect sequences array solver to strategy in theory... tree | commitdiff
2021-12-20 Andrew ReynoldsEliminating some uses of const rational in arithmetic... tree | commitdiff
2021-12-20 Andrew ReynoldsUpdates to LFSC signatures (#7840) tree | commitdiff
2021-12-20 Andrew ReynoldsAllow SyGuS subsolver to be reused in incremental mode... tree | commitdiff
2021-12-20 Andres Noetzli[Sequences/Array Solver] Minor refactoring (#7843) tree | commitdiff
2021-12-17 Aina Niemetzapi: java: Support default arity for Solver::mkUnresolv... tree | commitdiff
2021-12-17 Andres Noetzli[Strings] Minor fixes/improvements (#7837) tree | commitdiff
2021-12-17 Ying ShengArray-inspired Sequence Solver - Fixing several issues... tree | commitdiff
2021-12-17 Andres NoetzliFix rewrite for `str.update(str.rev(s), n, t))` (#7838) tree | commitdiff
2021-12-17 Andrew ReynoldsMinor refactoring of API for eliminating arithmetic... tree | commitdiff
2021-12-17 Gereon KremerFix tracker in SubstitutionMap (#7829) tree | commitdiff
2021-12-17 mudathirmahgoubRemove Rewriter::rewrite from bags type enumerator... tree | commitdiff
2021-12-17 Andrew ReynoldsRefactoring initialization of proofs (#7834) tree | commitdiff
2021-12-17 Andrew ReynoldsGet getRealOrIntegerValueSign to the API (#7832) tree | commitdiff
2021-12-17 Andrew ReynoldsImplement model construction for the array extension... tree | commitdiff
2021-12-17 Aina Niemetzapi: Rename DatatypeSelector::getRangeSort() to getCodo... tree | commitdiff
2021-12-17 Aina Niemetzapi: Add Solver::mkUnresolvedSort(). (#7817) tree | commitdiff
2021-12-17 Andrew ReynoldsEliminate more uses of CONST_RATIONAL (#7816) tree | commitdiff
2021-12-16 Andrew ReynoldsEliminate most static calls to rewrite in quantifiers... tree | commitdiff
2021-12-16 Andrew ReynoldsFix get-model when sort constructors are present (... tree | commitdiff
2021-12-16 Haniel Barbosa[proofs] Simplifying and adding new utils to SAT proof... tree | commitdiff
2021-12-16 Aina Niemetzapi: Add Sort::hasSymbol() and Sort::getSymbol(). ... tree | commitdiff
2021-12-16 Andrew ReynoldsMinor fix for print benchmark. (#7821) tree | commitdiff
2021-12-16 yoni206bv-to-int: use pow2 operator (#7812) tree | commitdiff
2021-12-16 yoni206int-to-bv: fail if one of the arguments has type real... tree | commitdiff
2021-12-16 mudathirmahgoubAdd regression bags-of-bags-subtypes.smt2 (#7814) tree | commitdiff
2021-12-16 Andres NoetzliExplicitly disallow `mkConst(Rational)` (#7818) tree | commitdiff
2021-12-15 Andrew ReynoldsEnsure match terms are exhaustive in its type rule... tree | commitdiff
2021-12-15 Aina Niemetzapi: Fix smt-lib code blocks and math in C++ docs.... tree | commitdiff
2021-12-15 Andrew ReynoldsAdd trace to see inferences in final proof (#7813) tree | commitdiff
2021-12-14 Andrew ReynoldsEliminate static calls to rewrite in strings (#7803) tree | commitdiff
2021-12-14 mudathirmahgoubFix cvc5-projects issue 358 (#7804) tree | commitdiff
2021-12-14 Abdalrhman MohamedAdd a random Sygus enumerator. (#7782) tree | commitdiff
2021-12-14 Gereon KremerMake some undocumented options regular/expert (#7805) tree | commitdiff
2021-12-14 Gereon KremerFix issues with tracing builds (#7809) tree | commitdiff
2021-12-14 Andres NoetzliAdd switches to toggle eager and inclusion solvers... tree | commitdiff
2021-12-14 Andrew ReynoldsConnecting the core array solver in strings (#7800) tree | commitdiff
2021-12-14 Andrew ReynoldsMinor fix for sygus unsat query generator (#7811) tree | commitdiff
2021-12-14 Andrew ReynoldsThrow exception for getting value of non-well-founded... tree | commitdiff
2021-12-14 Andrew ReynoldsEliminate use of rewrite, CONST_RATIONAL in ArithMSum... tree | commitdiff
2021-12-14 Aina Niemetzapi: Add note to Solver::mkDatatypeSorts. (#7799) tree | commitdiff
2021-12-13 Andrew ReynoldsDistinguishing more uses of CONST_RATIONAL (#7802) tree | commitdiff
2021-12-13 mudathirmahgoubA more efficient implementation for bag.card operator... tree | commitdiff
2021-12-13 Andrew ReynoldsInitial cut at distinguishing uses of CONST_RATIONAL... tree | commitdiff
2021-12-13 Andrew ReynoldsFixes and additions for API for parametric datatypes... tree | commitdiff
2021-12-13 Gereon KremerImprove nonlinear solver (#7787) tree | commitdiff
2021-12-13 yoni206Integrate new int-blaster (#7781) tree | commitdiff
2021-12-13 mudathirmahgoubFix cvc5-projects issues #358 and #375 (#7743) tree | commitdiff
2021-12-10 Aina Niemetzapi: Use 'note' constructs for API documentation. ... tree | commitdiff
2021-12-10 Andrew ReynoldsRefactor and fixes related to getSpecializedConstructor... tree | commitdiff
2021-12-10 Ying ShengArray-inspired Sequence Solver - Adding the ArrayCoreSo... tree | commitdiff
2021-12-10 Gereon KremerEliminate more static rewrites (#7786) tree | commitdiff
2021-12-10 Gereon KremerSome cleanup around trace and debug (#7792) tree | commitdiff
2021-12-10 Abdalrhman MohamedMute `define-fun` command generated for named terms... tree | commitdiff
2021-12-10 Gereon KremerAllow for wildcards in `-t` (#7791) tree | commitdiff
2021-12-10 Haniel Barbosa[proofs] Make LazyCDProofChain extend CDProof (#7726) tree | commitdiff
2021-12-10 Haniel Barbosa[proofs] Add option to prune inputs from final proof... tree | commitdiff
2021-12-09 Andrew ReynoldsConsider polarity in relevance manager (#7768) tree | commitdiff
2021-12-09 Gereon KremerFix sine symmetry proof (#7783) tree | commitdiff
2021-12-09 Andrew ReynoldsRemove a few static access to options in proof code... tree | commitdiff
next