projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
genkinds: Do not use relative paths to find src directory. (#6293)
[cvc5.git]
/
src
/
options
/
2021-04-06
Andrew Reynolds
Remove stdPrintAscii option (#6280)
tree
|
commitdiff
2021-04-02
Gereon Kremer
New statistics registry (#6210)
tree
|
commitdiff
2021-04-01
Aina Niemetz
Rename namespace CVC5 to cvc5. (#6258)
tree
|
commitdiff
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
tree
|
commitdiff
2021-03-23
Haniel Barbosa
Removing unused build options and deprecated proof...
tree
|
commitdiff
2021-03-16
Mathias Preiner
cmake: Generate cvc4_export.h and set visibility to...
tree
|
commitdiff
2021-03-16
Haniel Barbosa
[proof-new] Renaming proof option to be in sync with...
tree
|
commitdiff
2021-03-14
Diego Della Rocca...
[proof-new] Adding a dot printer for proof nodes (...
tree
|
commitdiff
2021-03-11
MikolasJanota
Improvements and refactoring for enumeratative strategy...
tree
|
commitdiff
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
tree
|
commitdiff
2021-03-06
Mathias Preiner
Remove SMT-LIB 2.5 and 2.0 support. (#6068)
tree
|
commitdiff
2021-03-03
Gereon Kremer
More cleanup of includes to reduce compilation times...
tree
|
commitdiff
2021-02-22
Andrew Reynolds
(proof-new) Change proof-new option to proof (#5955)
tree
|
commitdiff
2021-02-22
Andrew Reynolds
Require length-in-conclusion form for strings inference...
tree
|
commitdiff
2021-02-22
Haniel Barbosa
[proof-new] Optionally print conclusion in the AST...
tree
|
commitdiff
2021-02-10
Andrew Reynolds
Remove track instantiations infrastructure (#5883)
tree
|
commitdiff
2021-02-09
Mathias Preiner
cmake: Make Python3 default and improve toml error...
tree
|
commitdiff
2021-02-09
Andrew Reynolds
Make term database optionally SAT-context-dependent...
tree
|
commitdiff
2021-02-08
Andrew Reynolds
Remove support for inst closure (#5874)
tree
|
commitdiff
2021-02-04
yoni206
Adding an option to optimize polite combination for...
tree
|
commitdiff
2021-02-03
Mathias Preiner
Add BV solver bitblast. (#5851)
tree
|
commitdiff
2021-01-29
Haniel Barbosa
[proof-new] Connecting new unsat cores (#5834)
tree
|
commitdiff
2021-01-27
Andrew Reynolds
(proof-new) Improvements to quantifiers engine and...
tree
|
commitdiff
2021-01-26
Andrew Reynolds
Remove deprecated quantifiers modules (#5820)
tree
|
commitdiff
2021-01-24
Andrew Reynolds
Initial cleaning of triggers (#5795)
tree
|
commitdiff
2021-01-12
yoni206
Foreign theory rewrite option (#5763)
tree
|
commitdiff
2020-12-23
Haniel Barbosa
Dumping unsat cores after check-sat-assuming/QUERY...
tree
|
commitdiff
2020-12-23
Andrew Reynolds
Remove quant EPR option (#5716)
tree
|
commitdiff
2020-12-22
Andrew Reynolds
Remove preregister instantiation heuristic (#5713)
tree
|
commitdiff
2020-12-16
Andrew Reynolds
Simplify preprocessing (#5647)
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Remove bv divide by zero option (#5672)
tree
|
commitdiff
2020-12-14
Andrew Reynolds
Properly implement datatype selector triggers (#5624)
tree
|
commitdiff
2020-12-09
yoni206
update doc (#5619)
tree
|
commitdiff
2020-12-08
Mathias Preiner
Disable algebraic BV subtheory by default and make...
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Fix issue with free variables introduced by quantifier...
tree
|
commitdiff
2020-12-05
Everett Maus
Change generated options to be thread_local. (#5583)
tree
|
commitdiff
2020-12-03
yoni206
Models as (#5581)
tree
|
commitdiff
2020-11-19
Aina Niemetz
Include stddef.h (needed for size_t) in cvc4_public...
tree
|
commitdiff
2020-11-16
Gereon Kremer
Improve accuracy of resource limitation (#4763)
tree
|
commitdiff
2020-11-13
yoni206
Model declarations printing options (#5432)
tree
|
commitdiff
2020-11-12
Andrew Reynolds
(proof-new) Improve printing and debugging for pedantic...
tree
|
commitdiff
2020-11-06
Andrew Reynolds
Simplify printing with respect to expression types...
tree
|
commitdiff
2020-10-27
Gereon Kremer
Disable --nl-cad option by default (#5350)
tree
|
commitdiff
2020-10-27
Gereon Kremer
Enable --nl-cad by default (#5345)
tree
|
commitdiff
2020-10-12
Andrew Reynolds
Remove uf-ss-totality option (#5251)
tree
|
commitdiff
2020-10-11
Mathias Preiner
SyGuS instantiation modes (#5228)
tree
|
commitdiff
2020-10-05
Andrew Reynolds
Make sygus more robust to unknown responses in solution...
tree
|
commitdiff
2020-10-01
Mathias Preiner
Add additional ground terms to SyGuS instantiation...
tree
|
commitdiff
2020-10-01
Gereon Kremer
Allow to use the initial assignment for CAD (#5177)
tree
|
commitdiff
2020-09-23
yoni206
bv2int: new options for bvand translation (#5096)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Add simple BV solver (#5065)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-22
Gereon Kremer
ICP-based solver for nonlinear arithmetic (#5017)
tree
|
commitdiff
2020-09-12
Andrew Reynolds
(proof-new) Add SMT proof manager (#5054)
tree
|
commitdiff
2020-09-08
Andres Noetzli
Make CVC/API BV div/mod semantics match SMT-LIB (#4997)
tree
|
commitdiff
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
tree
|
commitdiff
2020-08-25
Andrew Reynolds
Add the combination engine (#4939)
tree
|
commitdiff
2020-08-21
Andrew Reynolds
Connect the relevance manager to TheoryEngine and use...
tree
|
commitdiff
2020-08-21
Andrew Reynolds
Remove BV equality slicer (#4928)
tree
|
commitdiff
2020-08-14
E Polgreen
correctly parse sygus lang option (#4884)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
(proof-new) Improve interfaces to proof generators...
tree
|
commitdiff
2020-08-12
Andrew Reynolds
(proof-new) Extensions to proof checker interface ...
tree
|
commitdiff
2020-08-11
Andrew Reynolds
Remove instantiation model true option (#4861)
tree
|
commitdiff
2020-08-05
Andres Noetzli
[Strings] Add eager context-dependent evaluation (...
tree
|
commitdiff
2020-08-04
Gereon Kremer
Add CAD-based solver (#4834)
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Remove arrays lazy rintro option (#4806)
tree
|
commitdiff
2020-07-17
Andrew Reynolds
Replace options listener infrastructure (#4764)
tree
|
commitdiff
2020-07-17
Andrew V. Jones
Support for using 'libedit' over 'readline' #4571 ...
tree
|
commitdiff
2020-07-17
Andrew Reynolds
(proof-new) Updates to strings core solver (#4642)
tree
|
commitdiff
2020-07-17
Andrew Reynolds
Add option manager and simpler option listener (#4745)
tree
|
commitdiff
2020-07-17
Gereon Kremer
Integration of libpoly (#4679)
tree
|
commitdiff
2020-07-16
Gereon Kremer
Resource manager cleanup (#4732)
tree
|
commitdiff
2020-07-16
Gereon Kremer
Remove cumulative time limits and cpu time limits ...
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Make use of options in setDefaults more consistent...
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Debug instantiations output (#4739)
tree
|
commitdiff
2020-07-14
Haniel Barbosa
Fix options messages that were inverted (#4734)
tree
|
commitdiff
2020-07-13
Andrew Reynolds
User-facing print debug option for sygus candidates...
tree
|
commitdiff
2020-07-13
Andrew Reynolds
Statistics on instantiations per quantified formula...
tree
|
commitdiff
2020-07-11
yoni206
Changing bv_to_int options (#4721)
tree
|
commitdiff
2020-07-08
Gereon Kremer
Re-implement handling of --tlimit (#4655)
tree
|
commitdiff
2020-07-08
Mathias Preiner
Add getName() method to options. (#4704)
tree
|
commitdiff
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
tree
|
commitdiff
2020-07-03
Andres Noetzli
Remove SWIG bindings (#4683)
tree
|
commitdiff
2020-07-01
Andrew Reynolds
Add solver for integer AND (#4681)
tree
|
commitdiff
2020-06-30
Ying Sheng
Interpolation step 1 (#4638)
tree
|
commitdiff
2020-06-25
Andrew Reynolds
Remove sygus1 parser (#4651)
tree
|
commitdiff
2020-06-25
Andrew Reynolds
Update option --nl-ext to enable/disable incremental...
tree
|
commitdiff
2020-06-23
Mathias Preiner
Add support for eqrange predicate (#4562)
tree
|
commitdiff
2020-06-22
Andrew Reynolds
(proof-new) Add proof-new to options file (#4641)
tree
|
commitdiff
2020-06-22
yoni206
fix (#4637)
tree
|
commitdiff
2020-06-18
Andres Noetzli
Improve memory management in Java bindings (#4629)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-11
Andrew Reynolds
(proof-new) Remove arith-snorm option. (#4591)
tree
|
commitdiff
2020-06-05
Andrew Reynolds
Datatypes with nested recursion are not handled in...
tree
|
commitdiff
2020-06-05
Haniel Barbosa
Printing FP values as binary or indexed BVs according...
tree
|
commitdiff
2020-06-03
Andrew Reynolds
Do not apply unconstrained simplification when quantifi...
tree
|
commitdiff
2020-06-03
Andrew Reynolds
Use prenex normal form when using cegqi-nested-qe ...
tree
|
commitdiff
2020-05-28
Andrew Reynolds
Fix term registry for constant case, simplify. (#4538)
tree
|
commitdiff
2020-05-23
Andrew Reynolds
Refactor operator elimination in arithmetic (#4519)
tree
|
commitdiff
2020-05-22
Aina Niemetz
Add support for SAT solver Kissat. (#4514)
tree
|
commitdiff
next