cvc5.git
2022-01-21 Andrew ReynoldsRef count nodes in trigger trie (#7972)
2022-01-21 Andrew ReynoldsFix trivial explantions in sequences array solver ...
2022-01-20 Andres NoetzliFix `Nth-Update` rule, add `Update-Bound` rule (#7968)
2022-01-20 Andrew ReynoldsFix proofs for trivial cases of datatypes tester merge...
2022-01-20 Gereon KremerRefactor abs rewriting (#7935)
2022-01-20 Andres NoetzliFix CI build for macOS (#7970)
2022-01-19 Andres NoetzliAdd rewrites for `seq.update`/`seq.nth` (#7966)
2022-01-19 Gereon KremerFix a subtle issue with double negations in coverings...
2022-01-19 Gereon KremerMake tracing for arithmetic rewriter more consistent...
2022-01-19 Gereon KremerUpdate to latest libpoly version (#7963)
2022-01-18 Andrew ReynoldsDistinguish purification types for strings proof recons...
2022-01-18 Gereon KremerSome random documentation issues (#7921)
2022-01-18 Andres Noetzli[API] Add missing arity check (#7905)
2022-01-18 Matthew SotoudehFix CMake script for static, auto-download, cln configu...
2022-01-18 Andrew ReynoldsPrint original form for substitutions and learned liter...
2022-01-17 Andrew ReynoldsRefactor options related to rewriting and symmetry...
2022-01-17 Andres Noetzli[Strings] Fix rewriter for `re.loop` (#7956)
2022-01-15 Gereon KremerChange how RANs are printed (#7955)
2022-01-15 Andrew ReynoldsAdd inverse inference for update-over-concat (#7954)
2022-01-14 Andrew ReynoldsImprove names for sygus enumeration option (#7945)
2022-01-14 Andrew ReynoldsClean enumerative instantiation options (#7947)
2022-01-14 Andrew ReynoldsImplement -o subs to show learned top-level substitutio...
2022-01-14 Alex OzdemirRename python APIs (#7950)
2022-01-14 Gereon KremerPreprare central model building for RANs (#7951)
2022-01-14 Gereon Kremerrefactor div rewriter, add support for ran (#7941)
2022-01-14 Andrew ReynoldsFix learned rewrite pass for non-real equalties (#7936)
2022-01-14 Gereon KremerAdd operator<<(RewriteStatus) (#7952)
2022-01-14 Andrew ReynoldsWeaken assertion in relevance manager (#7943)
2022-01-14 Gereon KremerRefactor arithmetic pre-rewriter for multiplication...
2022-01-14 Gereon KremerAdd support for RANs in rewriter for `MULT` (#7940)
2022-01-14 Gereon KremerAdd RAN support in UMINUS rewriter (#7933)
2022-01-13 Gereon KremerAdd arithmetic rewriter for RAN (#7929)
2022-01-13 Andrew ReynoldsFix bug in evaluator for division by zero (#7942)
2022-01-13 Andres NoetzliUnify abstract values and uninterpreted constants ...
2022-01-13 Gereon KremerRefactor post rewriter for addition (#7931)
2022-01-13 Gereon KremerFix check whether we have a tag (#7901)
2022-01-12 Andrew ReynoldsAdd -o learned-lits to output learned literals (#7934)
2022-01-12 Gereon KremerRefactor atom rewriting to be RAN-aware (#7928)
2022-01-12 Gereon KremerRefactor rewriteMinus (#7932)
2022-01-12 Andrew ReynoldsEnsure configuration of shared selectors is consistent...
2022-01-12 Gereon KremerAlways enable RAN, but disable its implementation witho...
2022-01-12 Gereon KremerAdd mkRealAlgebraicNumber (#7923)
2022-01-12 Andrew ReynoldsAlways use partial function for sqrt (#7926)
2022-01-12 Andrew ReynoldsEliminate use of subtyping from results of quantifier...
2022-01-11 Gereon KremerAdds a kind to hold RealAlgebraicNumber constants ...
2022-01-11 Abdalrhman... Disable filtering of shapes in sygus-rcons pool. (...
2022-01-11 Andres NoetzliFix `TypeNode::substitute()` for type constants (#7920)
2022-01-11 Aina Niemetzapi: Fix formatting of docs for Term::getSetValue(...
2022-01-11 Gereon KremerRemove static accesses to options (#7913)
2022-01-11 Andrew ReynoldsTighten policy for unsat cores in sygus core connective...
2022-01-11 Andrew ReynoldsGuard use of unsat core mode pp-only (#7899)
2022-01-11 Andres NoetzliFix `TypeNode::substitute()` (#7916)
2022-01-11 Abdalrhman... Check the synthesized funs of `check-synth-next`. ...
2022-01-11 Alex OzdemirAdd new idiomatic examples (#7912)
2022-01-11 Andres Noetzli[Win64] Link LibPoly statically for static builds ...
2022-01-10 Andrew ReynoldsFix internal type error when printing lambdas with...
2022-01-10 Andrew ReynoldsCheck arity in Sort::instantiate (#7897)
2022-01-10 Gereon KremerAdd new methods for RealAlgebraicNumber (#7907)
2022-01-10 Gereon KremerUpdate to latest libpoly version (#7906)
2022-01-10 Aina Niemetzapi: Remove Sort::isComparableTo(). (#7903)
2022-01-10 Matthew SotoudehAvoid gcc/10.1.0 bug by moving some configuration into...
2022-01-08 Mathias PreinerStart post-release for 0.0.5
2022-01-08 Mathias PreinerBump version to 0.0.5
2022-01-07 Gereon KremerImprove docs extension for examples (#7900)
2022-01-07 Alex OzdemirPython Idomatic API: Document solver, results, utilitie...
2022-01-07 Matthew SotoudehRemove CDDenseSet data structure (#7890)
2022-01-07 Andrew ReynoldsFix eager string preprocessing in incremental mode...
2022-01-07 Gereon KremerSome minor improvements to the theory references (...
2022-01-07 Andrew ReynoldsAdd regressions for array sequence solver (#7874)
2022-01-07 Alex OzdemirDocument quantifiers in idiomatic python API (#7880)
2022-01-07 Andres Noetzli[Regressions] Add directive for disabling testers ...
2022-01-06 Andrew ReynoldsMake alpha equivalence user context dependent (#7889)
2022-01-06 Andrew ReynoldsDisallow separation logic in incremental mode (#7888)
2022-01-06 Gereon KremerImprove theory combination in the presence of real...
2022-01-06 Andrew ReynoldsFix non-idempotent rewrite in arrays (#7887)
2022-01-06 Andrew ReynoldsMinor cleaning of non-clausal simplification (#7886)
2022-01-05 Aina Niemetzcppapi: Remove Datatype::hasNestedRecursion(). (#7878)
2022-01-05 Alex OzdemirPy idiomatic API: Doc sets, datatypes, FP (#7877)
2022-01-05 Aina Niemetzapi: Add missing guard for Datatype::isFinite(). (...
2022-01-05 Andrew ReynoldsProperly parse arithmetic values (#7876)
2022-01-05 Andrew ReynoldsTrack input list for atoms in difficulty manager (...
2022-01-05 Alex OzdemirDon't use python's collections.Set (#7875)
2022-01-05 yoni206Properly set __file__ in python bindings (#7867)
2022-01-04 Andrew ReynoldsFix proofs for datatype purify (#7841)
2022-01-04 Andrew ReynoldsChange default granularity of proofs to macro (#7855)
2022-01-04 Aina NiemetzReorder NodeManager class according to code guidelines...
2022-01-04 Andrew ReynoldsAdd utility expr::isBooleanConnective (#7869)
2022-01-04 Andrew ReynoldsRemove spurious call to applySubs (#7871)
2022-01-04 Andrew ReynoldsRemove unused shutdown infrastructure (#7872)
2022-01-04 Andrew ReynoldsFix int blaster (#7856)
2022-01-04 mudathirmahgoubAdd bag.member operator to theory of bags (#7857)
2022-01-04 Haniel Barbosa[proofs] [sat] Add manager for optimized clauses and...
2022-01-04 mudathirmahgoubRefactor bag solver (#7770)
2022-01-04 yoni206Adding interpolation and abduction to the python API...
2022-01-04 Aina Niemetzapi: Add unit test for null case of Sort::toString...
2022-01-04 Aina Niemetzapi: Remove redundant check in Term::toString(). (...
2022-01-03 Andrew ReynoldsUpdate quantifiers compute elim symbols to be iterative...
2022-01-03 Andres Noetzli[BV] Remove non-existent `friend` class (#7864)
2022-01-03 Gereon KremerAdd download link for examples in documentation (#7836)
2022-01-03 Aina Niemetzapi: Remove redundant check in Sort::toString(). (...
next