summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-28Do not delay processing equivalence class merges in datatypes (#4952)Andrew Reynolds
2020-08-27Add the buffered inference manager (#4954)Andrew Reynolds
2020-08-27(new theory) Update TheorySep to new interface (#4947)Andrew Reynolds
2020-08-27Make iand lemmas use proper Inference types. (#4956)Gereon Kremer
2020-08-27(proof-new) Add the proof equality engine (#4881)Andrew Reynolds
2020-08-26Add irrelevant kinds infrastructure to TheoryModel (#4945)Andrew Reynolds
2020-08-26Add the theory inference manager (#4948)Andrew Reynolds
2020-08-26(new theory) Update TheoryUF to new interface (#4944)Andrew Reynolds
2020-08-25Connect combination engine to theory engine (#4940)Andrew Reynolds
2020-08-25Replace Expr-level datatype with Node-level DType (#4875)Andrew Reynolds
2020-08-25Eliminating spurious replay of commands for define funs expansion when checki...Haniel Barbosa
2020-08-25Add the combination engine (#4939)Andrew Reynolds
2020-08-24Add a few basic extensions for equality engine (#4937)Andrew Reynolds
2020-08-24Fix memory issue in AntlrInput::parseError (#4873)Gereon Kremer
2020-08-24Do not use relevance during non-linear check model (#4938)Andrew Reynolds
2020-08-24Increase regress level to 2 for production build. (#4888)Mathias Preiner
2020-08-24Add the distributed model manager (#4934)Andrew Reynolds
2020-08-24Extend the standard Theory template based on equality engine (#4929)Andrew Reynolds
2020-08-21Remove unecessary theory model builder base class (#4933)Andrew Reynolds
2020-08-21Dynamic allocation of model equality engine (#4911)Andrew Reynolds
2020-08-21Limit trigger terms to shared terms in arrays (#4932)Andrew Reynolds
2020-08-21Remove spurious theory methods calls (#4931)Andrew Reynolds
2020-08-21Connect the relevance manager to TheoryEngine and use it in non-linear arithm...Andrew Reynolds
2020-08-21Simplify and fix care graph for ufHo (#4924)Andrew Reynolds
2020-08-21Remove BV equality slicer (#4928)Andrew Reynolds
2020-08-20Add TheoryState objects to each Theory (#4920)Andrew Reynolds
2020-08-20Split QuantElimSolver from SmtEngine (#4919)Andrew Reynolds
2020-08-19Simplify trigger notifications in equality engine (#4921)Andrew Reynolds
2020-08-19Remove example theory (#4922)Andrew Reynolds
2020-08-19Add strings-exp to regression (#4923)Andrew Reynolds
2020-08-19(cad solver) Add a partial check method. (#4904)Gereon Kremer
2020-08-19Make sets and strings solver states inherit from TheoryState (#4918)Andrew Reynolds
2020-08-19Require `--strings-exp` when using `str.substr` (#4916)Andres Noetzli
2020-08-19Changes assertion (about maximum set cardinality) to an exception. (#4907)Gereon Kremer
2020-08-19[Regressions] Do not test `--check-proofs` anymore (#4914)Andres Noetzli
2020-08-19Fix SmtEngine::reset() (#4917)Gereon Kremer
2020-08-18Refactor functions that print commands (Part 2) (#4905)Abdalrhman Mohamed
2020-08-18(proof-new) Theory preprocessor proof producing (#4807)Andrew Reynolds
2020-08-18Introduce the theory state object (#4910)Andrew Reynolds
2020-08-18Standardize collectModelInfo and theory-specific collectRelevantTerms (#4909)Andrew Reynolds
2020-08-18(proof-new) Minor updates to trust node (#4900)Andrew Reynolds
2020-08-18(proof-new) SMT proof postprocess callback (#4883)Andrew Reynolds
2020-08-18Quantifiers engine stores a pointer to the master equality engine (#4908)Andrew Reynolds
2020-08-18Split SygusSolver from SmtEngine (#4891)Andrew Reynolds
2020-08-18Add the relevance manager module (#4894)Andrew Reynolds
2020-08-18(proof-new) Callbacks for term-context-sensitive terms (#4842)Andrew Reynolds
2020-08-17Add identifier name for side condition. (#4902)Alex Ozdemir
2020-08-17[CI] Update package list (#4906)Andres Noetzli
2020-08-17Dynamic allocation of equality engine in Theory (#4890)Andrew Reynolds
2020-08-17(proof-new) Prepare the theory of strings for proof reconstruction (#4885)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback