projects
/
cvc5.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
cvc5.git
2017-12-01
Andres Noetzli
Fix reset-assertions (#1413)
commit
|
commitdiff
|
tree
2017-12-01
Andrew Reynolds
Minor additions for sygus (#1419)
commit
|
commitdiff
|
tree
2017-12-01
Andrew Reynolds
Refactor and generalize PBE strategies (#1410)
commit
|
commitdiff
|
tree
2017-12-01
Andres Noetzli
Fix build when Valgrind instrumentation enabled
commit
|
commitdiff
|
tree
2017-12-01
Andres Noetzli
Add debugging tools for ContextMemoryManager (#1407)
commit
|
commitdiff
|
tree
2017-11-30
Aina Niemetz
Add Gaussian Elimination as a preprocessing pass for...
commit
|
commitdiff
|
tree
2017-11-30
Andrew Reynolds
Fixes for issue 1404 (#1409)
commit
|
commitdiff
|
tree
2017-11-30
Andrew Reynolds
Remove remaining references to QuantArith (#1408)
commit
|
commitdiff
|
tree
2017-11-30
Andrew Reynolds
Minor improvements and changes to defaults for cbqi...
commit
|
commitdiff
|
tree
2017-11-29
Andrew Reynolds
Improve caching in term formula removal (#1398)
commit
|
commitdiff
|
tree
2017-11-29
Tim King
Adding missing break statements. CID 1362756. (#1394)
commit
|
commitdiff
|
tree
2017-11-29
Tim King
Simplifying the conditions in checkLetBinding to avoid...
commit
|
commitdiff
|
tree
2017-11-29
Mathias Preiner
Add Cryptominisat script and patches to source file...
commit
|
commitdiff
|
tree
2017-11-29
Andrew Reynolds
Improve the rewriter for SINE. (#1221)
commit
|
commitdiff
|
tree
2017-11-28
Andrew Reynolds
Improve rewrite for string substr (#1337)
commit
|
commitdiff
|
tree
2017-11-28
Andrew Reynolds
Improve trigger filter instances (#1402)
commit
|
commitdiff
|
tree
2017-11-28
Tim King
Removing throw specifiers from internal Printer hierarc...
commit
|
commitdiff
|
tree
2017-11-28
Andrew Reynolds
Fix models for --solve-real-as-int. (#1371)
commit
|
commitdiff
|
tree
2017-11-25
Andrew Reynolds
Fixes for higher-order (#1405)
commit
|
commitdiff
|
tree
2017-11-25
Andrew Reynolds
(Refactor) Instantiate utility (#1387)
commit
|
commitdiff
|
tree
2017-11-24
Andrew Reynolds
Implement tangent and secant planes for transcendental...
commit
|
commitdiff
|
tree
2017-11-24
Andrew Reynolds
Ho parsing and regressions (#1350)
commit
|
commitdiff
|
tree
2017-11-23
Haniel Barbosa
Converting defined functions and let expressions from...
commit
|
commitdiff
|
tree
2017-11-22
Andrew Reynolds
Sygus Lambda Grammars (#1390)
commit
|
commitdiff
|
tree
2017-11-22
Andrew Reynolds
Transcendental tangent planes utilities (#1288)
commit
|
commitdiff
|
tree
2017-11-21
Haniel Barbosa
Adding infrastructure for normalizing SyGuS grammars...
commit
|
commitdiff
|
tree
2017-11-21
Andrew Reynolds
Cegqi bv remove extract terms preprocess pass (#1376)
commit
|
commitdiff
|
tree
2017-11-20
Tim King
Initializes members of QuantInfo. Resolves CID 1362929...
commit
|
commitdiff
|
tree
2017-11-20
Tim King
Removing an unused variable from SygusInput. Resolves...
commit
|
commitdiff
|
tree
2017-11-19
Andrew Reynolds
Ho instantiation (#1204)
commit
|
commitdiff
|
tree
2017-11-19
Tim King
Names the Effort enum of QuantConflictFind class. ...
commit
|
commitdiff
|
tree
2017-11-17
Andrew Reynolds
(Refactor) Document and clean single invocation partiti...
commit
|
commitdiff
|
tree
2017-11-17
Aina Niemetz
Add random number generator. (#1370)
commit
|
commitdiff
|
tree
2017-11-16
Andrew Reynolds
(Refactor) Arithmetic monomial sum (#1381)
commit
|
commitdiff
|
tree
2017-11-16
Tim King
Initializes BitVectorProof::d_isAssumptionConflict...
commit
|
commitdiff
|
tree
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
next