projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2020-07-27
Andrew Reynolds
(proof-new) Arithmetic operator elim proof producing...
commit
|
commitdiff
|
tree
2020-07-27
Alex Ozdemir
Consider negation's proof before triggering arith pfs...
commit
|
commitdiff
|
tree
2020-07-21
Aina Niemetz
GH Actions: Cancel builds on push, remove redundant...
commit
|
commitdiff
|
tree
2020-07-21
Andrew Reynolds
Support uninterpreted constants in the evaluator (...
commit
|
commitdiff
|
tree
2020-07-21
Gereon Kremer
Preparations for a CAD-based arithmetic solver (#4762)
commit
|
commitdiff
|
tree
2020-07-20
Alex Ozdemir
Fix a deadlock in the signature tests. (#4772)
commit
|
commitdiff
|
tree
2020-07-18
Haniel Barbosa
Improving equality engine tracing (#4770)
commit
|
commitdiff
|
tree
2020-07-18
Andrew Reynolds
(proof-new) Proof recording for assertions pipeline...
commit
|
commitdiff
|
tree
2020-07-18
Andrew Reynolds
Enumerate shapes feature in fast sygus enumerator ...
commit
|
commitdiff
|
tree
2020-07-17
Andres Noetzli
Add NodeManagerScopes to fix use-after-free issues...
commit
|
commitdiff
|
tree
2020-07-17
Andrew Reynolds
Replace options listener infrastructure (#4764)
commit
|
commitdiff
|
tree
2020-07-17
Andrew V. Jones
Support for using 'libedit' over 'readline' #4571 ...
commit
|
commitdiff
|
tree
2020-07-17
Andrew Reynolds
(proof-new) Updates to strings core solver (#4642)
commit
|
commitdiff
|
tree
2020-07-17
Andrew Reynolds
Add option manager and simpler option listener (#4745)
commit
|
commitdiff
|
tree
2020-07-17
Gereon Kremer
Integration of libpoly (#4679)
commit
|
commitdiff
|
tree
2020-07-17
Haniel Barbosa
Fix EqProof to ProofNode conversion (#4760)
commit
|
commitdiff
|
tree
2020-07-16
Haniel Barbosa
(proof-new) Implements the conversion between EqProof...
commit
|
commitdiff
|
tree
2020-07-16
Gereon Kremer
Resource manager cleanup (#4732)
commit
|
commitdiff
|
tree
2020-07-16
Andrew Reynolds
Split abstract values utility from SmtEngine (#4754)
commit
|
commitdiff
|
tree
2020-07-16
Andrew Reynolds
Make ExtTheory a utility and not a member of Theory...
commit
|
commitdiff
|
tree
2020-07-16
Gereon Kremer
Remove cumulative time limits and cpu time limits ...
commit
|
commitdiff
|
tree
2020-07-16
Gereon Kremer
Fixes memory leak when an exception goes through runCvc...
commit
|
commitdiff
|
tree
2020-07-16
Haniel Barbosa
(proof-new) Adding API for converting EqProof into...
commit
|
commitdiff
|
tree
2020-07-15
Andres Noetzli
Use Nodes for SmtEngine assertions (#4752)
commit
|
commitdiff
|
tree
2020-07-15
Andrew Reynolds
Split abduction solver from SmtEngine (#4733)
commit
|
commitdiff
|
tree
2020-07-15
Andres Noetzli
Use TypeNode in UninterpretedConstant (#4748)
commit
|
commitdiff
|
tree
2020-07-15
Gereon Kremer
Add missing header (Fixes #4743) (#4749)
commit
|
commitdiff
|
tree
2020-07-15
Andrew Reynolds
Simplify entailment check interface (#4744)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Make use of options in setDefaults more consistent...
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Remove sygus print callback (#4727)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Fix regression output. (#4741)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
(proof-new) Skeleton proof support in the Rewriter...
commit
|
commitdiff
|
tree
2020-07-14
Andres Noetzli
Use TypeNode in EmptySet (#4740)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Debug instantiations output (#4739)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Minor refactoring of subsolver initialization (#4731)
commit
|
commitdiff
|
tree
2020-07-14
Andres Noetzli
Fix caching in TheoryEngine::getExplanation() (#4736)
commit
|
commitdiff
|
tree
2020-07-14
Haniel Barbosa
Fix options messages that were inverted (#4734)
commit
|
commitdiff
|
tree
2020-07-14
Andres Noetzli
Use TypeNode/Node in ArrayStoreAll (#4728)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Fix type comparisons involving pointer. (#4738)
commit
|
commitdiff
|
tree
2020-07-14
Andrew Reynolds
Fix whitespace issue in instantiations output. (#4737)
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
(proof-new) SMT Preprocess proof generator (#4708)
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
User-facing print debug option for sygus candidates...
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
Statistics on instantiations per quantified formula...
commit
|
commitdiff
|
tree
2020-07-13
Gereon Kremer
Implement --tlimit for windows (#4716)
commit
|
commitdiff
|
tree
2020-07-13
Andrew Reynolds
Add support for string/sequence update (#4725)
commit
|
commitdiff
|
tree
2020-07-13
Andres Noetzli
Remove ExprSequence (#4724)
commit
|
commitdiff
|
tree
2020-07-11
Andrew Reynolds
Cache explanations in TheoryEngine::getExplanation...
commit
|
commitdiff
|
tree
2020-07-11
yoni206
Changing bv_to_int options (#4721)
commit
|
commitdiff
|
tree
2020-07-11
Haniel Barbosa
Adding test for whether a kind is n-ary (#4718)
commit
|
commitdiff
|
tree
2020-07-11
Andrew V. Jones
Add support for printing 'get-abduct' in verbose mode...
commit
|
commitdiff
|
tree
2020-07-11
Andrew Reynolds
(proof-new) Add ONCE and FIXPOINT modes for term conver...
commit
|
commitdiff
|
tree
2020-07-11
Andrew Reynolds
(proof-new) Update Theory interface for proof-new ...
commit
|
commitdiff
|
tree
2020-07-10
Andres Noetzli
Always Update Git information when rebuilding (#4696)
commit
|
commitdiff
|
tree
2020-07-10
Andrew Reynolds
Front end support for integer AND (#4717)
commit
|
commitdiff
|
tree
2020-07-10
Ying Sheng
[Interpolation] Add interface for SyGuS interpolation...
commit
|
commitdiff
|
tree
2020-07-10
Gereon Kremer
Add deps/install/lib to RPATH and warn user when using...
commit
|
commitdiff
|
tree
2020-07-10
Andrew Reynolds
Update competition scripts (#4715)
commit
|
commitdiff
|
tree
2020-07-10
Andrew Reynolds
Ensure legal elimination for witness rewrite (#4688)
commit
|
commitdiff
|
tree
2020-07-09
Andrew Reynolds
Disable unsat cores in timeout regression (#4713)
commit
|
commitdiff
|
tree
2020-07-09
Andrew Reynolds
Associate all lemmas in non-linear arithmetic with...
commit
|
commitdiff
|
tree
2020-07-09
Andrew Reynolds
(proof-new) Theory engine proof generator (#4657)
commit
|
commitdiff
|
tree
2020-07-08
Gereon Kremer
Re-implement handling of --tlimit (#4655)
commit
|
commitdiff
|
tree
2020-07-08
Mathias Preiner
Add getName() method to options. (#4704)
commit
|
commitdiff
|
tree
2020-07-08
Andrew Reynolds
Always interleave theory combination with quantifiers...
commit
|
commitdiff
|
tree
2020-07-08
Andrew Reynolds
Improve and fix secant and tangent lemmas in the transc...
commit
|
commitdiff
|
tree
2020-07-07
Andrew Reynolds
Transfer ownership of internal Options from NodeManager...
commit
|
commitdiff
|
tree
2020-07-07
Andrew V. Jones
Increase the minimum version of CMake due to the use...
commit
|
commitdiff
|
tree
2020-07-06
Andrew Reynolds
Front end support for sequences (#4690)
commit
|
commitdiff
|
tree
2020-07-06
Andres Noetzli
[GitHub] Add link to fuzzing guidelines in issues ...
commit
|
commitdiff
|
tree
2020-07-03
Andres Noetzli
Remove SWIG bindings (#4683)
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
Fix regression option (#4680)
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
(proof-new) Updates to skolem manager interface (...
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
(proof-new) Proof rule checkers run on skolem forms...
commit
|
commitdiff
|
tree
2020-07-02
Andrew Reynolds
(proof-new) Proof node updater (#4647)
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
Add solver for integer AND (#4681)
commit
|
commitdiff
|
tree
2020-07-01
Andres Noetzli
Add testing infrastructure for LFSC signatures (#4678)
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
Inferences and model construction taking into account...
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
(proof-new) Updates to evaluator (#4659)
commit
|
commitdiff
|
tree
2020-07-01
Andrew Reynolds
(proof-new) Improve rewriter for WITNESS (#4661)
commit
|
commitdiff
|
tree
2020-06-30
Andrew Reynolds
Fix normal form for re.comp (#4676)
commit
|
commitdiff
|
tree
2020-06-30
Andres Noetzli
Update NEWS post 1.8 release (#4666)
commit
|
commitdiff
|
tree
2020-06-30
Mathias Preiner
Fix GMP compilation for win64. (#4675)
commit
|
commitdiff
|
tree
2020-06-30
Andrew Reynolds
Simplify quantifiers strategy for when to apply last...
commit
|
commitdiff
|
tree
2020-06-30
Ying Sheng
Interpolation step 1 (#4638)
commit
|
commitdiff
|
tree
2020-06-30
Mathias Preiner
contrib: Update to GMP 6.2.0, compile static and shared...
commit
|
commitdiff
|
tree
2020-06-30
Andrew Reynolds
Add internal support for integer and operator (#4668)
commit
|
commitdiff
|
tree
2020-06-29
Andres Noetzli
Make ExprManager constructor private (#4669)
commit
|
commitdiff
|
tree
2020-06-29
makaimann
Python Sort tests (#4639)
commit
|
commitdiff
|
tree
2020-06-29
Andres Noetzli
Fix memory leak in unit test node_algorithm_black ...
commit
|
commitdiff
|
tree
2020-06-28
Andrew Reynolds
Fix non-termination issues in simpleRegExpConsume ...
commit
|
commitdiff
|
tree
2020-06-28
Alex Ozdemir
Proof Rules and Checker for Arithmetic (#4665)
commit
|
commitdiff
|
tree
2020-06-27
Andres Noetzli
Add API for retrieving separation heap/nil term (#4663)
commit
|
commitdiff
|
tree
2020-06-26
yoni206
fix and test (#4658)
commit
|
commitdiff
|
tree
2020-06-25
Andrew Reynolds
(proof-new) Add TrustNode interfaces to OutputChannel...
commit
|
commitdiff
|
tree
2020-06-25
Andrew Reynolds
Remove sygus1 parser (#4651)
commit
|
commitdiff
|
tree
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
next