Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-05-31 | More simplify | ajreynol | |
2018-05-31 | Simplify beta reduction. | ajreynol | |
2018-05-31 | Fix | ajreynol | |
2018-05-31 | Deterministic vs non-deterministic PBE strategies. | ajreynol | |
2018-05-31 | Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2 | ajreynol | |
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 | Options | ajreynol | |
2018-05-30 | Repair condition to separate. | ajreynol | |
2018-05-30 | Fix for issue #2002 (#2012) | Andres Noetzli | |
2018-05-30 | More | ajreynol | |
2018-05-30 | Fixes for quantifiers + incremental (#2009) | Andrew Reynolds | |
2018-05-30 | Make declare-fun compatible with invariant synthesis format. | ajreynol | |
2018-05-30 | Support (higher-order) define-fun. | ajreynol | |
2018-05-30 | Normalize negated bit-vector terms over equalities. (#2017) | Mathias Preiner | |
2018-05-30 | Improve trace. | ajreynol | |
2018-05-30 | Doc | ajreynol | |
2018-05-30 | Improve org. | ajreynol | |
2018-05-30 | Minor, add option. | ajreynol | |
2018-05-29 | Fixes | ajreynol | |
2018-05-29 | Always produce models. | ajreynol | |
2018-05-29 | Merge branch 'sygusComp2018-2' into sym-break-anyconst | Haniel Barbosa | |
2018-05-29 | Merge opt3. | ajreynol | |
2018-05-29 | Merge branch 'sygusComp2018-2' into sym-break-anyconst | Haniel Barbosa | |
2018-05-29 | Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2 | ajreynol | |
2018-05-29 | Merge branch 'master' into sym-break-anyconst | Haniel Barbosa | |
2018-05-29 | deleting comment | Haniel Barbosa | |
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 | fixes | Haniel Barbosa | |
2018-05-29 | revert | Haniel Barbosa | |
2018-05-29 | draft | Haniel Babosa | |
2018-05-29 | Initialize with extRewBv branch. | ajreynol | |
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-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 | 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-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. |