summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-17FloatingPoint: Clean up and document header, format. (#5453)Aina Niemetz
2020-11-17ci: Simplify Python dependency installs for Linux and macOS. (#5458)Mathias Preiner
2020-11-17Fix tangent plane lemmas (#5455)Gereon Kremer
2020-11-16Refactor tangent plane lemmas (#5449)Gereon Kremer
2020-11-16Cleaning up scopes in preparation for symbol manager (#5442)Andrew Reynolds
2020-11-16Improve accuracy of resource limitation (#4763)Gereon Kremer
2020-11-14Fix double conflict in extended string solver (#5435)Andrew Reynolds
2020-11-14(proof-new) Proofs for non-clausal simplification (#5409)Andrew Reynolds
2020-11-13(proof-new) Enable proofs for datatypes (#5436)Andrew Reynolds
2020-11-13Model declarations printing options (#5432)yoni206
2020-11-13Add more features to symbol manager (#5434)Andrew Reynolds
2020-11-12Make regular expression difference left associative (#5430)Andrew Reynolds
2020-11-12Simplify sygus solver and sygus stream (#5389)Andrew Reynolds
2020-11-12Fix printing of define named function (#5425)Andrew Reynolds
2020-11-12Models standard (#5415)yoni206
2020-11-12(proof-new) Separate explanation stages in proof equality engine (#5356)Andrew Reynolds
2020-11-12Fix redundant refinement lemma in sygus solver (#5399)Andrew Reynolds
2020-11-12(proof-new) Proofs for skolemization (#5339)Andrew Reynolds
2020-11-12(proof-new) Fix true explanations of propagations in pf equality engine (#5338)Andrew Reynolds
2020-11-12(proof-new) Improve printing and debugging for pedantic checking (#5337)Andrew Reynolds
2020-11-12(proof-new) Add datatypes inference to proof constructor (#5408)Andrew Reynolds
2020-11-12Make symbol manager context dependent (#5424)Andrew Reynolds
2020-11-11Move symbol manager to src/expr/ (#5420)Andrew Reynolds
2020-11-11Rewrite witness terms at prerewrite (#5419)Andrew Reynolds
2020-11-11Add simple substitution utility (#5397)Andrew Reynolds
2020-11-11Pass symbol manager to commands (#5410)Andrew Reynolds
2020-11-10Fix preregistration in TheorySep before declare-heap (#5411)Andrew Reynolds
2020-11-10Do not mark extended functions as reduced based on decomposing contains (#5407)Andrew Reynolds
2020-11-10Pin LFSC version (#5412)Alex Ozdemir
2020-11-10Make mkGroundTerm deterministic (#5347)Andrew Reynolds
2020-11-10Add getSubtermKinds to node algorithm (#5398)Andrew Reynolds
2020-11-10Add proper support for the declare-heap command for separation logic (#5405)Andrew Reynolds
2020-11-09Migrate some documentation about attributes (#5390)Andrew Reynolds
2020-11-09Add symbol manager (#5380)Andrew Reynolds
2020-11-09Simplify handling of subtypes in smt2 printer (#5401)Andrew Reynolds
2020-11-09Properly clear interrupt for solve() as well. (#5403)Gereon Kremer
2020-11-09Do not regress explanations of datatype lemmas (#5376)Andrew Reynolds
2020-11-06Fix issue #5342 (#5349)mudathirmahgoub
2020-11-06(proof-new) Miscellaneous changes to strings for proofs (#5362)Andrew Reynolds
2020-11-05Split sygus template inference to its own file (#5388)Andrew Reynolds
2020-11-05Simplify printing with respect to expression types (#5394)Andrew Reynolds
2020-11-05Remove mkSingleton from the API (#5366)mudathirmahgoub
2020-11-03Add constants from equality engine evaluation to model (#5391)Andres Noetzli
2020-11-03Add scope methods constructing types in API (#5393)Andrew Reynolds
2020-11-03Add support for printing `re.loop` and `re.^` (#5392)Andres Noetzli
2020-11-03Reset built model flag at presolve in nonlinear (#5386)Andrew Reynolds
2020-11-02Move sygus qe preproc to its own file (#5375)Andrew Reynolds
2020-11-02Run python tests during make check (#5226)makaimann
2020-11-02contrib: Remove dependency directories. (#5367)Aina Niemetz
2020-11-02Update strings proxy variable map to be context independent (#5377)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback