projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2021-10-28
Gereon Kremer
Remove separate cpp docs for UnknownExplanation (#7516)
commit
|
commitdiff
|
tree
2021-10-28
Gereon Kremer
Build shared and static in CI (#7472)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Add missing API checks to getValue (#7475)
commit
|
commitdiff
|
tree
2021-10-27
Gereon Kremer
Add comments for arith type rules. (#7488)
commit
|
commitdiff
|
tree
2021-10-27
Gereon Kremer
Add documentation on output tags (#7499)
commit
|
commitdiff
|
tree
2021-10-27
Andres Noetzli
[Regression Script] Fix use of undefined variables...
commit
|
commitdiff
|
tree
2021-10-27
Gereon Kremer
Fix patching for poly on windows (#7513)
commit
|
commitdiff
|
tree
2021-10-27
Andres Noetzli
Require ITE branches to be first class types (#7508)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Fix care graph computation for higher-order (#7474)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Fix model unsoundness for relation join (#7511)
commit
|
commitdiff
|
tree
2021-10-27
yoni206
Python api documentation for sorts (#7440)
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Avoid non-terminating check with assumptions in strings...
commit
|
commitdiff
|
tree
2021-10-27
Andrew Reynolds
Deterministic variables for RE elim (#7489)
commit
|
commitdiff
|
tree
2021-10-27
mudathirmahgoub
Fix mac compile errors in sort.cpp (#7507)
commit
|
commitdiff
|
tree
2021-10-27
Gereon Kremer
Make --version exit (#7506)
commit
|
commitdiff
|
tree
2021-10-27
Gereon Kremer
Fix libpoly build on windows (#7502)
commit
|
commitdiff
|
tree
2021-10-26
Haniel Barbosa
[proofs] Fix singleton check in MACRO_RES post-processi...
commit
|
commitdiff
|
tree
2021-10-26
Haniel Barbosa
[proofs] Modularize check for whether a clause is singl...
commit
|
commitdiff
|
tree
2021-10-26
Haniel Barbosa
[proofs] Reset local var in SatProofManager since incre...
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Disable automatic symmetry in proofs of theory explanat...
commit
|
commitdiff
|
tree
2021-10-26
Haniel Barbosa
[proofs] Fix and simplify CHAIN_RESOLUTION checker...
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Add regressions for fixed issues (#7495)
commit
|
commitdiff
|
tree
2021-10-26
Andrew Reynolds
Disable sygus-inst when incremental (#7485)
commit
|
commitdiff
|
tree
2021-10-26
Lachnitt
[proofs] Alethe: Translate Block of clause pattern...
commit
|
commitdiff
|
tree
2021-10-26
Lachnitt
[proofs] Alethe: Translate AND_INTRO rule (#7405)
commit
|
commitdiff
|
tree
2021-10-26
Lachnitt
[proofs] Alethe: Translate AND_ELIM rule (#7404)
commit
|
commitdiff
|
tree
2021-10-26
Lachnitt
[proofs] Alethe: Translate CONTRA rule (#7403)
commit
|
commitdiff
|
tree
2021-10-26
Gereon Kremer
Upload docs for tags to docs-releases (#7415)
commit
|
commitdiff
|
tree
2021-10-26
Gereon Kremer
Fix frequent rebuild of options target (#7450)
commit
|
commitdiff
|
tree
2021-10-26
Gereon Kremer
Fix Configuration::isStaticBuild (#7456)
commit
|
commitdiff
|
tree
2021-10-26
Lachnitt
[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)
commit
|
commitdiff
|
tree
2021-10-25
Lachnitt
[proofs] Alethe: Translate MODUS_PONENS rule (#7401)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Add new method for enumerating unsat queries with SyGuS...
commit
|
commitdiff
|
tree
2021-10-25
Lachnitt
[proofs] Alethe: Translate EQ_RESOLVE rule (#7400)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Fix spurious checks to closed proofs (#7484)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Java and python unit tests for mkCardinalityConstraint...
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Fix more missing uses of CDProof::isSame (#7491)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Fix support for global declarations (#7480)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Remove HOL/fmf bound messages in set defaults (#7487)
commit
|
commitdiff
|
tree
2021-10-25
mudathirmahgoub
Add inference for count map (#7264)
commit
|
commitdiff
|
tree
2021-10-25
Andrew Reynolds
Reenable proofs on some regressions (#7483)
commit
|
commitdiff
|
tree
2021-10-25
Lachnitt
[proofs] Alethe: Translate SPLIT rule (#7399)
commit
|
commitdiff
|
tree
2021-10-25
Andres Noetzli
[Regression Script] Support older Python versions ...
commit
|
commitdiff
|
tree
2021-10-24
mudathirmahgoub
Delete redundant file option_Info.cpp (#7477)
commit
|
commitdiff
|
tree
2021-10-24
Andrew Reynolds
Add new eager conflict detection in strings for integer...
commit
|
commitdiff
|
tree
2021-10-23
Andrew Reynolds
Remove spurious assertoin (#7458)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Add requires libpoly to regression (#7467)
commit
|
commitdiff
|
tree
2021-10-22
mudathirmahgoub
Refactor java package name from cvc5 to io.github.cvc5...
commit
|
commitdiff
|
tree
2021-10-22
Gereon Kremer
Remove options::X__name (#7414)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Remove stale pointer to proof node manager from skolemi...
commit
|
commitdiff
|
tree
2021-10-22
Haniel Barbosa
[proof] Fixing CHAIN_RESOLUTION checker (#7465)
commit
|
commitdiff
|
tree
2021-10-22
Gereon Kremer
Fix out-of-sync pruning in CDCAC proofs (#7470)
commit
|
commitdiff
|
tree
2021-10-22
Gereon Kremer
Fix another double negation proof issue (#7468)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Remove `--uf-ho` option (#7463)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Fix symmetry issue in theory engine conflicts (#7469)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Add more abduction regressions (#7461)
commit
|
commitdiff
|
tree
2021-10-22
Lachnitt
[proofs] Alethe: Translate FACTORING rule (#7398)
commit
|
commitdiff
|
tree
2021-10-22
Lachnitt
[proofs] Alethe: Translate CHAIN_RESOLUTION rule (...
commit
|
commitdiff
|
tree
2021-10-22
Gereon Kremer
Make CAD proofs user context dependent (#7466)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Refactor theory inference manager constructor (#7457)
commit
|
commitdiff
|
tree
2021-10-22
yoni206
Making `IntBlaster` inherit from `EnvObj` (#7431)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Do not use global proxy variable attribute for strings...
commit
|
commitdiff
|
tree
2021-10-22
Andres Noetzli
Fix memory management of `ErrorInformation` (#7388)
commit
|
commitdiff
|
tree
2021-10-22
mudathirmahgoub
Add missing methods to Solver.java (#7299)
commit
|
commitdiff
|
tree
2021-10-22
Andrew Reynolds
Make expression mining use configurable options and...
commit
|
commitdiff
|
tree
2021-10-21
Aina Niemetz
docs: Use light gray for background on the right. ...
commit
|
commitdiff
|
tree
2021-10-21
Gereon Kremer
Also fix case of negated ite (#7454)
commit
|
commitdiff
|
tree
2021-10-21
Gereon Kremer
Fix symmetric proof issue for ITE in circuit propagator...
commit
|
commitdiff
|
tree
2021-10-21
Andrew Reynolds
Split utilites from CEGIS core connective module (...
commit
|
commitdiff
|
tree
2021-10-21
Andres Noetzli
[Regression Script] Fix printing of error diff (#7451)
commit
|
commitdiff
|
tree
2021-10-21
Haniel Barbosa
[proofs] Fix open proof in SAT solver due to cycles...
commit
|
commitdiff
|
tree
2021-10-21
Gereon Kremer
Add regression (#7447)
commit
|
commitdiff
|
tree
2021-10-21
Gereon Kremer
Fix incorrect proof from ITE in circuit propagator...
commit
|
commitdiff
|
tree
2021-10-21
Andres Noetzli
Refactor regressions script (#7249)
commit
|
commitdiff
|
tree
2021-10-21
Andrew Reynolds
Make cardinality constraint a nullary operator (#7333)
commit
|
commitdiff
|
tree
2021-10-21
Gereon Kremer
Working on windows builds (#7381)
commit
|
commitdiff
|
tree
2021-10-21
Gereon Kremer
Add setup to generate graphs for cmake target dependenc...
commit
|
commitdiff
|
tree
2021-10-21
Andres Noetzli
Enable and fix dump test (#7387)
commit
|
commitdiff
|
tree
2021-10-21
Gereon Kremer
Fix (#7437)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Enable some previously failing regressions (#7434)
commit
|
commitdiff
|
tree
2021-10-20
Gereon Kremer
Fix docs upload (again) (#7435)
commit
|
commitdiff
|
tree
2021-10-20
Aina Niemetz
api: Add Solver::mkSepEmp(). (#7432)
commit
|
commitdiff
|
tree
2021-10-20
Aina Niemetz
api: Improve documentation for special cases with nulla...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Move variadic trie utility to its own file (#7410)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Add regressions for fixed issues (#7421)
commit
|
commitdiff
|
tree
2021-10-20
yoni206
Add `isNull` and `isUpdater` to `Sort` class of python...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Throw exception if checking model with separation logic...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Check for higher-order variables in TheoryUF::ppRewrite...
commit
|
commitdiff
|
tree
2021-10-20
Gereon Kremer
Fix inadvertent failure of workflow step (#7420)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Eliminate last static calls to rewriter from smt layer...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Make SyGuS solver robust to non-closed enumerable sorts...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Do not construct instantiation for checking propagating...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Check whether abduct option is enabled (#7418)
commit
|
commitdiff
|
tree
2021-10-20
Aina Niemetz
api: Rename get(BV|FP)*Size functions for consistency...
commit
|
commitdiff
|
tree
2021-10-20
Lachnitt
[proofs] Alethe: Documentation on Translation (#7394)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Add LFSC signature for n-ary programs (#7360)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Use codatatype bound variables for codatatype values...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Reimplement support for relational triggers (#7063)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Do not make assumption about model for Boolean variable...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Correctly parse uninterpreted constant values in get...
commit
|
commitdiff
|
tree
next