summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2018-05-31More simplifyajreynol
2018-05-31Simplify beta reduction.ajreynol
2018-05-31Fixajreynol
2018-05-31Deterministic vs non-deterministic PBE strategies.ajreynol
2018-05-31Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2ajreynol
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-30Optionsajreynol
2018-05-30Repair condition to separate.ajreynol
2018-05-30Fix for issue #2002 (#2012)Andres Noetzli
2018-05-30Moreajreynol
2018-05-30Fixes for quantifiers + incremental (#2009)Andrew Reynolds
2018-05-30Make declare-fun compatible with invariant synthesis format.ajreynol
2018-05-30Support (higher-order) define-fun.ajreynol
2018-05-30Normalize negated bit-vector terms over equalities. (#2017)Mathias Preiner
2018-05-30Improve trace.ajreynol
2018-05-30Docajreynol
2018-05-30Improve org.ajreynol
2018-05-30Minor, add option.ajreynol
2018-05-29Fixesajreynol
2018-05-29Always produce models.ajreynol
2018-05-29Merge branch 'sygusComp2018-2' into sym-break-anyconstHaniel Barbosa
2018-05-29Merge opt3.ajreynol
2018-05-29Merge branch 'sygusComp2018-2' into sym-break-anyconstHaniel Barbosa
2018-05-29Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2ajreynol
2018-05-29Merge branch 'master' into sym-break-anyconstHaniel Barbosa
2018-05-29deleting commentHaniel Barbosa
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-29fixesHaniel Barbosa
2018-05-29revertHaniel Barbosa
2018-05-29draftHaniel Babosa
2018-05-29Initialize with extRewBv branch.ajreynol
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-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-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-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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback