projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2017-09-29
Mathias Preiner
Move BvInverter class into separate file. (#1173)
commit
|
commitdiff
|
tree
2017-09-29
Clark Barrett
A few updates to license files.
commit
|
commitdiff
|
tree
2017-09-29
Andres Noetzli
Add license information for GMP
commit
|
commitdiff
|
tree
2017-09-29
Andrew Reynolds
Simplify representation of inversion Skolems for bv...
commit
|
commitdiff
|
tree
2017-09-29
Andrew Reynolds
Initial working version of BV word-level instantiation...
commit
|
commitdiff
|
tree
2017-09-29
Andres Noetzli
Better hash function for pairs (#1157)
commit
|
commitdiff
|
tree
2017-09-29
Andrew Reynolds
Update symbol table to support operator overloading...
commit
|
commitdiff
|
tree
2017-09-29
Mathias Preiner
Fix output of --show-config for readline. (#1159)
commit
|
commitdiff
|
tree
2017-09-28
Andrew Reynolds
Cegqi refactor prep bv (#1155)
commit
|
commitdiff
|
tree
2017-09-28
Andrew Reynolds
Improve finite model finding for recursive predicates...
commit
|
commitdiff
|
tree
2017-09-27
Andrew Reynolds
Minor fixes for partial quantifier elimination. (#1147)
commit
|
commitdiff
|
tree
2017-09-27
Aina Niemetz
CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)
commit
|
commitdiff
|
tree
2017-09-27
Andrew Reynolds
Add quantifiers API example, fixes #879 (#1146)
commit
|
commitdiff
|
tree
2017-09-27
Andres Noetzli
Fix seeking for buffered input (#1145)
commit
|
commitdiff
|
tree
2017-09-27
Martin Brain
Fix type checking of to_real (#1127)
commit
|
commitdiff
|
tree
2017-09-27
Martin Brain
Improve FP rewriter: const folding, other (#1126)
commit
|
commitdiff
|
tree
2017-09-26
Tim King
Fixing CIDs 1172014 and 1172013: Initializing members...
commit
|
commitdiff
|
tree
2017-09-26
Tim King
Fixing Cid 1172009 (#1141)
commit
|
commitdiff
|
tree
2017-09-26
Tim King
Fixing CID 1172020: Initializing CDHashMap::iterator...
commit
|
commitdiff
|
tree
2017-09-26
Tim King
Fixing CID 1362903: Initializing d_bvp to nullptr....
commit
|
commitdiff
|
tree
2017-09-26
Tim King
CID 1362904: Initializing GetInstantiationsCommand...
commit
|
commitdiff
|
tree
2017-09-26
Andres Noetzli
Fix build for old GMP version (#1114)
commit
|
commitdiff
|
tree
2017-09-26
Tim King
Fixing CIDs 1172012 and 1172011: Initiallzing d_exprMan...
commit
|
commitdiff
|
tree
2017-09-26
Andrew Reynolds
Cegqi refactor substitutions (#1129)
commit
|
commitdiff
|
tree
2017-09-25
Tim King
Initializing BVMinisat Solver::notify to nullptr. ...
commit
|
commitdiff
|
tree
2017-09-25
Andrew Reynolds
Fix bug related to sort inference + subtypes. (#1125)
commit
|
commitdiff
|
tree
2017-09-25
Tim King
Fixing CID 1362917: There was a branch where d_issup...
commit
|
commitdiff
|
tree
2017-09-25
Tim King
Fixing CID 1362895: Initializing d_bvp to nullptr....
commit
|
commitdiff
|
tree
2017-09-25
Tim King
CID 1362907: Initializing d_smtEngine to nullptr. ...
commit
|
commitdiff
|
tree
2017-09-21
Andrew Reynolds
Sygus inv templ refactor (#1110)
commit
|
commitdiff
|
tree
2017-09-21
Andrew Reynolds
Extend quantifier-free UF solver to higher-order. This...
commit
|
commitdiff
|
tree
2017-09-20
Andres Noetzli
Fix issue #1081, memory leak in cmd executor (#1109)
commit
|
commitdiff
|
tree
2017-09-20
Martin
Add FP type enumerator and cardinality computer (#1104)
commit
|
commitdiff
|
tree
2017-09-19
Tim King
Fixing a null pointer dereference in the cvc3 compatibi...
commit
|
commitdiff
|
tree
2017-09-19
Tim King
Removing a potentially invalid comparison in the TPTP...
commit
|
commitdiff
|
tree
2017-09-19
Andres Noetzli
Fix issue #1074, improve non-fatal error handling ...
commit
|
commitdiff
|
tree
2017-09-19
Andrew Reynolds
Refactor cegqi instantiation infrastructure so that...
commit
|
commitdiff
|
tree
2017-09-19
Andrew Reynolds
Fix issue #1105 involving string to int (#1112)
commit
|
commitdiff
|
tree
2017-09-19
Martin
Floating point symfpu support (#1103)
commit
|
commitdiff
|
tree
2017-09-18
Tim King
Moving the CVC4_PUBLIC attribute to the beginning of...
commit
|
commitdiff
|
tree
2017-09-15
Martin
Make floating-point comparison operators chainable...
commit
|
commitdiff
|
tree
2017-09-15
makaimann
Add missing CVC4_PUBLIC in kind_template (#1078)
commit
|
commitdiff
|
tree
2017-09-14
Andres Noetzli
Enable ccache compression, increase cache size (#1099)
commit
|
commitdiff
|
tree
2017-09-14
Andrew Reynolds
Remove unhandled subtypes (#1098)
commit
|
commitdiff
|
tree
2017-09-14
Tim King
Simplifying the throw specifier of SmtEngine::checkSat...
commit
|
commitdiff
|
tree
2017-09-14
Martin
Floating point symfpu support (#1093)
commit
|
commitdiff
|
tree
2017-09-14
Andrew Reynolds
Add new kinds required for higher-order. (#1083)
commit
|
commitdiff
|
tree
2017-09-14
Andrew Reynolds
Add isConst check for lambda expressions. (#1084)
commit
|
commitdiff
|
tree
2017-09-13
Andres Noetzli
Make ccache work with Clang on Travis (#1097)
commit
|
commitdiff
|
tree
2017-09-13
Andrew Reynolds
Modify equality engine to allow operators to be marked...
commit
|
commitdiff
|
tree
2017-09-13
Andres Noetzli
Remove unused RecordSelect and TupleSelect (#1087)
commit
|
commitdiff
|
tree
2017-09-13
Andres Noetzli
Enable ccache on Travis, disable debug symbols (#1094)
commit
|
commitdiff
|
tree
2017-09-12
Andrew Reynolds
Initial infrastructure for BV instantiation via word...
commit
|
commitdiff
|
tree
2017-09-12
Tim King
Adding reasonable breaks in switch statement in TheoryS...
commit
|
commitdiff
|
tree
2017-09-11
Tim King
Addressing a coverity scan complaint in theory_strings...
commit
|
commitdiff
|
tree
2017-09-10
Andrew Reynolds
Ensure that expand definitions is called on all non...
commit
|
commitdiff
|
tree
2017-09-07
Andrew Reynolds
Properly handle user cardinality constraints for uf...
commit
|
commitdiff
|
tree
2017-09-05
Mathias Preiner
Fix link in configure.ac.
commit
|
commitdiff
|
tree
2017-09-05
Andrew Reynolds
Remove support for conversions between uint32/uint16...
commit
|
commitdiff
|
tree
2017-09-01
Aina Niemetz
Add travis debug build with cln. (#1066)
commit
|
commitdiff
|
tree
2017-09-01
Andres Noetzli
Add GCC7 jobs to Travis (#1054)
commit
|
commitdiff
|
tree
2017-09-01
Andres Noetzli
Replace CVC4_THREADLOCAL in interactive_shell (#1065)
commit
|
commitdiff
|
tree
2017-08-31
Andrew Reynolds
Answer unknown when uf-ss=no-minimal is combined with...
commit
|
commitdiff
|
tree
2017-08-31
Andres Noetzli
Use thread_local instead of compiler extensions (#210)
commit
|
commitdiff
|
tree
2017-08-30
Andrew Reynolds
Fix model construction for parametric types (#1059)
commit
|
commitdiff
|
tree
2017-08-30
Mathias Preiner
Remove Coverity SSL certificate workaround from Travis...
commit
|
commitdiff
|
tree
2017-08-29
Mathias Preiner
Fix indentation for disabled Java tests.
commit
|
commitdiff
|
tree
2017-08-29
Mathias Preiner
Disable Java tests for now until they get fixed.
commit
|
commitdiff
|
tree
2017-08-28
Pat Hawks
Run Ant on Travis
commit
|
commitdiff
|
tree
2017-08-28
Andres Noetzli
Travis: Package instead of download for cxxtest (#1055)
commit
|
commitdiff
|
tree
2017-08-25
Aina Niemetz
Move LFSC checker out of the CVC repository. (#222)
commit
|
commitdiff
|
tree
2017-08-25
Aina Niemetz
Added missing includes (algorithm).
commit
|
commitdiff
|
tree
2017-08-24
Pat Hawks
Test Java API on CI
commit
|
commitdiff
|
tree
2017-08-24
Andres Noetzli
Add include to fix build
commit
|
commitdiff
|
tree
2017-08-24
Andrew Reynolds
Merge pull request #191 from timothy-king/cleanup-regexp
commit
|
commitdiff
|
tree
2017-08-24
Andres Noetzli
Fix typos
commit
|
commitdiff
|
tree
2017-08-23
Tim King
Removing TODO for 'Optimize via the iterator'. Not...
commit
|
commitdiff
|
tree
2017-08-22
Aina Niemetz
Cleanup: use Assert rather than C assert. (#1052)
commit
|
commitdiff
|
tree
2017-08-22
Clark Barrett
Updated NYU -> Stanford
commit
|
commitdiff
|
tree
2017-08-21
Mathias Preiner
Change Bugzilla urls to Github issues.
commit
|
commitdiff
|
tree
2017-08-17
Andres Noetzli
Remove unused SubrangeBound(s) classes (#221)
commit
|
commitdiff
|
tree
2017-08-17
ajreynol
Add mbqi interleave option, change option fs-inst to...
commit
|
commitdiff
|
tree
2017-08-15
Andres Noetzli
Minimize includes in expr.h: remove dups, iostream...
commit
|
commitdiff
|
tree
2017-08-15
Andres Noetzli
Move function definitions from metakind.h to cpp (...
commit
|
commitdiff
|
tree
2017-08-15
Andres Noetzli
Move function definitions from kind.h to kind.cpp ...
commit
|
commitdiff
|
tree
2017-08-14
Andres Noetzli
Move function defns from smt_engine_scope.h to cpp...
commit
|
commitdiff
|
tree
2017-08-14
Mathias Preiner
Use antlr-3.4 directory if already present in CVC4...
commit
|
commitdiff
|
tree
2017-08-14
Aina Niemetz
Merge pull request #214 from CVC4/fix_warn_nonlinear
commit
|
commitdiff
|
tree
2017-08-14
Mark Laws
Build and test suite fixes for Windows (#186)
commit
|
commitdiff
|
tree
2017-08-12
Aina Niemetz
Fix compiler warnings in theory/arith/nonlinear_extensi...
commit
|
commitdiff
|
tree
2017-08-11
ajreynol
Maintain frontier for tangent planes.
commit
|
commitdiff
|
tree
2017-08-10
Andres Noetzli
Fix line numbers in options_template
commit
|
commitdiff
|
tree
2017-08-09
Mathias Preiner
Fix compiler warning in src/context/context.h.
commit
|
commitdiff
|
tree
2017-08-09
Aina Niemetz
Fix help message for disable-unit-testing in configure...
commit
|
commitdiff
|
tree
2017-08-09
Mathias Preiner
Remove AigBitblaster implementation if ABC is not compi...
commit
|
commitdiff
|
tree
2017-08-09
Aina Niemetz
Fix Assertion (compiler warning) in theory/bv/theory_bv.cpp
commit
|
commitdiff
|
tree
2017-08-09
Andres Noetzli
Fix compiler warning in sat_proof_implementation
commit
|
commitdiff
|
tree
2017-08-08
ajreynol
Use cache for datatypes cycle check, add regression.
commit
|
commitdiff
|
tree
2017-08-08
Andrew Reynolds
Merge pull request #211 from CVC4/fix_warn_sygus
commit
|
commitdiff
|
tree
2017-08-08
Andres Noetzli
Optionally split regression tests into test groups...
commit
|
commitdiff
|
tree
next