summaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2021-09-02Fixes from mergeajreynol
2021-08-31Use more robust conversion for arithmetic trichotomyajreynol
2021-08-31Support arith trichotomy in LFSCajreynol
2021-08-31Add support concat unify in LFSCajreynol
2021-08-04Add test_proof_newajreynol
2021-08-04Improved and updated testing scriptsajreynol
2021-07-30Add proper conversion for bitblast term, proper printing for bitOf, update ↵ajreynol
LFSC version
2021-07-30Simplify smt2 printer, fix order issue in strings eager reduction, update ↵ajreynol
LFSC version
2021-06-21Merge branch 'master' into proof-newHaniel Barbosa
2021-06-16Archive SMT-COMP 2021 run scripts (#6748)Andres Noetzli
This commit copies the run-script-smtcomp-current* scripts to run-script-smtcomp2021* to archive them.
2021-06-14Final update to SMT-COMP 2021 options (#6739)Andres Noetzli
This commit: - Disables `--tear-down-incremental=X` for the competition since it currently does not work correctly on master and a fixed version did not show significant benefits. - Changes the occurrences of `--nl-ext` to `--nl-ext=full` because it is now a mode option. - Removes the use of `--bv-assert-input` because the option currently has some issues in incremental mode (#6738) - Removes the use of `--bitblast=eager` for the model validation track because it produces invalid models (#6741)
2021-06-11Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-06-10smtcomp: Change some BV configs for SQ and INC track. (#6721)Mathias Preiner
2021-06-09Update options for SMT-COMP (#6704)Andres Noetzli
This commit removes obsolete options for BV and strings logics, and updates QF_NIA to spend more time on our best configuration. Co-authored-by: Gereon Kremer nafur42@gmail.com Co-authored-by: Mathias Preiner mathias.preiner@gmail.com
2021-06-04Format, update LFSC commitajreynol
2021-06-01Update LFSC commitajreynol
2021-06-01Merge branch 'master' of https://github.com/cvc5/cvc5 into proof-newajreynol
2021-05-30Remove invalid options from run scripts (#6645)Andres Noetzli
This commit removes some of the options in the run scripts that are not supported anymore: `--bv-div-zero-const` and `--rewrite-divk`. Both of those options are effectively enabled by default in cvc5.
2021-05-27Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-05-27Enable new justification heuristic by default (#6613)Andrew Reynolds
This enables the new implementation of justification heuristic by default. Fixes #5454, fixes #5785. Fixes wishues 114, 115, 149, 160.
2021-05-25Generalize string reductions to sequences, simplify.ajreynol
2021-05-25Use side condition for and elim, simplify policy for assigning assumption ↵ajreynol
ids, fixes
2021-05-25Improved support for datatype testers and updaters in LFSC outputajreynol
2021-05-25Drop type annotations on ITE in LFSCajreynol
2021-05-25Minor fix for quantifier skolemsajreynol
2021-05-25Fix related to original form of witness skolems in LFSCajreynol
2021-05-24Fix LFSC for nested skolems in purificationajreynol
2021-05-21Refactor regular expression unfolding, formalize skolems, working LFSC ↵ajreynol
translation of RE_UNFOLD_POS
2021-05-21Support shared selectors in LFSC proof outputajreynol
2021-05-19Use skolem function for shared selectorsajreynol
2021-05-19Update LFSC commitajreynol
2021-05-19Minor, update LFSC signatureajreynol
2021-05-17Update LFSC signatureajreynol
2021-05-17Minor fixes for LFSC conversionajreynol
2021-05-17Constant sequences, more fixes, exclude bad regressionsajreynol
2021-05-17LFSC commitajreynol
2021-05-17Simplify indexof reduction, update LFSC sig commitajreynol
2021-05-14More additions for LFSC, ho congruence, missing operatorsajreynol
2021-05-14Increment lfsc commitajreynol
2021-05-13Increment LFSC commitajreynol
2021-05-13Fixes to LFSC printerajreynol
2021-05-13Fix congruence over quantifiers in LFSCajreynol
2021-05-13Properly print sorts using user names in LFSC, fix pow.ajreynol
2021-05-12Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-05-12Preliminary draft of changes for SMT comp 2021 (#6522)Andrew Reynolds
Covers improvements to quantifiers.
2021-05-05Merge branch 'master' of https://github.com/CVC4/CVC4 into proof-newajreynol
2021-04-28Allow Int/Real subtyping in LFSC proofsajreynol
2021-04-27LFSC commitajreynol
2021-04-27Minor fixes, additions to LFSCajreynol
2021-04-27Work on indexed operators in LFSCajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback