projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
[proof-new] Optimizing sat proof (#6324)
[cvc5.git] / src /
2021-04-09 Haniel Barbosa[proof-new] Optimizing sat proof (#6324) tree | commitdiff
2021-04-09 Andrew ReynoldsAdd identifiers for extended function reductions (... tree | commitdiff
2021-04-09 Andres NoetzliLearn equalities involving Boolean variables (#6323) tree | commitdiff
2021-04-09 Andrew ReynoldsUse expr miner timeout (#6321) tree | commitdiff
2021-04-09 Gereon KremerAdd missing InferenceIds to toString (#6320) tree | commitdiff
2021-04-08 Andrew ReynoldsUse exceptions when constructing malformed datatypes... tree | commitdiff
2021-04-08 Andrew ReynoldsAdd identifiers for sources of incompleteness (#6311) tree | commitdiff
2021-04-08 Andrew ReynoldsInitial support for parametric datatypes in sygus ... tree | commitdiff
2021-04-07 Aina NiemetzRemove old API header. (#6309) tree | commitdiff
2021-04-07 Andrew ReynoldsAdd cardinality class definition (#6302) tree | commitdiff
2021-04-07 Haniel Barbosa[proof-new] Fixing SMT post-processor's handling of... tree | commitdiff
2021-04-07 Andrew ReynoldsSet incomplete if not applying ho extensionality (... tree | commitdiff
2021-04-07 Andrew ReynoldsFixes for abducts (#6279) tree | commitdiff
2021-04-07 Aina NiemetzNew C++ Api: Rename and move checks.h. (#6306) tree | commitdiff
2021-04-07 Andrew Reynolds(proof-new) Proper implementation of proof node cloning... tree | commitdiff
2021-04-07 Andrew ReynoldsAdd term pools utility (#6243) tree | commitdiff
2021-04-07 Aina NiemetzNew C++ Api: Initial setup of Api documentation. (... tree | commitdiff
2021-04-07 Andrew ReynoldsReplace calls to NodeManager::mkSkolem with SkolemManag... tree | commitdiff
2021-04-07 Mathias Preinercmake: Do not always regenerate cvc4kinds.{pxi,pxd... tree | commitdiff
2021-04-06 Mathias Preinercmake: Add helper to check if a given Python module... tree | commitdiff
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290) tree | commitdiff
2021-04-06 Andrew ReynoldsFix tptp parser for negative rational (#6297) tree | commitdiff
2021-04-06 Andrew ReynoldsFix issue with lemma during equality engine iterator... tree | commitdiff
2021-04-06 Mathias Preinergenkinds: Do not use relative paths to find src directo... tree | commitdiff
2021-04-06 Andrew ReynoldsRemove stdPrintAscii option (#6280) tree | commitdiff
2021-04-06 Aina NiemetzNew C++ Api: Rename and move headers. (#6292) tree | commitdiff
2021-04-06 Mathias Preinerparsekinds: Remove DEFAULT_HEADER. (#6294) tree | commitdiff
2021-04-05 mudathirmahgoubAdd documentation for theory_bags_type_rules.h (#6268) tree | commitdiff
2021-04-05 Andrew ReynoldsFix spurious antecedant for symbolic regular expression... tree | commitdiff
2021-04-05 Haniel Barbosa[proof-new] Registering proof checkers uniformly from... tree | commitdiff
2021-04-05 Andrew ReynoldsEnable UF when pre-skolem nested option is enabled... tree | commitdiff
2021-04-05 NicolaasWeidemanpython: Fix type casting in mkBitVector (#6261) tree | commitdiff
2021-04-05 Andrew ReynoldsFix subtyping for sets care graph (#6278) tree | commitdiff
2021-04-05 Andrew ReynoldsAdd interface for skolem functions in SkolemManager... tree | commitdiff
2021-04-05 Yancheng OuOptimizer for BitVectors (#6213) tree | commitdiff
2021-04-03 Andrew ReynoldsDisable substring component contains in strip endpoints... tree | commitdiff
2021-04-02 Mathias Preinercmake: Do not link against main object library. (#6269) tree | commitdiff
2021-04-02 Gereon KremerNew statistics registry (#6210) tree | commitdiff
2021-04-02 Gereon KremerMinor refactoring (#6273) tree | commitdiff
2021-04-02 Andrew ReynoldsCleaning up friend relationships for commands (#6254) tree | commitdiff
2021-04-02 Andrew ReynoldsFix case where RE unfolding generates a trivially true... tree | commitdiff
2021-04-01 Gereon KremerAdd utility classes for new statistics (#6178) tree | commitdiff
2021-04-01 Andrew ReynoldsSimplify caching of regular expression unfolding (... tree | commitdiff
2021-04-01 Aina NiemetzFP: Factor out symfpu traits. (#6246) tree | commitdiff
2021-04-01 Andrew ReynoldsFix type rule for to_real (#6257) tree | commitdiff
2021-04-01 Gereon KremerRefactor CLN dependency & Cleanup (#6251) tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-04-01 Aina Niemetzkinds: Remove non-existent properties. (#6253) tree | commitdiff
2021-04-01 Andrew Reynolds Add debug traces to theory inference manager (#6250) tree | commitdiff
2021-04-01 Andrew ReynoldsFix non-linear for unknown case (#6252) tree | commitdiff
2021-04-01 Gereon KremerMake ResetCommand go through APISolver (#6172) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-31 Gereon KremerRefactor GMP and Poly dependencies (#6245) tree | commitdiff
2021-03-31 Gereon KremerRefactor dependencies for external SAT solvers (#6215) tree | commitdiff
2021-03-31 Gereon KremerRefactor SymFPU dependency (#6218) tree | commitdiff
2021-03-31 Aina NiemetzBags: Move implementation of type rules from header... tree | commitdiff
2021-03-31 Andrew ReynoldsEliminate dependencies on quantifiers engine in interna... tree | commitdiff
2021-03-31 Andrew ReynoldsAdd missing inference ids (#6242) tree | commitdiff
2021-03-31 Aina NiemetzFP: Move implementation of type rules from header to... tree | commitdiff
2021-03-31 yoni206Fix compilation of Python bindings for named build... tree | commitdiff
2021-03-30 Andrew ReynoldsFix printing for double patterns (#6235) tree | commitdiff
2021-03-30 Andrew ReynoldsMake SEXPR simply typed (#6160) tree | commitdiff
2021-03-30 Andrew ReynoldsImplement simple tracking of instantiation lemmas ... tree | commitdiff
2021-03-30 Andrew ReynoldsRefactoring quantifier annotation kinds, add kinds... tree | commitdiff
2021-03-30 Andrew ReynoldsEliminate use of rational from tptp parser (#6239) tree | commitdiff
2021-03-30 Abdalrhman MohamedGive a better error when sygus grammar rules contain... tree | commitdiff
2021-03-30 Gereon KremerFix total time statistic (#6233) tree | commitdiff
2021-03-30 Andrew ReynoldsMiscellaneous elimination of dependencies on quantifier... tree | commitdiff
2021-03-29 Andrew ReynoldsEliminate the use of quantifiers engine in sygus solver... tree | commitdiff
2021-03-29 Andrew ReynoldsEliminate use of quantifiers engine in enumerative... tree | commitdiff
2021-03-29 Andrew ReynoldsMove decision manager into theory inference manager... tree | commitdiff
2021-03-29 yoni206Modular bv2int part 1 (#6212) tree | commitdiff
2021-03-29 Aina NiemetzFloatingPointLiteral: Constructor for special consts... tree | commitdiff
2021-03-27 Gereon KremerRefactor ANTLR3 dependency (#6202) tree | commitdiff
2021-03-26 Aina NiemetzFloatingPointLiteral: Make constructors that shouldn... tree | commitdiff
2021-03-26 Andrew ReynoldsPass term registry to quantifiers modules (#6216) tree | commitdiff
2021-03-25 Gereon KremerEnsure nonlinear extensions properly reconsiders its... tree | commitdiff
2021-03-25 Aina NiemetzFP: Refactor FloatingPointLiteral in preparation for... tree | commitdiff
2021-03-25 Andrew ReynoldsRefactor construction of triggers (#6209) tree | commitdiff
2021-03-25 Gereon KremerAdd missing includes. (#6207) tree | commitdiff
2021-03-24 Andrew ReynoldsUse inference manager to access intantiate utility... tree | commitdiff
2021-03-24 Gereon KremerOnly consider relevant terms for integer branches ... tree | commitdiff
2021-03-23 Andrew ReynoldsRemove unused code for axioms (#6197) tree | commitdiff
2021-03-23 Haniel BarbosaRemoving unused build options and deprecated proof... tree | commitdiff
2021-03-23 Andrew ReynoldsPassing term registry to ematching utilities (#6190) tree | commitdiff
2021-03-23 Aina NiemetzRemove internal includes of Api header. (#6193) tree | commitdiff
2021-03-23 Abdalrhman MohamedReplace old sygus term reconstruction algorithm with... tree | commitdiff
2021-03-23 Andrew ReynoldsMoving instantiate and skolemize into quantifiers infer... tree | commitdiff
2021-03-22 Gereon KremerMove statistics from the driver into the SmtEngine... tree | commitdiff
2021-03-22 Andrew ReynoldsMove equality query utility into quantifiers model... tree | commitdiff
2021-03-22 Andrew Reynolds Function types are always first-class (#6167) tree | commitdiff
2021-03-22 Andrew ReynoldsAdd skolem definition manager (#6187) tree | commitdiff
2021-03-22 Aina NiemetzFP: Add documentation for FloatingPointLiteral construc... tree | commitdiff
2021-03-22 Andrew ReynoldsGuard for non-unique skolems in term formula removal... tree | commitdiff
2021-03-21 Andrew ReynoldsSimplify strings term registration (#6174) tree | commitdiff
2021-03-21 Andrew ReynoldsClean up remaining raw uses of output channel (#6161) tree | commitdiff
2021-03-20 Andrew ReynoldsImproved tracing for equivalence classes of EE (#6169) tree | commitdiff
2021-03-20 mudathirmahgoubGenerate cvc/Kind.java for the java API (#6143) tree | commitdiff
2021-03-19 Andrew ReynoldsRefactor initialization of quantifiers model and builde... tree | commitdiff
2021-03-19 Aina NiemetzBitVector: Change setBit to set the bit in place. ... tree | commitdiff
next