projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2022-05-05
Andrew Reynolds
Fix more issues with subtypes in regressions (#8727)
commit
|
commitdiff
|
tree
2022-05-05
mudathirmahgoub
Add operators table.aggr and table.join (#8681)
commit
|
commitdiff
|
tree
2022-05-05
Andrew Reynolds
Use purification for set comprehension reduction (...
commit
|
commitdiff
|
tree
2022-05-04
Andres Noetzli
Improve finding Python library/includes (#8718)
commit
|
commitdiff
|
tree
2022-05-04
yoni206
fix link to `Testing cvc5` in `INSTALL.md` (#8675)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Make equality solver the entry point for all equality...
commit
|
commitdiff
|
tree
2022-05-04
Gereon Kremer
Make printStatisticsSafe public (#8721)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Add declareOracleFun interface to SolverEngine (#8622)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Refactor oracles using new std::function backend (...
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Remove unecessary calls to equality engine from congrue...
commit
|
commitdiff
|
tree
2022-05-04
Gereon Kremer
Remove obsolete private methods from API (#8716)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Fix rewrite for to_real in division by zero (#8714)
commit
|
commitdiff
|
tree
2022-05-04
Andrew Reynolds
Add support for oracle constant nodes (#8707)
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Fix LFSC node converter for 0-ary tuples (#8706)
commit
|
commitdiff
|
tree
2022-05-03
Andres Noetzli
Update LFSC version (#8713)
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Use (non-recursive) unpurified form instead of original...
commit
|
commitdiff
|
tree
2022-05-03
Aina Niemetz
docs: Some fixes in options docs. (#8710)
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Change option name for mbqi in fmf (#8701)
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Simplify representation of datatypes at the TypeNode...
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Final preparation for CONST_INTEGER (#8700)
commit
|
commitdiff
|
tree
2022-05-03
Andrew Reynolds
Migrate basic EqualityEngine management from Congruence...
commit
|
commitdiff
|
tree
2022-05-02
Amalee Wilson
Add strict-cube and decision-trail partitioning strateg...
commit
|
commitdiff
|
tree
2022-05-02
Andrew Reynolds
More robust treatment of flattening in arith rewriter...
commit
|
commitdiff
|
tree
2022-05-02
Andrew Reynolds
Make arith msum utility agnostic to Int (#8694)
commit
|
commitdiff
|
tree
2022-05-02
Gereon Kremer
Add missing tests for some corners of the API (#8688)
commit
|
commitdiff
|
tree
2022-05-02
Aina Niemetz
docs: Do not use explicit line numbers in literalinclud...
commit
|
commitdiff
|
tree
2022-05-02
Andrew Reynolds
Further refactoring in preparation for CONST_INTEGER...
commit
|
commitdiff
|
tree
2022-05-02
Andrew Reynolds
Fix tuple printing in LFSC (#8696)
commit
|
commitdiff
|
tree
2022-04-29
Andrew Reynolds
Properly represent Tuples in the TypeNode AST (#8648)
commit
|
commitdiff
|
tree
2022-04-29
Andres Noetzli
Add simple type rule for real-or-int arguments (#8685)
commit
|
commitdiff
|
tree
2022-04-29
Gereon Kremer
Replace mkConst(CONST_RATIONAL) by mkConstReal (#8686)
commit
|
commitdiff
|
tree
2022-04-29
Andrew Reynolds
Towards proper usage of TO_REAL (#8680)
commit
|
commitdiff
|
tree
2022-04-29
Andres Noetzli
Document non-standard string operators (#8679)
commit
|
commitdiff
|
tree
2022-04-29
Andrew Reynolds
Ensure mkConstInt is used on integral rationals only...
commit
|
commitdiff
|
tree
2022-04-29
Andrew Reynolds
Refactor interfaces for E-matching (#8665)
commit
|
commitdiff
|
tree
2022-04-29
Andrew Reynolds
Make extended rewriter use standard Subs utility (...
commit
|
commitdiff
|
tree
2022-04-29
Abdalrhman...
Add an option to enable all testers. (#8676)
commit
|
commitdiff
|
tree
2022-04-29
yoni206
Add missing parenthesis for bags documentation (#8673)
commit
|
commitdiff
|
tree
2022-04-29
Gereon Kremer
Add unit test for code not exposed by java API (#8678)
commit
|
commitdiff
|
tree
2022-04-29
Gereon Kremer
Add unit test for code not exposed by python API (...
commit
|
commitdiff
|
tree
2022-04-29
Gereon Kremer
Add some missing API tests (#8669)
commit
|
commitdiff
|
tree
2022-04-28
Gereon Kremer
Move tests around (#8670)
commit
|
commitdiff
|
tree
2022-04-28
yoni206
int-blaster: not allowing higher order functions (...
commit
|
commitdiff
|
tree
2022-04-28
Andrew Reynolds
Move datatype split inference scheme to its own method...
commit
|
commitdiff
|
tree
2022-04-28
Andrew Reynolds
Clean code for datatypes split (#8667)
commit
|
commitdiff
|
tree
2022-04-28
Andrew Reynolds
Make labelled separation logic asserts preserve labels...
commit
|
commitdiff
|
tree
2022-04-28
Andrey Andreyevich...
Fix PyUnicode_AsWideCharString signature (#8522)
commit
|
commitdiff
|
tree
2022-04-28
Gereon Kremer
Add resource limiting to coverings solver (#8672)
commit
|
commitdiff
|
tree
2022-04-27
Andrew Reynolds
Add option to apply constant propagation for all learne...
commit
|
commitdiff
|
tree
2022-04-27
Andrew Reynolds
Refactoring of initial lemmas in datatypes (#8666)
commit
|
commitdiff
|
tree
2022-04-27
Andrew Reynolds
Minor improvements for entailment test (#8663)
commit
|
commitdiff
|
tree
2022-04-26
Andrew Reynolds
Minor improvements to quantifiers utilities (#8661)
commit
|
commitdiff
|
tree
2022-04-26
Andrew Reynolds
Make IndexTrie take nodes (#8649)
commit
|
commitdiff
|
tree
2022-04-26
Andrew Reynolds
Move rep set iterator to its own file (#8647)
commit
|
commitdiff
|
tree
2022-04-26
Andrew Reynolds
Refactor InstMatch (#8646)
commit
|
commitdiff
|
tree
2022-04-26
Andrew Reynolds
Refactor mkRep option for instantiation (#8657)
commit
|
commitdiff
|
tree
2022-04-26
Gereon Kremer
Add some missing resultants in the coverings solver...
commit
|
commitdiff
|
tree
2022-04-26
Andrew Reynolds
Simplify internal represenation of uninterpreted sorts...
commit
|
commitdiff
|
tree
2022-04-26
Andres Noetzli
Fix GMP cross-compilation when Wine installed (#8645)
commit
|
commitdiff
|
tree
2022-04-26
Andrew Reynolds
Simplify internal representation of instantiated sorts...
commit
|
commitdiff
|
tree
2022-04-25
Andres Noetzli
[Regressions] Use Wine for Windows builds (#8652)
commit
|
commitdiff
|
tree
2022-04-25
Andrew Reynolds
Move VTS term cache to term registry (#8656)
commit
|
commitdiff
|
tree
2022-04-25
Andrew Reynolds
Option exception for quantified bit-vectors + eager...
commit
|
commitdiff
|
tree
2022-04-25
Andrew Reynolds
Make BVInstantiatorUtil an EnvObj (#8633)
commit
|
commitdiff
|
tree
2022-04-25
Abdalrhman...
Add custom targets for specific testers. (#8653)
commit
|
commitdiff
|
tree
2022-04-23
Andrew Reynolds
Minor cleanup of NodeManager (#8650)
commit
|
commitdiff
|
tree
2022-04-22
Andrew Reynolds
Add `deep-restart` option (#8644)
commit
|
commitdiff
|
tree
2022-04-21
Abdalrhman...
Add tester for LFSC printer. (#8606)
commit
|
commitdiff
|
tree
2022-04-21
Andres Noetzli
[Seq] Remove `SkolemCache::mkSkolemSeqNth()` (#8643)
commit
|
commitdiff
|
tree
2022-04-21
mudathirmahgoub
Add bag.partition evaluation (#8637)
commit
|
commitdiff
|
tree
2022-04-20
Andrew Reynolds
Add utilities in preparation for deep restarts (#8642)
commit
|
commitdiff
|
tree
2022-04-20
Andres Noetzli
Remove unused `SEQ_NTH_TOTAL` kind (#8048)
commit
|
commitdiff
|
tree
2022-04-20
Andres Noetzli
Improve handling of `(push)` and `(pop)` (#8641)
commit
|
commitdiff
|
tree
2022-04-20
Andrew Reynolds
Add declare-oracle-fun command (#8621)
commit
|
commitdiff
|
tree
2022-04-20
Andrew Reynolds
Minor simplifications for datatype selector triggers...
commit
|
commitdiff
|
tree
2022-04-20
yoni206
int-blaster: direct support for bvcomp (#8640)
commit
|
commitdiff
|
tree
2022-04-20
yoni206
Remove redundant assertion in int-blaster (#8639)
commit
|
commitdiff
|
tree
2022-04-20
Andrew Reynolds
Updates to zero level learner (#8597)
commit
|
commitdiff
|
tree
2022-04-19
Andrew Reynolds
Avoid trivial equalities in explanation of SETS_CARD_CY...
commit
|
commitdiff
|
tree
2022-04-19
Andrew Reynolds
Simplify implementation of subtype methods in TypeNode...
commit
|
commitdiff
|
tree
2022-04-19
mudathirmahgoub
Add table.project evaluator (#8632)
commit
|
commitdiff
|
tree
2022-04-19
Andrew Reynolds
Move linear arithmetic solver to theory::arith::linear...
commit
|
commitdiff
|
tree
2022-04-19
Andrew Reynolds
Generalize concat conflict for sequences in LFSC (...
commit
|
commitdiff
|
tree
2022-04-18
Abdalrhman...
Remove instances of `check-proofs` in regressions....
commit
|
commitdiff
|
tree
2022-04-18
Andrew Reynolds
Add some missing FP symbols to LFSC (#8629)
commit
|
commitdiff
|
tree
2022-04-18
Andrew Reynolds
Distinguish name variants for types in LFSC node conver...
commit
|
commitdiff
|
tree
2022-04-18
Andrew Reynolds
Make more utilities distinguish Int and Real (#8626)
commit
|
commitdiff
|
tree
2022-04-18
Andrew Reynolds
Simplify management of separation logic heap (#8580)
commit
|
commitdiff
|
tree
2022-04-18
Andres Noetzli
Remove support for unused `declare-*` commands (#8623)
commit
|
commitdiff
|
tree
2022-04-14
Andrew Reynolds
Fix internal type issue for congruence over quantifiers...
commit
|
commitdiff
|
tree
2022-04-14
Andrew Reynolds
Implement internal support for (definitional) satisfiab...
commit
|
commitdiff
|
tree
2022-04-14
Andrew Reynolds
Make LFSC printer robust to internal types (#8616)
commit
|
commitdiff
|
tree
2022-04-14
Andrew Reynolds
Implement internal support for synthesis modulo oracles...
commit
|
commitdiff
|
tree
2022-04-14
Andrew Reynolds
Remove static calls to rewrite involving array constant...
commit
|
commitdiff
|
tree
2022-04-14
Andrew Reynolds
Improvements to phase shifting + purification lemmas...
commit
|
commitdiff
|
tree
2022-04-14
Amalee Wilson
Revised partitioning (#8143)
commit
|
commitdiff
|
tree
2022-04-14
vinciusb
[proofs] [dot] New way to traverse the proof when print...
commit
|
commitdiff
|
tree
2022-04-14
Andrew Reynolds
Integrate oracle checker into quantifiers term registry...
commit
|
commitdiff
|
tree
2022-04-14
Andrew Reynolds
Fix spurious assertion involving subtypes (#8611)
commit
|
commitdiff
|
tree
2022-04-14
Andrew Reynolds
Update LFSC version (#8614)
commit
|
commitdiff
|
tree
next