cvc5.git
2020-11-16 Gereon KremerImprove accuracy of resource limitation (#4763)
2020-11-14 Andrew ReynoldsFix double conflict in extended string solver (#5435)
2020-11-14 Andrew Reynolds(proof-new) Proofs for non-clausal simplification ...
2020-11-13 Andrew Reynolds(proof-new) Enable proofs for datatypes (#5436)
2020-11-13 yoni206Model declarations printing options (#5432)
2020-11-13 Andrew ReynoldsAdd more features to symbol manager (#5434)
2020-11-13 Andrew ReynoldsMake regular expression difference left associative...
2020-11-12 Andrew ReynoldsSimplify sygus solver and sygus stream (#5389)
2020-11-12 Andrew ReynoldsFix printing of define named function (#5425)
2020-11-12 yoni206Models standard (#5415)
2020-11-12 Andrew Reynolds(proof-new) Separate explanation stages in proof equali...
2020-11-12 Andrew ReynoldsFix redundant refinement lemma in sygus solver (#5399)
2020-11-12 Andrew Reynolds(proof-new) Proofs for skolemization (#5339)
2020-11-12 Andrew Reynolds(proof-new) Fix true explanations of propagations in...
2020-11-12 Andrew Reynolds(proof-new) Improve printing and debugging for pedantic...
2020-11-12 Andrew Reynolds(proof-new) Add datatypes inference to proof constructo...
2020-11-12 Andrew ReynoldsMake symbol manager context dependent (#5424)
2020-11-11 Andrew ReynoldsMove symbol manager to src/expr/ (#5420)
2020-11-11 Andrew ReynoldsRewrite witness terms at prerewrite (#5419)
2020-11-11 Andrew ReynoldsAdd simple substitution utility (#5397)
2020-11-11 Andrew ReynoldsPass symbol manager to commands (#5410)
2020-11-11 Andrew ReynoldsFix preregistration in TheorySep before declare-heap...
2020-11-10 Andrew ReynoldsDo not mark extended functions as reduced based on...
2020-11-10 Alex OzdemirPin LFSC version (#5412)
2020-11-10 Andrew ReynoldsMake mkGroundTerm deterministic (#5347)
2020-11-10 Andrew ReynoldsAdd getSubtermKinds to node algorithm (#5398)
2020-11-10 Andrew ReynoldsAdd proper support for the declare-heap command for...
2020-11-10 Andrew ReynoldsMigrate some documentation about attributes (#5390)
2020-11-09 Andrew ReynoldsAdd symbol manager (#5380)
2020-11-09 Andrew ReynoldsSimplify handling of subtypes in smt2 printer (#5401)
2020-11-09 Gereon KremerProperly clear interrupt for solve() as well. (#5403)
2020-11-09 Andrew ReynoldsDo not regress explanations of datatype lemmas (#5376)
2020-11-06 mudathirmahgoubFix issue #5342 (#5349)
2020-11-06 Andrew Reynolds(proof-new) Miscellaneous changes to strings for proofs...
2020-11-06 Andrew ReynoldsSplit sygus template inference to its own file (#5388)
2020-11-06 Andrew ReynoldsSimplify printing with respect to expression types...
2020-11-05 mudathirmahgoubRemove mkSingleton from the API (#5366)
2020-11-04 Andres NoetzliAdd constants from equality engine evaluation to model...
2020-11-03 Andrew ReynoldsAdd scope methods constructing types in API (#5393)
2020-11-03 Andres NoetzliAdd support for printing `re.loop` and `re.^` (#5392)
2020-11-03 Andrew ReynoldsReset built model flag at presolve in nonlinear (#5386)
2020-11-03 Andrew ReynoldsMove sygus qe preproc to its own file (#5375)
2020-11-03 makaimannRun python tests during make check (#5226)
2020-11-02 Aina Niemetzcontrib: Remove dependency directories. (#5367)
2020-11-02 Andrew ReynoldsUpdate strings proxy variable map to be context indepen...
2020-11-02 Andrew ReynoldsMiscellaneous cleaning of parser (#5369)
2020-11-02 Andrew ReynoldsAvoid dynamic allocation in symbol table implementation...
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...
next