projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2018-08-10
Andres Noetzli
Do not use static initialization in CxxTest runner...
commit
|
commitdiff
|
tree
2018-08-09
Andrew Reynolds
Fix char overflow issues in regular expression solver...
commit
|
commitdiff
|
tree
2018-08-09
Andres Noetzli
Fix documentation of regression tests (#2290)
commit
|
commitdiff
|
tree
2018-08-09
Aina Niemetz
Plug solver API object into parser. (#2240)
commit
|
commitdiff
|
tree
2018-08-09
Tim King
Fixing documentation nit from PR#2232. (#2289)
commit
|
commitdiff
|
tree
2018-08-08
Tim King
Proposal for adding map utility functions to CVC4...
commit
|
commitdiff
|
tree
2018-08-08
Andrew Reynolds
Disable argument relevance for sygus by default (#2288)
commit
|
commitdiff
|
tree
2018-08-08
Andrew Reynolds
Add debug test for sygus subcall verify calls. (#2287)
commit
|
commitdiff
|
tree
2018-08-08
Andrew Reynolds
Move uf model code from uf to quantifiers (#2095)
commit
|
commitdiff
|
tree
2018-08-08
Andrew Reynolds
Do beta-reduction in expandDefinitions (#2286)
commit
|
commitdiff
|
tree
2018-08-08
Andres Noetzli
Require Swig 3 (#2283)
commit
|
commitdiff
|
tree
2018-08-08
Andrew Reynolds
Simplify and improve the sygus parser (#2266)
commit
|
commitdiff
|
tree
2018-08-08
Andrew Reynolds
Document/refactor datatypes sygus simple symmetry break...
commit
|
commitdiff
|
tree
2018-08-08
Andrew Reynolds
Fix simple reg exp consume rewrite (#2281)
commit
|
commitdiff
|
tree
2018-08-08
Andres Noetzli
Delete functions instead of using CVC4_UNDEFINED (...
commit
|
commitdiff
|
tree
2018-08-07
Andrew Reynolds
Wait to do sygus qe preprocess until full effort check...
commit
|
commitdiff
|
tree
2018-08-07
Andrew Reynolds
Fix inference of pre and post conditions for non variab...
commit
|
commitdiff
|
tree
2018-08-07
Mathias Preiner
Make output of flushInformation and safeFlushInformatio...
commit
|
commitdiff
|
tree
2018-08-07
Aina Niemetz
Add rewrite for nested BITVECTOR_ITE that can be merged...
commit
|
commitdiff
|
tree
2018-08-07
Andrew Reynolds
Make flat form inferences optional in strings (#2277)
commit
|
commitdiff
|
tree
2018-08-07
Andrew Reynolds
Add RegLan to smt2/sygus parsers. (#2276)
commit
|
commitdiff
|
tree
2018-08-07
Andrew Reynolds
Move sygus quantifier elimination step for non-ground...
commit
|
commitdiff
|
tree
2018-08-07
Andrew Reynolds
Remove support for Enum sygus syntax. (#2264)
commit
|
commitdiff
|
tree
2018-08-06
Andrew Reynolds
Fixes for sygus inference (#2238)
commit
|
commitdiff
|
tree
2018-08-06
Andrew Reynolds
Fixes and improvements for single invocation inference...
commit
|
commitdiff
|
tree
2018-08-06
Andrew Reynolds
Fix degenerate case of sygus grammar construction for...
commit
|
commitdiff
|
tree
2018-08-04
Aina Niemetz
Add rewrite for nested BITVECTOR_ITE with cond_outer...
commit
|
commitdiff
|
tree
2018-08-04
Aina Niemetz
Add rewrite for BITVECTOR_ITE with const children....
commit
|
commitdiff
|
tree
2018-08-03
Aina Niemetz
Add rewrite for BITVECTOR_ITE with term_then == term_el...
commit
|
commitdiff
|
tree
2018-08-03
Andrew Reynolds
Eliminate option for sygus UF evaluation functions...
commit
|
commitdiff
|
tree
2018-08-03
Mathias Preiner
Fix printing statistics in case of signals. (#2267)
commit
|
commitdiff
|
tree
2018-08-03
Aina Niemetz
Add timer for BV inequality solver. (#2265)
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Parse standard separation logic inputs (#2257)
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Improve CEGQI heuristics involving equality and multipl...
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Fix candidate rewrite utilities for non-first-class...
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Make strings robust to regular expression variables...
commit
|
commitdiff
|
tree
2018-08-02
Aina Niemetz
Add rewrites for BITVECTOR_ITE and BITVECTOR_COMP with...
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Remove references to deprecated propagate as decision...
commit
|
commitdiff
|
tree
2018-08-02
Andres Noetzli
Remove Subversion build info (#2250)
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Fix API call for reg exp. (#2248)
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Improvements and fixes in cegqi arithmetic (#2247)
commit
|
commitdiff
|
tree
2018-08-02
Andres Noetzli
Remove outdated references to TLS (#2245)
commit
|
commitdiff
|
tree
2018-08-02
Andrew Reynolds
Fix issues with printing parametric datatypes in smt2...
commit
|
commitdiff
|
tree
2018-08-01
Andres Noetzli
Fix wrong evaluation of STRING_STOI (#2252)
commit
|
commitdiff
|
tree
2018-08-01
Mathias Preiner
Fix bool-to-bv preprocessing pass for non-{bv,bool...
commit
|
commitdiff
|
tree
2018-08-01
Aina Niemetz
InteractiveShell: Remove redundant options argument...
commit
|
commitdiff
|
tree
2018-08-01
Aina Niemetz
New C++ API: Fixed ownership of options object. (#2243)
commit
|
commitdiff
|
tree
2018-08-01
Andrew Reynolds
Fix issues with bv2nat (#2219)
commit
|
commitdiff
|
tree
2018-08-01
Andrew Reynolds
Fix assertion in conjecture generator (#2246)
commit
|
commitdiff
|
tree
2018-08-01
Andrew Reynolds
Make conjecture generator's uf term enumeration safer...
commit
|
commitdiff
|
tree
2018-08-01
Andrew Reynolds
Make candidate rewrite match filtering handle polymorph...
commit
|
commitdiff
|
tree
2018-08-01
ayveejay
Improvements and tests for the API around separation...
commit
|
commitdiff
|
tree
2018-08-01
Mathias Preiner
Remove hasAssertions() method from eager BV solver...
commit
|
commitdiff
|
tree
2018-07-31
Mathias Preiner
Fix option handler for lazy/bv-sat-solver combinations...
commit
|
commitdiff
|
tree
2018-07-30
Mathias Preiner
Add support for incremental eager bit-blasting. (#1838)
commit
|
commitdiff
|
tree
2018-07-30
FabianWolff
Fix several spelling errors (#2231)
commit
|
commitdiff
|
tree
2018-07-30
Tim King
Storing a std::pair<Key,Data> on CDOhash_map.
commit
|
commitdiff
|
tree
2018-07-27
Mathias Preiner
Require argument description for non-{bool,void} option...
commit
|
commitdiff
|
tree
2018-07-27
Andres Noetzli
Fix issues related to cxxtest in configure.ac (#2226)
commit
|
commitdiff
|
tree
2018-07-27
Mathias Preiner
Make Python a required CVC4 dependency. (#2227)
commit
|
commitdiff
|
tree
2018-07-27
Andrew Reynolds
Fix for candidate rewrite rule filtering. (#2220)
commit
|
commitdiff
|
tree
2018-07-27
Andrew Reynolds
Make check-synth robust for assertions that are not...
commit
|
commitdiff
|
tree
2018-07-27
Andrew Reynolds
Fix Node::hasFreeVar for function variables (#2216)
commit
|
commitdiff
|
tree
2018-07-27
Mathias Preiner
Fix CryptoMiniSat config to allow system versions....
commit
|
commitdiff
|
tree
2018-07-26
Aina Niemetz
New C++ API: Enable examples. (#2222)
commit
|
commitdiff
|
tree
2018-07-26
Tim King
Removing unused CDTrailHashmap. (#2221)
commit
|
commitdiff
|
tree
2018-07-26
yoni206
Disabling bvLazyRewriteExtf in the right place (#2214)
commit
|
commitdiff
|
tree
2018-07-26
Tim King
Changing CDInsertHashMap to store <const Key, const...
commit
|
commitdiff
|
tree
2018-07-26
Tim King
Changing the arithmetic static learner to use CDHashMap...
commit
|
commitdiff
|
tree
2018-07-26
Andrew Reynolds
Fix rewriter for lambda (#2211)
commit
|
commitdiff
|
tree
2018-07-26
Andrew Reynolds
Fix a few issues in the sygus sampler related to evalu...
commit
|
commitdiff
|
tree
2018-07-26
ayveejay
Avoid explicit dependency on Python 3 (#2195)
commit
|
commitdiff
|
tree
2018-07-26
Aina Niemetz
New C++ API: Third batch of commands (SMT-LIB). (#2212)
commit
|
commitdiff
|
tree
2018-07-26
Aina Niemetz
New C++ API: Second batch of commands (SMT-LIB). (...
commit
|
commitdiff
|
tree
2018-07-25
Tim King
Changing ArithIteUtils to use CDInsertHashMap. (#2206)
commit
|
commitdiff
|
tree
2018-07-25
Tim King
Removing support for CDHashMap::iterator's postfix...
commit
|
commitdiff
|
tree
2018-07-25
Andrew Reynolds
Move reg exp rewrites from prerewrite to postrewrite...
commit
|
commitdiff
|
tree
2018-07-25
ayveejay
Performing clang-format on the original change-set...
commit
|
commitdiff
|
tree
2018-07-25
Mathias Preiner
Use CryptoMiniSat 5.6.3. (#2205)
commit
|
commitdiff
|
tree
2018-07-24
Andrew Reynolds
Improvements to sets + cardinality + quantifiers (...
commit
|
commitdiff
|
tree
2018-07-24
ayveejay
Adding API access methods to get heap/nil expressions...
commit
|
commitdiff
|
tree
2018-07-24
Aina Niemetz
New C++ API: First batch of commands (SMT-LIB and...
commit
|
commitdiff
|
tree
2018-07-23
Andrew Reynolds
Improve rewriter for regular expression concatenation...
commit
|
commitdiff
|
tree
2018-07-23
Andrew Reynolds
Generalize symmetry detection for 1 symmetry variable...
commit
|
commitdiff
|
tree
2018-07-23
Aina Niemetz
New C++ API: Implementation of Solver class: OpTerm...
commit
|
commitdiff
|
tree
2018-07-23
Aina Niemetz
New C++ API: declare-datatype. (#2166)
commit
|
commitdiff
|
tree
2018-07-23
Andrew Reynolds
sygusComp2018: add regressions (#2191)
commit
|
commitdiff
|
tree
2018-07-23
Andrew Reynolds
Fix warning in sygus PBE (#2190)
commit
|
commitdiff
|
tree
2018-07-22
Andrew Reynolds
sygusComp2018: Improvements to CEGIS loop (#2187)
commit
|
commitdiff
|
tree
2018-07-21
Andrew Reynolds
Optimizations and fixes for computing whether a type...
commit
|
commitdiff
|
tree
2018-07-21
Andrew Reynolds
sygusComp2018: refactor and improve sygus io utility...
commit
|
commitdiff
|
tree
2018-07-21
yoni206
Remove --no-check-proofs and --no-check-unsat-cores...
commit
|
commitdiff
|
tree
2018-07-20
Andrew Reynolds
Cleanup and additions for candidate generator (#2173)
commit
|
commitdiff
|
tree
2018-07-20
Andrew Reynolds
sygusComp2018: minor changes to repair constant utilit...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
sygusComp2018: pbe multi-enumerator fairness option...
commit
|
commitdiff
|
tree
2018-07-17
yoni206
Refactor sep-pre-skolem-emp preprocessing pass
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
Minor cleanup and fixes for conflict-based instantiatio...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
Do extended rewrite on results of quantifier eliminatio...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
Purify applications of exp to transcendental arguments...
commit
|
commitdiff
|
tree
2018-07-17
Andrew Reynolds
sygusComp2018: update policies for solution reconstruc...
commit
|
commitdiff
|
tree
next