| 2019-05-18 |
Andres Noetzli | Fix BV ITE rewrite (#3004) |
tree | commitdiff |
| 2019-05-17 |
Martin | Add the problematic input from issue 2183 as a regressi... |
tree | commitdiff |
| 2019-05-15 |
Andres Noetzli | Fix model of Boolean vars with eager bit-blaster (... |
tree | commitdiff |
| 2019-05-15 |
Andrew Reynolds | Fix printing of bvurem (#2963) |
tree | commitdiff |
| 2019-05-09 |
Andrew Reynolds | Fixes for relational triggers (#2967) |
tree | commitdiff |
| 2019-05-06 |
Andres Noetzli | Add support for re.all (#2980) |
tree | commitdiff |
| 2019-05-01 |
Andrew Reynolds | Fix re-elim-agg regressions (#2987) |
tree | commitdiff |
| 2019-05-01 |
Andrew Reynolds | Use total versions of div/mod in re-elim-agg (#2986) |
tree | commitdiff |
| 2019-04-30 |
Andres Noetzli | Fix concat-find regexp elimination (#2983) |
tree | commitdiff |
| 2019-04-30 |
Andrew Reynolds | Remove stoi solve rewrite (#2985) |
tree | commitdiff |
| 2019-04-30 |
Andrew Reynolds | Eliminate APPLY kind (#2976) |
tree | commitdiff |
| 2019-04-26 |
Aina Niemetz | New C++ API: Clean up API: mkVar vs mkConst vs mkBoundV... |
tree | commitdiff |
| 2019-04-17 |
Andrew Reynolds | Fix extended function decomposition (#2960) |
tree | commitdiff |
| 2019-04-16 |
Andres Noetzli | Make bv{add,mul,and,or,xor,xnor} left-associative ... |
tree | commitdiff |
| 2019-04-16 |
Andrew Reynolds | Stratify enumerative instantiation (#2954) |
tree | commitdiff |
| 2019-04-16 |
Andrew Reynolds | Minor simplifications to theory quantifiers (#2953) |
tree | commitdiff |
| 2019-04-11 |
Andrew Reynolds | Eliminate Boolean ITE within terms, fixes 2947 (#2949) |
tree | commitdiff |
| 2019-04-05 |
Andrew Reynolds | Fix another corner case of datatypes+PBE (#2938) |
tree | commitdiff |
| 2019-04-05 |
Haniel Barbosa | fix fp issue (#2940) |
tree | commitdiff |
| 2019-04-04 |
Haniel Barbosa | Ignoring FP benchmarks with "unsafe" sizes unless optio... |
tree | commitdiff |
| 2019-04-03 |
Aina Niemetz | Update copyright headers. |
tree | commitdiff |
| 2019-04-03 |
Andrew Reynolds | Fix combination of datatypes + strings in PBE (#2930) |
tree | commitdiff |
| 2019-04-01 |
Andres Noetzli | FP: Fix wrong model due to partial assignment (#2910) |
tree | commitdiff |
| 2019-04-01 |
Andres Noetzli | Fix RewriteITEBv to ensure rewrite to fixpoint (#2878) |
tree | commitdiff |
| 2019-04-01 |
Andres Noetzli | Move slow string regression to regress3 (#2913) |
tree | commitdiff |
| 2019-03-29 |
Andrew Reynolds | Apply empty splits more aggressively in sets+cardinalit... |
tree | commitdiff |
| 2019-03-29 |
Andres Noetzli | Fix freeing nodes with maxed refcounts (#2903) |
tree | commitdiff |
| 2019-03-29 |
Andrew Reynolds | Fix issues in cvc parser (#2901) |
tree | commitdiff |
| 2019-03-26 |
Aina Niemetz | Update copyright headers. |
tree | commitdiff |
| 2019-03-24 |
Aina Niemetz | BV: Fix typerules for rotate operators. (#2895) |
tree | commitdiff |
| 2019-03-23 |
Andres Noetzli | Fix memory leak when using subsolvers (#2893) |
tree | commitdiff |
| 2019-03-23 |
Andres Noetzli | Strip non-matching beginning from indexof operator... |
tree | commitdiff |
| 2019-03-22 |
Andrew Reynolds | More fixes for PBE with datatypes (#2882) |
tree | commitdiff |
| 2019-03-22 |
Andres Noetzli | Fix stripConstantEndpoints in strings rewriter (#2883) |
tree | commitdiff |
| 2019-03-21 |
Andrew Reynolds | Rewrite selectors correctly applied to constructors... |
tree | commitdiff |
| 2019-03-20 |
Andrew Reynolds | Sygus abduction feature (#2744) |
tree | commitdiff |
| 2019-03-19 |
Andrew Reynolds | Fix fairness issue with fast sygus enumerator (#2873) |
tree | commitdiff |
| 2019-03-19 |
Aina Niemetz | New C++: Remove redundant mkBoundVar function. |
tree | commitdiff |
| 2019-03-19 |
Aina Niemetz | New C++: Remove redundant mkVar function. |
tree | commitdiff |
| 2019-03-18 |
Aina Niemetz | BitVector: Allow base 10 in constructor. (#2870) |
tree | commitdiff |
| 2019-03-16 |
Alex Ozdemir | Enable CryptoMiniSat-backed BV proofs (#2847) |
tree | commitdiff |
| 2019-03-15 |
Haniel Barbosa | New beta-reduction for HOL solving (#2869) |
tree | commitdiff |
| 2019-03-14 |
Andrew Reynolds | Use zero slope tangent planes for transcendental functi... |
tree | commitdiff |
| 2019-03-14 |
Andrew Reynolds | Implement proper semantics for TPTP predicate is_rat... |
tree | commitdiff |
| 2019-03-12 |
Andrew Reynolds | Move tuple/record update elimination from ppRewrite... |
tree | commitdiff |
| 2019-03-01 |
Alex Ozdemir | ErProof class with LFSC output (#2812) |
tree | commitdiff |
| 2019-02-13 |
Aina Niemetz | New C++ API: Remove redundant declareFun function.... |
tree | commitdiff |
| 2019-02-13 |
Andres Noetzli | Rewrite simple regexp pattern to str.contains (#2827) |
tree | commitdiff |
| 2019-02-13 |
Aina Niemetz | New C++ API: Remove redundant mkTerm function. (#2836) |
tree | commitdiff |
| 2019-02-11 |
Aina Niemetz | New C++ API: Unit tests for declare* functions. (#2831) |
tree | commitdiff |
| 2019-02-05 |
Andres Noetzli | Make stripConstantEndpoints() less aggressive (#2830) |
tree | commitdiff |
| 2019-02-04 |
Andres Noetzli | Add rewrite for contains + const strings replace (... |
tree | commitdiff |
| 2019-02-02 |
Andres Noetzli | Fix corner case in stripConstantEndpoints (#2824) |
tree | commitdiff |
| 2019-01-29 |
Andres Noetzli | Fix warning due to catching polymorphic exceptions... |
tree | commitdiff |
| 2019-01-29 |
Aina Niemetz | New C++ API: Fix checks for mkTerm. (#2820) |
tree | commitdiff |
| 2019-01-29 |
Andres Noetzli | Strings: Remove redundant replace rewrite (#2822) |
tree | commitdiff |
| 2019-01-23 |
Andres Noetzli | Strings: Strengthen multiset reasoning (#2817) |
tree | commitdiff |
| 2019-01-22 |
Andrew Reynolds | Fix tuple and record CVC printing (#2818) |
tree | commitdiff |
| 2019-01-22 |
Andrew Reynolds | Fix parsing of overloaded parametric datatype selector... |
tree | commitdiff |
| 2019-01-17 |
Andres Noetzli | Add option to print BV constants in binary (#2805) |
tree | commitdiff |
| 2019-01-16 |
Andrew Reynolds | Fix constant contains ITOS rewrite (#2799) |
tree | commitdiff |
| 2019-01-15 |
Andrew Reynolds | Fix unsound double abs rewrite rule for FP (#2792) |
tree | commitdiff |
| 2019-01-13 |
Alex Ozdemir | LFSC LRAT Output (#2787) |
tree | commitdiff |
| 2019-01-11 |
Aina Niemetz | New C++ API: Add unit tests for setInfo, setLogic,... |
tree | commitdiff |
| 2019-01-10 |
Aina Niemetz | New C++ API: Get rid of mkConst functions (simplify... |
tree | commitdiff |
| 2019-01-09 |
Andrew Reynolds | Do not rewrite 1-constructor sygus testers to true... |
tree | commitdiff |
| 2019-01-09 |
Alex Ozdemir | Clause proof printing (#2779) |
tree | commitdiff |
| 2019-01-09 |
Alex Ozdemir | LFSC drat output (#2776) |
tree | commitdiff |
| 2019-01-07 |
Aina Niemetz | New C++ API: Add missing getType() calls to kick off... |
tree | commitdiff |
| 2019-01-06 |
Alex Ozdemir | [DRAT] DRAT data structure (#2767) |
tree | commitdiff |
| 2019-01-04 |
Andres Noetzli | C++ API: Fix OOB read in unit test (#2774) |
tree | commitdiff |
| 2019-01-03 |
Andres Noetzli | API/Smt2 parser: refactor termAtomic (#2674) |
tree | commitdiff |
| 2019-01-03 |
Andres Noetzli | C++ API: Reintroduce zero-value mkBitVector method... |
tree | commitdiff |
| 2019-01-03 |
Aina Niemetz | New C++ API: Add tests for mk-functions in solver objec... |
tree | commitdiff |
| 2018-12-19 |
Andrew Reynolds | Fix issues with REWRITE_DONE in floating point rewriter... |
tree | commitdiff |
| 2018-12-17 |
Aina Niemetz | New C++ API: Add tests for term object. (#2755) |
tree | commitdiff |
| 2018-12-14 |
Aina Niemetz | New C++ API: Add tests for opterm object. (#2756) |
tree | commitdiff |
| 2018-12-14 |
Andrew Reynolds | Fix extended rewriter for binary associative operators... |
tree | commitdiff |
| 2018-12-13 |
Aina Niemetz | New C++ API: Add tests for sort functions of solver... |
tree | commitdiff |
| 2018-12-12 |
Andres Noetzli | API: Add simple empty/sigma regexp unit tests (#2746) |
tree | commitdiff |
| 2018-12-11 |
Andrew Reynolds | Remove alternate versions of mbqi (#2742) |
tree | commitdiff |
| 2018-12-10 |
makaimann | BoolToBV modes (off, ite, all) (#2530) |
tree | commitdiff |
| 2018-12-07 |
Andres Noetzli | Strings: Make EXTF_d inference more conservative (... |
tree | commitdiff |
| 2018-12-07 |
Alex Ozdemir | Enable BV proofs when using an eager bitblaster (#2733) |
tree | commitdiff |
| 2018-11-28 |
Andrew Reynolds | Optimize re-elim for re.allchar components (#2725) |
tree | commitdiff |
| 2018-11-28 |
Andres Noetzli | Improve skolem caching by normalizing skolem args ... |
tree | commitdiff |
| 2018-11-22 |
Andres Noetzli | Add rewrite for (str.substr s x y) --> "" (#2695) |
tree | commitdiff |
| 2018-11-21 |
Andrew Reynolds | Quickly recognize when PBE conjectures are infeasible... |
tree | commitdiff |
| 2018-11-21 |
Andrew Reynolds | Support string replace all (#2704) |
tree | commitdiff |
| 2018-11-20 |
Andrew Reynolds | Fix real2int regression. (#2716) |
tree | commitdiff |
| 2018-11-19 |
Andrew Reynolds | Fix E-matching for case where candidate generator is... |
tree | commitdiff |
| 2018-11-08 |
Andres Noetzli | Evaluator: add support for str.code (#2696) |
tree | commitdiff |
| 2018-11-07 |
Haniel Barbosa | Adding default SyGuS grammar construction for arrays... |
tree | commitdiff |
| 2018-11-07 |
Andres Noetzli | Fix collectEmptyEqs in string rewriter (#2692) |
tree | commitdiff |
| 2018-11-05 |
Aina Niemetz | New C++ API: Split unit tests. (#2688) |
tree | commitdiff |
| 2018-11-05 |
yoni206 | Increasing coverage (#2683) |
tree | commitdiff |
| 2018-11-05 |
Andres Noetzli | API: Fix assignment operators (#2680) |
tree | commitdiff |
| 2018-11-05 |
Andrew Reynolds | Allow partial models with optimized sygus enumeration... |
tree | commitdiff |
| 2018-11-02 |
yoni206 | fixes to regression docs (#2679) |
tree | commitdiff |
| 2018-10-22 |
Andres Noetzli | Recover from wrong use of get-info :reason-unknown... |
tree | commitdiff |
| next |
projects / cvc5.git / history