projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Refactoring and fixes of set defaults for quantifiers (#7120)
[cvc5.git]
/
test
/
regress
/
CMakeLists.txt
2021-09-07
Andrew Reynolds
Refactoring and fixes of set defaults for quantifiers...
blob
|
commitdiff
|
raw
2021-09-02
Aina Niemetz
Enable sygus-inst for FP, NIA and NRA. (#7098)
blob
|
commitdiff
|
raw
|
diff to current
2021-09-01
Haniel Barbosa
[proof] [sat] Fix lost reference to reason when process...
blob
|
commitdiff
|
raw
|
diff to current
2021-09-01
Andrew Reynolds
Fix issues with cyclic proofs due to double SYMM applic...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-30
Andrew Reynolds
Fix proof equality engine for "no-explain" premises...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-30
Andrew Reynolds
Fix quantifiers dynamic split module for parametric...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-26
Mathias Preiner
int2bv: Fix conversion of signed bit-vector values...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-23
Andrew Reynolds
Purify substitutions in strings proof reconstruction...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-23
Andrew Reynolds
Generalize inequality elimination in quantifiers rewrit...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-23
Andrew Reynolds
Fix single invocation partition for higher-order (...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-22
Andrew Reynolds
Prenex quantified formulas with user annotations by...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-20
Andrew Reynolds
Support sygus standard command syntax set-feature ...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-17
Andrew Reynolds
Fix policy for eliminating quantified formulas (#7017)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-09
Andrew V. Jones
Create grouping of tests that exercise '--use-approx...
blob
|
commitdiff
|
raw
|
diff to current
2021-08-05
Andrew Reynolds
Fix policy for rewriting string equalities (#6916)
blob
|
commitdiff
|
raw
|
diff to current
2021-08-04
Andrew Reynolds
Fix policy for merging subproofs (#6981)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-30
Gereon Kremer
Allow changing certain options while solving (#6945)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-29
Andrew Reynolds
Integrate central equality engine approach into theory...
blob
|
commitdiff
|
raw
|
diff to current
2021-07-27
Andres Noetzli
Add regression for fixed `str.indexof_re` issue (#6938)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-23
Aina Niemetz
FP: Add option to word-blast more lazily. (#6904)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-22
Andres Noetzli
Add support for minimal unsat cores (#4605)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-14
Haniel Barbosa
[proof] Fix open proof issues in SAT proof (#6887)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-14
Andrew Reynolds
Fix for context on input proof generator (#6873)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-13
Haniel Barbosa
[rewriter] Add rewrite to order IFF (equality for Boole...
blob
|
commitdiff
|
raw
|
diff to current
2021-07-12
Andrew Reynolds
Fix for learned rewrite pass, add regression (#6850)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-09
Andrew Reynolds
Fix sets cardinality inference involving equivalent...
blob
|
commitdiff
|
raw
|
diff to current
2021-07-07
Haniel Barbosa
[unsat cores] Adding regressions from #4971 (#6852)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-05
Andres Noetzli
[Strings] Fix incorrect rewrite (#6837)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-02
Mathias Preiner
Fix bv assert input reset assertions (#6820)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-02
Andrew Reynolds
Fix rewriter for negative constant seq.nth (#6827)
blob
|
commitdiff
|
raw
|
diff to current
2021-07-01
Andrew Reynolds
Add recursive function definitions to subsolver in...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-30
Mathias Preiner
Use SAT context level for --bv-assert-input instead...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-30
yoni206
pow2: new test (#6819)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-30
Andrew Reynolds
Do not apply fmfBound to standard quantifiers when...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-30
Andrew Reynolds
Fix pre vs. post-rewrite in proofs for theory preproces...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-30
yoni206
int-to-bv: correct model values (#6811)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-28
yoni206
Rewrite POW to POW2 when the base is 2 (#6806)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-26
yoni206
pow2 -- final changes (#6800)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-24
Andrew Reynolds
Fix linear arithmetic for duplicate lemmas in increment...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-23
Haniel Barbosa
[hol] Disable bound fmf when HOL (#6792)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-23
Haniel Barbosa
[regressions] Adding regression from #5371 (#6791)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-23
Haniel Barbosa
[parser] [hol] Fix parser check for allowing functions...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-22
Andrew Reynolds
Always check legal eliminations in quantified logics...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-22
Andrew Reynolds
Fix type enumeration for non first-class sorts in FMF...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-21
Mathias Preiner
Fix model issues with --bitblast=eager. (#6753)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-10
Andrew Reynolds
Ensure bv2nat and int2bv are not rewritten when using...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-09
Andres Noetzli
Make `--solve-int-as-bv=X` robust to rewriting (#6722)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-09
Andres Noetzli
Reorder ITE rewrites (#6723)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-08
Andrew Reynolds
Fix for 2 dimensional dependent bounded quantifiers...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-08
Gereon Kremer
Fix statistics option handler (#6703)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-08
Andrew Reynolds
Fix str.update reduction (#6696)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-07
Andrew Reynolds
(proof-new) Fix missing connection in trust substitutio...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-05
Andres Noetzli
Remove unwanted side effects in `SPLIT_EQ_STRIP_L`...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-04
Mathias Preiner
bv: Enable bitblast solver by default. (#6660)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-04
Andres Noetzli
Fix handling of start index in `str.indexof_re` (#6674)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-02
Andrew Reynolds
Fix unsat core proofs (#6655)
blob
|
commitdiff
|
raw
|
diff to current
2021-06-02
Andres Noetzli
Make `STRINGS_CTN_DECOMPOSE` an explicit conflict ...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-02
Gereon Kremer
Fix issues with double negation in circuit propagator...
blob
|
commitdiff
|
raw
|
diff to current
2021-06-01
Andrew Reynolds
Disable timeout regressions (#6650)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-31
Andres Noetzli
Compute model values for nested sequences in order...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-28
Andres Noetzli
`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts ...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-27
Andrew Reynolds
Fix regular expression aggressive elim (#6627)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-27
Andres Noetzli
Fix `str.replace_re` and `str.replace_re_all` (#6615)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-27
Andrew Reynolds
Fix CEGQI for datatypes with Boolean subfields (#6630)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-27
Andrew Reynolds
Fix spurious assertion for trivial abduction (#6629)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-27
Andres Noetzli
Return `REWRITE_AGAIN` after rewriting bvcomp (#6624)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-27
Andrew Reynolds
Enable new justification heuristic by default (#6613)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-24
Andrew Reynolds
Fix non-fixed length case in re-elim (#6612)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-24
Andrew Reynolds
Fix re-elim length requirement for symbolic RE membersh...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-20
Aina Niemetz
Fix echo printing. (#6573)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-19
Andrew Reynolds
Pass empty vector when constructing re empty, fixes...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-19
Haniel Barbosa
Adding regressions that failed on old unsat cores ...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-19
Andrew Reynolds
Fix positive contains indexof rewrites for empty string...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-19
Andres Noetzli
Improve handling of `:named` attributes (#6549)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-18
Andres Noetzli
Fix `collectEmptyEqs()` in string utils (#6562)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-17
Andres Noetzli
Fix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-12
Andrew Reynolds
Ensure sequences of Booleans generate Boolean term...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-08
Andrew Reynolds
Add support for datatype update (#6449)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-07
Aina Niemetz
Move slow regressions and update guidelines. (#6508)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-06
Andrew Reynolds
Discard duplicate terms in patterns (#6501)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-04
Aina Niemetz
FP: Move removal of generic to_fp operations to rewrite...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-03
Aina Niemetz
FP: Rewrite to_fp conversion from signed bit-vector...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-03
Aina Niemetz
SymFPU: Automatically apply patch from 2020-11-14....
blob
|
commitdiff
|
raw
|
diff to current
2021-04-27
Andrew Reynolds
Move slow regression to regress3 (#6451)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-27
Andrew Reynolds
Fix refutational soundness bug in quantifier prenexing...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-24
Andrew Reynolds
Improve getValue for non-evaluated operators (#6436)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-21
Mathias Preiner
Goodbye CVC4, hello cvc5! (#6371)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-20
Andrew Reynolds
Add instantiation pool feature to the API (#6358)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-15
Aina Niemetz
preprocessing context: Add wrapper for model substituti...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-15
Andrew Reynolds
Reenable regression for minimizing instantiations ...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-14
Abdalrhman Mohamed
Merge equivalent sub-obligations instead of discarding...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-13
Andrew Reynolds
Refactor quantifiers macros (#6348)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-13
Abdalrhman Mohamed
Fix sexpr bug with AST output language. (#6329)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-09
Andrew Reynolds
Add regressions for issue 6214 (#6305)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-09
Andres Noetzli
Learn equalities involving Boolean variables (#6323)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-08
Andrew Reynolds
Add benchmark for issue 5101 (#6301)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-08
Andrew Reynolds
Add benchmark for issue 4400 (#6288)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-08
Andrew Reynolds
Initial support for parametric datatypes in sygus ...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-07
Andrew Reynolds
Add benchmark for 6270 (#6283)
blob
|
commitdiff
|
raw
|
diff to current
next