cvc5.git
2018-07-06 Aina NiemetzNew C++ API: Implementation of Solver class: Term handl...
2018-07-06 Aina NiemetzNew C++ API: Implementation of Solver class: Sort handl...
2018-07-06 Andres NoetzliAdd option for timeout for rewrite candidate check...
2018-07-06 Andrew ReynoldssygusComp2018: simplify beta reduction in uf rewriter...
2018-07-05 Andrew Reynolds Make string length lemmas more robust to rewriting...
2018-07-05 Andrew ReynoldsMinor changes to sygus-rr utilities to support floating...
2018-07-05 Andres NoetzlisygusComp2018: Improve string rewriter (#2141)
2018-07-04 Andrew ReynoldsMore cleanup in strings (#2138)
2018-07-04 Aina NiemetzNew C++ API: Implementation of datatype declaration...
2018-07-04 Andrew ReynoldsReorganize candidate rewrite rule filtering (#2116)
2018-07-04 Andres NoetzliRemove unused CDVector (#2139)
2018-07-04 Aina NiemetzNew C++ API: Implementation of OpTerm. (#2132)
2018-07-04 Andrew ReynoldsFix fmf-fun for non-equality function definitions ...
2018-07-03 Aina NiemetzNew C++ API: Implementation of Term. (#2131)
2018-07-03 Aina NiemetzNew C++ API: Implementation of Kind maps. (#2130)
2018-07-03 Aina NiemetzFix datatypes example: nil constructor was missing...
2018-07-03 Andrew ReynoldssygusComp2018: update sygus-related options setting...
2018-07-03 Andrew ReynoldsRemove miscellaneous dead and unused code from quantifi...
2018-07-03 Andres NoetzliAdd regression test for issue #1986 (#2114)
2018-07-02 Aina NiemetzRefactor ApplySubsts preprocessing pass. (#2120)
2018-07-02 Aina NiemetzNew C++ API: Implementation of Sort. (#2122)
2018-07-02 Andrew ReynoldsRemove some dead code from theory strings (#2125)
2018-07-02 Caleb DonovickAdd missing include (#2127)
2018-07-02 Andrew ReynoldsModify cegqi heuristic for finite datatypes (#2126)
2018-07-02 Andrew ReynoldsImprove error message. (#2124)
2018-06-29 Andrew ReynoldsUse evaluator in sygus sampler. (#2117)
2018-06-29 Aina NiemetzNew C++ API: Implementation of Result. (#2112)
2018-06-28 Andrew ReynoldsRemove comment about model value hack (#2118)
2018-06-28 Andrew Reynolds sygusComp2018: optimization for invariance test (...
2018-06-28 Andres NoetzliFix stale reference in MiniSat when generating UC ...
2018-06-28 Andrew ReynoldsDo not rename uninterpreted constants (#2098)
2018-06-28 Andrew ReynoldsSplit and document ceg theory instantiators (#2094)
2018-06-27 Aina NiemetzHeader for new C++ API. (#1697)
2018-06-27 Andrew ReynoldsSynthesize candidate-rewrites from standard inputs...
2018-06-26 Andrew ReynoldssygusComp2018: add scripts. (#2103)
2018-06-26 Andres NoetzlisygusComp2018: Add evaluator (#2090)
2018-06-26 Andrew ReynoldsAdd casc j9 tfn script (#2100)
2018-06-26 Andrew Reynolds Disable uf symmetry breaker in incremental mode (...
2018-06-26 Andrew ReynoldsFix assertion for relational triggers (#2096)
2018-06-26 Andrew Reynolds Do not dagify printing over binders (#2093)
2018-06-26 Andrew ReynoldsRemove unnecessary code in register quantifier internal...
2018-06-26 Andres NoetzliMinor improvements in SMT2 and CVC printers (#2089)
2018-06-26 Aina NiemetzBump library version to 1.7-prerelease.
2018-06-26 Aina NiemetzCutting release 1.6.
2018-06-25 Aina NiemetzMore updates to NEWS for 1.6.
2018-06-25 Aina NiemetzUpdate AUTHORS, NEWS, README, RELEASE-NOTES and THANKS...
2018-06-25 Aina NiemetzBump library version.
2018-06-25 Aina NiemetzUpdate copyright year in configuration.cpp:copyright().
2018-06-25 Aina NiemetzUpdated copyright headers.
2018-06-25 Aina NiemetzDo not use git blame -C in get-authors (too many false...
2018-06-25 Aina NiemetzFix update-copyright script for files without a header.
2018-06-25 Aina NiemetzAdded Makai and Yoni to get-authors script.
2018-06-25 Andres NoetzliRemove parentheses for prefix ops without args (#2082)
2018-06-21 Andres NoetzliFix warnings and enable -Wnon-virtual-dtor warning...
2018-06-21 Andres NoetzliCheck unsat cores in regressions also without LFSC...
2018-06-21 Aina NiemetzUpdated installation instructions to mention autogen...
2018-06-20 Andres NoetzliResolve CVC4_USE_SYMFPU in headers at config-time ...
2018-06-15 Andrew ReynoldsDisable solving non-linear BV literals by default ...
2018-06-13 Andres NoetzliWorkaround for incremental unsat cores (#1962)
2018-06-13 Andrew ReynoldsFix simple regexp consume (#2066)
2018-06-13 Andres NoetzliDisable unconstrainedSimp pass when proofs enabled...
2018-06-12 Andrew ReynoldsFix strip constant endpoint for ITOS in strings rewrite...
2018-06-11 Andrew ReynoldsFix equality conflicts reported by FP (#2064)
2018-06-10 Andres NoetzliDisable test that fails in competition mode (#2063)
2018-06-09 Andres NoetzliAdd flag to skip regression if feature enabled (#2062)
2018-06-09 Andres NoetzliReset decisions at SAT level after solving (#2059)
2018-06-08 Mathias PreinerDisable BV-abstraction in the competition script. ...
2018-06-07 Andres NoetzliLook for cryptominisat5_simple, not cryptominisat5...
2018-06-07 Aina NiemetzRemove invalid assertion (#1993). (#2057)
2018-06-07 Andrew ReynoldsClear pending inferences during datatypes splitting...
2018-06-05 Andres NoetzliOnly enable transcendentals if logic is N[I]RAT (#2052)
2018-06-04 Andrew ReynoldsMove assertion. (#2051)
2018-06-04 Andres Noetzli[SMT-COMP] Add new logics to run-scripts (#2022)
2018-06-04 Andrew ReynoldsEnable cegqi (with model values) for floating point...
2018-06-04 Andres NoetzliRegressions: Support for requiring CVC4 features (...
2018-06-02 Andrew Reynolds Fix assertion involving unassigned Boolean eqc in...
2018-06-02 Andrew ReynoldsFix corner case of mixed int/real cegqi. (#2046)
2018-06-02 Mathias PreinerFix BV-abstraction check to consider SKOLEM. (#2042)
2018-06-02 Andrew ReynoldsFix preinitialization pass for finite model finding...
2018-06-01 Andrew ReynoldsFix quantified bv variable elimination (#2039)
2018-06-01 Andrew ReynoldsFix quantifiers conflict lemma handling (#2043)
2018-06-01 Andrew ReynoldsApply preprocessing to counterexample lemmas in CEGQI...
2018-06-01 Andrew Reynolds Use monomial sum utility to solve for quantifiers...
2018-06-01 Andrew ReynoldsReduce before preregister. (#2025)
2018-05-31 Mathias PreinerFix bv-abstraction check for AND with non bit-vector...
2018-05-30 Aina NiemetzIgnore license key in set-info command. (#2021)
2018-05-30 Andres NoetzliFix for issue #2002 (#2012)
2018-05-30 Andrew ReynoldsFixes for quantifiers + incremental (#2009)
2018-05-30 Andres Noetzli[SMT-COMP] Print non-(un)sat output to stderr (#2019)
2018-05-30 Mathias PreinerNormalize negated bit-vector terms over equalities...
2018-05-30 Mathias PreinerUse CaDiCaL for eager bit-blasting in QF_NIA and QF_UFB...
2018-05-30 Andrew ReynoldsDraft run script for strings smt comp 2018. (#2016)
2018-05-29 Andres Noetzli Make user's SMT2 version override file version (#2004)
2018-05-29 Andrew ReynoldsDisable minisat elimination when nonlinear is enabled...
2018-05-29 Andres NoetzliTrack input language in a single place (#2003)
2018-05-28 Andrew ReynoldsBuiltin evaluation functions for sygus (#1991)
2018-05-27 Andrew ReynoldsFix cegqi assertions for quantified non-linear cases...
2018-05-27 Andres NoetzliFix no-cbqi-innermost option name in run script (#1994)
2018-05-26 Mathias PreinerUpdate SymFPU. (#1992)
2018-05-25 Andrew ReynoldsReenable repair const (#1983)
next