projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2017-12-06 Aina NiemetzFixed time stats for MiniSat solve time. (#1431) commit | commitdiff | tree
2017-12-06 Andres NoetzliRemove CDChunkList (#1414) commit | commitdiff | tree
2017-12-05 Mathias PreinerFix output of --show-trace-tags. (#1430) commit | commitdiff | tree
2017-12-05 Haniel BarbosaAdding SyGuS grammars for rationals. (#1426) commit | commitdiff | tree
2017-12-04 Andrew ReynoldsEliminate expand definitions from Sygus (#1425) commit | commitdiff | tree
2017-12-04 Andrew ReynoldsFix strings rewriter for strip constant endpoint revers... commit | commitdiff | tree
2017-12-04 Mathias PreinerFix side condition for BITVECTOR_MULT. (#1422) commit | commitdiff | tree
2017-12-03 Haniel BarbosaNormalize grammars - 2 (#1420) commit | commitdiff | tree
2017-12-02 Andrew ReynoldsMinor improvements to inst match generator (#1415) commit | commitdiff | tree
2017-12-02 Andrew ReynoldsImprove rewriter for string replace (#1416) commit | commitdiff | tree
2017-12-01 Andres NoetzliFix reset-assertions (#1413) commit | commitdiff | tree
2017-12-01 Andrew ReynoldsMinor additions for sygus (#1419) commit | commitdiff | tree
2017-12-01 Andrew ReynoldsRefactor and generalize PBE strategies (#1410) commit | commitdiff | tree
2017-12-01 Andres NoetzliFix build when Valgrind instrumentation enabled commit | commitdiff | tree
2017-12-01 Andres NoetzliAdd debugging tools for ContextMemoryManager (#1407) commit | commitdiff | tree
2017-11-30 Aina NiemetzAdd Gaussian Elimination as a preprocessing pass for... commit | commitdiff | tree
2017-11-30 Andrew ReynoldsFixes for issue 1404 (#1409) commit | commitdiff | tree
2017-11-30 Andrew ReynoldsRemove remaining references to QuantArith (#1408) commit | commitdiff | tree
2017-11-30 Andrew ReynoldsMinor improvements and changes to defaults for cbqi... commit | commitdiff | tree
2017-11-29 Andrew ReynoldsImprove caching in term formula removal (#1398) commit | commitdiff | tree
2017-11-29 Tim KingAdding missing break statements. CID 1362756. (#1394) commit | commitdiff | tree
2017-11-29 Tim KingSimplifying the conditions in checkLetBinding to avoid... commit | commitdiff | tree
2017-11-29 Mathias PreinerAdd Cryptominisat script and patches to source file... commit | commitdiff | tree
2017-11-29 Andrew ReynoldsImprove the rewriter for SINE. (#1221) commit | commitdiff | tree
2017-11-28 Andrew ReynoldsImprove rewrite for string substr (#1337) commit | commitdiff | tree
2017-11-28 Andrew ReynoldsImprove trigger filter instances (#1402) commit | commitdiff | tree
2017-11-28 Tim KingRemoving throw specifiers from internal Printer hierarc... commit | commitdiff | tree
2017-11-28 Andrew ReynoldsFix models for --solve-real-as-int. (#1371) commit | commitdiff | tree
2017-11-25 Andrew ReynoldsFixes for higher-order (#1405) commit | commitdiff | tree
2017-11-25 Andrew Reynolds(Refactor) Instantiate utility (#1387) commit | commitdiff | tree
2017-11-24 Andrew ReynoldsImplement tangent and secant planes for transcendental... commit | commitdiff | tree
2017-11-24 Andrew ReynoldsHo parsing and regressions (#1350) commit | commitdiff | tree
2017-11-23 Haniel BarbosaConverting defined functions and let expressions from... commit | commitdiff | tree
2017-11-22 Andrew ReynoldsSygus Lambda Grammars (#1390) commit | commitdiff | tree
2017-11-22 Andrew ReynoldsTranscendental tangent planes utilities (#1288) commit | commitdiff | tree
2017-11-21 Haniel BarbosaAdding infrastructure for normalizing SyGuS grammars... commit | commitdiff | tree
2017-11-21 Andrew ReynoldsCegqi bv remove extract terms preprocess pass (#1376) commit | commitdiff | tree
2017-11-20 Tim KingInitializes members of QuantInfo. Resolves CID 1362929... commit | commitdiff | tree
2017-11-20 Tim KingRemoving an unused variable from SygusInput. Resolves... commit | commitdiff | tree
2017-11-19 Andrew ReynoldsHo instantiation (#1204) commit | commitdiff | tree
2017-11-19 Tim KingNames 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 NiemetzAdd random number generator. (#1370) commit | commitdiff | tree
2017-11-16 Andrew Reynolds(Refactor) Arithmetic monomial sum (#1381) commit | commitdiff | tree
2017-11-16 Tim KingInitializes BitVectorProof::d_isAssumptionConflict... commit | commitdiff | tree
2017-11-15 Andrew ReynoldsSygus print callbacks (#1348) commit | commitdiff | tree
2017-11-15 Andrew ReynoldsReenable some regressions, minor. (#1369) commit | commitdiff | tree
2017-11-15 Tim KingRemoves an unused variable from Theory. (#1375) commit | commitdiff | tree
2017-11-15 Tim KingInitializing members of Datatype. Addresses CIDs 136289... commit | commitdiff | tree
2017-11-15 Tim KingAdding garbage collection for Proof objects. (#1294) commit | commitdiff | tree
2017-11-15 Andrew ReynoldsMake 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 ReynoldsClean Ceg Instantiators (#1365) commit | commitdiff | tree
2017-11-14 Tim KingCleaning up exporting vectors within commands. Resolves... commit | commitdiff | tree
2017-11-14 Tim KingInitializes InstPropagator::d_has_relevant_inst. Resolv... commit | commitdiff | tree
2017-11-14 Tim KingInitializes RegExpOpr::d_char_start and d_char_end... commit | commitdiff | tree
2017-11-14 Tim KingInitializes TriggerInfo::polarity. Resolves CID 1172054... commit | commitdiff | tree
2017-11-14 Tim KingInitializes 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 KingInitializing SharedTermsDatabase::d_conflictPolarity... commit | commitdiff | tree
2017-11-13 Andrew ReynoldsDisable sygus qe preprocessing by default (#1353) commit | commitdiff | tree
2017-11-13 Andrew ReynoldsImplement enumerator for functions. (#1243) commit | commitdiff | tree
2017-11-13 Andrew ReynoldsArgument Relevance for Synthesis Conjectures (#1311) commit | commitdiff | tree
2017-11-13 Tim KingInitializes CegConjectureSingleInvSol::d_root_id. ... commit | commitdiff | tree
2017-11-13 Tim KingInitializing SortInference::initialSortCount. Resolves... commit | commitdiff | tree
2017-11-10 Andrew Reynolds(Documentation-only) datatype.h (#1346) commit | commitdiff | tree
2017-11-10 Andrew ReynoldsPrinting for higher-order (#1347) commit | commitdiff | tree
2017-11-09 Andrew ReynoldsHigher-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 NiemetzAdd modular arithmetic operators. (#1321) commit | commitdiff | tree
2017-11-08 Tim KingInitializing QModelBuilder members. (#1334) commit | commitdiff | tree
2017-11-08 Tim KingCombining d_conflictHasBeenRaised and d_conflictIndex... commit | commitdiff | tree
2017-11-08 Tim KingInitializing TrailHashMap::d_uniqueKeys. (#1331) commit | commitdiff | tree
2017-11-07 Tim King Initialize TimerStat::d_start. (#1330) commit | commitdiff | tree
2017-11-07 Tim KingInitializing Smt1::d_logic in all cases. This was resol... commit | commitdiff | tree
2017-11-07 Andrew ReynoldsGuard 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 KingMoving the enum ArithType to partial_model. Adding... commit | commitdiff | tree
2017-11-07 Andrew ReynoldsAllow FORALL in quantifier elimination command (#1322) commit | commitdiff | tree
2017-11-07 Tim KingInitializing EquivSygusInvarianceTest::d_conj in the... commit | commitdiff | tree
2017-11-07 Tim KingInitializing NegContainsSygusInvarianceTest::d_cpbe... commit | commitdiff | tree
2017-11-07 Tim KingUsing unique_ptr's for members of CegConjecture. (... commit | commitdiff | tree
2017-11-07 Andrew ReynoldsUpdates to interface for Sygus grammar construction... commit | commitdiff | tree
2017-11-06 Andrew ReynoldsUnrecurisify rewrite solve assertion for cbqi bv (... commit | commitdiff | tree
2017-11-06 Aina NiemetzAdd getValue() for Rational and Integer (GMP and CLN... commit | commitdiff | tree
2017-11-06 Andrew ReynoldsImprove rewriting for string contains part 2 (#1300) commit | commitdiff | tree
2017-11-05 Andrew ReynoldsMake higher-order a flag in logic info. (#1318) commit | commitdiff | tree
2017-11-04 Andrew ReynoldsSuppport SAT logic (#1310) commit | commitdiff | tree
2017-11-04 Andrew ReynoldsFix bv help message. (#1315) commit | commitdiff | tree
2017-11-03 Andrew ReynoldsSygus 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 ReynoldsCBQI 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 KingCID 1459592: Always checking whether rd is null or... commit | commitdiff | tree
2017-10-31 Andrew ReynoldsRemove include (#1298) commit | commitdiff | tree
2017-10-28 Andres NoetzliChange 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 ReynoldsSygus process conjecture (#1286) commit | commitdiff | tree
next