summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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
2019-03-18BitVector: Allow base 10 in constructor. (#2870)Aina Niemetz
2019-03-16Limit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL (#2868)Andres Noetzli
2019-03-16Enable CryptoMiniSat-backed BV proofs (#2847)Alex Ozdemir
2019-03-15New beta-reduction for HOL solving (#2869)Haniel Barbosa
2019-03-15Adding capture avoiding substitution (#2867)Haniel Barbosa
2019-03-14Fix non-variable function head elimination in UF. (#2864)Andrew Reynolds
2019-03-14Fix function term set for theory strings compute care graph. (#2862)Andrew Reynolds
2019-03-14Use zero slope tangent planes for transcendental functions (#2803)Andrew Reynolds
2019-03-14Properly handle lambdas in relevant domain (#2853)Andrew Reynolds
2019-03-14 Add getFreeVariables method to node algorithm (#2852)Andrew Reynolds
2019-03-14Implement proper semantics for TPTP predicate is_rat. (#2861)Andrew Reynolds
2019-03-14 Fix substitution step in ho matching (#2825)Andrew Reynolds
2019-03-14Generalize sygus-rr-verify for fast enumerator (#2829)Andrew Reynolds
2019-03-14check for null assumption in query and replace with false (#2858)makaimann
2019-03-13Add statistics for proof gen./checking time, size (#2850)Andres Noetzli
2019-03-13Remove spurious data member. (#2857)Andrew Reynolds
2019-03-12Fix public headers for make install. (#2856)Mathias Preiner
2019-03-12Add option --sygus-rr-synth-rec for considering all grammar types recursively...Andrew Reynolds
2019-03-12 Move tuple/record update elimination from ppRewrite to expandDefinition (#2839)Andrew Reynolds
2019-02-28ErProof class with LFSC output (#2812)Alex Ozdemir
2019-02-27Use string stream for proofs instead of tmp files (#2841)Andres Noetzli
2019-02-13New C++ API: Remove redundant declareFun function. (#2837)Aina Niemetz
2019-02-13Rewrite simple regexp pattern to str.contains (#2827)Andres Noetzli
2019-02-12New C++ API: Remove redundant mkTerm function. (#2836)Aina Niemetz
2019-02-12Delete temporary proof files when aborting CVC4 (#2834)Andres Noetzli
2019-02-11New C++ API: Unit tests for declare* functions. (#2831)Aina Niemetz
2019-02-05Make stripConstantEndpoints() less aggressive (#2830)Andres Noetzli
2019-02-03Add rewrite for contains + const strings replace (#2828)Andres Noetzli
2019-02-02Fix corner case in stripConstantEndpoints (#2824)Andres Noetzli
2019-01-29New C++ API: Fix checks for mkTerm. (#2820)Aina Niemetz
2019-01-29Strings: Remove redundant replace rewrite (#2822)Andres Noetzli
2019-01-23Avoid using ProofManager in non-proof CMS build (#2814)Andres Noetzli
2019-01-22Strings: Strengthen multiset reasoning (#2817)Andres Noetzli
2019-01-22 Fix tuple and record CVC printing (#2818)Andrew Reynolds
2019-01-22 Fix parsing of overloaded parametric datatype selectors (#2819)Andrew Reynolds
2019-01-19Fix missing-override warning (#2811)Andres Noetzli
2019-01-18Extract DIMACS Printing (#2800)Alex Ozdemir
2019-01-18Strings: Introduce checkEntailContains() (#2809)Andres Noetzli
2019-01-18 Fix ABC build (#2808)Andres Noetzli
2019-01-16Add option to print BV constants in binary (#2805)Andres Noetzli
2019-01-15Fix constant contains ITOS rewrite (#2799)Andrew Reynolds
2019-01-15Strings: Add option to change loop process mode (#2794)Andres Noetzli
2019-01-15 Fix unsound double abs rewrite rule for FP (#2792)Andrew Reynolds
2019-01-14 Only check disequal terms with sygus-rr-verify (#2793)Andrew Reynolds
2019-01-14ClausalBitvectorProof (#2786)Alex Ozdemir
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback