summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2019-06-11 Fix spurious assertion in get-value (#3052)Andrew Reynolds
2019-06-10Optimization for negative concatenation membership. (#3048)Andrew Reynolds
2019-06-10Optimization for strings normalize disequalities (#3047)Andrew Reynolds
2019-06-05Prevent letification from shadowing variables (#3042)Andres Noetzli
2019-06-05DRAT-Optimization (#2971)Alex Ozdemir
2019-06-05Add support for SWIG 4 (#3041)Andres Noetzli
2019-06-04Enable proof checking for QF_LRA benchmarks (#2928)Andres Noetzli
2019-06-04Add check that result matches benchmark status (#3028)Andres Noetzli
2019-06-02Enable SymFPU assertions in production (#3036)Andres Noetzli
2019-06-02Add check for limit of number of node children (#3035)Andres Noetzli
2019-06-01 Require that FMF model basis terms are variables (#3031)Andrew Reynolds
2019-06-01Fix rewriter for regular expression consume (#3029)Andrew Reynolds
2019-05-30Quote symbol when printing empty symbol name (#3025)Andres Noetzli
2019-05-27Avoid substituting Boolean term variables (#3022)Andres Noetzli
2019-05-17Support for incremental bit-blasting with CaDiCaL (#3006)Andres Noetzli
2019-05-17Fix BV ITE rewrite (#3004)Andres Noetzli
2019-05-15Fix iterators in Java API (#3000)Andres Noetzli
2019-05-15cmake: Install JAR and JNI files for Java bindings. (#3002)Mathias Preiner
2019-05-15 BV: Do not enable abstraction when eager bit-blasting by default. (#3001)Aina Niemetz
2019-05-15Fix model of Boolean vars with eager bit-blaster (#2998)Andres Noetzli
2019-05-15Fix printing of bvurem (#2963)Andrew Reynolds
2019-05-10Disable relational triggers (#2994)Andrew Reynolds
2019-05-09Fixes for relational triggers (#2967)Andrew Reynolds
2019-05-06Add support for re.all (#2980)Andres Noetzli
2019-05-02Simple optimizations to core strings theory. (#2988)Andrew Reynolds
2019-05-01 Use total versions of div/mod in re-elim-agg (#2986)Andrew Reynolds
2019-04-30Fix concat-find regexp elimination (#2983)Andres Noetzli
2019-04-30Remove stoi solve rewrite (#2985)Andrew Reynolds
2019-04-29Eliminate APPLY kind (#2976)Andrew Reynolds
2019-04-29Optimization for evaluation with unfolding (#2979)Andrew Reynolds
2019-04-25New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)Aina Niemetz
2019-04-24Fix compiler warning. (#2975)Aina Niemetz
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
2019-04-23[BV] An option for SAT proof optimization (#2915)Alex Ozdemir
2019-04-23Refactor normal forms in strings (#2897)Andrew Reynolds
2019-04-18Fail fast strategy for propagating instances (#2939)Andrew Reynolds
2019-04-18 Less aggressive caching in equality engine when proofs are enabled (#2964)Andrew Reynolds
2019-04-17Cache explanations in the equality engine (#2937)Andrew Reynolds
2019-04-17More use of isClosure (#2959)Andrew Reynolds
2019-04-17Fix extended function decomposition (#2960)Andrew Reynolds
2019-04-16Add interface for term enumeration (#2956)Andrew Reynolds
2019-04-16Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)Andres Noetzli
2019-04-16Stratify enumerative instantiation (#2954)Andrew Reynolds
2019-04-16Minor simplifications to theory quantifiers (#2953)Andrew Reynolds
2019-04-15Check for rt library in configuration -- support for glibc<2.17 (#2854)makaimann
2019-04-11 Eliminate Boolean ITE within terms, fixes 2947 (#2949)Andrew Reynolds
2019-04-08fix copyright year in configuration file (#2942)Haniel Barbosa
2019-04-05Fix another corner case of datatypes+PBE (#2938)Andrew Reynolds
2019-04-05fix fp issue (#2940)Haniel Barbosa
2019-04-05SatClauseSetHashFunction (#2916)Alex Ozdemir
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback