projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
[proof-new] Fix arity check when building equality engine proofs (#6133)
[cvc5.git] / src /
2021-03-12 Haniel Barbosa[proof-new] Fix arity check when building equality... tree | commitdiff
2021-03-12 Gereon KremerAdd missing includes for statistics (#6124) tree | commitdiff
2021-03-12 Andrew ReynoldsSimplify instantiation match generator interface (... tree | commitdiff
2021-03-11 Gereon KremerMake linear arithmetic use its inference manager (... tree | commitdiff
2021-03-11 Alex Ozdemirarith proof rules shuffle & add ARITH_SUM_UB (#6118) tree | commitdiff
2021-03-11 Andrew ReynoldsIntroduce inference ids for quantifier instantiation... tree | commitdiff
2021-03-11 Gereon KremerFirst refactoring of statistics classes (#6105) tree | commitdiff
2021-03-11 Aina NiemetzDelete Expr layer. (#6117) tree | commitdiff
2021-03-11 MikolasJanotaImprovements and refactoring for enumeratative strategy... tree | commitdiff
2021-03-11 Andrew Reynolds(proof-new) Clean up uses of witness with skolem lemmas... tree | commitdiff
2021-03-11 Andrew ReynoldsDirect lemmas and inference ids for sygus extension... tree | commitdiff
2021-03-11 Mathias PreinerFix compile warnings when compiling with GLPK. (#6115) tree | commitdiff
2021-03-11 Aina NiemetzClean up ownership of Datatypes in NodeManager. (#6113) tree | commitdiff
2021-03-11 Aina NiemetzRefactor Node::getOperator() to fix compiler warning... tree | commitdiff
2021-03-11 Mathias PreinerUse CVC4_ASSERTIONS instead of NDEBUG. (#6099) tree | commitdiff
2021-03-10 Mathias PreinerUse Assert instead of assert. (#6095) tree | commitdiff
2021-03-10 Aina NiemetzNew C++ Api: Add missing argument checks in Solver... tree | commitdiff
2021-03-10 Andrew ReynoldsAdd Env class (#6093) tree | commitdiff
2021-03-10 Haniel Barbosa[proof-new] Clarifying doc (#6108) tree | commitdiff
2021-03-10 Aina NiemetzMove ExprManager::isNAryKind to NodeManager. (#6107) tree | commitdiff
2021-03-10 Gereon KremerImprove arithmetic proofs (#6106) tree | commitdiff
2021-03-10 Andrew Reynolds(proof-new) Update ppRewrite to use skolem lemmas ... tree | commitdiff
2021-03-10 Andrew ReynoldsFix extended equality rewrite involving replace. (... tree | commitdiff
2021-03-10 Andrew ReynoldsFix term registration and non-theory-preprocessed terms... tree | commitdiff
2021-03-10 Andrew Reynolds(proof-new) Replace witness form by original form in... tree | commitdiff
2021-03-09 Aina NiemetzNew C++ Api: Use const ref for arguments when possible... tree | commitdiff
2021-03-09 Andrew ReynoldsMerge initialization steps in TheoryModelBuilder (... tree | commitdiff
2021-03-09 Andrew ReynoldsRemove logic request (#6089) tree | commitdiff
2021-03-09 Aina NiemetzNew C++ Api: Migrate stats collection for consts, vars... tree | commitdiff
2021-03-09 Aina NiemetzContextObj::destroy(): Guard against invalid use. ... tree | commitdiff
2021-03-09 Aina NiemetzNew C++ Api: Clean up usage of internal kind. (#6087) tree | commitdiff
2021-03-09 Andrew Reynolds(proof-new) Minor fix and allow proof option (#6085) tree | commitdiff
2021-03-09 Aina NiemetzNew C++ API: Reorder and clean up cpp file. (#6086) tree | commitdiff
2021-03-09 Gereon KremerAdd missing include if GLPK is enabled. (#6084) tree | commitdiff
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-09 Aina NiemetzNew C++ API: Migrate to Node layer. (#6070) tree | commitdiff
2021-03-08 Andrew ReynoldsFix handling of negation of Boolean bound variables... tree | commitdiff
2021-03-08 Andrew Reynolds(proof-new) Separating optimizations for strings skolem... tree | commitdiff
2021-03-08 Andrew Reynolds(proof-new) Prepare arithmetic for changes to ppRewrite... tree | commitdiff
2021-03-08 Andrew ReynoldsSimplify theory preprocessing (#6058) tree | commitdiff
2021-03-08 Gereon KremerFix justification heuristic again (#6074) tree | commitdiff
2021-03-08 Andrew ReynoldsDo not process conjunctions as facts in strings (#6065) tree | commitdiff
2021-03-06 Mathias PreinerRemove partial UDIV/UREM operators. (#6069) tree | commitdiff
2021-03-06 Mathias PreinerRemove SMT-LIB 2.5 and 2.0 support. (#6068) tree | commitdiff
2021-03-05 mcjunehoInitial implementation of an optimization solver with... tree | commitdiff
2021-03-05 Gereon KremerReimplement time limit mechanism for windows (#6049) tree | commitdiff
2021-03-04 Aina NiemetzNew C++ API: Clean up usage of interal datatype classes... tree | commitdiff
2021-03-04 Aina NiemetzAdd initial bit-blaster for proof logging. (#6053) tree | commitdiff
2021-03-04 Aina NiemetzNew C++ Api: Clean up usage of internal types in Term... tree | commitdiff
2021-03-04 Gereon KremerAdd proper define for libpoly usage (#6050) tree | commitdiff
2021-03-04 Gereon KremerIgnore isInConflict when adding conflicts (#5995) tree | commitdiff
2021-03-04 Aina NiemetzNew C++ API: Clean up usage of internal Type/TypeNodes... tree | commitdiff
2021-03-04 Aina NiemetzNew C++ API: Clean up usage of internal Result. (#6043) tree | commitdiff
2021-03-04 Aina NiemetzNew C++ API: Clean up usage of internal types in Op... tree | commitdiff
2021-03-03 Andrew Reynolds(proof-new) Simplifications to arithmetic operator... tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-03 Abdalrhman MohamedRemove uses of SExpr class. (#6035) tree | commitdiff
2021-03-03 mudathirmahgoubAdd tuple projection operator (#5904) tree | commitdiff
2021-03-02 Mathias PreinerRemove non-ASCII characters from source files. (#6039) tree | commitdiff
2021-03-02 Gereon KremerImprove handling of utf8 encoded inputs (#5694) tree | commitdiff
2021-03-02 Mathias PreinerAdd aarch64 (ARM64) cross-compile support. (#6033) tree | commitdiff
2021-03-02 Mathias PreinerFix nightly errors. (#6034) tree | commitdiff
2021-03-02 Andrew ReynoldsIntroduce quantifiers term registry (#5983) tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-03-01 Gereon KremerRefactor collection of debug and trace tags (#5996) tree | commitdiff
2021-02-27 Aina Niemetzgoogle test: theory: Migrate theory_white. (#6006) tree | commitdiff
2021-02-26 Haniel BarbosaSome formatting and better tracing in prop engine ... tree | commitdiff
2021-02-26 Andrew ReynoldsMinor improvement and fix to smt2 printer (#6009) tree | commitdiff
2021-02-26 Andrew ReynoldsOptionally permit creation of non-flat function types... tree | commitdiff
2021-02-26 Gereon KremerStore Node instead of TNode (#5993) tree | commitdiff
2021-02-26 Andrew Reynolds(proof-new) Fix regular expression unfolding under... tree | commitdiff
2021-02-25 Gereon KremerMove (optional) rewrite from TrustSubstitutionMap to... tree | commitdiff
2021-02-25 yoni206Datatypes lemmas: share only external types (#5997) tree | commitdiff
2021-02-25 Mathias PreinerEnable -Werror. (#5969) tree | commitdiff
2021-02-24 Gereon KremerEnsure static-learning adds rewritten assertions. ... tree | commitdiff
2021-02-24 Gereon Kremer(proof-new) Add proofs for CAD solver (#5981) tree | commitdiff
2021-02-24 Andrew ReynoldsAdd state and inference manager to inst match generator... tree | commitdiff
2021-02-24 Andrew ReynoldsAdd interface to TheoryState for sort inference and... tree | commitdiff
2021-02-23 Mathias PreinerSwitch to C++17. (#5959) tree | commitdiff
2021-02-23 Gereon KremerAdd proof for mult sign lemma (#5966) tree | commitdiff
2021-02-23 Haniel Barbosa[proof-new] Fix dangling pointer in SAT proof generatio... tree | commitdiff
2021-02-23 Gereon KremerAdd proof for monomial bounds check (#5965) tree | commitdiff
2021-02-23 Gereon Kremer(proof-new) Add proof generator for CAD solver (#5964) tree | commitdiff
2021-02-23 Haniel Barbosa[proof-new] Fix handling of removable clauses in proof... tree | commitdiff
2021-02-23 Gereon KremerAdd trans secant proofs. (#5957) tree | commitdiff
2021-02-23 Andrew ReynoldsExplanation of failure for instantiate, use in enumerat... tree | commitdiff
2021-02-22 Andrew ReynoldsEliminate raw use of output channel and valuation in... tree | commitdiff
2021-02-22 Andrew ReynoldsMove quantifiers attributes to quantifiers registry... tree | commitdiff
2021-02-22 Andrew Reynolds(proof-new) Change proof-new option to proof (#5955) tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add proofs for exponential functions (... tree | commitdiff
2021-02-22 Andrew ReynoldsRequire length-in-conclusion form for strings inference... tree | commitdiff
2021-02-22 Andrew Reynolds(proof-new) Option to automatically add SYMM steps... tree | commitdiff
2021-02-22 Haniel Barbosa[proof-new] Optionally print conclusion in the AST... tree | commitdiff
2021-02-22 Gereon KremerAdd the LazyTreeProofGenerator. (#5948) tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDIC... tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add proofs for sine lemmas in the transcend... tree | commitdiff
2021-02-22 Gereon KremerCleanup in transcendental solver, add ApproximationBoun... tree | commitdiff
2021-02-22 Gereon Kremeradd pruneRedundantIntervals (#5950) tree | commitdiff
2021-02-22 Andrew ReynoldsFix datatypes inference manager when proofs are enabled... tree | commitdiff
next