summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-10Fix preregistration in TheorySep before declare-heap (#5411)Andrew Reynolds
2020-11-10Do not mark extended functions as reduced based on decomposing contains (#5407)Andrew Reynolds
2020-11-10Pin LFSC version (#5412)Alex Ozdemir
2020-11-10Make mkGroundTerm deterministic (#5347)Andrew Reynolds
2020-11-10Add getSubtermKinds to node algorithm (#5398)Andrew Reynolds
2020-11-10Add proper support for the declare-heap command for separation logic (#5405)Andrew Reynolds
2020-11-09Migrate some documentation about attributes (#5390)Andrew Reynolds
2020-11-09Add symbol manager (#5380)Andrew Reynolds
2020-11-09Simplify handling of subtypes in smt2 printer (#5401)Andrew Reynolds
2020-11-09Properly clear interrupt for solve() as well. (#5403)Gereon Kremer
2020-11-09Do not regress explanations of datatype lemmas (#5376)Andrew Reynolds
2020-11-06Fix issue #5342 (#5349)mudathirmahgoub
2020-11-06(proof-new) Miscellaneous changes to strings for proofs (#5362)Andrew Reynolds
2020-11-05Split sygus template inference to its own file (#5388)Andrew Reynolds
2020-11-05Simplify printing with respect to expression types (#5394)Andrew Reynolds
2020-11-05Remove mkSingleton from the API (#5366)mudathirmahgoub
2020-11-03Add constants from equality engine evaluation to model (#5391)Andres Noetzli
2020-11-03Add scope methods constructing types in API (#5393)Andrew Reynolds
2020-11-03Add support for printing `re.loop` and `re.^` (#5392)Andres Noetzli
2020-11-03Reset built model flag at presolve in nonlinear (#5386)Andrew Reynolds
2020-11-02Move sygus qe preproc to its own file (#5375)Andrew Reynolds
2020-11-02Run python tests during make check (#5226)makaimann
2020-11-02contrib: Remove dependency directories. (#5367)Aina Niemetz
2020-11-02Update strings proxy variable map to be context independent (#5377)Andrew Reynolds
2020-11-02Miscellaneous cleaning of parser (#5369)Andrew Reynolds
2020-11-02Avoid dynamic allocation in symbol table implementation (#5368)Andrew Reynolds
2020-10-30Use BoundInference in nonlinear extension (#5359)Gereon Kremer
2020-10-29Update api::Sort to use TypeNode instead of Type (#5363)Andrew Reynolds
2020-10-29Set strings pending conflict flag (#5364)Andrew Reynolds
2020-10-29Add mkInteger to the API (#5274)mudathirmahgoub
2020-10-29(proof-new) Update the strings inference manager for proofs (#5220)Andrew Reynolds
2020-10-29Add NodeManager::mkOr() (#5360)Gereon Kremer
2020-10-28run_regression.py to fail on invalid requirements (#5264)yoni206
2020-10-28Remove more uses of Expr (#5357)Andrew Reynolds
2020-10-28Fixes for unconstrained variables in nonlinear model (#5351)Andrew Reynolds
2020-10-28Convert symbol table from Expr-level to Term-level (#5355)Andrew Reynolds
2020-10-28Split NlSolver in multiple subsolvers (#5315)Gereon Kremer
2020-10-28Add rewrites for div/mod in the arithmetic rewriter (#5352)Andrew Reynolds
2020-10-27run_regression: Add --skip-timeout option, lower timeout to 600 seconds. (#5...Mathias Preiner
2020-10-27Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)Abdalrhman Mohamed
2020-10-27Add missing methods involving datatype sorts to the API (#5290)Andrew Reynolds
2020-10-27Disable --nl-cad option by default (#5350)Gereon Kremer
2020-10-27Enable --nl-cad by default (#5345)Gereon Kremer
2020-10-26Add DUPICATE_REMOVAL operator to bags (#5336)mudathirmahgoub
2020-10-26(proof-new) Add datatypes proof checker (#5340)Andrew Reynolds
2020-10-26Send external equalities from collapse selector as lemmas (#5346)Andrew Reynolds
2020-10-24Fix issue 5271 (#5335)mudathirmahgoub
2020-10-23[proof-new] Fix n-ary kind handling in EqEngine explanations (#5332)Haniel Barbosa
2020-10-23Apply alpha equivalence to annotated quantified formulas (#5324)Andrew Reynolds
2020-10-23Change datatypes lemma policy for equalities not coming from instantiate (#5325)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback