cvc5.git
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...
2017-10-05 Aina NiemetzAdd mkZero, mkOne and mkUmulo to bv utils. (#1200)
2017-10-04 Andrew ReynoldsHo quant util (#1119)
2017-10-04 Tim KingRemoving the throw specifier from ArrayStoreAll constru...
2017-10-04 Andrew ReynoldsAdd regression from #50 regarding "as" parsing in smt2...
2017-10-03 Mathias PreinerAdd Cryptominisat and LFSC to --show-config output...
2017-10-03 Andrew ReynoldsMove sygus grammar utilities to separate file. (#1184)
2017-10-03 Andrew ReynoldsOp overload parser (#1162)
2017-10-03 Andres NoetzliAdd initial version of the SMTCOMP2018 run scripts...
2017-10-03 Andres NoetzliUnify hash functions for pairs (#1161)
2017-10-03 MartinAdd 5 FP kinds for partial to total fn conversion ...
2017-10-02 Mathias PreinerAddress comments from PR #1164. (#1174)
2017-10-02 Tim KingRemoving throw specifiers from SymbolTable::Implementat...
2017-10-02 Tim KingRemoving throw specifiers from TypeEnumeratorBase's...
2017-10-02 Tim KingCID 1457268: Initializing CegConjecture::d_syntax_guide...
2017-10-01 Andrew ReynoldsRefactor check function in last call effort of non...
2017-09-30 Andrew ReynoldsSyGuS streaming solution mode (#1131)
2017-09-29 Mathias PreinerMove BvInverter class into separate file. (#1173)
2017-09-29 Clark BarrettA few updates to license files.
2017-09-29 Andres NoetzliAdd license information for GMP
2017-09-29 Andrew ReynoldsSimplify representation of inversion Skolems for bv...
2017-09-29 Andrew ReynoldsInitial working version of BV word-level instantiation...
2017-09-29 Andres NoetzliBetter hash function for pairs (#1157)
2017-09-29 Andrew ReynoldsUpdate symbol table to support operator overloading...
2017-09-29 Mathias PreinerFix output of --show-config for readline. (#1159)
2017-09-28 Andrew ReynoldsCegqi refactor prep bv (#1155)
2017-09-28 Andrew ReynoldsImprove finite model finding for recursive predicates...
2017-09-27 Andrew ReynoldsMinor fixes for partial quantifier elimination. (#1147)
2017-09-27 Aina NiemetzCEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153)
2017-09-27 Andrew ReynoldsAdd quantifiers API example, fixes #879 (#1146)
2017-09-27 Andres NoetzliFix seeking for buffered input (#1145)
2017-09-27 Martin BrainFix type checking of to_real (#1127)
2017-09-27 Martin BrainImprove FP rewriter: const folding, other (#1126)
2017-09-26 Tim KingFixing CIDs 1172014 and 1172013: Initializing members...
2017-09-26 Tim KingFixing Cid 1172009 (#1141)
2017-09-26 Tim KingFixing CID 1172020: Initializing CDHashMap::iterator...
2017-09-26 Tim KingFixing CID 1362903: Initializing d_bvp to nullptr....
2017-09-26 Tim KingCID 1362904: Initializing GetInstantiationsCommand...
2017-09-26 Andres NoetzliFix build for old GMP version (#1114)
2017-09-26 Tim KingFixing CIDs 1172012 and 1172011: Initiallzing d_exprMan...
2017-09-26 Andrew ReynoldsCegqi refactor substitutions (#1129)
2017-09-25 Tim KingInitializing BVMinisat Solver::notify to nullptr. ...
2017-09-25 Andrew ReynoldsFix bug related to sort inference + subtypes. (#1125)
2017-09-25 Tim KingFixing CID 1362917: There was a branch where d_issup...
2017-09-25 Tim KingFixing CID 1362895: Initializing d_bvp to nullptr....
2017-09-25 Tim KingCID 1362907: Initializing d_smtEngine to nullptr. ...
2017-09-21 Andrew ReynoldsSygus inv templ refactor (#1110)
2017-09-21 Andrew ReynoldsExtend quantifier-free UF solver to higher-order. This...
2017-09-20 Andres NoetzliFix issue #1081, memory leak in cmd executor (#1109)
2017-09-20 MartinAdd FP type enumerator and cardinality computer (#1104)
2017-09-19 Tim KingFixing a null pointer dereference in the cvc3 compatibi...
2017-09-19 Tim KingRemoving a potentially invalid comparison in the TPTP...
2017-09-19 Andres NoetzliFix issue #1074, improve non-fatal error handling ...
2017-09-19 Andrew ReynoldsRefactor cegqi instantiation infrastructure so that...
2017-09-19 Andrew ReynoldsFix issue #1105 involving string to int (#1112)
2017-09-19 MartinFloating point symfpu support (#1103)
2017-09-18 Tim KingMoving the CVC4_PUBLIC attribute to the beginning of...
2017-09-15 MartinMake floating-point comparison operators chainable...
2017-09-15 makaimannAdd missing CVC4_PUBLIC in kind_template (#1078)
2017-09-14 Andres NoetzliEnable ccache compression, increase cache size (#1099)
2017-09-14 Andrew ReynoldsRemove unhandled subtypes (#1098)
next