summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2020-10-18(proof-new) More features for SMT proof post-processor (#5246)Andrew Reynolds
2020-10-17(proof-new) Improvements for theory engine (#5292)Andrew Reynolds
2020-10-16Refactor SMT-level model object (#5277)Andrew Reynolds
2020-10-16Catch more cases of nested recursion in datatypes (#5285)Andrew Reynolds
2020-10-16bv2int: caching introduced terms (#5283)yoni206
2020-10-16Add inference enumeration to datatypes (#5275)Andrew Reynolds
2020-10-15(proof-new) TheoryArithPrivate: farkas lemma proof (#5267)Alex Ozdemir
2020-10-14Fix issue #5269 (#5270)mudathirmahgoub
2020-10-14bv2int: implementing the iand-sum mode (#5265)yoni206
2020-10-14(proof-new) debug statements & docs for INT_TRUST (#5259)Alex Ozdemir
2020-10-14(proof-new) pfs in TheoryArith(Private) explainations (#5258)Alex Ozdemir
2020-10-14Guard uses of printing approximations for constants (#5247)Andrew Reynolds
2020-10-14(proof-new) pfs for conflicts in TheoryArithPrivate (#5257)Alex Ozdemir
2020-10-13bv2int: rewritings and unsat cores (#5263)yoni206
2020-10-13using NOT_NOT_ELIM rather than macros to do double-neg elimination (#5261)Haniel Barbosa
2020-10-13(proof-new) Prove lemmas in Constraint (#5254)Alex Ozdemir
2020-10-13(proof-new) Generalize preprocess proof generator (#5245)Andrew Reynolds
2020-10-13(proof-new) Simplifications for proof rule checker interface (#5244)Andrew Reynolds
2020-10-13 (proof-new) Miscellaneous minor improvements and fixes to proofs in theory f...Andrew Reynolds
2020-10-13(proof-new) New rules for Booleans (#5243)Andrew Reynolds
2020-10-13(proof-new) Change merge policy for proof node updater (#5242)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback