projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2018-03-26
Andres Noetzli
Add support for filtering regressions with regex (...
commit
|
commitdiff
|
tree
2018-03-26
Andres Noetzli
Fix memory leak in bvminisat (#1710)
commit
|
commitdiff
|
tree
2018-03-26
Andres Noetzli
Make Java bindings work with newer build envs (#1709)
commit
|
commitdiff
|
tree
2018-03-26
Andres Noetzli
Add reasoning for inequalities in str rewriter (#1713)
commit
|
commitdiff
|
tree
2018-03-26
Andrew Reynolds
Synth-check and accelerate options for sygus-rr (#1691)
commit
|
commitdiff
|
tree
2018-03-26
Andrew Reynolds
Abort when sygus-verify finds unsoundness. (#1717)
commit
|
commitdiff
|
tree
2018-03-26
Andres Noetzli
Rewrites for substr of strings of length one (#1712)
commit
|
commitdiff
|
tree
2018-03-26
Andrew Reynolds
Check model only when sat (#1694)
commit
|
commitdiff
|
tree
2018-03-25
Andrew Reynolds
Cleanup various exit calls (#1692)
commit
|
commitdiff
|
tree
2018-03-25
Mathias Preiner
Remove doc/libcvc4.3 from options/Makefile.am. (#1696)
commit
|
commitdiff
|
tree
2018-03-23
Andrew Reynolds
Add a few quantifiers regressions to improve coverage...
commit
|
commitdiff
|
tree
2018-03-23
Andrew Reynolds
Remove abstract regular expression constant (#1698)
commit
|
commitdiff
|
tree
2018-03-23
Andrew Reynolds
Remove unused code (#1700)
commit
|
commitdiff
|
tree
2018-03-23
Andrew Reynolds
Minor reorganization for ematching (#1701)
commit
|
commitdiff
|
tree
2018-03-23
Andrew Reynolds
Enable post-condition strenghtening by default for...
commit
|
commitdiff
|
tree
2018-03-22
Mathias Preiner
Ignore whitespaces and moved code for contrib/get-authors.
commit
|
commitdiff
|
tree
2018-03-21
Andres Noetzli
Fix 'make regress' (#1683)
commit
|
commitdiff
|
tree
2018-03-21
Mathias Preiner
Refactor mkoptions (#1631)
commit
|
commitdiff
|
tree
2018-03-21
Aina Niemetz
Add bit-vector extract example. (#1681)
commit
|
commitdiff
|
tree
2018-03-21
Andrew Reynolds
More rewrites for indexof (#1648)
commit
|
commitdiff
|
tree
2018-03-21
Andres Noetzli
Move regression tests to single Makefile.am (#1658)
commit
|
commitdiff
|
tree
2018-03-21
Andres Noetzli
Fix various regression tests (#1657)
commit
|
commitdiff
|
tree
2018-03-21
Andrew Reynolds
Fix for string disequality processing (#1679)
commit
|
commitdiff
|
tree
2018-03-20
Mathias Preiner
Add support for CaDiCaL as eager BV SAT solver. (#1675)
commit
|
commitdiff
|
tree
2018-03-20
Andrew Reynolds
Minor refactor datatypes sygus (#1673)
commit
|
commitdiff
|
tree
2018-03-20
Andrew Reynolds
Internally remove redundant assertions and infer equali...
commit
|
commitdiff
|
tree
2018-03-20
Andrew Reynolds
Fix datatype dump regression. (#1672)
commit
|
commitdiff
|
tree
2018-03-20
Andrew Reynolds
Minor fix and addition to sygus sampler (#1678)
commit
|
commitdiff
|
tree
2018-03-20
Aina Niemetz
Add parameterized datatypes example. (#1676)
commit
|
commitdiff
|
tree
2018-03-20
yoni206
correct instruction for running example (#1669)
commit
|
commitdiff
|
tree
2018-03-20
Andrew Reynolds
Enable CEGQI for non-linear (#1674)
commit
|
commitdiff
|
tree
2018-03-19
Andrew Reynolds
Document inferences for strings (#1642)
commit
|
commitdiff
|
tree
2018-03-13
Mathias Preiner
Use Cryptominisat version 5.0.2 (instead of 4.2.0)...
commit
|
commitdiff
|
tree
2018-03-13
Aina Niemetz
SmtEngine::getModel() is now public. (#1665)
commit
|
commitdiff
|
tree
2018-03-09
Aina Niemetz
Printers are now managed as unique_ptr (fix mem leak...
commit
|
commitdiff
|
tree
2018-03-09
Aina Niemetz
Some minor cleanup in bv::utils. (#1663)
commit
|
commitdiff
|
tree
2018-03-09
Aina Niemetz
Add support for SMT-LIB v2.5 command get-unsat-assumpti...
commit
|
commitdiff
|
tree
2018-03-09
Andres Noetzli
Skip (get-unsat-assumptions) tests not supported (...
commit
|
commitdiff
|
tree
2018-03-09
Mathias Preiner
Cleanup Cryptominisat SAT wrapper. (#1652)
commit
|
commitdiff
|
tree
2018-03-09
Aina Niemetz
Fixed message in get-antlr script.
commit
|
commitdiff
|
tree
2018-03-09
Mathias Preiner
Fix Travis for unit test compilation errors. (#1651)
commit
|
commitdiff
|
tree
2018-03-07
Mathias Preiner
Make statistics output consistent. (#1647)
commit
|
commitdiff
|
tree
2018-03-06
Andrew Reynolds
Simplify initialization of quantifiers engine (#1641)
commit
|
commitdiff
|
tree
2018-03-06
Andrew Reynolds
Refactor symmetry breaking in datatypes sygus (#1640)
commit
|
commitdiff
|
tree
2018-03-06
Andres Noetzli
Remove printf from output utilities (#1629)
commit
|
commitdiff
|
tree
2018-03-06
Andrew Reynolds
Update semantics for string indexof and replace (#1630)
commit
|
commitdiff
|
tree
2018-03-05
Mathias Preiner
Fix boost url in contrib/get-win-dependencies.
commit
|
commitdiff
|
tree
2018-03-05
Mathias Preiner
Enable -Wsuggest-override by default. (#1643)
commit
|
commitdiff
|
tree
2018-03-05
Andrew Reynolds
Fix for sampler. (#1639)
commit
|
commitdiff
|
tree
2018-03-05
Aina Niemetz
Add support for check-sat-assuming. (#1637)
commit
|
commitdiff
|
tree
2018-03-05
Aina Niemetz
Add CVC4_PUBLIC keyword to overloads of << for Expr...
commit
|
commitdiff
|
tree
2018-03-05
Aina Niemetz
Add uniform way to serialize containers of Expr to...
commit
|
commitdiff
|
tree
2018-03-02
Aina Niemetz
Fixed typo.
commit
|
commitdiff
|
tree
2018-03-02
Andrew Reynolds
Optimization for sygus streaming mode (#1636)
commit
|
commitdiff
|
tree
2018-03-02
Andrew Reynolds
Simplify sygus wrt miniscoping (#1634)
commit
|
commitdiff
|
tree
2018-03-02
Aina Niemetz
Fixed comments in smt_engine.h.
commit
|
commitdiff
|
tree
2018-03-02
Andrew Reynolds
Print candidate rewrites in terms of original grammar...
commit
|
commitdiff
|
tree
2018-03-02
Andrew Reynolds
Create infrastructure for sygus modules (#1632)
commit
|
commitdiff
|
tree
2018-02-28
Aina Niemetz
SmtEngine::getAssignment now returns a vector of assign...
commit
|
commitdiff
|
tree
2018-02-28
Andrew Reynolds
Minor fixes for rec-fun (#1616)
commit
|
commitdiff
|
tree
2018-02-28
Aina Niemetz
Remove unused code in pushDefineFunRecScop in smt2...
commit
|
commitdiff
|
tree
2018-02-27
Andrew Reynolds
Improve rewriter for string indexof (#1592)
commit
|
commitdiff
|
tree
2018-02-27
Andrew Reynolds
Option to not use partial function semantics for arithm...
commit
|
commitdiff
|
tree
2018-02-27
Andrew Reynolds
Improvements to sygus sampling (#1621)
commit
|
commitdiff
|
tree
2018-02-24
Andres Noetzli
Add unit tests for BitVector, minor BV rewrite fix...
commit
|
commitdiff
|
tree
2018-02-23
Aina Niemetz
Split and document bitvector.h. (#1615)
commit
|
commitdiff
|
tree
2018-02-23
Andrew Reynolds
Fix cd-simplification for strings (#1624)
commit
|
commitdiff
|
tree
2018-02-22
Andrew Reynolds
Minor improvements to string rewriter (#1572)
commit
|
commitdiff
|
tree
2018-02-22
Aina Niemetz
Fixed disabling the BV equality slicer for quantifiers...
commit
|
commitdiff
|
tree
2018-02-22
Aina Niemetz
Disable BV equality slicer if not pure QF_BV. (#1619)
commit
|
commitdiff
|
tree
2018-02-20
Aina Niemetz
Improve documentation of bv::utils::isCoreTerm (#1617)
commit
|
commitdiff
|
tree
2018-02-20
Aina Niemetz
Moved and simplified bv::utils::intersect. (#1614)
commit
|
commitdiff
|
tree
2018-02-20
Andrew Reynolds
Minor fixes and additions for transcendental functions...
commit
|
commitdiff
|
tree
2018-02-20
Aina Niemetz
Unrecursified and merged bv::utils::is(Core|Equality...
commit
|
commitdiff
|
tree
2018-02-17
Aina Niemetz
bv::utils::mk(And|Or) Do not return true if size of...
commit
|
commitdiff
|
tree
2018-02-16
Aina Niemetz
Make regress1 default, only test regress0 on Travis...
commit
|
commitdiff
|
tree
2018-02-16
Aina Niemetz
Removed bv::utils::mkConjunction (redundant). (#1610)
commit
|
commitdiff
|
tree
2018-02-15
Andrew Reynolds
Fix corner case for rewrite of mult by pow 2 (#1601)
commit
|
commitdiff
|
tree
2018-02-15
Andrew Reynolds
Refactor regressions (#1581)
commit
|
commitdiff
|
tree
2018-02-15
Andres Noetzli
Fix context memory manager unit test (#1609)
commit
|
commitdiff
|
tree
2018-02-14
Andrew Reynolds
Quantifiers subdirectories (#1608)
commit
|
commitdiff
|
tree
2018-02-14
Andres Noetzli
Remove unused cd_set_collection.h (#1606)
commit
|
commitdiff
|
tree
2018-02-14
Aina Niemetz
Provide a uniform way to serialize node containers...
commit
|
commitdiff
|
tree
2018-02-13
Aina Niemetz
Moved (unrecursified) bv::utils::collectVars. (#1602)
commit
|
commitdiff
|
tree
2018-02-13
Aina Niemetz
Skip header for determining top contributors list....
commit
|
commitdiff
|
tree
2018-02-13
Andrew Reynolds
Option to use extended rewriter as a preprocessing...
commit
|
commitdiff
|
tree
2018-02-12
Andrew Reynolds
Minor improvements to sygus sampler (#1598)
commit
|
commitdiff
|
tree
2018-02-11
Aina Niemetz
Move (unrecursified) bv::utils::numNodes to lazy_bitbla...
commit
|
commitdiff
|
tree
2018-02-11
Andrew Reynolds
More minor improvements to synth-rr (#1597)
commit
|
commitdiff
|
tree
2018-02-10
Aina Niemetz
Move BitVector specific funs from bv::utils to util...
commit
|
commitdiff
|
tree
2018-02-10
Aina Niemetz
Remove mkNode from bv::utils (#1587)
commit
|
commitdiff
|
tree
2018-02-09
Tim King
Removing an always true comparison (unsigned) >= 0u...
commit
|
commitdiff
|
tree
2018-02-09
Andrew Reynolds
Class to reduce printing of redundant candidate rewrite...
commit
|
commitdiff
|
tree
2018-02-09
Tim King
Renaming CHECK to CVC4_CHECK. This avoids name collisio...
commit
|
commitdiff
|
tree
2018-02-09
Tim King
Replacing an incorrect reference to an injected class...
commit
|
commitdiff
|
tree
2018-02-09
Andres Noetzli
Replace CMM flag with debug CMM flag, fix leak in debug...
commit
|
commitdiff
|
tree
2018-02-09
Tim King
Inlining line_buffered_input to avoid warning about...
commit
|
commitdiff
|
tree
2018-02-08
Aina Niemetz
Clean up bv utils (part one). (#1580)
commit
|
commitdiff
|
tree
2018-02-08
Tim King
Adding virtual destructors on classes with virtual...
commit
|
commitdiff
|
tree
2018-02-08
Andrew Reynolds
Minor improvements to sygus sampling. (#1577)
commit
|
commitdiff
|
tree
next