summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2017-10-09Add skeleton of the FP theory solver (#1130)Martin
2017-10-09Split term database (#1206)Andrew Reynolds
2017-10-09CBQI BV: Add inverse for more operators. (#1213)Aina Niemetz
2017-10-05Fix typo in comment.Clark Barrett
2017-10-05Split COPYING file, add missing licenses. (#1195)Mathias Preiner
2017-10-05Minor change to how SyGus commands are translated to SmtEngine commands. This...Andrew Reynolds
2017-10-05Ho model (#1120)Andrew Reynolds
2017-10-05Allow CDHashMaps for objects without default constructors (#1092)Martin
2017-10-04Add mkZero, mkOne and mkUmulo to bv utils. (#1200)Aina Niemetz
2017-10-04Ho quant util (#1119)Andrew Reynolds
2017-10-04Removing the throw specifier from ArrayStoreAll constructor. (#1182)Tim King
2017-10-03Add regression from #50 regarding "as" parsing in smt2 (#1188)Andrew Reynolds
2017-10-03Add Cryptominisat and LFSC to --show-config output. (#1194)Mathias Preiner
2017-10-03Move sygus grammar utilities to separate file. (#1184)Andrew Reynolds
2017-10-03Op overload parser (#1162)Andrew Reynolds
2017-10-03Add initial version of the SMTCOMP2018 run scripts (#1185)Andres Noetzli
2017-10-02Unify hash functions for pairs (#1161)Andres Noetzli
2017-10-02Add 5 FP kinds for partial to total fn conversion (#1128)Martin
2017-10-02Address comments from PR #1164. (#1174)Mathias Preiner
2017-10-02Removing throw specifiers from SymbolTable::Implementation. (#1183)Tim King
2017-10-01Removing throw specifiers from TypeEnumeratorBase's operator* and isFinished....Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback