projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first
⋅
prev
⋅
next
Add bag inferences for operators: intersection, duplicate_removal, and empty bags...
[cvc5.git]
/
src
/
options
/
2020-03-12
Andrew Reynolds
Remove local theory extension option (#4048)
tree
|
commitdiff
2020-03-12
Aina Niemetz
Hide options for and related to the BV abstraction...
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Remove experimental symmetry breaker (#4005)
tree
|
commitdiff
2020-03-11
Andrew Reynolds
Remove partial instantiation for local theory extension...
tree
|
commitdiff
2020-03-10
Andrew Reynolds
Rename sygus option name (#3977)
tree
|
commitdiff
2020-03-06
Andres Noetzli
Remove --apply-to-const preprocessing pass (#3919)
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-02-29
Andrew Reynolds
Replace conditional rewrite pass in quantifiers with...
tree
|
commitdiff
2020-02-26
Andrew Reynolds
Support for witnessing choice in models (#3781)
tree
|
commitdiff
2020-02-26
Andres Noetzli
Remove portfolio leftovers (#3821)
tree
|
commitdiff
2020-02-25
yoni206
bv_to_int preprocessing pass
tree
|
commitdiff
2020-02-21
Andrew V. Jones
Adding checks to the validation of 'bv-sat-solver'...
tree
|
commitdiff
2020-02-20
Mathias Preiner
resource manager: Add statistic for every resource...
tree
|
commitdiff
2020-02-17
Andrew Reynolds
Option to limit the number of rounds of enumerative...
tree
|
commitdiff
2020-02-14
Andrew Reynolds
Remove quantifiers rewrite rules infrastructure (#3754)
tree
|
commitdiff
2020-02-11
Andres Noetzli
Remove `--strings-binary-csp` option (#3743)
tree
|
commitdiff
2020-01-31
Andrew Reynolds
Allow PBE symmetry breaking with sygus stream (#3686)
tree
|
commitdiff
2019-12-19
Mathias Preiner
Fix typo in smt_options.toml. (#3579)
tree
|
commitdiff
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
tree
|
commitdiff
2019-12-10
Haniel Barbosa
Fix ufho issues (#3551)
tree
|
commitdiff
2019-12-06
Andrew Reynolds
New algorithm for interpolation and abduction based...
tree
|
commitdiff
2019-12-05
Andrew Reynolds
Refactor mode options for Unif+PI (#3531)
tree
|
commitdiff
2019-12-04
Andrew Reynolds
New grammar construction modes for SyGuS (#3486)
tree
|
commitdiff
2019-11-29
Andrew Reynolds
Check free variables in assertions when using SyGuS...
tree
|
commitdiff
2019-11-27
Haniel Barbosa
Enable sygusRecFun by default and fixes SyGuS+RecFun...
tree
|
commitdiff
2019-11-21
Haniel Barbosa
hard limit for rec-fun eval (#3485)
tree
|
commitdiff
2019-11-17
Andres Noetzli
Add support for ThreadSanitizer instrumentation (#3467)
tree
|
commitdiff
2019-11-06
Andrew Reynolds
Support for SyGuS PBE + recursive functions (#3433)
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-10-20
Andrew V. Jones
Cleaning-up the declaration of wrapped functions/method...
tree
|
commitdiff
2019-10-11
Andres Noetzli
Add support for UBSan instrumentation (#3382)
tree
|
commitdiff
2019-10-08
Ying Sheng
Make ackermannization generally applicable rather than...
tree
|
commitdiff
2019-09-30
Andrew Reynolds
Add help for sygus 2.0 (#3318)
tree
|
commitdiff
2019-09-16
Andrew Reynolds
Remove equality inference option for quantifiers (...
tree
|
commitdiff
2019-09-16
Aina Niemetz
Fix compiler warning in options.cpp. (#3284)
tree
|
commitdiff
2019-09-12
Andrew Reynolds
Rename UF with cardinality extension (#3241)
tree
|
commitdiff
2019-09-07
Andrew Reynolds
Remove portfolio (#3236)
tree
|
commitdiff
2019-09-06
Mathias Preiner
Remove SMT1 parser. (#3228)
tree
|
commitdiff
2019-08-23
Andrew Reynolds
Update dynamic splitting strategy for quantifiers ...
tree
|
commitdiff
2019-08-14
Mathias Preiner
Remove option --continued-execution. (#3189)
tree
|
commitdiff
2019-08-14
Andrew Reynolds
Call separate SMT engine for single invocation sygus...
tree
|
commitdiff
2019-08-13
Andrew Reynolds
Implement check abduct feature (#3152)
tree
|
commitdiff
2019-08-10
Andrew Reynolds
Add option to only dump unsolved queries for --sygus...
tree
|
commitdiff
2019-08-03
Haniel Barbosa
Collapse @ chains in SMT2 printer (#3140)
tree
|
commitdiff
2019-08-02
Mathias Preiner
Update CaDiCaL to version 1.0.3. (#3137)
tree
|
commitdiff
2019-08-01
Andrew Reynolds
Regular expression intersection modes (#3134)
tree
|
commitdiff
2019-07-31
Haniel Barbosa
Parsing THF and adding several regressions (#3131)
tree
|
commitdiff
2019-07-29
Andrew Reynolds
Model blocker feature (#3112)
tree
|
commitdiff
2019-07-29
Andrew Reynolds
Support get-abduct smt2 command (#3122)
tree
|
commitdiff
2019-07-23
Andrew Reynolds
Fix help messages (#3096)
tree
|
commitdiff
2019-07-18
Andrew V. Jones
Removing forward-declaration of undefined function...
tree
|
commitdiff
2019-07-08
Andrew Reynolds
Towards refactoring relations (#3078)
tree
|
commitdiff
2019-07-01
Andrew Reynolds
Support sygus version 2 format (#3066)
tree
|
commitdiff
2019-07-01
Andrew Reynolds
Add higher-order elimination preprocessing pass (#2865)
tree
|
commitdiff
2019-06-21
Andres Noetzli
Fix and simplify handling of --force-logic (#3062)
tree
|
commitdiff
2019-05-18
Andres Noetzli
Support for incremental bit-blasting with CaDiCaL ...
tree
|
commitdiff
2019-05-15
Aina Niemetz
BV: Do not enable abstraction when eager bit-blasting...
tree
|
commitdiff
2019-05-10
Andrew Reynolds
Disable relational triggers (#2994)
tree
|
commitdiff
2019-05-09
Andrew Reynolds
Fixes for relational triggers (#2967)
tree
|
commitdiff
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
tree
|
commitdiff
2019-04-23
Alex Ozdemir
[BV] An option for SAT proof optimization (#2915)
tree
|
commitdiff
2019-04-16
Andrew Reynolds
Stratify enumerative instantiation (#2954)
tree
|
commitdiff
2019-04-16
Andrew Reynolds
Minor simplifications to theory quantifiers (#2953)
tree
|
commitdiff
2019-04-04
Haniel Barbosa
Ignoring FP benchmarks with "unsafe" sizes unless optio...
tree
|
commitdiff
2019-04-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-03-26
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-03-22
Haniel Barbosa
fix help information on TPTP parsing (#2884)
tree
|
commitdiff
2019-03-20
Andrew Reynolds
Sygus abduction feature (#2744)
tree
|
commitdiff
2019-03-16
Alex Ozdemir
Enable CryptoMiniSat-backed BV proofs (#2847)
tree
|
commitdiff
2019-03-12
Andrew Reynolds
Add option --sygus-rr-synth-rec for considering all...
tree
|
commitdiff
2019-01-17
Andres Noetzli
Add option to print BV constants in binary (#2805)
tree
|
commitdiff
2019-01-15
Andres Noetzli
Strings: Add option to change loop process mode (#2794)
tree
|
commitdiff
2019-01-09
Alex Ozdemir
[BV Proofs] Option for proof format (#2777)
tree
|
commitdiff
2018-12-14
Aina Niemetz
Fixed typos.
tree
|
commitdiff
2018-12-11
Andrew Reynolds
Remove alternate versions of mbqi (#2742)
tree
|
commitdiff
2018-12-10
makaimann
BoolToBV modes (off, ite, all) (#2530)
tree
|
commitdiff
2018-12-07
Alex Ozdemir
Enable BV proofs when using an eager bitblaster (#2733)
tree
|
commitdiff
2018-12-04
Andrew Reynolds
Enable regular expression elimination by default. ...
tree
|
commitdiff
2018-11-28
Andrew Reynolds
Generalize sygus stream solution filtering to logical...
tree
|
commitdiff
2018-11-05
Andrew Reynolds
Change default sygus enumeration mode to auto (#2689)
tree
|
commitdiff
2018-10-31
Andrew Reynolds
Add optimized sygus enumeration (#2677)
tree
|
commitdiff
2018-10-20
Andrew Reynolds
Sygus streaming non-implied predicates (#2660)
tree
|
commitdiff
2018-10-19
Mathias Preiner
Remove autotools build system. (#2639)
tree
|
commitdiff
2018-10-19
Andres Noetzli
Add OptionException handling during initialization...
tree
|
commitdiff
2018-10-19
Andrew Reynolds
Non-implied mode for model cores (#2653)
tree
|
commitdiff
2018-10-18
Andres Noetzli
Show if ASAN build in --show-config (#2650)
tree
|
commitdiff
2018-10-18
Andrew Reynolds
Sygus query generator (#2465)
tree
|
commitdiff
2018-10-16
Haniel Barbosa
Option for shuffling condition pool in CegisUnif (...
tree
|
commitdiff
2018-10-15
Andrew Reynolds
Delay initialization of theory engine (#2621)
tree
|
commitdiff
2018-10-13
Andres Noetzli
Reset input language for ExprMiner subsolver (#2624)
tree
|
commitdiff
2018-10-12
Andrew Reynolds
Improvements to rewrite rules from inputs (#2625)
tree
|
commitdiff
2018-10-11
Haniel Barbosa
Fix default setting of CegisUnif options (#2605)
tree
|
commitdiff
2018-10-11
Andrew Reynolds
Synthesize rewrite rules from inputs (#2608)
tree
|
commitdiff
2018-10-09
Andrew Reynolds
Support for basic actively-generated enumerators ...
tree
|
commitdiff
2018-10-05
Andrew Reynolds
Update default options for sygus (#2586)
tree
|
commitdiff
2018-10-04
Aina Niemetz
New C++ API: Add checks for Sorts. (#2519)
tree
|
commitdiff
2018-10-03
Andrew Reynolds
Add actively generated sygus enumerators (#2552)
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Only build libcvc4 and libcvc4parser as libraries.
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Cleanup CMakeLists.txt files, remove SHARED.
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Working build infrastructure.
tree
|
commitdiff
next