cvc5.git
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)
2018-05-25 Andres NoetzliMiniSat: Be more careful about running proof code ...
2018-05-25 Mathias PreinerAdd QF_BV configuration for SMTCOMP'18. (#1981)
2018-05-25 Andrew ReynoldsFix various nl assertions. (#1980)
2018-05-25 Andrew ReynoldsFix (#1979)
2018-05-24 Andrew ReynoldsImprove simple constant symmetry breaking for sygus...
2018-05-24 Andres NoetzliFix compiler warnings (#1959)
2018-05-24 Andrew ReynoldsFix (#1975)
2018-05-24 Andrew ReynoldsFixes for non-linear check model (#1974)
2018-05-24 Andrew ReynoldsFix nl regression for unsat cores. (#1973)
2018-05-24 Andrew ReynoldsRemove spurious assertion in nonlinear extension (...
2018-05-23 Haniel BarbosaTowards better symbolic enumeration in SyGuS (#1971)
2018-05-23 Andrew ReynoldsAdd notions of evaluated kinds in TheoryModel (#1947)
2018-05-23 Andres NoetzliRemove ProofProxy (#1965)
2018-05-23 Andrew ReynoldsGeneralize check-model in NonLinearExtension for quadra...
2018-05-23 Andres NoetzliSet same options for proofs as for unsat cores (#1957)
2018-05-23 Andrew ReynoldsRepair constants using symbolic constructors (#1960)
2018-05-22 Andrew ReynoldsParse error for sygus grammar term with multiple let...
2018-05-22 Andres NoetzliDisable symmetry breaker for unsat cores (#1958)
2018-05-22 Andrew ReynoldsMake sygus infer find function definitions (#1951)
2018-05-22 Andrew ReynoldsInfrastructure for strings strategies (#1883)
2018-05-22 Mathias PreinerAdd SymFPU licensing information. (#1952)
2018-05-21 Andrew ReynoldsImprovements in parsing and printing related to mixed...
2018-05-21 Andrew ReynoldsInfrastructure to mark unused sygus strategies (#1950)
2018-05-21 makaimannHandle IMPLIES in bool-to-bv and test it in regress0...
2018-05-21 Andrew ReynoldsRefactor sygus eval unfold (#1946)
2018-05-21 Andres NoetzliRemove Eclipse project files (#1928)
2018-05-21 Andres NoetzliFix compiler warning in hashsmt example (#1927)
2018-05-21 Haniel BarbosaAssign weight 1 for Boolean variables in SyGuS default...
2018-05-21 Caleb DonovickFix file extension (#1919)
2018-05-19 Haniel Barbosachanging default (#1944)
2018-05-18 Andrew ReynoldsCache isInterpretedFinite (#1943)
2018-05-18 Andrew ReynoldsCegis unif defaults to cegis when no unif (#1942)
2018-05-18 Andrew ReynoldsUnified fairness scheme for cegis unif (#1941)
2018-05-17 Andrew ReynoldsCatch type errors in sygus grammars for lambda (define...
2018-05-17 Andrew ReynoldsFix debugPrint and add regress. (#1934)
2018-05-17 Haniel BarbosaOption to force return values of Bool functions to...
2018-05-17 Andrew ReynoldsCegis-specific infrastructure (#1933)
2018-05-17 Andrew ReynoldsInternal propagation for refinement lemmas (#1932)
2018-05-16 Andrew ReynoldsImprove the separation resolution scheme in cegis unif...
2018-05-16 yoni206Refactor static learning preprocessing pass (#1857)
2018-05-15 Andrew ReynoldsRefactoring get enumerator values in construct candidat...
2018-05-15 Haniel Barbosaadding regressions (#1925)
2018-05-15 Haniel BarbosaBuilding and refining solutions with dynamic condition...
2018-05-15 Andrew ReynoldsFix free variables in cbqi preregister inst. (#1921)
2018-05-15 Andrew ReynoldsFix annotations in regress2. (#1917)
2018-05-15 Andrew ReynoldsMinor improvements to --nl-ext-purify (#1896)
2018-05-15 Andrew Reynolds Incorporating dynamic condition enumeration into cegis...
next