projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2018-04-08
Andrew Reynolds
Allow predetermined first-order variables when construc...
commit
|
commitdiff
|
tree
2018-04-08
Andrew Reynolds
Check free variables in assertions (#1737)
commit
|
commitdiff
|
tree
2018-04-08
Andrew Reynolds
Do not introduce uinterpreted constants in TPTP parser...
commit
|
commitdiff
|
tree
2018-04-08
Andrew Reynolds
Add quantifier name attribute. (#1756)
commit
|
commitdiff
|
tree
2018-04-07
Aina Niemetz
Fixed get-authors.
commit
|
commitdiff
|
tree
2018-04-06
Arjun Viswanathan
Add define rec fun to cvc parser (#1738)
commit
|
commitdiff
|
tree
2018-04-06
Andres Noetzli
Python regression script (#1662)
commit
|
commitdiff
|
tree
2018-04-05
Mathias Preiner
Add more general SignExtendUltConst rewriting. (#1385)
commit
|
commitdiff
|
tree
2018-04-05
Andres Noetzli
Make Python bindings example compatible w/ Python3...
commit
|
commitdiff
|
tree
2018-04-05
Andres Noetzli
Update README for regression tests (#1746)
commit
|
commitdiff
|
tree
2018-04-04
Andrew Reynolds
Proper initialization and destruction of sygus unif...
commit
|
commitdiff
|
tree
2018-04-04
Andrew Reynolds
Fix for corner case of higher-order matching (#1708)
commit
|
commitdiff
|
tree
2018-04-04
Andrew Reynolds
Do not debug check models when unknown (#1748)
commit
|
commitdiff
|
tree
2018-04-04
Andrew Reynolds
Fix sygus infer (#1747)
commit
|
commitdiff
|
tree
2018-04-04
Andres Noetzli
Refactor IntToBV preprocessing pass (#1716)
commit
|
commitdiff
|
tree
2018-04-04
Andrew Reynolds
Option to turn arbitrary input into sygus (#1704)
commit
|
commitdiff
|
tree
2018-04-04
Andres Noetzli
[BVMiniSat] Avoid duplicates in conflicts (#1745)
commit
|
commitdiff
|
tree
2018-04-03
Andrew Reynolds
Make sygus unif I/O an subclass of sygus unif (#1741)
commit
|
commitdiff
|
tree
2018-04-03
Andrew Reynolds
Use choice when expanding definitions for inverse trans...
commit
|
commitdiff
|
tree
2018-04-03
Andrew Reynolds
Internal sygus type checking (#1734)
commit
|
commitdiff
|
tree
2018-04-03
Andrew Reynolds
Improvements to extended rewriter for Booleans and...
commit
|
commitdiff
|
tree
2018-04-02
Andrew Reynolds
Make sygus unif utility use sygus unif strategies ...
commit
|
commitdiff
|
tree
2018-04-02
yoni206
a formula should be an instance of itself (#1668)
commit
|
commitdiff
|
tree
2018-04-02
Clark Barrett
Remove references to nyu (#1721)
commit
|
commitdiff
|
tree
2018-04-02
Mathias Preiner
Reorganize bitblaster code. (#1695)
commit
|
commitdiff
|
tree
2018-04-02
yoni206
Do not call toString() on malformed node when throwing...
commit
|
commitdiff
|
tree
2018-03-30
Andrew Reynolds
Disable regression (#1731)
commit
|
commitdiff
|
tree
2018-03-30
Andrew Reynolds
Split strategy representation from SygusUnif (#1730)
commit
|
commitdiff
|
tree
2018-03-30
Andrew Reynolds
Do not use factoring inference for transcendental funct...
commit
|
commitdiff
|
tree
2018-03-29
Andrew Reynolds
Simplify sygus unif so that it is one-to-one with funct...
commit
|
commitdiff
|
tree
2018-03-27
Andrew Reynolds
Make sygus pbe use sygus unif utility (#1724)
commit
|
commitdiff
|
tree
2018-03-27
Andrew Reynolds
Fix for --sygus-rr-synth (#1723)
commit
|
commitdiff
|
tree
2018-03-27
Andrew Reynolds
Make sygus unif utility (#1720)
commit
|
commitdiff
|
tree
2018-03-27
Andrew Reynolds
Filter candidate rewrites based on matching (#1682)
commit
|
commitdiff
|
tree
2018-03-27
Andres Noetzli
Better normalization of string concatenation (#1719)
commit
|
commitdiff
|
tree
2018-03-27
Andrew Reynolds
Documentation and simplifications for PBE (#1677)
commit
|
commitdiff
|
tree
2018-03-26
Andres Noetzli
Regression level 0 for distcheck on Travis (#1714)
commit
|
commitdiff
|
tree
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
next