2019-06-27 |
Andrew Reynolds | Variable elimination rewrite for quantified strings... |
tree | commitdiff |
2019-06-24 |
Andrew Reynolds | Stratify unfolding of regular expressions based on... |
tree | commitdiff |
2019-06-24 |
Andres Noetzli | Fix memory leak in unit test (#3068) |
tree | commitdiff |
2019-06-21 |
Andres Noetzli | Fix and simplify handling of --force-logic (#3062) |
tree | commitdiff |
2019-06-21 |
Andres Noetzli | Use TMPDIR environment variable for temp files (#2849) |
tree | commitdiff |
2019-06-12 |
Andres Noetzli | Refactor parser to define fewer tokens for symbols... |
tree | commitdiff |
2019-06-12 |
Andres Noetzli | Disable dumping regression for non-dumping builds ... |
tree | commitdiff |
2019-06-11 |
Andrew Reynolds | Do not require sygus constructors to be flattened ... |
tree | commitdiff |
2019-06-10 |
Andrew Reynolds | Optimization for negative concatenation membership... |
tree | commitdiff |
2019-06-05 |
Andres Noetzli | Prevent letification from shadowing variables (#3042) |
tree | commitdiff |
2019-06-05 |
Alex Ozdemir | DRAT-Optimization (#2971) |
tree | commitdiff |
2019-06-04 |
Andres Noetzli | Enable proof checking for QF_LRA benchmarks (#2928) |
tree | commitdiff |
2019-06-04 |
Andres Noetzli | Add check that result matches benchmark status (#3028) |
tree | commitdiff |
2019-06-01 |
Andrew Reynolds | Fix rewriter for regular expression consume (#3029) |
tree | commitdiff |
2019-05-30 |
Andres Noetzli | Quote symbol when printing empty symbol name (#3025) |
tree | commitdiff |
2019-05-27 |
Andres Noetzli | Avoid substituting Boolean term variables (#3022) |
tree | commitdiff |
2019-05-21 |
Martin | Update to symfpu 0.0.7, fixes RTI 3/5 issue (#3007) |
tree | commitdiff |
2019-05-18 |
Aina Niemetz | FP: Fix regression test and enable SymFPU on Travis... |
tree | commitdiff |
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 |
next |