summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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
2019-04-04Ignoring FP benchmarks with "unsafe" sizes unless option (#2931)Haniel Barbosa
2019-04-03Update copyright headers.Aina Niemetz
2019-04-03Fix combination of datatypes + strings in PBE (#2930)Andrew Reynolds
2019-04-01FP: Fix wrong model due to partial assignment (#2910)Andres Noetzli
2019-04-01Fix RewriteITEBv to ensure rewrite to fixpoint (#2878)Andres Noetzli
2019-04-01Modify strategy in sets+cardinality (#2909)Andrew Reynolds
2019-03-29Apply empty splits more aggressively in sets+cardinality (#2907)Andrew Reynolds
2019-03-28Fix freeing nodes with maxed refcounts (#2903)Andres Noetzli
2019-03-28Fix issues in cvc parser (#2901)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
2019-03-26Fix warnings about wrong line numbers (#2899)Andres Noetzli
2019-03-26Fix a few warnings (#2898)Andrew Reynolds
2019-03-24 Split regular expression solver (#2891)Andrew Reynolds
2019-03-24New C++ API: Fix include. (#2896)Aina Niemetz
2019-03-23BV: Fix typerules for rotate operators. (#2895)Aina Niemetz
2019-03-23Fix memory leak when using subsolvers (#2893)Andres Noetzli
2019-03-23Strip non-matching beginning from indexof operator (#2885)Andres Noetzli
2019-03-22Revisit strings extended function decomposition (#2892)Andrew Reynolds
2019-03-22Fix instantiation stat for fmf (#2889)Andrew Reynolds
2019-03-22More fixes for PBE with datatypes (#2882)Andrew Reynolds
2019-03-22fix help information on TPTP parsing (#2884)Haniel Barbosa
2019-03-22Fix stripConstantEndpoints in strings rewriter (#2883)Andres Noetzli
2019-03-22Use empty vector instead of false in query with null Expr assumption (#2876)makaimann
2019-03-21 Fix bad comparison in RE solver's addMembership (#2880)Andrew Reynolds
2019-03-21Rewrite selectors correctly applied to constructors (#2875)Andrew Reynolds
2019-03-19Sygus abduction feature (#2744)Andrew Reynolds
2019-03-19Make declare-datatype(s) a standard, non-extended command in the Smt2 parser....Andrew Reynolds
2019-03-19Fix fairness issue with fast sygus enumerator (#2873)Andrew Reynolds
2019-03-18New C++: Remove redundant mkBoundVar function.Aina Niemetz
2019-03-18New C++: Remove redundant mkVar function.Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback