cvc5.git
2017-11-21 Andrew ReynoldsCegqi bv remove extract terms preprocess pass (#1376)
2017-11-20 Tim KingInitializes members of QuantInfo. Resolves CID 1362929...
2017-11-20 Tim KingRemoving an unused variable from SygusInput. Resolves...
2017-11-19 Andrew ReynoldsHo instantiation (#1204)
2017-11-19 Tim KingNames the Effort enum of QuantConflictFind class. ...
2017-11-17 Andrew Reynolds(Refactor) Document and clean single invocation partiti...
2017-11-17 Aina NiemetzAdd random number generator. (#1370)
2017-11-16 Andrew Reynolds(Refactor) Arithmetic monomial sum (#1381)
2017-11-16 Tim KingInitializes BitVectorProof::d_isAssumptionConflict...
2017-11-15 Andrew ReynoldsSygus print callbacks (#1348)
2017-11-15 Andrew ReynoldsReenable some regressions, minor. (#1369)
2017-11-15 Tim KingRemoves an unused variable from Theory. (#1375)
2017-11-15 Tim KingInitializing members of Datatype. Addresses CIDs 136289...
2017-11-15 Tim KingAdding garbage collection for Proof objects. (#1294)
2017-11-15 Andrew ReynoldsMake QEffort an enum (#1366)
2017-11-14 Andrew Reynolds(Refactor) Split sygus term db (#1335)
2017-11-14 Andrew ReynoldsClean Ceg Instantiators (#1365)
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...
next