summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-11-07Guard relevant domain computation properly, minor. (#1325)Andrew Reynolds
2017-11-07 Removing an unused member from Tptp. Initializing members of Tptp. (#1326)Tim King
2017-11-07Moving the enum ArithType to partial_model. Adding a new type Unset in the en...Tim King
2017-11-07Allow FORALL in quantifier elimination command (#1322)Andrew Reynolds
2017-11-07Initializing EquivSygusInvarianceTest::d_conj in the constructor. (#1327)Tim King
2017-11-07Initializing NegContainsSygusInvarianceTest::d_cpbe in constructor. (#1328)Tim King
2017-11-06Using unique_ptr's for members of CegConjecture. (#1324)Tim King
2017-11-06Updates to interface for Sygus grammar construction. (#1323)Andrew Reynolds
2017-11-06Unrecurisify rewrite solve assertion for cbqi bv (#1312)Andrew Reynolds
2017-11-06Add getValue() for Rational and Integer (GMP and CLN). (#1309)Aina Niemetz
2017-11-05Improve rewriting for string contains part 2 (#1300)Andrew Reynolds
2017-11-05Make higher-order a flag in logic info. (#1318)Andrew Reynolds
2017-11-03Suppport SAT logic (#1310)Andrew Reynolds
2017-11-03Fix bv help message. (#1315)Andrew Reynolds
2017-11-03Sygus clean main (#1297)Andrew Reynolds
2017-11-01(Move-only) Split quant util (#1306)Andrew Reynolds
2017-11-01(Refactor) Split term util (#1303)Andrew Reynolds
2017-11-01CBQI BV choice expressions (#1296)Andrew Reynolds
2017-11-01 Add option to build shared Windows dependencies (#1282)Andres Noetzli
2017-11-01(Move-only) Refactor and document theory model part 2 (#1305)Andrew Reynolds
2017-10-31CID 1459592: Always checking whether rd is null or not. (#1299)Tim King
2017-10-30Remove include (#1298)Andrew Reynolds
2017-10-28Change bvudiv semantics based on input language (#1292)Andres Noetzli
2017-10-28(Move only) Move enumerative instantiation strategy to its own file and docum...Andrew Reynolds
2017-10-28Sygus process conjecture (#1286)Andrew Reynolds
2017-10-28Document term db (#1220)Andrew Reynolds
2017-10-27Improve strings rewriter for contains (#1207)Andrew Reynolds
2017-10-27Document quant arith (#1271)Andrew Reynolds
2017-10-27Modify LDFLAGS to support shared libraries for Win (#1280)Andres Noetzli
2017-10-27Cbqi multiple instantiation (#1289)Andrew Reynolds
2017-10-27Refactor theory model (#1236)Andrew Reynolds
2017-10-27Implement Hilbert choice operator (#1291)Andrew Reynolds
2017-10-26Adds a macro to SWIG to ignore the override and final C++11 keywords in older...Tim King
2017-10-26Op overload no fun variant (#1285)Andrew Reynolds
2017-10-25Use uintptr_t for pointer casts in Swig files (#1278)Andres Noetzli
2017-10-25Removing throw specifiers from OutputChannel and subclasses. (#1209)Tim King
2017-10-25Switching EqProof to use shared_ptr everywhere. (#1217)Tim King
2017-10-25CBQI BV: Add handling for missing operators. (#1274)Aina Niemetz
2017-10-24Cbqi bv ineq mode (#1273)Andrew Reynolds
2017-10-24Removing deprecated file. (#1270)Andrew Reynolds
2017-10-24Remove clang-format options introduced in version 5.0.Mathias Preiner
2017-10-24New clang-format style based on the Google style. (#1264)Mathias Preiner
2017-10-23CBQI BV: Add ULT/SLT inverse handling. (#1268)Aina Niemetz
2017-10-23Document sygus programming-by-examples utility (#1260)Andrew Reynolds
2017-10-20Add rewriting rules for Eq/Ult with sign_extend and constants. (#1258)Mathias Preiner
2017-10-20Simplify atoms introduced while bitblasting. (#1267)Mathias Preiner
2017-10-20SyGuS term size limit (#1262)Andrew Reynolds
2017-10-20Make Sygus conjectures higher-order (#1244)Andrew Reynolds
2017-10-19CBQI BV: Refactor solve_bv_constraint. (#1265)Aina Niemetz
2017-10-18Tptp unsat cores (#1228)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback