projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
README: Remove project leaders, history.
[cvc5.git]
/
src
/
options
/
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
2018-09-22
Aina Niemetz
cmake: .cpp generation done, .h generation not yet...
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-09-17
Andrew Reynolds
More aggressive skolem caching for strings, document...
tree
|
commitdiff
2018-09-14
Andrew Reynolds
Generalize CandidateRewriteDatabase to ExprMiner (...
tree
|
commitdiff
2018-09-13
Haniel Barbosa
Uses information gain heuristic for building better...
tree
|
commitdiff
2018-09-11
Andrew Reynolds
Support model cores via option --produce-model-cores...
tree
|
commitdiff
2018-09-11
Haniel Barbosa
Using a single condition enumerator in sygus-unif ...
tree
|
commitdiff
2018-09-07
Mathias Preiner
Replace boost::integer_traits with std::numeric_limits...
tree
|
commitdiff
2018-09-04
Andres Noetzli
Remove unused options file (#2413)
tree
|
commitdiff
2018-08-31
Haniel Barbosa
Allows SAT checks of repair const to have different...
tree
|
commitdiff
2018-08-30
Andrew Reynolds
Add regular expression elimination module (#2400)
tree
|
commitdiff
2018-08-22
Andrew Reynolds
More unused code elimination (#2358)
tree
|
commitdiff
2018-08-21
Haniel Barbosa
Makes the new row propagation system default (#2335)
tree
|
commitdiff
2018-08-21
Andrew Reynolds
More unused code elimination (#2339)
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Disable argument relevance for sygus by default (#2288)
tree
|
commitdiff
2018-08-08
Andres Noetzli
Require Swig 3 (#2283)
tree
|
commitdiff
2018-08-08
Andres Noetzli
Delete functions instead of using CVC4_UNDEFINED (...
tree
|
commitdiff
2018-08-07
Andrew Reynolds
Make flat form inferences optional in strings (#2277)
tree
|
commitdiff
2018-08-03
Andrew Reynolds
Eliminate option for sygus UF evaluation functions...
tree
|
commitdiff
2018-08-02
Andres Noetzli
Remove Subversion build info (#2250)
tree
|
commitdiff
2018-08-02
Andres Noetzli
Remove outdated references to TLS (#2245)
tree
|
commitdiff
2018-07-31
Mathias Preiner
Fix option handler for lazy/bv-sat-solver combinations...
tree
|
commitdiff
2018-07-30
Mathias Preiner
Add support for incremental eager bit-blasting. (#1838)
tree
|
commitdiff
2018-07-30
FabianWolff
Fix several spelling errors (#2231)
tree
|
commitdiff
2018-07-27
Mathias Preiner
Require argument description for non-{bool,void} option...
tree
|
commitdiff
2018-07-27
Mathias Preiner
Make Python a required CVC4 dependency. (#2227)
tree
|
commitdiff
2018-07-26
ayveejay
Avoid explicit dependency on Python 3 (#2195)
tree
|
commitdiff
2018-07-24
Andrew Reynolds
Improvements to sets + cardinality + quantifiers (...
tree
|
commitdiff
2018-07-22
Andrew Reynolds
sygusComp2018: Improvements to CEGIS loop (#2187)
tree
|
commitdiff
2018-07-21
Andrew Reynolds
Optimizations and fixes for computing whether a type...
tree
|
commitdiff
2018-07-20
Andrew Reynolds
sygusComp2018: minor changes to repair constant utilit...
tree
|
commitdiff
2018-07-17
Andrew Reynolds
sygusComp2018: pbe multi-enumerator fairness option...
tree
|
commitdiff
2018-07-17
Andrew Reynolds
Minor cleanup and fixes for conflict-based instantiatio...
tree
|
commitdiff
2018-07-17
Andrew Reynolds
sygusComp2018: update policies for solution reconstruc...
tree
|
commitdiff
2018-07-17
Andrew Reynolds
sygusComp 2018: updates to sygus term database (#2170)
tree
|
commitdiff
2018-07-08
Andres Noetzli
Add more sophisticated floating-point sampler (#2155)
tree
|
commitdiff
2018-07-06
Andres Noetzli
Add option for timeout for rewrite candidate check...
tree
|
commitdiff
2018-07-03
Andrew Reynolds
Remove miscellaneous dead and unused code from quantifi...
tree
|
commitdiff
2018-07-02
Andrew Reynolds
Remove some dead code from theory strings (#2125)
tree
|
commitdiff
2018-06-27
Andrew Reynolds
Synthesize candidate-rewrites from standard inputs...
tree
|
commitdiff
2018-06-26
Andres Noetzli
sygusComp2018: Add evaluator (#2090)
tree
|
commitdiff
2018-06-25
Aina Niemetz
Updated copyright headers.
tree
|
commitdiff
2018-06-15
Andrew Reynolds
Disable solving non-linear BV literals by default ...
tree
|
commitdiff
2018-05-28
Andrew Reynolds
Builtin evaluation functions for sygus (#1991)
tree
|
commitdiff
2018-05-25
Andrew Reynolds
Reenable repair const (#1983)
tree
|
commitdiff
2018-05-23
Andrew Reynolds
Add notions of evaluated kinds in TheoryModel (#1947)
tree
|
commitdiff
2018-05-23
Andrew Reynolds
Generalize check-model in NonLinearExtension for quadra...
tree
|
commitdiff
2018-05-23
Andrew Reynolds
Repair constants using symbolic constructors (#1960)
tree
|
commitdiff
2018-05-22
Mathias Preiner
Add SymFPU licensing information. (#1952)
tree
|
commitdiff
2018-05-19
Haniel Barbosa
changing default (#1944)
tree
|
commitdiff
2018-05-17
Haniel Barbosa
Option to force return values of Bool functions to...
tree
|
commitdiff
2018-05-17
Andrew Reynolds
Cegis-specific infrastructure (#1933)
tree
|
commitdiff
2018-05-14
Andrew Reynolds
Add regressions, change defaults. (#1911)
tree
|
commitdiff
2018-05-10
Andrew Reynolds
Sygus repair constants (#1812)
tree
|
commitdiff
2018-05-09
Andrew Reynolds
Better option names for PBE (#1891)
tree
|
commitdiff
2018-05-09
PaulMeng
Add the symmetry breaker module (#1847)
tree
|
commitdiff
2018-05-04
Andres Noetzli
Make --output-lang consistent with --lang (#1877)
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Option to interleave tangent plane inferences (#1833)
tree
|
commitdiff
2018-05-03
Andres Noetzli
Remove (dummy) SMT1 printer (#1854)
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Initial support for string standard in smt lib 2.6...
tree
|
commitdiff
next