summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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
2020-10-06(proof-new) Allow null proofs from generators in LazyCDProof (#5196)Andrew Reynolds
2020-10-06Add operators bag.from_set, bag.to_set to the theory of bags (#5186)mudathirmahgoub
2020-10-06Add arithmetic preprocess module (#5188)Andrew Reynolds
2020-10-05Recover from some exceptions. (#5203)Abdalrhman Mohamed
2020-10-05Remove subtyping for sets (#5205)mudathirmahgoub
2020-10-05SyGuS: Add fp.sub to default FP grammar. (#5206)Aina Niemetz
2020-10-05Integer: GMP: Move implementation of member functions to .cpp file. (#5190)Aina Niemetz
2020-10-05Make sygus more robust to unknown responses in solution verification (#5199)Andrew Reynolds
2020-10-04Remove subtyping for sets theory (#5179)mudathirmahgoub
2020-10-03sygus-inst: Add more special BV values. (#5191)Aina Niemetz
2020-10-03Standardization of Theory (#5181)Andrew Reynolds
2020-10-02Minor simplifications to substitution map class (#5180)Andrew Reynolds
2020-10-02(proof-new) Fixes for theory preprocessing proofs (#5171)Andrew Reynolds
2020-10-02(proof-new) Make shared solver proof producing (#5169)Andrew Reynolds
2020-10-02Allow for theory combination of strings with nonlinear real arithmetic. (#5111)Gereon Kremer
2020-10-02Decouple modules from TheoryArithPrivate (#5184)Andrew Reynolds
2020-10-02(proof-new) New proofs in arith::Constraint::externalExplain (#5176)Alex Ozdemir
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback