projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Improve arithmetic proofs (#6106)
[cvc5.git] / src /
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
2021-02-19 Andrew ReynoldsSimplify interface to instantiate (#5926) tree | commitdiff
2021-02-19 Andrew ReynoldsFill in missing inference ids in datatypes theory ... tree | commitdiff
2021-02-19 Andrew ReynoldsRefactoring theory inference process (#5920) tree | commitdiff
2021-02-19 Andrew ReynoldsFix rewrite for contains over replace (#5924) tree | commitdiff
2021-02-19 Andrew ReynoldsRemove string stat for inferences (#5932) tree | commitdiff
2021-02-19 Gereon KremerCleanup of inferences in arithmetic theory (#5927) tree | commitdiff
2021-02-18 Gereon KremerAdd statistic for InferenceId to TheoryInferenceManager... tree | commitdiff
2021-02-18 Gereon KremerAdd InferenceIds for sets theory. (#5900) tree | commitdiff
2021-02-18 Gereon KremerNew InferenceIds for BV theory (#5909) tree | commitdiff
2021-02-18 Andrew ReynoldsDocument UF inferences (#5917) tree | commitdiff
2021-02-18 Andrew ReynoldsEliminate non-static members in term util (#5919) tree | commitdiff
2021-02-18 Andrew ReynoldsMove first order model for full model check to own... tree | commitdiff
2021-02-17 Andrew ReynoldsMove methods from term util to quantifiers registry... tree | commitdiff
2021-02-17 Andrew ReynoldsCompute fact or lemma in datatypes prior to buffering... tree | commitdiff
2021-02-17 Gereon KremerUse InferenceId in sep theory. (#5912) tree | commitdiff
2021-02-17 Gereon KremerTheoryIds for UF theory. (#5901) tree | commitdiff
2021-02-17 Gereon KremerAdd InferenceIds for theory of arrays (#5910) tree | commitdiff
2021-02-17 Gereon KremerAdd InferenceId to buffered inference manager (#5911) tree | commitdiff
2021-02-17 Gereon KremerAdd new IntegralHistogramStat (#5898) tree | commitdiff
2021-02-17 Mathias PreinerAdd bit-level propagation support to BV bitblast solver... tree | commitdiff
next