projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix non-lib-poly-build issues (#5028)
[cvc5.git]
/
test
/
2020-09-04
Mathias Preiner
Split lazy bit-vector solver from TheoryBV (#5009)
tree
|
commitdiff
2020-09-03
Gereon Kremer
Added a new rule to simplify (bvugt (bvurem T x) x...
tree
|
commitdiff
2020-09-03
yoni206
Changing the handled operators in bv2int preprocessing...
tree
|
commitdiff
2020-09-02
Andres Noetzli
Fix CryptoMiniSat build, regression (#5006)
tree
|
commitdiff
2020-09-02
Andres Noetzli
[Python API] Add missing methods to Datatype/Term ...
tree
|
commitdiff
2020-09-02
Andres Noetzli
[API] Fix Python Examples (#4943)
tree
|
commitdiff
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
tree
|
commitdiff
2020-08-31
Gereon Kremer
Fix --ackermann in the presence on syntactically differ...
tree
|
commitdiff
2020-08-28
yoni206
Incremental support for bv_to_int (#4967)
tree
|
commitdiff
2020-08-26
Andrew Reynolds
Replace Expr-level datatype with Node-level DType ...
tree
|
commitdiff
2020-08-24
Mathias Preiner
Increase regress level to 2 for production build. ...
tree
|
commitdiff
2020-08-21
Andrew Reynolds
Connect the relevance manager to TheoryEngine and use...
tree
|
commitdiff
2020-08-21
Andrew Reynolds
Simplify and fix care graph for ufHo (#4924)
tree
|
commitdiff
2020-08-20
Andrew Reynolds
Add strings-exp to regression (#4923)
tree
|
commitdiff
2020-08-19
Andres Noetzli
Require `--strings-exp` when using `str.substr` (#4916)
tree
|
commitdiff
2020-08-19
Gereon Kremer
Changes assertion (about maximum set cardinality) to...
tree
|
commitdiff
2020-08-19
Andres Noetzli
[Regressions] Do not test `--check-proofs` anymore...
tree
|
commitdiff
2020-08-19
Gereon Kremer
Fix SmtEngine::reset() (#4917)
tree
|
commitdiff
2020-08-17
Alex Ozdemir
Add identifier name for side condition. (#4902)
tree
|
commitdiff
2020-08-13
Andrew Reynolds
Split SmtSolver from SmtEngine (#4880)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Fixes for degenerate case of sygus decision tree learni...
tree
|
commitdiff
2020-08-12
makaimann
Add option to only build library (#4801)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Fix unsupported option in regress1. (#4874)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Split SmtEngineState from SmtEngine (#4855)
tree
|
commitdiff
2020-08-11
Andrew Reynolds
Update Expr-level unit tests that depend on datatypes...
tree
|
commitdiff
2020-08-11
Aina Niemetz
New C++ API: Remove redundant API functions for mkReal...
tree
|
commitdiff
2020-08-06
Andrew Reynolds
Updates not related to creation for eliminating Expr...
tree
|
commitdiff
2020-08-06
Andrew Reynolds
(proof-new) Refactor regular expression operation ...
tree
|
commitdiff
2020-08-05
Gereon Kremer
Improve error message for unsupported exponents (#4852)
tree
|
commitdiff
2020-08-04
Andrew Reynolds
Add API interface for specialized constructor term...
tree
|
commitdiff
2020-08-03
makaimann
Delete solver pointer in Cython __dealloc__ (#4799)
tree
|
commitdiff
2020-08-02
Andres Noetzli
Ensure strict length constraint for decompose rule...
tree
|
commitdiff
2020-08-01
Andrew Reynolds
Fix component contains for splicing due to substring...
tree
|
commitdiff
2020-08-01
yoni206
Add SyGuS Python API (#4812)
tree
|
commitdiff
2020-07-30
Andres Noetzli
Python API: Add support for sequences (#4757)
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Fix regular expression delta for complement (#4765)
tree
|
commitdiff
2020-07-28
yoni206
Supporting seq.nth (#4723)
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Use lemma property enum for OutputChannel::lemma (...
tree
|
commitdiff
2020-07-27
Alex Ozdemir
Consider negation's proof before triggering arith pfs...
tree
|
commitdiff
2020-07-21
Andrew Reynolds
Support uninterpreted constants in the evaluator (...
tree
|
commitdiff
2020-07-20
Alex Ozdemir
Fix a deadlock in the signature tests. (#4772)
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
Gereon Kremer
Integration of libpoly (#4679)
tree
|
commitdiff
2020-07-15
Andres Noetzli
Use Nodes for SmtEngine assertions (#4752)
tree
|
commitdiff
2020-07-15
Andres Noetzli
Use TypeNode in UninterpretedConstant (#4748)
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Fix regression output. (#4741)
tree
|
commitdiff
2020-07-14
Andres Noetzli
Use TypeNode in EmptySet (#4740)
tree
|
commitdiff
2020-07-14
Andrew Reynolds
Debug instantiations output (#4739)
tree
|
commitdiff
2020-07-14
Andres Noetzli
Fix caching in TheoryEngine::getExplanation() (#4736)
tree
|
commitdiff
2020-07-14
Andres Noetzli
Use TypeNode/Node in ArrayStoreAll (#4728)
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-13
Andrew Reynolds
Add support for string/sequence update (#4725)
tree
|
commitdiff
2020-07-11
yoni206
Changing bv_to_int options (#4721)
tree
|
commitdiff
2020-07-11
Andrew Reynolds
(proof-new) Update Theory interface for proof-new ...
tree
|
commitdiff
2020-07-10
Andrew Reynolds
Front end support for integer AND (#4717)
tree
|
commitdiff
2020-07-10
Andrew Reynolds
Ensure legal elimination for witness rewrite (#4688)
tree
|
commitdiff
2020-07-09
Andrew Reynolds
Disable unsat cores in timeout regression (#4713)
tree
|
commitdiff
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
tree
|
commitdiff
2020-07-06
Andrew Reynolds
Front end support for sequences (#4690)
tree
|
commitdiff
2020-07-02
Andrew Reynolds
Fix regression option (#4680)
tree
|
commitdiff
2020-07-01
Andres Noetzli
Add testing infrastructure for LFSC signatures (#4678)
tree
|
commitdiff
2020-06-30
Andrew Reynolds
Fix normal form for re.comp (#4676)
tree
|
commitdiff
2020-06-30
Andrew Reynolds
Simplify quantifiers strategy for when to apply last...
tree
|
commitdiff
2020-06-30
Ying Sheng
Interpolation step 1 (#4638)
tree
|
commitdiff
2020-06-29
Andres Noetzli
Make ExprManager constructor private (#4669)
tree
|
commitdiff
2020-06-29
makaimann
Python Sort tests (#4639)
tree
|
commitdiff
2020-06-29
Andres Noetzli
Fix memory leak in unit test node_algorithm_black ...
tree
|
commitdiff
2020-06-28
Andrew Reynolds
Fix non-termination issues in simpleRegExpConsume ...
tree
|
commitdiff
2020-06-27
Andres Noetzli
Add API for retrieving separation heap/nil term (#4663)
tree
|
commitdiff
2020-06-26
yoni206
fix and test (#4658)
tree
|
commitdiff
2020-06-24
Andres Noetzli
[unconstrained] Fix gathering of visited-once vars...
tree
|
commitdiff
2020-06-23
Mathias Preiner
Add support for eqrange predicate (#4562)
tree
|
commitdiff
2020-06-22
Andrew Reynolds
Add trascendental function kinds to list of unevaluated...
tree
|
commitdiff
2020-06-20
Alex Ozdemir
Use traversal iterators in IntToBv (#4169)
tree
|
commitdiff
2020-06-20
Abdalrhman Mohamed
Add Match utility function. (#4632)
tree
|
commitdiff
2020-06-19
Andrew Reynolds
Convert more uses of strings to words (#4584)
tree
|
commitdiff
2020-06-19
yoni206
Bv to int elimination bugfix (#4435)
tree
|
commitdiff
2020-06-19
Andres Noetzli
Add logic check for define-fun(s)-rec (#4577)
tree
|
commitdiff
2020-06-18
Andres Noetzli
Improve memory management in Java bindings (#4629)
tree
|
commitdiff
2020-06-17
Andrew Reynolds
Do not traverse WITNESS for partial substitutions in...
tree
|
commitdiff
2020-06-17
Haniel Barbosa
Improve polynomial anyterm grammar (#3566)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-06-16
Aina Niemetz
Add missing REQUIRES to new regressions. (#4625)
tree
|
commitdiff
2020-06-16
Aina Niemetz
BV: Fix querying equality status in lazy bit-blaster...
tree
|
commitdiff
2020-06-16
Aina Niemetz
Fix regressions in regress1 after #4613. (#4616)
tree
|
commitdiff
2020-06-15
Aina Niemetz
BV: Add missing type check for BITVECTOR_REPEAT_OP...
tree
|
commitdiff
2020-06-15
Aina Niemetz
BV: Add missing type check for INT_TO_BITVECTOR. (...
tree
|
commitdiff
2020-06-15
Andrew Reynolds
Do RE derivation inference only for concrete constant...
tree
|
commitdiff
2020-06-11
Andrew Reynolds
(proof-new) Remove arith-snorm option. (#4591)
tree
|
commitdiff
2020-06-10
Andres Noetzli
Add support for str.replace_re/str.replace_re_all ...
tree
|
commitdiff
2020-06-10
makaimann
Fix getKind for Python bindings (#4496)
tree
|
commitdiff
2020-06-08
Andres Noetzli
Fix ambiguous overload in unit test (#4582)
tree
|
commitdiff
2020-06-06
Andres Noetzli
Fix destruction order in NodeManager (#4578)
tree
|
commitdiff
2020-06-06
Andres Noetzli
Keep definitions when global-declarations enabled ...
tree
|
commitdiff
2020-06-06
Andrew Reynolds
Smt2 parsing support for nested recursive datatypes...
tree
|
commitdiff
2020-06-05
Andrew Reynolds
Datatypes with nested recursion are not handled in...
tree
|
commitdiff
2020-06-05
Andres Noetzli
Skip parse-error regression for comp builds (#4567)
tree
|
commitdiff
2020-06-05
Haniel Barbosa
Changing default language (#4561)
tree
|
commitdiff
next