projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
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
2021-10-20
Abdalrhman...
Avoid escaping `double-quotes` twice. (#7409)
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Make proofs of rewrites robust to use in internal subso...
commit
|
commitdiff
|
tree
2021-10-20
Andrew Reynolds
Add basic regular expression type enumerator (#7416)
commit
|
commitdiff
|
tree
2021-10-19
Andrew Reynolds
Fix expected conclusion for EQ_RESOLVE when expanding...
commit
|
commitdiff
|
tree
2021-10-19
Andrew Reynolds
Support sequences of fixed finite cardinality (#7371)
commit
|
commitdiff
|
tree
2021-10-19
Andrew Reynolds
Fix issue related to sanity checking integer models...
commit
|
commitdiff
|
tree
2021-10-19
Gereon Kremer
Remove setDefaults methods (#7413)
commit
|
commitdiff
|
tree
2021-10-18
Andrew Reynolds
Add regression for fixed issue (#7395)
commit
|
commitdiff
|
tree
2021-10-18
Abdalrhman...
Move check for experimental arrays features to `theory_...
commit
|
commitdiff
|
tree
2021-10-18
Andres Noetzli
Update SMT-COMP script (#7389)
commit
|
commitdiff
|
tree
2021-10-15
yoni206
Python api documentation: Op, Grammar, Result, Enums...
commit
|
commitdiff
|
tree
2021-10-15
Andrew Reynolds
Add more regressions for fixed issues (#7382)
commit
|
commitdiff
|
tree
2021-10-15
Gereon Kremer
Have docs_upload properly upload tags. (#7352)
commit
|
commitdiff
|
tree
2021-10-15
Alex Ozdemir
Fix bad cast in the python API (#7359)
commit
|
commitdiff
|
tree
2021-10-15
Andrew Reynolds
Fix issues related to proofs of lemmas with duplicate...
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Add regressions for fixed issues (#7369)
commit
|
commitdiff
|
tree
2021-10-14
Gereon Kremer
Fix (get-info :authors) (#7373)
commit
|
commitdiff
|
tree
2021-10-14
Gereon Kremer
Improve ManagedStreams (#7367)
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Add regression for fixed issue (#7365)
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Improve parser for tuple select (#7364)
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Split entailment check from term database (#7342)
commit
|
commitdiff
|
tree
2021-10-14
Gereon Kremer
Also test older cmake versions (#7347)
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Fix quantifiers variable elimination for parametric...
commit
|
commitdiff
|
tree
2021-10-14
Gereon Kremer
Fix GLPK linking (#7357)
commit
|
commitdiff
|
tree
2021-10-14
Andrew Reynolds
Add core LFSC signatures (#7289)
commit
|
commitdiff
|
tree
2021-10-13
Andrew Reynolds
Eliminate uses of rewrite from datatypes theory (#7354)
commit
|
commitdiff
|
tree
2021-10-13
Andrew Reynolds
Make (proof) equality engine use Env (#7336)
commit
|
commitdiff
|
tree
2021-10-12
Andrew Reynolds
Simplify refinement in sygus solver (#7343)
commit
|
commitdiff
|
tree
2021-10-12
Andrew Reynolds
Eliminate calls to currentResourceManager (#7350)
commit
|
commitdiff
|
tree
2021-10-12
Mathias Preiner
cmake: Fix git info if build directory is outside of...
commit
|
commitdiff
|
tree
2021-10-12
Aina Niemetz
Clean up occurrences of SmtEngine in comments. (#7349)
commit
|
commitdiff
|
tree
2021-10-12
Aina Niemetz
Get rid of unused member d_smtStats in ExpandDefs....
commit
|
commitdiff
|
tree
2021-10-12
Aina Niemetz
Rename SmtEngineState to SolverEngineState. (#7344)
commit
|
commitdiff
|
tree
2021-10-12
Gereon Kremer
Fix glpk, add antlr.so (#7341)
commit
|
commitdiff
|
tree
2021-10-12
Andrew Reynolds
Provide a non-traversal interface to term formula remov...
commit
|
commitdiff
|
tree
2021-10-12
Andrew Reynolds
Minor cleaning of instantiation utilities (#7334)
commit
|
commitdiff
|
tree
2021-10-12
Andrew Reynolds
Simplify skolemization in sygus solver (#7331)
commit
|
commitdiff
|
tree
2021-10-12
Ouyancheng
fix deprecation of std::iterator (#7332)
commit
|
commitdiff
|
tree
2021-10-11
Mathias Preiner
Start post-release for 0.0.2
commit
|
commitdiff
|
tree
2021-10-11
Mathias Preiner
Bump version to 0.0.2
commit
|
commitdiff
|
tree
2021-10-11
Mathias Preiner
Fix release action.
commit
|
commitdiff
|
tree
2021-10-11
Aina Niemetz
Rename SmtEngineStatistics to SolverEngineStatistics...
commit
|
commitdiff
|
tree
2021-10-11
Mathias Preiner
Start post-release for 0.0.1
commit
|
commitdiff
|
tree
2021-10-11
Mathias Preiner
Bump version to 0.0.1
commit
|
commitdiff
|
tree
2021-10-11
Gereon Kremer
Antlr: runtime -> libraries (#7338)
commit
|
commitdiff
|
tree
next