projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2020-06-12
Andrew Reynolds
(proof-new) Minor updates to strings base solver (...
commit
|
commitdiff
|
tree
2020-06-12
Andrew Reynolds
Cardinality-related inferences per type in theory of...
commit
|
commitdiff
|
tree
2020-06-12
Andrew Reynolds
(proof-new) Split TheoryEngine (#4558)
commit
|
commitdiff
|
tree
2020-06-12
Andres Noetzli
Fix install of static builds (#4604)
commit
|
commitdiff
|
tree
2020-06-12
Andrew Reynolds
Add rewrite for str.replace_re. (#4601)
commit
|
commitdiff
|
tree
2020-06-11
Andrew Reynolds
(proof-new) Add lazy proof utility (#4589)
commit
|
commitdiff
|
tree
2020-06-11
Andrew Reynolds
(proof-new) Add eager proof generator utility. (#4592)
commit
|
commitdiff
|
tree
2020-06-11
Andrew Reynolds
(proof-new) Remove arith-snorm option. (#4591)
commit
|
commitdiff
|
tree
2020-06-10
Andrew Reynolds
(proof-new) Theory proof step buffer utility (#4580)
commit
|
commitdiff
|
tree
2020-06-10
Andres Noetzli
Add support for str.replace_re/str.replace_re_all ...
commit
|
commitdiff
|
tree
2020-06-10
makaimann
Fix getKind for Python bindings (#4496)
commit
|
commitdiff
|
tree
2020-06-09
Andrew Reynolds
(proof-new) Refactor skolemization (#4586)
commit
|
commitdiff
|
tree
2020-06-09
Andrew Reynolds
(proof-new) Add trust node utility (#4588)
commit
|
commitdiff
|
tree
2020-06-09
Andres Noetzli
Language bindings: Enable catching of exceptions (...
commit
|
commitdiff
|
tree
2020-06-09
Andrew V. Jones
Ensure correct CMake dependencies on Debug_tags.h/Trace...
commit
|
commitdiff
|
tree
2020-06-09
Andres Noetzli
Fix Java target and Relations example (#4583)
commit
|
commitdiff
|
tree
2020-06-08
Andres Noetzli
Fix ambiguous overload in unit test (#4582)
commit
|
commitdiff
|
tree
2020-06-08
Andrew Reynolds
(proof-new) Add abstract proof generator class (#4574)
commit
|
commitdiff
|
tree
2020-06-08
Andres Noetzli
Fix Coverity issues (#4587)
commit
|
commitdiff
|
tree
2020-06-06
Andrew Reynolds
Use NlLemma utility for all lemmas in non-linear. ...
commit
|
commitdiff
|
tree
2020-06-06
Andres Noetzli
Fix destruction order in NodeManager (#4578)
commit
|
commitdiff
|
tree
2020-06-06
Andres Noetzli
Keep definitions when global-declarations enabled ...
commit
|
commitdiff
|
tree
2020-06-06
Andrew Reynolds
Smt2 parsing support for nested recursive datatypes...
commit
|
commitdiff
|
tree
2020-06-05
Andrew Reynolds
Datatypes with nested recursion are not handled in...
commit
|
commitdiff
|
tree
2020-06-05
Andrew Reynolds
(proof-new) Updates to CDProof (#4565)
commit
|
commitdiff
|
tree
2020-06-05
Andres Noetzli
Skip parse-error regression for comp builds (#4567)
commit
|
commitdiff
|
tree
2020-06-05
Andrew Reynolds
(proof-new) Rename ProofSkolemCache to SkolemManager...
commit
|
commitdiff
|
tree
2020-06-05
Haniel Barbosa
Changing default language (#4561)
commit
|
commitdiff
|
tree
2020-06-05
Haniel Barbosa
Printing FP values as binary or indexed BVs according...
commit
|
commitdiff
|
tree
2020-06-05
Andres Noetzli
Fix handling of Boolean term variables (#4550)
commit
|
commitdiff
|
tree
2020-06-05
Andres Noetzli
Fix lifetime and copy issues with NodeDfsIterable ...
commit
|
commitdiff
|
tree
2020-06-05
Andrew V. Jones
If using 'ninja', tell the user to run 'ninja' not...
commit
|
commitdiff
|
tree
2020-06-05
makaimann
Add a method for retrieving base of a constant array...
commit
|
commitdiff
|
tree
2020-06-05
Andres Noetzli
Update Java tests to match changes in API (#4535)
commit
|
commitdiff
|
tree
2020-06-04
makaimann
Wrap Result in Python API (#4473)
commit
|
commitdiff
|
tree
2020-06-04
Aina Niemetz
New C++ Api: Second and last batch of API guards. ...
commit
|
commitdiff
|
tree
2020-06-04
Andrew Reynolds
Add sygus datatype substitution utility method (#4390)
commit
|
commitdiff
|
tree
2020-06-04
Andrew Reynolds
Fix abduction with datatypes (#4566)
commit
|
commitdiff
|
tree
2020-06-04
Andrew Reynolds
Theory strings preprocess (#4534)
commit
|
commitdiff
|
tree
2020-06-04
Aina Niemetz
New C++ Api: First batch of API guards. (#4557)
commit
|
commitdiff
|
tree
2020-06-03
Haniel Barbosa
(proof-new) Adding rules and proof checker for EUF...
commit
|
commitdiff
|
tree
2020-06-03
Haniel Barbosa
(proof-new) Adding rules and proof checker for Boolean...
commit
|
commitdiff
|
tree
2020-06-03
Andrew Reynolds
(proof-new) Add builtin proof checker (#4537)
commit
|
commitdiff
|
tree
2020-06-03
Mathias Preiner
Fix normalization of author names in contrib/get-author...
commit
|
commitdiff
|
tree
2020-06-03
Andrew Reynolds
Do not apply unconstrained simplification when quantifi...
commit
|
commitdiff
|
tree
2020-06-03
Andrew Reynolds
Update CEGQI to use lemma status instead of forcing...
commit
|
commitdiff
|
tree
2020-06-03
Andrew Reynolds
Use prenex normal form when using cegqi-nested-qe ...
commit
|
commitdiff
|
tree
2020-06-03
makaimann
Add Term::substitute to Python bindings (#4499)
commit
|
commitdiff
|
tree
2020-06-02
makaimann
Add hash Op, Sort and Term in Python bindings (#4498)
commit
|
commitdiff
|
tree
2020-06-02
Andrew Reynolds
Fix scope issue with pulling ITEs in extended rewriter...
commit
|
commitdiff
|
tree
2020-06-02
Andrew Reynolds
Do not handle universal quantification on functions...
commit
|
commitdiff
|
tree
2020-06-02
Aina Niemetz
New C++ API: Keep reference to solver object in non...
commit
|
commitdiff
|
tree
2020-06-01
Andrew Reynolds
(proof-new) Proof step buffer utilities (#4533)
commit
|
commitdiff
|
tree
2020-06-01
Andrew Reynolds
Move non-linear files to src/theory/arith/nl (#4548)
commit
|
commitdiff
|
tree
2020-06-01
Andres Noetzli
Set theoryof-mode after theory widening (#4545)
commit
|
commitdiff
|
tree
2020-06-01
Andres Noetzli
Do not parse ->/lambda unless --uf-ho enabled (#4544)
commit
|
commitdiff
|
tree
2020-06-01
Andrew Reynolds
Incorporate sequences into the word interface (#4543)
commit
|
commitdiff
|
tree
2020-05-31
Andres Noetzli
Do not cache operator eliminations in arith (#4542)
commit
|
commitdiff
|
tree
2020-05-31
yoni206
update example in README to use ctest. (#4540)
commit
|
commitdiff
|
tree
2020-05-30
Andrew Reynolds
Add the sequence type (#4539)
commit
|
commitdiff
|
tree
2020-05-28
Andrew Reynolds
Fix term registry for constant case, simplify. (#4538)
commit
|
commitdiff
|
tree
2020-05-27
Andrew Reynolds
Add the Expr-level sequence datatype (#4526)
commit
|
commitdiff
|
tree
2020-05-27
Martin
Tweak the use of static_assert to support older compile...
commit
|
commitdiff
|
tree
2020-05-26
Martin
Fix an incorrect limit in conversion from real to float...
commit
|
commitdiff
|
tree
2020-05-26
Andrew Reynolds
Convert more uses of strings to words (#4527)
commit
|
commitdiff
|
tree
2020-05-26
Mathias Preiner
Fix mismatched iterators (CID 1493892). (#4531)
commit
|
commitdiff
|
tree
2020-05-26
Andrew Reynolds
(proof-new) Update proof checker. (#4511)
commit
|
commitdiff
|
tree
2020-05-26
Andrew Reynolds
(proof-new) Updates to strings skolem cache. (#4524)
commit
|
commitdiff
|
tree
2020-05-26
Mathias Preiner
Update to CaDiCaL version 1.2.1. (#4530)
commit
|
commitdiff
|
tree
2020-05-24
Andres Noetzli
[SMT-COMP] Redirect non-answers to /dev/null (#4528)
commit
|
commitdiff
|
tree
2020-05-23
mudathirmahgoub
remove unused field d_emp_exp in TheorySetsPrivate...
commit
|
commitdiff
|
tree
2020-05-23
Andrew Reynolds
Add the sequence datatype (#4153)
commit
|
commitdiff
|
tree
2020-05-23
Abdalrhman...
Fix mistakes in sygus API comments. (#4520)
commit
|
commitdiff
|
tree
2020-05-23
Andrew Reynolds
Refactor operator elimination in arithmetic (#4519)
commit
|
commitdiff
|
tree
2020-05-22
Andres Noetzli
[SMT-COMP] Use tear-down-incremental for arithmetic...
commit
|
commitdiff
|
tree
2020-05-22
Aina Niemetz
CaDiCaL: Clean up initialization on creation. (#4516)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
(proof-new) Add rewrite corresponding to regular expres...
commit
|
commitdiff
|
tree
2020-05-22
Aina Niemetz
Cryptominisat: Clean up initialization on creation...
commit
|
commitdiff
|
tree
2020-05-22
Aina Niemetz
Add support for SAT solver Kissat. (#4514)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
(proof-new) Proof node to SExpr utility. (#4512)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
Update string kind names in new API (#4509)
commit
|
commitdiff
|
tree
2020-05-22
Andrew Reynolds
(proof-new) Minor update to strings solver state (...
commit
|
commitdiff
|
tree
2020-05-21
Andrew Reynolds
Disable re-elim by default (#4508)
commit
|
commitdiff
|
tree
2020-05-21
Abdalrhman...
Make Grammar reusable. (#4506)
commit
|
commitdiff
|
tree
2020-05-21
Andrew Reynolds
Throw logic exception for equality between regular...
commit
|
commitdiff
|
tree
2020-05-21
Andrew Reynolds
Fix missing check for cardinality one in unconstrained...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Normal form equality conflicts and uniqueness check...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Add proof skolem cache (#4485)
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Fix parametric datatype instantiation (#4493)
commit
|
commitdiff
|
tree
2020-05-20
Aina Niemetz
CegqiBv: Clean up after renaming options. (#4487)
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Use debug-check-model to enable internal debugging...
commit
|
commitdiff
|
tree
2020-05-20
Abdalrhman...
Add a simple script to convert sygus v1 files to v2...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Do not eliminate variables that are equal to unevaluata...
commit
|
commitdiff
|
tree
2020-05-20
Andrew Reynolds
Fix cached free variable identifiers in sygus term...
commit
|
commitdiff
|
tree
2020-05-19
mudathirmahgoub
Renamed operator CHOICE to WITNESS (#4207)
commit
|
commitdiff
|
tree
2020-05-19
Andrew Reynolds
Use fresh variables when miniscoping (#4296)
commit
|
commitdiff
|
tree
2020-05-19
Andrew Reynolds
Update enum and option names for sygus languages (...
commit
|
commitdiff
|
tree
2020-05-19
Andres Noetzli
Make SolveEq and PlusCombineLikeTerms idempotent (...
commit
|
commitdiff
|
tree
2020-05-12
Andrew Reynolds
Do not enable unconstrained simplification if arithmeti...
commit
|
commitdiff
|
tree
2020-05-06
Andres Noetzli
Update run scripts for SMT-COMP 2020 (#4454)
commit
|
commitdiff
|
tree
next