projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
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
2017-10-28 Andrew ReynoldsDocument term db (#1220) commit | commitdiff | tree
2017-10-28 Andrew ReynoldsImprove strings rewriter for contains (#1207) commit | commitdiff | tree
2017-10-28 Andrew ReynoldsDocument quant arith (#1271) commit | commitdiff | tree
2017-10-27 Andres NoetzliModify LDFLAGS to support shared libraries for Win... commit | commitdiff | tree
2017-10-27 Andrew ReynoldsCbqi multiple instantiation (#1289) commit | commitdiff | tree
2017-10-27 Andrew ReynoldsRefactor theory model (#1236) commit | commitdiff | tree
2017-10-27 Andrew ReynoldsImplement Hilbert choice operator (#1291) commit | commitdiff | tree
2017-10-27 Tim KingAdds a macro to SWIG to ignore the override and final... commit | commitdiff | tree
2017-10-26 Andrew ReynoldsOp overload no fun variant (#1285) commit | commitdiff | tree
2017-10-26 Andres NoetzliUse uintptr_t for pointer casts in Swig files (#1278) commit | commitdiff | tree
2017-10-26 Tim KingRemoving throw specifiers from OutputChannel and subcla... commit | commitdiff | tree
2017-10-25 Tim KingSwitching EqProof to use shared_ptr everywhere. (... commit | commitdiff | tree
2017-10-25 Aina NiemetzCBQI BV: Add handling for missing operators. (#1274) commit | commitdiff | tree
2017-10-25 Andrew ReynoldsCbqi bv ineq mode (#1273) commit | commitdiff | tree
2017-10-24 Andrew ReynoldsRemoving deprecated file. (#1270) commit | commitdiff | tree
2017-10-24 Mathias PreinerRemove clang-format options introduced in version 5.0. commit | commitdiff | tree
2017-10-24 Mathias PreinerNew clang-format style based on the Google style. ... commit | commitdiff | tree
2017-10-24 Aina NiemetzCBQI BV: Add ULT/SLT inverse handling. (#1268) commit | commitdiff | tree
2017-10-23 Andrew ReynoldsDocument sygus programming-by-examples utility (#1260) commit | commitdiff | tree
2017-10-21 Mathias PreinerAdd rewriting rules for Eq/Ult with sign_extend and... commit | commitdiff | tree
2017-10-21 Mathias PreinerSimplify atoms introduced while bitblasting. (#1267) commit | commitdiff | tree
2017-10-20 Andrew ReynoldsSyGuS term size limit (#1262) commit | commitdiff | tree
2017-10-20 Andrew ReynoldsMake Sygus conjectures higher-order (#1244) commit | commitdiff | tree
2017-10-19 Aina NiemetzCBQI BV: Refactor solve_bv_constraint. (#1265) commit | commitdiff | tree
2017-10-18 Andrew ReynoldsTptp unsat cores (#1228) commit | commitdiff | tree
2017-10-18 Andrew ReynoldsStrings API escape sequences (#1245) commit | commitdiff | tree
2017-10-17 Tim KingMaking the values argument const in the SetUserAttribut... commit | commitdiff | tree
2017-10-17 Tim KingFixing 2 instances of an unused variable. (#1253) commit | commitdiff | tree
2017-10-17 Clark BarrettFix for issue 1247 (#1257) commit | commitdiff | tree
2017-10-17 Andrew ReynoldsSygus enumerators to conjecture (#1237) commit | commitdiff | tree
2017-10-16 Tim KingAdds unit test that show Node and TNode work with for... commit | commitdiff | tree
2017-10-13 Aina NiemetzCBQI BV: Added EXTRACT handling. (#1240) commit | commitdiff | tree
2017-10-13 Andrew ReynoldsCBQI BV quick heuristics (#1239) commit | commitdiff | tree
2017-10-12 Andrew ReynoldsInitial support for solving bit-vector inequalities... commit | commitdiff | tree
2017-10-12 Andrew ReynoldsSygus logics (#1226) commit | commitdiff | tree
2017-10-12 Aina NiemetzEnable regressions for CBQI BV and fix inverse for... commit | commitdiff | tree
2017-10-12 Mathias PreinerReduce number of travis builds. commit | commitdiff | tree
2017-10-12 Mathias PreinerAdd side conditions for UDIV_TOTAL, SHL, CONCAT. (... commit | commitdiff | tree
2017-10-11 Tim KingCleaning up ProofArray class. (#1208) commit | commitdiff | tree
2017-10-11 Andrew ReynoldsHo Lambda Lifting (#1116) commit | commitdiff | tree
2017-10-11 Andrew ReynoldsAdds infrastructure for a rewriting pass in BvInstantia... commit | commitdiff | tree
2017-10-11 Andrew ReynoldsMove unsat core names to smt engine (#1192) commit | commitdiff | tree
2017-10-11 Andrew ReynoldsHo node manager types (#1203) commit | commitdiff | tree
2017-10-10 Aina NiemetzAdd copyright information. (#1201) commit | commitdiff | tree
2017-10-10 Andres NoetzliFix memory leak in quantifiers engine (#1219) commit | commitdiff | tree
2017-10-10 MartinAdd skeleton of the FP theory solver (#1130) commit | commitdiff | tree
2017-10-10 Andrew ReynoldsSplit term database (#1206) commit | commitdiff | tree
2017-10-10 Aina NiemetzCBQI BV: Add inverse for more operators. (#1213) commit | commitdiff | tree
2017-10-05 Clark BarrettFix typo in comment. commit | commitdiff | tree
2017-10-05 Mathias PreinerSplit COPYING file, add missing licenses. (#1195) commit | commitdiff | tree
2017-10-05 Andrew ReynoldsMinor change to how SyGus commands are translated to... commit | commitdiff | tree
2017-10-05 Andrew ReynoldsHo model (#1120) commit | commitdiff | tree
2017-10-05 MartinAllow CDHashMaps for objects without default constructo... commit | commitdiff | tree
2017-10-05 Aina NiemetzAdd mkZero, mkOne and mkUmulo to bv utils. (#1200) commit | commitdiff | tree
2017-10-04 Andrew ReynoldsHo quant util (#1119) commit | commitdiff | tree
2017-10-04 Tim KingRemoving the throw specifier from ArrayStoreAll constru... commit | commitdiff | tree
2017-10-04 Andrew ReynoldsAdd regression from #50 regarding "as" parsing in smt2... commit | commitdiff | tree
2017-10-03 Mathias PreinerAdd Cryptominisat and LFSC to --show-config output... commit | commitdiff | tree
2017-10-03 Andrew ReynoldsMove sygus grammar utilities to separate file. (#1184) commit | commitdiff | tree
2017-10-03 Andrew ReynoldsOp overload parser (#1162) commit | commitdiff | tree
2017-10-03 Andres NoetzliAdd initial version of the SMTCOMP2018 run scripts... commit | commitdiff | tree
2017-10-03 Andres NoetzliUnify hash functions for pairs (#1161) commit | commitdiff | tree
2017-10-03 MartinAdd 5 FP kinds for partial to total fn conversion ... commit | commitdiff | tree
next