cvc5.git
2017-11-14 Tim KingCleaning up exporting vectors within commands. Resolves...
2017-11-14 Tim KingInitializes InstPropagator::d_has_relevant_inst. Resolv...
2017-11-14 Tim KingInitializes RegExpOpr::d_char_start and d_char_end...
2017-11-14 Tim KingInitializes TriggerInfo::polarity. Resolves CID 1172054...
2017-11-14 Tim KingInitializes NodeTheoryPair::timestamp in the default...
2017-11-14 Andrew Reynolds(Refactor) Decouple rep set iterator and quantifiers...
2017-11-13 Tim KingInitializing SharedTermsDatabase::d_conflictPolarity...
2017-11-13 Andrew ReynoldsDisable sygus qe preprocessing by default (#1353)
2017-11-13 Andrew ReynoldsImplement enumerator for functions. (#1243)
2017-11-13 Andrew ReynoldsArgument Relevance for Synthesis Conjectures (#1311)
2017-11-13 Tim KingInitializes CegConjectureSingleInvSol::d_root_id. ...
2017-11-13 Tim KingInitializing SortInference::initialSortCount. Resolves...
2017-11-10 Andrew Reynolds(Documentation-only) datatype.h (#1346)
2017-11-10 Andrew ReynoldsPrinting for higher-order (#1347)
2017-11-09 Andrew ReynoldsHigher-order prep (#1338)
2017-11-09 Andrew Reynolds Decouple sygus term database and term database. (...
2017-11-09 Aina NiemetzAdd modular arithmetic operators. (#1321)
2017-11-08 Tim KingInitializing QModelBuilder members. (#1334)
2017-11-08 Tim KingCombining d_conflictHasBeenRaised and d_conflictIndex...
2017-11-08 Tim KingInitializing TrailHashMap::d_uniqueKeys. (#1331)
2017-11-07 Tim King Initialize TimerStat::d_start. (#1330)
2017-11-07 Tim KingInitializing Smt1::d_logic in all cases. This was resol...
2017-11-07 Andrew ReynoldsGuard relevant domain computation properly, minor....
2017-11-07 Tim King Removing an unused member from Tptp. Initializing...
2017-11-07 Tim KingMoving the enum ArithType to partial_model. Adding...
2017-11-07 Andrew ReynoldsAllow FORALL in quantifier elimination command (#1322)
2017-11-07 Tim KingInitializing EquivSygusInvarianceTest::d_conj in the...
2017-11-07 Tim KingInitializing NegContainsSygusInvarianceTest::d_cpbe...
2017-11-07 Tim KingUsing unique_ptr's for members of CegConjecture. (...
2017-11-07 Andrew ReynoldsUpdates to interface for Sygus grammar construction...
2017-11-06 Andrew ReynoldsUnrecurisify rewrite solve assertion for cbqi bv (...
2017-11-06 Aina NiemetzAdd getValue() for Rational and Integer (GMP and CLN...
2017-11-06 Andrew ReynoldsImprove rewriting for string contains part 2 (#1300)
2017-11-05 Andrew ReynoldsMake higher-order a flag in logic info. (#1318)
2017-11-04 Andrew ReynoldsSuppport SAT logic (#1310)
2017-11-04 Andrew ReynoldsFix bv help message. (#1315)
2017-11-03 Andrew ReynoldsSygus clean main (#1297)
2017-11-02 Andrew Reynolds(Move-only) Split quant util (#1306)
2017-11-01 Andrew Reynolds(Refactor) Split term util (#1303)
2017-11-01 Andrew ReynoldsCBQI BV choice expressions (#1296)
2017-11-01 Andres Noetzli Add option to build shared Windows dependencies (...
2017-11-01 Andrew Reynolds(Move-only) Refactor and document theory model part...
2017-10-31 Tim KingCID 1459592: Always checking whether rd is null or...
2017-10-31 Andrew ReynoldsRemove include (#1298)
2017-10-28 Andres NoetzliChange bvudiv semantics based on input language (#1292)
2017-10-28 Andrew Reynolds(Move only) Move enumerative instantiation strategy...
2017-10-28 Andrew ReynoldsSygus process conjecture (#1286)
2017-10-28 Andrew ReynoldsDocument term db (#1220)
2017-10-28 Andrew ReynoldsImprove strings rewriter for contains (#1207)
2017-10-28 Andrew ReynoldsDocument quant arith (#1271)
2017-10-27 Andres NoetzliModify LDFLAGS to support shared libraries for Win...
2017-10-27 Andrew ReynoldsCbqi multiple instantiation (#1289)
2017-10-27 Andrew ReynoldsRefactor theory model (#1236)
2017-10-27 Andrew ReynoldsImplement Hilbert choice operator (#1291)
2017-10-27 Tim KingAdds a macro to SWIG to ignore the override and final...
2017-10-26 Andrew ReynoldsOp overload no fun variant (#1285)
2017-10-26 Andres NoetzliUse uintptr_t for pointer casts in Swig files (#1278)
2017-10-26 Tim KingRemoving throw specifiers from OutputChannel and subcla...
2017-10-25 Tim KingSwitching EqProof to use shared_ptr everywhere. (...
2017-10-25 Aina NiemetzCBQI BV: Add handling for missing operators. (#1274)
2017-10-25 Andrew ReynoldsCbqi bv ineq mode (#1273)
2017-10-24 Andrew ReynoldsRemoving deprecated file. (#1270)
2017-10-24 Mathias PreinerRemove clang-format options introduced in version 5.0.
2017-10-24 Mathias PreinerNew clang-format style based on the Google style. ...
2017-10-24 Aina NiemetzCBQI BV: Add ULT/SLT inverse handling. (#1268)
2017-10-23 Andrew ReynoldsDocument sygus programming-by-examples utility (#1260)
2017-10-21 Mathias PreinerAdd rewriting rules for Eq/Ult with sign_extend and...
2017-10-21 Mathias PreinerSimplify atoms introduced while bitblasting. (#1267)
2017-10-20 Andrew ReynoldsSyGuS term size limit (#1262)
2017-10-20 Andrew ReynoldsMake Sygus conjectures higher-order (#1244)
2017-10-19 Aina NiemetzCBQI BV: Refactor solve_bv_constraint. (#1265)
2017-10-18 Andrew ReynoldsTptp unsat cores (#1228)
2017-10-18 Andrew ReynoldsStrings API escape sequences (#1245)
2017-10-17 Tim KingMaking the values argument const in the SetUserAttribut...
2017-10-17 Tim KingFixing 2 instances of an unused variable. (#1253)
2017-10-17 Clark BarrettFix for issue 1247 (#1257)
2017-10-17 Andrew ReynoldsSygus enumerators to conjecture (#1237)
2017-10-16 Tim KingAdds unit test that show Node and TNode work with for...
2017-10-13 Aina NiemetzCBQI BV: Added EXTRACT handling. (#1240)
2017-10-13 Andrew ReynoldsCBQI BV quick heuristics (#1239)
2017-10-12 Andrew ReynoldsInitial support for solving bit-vector inequalities...
2017-10-12 Andrew ReynoldsSygus logics (#1226)
2017-10-12 Aina NiemetzEnable regressions for CBQI BV and fix inverse for...
2017-10-12 Mathias PreinerReduce number of travis builds.
2017-10-12 Mathias PreinerAdd side conditions for UDIV_TOTAL, SHL, CONCAT. (...
2017-10-11 Tim KingCleaning up ProofArray class. (#1208)
2017-10-11 Andrew ReynoldsHo Lambda Lifting (#1116)
2017-10-11 Andrew ReynoldsAdds infrastructure for a rewriting pass in BvInstantia...
2017-10-11 Andrew ReynoldsMove unsat core names to smt engine (#1192)
2017-10-11 Andrew ReynoldsHo node manager types (#1203)
2017-10-10 Aina NiemetzAdd copyright information. (#1201)
2017-10-10 Andres NoetzliFix memory leak in quantifiers engine (#1219)
2017-10-10 MartinAdd skeleton of the FP theory solver (#1130)
2017-10-10 Andrew ReynoldsSplit term database (#1206)
2017-10-10 Aina NiemetzCBQI BV: Add inverse for more operators. (#1213)
2017-10-05 Clark BarrettFix typo in comment.
2017-10-05 Mathias PreinerSplit COPYING file, add missing licenses. (#1195)
2017-10-05 Andrew ReynoldsMinor change to how SyGus commands are translated to...
2017-10-05 Andrew ReynoldsHo model (#1120)
2017-10-05 MartinAllow CDHashMaps for objects without default constructo...
next