summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-06-04Merge branch 'master' into run_new_logicsrun_new_logicsAndrew Reynolds
2018-06-04Enable cegqi (with model values) for floating point by default (#2023)Andrew Reynolds
2018-06-04Regressions: 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-02Fix corner case of mixed int/real cegqi. (#2046)Andrew Reynolds
2018-06-02Fix 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-02Fix preinitialization pass for finite model finding (#2047)Andrew Reynolds
2018-06-01Fix quantified bv variable elimination (#2039)Andrew Reynolds
2018-06-01Fix quantifiers conflict lemma handling (#2043)Andrew Reynolds
2018-06-01Apply 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-31Reduce before preregister. (#2025)Andrew Reynolds
2018-05-30Fix bv-abstraction check for AND with non bit-vector atoms. (#2024)Mathias Preiner
2018-05-30Ignore license key in set-info command. (#2021)Aina Niemetz
2018-05-30Incorporate Andy's feedbackAndres Noetzli
2018-05-30[SMT-COMP] Add new logics to run-scriptsAndres Noetzli
Fixes #2014. Note: The new logics just use the defaults.
2018-05-30Fix for issue #2002 (#2012)Andres Noetzli
2018-05-30Fixes 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-30Normalize negated bit-vector terms over equalities. (#2017)Mathias Preiner
2018-05-30Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV. (#2018)Mathias Preiner
2018-05-30Draft 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-29Disable minisat elimination when nonlinear is enabled (#2006)Andrew Reynolds
2018-05-29Track input language in a single place (#2003)Andres Noetzli
2018-05-28Builtin evaluation functions for sygus (#1991)Andrew Reynolds
2018-05-27Fix cegqi assertions for quantified non-linear cases. (#1999)Andrew Reynolds
2018-05-27Fix no-cbqi-innermost option name in run script (#1994)Andres Noetzli
2018-05-26Update SymFPU. (#1992)Mathias Preiner
2018-05-25Reenable repair const (#1983)Andrew Reynolds
2018-05-25MiniSat: 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-25Add QF_BV configuration for SMTCOMP'18. (#1981)Mathias Preiner
2018-05-25Fix various nl assertions. (#1980)Andrew Reynolds
2018-05-24Fix (#1979)Andrew Reynolds
2018-05-24Improve simple constant symmetry breaking for sygus (#1977)Andrew Reynolds
2018-05-24Fix compiler warnings (#1959)Andres Noetzli
2018-05-24Fix (#1975)Andrew Reynolds
2018-05-24Fixes for non-linear check model (#1974)Andrew Reynolds
2018-05-24Fix nl regression for unsat cores. (#1973)Andrew Reynolds
2018-05-23Remove spurious assertion in nonlinear extension (#1972)Andrew Reynolds
2018-05-23Towards better symbolic enumeration in SyGuS (#1971)Haniel Barbosa
2018-05-23Add notions of evaluated kinds in TheoryModel (#1947)Andrew Reynolds
2018-05-23Remove ProofProxy (#1965)Andres Noetzli
2018-05-23Generalize check-model in NonLinearExtension for quadratic equations (#1892)Andrew Reynolds
2018-05-22Set 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-22Repair constants using symbolic constructors (#1960)Andrew Reynolds
2018-05-22Parse error for sygus grammar term with multiple let bodies (#1961)Andrew Reynolds
2018-05-22Disable 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-22Make sygus infer find function definitions (#1951)Andrew Reynolds
2018-05-21Infrastructure for strings strategies (#1883)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback