| 2017-10-20 |
Andrew Reynolds | SyGuS term size limit (#1262) |
commit | commitdiff | tree |
| 2017-10-20 |
Andrew Reynolds | Make Sygus conjectures higher-order (#1244) |
commit | commitdiff | tree |
| 2017-10-19 |
Aina Niemetz | CBQI BV: Refactor solve_bv_constraint. (#1265) |
commit | commitdiff | tree |
| 2017-10-18 |
Andrew Reynolds | Tptp unsat cores (#1228) |
commit | commitdiff | tree |
| 2017-10-18 |
Andrew Reynolds | Strings API escape sequences (#1245) |
commit | commitdiff | tree |
| 2017-10-17 |
Tim King | Making the values argument const in the SetUserAttribut... |
commit | commitdiff | tree |
| 2017-10-17 |
Tim King | Fixing 2 instances of an unused variable. (#1253) |
commit | commitdiff | tree |
| 2017-10-17 |
Clark Barrett | Fix for issue 1247 (#1257) |
commit | commitdiff | tree |
| 2017-10-17 |
Andrew Reynolds | Sygus enumerators to conjecture (#1237) |
commit | commitdiff | tree |
| 2017-10-16 |
Tim King | Adds unit test that show Node and TNode work with for... |
commit | commitdiff | tree |
| 2017-10-13 |
Aina Niemetz | CBQI BV: Added EXTRACT handling. (#1240) |
commit | commitdiff | tree |
| 2017-10-13 |
Andrew Reynolds | CBQI BV quick heuristics (#1239) |
commit | commitdiff | tree |
| 2017-10-12 |
Andrew Reynolds | Initial support for solving bit-vector inequalities... |
commit | commitdiff | tree |
| 2017-10-12 |
Andrew Reynolds | Sygus logics (#1226) |
commit | commitdiff | tree |
| 2017-10-12 |
Aina Niemetz | Enable regressions for CBQI BV and fix inverse for... |
commit | commitdiff | tree |
| 2017-10-12 |
Mathias Preiner | Reduce number of travis builds. |
commit | commitdiff | tree |
| 2017-10-12 |
Mathias Preiner | Add side conditions for UDIV_TOTAL, SHL, CONCAT. (... |
commit | commitdiff | tree |
| 2017-10-11 |
Tim King | Cleaning up ProofArray class. (#1208) |
commit | commitdiff | tree |
| 2017-10-11 |
Andrew Reynolds | Ho Lambda Lifting (#1116) |
commit | commitdiff | tree |
| 2017-10-11 |
Andrew Reynolds | Adds infrastructure for a rewriting pass in BvInstantia... |
commit | commitdiff | tree |
| 2017-10-11 |
Andrew Reynolds | Move unsat core names to smt engine (#1192) |
commit | commitdiff | tree |
| 2017-10-11 |
Andrew Reynolds | Ho node manager types (#1203) |
commit | commitdiff | tree |
| 2017-10-10 |
Aina Niemetz | Add copyright information. (#1201) |
commit | commitdiff | tree |
| 2017-10-10 |
Andres Noetzli | Fix memory leak in quantifiers engine (#1219) |
commit | commitdiff | tree |
| 2017-10-10 |
Martin | Add skeleton of the FP theory solver (#1130) |
commit | commitdiff | tree |
| 2017-10-10 |
Andrew Reynolds | Split term database (#1206) |
commit | commitdiff | tree |
| 2017-10-10 |
Aina Niemetz | CBQI BV: Add inverse for more operators. (#1213) |
commit | commitdiff | tree |
| 2017-10-05 |
Clark Barrett | Fix typo in comment. |
commit | commitdiff | tree |
| 2017-10-05 |
Mathias Preiner | Split COPYING file, add missing licenses. (#1195) |
commit | commitdiff | tree |
| 2017-10-05 |
Andrew Reynolds | Minor change to how SyGus commands are translated to... |
commit | commitdiff | tree |
| 2017-10-05 |
Andrew Reynolds | Ho model (#1120) |
commit | commitdiff | tree |
| 2017-10-05 |
Martin | Allow CDHashMaps for objects without default constructo... |
commit | commitdiff | tree |
| 2017-10-05 |
Aina Niemetz | Add mkZero, mkOne and mkUmulo to bv utils. (#1200) |
commit | commitdiff | tree |
| 2017-10-04 |
Andrew Reynolds | Ho quant util (#1119) |
commit | commitdiff | tree |
| 2017-10-04 |
Tim King | Removing the throw specifier from ArrayStoreAll constru... |
commit | commitdiff | tree |
| 2017-10-04 |
Andrew Reynolds | Add regression from #50 regarding "as" parsing in smt2... |
commit | commitdiff | tree |
| 2017-10-03 |
Mathias Preiner | Add Cryptominisat and LFSC to --show-config output... |
commit | commitdiff | tree |
| 2017-10-03 |
Andrew Reynolds | Move sygus grammar utilities to separate file. (#1184) |
commit | commitdiff | tree |
| 2017-10-03 |
Andrew Reynolds | Op overload parser (#1162) |
commit | commitdiff | tree |
| 2017-10-03 |
Andres Noetzli | Add initial version of the SMTCOMP2018 run scripts... |
commit | commitdiff | tree |
| 2017-10-03 |
Andres Noetzli | Unify hash functions for pairs (#1161) |
commit | commitdiff | tree |
| 2017-10-03 |
Martin | Add 5 FP kinds for partial to total fn conversion ... |
commit | commitdiff | tree |
| 2017-10-02 |
Mathias Preiner | Address comments from PR #1164. (#1174) |
commit | commitdiff | tree |
| 2017-10-02 |
Tim King | Removing throw specifiers from SymbolTable::Implementat... |
commit | commitdiff | tree |
| 2017-10-02 |
Tim King | Removing throw specifiers from TypeEnumeratorBase's... |
commit | commitdiff | tree |
| 2017-10-02 |
Tim King | CID 1457268: Initializing CegConjecture::d_syntax_guide... |
commit | commitdiff | tree |
| 2017-10-01 |
Andrew Reynolds | Refactor check function in last call effort of non... |
commit | commitdiff | tree |
| 2017-09-30 |
Andrew Reynolds | SyGuS streaming solution mode (#1131) |
commit | commitdiff | tree |
| 2017-09-29 |
Mathias Preiner | Move BvInverter class into separate file. (#1173) |
commit | commitdiff | tree |
| 2017-09-29 |
Clark Barrett | A few updates to license files. |
commit | commitdiff | tree |
| 2017-09-29 |
Andres Noetzli | Add license information for GMP |
commit | commitdiff | tree |
| 2017-09-29 |
Andrew Reynolds | Simplify representation of inversion Skolems for bv... |
commit | commitdiff | tree |
| 2017-09-29 |
Andrew Reynolds | Initial working version of BV word-level instantiation... |
commit | commitdiff | tree |
| 2017-09-29 |
Andres Noetzli | Better hash function for pairs (#1157) |
commit | commitdiff | tree |
| 2017-09-29 |
Andrew Reynolds | Update symbol table to support operator overloading... |
commit | commitdiff | tree |
| 2017-09-29 |
Mathias Preiner | Fix output of --show-config for readline. (#1159) |
commit | commitdiff | tree |
| 2017-09-28 |
Andrew Reynolds | Cegqi refactor prep bv (#1155) |
commit | commitdiff | tree |
| 2017-09-28 |
Andrew Reynolds | Improve finite model finding for recursive predicates... |
commit | commitdiff | tree |
| 2017-09-27 |
Andrew Reynolds | Minor fixes for partial quantifier elimination. (#1147) |
commit | commitdiff | tree |
| 2017-09-27 |
Aina Niemetz | CEGQI for BV: Add inverse for BITVECTOR_MULT. (#1153) |
commit | commitdiff | tree |
| 2017-09-27 |
Andrew Reynolds | Add quantifiers API example, fixes #879 (#1146) |
commit | commitdiff | tree |
| 2017-09-27 |
Andres Noetzli | Fix seeking for buffered input (#1145) |
commit | commitdiff | tree |
| 2017-09-27 |
Martin Brain | Fix type checking of to_real (#1127) |
commit | commitdiff | tree |
| 2017-09-27 |
Martin Brain | Improve FP rewriter: const folding, other (#1126) |
commit | commitdiff | tree |
| 2017-09-26 |
Tim King | Fixing CIDs 1172014 and 1172013: Initializing members... |
commit | commitdiff | tree |
| 2017-09-26 |
Tim King | Fixing Cid 1172009 (#1141) |
commit | commitdiff | tree |
| 2017-09-26 |
Tim King | Fixing CID 1172020: Initializing CDHashMap::iterator... |
commit | commitdiff | tree |
| 2017-09-26 |
Tim King | Fixing CID 1362903: Initializing d_bvp to nullptr.... |
commit | commitdiff | tree |
| 2017-09-26 |
Tim King | CID 1362904: Initializing GetInstantiationsCommand... |
commit | commitdiff | tree |
| 2017-09-26 |
Andres Noetzli | Fix build for old GMP version (#1114) |
commit | commitdiff | tree |
| 2017-09-26 |
Tim King | Fixing CIDs 1172012 and 1172011: Initiallzing d_exprMan... |
commit | commitdiff | tree |
| 2017-09-26 |
Andrew Reynolds | Cegqi refactor substitutions (#1129) |
commit | commitdiff | tree |
| 2017-09-25 |
Tim King | Initializing BVMinisat Solver::notify to nullptr. ... |
commit | commitdiff | tree |
| 2017-09-25 |
Andrew Reynolds | Fix bug related to sort inference + subtypes. (#1125) |
commit | commitdiff | tree |
| 2017-09-25 |
Tim King | Fixing CID 1362917: There was a branch where d_issup... |
commit | commitdiff | tree |
| 2017-09-25 |
Tim King | Fixing CID 1362895: Initializing d_bvp to nullptr.... |
commit | commitdiff | tree |
| 2017-09-25 |
Tim King | CID 1362907: Initializing d_smtEngine to nullptr. ... |
commit | commitdiff | tree |
| 2017-09-21 |
Andrew Reynolds | Sygus inv templ refactor (#1110) |
commit | commitdiff | tree |
| 2017-09-21 |
Andrew Reynolds | Extend quantifier-free UF solver to higher-order. This... |
commit | commitdiff | tree |
| 2017-09-20 |
Andres Noetzli | Fix issue #1081, memory leak in cmd executor (#1109) |
commit | commitdiff | tree |
| 2017-09-20 |
Martin | Add FP type enumerator and cardinality computer (#1104) |
commit | commitdiff | tree |
| 2017-09-19 |
Tim King | Fixing a null pointer dereference in the cvc3 compatibi... |
commit | commitdiff | tree |
| 2017-09-19 |
Tim King | Removing a potentially invalid comparison in the TPTP... |
commit | commitdiff | tree |
| 2017-09-19 |
Andres Noetzli | Fix issue #1074, improve non-fatal error handling ... |
commit | commitdiff | tree |
| 2017-09-19 |
Andrew Reynolds | Refactor cegqi instantiation infrastructure so that... |
commit | commitdiff | tree |
| 2017-09-19 |
Andrew Reynolds | Fix issue #1105 involving string to int (#1112) |
commit | commitdiff | tree |
| 2017-09-19 |
Martin | Floating point symfpu support (#1103) |
commit | commitdiff | tree |
| 2017-09-18 |
Tim King | Moving the CVC4_PUBLIC attribute to the beginning of... |
commit | commitdiff | tree |
| 2017-09-15 |
Martin | Make floating-point comparison operators chainable... |
commit | commitdiff | tree |
| 2017-09-15 |
makaimann | Add missing CVC4_PUBLIC in kind_template (#1078) |
commit | commitdiff | tree |
| 2017-09-14 |
Andres Noetzli | Enable ccache compression, increase cache size (#1099) |
commit | commitdiff | tree |
| 2017-09-14 |
Andrew Reynolds | Remove unhandled subtypes (#1098) |
commit | commitdiff | tree |
| 2017-09-14 |
Tim King | Simplifying the throw specifier of SmtEngine::checkSat... |
commit | commitdiff | tree |
| 2017-09-14 |
Martin | Floating point symfpu support (#1093) |
commit | commitdiff | tree |
| 2017-09-14 |
Andrew Reynolds | Add new kinds required for higher-order. (#1083) |
commit | commitdiff | tree |
| 2017-09-14 |
Andrew Reynolds | Add isConst check for lambda expressions. (#1084) |
commit | commitdiff | tree |
| 2017-09-13 |
Andres Noetzli | Make ccache work with Clang on Travis (#1097) |
commit | commitdiff | tree |
| 2017-09-13 |
Andrew Reynolds | Modify equality engine to allow operators to be marked... |
commit | commitdiff | tree |
| 2017-09-13 |
Andres Noetzli | Remove unused RecordSelect and TupleSelect (#1087) |
commit | commitdiff | tree |
| 2017-09-13 |
Andres Noetzli | Enable ccache on Travis, disable debug symbols (#1094) |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog