summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2020-11-19Use symbol manager for unsat cores (#5468)Andrew Reynolds
2020-11-18Minor cleanup of SmtEngine (#5450)Andrew Reynolds
2020-11-18Do not expand definitions of extended arithmetic operators (#5433)Andrew Reynolds
2020-11-18Use symbol manager for get assignment (#5451)Andrew Reynolds
2020-11-12Fix printing of define named function (#5425)Andrew Reynolds
2020-11-12(proof-new) Improve printing and debugging for pedantic checking (#5337)Andrew Reynolds
2020-11-11Move symbol manager to src/expr/ (#5420)Andrew Reynolds
2020-11-11Pass symbol manager to commands (#5410)Andrew Reynolds
2020-11-10Do not mark extended functions as reduced based on decomposing contains (#5407)Andrew Reynolds
2020-11-10Add proper support for the declare-heap command for separation logic (#5405)Andrew Reynolds
2020-11-09Simplify handling of subtypes in smt2 printer (#5401)Andrew Reynolds
2020-11-05Simplify printing with respect to expression types (#5394)Andrew Reynolds
2020-10-29Update api::Sort to use TypeNode instead of Type (#5363)Andrew Reynolds
2020-10-28Remove more uses of Expr (#5357)Andrew Reynolds
2020-10-27Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)Abdalrhman Mohamed
2020-10-27Disable --nl-cad option by default (#5350)Gereon Kremer
2020-10-27Enable --nl-cad by default (#5345)Gereon Kremer
2020-10-22Use theoryof-mode=type for QF_NRA (#5326)Gereon Kremer
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-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-20Split CheckModels utility to its own file (#5303)Andrew Reynolds
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-18 (proof-new) Witness axiom reconstruction for purification skolems (#5289)Andrew Reynolds
2020-10-18(proof-new) More features for SMT proof post-processor (#5246)Andrew Reynolds
2020-10-16Refactor SMT-level model object (#5277)Andrew Reynolds
2020-10-13(proof-new) Generalize preprocess proof generator (#5245)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-10Provide API version of some SMT Commands. (#5222)Abdalrhman Mohamed
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-06bv-to-int: change order of passes (#5208)yoni206
2020-10-05Recover from some exceptions. (#5203)Abdalrhman Mohamed
2020-10-05Make sygus more robust to unknown responses in solution verification (#5199)Andrew Reynolds
2020-10-02(proof-new) Fixes for theory preprocessing proofs (#5171)Andrew Reynolds
2020-10-02Allow for theory combination of strings with nonlinear real arithmetic. (#5111)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-30Remove too strict assertion to allow for approximate models (#5168)Gereon Kremer
2020-09-29(proof-new) Fixes for preprocess proof generator and proofs in assertion pipe...Andrew Reynolds
2020-09-29[proof-new] Updates to proof node updater (#5156)Haniel Barbosa
2020-09-28Reset assertions on resetAssertions (#5153)Andrew Reynolds
2020-09-24 Function definition fmf preprocessing pass (#5064)Andrew Reynolds
2020-09-23Disable cegqi-bv when using sygus (#5124)Andrew Reynolds
2020-09-22Allow E-matching by default when strings are enabled (#5117)Andrew Reynolds
2020-09-22Refactor Commands to use the Public API. (#5105)Abdalrhman Mohamed
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback