summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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
2020-10-01SyGuS: Add min/max (sub)normal constants to FP default grammar. (#5185)Aina Niemetz
2020-10-01(proof-new) Make arrays proof producing (#5112)Andrew Reynolds
2020-10-01Add additional ground terms to SyGuS instantiation grammar (#5167)Mathias Preiner
2020-10-01Update theory of arithmetic to standard check (#5178)Andrew Reynolds
2020-10-01FloatingPoint: Add utility functions for largest and smallest normal. (#5174)Aina Niemetz
2020-10-01Allow to use the initial assignment for CAD (#5177)Gereon Kremer
2020-10-01(proof-new) Preprocessing passes use proper interfaces to assertions pipeline...Andrew Reynolds
2020-10-01Make SygusSolver use sygus attributes directly (#5172)Andrew Reynolds
2020-09-30BitVector: Extend interface of setBit to set it to a specific value. (#5173)Aina Niemetz
2020-09-30FloatingPoint: Add utility functions for largest and smallest subnormal. (#5166)Aina Niemetz
2020-09-30Remove too strict assertion to allow for approximate models (#5168)Gereon Kremer
2020-09-30Add missing includes. (#5170)Gereon Kremer
2020-09-30Add strategy for nonlinear extension (#5160)Gereon Kremer
2020-09-30Dynamic allocation of equality engine for shared solver (#5152)Andrew Reynolds
2020-09-30(proof-new) Add the term conversion sequence generator (#5097)Andrew Reynolds
2020-09-29[proof-new] Adds a proof manager for prop engine (#5162)Haniel Barbosa
2020-09-29Fix bags headers (#5165)mudathirmahgoub
2020-09-29(proof-new) Add proof managers and eager gens to arith (#5159)Alex Ozdemir
2020-09-29(proof-new) Fixes for preprocess proof generator and proofs in assertion pipe...Andrew Reynolds
2020-09-29[proof-new] Adds a proof post processor for the Prop Engine (#5161)Haniel Barbosa
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback