Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-06-04 | Merge branch 'master' into run_new_logicsrun_new_logics | Andrew Reynolds | |
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 | Incorporate Andy's feedback | Andres Noetzli | |
2018-05-30 | [SMT-COMP] Add new logics to run-scripts | Andres Noetzli | |
Fixes #2014. Note: The new logics just use the defaults. | |||
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 | |
2018-05-22 | Parse error for sygus grammar term with multiple let bodies (#1961) | Andrew Reynolds | |
2018-05-22 | Disable symmetry breaker for unsat cores (#1958) | Andres Noetzli | |
Currently, --check-unsat-cores fails for one of our regressions. It turns out that the issue is due to preprocessing done by the symmetry breaker. The symmetry breaker does not add dependencies and thus the generated unsat core is incomplete/wrong. This commit disables the symmetry breaker when we are generating unsat cores (it was previously only disabled when generating proofs). Fixes issue #1953. | |||
2018-05-22 | Make sygus infer find function definitions (#1951) | Andrew Reynolds | |
2018-05-21 | Infrastructure for strings strategies (#1883) | Andrew Reynolds | |