projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2017-11-15
Andrew Reynolds
Sygus print callbacks (#1348)
commit
|
commitdiff
|
tree
2017-11-15
Andrew Reynolds
Reenable some regressions, minor. (#1369)
commit
|
commitdiff
|
tree
2017-11-15
Tim King
Removes an unused variable from Theory. (#1375)
commit
|
commitdiff
|
tree
2017-11-15
Tim King
Initializing members of Datatype. Addresses CIDs 136289...
commit
|
commitdiff
|
tree
2017-11-15
Tim King
Adding garbage collection for Proof objects. (#1294)
commit
|
commitdiff
|
tree
2017-11-15
Andrew Reynolds
Make QEffort an enum (#1366)
commit
|
commitdiff
|
tree
2017-11-14
Andrew Reynolds
(Refactor) Split sygus term db (#1335)
commit
|
commitdiff
|
tree
2017-11-14
Andrew Reynolds
Clean Ceg Instantiators (#1365)
commit
|
commitdiff
|
tree
2017-11-14
Tim King
Cleaning up exporting vectors within commands. Resolves...
commit
|
commitdiff
|
tree
2017-11-14
Tim King
Initializes InstPropagator::d_has_relevant_inst. Resolv...
commit
|
commitdiff
|
tree
2017-11-14
Tim King
Initializes RegExpOpr::d_char_start and d_char_end...
commit
|
commitdiff
|
tree
2017-11-14
Tim King
Initializes TriggerInfo::polarity. Resolves CID 1172054...
commit
|
commitdiff
|
tree
2017-11-14
Tim King
Initializes NodeTheoryPair::timestamp in the default...
commit
|
commitdiff
|
tree
2017-11-14
Andrew Reynolds
(Refactor) Decouple rep set iterator and quantifiers...
commit
|
commitdiff
|
tree
2017-11-13
Tim King
Initializing SharedTermsDatabase::d_conflictPolarity...
commit
|
commitdiff
|
tree
2017-11-13
Andrew Reynolds
Disable sygus qe preprocessing by default (#1353)
commit
|
commitdiff
|
tree
2017-11-13
Andrew Reynolds
Implement enumerator for functions. (#1243)
commit
|
commitdiff
|
tree
2017-11-13
Andrew Reynolds
Argument Relevance for Synthesis Conjectures (#1311)
commit
|
commitdiff
|
tree
2017-11-13
Tim King
Initializes CegConjectureSingleInvSol::d_root_id. ...
commit
|
commitdiff
|
tree
2017-11-13
Tim King
Initializing SortInference::initialSortCount. Resolves...
commit
|
commitdiff
|
tree
2017-11-10
Andrew Reynolds
(Documentation-only) datatype.h (#1346)
commit
|
commitdiff
|
tree
2017-11-10
Andrew Reynolds
Printing for higher-order (#1347)
commit
|
commitdiff
|
tree
2017-11-09
Andrew Reynolds
Higher-order prep (#1338)
commit
|
commitdiff
|
tree
2017-11-09
Andrew Reynolds
Decouple sygus term database and term database. (...
commit
|
commitdiff
|
tree
2017-11-09
Aina Niemetz
Add modular arithmetic operators. (#1321)
commit
|
commitdiff
|
tree
2017-11-08
Tim King
Initializing QModelBuilder members. (#1334)
commit
|
commitdiff
|
tree
2017-11-08
Tim King
Combining d_conflictHasBeenRaised and d_conflictIndex...
commit
|
commitdiff
|
tree
2017-11-08
Tim King
Initializing TrailHashMap::d_uniqueKeys. (#1331)
commit
|
commitdiff
|
tree
2017-11-07
Tim King
Initialize TimerStat::d_start. (#1330)
commit
|
commitdiff
|
tree
2017-11-07
Tim King
Initializing Smt1::d_logic in all cases. This was resol...
commit
|
commitdiff
|
tree
2017-11-07
Andrew Reynolds
Guard relevant domain computation properly, minor....
commit
|
commitdiff
|
tree
2017-11-07
Tim King
Removing an unused member from Tptp. Initializing...
commit
|
commitdiff
|
tree
2017-11-07
Tim King
Moving the enum ArithType to partial_model. Adding...
commit
|
commitdiff
|
tree
2017-11-07
Andrew Reynolds
Allow FORALL in quantifier elimination command (#1322)
commit
|
commitdiff
|
tree
2017-11-07
Tim King
Initializing EquivSygusInvarianceTest::d_conj in the...
commit
|
commitdiff
|
tree
2017-11-07
Tim King
Initializing NegContainsSygusInvarianceTest::d_cpbe...
commit
|
commitdiff
|
tree
2017-11-07
Tim King
Using unique_ptr's for members of CegConjecture. (...
commit
|
commitdiff
|
tree
2017-11-07
Andrew Reynolds
Updates to interface for Sygus grammar construction...
commit
|
commitdiff
|
tree
2017-11-06
Andrew Reynolds
Unrecurisify rewrite solve assertion for cbqi bv (...
commit
|
commitdiff
|
tree
2017-11-06
Aina Niemetz
Add getValue() for Rational and Integer (GMP and CLN...
commit
|
commitdiff
|
tree
2017-11-06
Andrew Reynolds
Improve rewriting for string contains part 2 (#1300)
commit
|
commitdiff
|
tree
2017-11-05
Andrew Reynolds
Make higher-order a flag in logic info. (#1318)
commit
|
commitdiff
|
tree
2017-11-04
Andrew Reynolds
Suppport SAT logic (#1310)
commit
|
commitdiff
|
tree
2017-11-04
Andrew Reynolds
Fix bv help message. (#1315)
commit
|
commitdiff
|
tree
2017-11-03
Andrew Reynolds
Sygus clean main (#1297)
commit
|
commitdiff
|
tree
2017-11-02
Andrew Reynolds
(Move-only) Split quant util (#1306)
commit
|
commitdiff
|
tree
2017-11-01
Andrew Reynolds
(Refactor) Split term util (#1303)
commit
|
commitdiff
|
tree
2017-11-01
Andrew Reynolds
CBQI BV choice expressions (#1296)
commit
|
commitdiff
|
tree
2017-11-01
Andres Noetzli
Add option to build shared Windows dependencies (...
commit
|
commitdiff
|
tree
2017-11-01
Andrew Reynolds
(Move-only) Refactor and document theory model part...
commit
|
commitdiff
|
tree
2017-10-31
Tim King
CID 1459592: Always checking whether rd is null or...
commit
|
commitdiff
|
tree
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
next