cvc5.git
2020-10-30 Gereon KremerUse BoundInference in nonlinear extension (#5359)
2020-10-30 Andrew ReynoldsUpdate api::Sort to use TypeNode instead of Type (...
2020-10-29 Andrew ReynoldsSet strings pending conflict flag (#5364)
2020-10-29 mudathirmahgoubAdd mkInteger to the API (#5274)
2020-10-29 Andrew Reynolds(proof-new) Update the strings inference manager for...
2020-10-29 Gereon KremerAdd NodeManager::mkOr() (#5360)
2020-10-28 yoni206run_regression.py to fail on invalid requirements ...
2020-10-28 Andrew ReynoldsRemove more uses of Expr (#5357)
2020-10-28 Andrew ReynoldsFixes for unconstrained variables in nonlinear model...
2020-10-28 Andrew ReynoldsConvert symbol table from Expr-level to Term-level...
2020-10-28 Gereon KremerSplit NlSolver in multiple subsolvers (#5315)
2020-10-28 Andrew ReynoldsAdd rewrites for div/mod in the arithmetic rewriter...
2020-10-27 Mathias Preinerrun_regression: Add --skip-timeout option, lower timeou...
2020-10-27 Abdalrhman... Refactor DeclareSygusVarCommand and SynthFunCommand...
2020-10-27 Andrew ReynoldsAdd missing methods involving datatype sorts to the...
2020-10-27 Gereon KremerDisable --nl-cad option by default (#5350)
2020-10-27 Gereon KremerEnable --nl-cad by default (#5345)
2020-10-27 mudathirmahgoubAdd DUPICATE_REMOVAL operator to bags (#5336)
2020-10-26 Andrew Reynolds(proof-new) Add datatypes proof checker (#5340)
2020-10-26 Andrew ReynoldsSend external equalities from collapse selector as...
2020-10-24 mudathirmahgoubFix issue 5271 (#5335)
2020-10-24 Haniel Barbosa[proof-new] Fix n-ary kind handling in EqEngine explana...
2020-10-23 Andrew ReynoldsApply alpha equivalence to annotated quantified formula...
2020-10-23 Andrew ReynoldsChange datatypes lemma policy for equalities not coming...
2020-10-23 Andrew ReynoldsFix related to preregistering boolean term variables...
2020-10-22 Gereon KremerUse theoryof-mode=type for QF_NRA (#5326)
2020-10-22 Andrew ReynoldsRemove unused equality engine types (#5319)
2020-10-22 mudathirmahgoubFix issue 5309 (#5327)
2020-10-22 Andrew Reynolds(proof-new) Make theory preprocessor user-context depen...
2020-10-21 Gereon Kremer(proof-new) Make circuit propagator proof producing...
2020-10-21 mudathirmahgoubImplement bags evaluator (#5322)
2020-10-21 Alex Ozdemir(proof-new) Add arith proof macros file to CMake (...
2020-10-21 Alex Ozdemir(proof-new) arith: dedup literals in flattenImpl (...
2020-10-21 Andrew Reynolds(proof-new) Updates to lazy proof chain (#5317)
2020-10-21 mudathirmahgoubAdd operator MakeBagOp for constructing bags (#5209)
2020-10-21 Abdalrhman... Add finishInit for getInterpol and getAbduct. (#5316)
2020-10-21 Andrew Reynolds(proof-new) Fixes for proofs in rewriter (#5307)
2020-10-20 Aina NiemetzFix compiler warnings. (#5305)
2020-10-20 Gereon Kremer(proof-new) Add proofs for circuit propagator (#5301)
2020-10-20 Andrew Reynolds(proof-new) Fix for CDProof::isSame (#5297)
2020-10-20 Andrew Reynolds(proof-new) Update add lazy step interface in LazyCDPro...
2020-10-20 Abdalrhman... Remove some Commands from the API. (#5268)
2020-10-20 Andrew ReynoldsFix miscellaneous warnings (#5256)
2020-10-20 Andrew ReynoldsMake seq.nth a trigger kind (#5314)
2020-10-20 Gereon KremerHandle rewrite to bool in BoundInference (#5311)
2020-10-20 Andrew ReynoldsSplit CheckModels utility to its own file (#5303)
2020-10-20 Aina NiemetzInteger (CLN): Minor improvements. (#5306)
2020-10-20 yoni206Expand `seq.nth` lazily (#5287)
2020-10-19 Aina NiemetzInteger: CLN: Move implementation of member functions...
2020-10-19 Haniel Barbosa[proof-new] Fixing resolution proof checker (#5262)
2020-10-19 Andrew Reynolds(proof-new) Updates to assertions pipeline and preproce...
2020-10-19 Andrew Reynolds(proof-new) Update preprocessing pass context for proof...
2020-10-19 Haniel Barbosa[proof-new] Improving cycle checking in lazycdproofchai...
2020-10-19 Andrew ReynoldsSafer version of pending lemma processing in inference...
2020-10-19 Andrew Reynolds(proof-new) Refactoring cyclic checks (#5291)
2020-10-18 Andrew Reynolds (proof-new) Witness axiom reconstruction for purificat...
2020-10-18 Andrew Reynolds(proof-new) Implementation of trust substitution (...
2020-10-18 Andrew Reynolds(proof-new) More features for SMT proof post-processor...
2020-10-18 Andrew Reynolds(proof-new) Improvements for theory engine (#5292)
2020-10-16 Andrew ReynoldsRefactor SMT-level model object (#5277)
2020-10-16 Andrew ReynoldsCatch more cases of nested recursion in datatypes ...
2020-10-16 yoni206bv2int: caching introduced terms (#5283)
2020-10-16 Andrew ReynoldsAdd inference enumeration to datatypes (#5275)
2020-10-15 Alex Ozdemir(proof-new) TheoryArithPrivate: farkas lemma proof...
2020-10-14 mudathirmahgoubFix issue #5269 (#5270)
2020-10-14 yoni206bv2int: implementing the iand-sum mode (#5265)
2020-10-14 Alex Ozdemir(proof-new) debug statements & docs for INT_TRUST ...
2020-10-14 Alex Ozdemir(proof-new) pfs in TheoryArith(Private) explainations...
2020-10-14 Andrew ReynoldsGuard uses of printing approximations for constants...
2020-10-14 Alex Ozdemir(proof-new) pfs for conflicts in TheoryArithPrivate...
2020-10-14 yoni206bv2int: rewritings and unsat cores (#5263)
2020-10-14 Haniel Barbosausing NOT_NOT_ELIM rather than macros to do double...
2020-10-14 Alex Ozdemir(proof-new) Prove lemmas in Constraint (#5254)
2020-10-14 Andrew Reynolds(proof-new) Generalize preprocess proof generator ...
2020-10-14 Andrew Reynolds(proof-new) Simplifications for proof rule checker...
2020-10-14 Andrew Reynolds (proof-new) Miscellaneous minor improvements and fixes...
2020-10-13 Andrew Reynolds(proof-new) New rules for Booleans (#5243)
2020-10-13 Andrew Reynolds(proof-new) Change merge policy for proof node updater...
2020-10-13 yoni206bv2int: improving bvand tables (#5235)
2020-10-12 Andrew ReynoldsRemove uf-ss-totality option (#5251)
2020-10-12 Andrew ReynoldsEliminate uses of Expr in SmtEngine interface (#5240)
2020-10-12 Andrew ReynoldsEnsure uninterpreted sort owner is UF if uf-ho or finit...
2020-10-11 Mathias PreinerSyGuS instantiation modes (#5228)
2020-10-11 Gereon KremerAdd conversion of poly polynomial to cvc node. (#5218)
2020-10-10 Abdalrhman... Provide API version of some SMT Commands. (#5222)
2020-10-10 yoni206bv2int: bvand translation code move (#5227)
2020-10-09 Mathias PreinerRemove deprecated add-path commands and use $GITHUB_PAT...
2020-10-09 Alex Ozdemiruse right arith explanation fn to fix regressions ...
2020-10-09 Alex Ozdemir(proof-new) proofs for arith-constraint explanations...
2020-10-09 Andres Noetzlireset-assertions: Remove all non-global symbols in...
2020-10-09 Andrew ReynoldsSimplify approach for collapsed selectors over non...
2020-10-09 Andrew Reynolds(proof-new) Add lazy proof set utility (#5221)
2020-10-09 Andrew Reynolds(proof-new) Theory engine proof producing (#5195)
2020-10-08 Andrew Reynolds(proof-new) Fixes and improvements for smt proof postpr...
2020-10-08 makaimannGet correct NodeManagerScope for toStrings in API ...
2020-10-08 yoni206fix unit failures on debug without symfpu (#5212)
2020-10-07 Alex Ozdemir(proof-new) proofs in ee -> arith pipeline (#5215)
2020-10-07 Aina NiemetzNew C++ API: Rename Term::isConst() to Term::isValue...
2020-10-07 Gereon KremerMake sure conflicts are not rewritten (in arithmetic...
2020-10-07 Andrew Reynolds(proof-new) Add the strings proof constructor (#4903)
next