summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-28Merge branch 'master' into div_semanticsdiv_semanticsAndrew Reynolds
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-26clang formatAndres Noetzli
2017-10-26Change bvudiv semantics based on input languageAndres Noetzli
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
2017-10-18Strings API escape sequences (#1245)Andrew Reynolds
2017-10-17Making the values argument const in the SetUserAttributeCommand const… (#1249)Tim King
2017-10-17Fixing 2 instances of an unused variable. (#1253)Tim King
2017-10-16Fix for issue 1247 (#1257)Clark Barrett
2017-10-16Sygus enumerators to conjecture (#1237)Andrew Reynolds
2017-10-16Adds unit test that show Node and TNode work with for each loops. (#1230)Tim King
2017-10-13CBQI BV: Added EXTRACT handling. (#1240)Aina Niemetz
2017-10-12CBQI BV quick heuristics (#1239)Andrew Reynolds
2017-10-12Initial support for solving bit-vector inequalities (#1229)Andrew Reynolds
2017-10-12Sygus logics (#1226)Andrew Reynolds
2017-10-11Enable regressions for CBQI BV and fix inverse for LSHR. (#1234)Aina Niemetz
2017-10-11Reduce number of travis builds.Mathias Preiner
2017-10-11Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)Mathias Preiner
2017-10-11Cleaning up ProofArray class. (#1208)Tim King
2017-10-11Ho Lambda Lifting (#1116)Andrew Reynolds
2017-10-11Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion ...Andrew Reynolds
2017-10-11Move unsat core names to smt engine (#1192)Andrew Reynolds
2017-10-10Ho node manager types (#1203)Andrew Reynolds
2017-10-10Add copyright information. (#1201)Aina Niemetz
2017-10-10Fix memory leak in quantifiers engine (#1219)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback