projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2017-10-31
Andrew Reynolds
Remove include (#1298)
commit
|
commitdiff
|
tree
2017-10-28
Andres Noetzli
Change bvudiv semantics based on input language (#1292)
commit
|
commitdiff
|
tree
2017-10-28
Andrew Reynolds
(Move only) Move enumerative instantiation strategy...
commit
|
commitdiff
|
tree
2017-10-28
Andrew Reynolds
Sygus process conjecture (#1286)
commit
|
commitdiff
|
tree
2017-10-28
Andrew Reynolds
Document term db (#1220)
commit
|
commitdiff
|
tree
2017-10-28
Andrew Reynolds
Improve strings rewriter for contains (#1207)
commit
|
commitdiff
|
tree
2017-10-28
Andrew Reynolds
Document quant arith (#1271)
commit
|
commitdiff
|
tree
2017-10-27
Andres Noetzli
Modify LDFLAGS to support shared libraries for Win...
commit
|
commitdiff
|
tree
2017-10-27
Andrew Reynolds
Cbqi multiple instantiation (#1289)
commit
|
commitdiff
|
tree
2017-10-27
Andrew Reynolds
Refactor theory model (#1236)
commit
|
commitdiff
|
tree
2017-10-27
Andrew Reynolds
Implement Hilbert choice operator (#1291)
commit
|
commitdiff
|
tree
2017-10-27
Tim King
Adds a macro to SWIG to ignore the override and final...
commit
|
commitdiff
|
tree
2017-10-26
Andrew Reynolds
Op overload no fun variant (#1285)
commit
|
commitdiff
|
tree
2017-10-26
Andres Noetzli
Use uintptr_t for pointer casts in Swig files (#1278)
commit
|
commitdiff
|
tree
2017-10-26
Tim King
Removing throw specifiers from OutputChannel and subcla...
commit
|
commitdiff
|
tree
2017-10-25
Tim King
Switching EqProof to use shared_ptr everywhere. (...
commit
|
commitdiff
|
tree
2017-10-25
Aina Niemetz
CBQI BV: Add handling for missing operators. (#1274)
commit
|
commitdiff
|
tree
2017-10-25
Andrew Reynolds
Cbqi bv ineq mode (#1273)
commit
|
commitdiff
|
tree
2017-10-24
Andrew Reynolds
Removing deprecated file. (#1270)
commit
|
commitdiff
|
tree
2017-10-24
Mathias Preiner
Remove clang-format options introduced in version 5.0.
commit
|
commitdiff
|
tree
2017-10-24
Mathias Preiner
New clang-format style based on the Google style. ...
commit
|
commitdiff
|
tree
2017-10-24
Aina Niemetz
CBQI BV: Add ULT/SLT inverse handling. (#1268)
commit
|
commitdiff
|
tree
2017-10-23
Andrew Reynolds
Document sygus programming-by-examples utility (#1260)
commit
|
commitdiff
|
tree
2017-10-21
Mathias Preiner
Add rewriting rules for Eq/Ult with sign_extend and...
commit
|
commitdiff
|
tree
2017-10-21
Mathias Preiner
Simplify atoms introduced while bitblasting. (#1267)
commit
|
commitdiff
|
tree
2017-10-20
Andrew Reynolds
SyGuS term size limit (#1262)
commit
|
commitdiff
|
tree
2017-10-20
Andrew Reynolds
Make Sygus conjectures higher-order (#1244)
commit
|
commitdiff
|
tree
2017-10-19
Aina Niemetz
CBQI BV: Refactor solve_bv_constraint. (#1265)
commit
|
commitdiff
|
tree
2017-10-18
Andrew Reynolds
Tptp unsat cores (#1228)
commit
|
commitdiff
|
tree
2017-10-18
Andrew Reynolds
Strings API escape sequences (#1245)
commit
|
commitdiff
|
tree
2017-10-17
Tim King
Making the values argument const in the SetUserAttribut...
commit
|
commitdiff
|
tree
2017-10-17
Tim King
Fixing 2 instances of an unused variable. (#1253)
commit
|
commitdiff
|
tree
2017-10-17
Clark Barrett
Fix for issue 1247 (#1257)
commit
|
commitdiff
|
tree
2017-10-17
Andrew Reynolds
Sygus enumerators to conjecture (#1237)
commit
|
commitdiff
|
tree
2017-10-16
Tim King
Adds unit test that show Node and TNode work with for...
commit
|
commitdiff
|
tree
2017-10-13
Aina Niemetz
CBQI BV: Added EXTRACT handling. (#1240)
commit
|
commitdiff
|
tree
2017-10-13
Andrew Reynolds
CBQI BV quick heuristics (#1239)
commit
|
commitdiff
|
tree
2017-10-12
Andrew Reynolds
Initial support for solving bit-vector inequalities...
commit
|
commitdiff
|
tree
2017-10-12
Andrew Reynolds
Sygus logics (#1226)
commit
|
commitdiff
|
tree
2017-10-12
Aina Niemetz
Enable regressions for CBQI BV and fix inverse for...
commit
|
commitdiff
|
tree
2017-10-12
Mathias Preiner
Reduce number of travis builds.
commit
|
commitdiff
|
tree
2017-10-12
Mathias Preiner
Add side conditions for UDIV_TOTAL, SHL, CONCAT. (...
commit
|
commitdiff
|
tree
2017-10-11
Tim King
Cleaning up ProofArray class. (#1208)
commit
|
commitdiff
|
tree
2017-10-11
Andrew Reynolds
Ho Lambda Lifting (#1116)
commit
|
commitdiff
|
tree
2017-10-11
Andrew Reynolds
Adds infrastructure for a rewriting pass in BvInstantia...
commit
|
commitdiff
|
tree
2017-10-11
Andrew Reynolds
Move unsat core names to smt engine (#1192)
commit
|
commitdiff
|
tree
2017-10-11
Andrew Reynolds
Ho node manager types (#1203)
commit
|
commitdiff
|
tree
2017-10-10
Aina Niemetz
Add copyright information. (#1201)
commit
|
commitdiff
|
tree
2017-10-10
Andres Noetzli
Fix memory leak in quantifiers engine (#1219)
commit
|
commitdiff
|
tree
2017-10-10
Martin
Add skeleton of the FP theory solver (#1130)
commit
|
commitdiff
|
tree
2017-10-10
Andrew Reynolds
Split term database (#1206)
commit
|
commitdiff
|
tree
2017-10-10
Aina Niemetz
CBQI BV: Add inverse for more operators. (#1213)
commit
|
commitdiff
|
tree
2017-10-05
Clark Barrett
Fix typo in comment.
commit
|
commitdiff
|
tree
2017-10-05
Mathias Preiner
Split COPYING file, add missing licenses. (#1195)
commit
|
commitdiff
|
tree
2017-10-05
Andrew Reynolds
Minor change to how SyGus commands are translated to...
commit
|
commitdiff
|
tree
2017-10-05
Andrew Reynolds
Ho model (#1120)
commit
|
commitdiff
|
tree
2017-10-05
Martin
Allow CDHashMaps for objects without default constructo...
commit
|
commitdiff
|
tree
2017-10-05
Aina Niemetz
Add mkZero, mkOne and mkUmulo to bv utils. (#1200)
commit
|
commitdiff
|
tree
2017-10-04
Andrew Reynolds
Ho quant util (#1119)
commit
|
commitdiff
|
tree
2017-10-04
Tim King
Removing the throw specifier from ArrayStoreAll constru...
commit
|
commitdiff
|
tree
2017-10-04
Andrew Reynolds
Add regression from #50 regarding "as" parsing in smt2...
commit
|
commitdiff
|
tree
2017-10-03
Mathias Preiner
Add Cryptominisat and LFSC to --show-config output...
commit
|
commitdiff
|
tree
2017-10-03
Andrew Reynolds
Move sygus grammar utilities to separate file. (#1184)
commit
|
commitdiff
|
tree
2017-10-03
Andrew Reynolds
Op overload parser (#1162)
commit
|
commitdiff
|
tree
2017-10-03
Andres Noetzli
Add initial version of the SMTCOMP2018 run scripts...
commit
|
commitdiff
|
tree
2017-10-03
Andres Noetzli
Unify hash functions for pairs (#1161)
commit
|
commitdiff
|
tree
2017-10-03
Martin
Add 5 FP kinds for partial to total fn conversion ...
commit
|
commitdiff
|
tree
2017-10-02
Mathias Preiner
Address comments from PR #1164. (#1174)
commit
|
commitdiff
|
tree
2017-10-02
Tim King
Removing throw specifiers from SymbolTable::Implementat...
commit
|
commitdiff
|
tree
2017-10-02
Tim King
Removing throw specifiers from TypeEnumeratorBase's...
commit
|
commitdiff
|
tree
2017-10-02
Tim King
CID 1457268: Initializing CegConjecture::d_syntax_guide...
commit
|
commitdiff
|
tree
2017-10-01
Andrew Reynolds
Refactor check function in last call effort of non...
commit
|
commitdiff
|
tree
2017-09-30
Andrew Reynolds
SyGuS streaming solution mode (#1131)
commit
|
commitdiff
|
tree
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
next