projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2022-01-14 Gereon Kremerrefactor div rewriter, add support for ran (#7941) commit | commitdiff | tree
2022-01-14 Andrew ReynoldsFix learned rewrite pass for non-real equalties (#7936) commit | commitdiff | tree
2022-01-14 Gereon KremerAdd operator<<(RewriteStatus) (#7952) commit | commitdiff | tree
2022-01-14 Andrew ReynoldsWeaken assertion in relevance manager (#7943) commit | commitdiff | tree
2022-01-14 Gereon KremerRefactor arithmetic pre-rewriter for multiplication... commit | commitdiff | tree
2022-01-14 Gereon KremerAdd support for RANs in rewriter for `MULT` (#7940) commit | commitdiff | tree
2022-01-14 Gereon KremerAdd RAN support in UMINUS rewriter (#7933) commit | commitdiff | tree
2022-01-13 Gereon KremerAdd arithmetic rewriter for RAN (#7929) commit | commitdiff | tree
2022-01-13 Andrew ReynoldsFix bug in evaluator for division by zero (#7942) commit | commitdiff | tree
2022-01-13 Andres NoetzliUnify abstract values and uninterpreted constants ... commit | commitdiff | tree
2022-01-13 Gereon KremerRefactor post rewriter for addition (#7931) commit | commitdiff | tree
2022-01-13 Gereon KremerFix check whether we have a tag (#7901) commit | commitdiff | tree
2022-01-12 Andrew ReynoldsAdd -o learned-lits to output learned literals (#7934) commit | commitdiff | tree
2022-01-12 Gereon KremerRefactor atom rewriting to be RAN-aware (#7928) commit | commitdiff | tree
2022-01-12 Gereon KremerRefactor rewriteMinus (#7932) commit | commitdiff | tree
2022-01-12 Andrew ReynoldsEnsure configuration of shared selectors is consistent... commit | commitdiff | tree
2022-01-12 Gereon KremerAlways enable RAN, but disable its implementation witho... commit | commitdiff | tree
2022-01-12 Gereon KremerAdd mkRealAlgebraicNumber (#7923) commit | commitdiff | tree
2022-01-12 Andrew ReynoldsAlways use partial function for sqrt (#7926) commit | commitdiff | tree
2022-01-12 Andrew ReynoldsEliminate use of subtyping from results of quantifier... commit | commitdiff | tree
2022-01-11 Gereon KremerAdds a kind to hold RealAlgebraicNumber constants ... commit | commitdiff | tree
2022-01-11 Abdalrhman... Disable filtering of shapes in sygus-rcons pool. (... commit | commitdiff | tree
2022-01-11 Andres NoetzliFix `TypeNode::substitute()` for type constants (#7920) commit | commitdiff | tree
2022-01-11 Aina Niemetzapi: Fix formatting of docs for Term::getSetValue(... commit | commitdiff | tree
2022-01-11 Gereon KremerRemove static accesses to options (#7913) commit | commitdiff | tree
2022-01-11 Andrew ReynoldsTighten policy for unsat cores in sygus core connective... commit | commitdiff | tree
2022-01-11 Andrew ReynoldsGuard use of unsat core mode pp-only (#7899) commit | commitdiff | tree
2022-01-11 Andres NoetzliFix `TypeNode::substitute()` (#7916) commit | commitdiff | tree
2022-01-11 Abdalrhman... Check the synthesized funs of `check-synth-next`. ... commit | commitdiff | tree
2022-01-11 Alex OzdemirAdd new idiomatic examples (#7912) commit | commitdiff | tree
2022-01-11 Andres Noetzli[Win64] Link LibPoly statically for static builds ... commit | commitdiff | tree
2022-01-10 Andrew ReynoldsFix internal type error when printing lambdas with... commit | commitdiff | tree
2022-01-10 Andrew ReynoldsCheck arity in Sort::instantiate (#7897) commit | commitdiff | tree
2022-01-10 Gereon KremerAdd new methods for RealAlgebraicNumber (#7907) commit | commitdiff | tree
2022-01-10 Gereon KremerUpdate to latest libpoly version (#7906) commit | commitdiff | tree
2022-01-10 Aina Niemetzapi: Remove Sort::isComparableTo(). (#7903) commit | commitdiff | tree
2022-01-10 Matthew SotoudehAvoid gcc/10.1.0 bug by moving some configuration into... commit | commitdiff | tree
2022-01-08 Mathias PreinerStart post-release for 0.0.5 commit | commitdiff | tree
2022-01-08 Mathias PreinerBump version to 0.0.5 commit | commitdiff | tree
2022-01-07 Gereon KremerImprove docs extension for examples (#7900) commit | commitdiff | tree
2022-01-07 Alex OzdemirPython Idomatic API: Document solver, results, utilitie... commit | commitdiff | tree
2022-01-07 Matthew SotoudehRemove CDDenseSet data structure (#7890) commit | commitdiff | tree
2022-01-07 Andrew ReynoldsFix eager string preprocessing in incremental mode... commit | commitdiff | tree
2022-01-07 Gereon KremerSome minor improvements to the theory references (... commit | commitdiff | tree
2022-01-07 Andrew ReynoldsAdd regressions for array sequence solver (#7874) commit | commitdiff | tree
2022-01-07 Alex OzdemirDocument quantifiers in idiomatic python API (#7880) commit | commitdiff | tree
2022-01-07 Andres Noetzli[Regressions] Add directive for disabling testers ... commit | commitdiff | tree
2022-01-06 Andrew ReynoldsMake alpha equivalence user context dependent (#7889) commit | commitdiff | tree
2022-01-06 Andrew ReynoldsDisallow separation logic in incremental mode (#7888) commit | commitdiff | tree
2022-01-06 Gereon KremerImprove theory combination in the presence of real... commit | commitdiff | tree
2022-01-06 Andrew ReynoldsFix non-idempotent rewrite in arrays (#7887) commit | commitdiff | tree
2022-01-06 Andrew ReynoldsMinor cleaning of non-clausal simplification (#7886) commit | commitdiff | tree
2022-01-05 Aina Niemetzcppapi: Remove Datatype::hasNestedRecursion(). (#7878) commit | commitdiff | tree
2022-01-05 Alex OzdemirPy idiomatic API: Doc sets, datatypes, FP (#7877) commit | commitdiff | tree
2022-01-05 Aina Niemetzapi: Add missing guard for Datatype::isFinite(). (... commit | commitdiff | tree
2022-01-05 Andrew ReynoldsProperly parse arithmetic values (#7876) commit | commitdiff | tree
2022-01-05 Andrew ReynoldsTrack input list for atoms in difficulty manager (... commit | commitdiff | tree
2022-01-05 Alex OzdemirDon't use python's collections.Set (#7875) commit | commitdiff | tree
2022-01-05 yoni206Properly set __file__ in python bindings (#7867) commit | commitdiff | tree
2022-01-04 Andrew ReynoldsFix proofs for datatype purify (#7841) commit | commitdiff | tree
2022-01-04 Andrew ReynoldsChange default granularity of proofs to macro (#7855) commit | commitdiff | tree
2022-01-04 Aina NiemetzReorder NodeManager class according to code guidelines... commit | commitdiff | tree
2022-01-04 Andrew ReynoldsAdd utility expr::isBooleanConnective (#7869) commit | commitdiff | tree
2022-01-04 Andrew ReynoldsRemove spurious call to applySubs (#7871) commit | commitdiff | tree
2022-01-04 Andrew ReynoldsRemove unused shutdown infrastructure (#7872) commit | commitdiff | tree
2022-01-04 Andrew ReynoldsFix int blaster (#7856) commit | commitdiff | tree
2022-01-04 mudathirmahgoubAdd bag.member operator to theory of bags (#7857) commit | commitdiff | tree
2022-01-04 Haniel Barbosa[proofs] [sat] Add manager for optimized clauses and... commit | commitdiff | tree
2022-01-04 mudathirmahgoubRefactor bag solver (#7770) commit | commitdiff | tree
2022-01-04 yoni206Adding interpolation and abduction to the python API... commit | commitdiff | tree
2022-01-04 Aina Niemetzapi: Add unit test for null case of Sort::toString... commit | commitdiff | tree
2022-01-04 Aina Niemetzapi: Remove redundant check in Term::toString(). (... commit | commitdiff | tree
2022-01-03 Andrew ReynoldsUpdate quantifiers compute elim symbols to be iterative... commit | commitdiff | tree
2022-01-03 Andres Noetzli[BV] Remove non-existent `friend` class (#7864) commit | commitdiff | tree
2022-01-03 Gereon KremerAdd download link for examples in documentation (#7836) commit | commitdiff | tree
2022-01-03 Aina Niemetzapi: Remove redundant check in Sort::toString(). (... commit | commitdiff | tree
2022-01-03 Gereon KremerRemove static options from sat solver. (#7790) commit | commitdiff | tree
2022-01-03 Andres NoetzliExecute `(reset)` command in parse-only mode (#7862) commit | commitdiff | tree
2021-12-23 Andres Noetzli[Regressions] Support more complex scrubbers (#7819) commit | commitdiff | tree
2021-12-22 Andrew ReynoldsRemove most uses of mkRationalNode (#7854) commit | commitdiff | tree
2021-12-22 Andrew ReynoldsAdd support for incremental + interpolants (#7853) commit | commitdiff | tree
2021-12-21 Andrew ReynoldsSupport get-abduct-next (#7850) commit | commitdiff | tree
2021-12-21 Andrew ReynoldsEliminate remaining calls to callExtendedRewrite (... commit | commitdiff | tree
2021-12-21 yoni206Rewrite (pow2 x) to (pow 2 x) when x is a constant... commit | commitdiff | tree
2021-12-21 Gereon KremerDisable unit tests without poly (#7844) commit | commitdiff | tree
2021-12-21 Andrew ReynoldsConnect sequences array solver to strategy in theory... commit | commitdiff | tree
2021-12-20 Andrew ReynoldsEliminating some uses of const rational in arithmetic... commit | commitdiff | tree
2021-12-20 Andrew ReynoldsUpdates to LFSC signatures (#7840) commit | commitdiff | tree
2021-12-20 Andrew ReynoldsAllow 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 Niemetzapi: java: Support default arity for Solver::mkUnresolv... commit | commitdiff | tree
2021-12-17 Andres Noetzli[Strings] Minor fixes/improvements (#7837) commit | commitdiff | tree
2021-12-17 Ying ShengArray-inspired Sequence Solver - Fixing several issues... commit | commitdiff | tree
2021-12-17 Andrew ReynoldsSimplify contrib/get-lfsc-checker and use cvc5 repo... commit | commitdiff | tree
2021-12-17 Andres NoetzliFix rewrite for `str.update(str.rev(s), n, t))` (#7838) commit | commitdiff | tree
2021-12-17 Andrew ReynoldsMinor refactoring of API for eliminating arithmetic... commit | commitdiff | tree
2021-12-17 Gereon KremerFix tracker in SubstitutionMap (#7829) commit | commitdiff | tree
2021-12-17 mudathirmahgoubRemove Rewriter::rewrite from bags type enumerator... commit | commitdiff | tree
2021-12-17 Andrew ReynoldsRefactoring initialization of proofs (#7834) commit | commitdiff | tree
next