projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Update option --nl-ext to enable/disable incremental linearization solver only (...
2020-06-25
Andrew Reynolds
Update option --nl-ext to enable/disable incremental...
commit
|
commitdiff
|
tree
2020-06-24
Andres Noetzli
Fix CVC4_EXTRAVERSION variable (#4653)
commit
|
commitdiff
|
tree
2020-06-24
Andres Noetzli
[unconstrained] Fix gathering of visited-once vars...
commit
|
commitdiff
|
tree
2020-06-23
Andrew Reynolds
(proof-new) Updates to proof node manager (#4617)
commit
|
commitdiff
|
tree
2020-06-23
Aina Niemetz
New C++ API: Remove examples for old API. (#4650)
commit
|
commitdiff
|
tree
2020-06-23
Mathias Preiner
Add support for eqrange predicate (#4562)
commit
|
commitdiff
|
tree
2020-06-22
Andrew Reynolds
(proof-new) Add REWRITE trust node kind. (#4624)
commit
|
commitdiff
|
tree
2020-06-22
Aina Niemetz
get-authors: Add alias for nafur. (#4646)
commit
|
commitdiff
|
tree
2020-06-22
nafur
Allow for better interaction of Integer/Rational with...
commit
|
commitdiff
|
tree
2020-06-22
Andrew Reynolds
(proof-new) Add proof-new to options file (#4641)
commit
|
commitdiff
|
tree
2020-06-22
Andrew Reynolds
Add trascendental function kinds to list of unevaluated...
commit
|
commitdiff
|
tree
2020-06-22
yoni206
fix (#4637)
commit
|
commitdiff
|
tree
2020-06-20
Alex Ozdemir
Use traversal iterators in IntToBv (#4169)
commit
|
commitdiff
|
tree
2020-06-20
Abdalrhman Mohamed
Add Match utility function. (#4632)
commit
|
commitdiff
|
tree
2020-06-20
Andrew Reynolds
(proof-new) Make static methods in re-elim (#4623)
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
(proof-new) CDProof inherits from ProofGenerator (...
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
Add casc j10 scripts (#4621)
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
(proof-new) Updates to strings term registry (#4599)
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
Convert more uses of strings to words (#4584)
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
(proof-new) Split operator elimination from arithmetic...
commit
|
commitdiff
|
tree
2020-06-19
Andrew Reynolds
Clean the header file of TheoryStrings (#4272)
commit
|
commitdiff
|
tree
2020-06-19
Andres Noetzli
Update version information post 1.8 release (#4635)
commit
|
commitdiff
|
tree
2020-06-19
Haniel Barbosa
Always rewrite boolean ITEs with constant then/else...
commit
|
commitdiff
|
tree
2020-06-19
Andres Noetzli
Update info for 1.8 release (#4633)
commit
|
commitdiff
|
tree
2020-06-19
Andres Noetzli
Cleanup examples (#4634)
commit
|
commitdiff
|
tree
2020-06-19
Haniel Barbosa
Generalize atom collection in old proof code (#4626)
commit
|
commitdiff
|
tree
2020-06-19
yoni206
Bv to int elimination bugfix (#4435)
...assertion error [here](https://
github
.com/CVC4/CVC4/blob/8236d7f9bff3aef4f7b3...
commit
|
commitdiff
|
tree
2020-06-19
Andres Noetzli
Add logic check for define-fun(s)-rec (#4577)
commit
|
commitdiff
|
tree
2020-06-19
Andrew V. Jones
Revert "[Python] Properly destroy CVC4 object (#3753...
commit
|
commitdiff
|
tree
2020-06-18
Andres Noetzli
Improve memory management in Java bindings (#4629)
commit
|
commitdiff
|
tree
2020-06-17
Andrew Reynolds
Do not traverse WITNESS for partial substitutions in...
commit
|
commitdiff
|
tree
2020-06-17
Haniel Barbosa
Improve polynomial anyterm grammar (#3566)
commit
|
commitdiff
|
tree
2020-06-16
Andrew Reynolds
Updates to NEWS. (#4628)
commit
|
commitdiff
|
tree
2020-06-16
Abdalrhman Mohamed
Simplify sygus conversion script. (#4627)
commit
|
commitdiff
|
tree
2020-06-16
Aina Niemetz
Add missing REQUIRES to new regressions. (#4625)
commit
|
commitdiff
|
tree
2020-06-16
Aina Niemetz
BV: Fix querying equality status in lazy bit-blaster...
commit
|
commitdiff
|
tree
2020-06-16
Aina Niemetz
Fix regressions in regress1 after #4613. (#4616)
commit
|
commitdiff
|
tree
2020-06-16
Andrew Reynolds
(proof-new) Add quantifiers proof checker (#4593)
commit
|
commitdiff
|
tree
2020-06-15
Andrew Reynolds
(proof-new) Update proof node, add proof node algorithm...
commit
|
commitdiff
|
tree
2020-06-15
Haniel Barbosa
Support AND/OR definitions in lambda to array rewriting...
commit
|
commitdiff
|
tree
2020-06-15
Aina Niemetz
BV: Add missing type check for BITVECTOR_REPEAT_OP...
commit
|
commitdiff
|
tree
2020-06-15
Aina Niemetz
BV: Add missing type check for INT_TO_BITVECTOR. (...
commit
|
commitdiff
|
tree
2020-06-15
Andrew Reynolds
Do RE derivation inference only for concrete constant...
commit
|
commitdiff
|
tree
2020-06-13
Andrew Reynolds
Move sygus datatype utility functions to their own...
commit
|
commitdiff
|
tree
2020-06-12
Andrew Reynolds
Update to consistent policy for removed terms in quantifier...
commit
|
commitdiff
|
tree
2020-06-12
Andrew Reynolds
(proof-new) Term conversion proof generator utility...
commit
|
commitdiff
|
tree
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_tags...
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...
...simply recursive datatypes (https://
github
.com/ajreynol/CVC4/tree/dtNonSimpleRec...
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-authors...
commit
|
commitdiff
|
tree
2020-06-03
Andrew Reynolds
Do not apply unconstrained simplification when quantifiers...
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
next