summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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
2020-10-13bv2int: improving bvand tables (#5235)yoni206
2020-10-12Remove uf-ss-totality option (#5251)Andrew Reynolds
2020-10-12Eliminate uses of Expr in SmtEngine interface (#5240)Andrew Reynolds
2020-10-12Ensure uninterpreted sort owner is UF if uf-ho or finite-model-find is enable...Andrew Reynolds
2020-10-11SyGuS instantiation modes (#5228)Mathias Preiner
2020-10-11Add conversion of poly polynomial to cvc node. (#5218)Gereon Kremer
2020-10-10Provide API version of some SMT Commands. (#5222)Abdalrhman Mohamed
2020-10-09bv2int: bvand translation code move (#5227)yoni206
2020-10-09use right arith explanation fn to fix regressions (#5231)Alex Ozdemir
2020-10-09(proof-new) proofs for arith-constraint explanations (#5224)Alex Ozdemir
2020-10-08reset-assertions: Remove all non-global symbols in the parser (#5229)Andres Noetzli
2020-10-08Simplify approach for collapsed selectors over non-closed enumerable types (#...Andrew Reynolds
2020-10-08(proof-new) Add lazy proof set utility (#5221)Andrew Reynolds
2020-10-08(proof-new) Theory engine proof producing (#5195)Andrew Reynolds
2020-10-08(proof-new) Fixes and improvements for smt proof postprocessor (#5197)Andrew Reynolds
2020-10-08Get correct NodeManagerScope for toStrings in API (#5216)makaimann
2020-10-07(proof-new) proofs in ee -> arith pipeline (#5215)Alex Ozdemir
2020-10-07New C++ API: Rename Term::isConst() to Term::isValue(). (#5211)Aina Niemetz
2020-10-07Make sure conflicts are not rewritten (in arithmetic) (#5219)Gereon Kremer
2020-10-07(proof-new) Add the strings proof constructor (#4903)Andrew Reynolds
2020-10-06Process pending inferences at the beginning of datatypes post check (#5213)Andrew Reynolds
2020-10-06bv-to-int: change order of passes (#5208)yoni206
2020-10-06(proof-new) proofs for ArithCongMan -> ee facts (#5207)Alex Ozdemir
2020-10-06(proof-new) Add interface for trusted substitution and update ppAssert (#5193)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback