projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2022-02-02 Andrew ReynoldsRemove more static calls to rewrite (#8025) commit | commitdiff | tree
2022-02-02 Andrew ReynoldsExtend proof step buffer to optionally ensure unique... commit | commitdiff | tree
2022-02-02 mudathirmahgoubFix parser issue with tuple_project operator (#8021) commit | commitdiff | tree
2022-02-01 Andres Noetzli[BV] Fix strategy for `RewriteExtract` (#8011) commit | commitdiff | tree
2022-02-01 Andres Noetzli[BV] Fix order of rewrites for `concat` (#8010) commit | commitdiff | tree
2022-02-01 Gereon KremerAdd new ordering utility (#8008) commit | commitdiff | tree
2022-02-01 Andrew ReynoldsAdd variant of get-difficulty for full effort lemmas... commit | commitdiff | tree
2022-02-01 Andres Noetzli[Arrays] Fix response for `store` chains (#8015) commit | commitdiff | tree
2022-02-01 mudathirmahgoubAdd bag.filter operator (#8006) commit | commitdiff | tree
2022-02-01 Gereon KremerConsider RANs in variable ordering (#7964) commit | commitdiff | tree
2022-01-31 Gereon KremerAdd utilities for flattening nodes (#7961) commit | commitdiff | tree
2022-01-31 Andres NoetzliFix memory leak in quantifier info (#8005) commit | commitdiff | tree
2022-01-29 Gereon KremerRename docs-releases to docs (#7999) commit | commitdiff | tree
2022-01-28 Mathias PreinerStart post-release for 0.0.7 commit | commitdiff | tree
2022-01-28 Mathias PreinerBump version to 0.0.7 commit | commitdiff | tree
2022-01-28 Bruno DutertreTry a bit harder on the EQ_NCTN rewrite rule (#7998) commit | commitdiff | tree
2022-01-28 Gereon KremerFix docs upload once again (#7997) commit | commitdiff | tree
2022-01-28 Andres Noetzli[Rewrite Synthesis] Fix args for non-chaining ops ... commit | commitdiff | tree
2022-01-27 Andrew ReynoldsDocument substitute in API (#7904) commit | commitdiff | tree
2022-01-27 Aina NiemetzUpdate AUTHORS und copyright of docs configuration... commit | commitdiff | tree
2022-01-27 Gereon KremerProperly recognize whether the current commit is a... commit | commitdiff | tree
2022-01-26 Andrew ReynoldsInitial refactoring of conflict-based instantiation... commit | commitdiff | tree
2022-01-26 mudathirmahgoubAdd Card solver to bags (#7986) commit | commitdiff | tree
2022-01-26 Andrew ReynoldsMore fixes and improvements for query generator (#7988) commit | commitdiff | tree
2022-01-25 Andrew ReynoldsAdd output -o post-asserts (#7987) commit | commitdiff | tree
2022-01-25 Mathias PreinerStart post-release for 0.0.6 commit | commitdiff | tree
2022-01-25 Mathias PreinerBump version to 0.0.6 commit | commitdiff | tree
2022-01-25 Andres NoetzliSend `nth(unit(...), ...)` terms to array solver (... commit | commitdiff | tree
2022-01-25 Andrew ReynoldsFixes and improvements to sygus satisfiable query gener... commit | commitdiff | tree
2022-01-25 Andres Noetzli[Strings] Avoid trivial explanation (#7982) commit | commitdiff | tree
2022-01-25 Andres Noetzli[Strings] Remove redundant call to rewriter (#7978) commit | commitdiff | tree
2022-01-25 Andres Noetzli[FP] Fix unused variable warning (#7977) commit | commitdiff | tree
2022-01-24 Gereon KremerDisable regression if poly is not available (#7981) commit | commitdiff | tree
2022-01-24 Gereon KremerAlways compile RANs (#7979) commit | commitdiff | tree
2022-01-24 Gereon KremerUse proper RAN nodes for nl model (#7939) commit | commitdiff | tree
2022-01-24 Gereon KremerRefactor how arith rewriting checks for mult-by-zero... commit | commitdiff | tree
2022-01-24 Abdalrhman... Enable dump tester. (#7884) commit | commitdiff | tree
2022-01-24 Gereon KremerHave RAN fall back to RANs (#7976) commit | commitdiff | tree
2022-01-21 Andrew ReynoldsRef count nodes in trigger trie (#7972) commit | commitdiff | tree
2022-01-21 Andrew ReynoldsFix trivial explantions in sequences array solver ... commit | commitdiff | tree
2022-01-20 Andres NoetzliFix `Nth-Update` rule, add `Update-Bound` rule (#7968) commit | commitdiff | tree
2022-01-20 Andrew ReynoldsFix proofs for trivial cases of datatypes tester merge... commit | commitdiff | tree
2022-01-20 Gereon KremerRefactor abs rewriting (#7935) commit | commitdiff | tree
2022-01-20 Andres NoetzliFix CI build for macOS (#7970) commit | commitdiff | tree
2022-01-19 Andres NoetzliAdd rewrites for `seq.update`/`seq.nth` (#7966) commit | commitdiff | tree
2022-01-19 Gereon KremerFix a subtle issue with double negations in coverings... commit | commitdiff | tree
2022-01-19 Gereon KremerMake tracing for arithmetic rewriter more consistent... commit | commitdiff | tree
2022-01-19 Gereon KremerUpdate to latest libpoly version (#7963) commit | commitdiff | tree
2022-01-18 Andrew ReynoldsDistinguish purification types for strings proof recons... commit | commitdiff | tree
2022-01-18 Gereon KremerSome random documentation issues (#7921) commit | commitdiff | tree
2022-01-18 Andres Noetzli[API] Add missing arity check (#7905) commit | commitdiff | tree
2022-01-18 Matthew SotoudehFix CMake script for static, auto-download, cln configu... commit | commitdiff | tree
2022-01-18 Andrew ReynoldsPrint original form for substitutions and learned liter... commit | commitdiff | tree
2022-01-17 Andrew ReynoldsRefactor options related to rewriting and symmetry... commit | commitdiff | tree
2022-01-17 Andres Noetzli[Strings] Fix rewriter for `re.loop` (#7956) commit | commitdiff | tree
2022-01-15 Gereon KremerChange how RANs are printed (#7955) commit | commitdiff | tree
2022-01-15 Andrew ReynoldsAdd inverse inference for update-over-concat (#7954) commit | commitdiff | tree
2022-01-14 Andrew ReynoldsImprove names for sygus enumeration option (#7945) commit | commitdiff | tree
2022-01-14 Andrew ReynoldsClean enumerative instantiation options (#7947) commit | commitdiff | tree
2022-01-14 Andrew ReynoldsImplement -o subs to show learned top-level substitutio... commit | commitdiff | tree
2022-01-14 Alex OzdemirRename python APIs (#7950) commit | commitdiff | tree
2022-01-14 Gereon KremerPreprare central model building for RANs (#7951) commit | commitdiff | tree
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
next