| 2022-01-25 |
Mathias Preiner | Bump version to 0.0.6 |
commit | commitdiff | tree |
| 2022-01-25 |
Andres Noetzli | Send `nth(unit(...), ...)` terms to array solver (... |
commit | commitdiff | tree |
| 2022-01-25 |
Andrew Reynolds | Fixes 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 Kremer | Disable regression if poly is not available (#7981) |
commit | commitdiff | tree |
| 2022-01-24 |
Gereon Kremer | Always compile RANs (#7979) |
commit | commitdiff | tree |
| 2022-01-24 |
Gereon Kremer | Use proper RAN nodes for nl model (#7939) |
commit | commitdiff | tree |
| 2022-01-24 |
Gereon Kremer | Refactor 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 Kremer | Have RAN fall back to RANs (#7976) |
commit | commitdiff | tree |
| 2022-01-21 |
Andrew Reynolds | Ref count nodes in trigger trie (#7972) |
commit | commitdiff | tree |
| 2022-01-21 |
Andrew Reynolds | Fix trivial explantions in sequences array solver ... |
commit | commitdiff | tree |
| 2022-01-20 |
Andres Noetzli | Fix `Nth-Update` rule, add `Update-Bound` rule (#7968) |
commit | commitdiff | tree |
| 2022-01-20 |
Andrew Reynolds | Fix proofs for trivial cases of datatypes tester merge... |
commit | commitdiff | tree |
| 2022-01-20 |
Gereon Kremer | Refactor abs rewriting (#7935) |
commit | commitdiff | tree |
| 2022-01-20 |
Andres Noetzli | Fix CI build for macOS (#7970) |
commit | commitdiff | tree |
| 2022-01-19 |
Andres Noetzli | Add rewrites for `seq.update`/`seq.nth` (#7966) |
commit | commitdiff | tree |
| 2022-01-19 |
Gereon Kremer | Fix a subtle issue with double negations in coverings... |
commit | commitdiff | tree |
| 2022-01-19 |
Gereon Kremer | Make tracing for arithmetic rewriter more consistent... |
commit | commitdiff | tree |
| 2022-01-19 |
Gereon Kremer | Update to latest libpoly version (#7963) |
commit | commitdiff | tree |
| 2022-01-18 |
Andrew Reynolds | Distinguish purification types for strings proof recons... |
commit | commitdiff | tree |
| 2022-01-18 |
Gereon Kremer | Some 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 Sotoudeh | Fix CMake script for static, auto-download, cln configu... |
commit | commitdiff | tree |
| 2022-01-18 |
Andrew Reynolds | Print original form for substitutions and learned liter... |
commit | commitdiff | tree |
| 2022-01-17 |
Andrew Reynolds | Refactor 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 Kremer | Change how RANs are printed (#7955) |
commit | commitdiff | tree |
| 2022-01-15 |
Andrew Reynolds | Add inverse inference for update-over-concat (#7954) |
commit | commitdiff | tree |
| 2022-01-14 |
Andrew Reynolds | Improve names for sygus enumeration option (#7945) |
commit | commitdiff | tree |
| 2022-01-14 |
Andrew Reynolds | Clean enumerative instantiation options (#7947) |
commit | commitdiff | tree |
| 2022-01-14 |
Andrew Reynolds | Implement -o subs to show learned top-level substitutio... |
commit | commitdiff | tree |
| 2022-01-14 |
Alex Ozdemir | Rename python APIs (#7950) |
commit | commitdiff | tree |
| 2022-01-14 |
Gereon Kremer | Preprare central model building for RANs (#7951) |
commit | commitdiff | tree |
| 2022-01-14 |
Gereon Kremer | refactor div rewriter, add support for ran (#7941) |
commit | commitdiff | tree |
| 2022-01-14 |
Andrew Reynolds | Fix learned rewrite pass for non-real equalties (#7936) |
commit | commitdiff | tree |
| 2022-01-14 |
Gereon Kremer | Add operator<<(RewriteStatus) (#7952) |
commit | commitdiff | tree |
| 2022-01-14 |
Andrew Reynolds | Weaken assertion in relevance manager (#7943) |
commit | commitdiff | tree |
| 2022-01-14 |
Gereon Kremer | Refactor arithmetic pre-rewriter for multiplication... |
commit | commitdiff | tree |
| 2022-01-14 |
Gereon Kremer | Add support for RANs in rewriter for `MULT` (#7940) |
commit | commitdiff | tree |
| 2022-01-14 |
Gereon Kremer | Add RAN support in UMINUS rewriter (#7933) |
commit | commitdiff | tree |
| 2022-01-13 |
Gereon Kremer | Add arithmetic rewriter for RAN (#7929) |
commit | commitdiff | tree |
| 2022-01-13 |
Andrew Reynolds | Fix bug in evaluator for division by zero (#7942) |
commit | commitdiff | tree |
| 2022-01-13 |
Andres Noetzli | Unify abstract values and uninterpreted constants ... |
commit | commitdiff | tree |
| 2022-01-13 |
Gereon Kremer | Refactor post rewriter for addition (#7931) |
commit | commitdiff | tree |
| 2022-01-13 |
Gereon Kremer | Fix check whether we have a tag (#7901) |
commit | commitdiff | tree |
| 2022-01-12 |
Andrew Reynolds | Add -o learned-lits to output learned literals (#7934) |
commit | commitdiff | tree |
| 2022-01-12 |
Gereon Kremer | Refactor atom rewriting to be RAN-aware (#7928) |
commit | commitdiff | tree |
| 2022-01-12 |
Gereon Kremer | Refactor rewriteMinus (#7932) |
commit | commitdiff | tree |
| 2022-01-12 |
Andrew Reynolds | Ensure configuration of shared selectors is consistent... |
commit | commitdiff | tree |
| 2022-01-12 |
Gereon Kremer | Always enable RAN, but disable its implementation witho... |
commit | commitdiff | tree |
| 2022-01-12 |
Gereon Kremer | Add mkRealAlgebraicNumber (#7923) |
commit | commitdiff | tree |
| 2022-01-12 |
Andrew Reynolds | Always use partial function for sqrt (#7926) |
commit | commitdiff | tree |
| 2022-01-12 |
Andrew Reynolds | Eliminate use of subtyping from results of quantifier... |
commit | commitdiff | tree |
| 2022-01-11 |
Gereon Kremer | Adds 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 Noetzli | Fix `TypeNode::substitute()` for type constants (#7920) |
commit | commitdiff | tree |
| 2022-01-11 |
Aina Niemetz | api: Fix formatting of docs for Term::getSetValue(... |
commit | commitdiff | tree |
| 2022-01-11 |
Gereon Kremer | Remove static accesses to options (#7913) |
commit | commitdiff | tree |
| 2022-01-11 |
Andrew Reynolds | Tighten policy for unsat cores in sygus core connective... |
commit | commitdiff | tree |
| 2022-01-11 |
Andrew Reynolds | Guard use of unsat core mode pp-only (#7899) |
commit | commitdiff | tree |
| 2022-01-11 |
Andres Noetzli | Fix `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 Ozdemir | Add 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 Reynolds | Fix internal type error when printing lambdas with... |
commit | commitdiff | tree |
| 2022-01-10 |
Andrew Reynolds | Check arity in Sort::instantiate (#7897) |
commit | commitdiff | tree |
| 2022-01-10 |
Gereon Kremer | Add new methods for RealAlgebraicNumber (#7907) |
commit | commitdiff | tree |
| 2022-01-10 |
Gereon Kremer | Update to latest libpoly version (#7906) |
commit | commitdiff | tree |
| 2022-01-10 |
Aina Niemetz | api: Remove Sort::isComparableTo(). (#7903) |
commit | commitdiff | tree |
| 2022-01-10 |
Matthew Sotoudeh | Avoid gcc/10.1.0 bug by moving some configuration into... |
commit | commitdiff | tree |
| 2022-01-08 |
Mathias Preiner | Start post-release for 0.0.5 |
commit | commitdiff | tree |
| 2022-01-08 |
Mathias Preiner | Bump version to 0.0.5 |
commit | commitdiff | tree |
| 2022-01-07 |
Gereon Kremer | Improve docs extension for examples (#7900) |
commit | commitdiff | tree |
| 2022-01-07 |
Alex Ozdemir | Python Idomatic API: Document solver, results, utilitie... |
commit | commitdiff | tree |
| 2022-01-07 |
Matthew Sotoudeh | Remove CDDenseSet data structure (#7890) |
commit | commitdiff | tree |
| 2022-01-07 |
Andrew Reynolds | Fix eager string preprocessing in incremental mode... |
commit | commitdiff | tree |
| 2022-01-07 |
Gereon Kremer | Some minor improvements to the theory references (... |
commit | commitdiff | tree |
| 2022-01-07 |
Andrew Reynolds | Add regressions for array sequence solver (#7874) |
commit | commitdiff | tree |
| 2022-01-07 |
Alex Ozdemir | Document 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 Reynolds | Make alpha equivalence user context dependent (#7889) |
commit | commitdiff | tree |
| 2022-01-06 |
Andrew Reynolds | Disallow separation logic in incremental mode (#7888) |
commit | commitdiff | tree |
| 2022-01-06 |
Gereon Kremer | Improve theory combination in the presence of real... |
commit | commitdiff | tree |
| 2022-01-06 |
Andrew Reynolds | Fix non-idempotent rewrite in arrays (#7887) |
commit | commitdiff | tree |
| 2022-01-06 |
Andrew Reynolds | Minor cleaning of non-clausal simplification (#7886) |
commit | commitdiff | tree |
| 2022-01-05 |
Aina Niemetz | cppapi: Remove Datatype::hasNestedRecursion(). (#7878) |
commit | commitdiff | tree |
| 2022-01-05 |
Alex Ozdemir | Py idiomatic API: Doc sets, datatypes, FP (#7877) |
commit | commitdiff | tree |
| 2022-01-05 |
Aina Niemetz | api: Add missing guard for Datatype::isFinite(). (... |
commit | commitdiff | tree |
| 2022-01-05 |
Andrew Reynolds | Properly parse arithmetic values (#7876) |
commit | commitdiff | tree |
| 2022-01-05 |
Andrew Reynolds | Track input list for atoms in difficulty manager (... |
commit | commitdiff | tree |
| 2022-01-05 |
Alex Ozdemir | Don't use python's collections.Set (#7875) |
commit | commitdiff | tree |
| 2022-01-05 |
yoni206 | Properly set __file__ in python bindings (#7867) |
commit | commitdiff | tree |
| 2022-01-04 |
Andrew Reynolds | Fix proofs for datatype purify (#7841) |
commit | commitdiff | tree |
| 2022-01-04 |
Andrew Reynolds | Change default granularity of proofs to macro (#7855) |
commit | commitdiff | tree |
| 2022-01-04 |
Aina Niemetz | Reorder NodeManager class according to code guidelines... |
commit | commitdiff | tree |
| 2022-01-04 |
Andrew Reynolds | Add utility expr::isBooleanConnective (#7869) |
commit | commitdiff | tree |
| 2022-01-04 |
Andrew Reynolds | Remove spurious call to applySubs (#7871) |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog