projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2022-05-11
Andrew Reynolds
Relax an assertion in the evaluator (#8751)
commit
|
commitdiff
|
tree
2022-05-10
Gereon Kremer
Ensure substitutions in nonlinear solver are properly...
commit
|
commitdiff
|
tree
2022-05-10
Gereon Kremer
Fix some issues with the Python API tests (#8746)
commit
|
commitdiff
|
tree
2022-05-10
Gereon Kremer
Add test coverage for almost everything from the Java...
commit
|
commitdiff
|
tree
2022-05-10
Gereon Kremer
Compress debug symbols to make libcvc5 smaller (#8743)
commit
|
commitdiff
|
tree
2022-05-09
Andrew Reynolds
Improvements for evaluation in model (#8738)
commit
|
commitdiff
|
tree
2022-05-09
Andrew Reynolds
Do not depend on subtyping for APPLY_UF in TPTP parser...
commit
|
commitdiff
|
tree
2022-05-09
Andrew Reynolds
Add unit tests for getInstantiations (#8741)
commit
|
commitdiff
|
tree
2022-05-07
Andrew Reynolds
Do not rely on subtyping in real-to-int preprocessing...
commit
|
commitdiff
|
tree
2022-05-07
Abdalrhman...
Disable proof testers for delicate regressions. (#8735)
commit
|
commitdiff
|
tree
2022-05-07
Andrew Reynolds
More preparation for strict type rules (#8733)
commit
|
commitdiff
|
tree
2022-05-07
Andrew Reynolds
Fix proofs for ppAssert for theory Bool (#8708)
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Fallback for sequential substitution proof reconstructi...
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Eliminate arithmetic subtyping for (dis)equalities...
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Separate ill-typed portion of arith models (#8734)
commit
|
commitdiff
|
tree
2022-05-06
Andrew Reynolds
Fix LFSC side condition for matching premise of concat_...
commit
|
commitdiff
|
tree
2022-05-05
Gereon Kremer
Add test coverage for almost everything from the Python...
commit
|
commitdiff
|
tree
2022-05-05
Andrew Reynolds
Preparation for making equality strictly typed (#8728)
commit
|
commitdiff
|
tree
2022-05-05
Andrew Reynolds
Fix cache in learned rewrite preprocessing pass (#8725)
commit
|
commitdiff
|
tree
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
next