summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2020-10-23Fix related to preregistering boolean term variables in strings (#5331)Andrew Reynolds
2020-10-22Use theoryof-mode=type for QF_NRA (#5326)Gereon Kremer
2020-10-22Remove unused equality engine types (#5319)Andrew Reynolds
2020-10-22Fix issue 5309 (#5327)mudathirmahgoub
2020-10-21(proof-new) Make theory preprocessor user-context dependent (#5296)Andrew Reynolds
2020-10-21(proof-new) Make circuit propagator proof producing (#5318)Gereon Kremer
2020-10-21Implement bags evaluator (#5322)mudathirmahgoub
2020-10-21(proof-new) Add arith proof macros file to CMake (#5321)Alex Ozdemir
2020-10-21(proof-new) arith: dedup literals in flattenImpl (#5320)Alex Ozdemir
2020-10-21(proof-new) Updates to lazy proof chain (#5317)Andrew Reynolds
2020-10-21Add operator MakeBagOp for constructing bags (#5209)mudathirmahgoub
2020-10-20Add finishInit for getInterpol and getAbduct. (#5316)Abdalrhman Mohamed
2020-10-20(proof-new) Fixes for proofs in rewriter (#5307)Andrew Reynolds
2020-10-20Fix compiler warnings. (#5305)Aina Niemetz
2020-10-20(proof-new) Add proofs for circuit propagator (#5301)Gereon Kremer
2020-10-20(proof-new) Fix for CDProof::isSame (#5297)Andrew Reynolds
2020-10-20(proof-new) Update add lazy step interface in LazyCDProof (#5299)Andrew Reynolds
2020-10-20Remove some Commands from the API. (#5268)Abdalrhman Mohamed
2020-10-20Fix miscellaneous warnings (#5256)Andrew Reynolds
2020-10-20Make seq.nth a trigger kind (#5314)Andrew Reynolds
2020-10-20Handle rewrite to bool in BoundInference (#5311)Gereon Kremer
2020-10-20Split CheckModels utility to its own file (#5303)Andrew Reynolds
2020-10-20Integer (CLN): Minor improvements. (#5306)Aina Niemetz
2020-10-19Expand `seq.nth` lazily (#5287)yoni206
2020-10-19Integer: CLN: Move implementation of member functions to .cpp file. (#5304)Aina Niemetz
2020-10-19[proof-new] Fixing resolution proof checker (#5262)Haniel Barbosa
2020-10-19(proof-new) Updates to assertions pipeline and preprocess generator (#5300)Andrew Reynolds
2020-10-19(proof-new) Update preprocessing pass context for proofs (#5298)Andrew Reynolds
2020-10-19[proof-new] Improving cycle checking in lazycdproofchain (#5302)Haniel Barbosa
2020-10-19Safer version of pending lemma processing in inference manager buffered (#5286)Andrew Reynolds
2020-10-18(proof-new) Refactoring cyclic checks (#5291)Andrew Reynolds
2020-10-18 (proof-new) Witness axiom reconstruction for purification skolems (#5289)Andrew Reynolds
2020-10-18(proof-new) Implementation of trust substitution (#5276)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback