Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-06-08 | Disable BV-abstraction in the competition script. (#2061) | Mathias Preiner | |
2018-06-07 | Look for cryptominisat5_simple, not cryptominisat5 (#2058) | Andres Noetzli | |
If the boost program_options library is missing, CryptoMiniSat5 only builds a cryptominisat5_simple binary and omits the cryptominisat5, which has more command-line options. We do not use the binary anyway, so this commit changes the cryptominisat.m4 script to look for the cryptominisat5_simple binary, which is always generated. | |||
2018-06-07 | Remove invalid assertion (#1993). (#2057) | Aina Niemetz | |
2018-06-06 | Clear pending inferences during datatypes splitting (#2056) | Andrew Reynolds | |
2018-06-04 | Only enable transcendentals if logic is N[I]RAT (#2052) | Andres Noetzli | |
2018-06-04 | Move assertion. (#2051) | Andrew Reynolds | |
2018-06-04 | [SMT-COMP] Add new logics to run-scripts (#2022) | Andres Noetzli | |
2018-06-04 | Enable cegqi (with model values) for floating point by default (#2023) | Andrew Reynolds | |
2018-06-04 | Regressions: Support for requiring CVC4 features (#2044) | Andres Noetzli | |
This commit adds supprt for the `REQUIRES` directive in our regression benchmarks. This directive can be used to enable certain benchmarks only if CVC4 has been configured with certain features enabled. | |||
2018-06-02 | Fix assertion involving unassigned Boolean eqc in model (#2050) | Andrew Reynolds | |
2018-06-02 | Fix corner case of mixed int/real cegqi. (#2046) | Andrew Reynolds | |
2018-06-02 | Fix BV-abstraction check to consider SKOLEM. (#2042) | Mathias Preiner | |
Further, fix a bug in the AIG bitblaster that was also uncovered with the minimized file. | |||
2018-06-02 | Fix preinitialization pass for finite model finding (#2047) | Andrew Reynolds | |
2018-06-01 | Fix quantified bv variable elimination (#2039) | Andrew Reynolds | |
2018-06-01 | Fix quantifiers conflict lemma handling (#2043) | Andrew Reynolds | |
2018-06-01 | Apply preprocessing to counterexample lemmas in CEGQI (#2027) | Andrew Reynolds | |
2018-06-01 | Use monomial sum utility to solve for quantifiers macros (#2038) | Andrew Reynolds | |
2018-05-31 | Reduce before preregister. (#2025) | Andrew Reynolds | |
2018-05-30 | Fix bv-abstraction check for AND with non bit-vector atoms. (#2024) | Mathias Preiner | |
2018-05-30 | Ignore license key in set-info command. (#2021) | Aina Niemetz | |
2018-05-30 | Fix for issue #2002 (#2012) | Andres Noetzli | |
2018-05-30 | Fixes for quantifiers + incremental (#2009) | Andrew Reynolds | |
2018-05-30 | [SMT-COMP] Print non-(un)sat output to stderr (#2019) | Andres Noetzli | |
In the SMT-COMP runscript, we are currently discarding output on stdout that is not "sat" or "unsat" when using `trywith` (this is not the case with `finishwith`). Due to this, our tests might miss cases where CVC4 fails and prints an error on stdout when using `trywith`. This commit changes the script to print output other than "sat" or "unsat" to stderr. | |||
2018-05-30 | Normalize negated bit-vector terms over equalities. (#2017) | Mathias Preiner | |
2018-05-30 | Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV. (#2018) | Mathias Preiner | |
2018-05-30 | Draft run script for strings smt comp 2018. (#2016) | Andrew Reynolds | |
2018-05-29 | Make user's SMT2 version override file version (#2004) | Andres Noetzli | |
2018-05-29 | Disable minisat elimination when nonlinear is enabled (#2006) | Andrew Reynolds | |
2018-05-29 | Track input language in a single place (#2003) | Andres Noetzli | |
2018-05-28 | Builtin evaluation functions for sygus (#1991) | Andrew Reynolds | |
2018-05-27 | Fix cegqi assertions for quantified non-linear cases. (#1999) | Andrew Reynolds | |
2018-05-27 | Fix no-cbqi-innermost option name in run script (#1994) | Andres Noetzli | |
2018-05-26 | Update SymFPU. (#1992) | Mathias Preiner | |
2018-05-25 | Reenable repair const (#1983) | Andrew Reynolds | |
2018-05-25 | MiniSat: Be more careful about running proof code (#1982) | Andres Noetzli | |
In `addClause_()`, we were checking the condition `ca[confl].size() == 1` regardless if proofs were enabled or not, even though both branches of the if statement only do something when proofs are enabled. This lead to issue #1978 occurring even when not generating proofs. Note: This commit is *not* a fix for #1978 but it makes sure that the issue does not occur when not generating proofs/unsat cores. | |||
2018-05-25 | Add QF_BV configuration for SMTCOMP'18. (#1981) | Mathias Preiner | |
2018-05-25 | Fix various nl assertions. (#1980) | Andrew Reynolds | |
2018-05-24 | Fix (#1979) | Andrew Reynolds | |
2018-05-24 | Improve simple constant symmetry breaking for sygus (#1977) | Andrew Reynolds | |
2018-05-24 | Fix compiler warnings (#1959) | Andres Noetzli | |
2018-05-24 | Fix (#1975) | Andrew Reynolds | |
2018-05-24 | Fixes for non-linear check model (#1974) | Andrew Reynolds | |
2018-05-24 | Fix nl regression for unsat cores. (#1973) | Andrew Reynolds | |
2018-05-23 | Remove spurious assertion in nonlinear extension (#1972) | Andrew Reynolds | |
2018-05-23 | Towards better symbolic enumeration in SyGuS (#1971) | Haniel Barbosa | |
2018-05-23 | Add notions of evaluated kinds in TheoryModel (#1947) | Andrew Reynolds | |
2018-05-23 | Remove ProofProxy (#1965) | Andres Noetzli | |
2018-05-23 | Generalize check-model in NonLinearExtension for quadratic equations (#1892) | Andrew Reynolds | |
2018-05-22 | Set same options for proofs as for unsat cores (#1957) | Andres Noetzli | |
In SmtEngine::setDefaults() we were setting options such as --simplifciation=none for unsat cores but not proofs. Producing unsat cores relies on the same infrastructure as proofs and should be a subset of the same work in most cases. Thus, this commit changes SmtEngine::setDefaults() to set the same options for proofs as we previously only did for unsat cores. Additionally, it changes the function to only set the simplificationMode to SIMPLIFICATION_MODE_BATCH if proofs and unsat cores are not enabled. Fixes issue #1953. | |||
2018-05-22 | Repair constants using symbolic constructors (#1960) | Andrew Reynolds | |