summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-31Add the inference manager for datatypes (#4968)Andrew Reynolds
2020-08-31Fix spelling errors (#4977)FabianWolff
2020-08-31(new theory) Update TheoryStrings to new standard (#4963)Andrew Reynolds
2020-08-31Fix --ackermann in the presence on syntactically different but possibly equal...Gereon Kremer
2020-08-31Simplify interface for computing relevant terms. (#4966)Andrew Reynolds
2020-08-31[CI] Fix Cython installation (#4983)Andres Noetzli
2020-08-31Basic proof support in inference manager (#4975)Andrew Reynolds
2020-08-28(proof-new) More term context utilities. (#4912)Andrew Reynolds
2020-08-28New C++ API: Add REGEXP_{REPEAT,LOOP}_OP handling in getIndices. (#4969)Mathias Preiner
2020-08-28Replace Theory::Set with TheoryIdSet (#4959)Andrew Reynolds
2020-08-28Incremental support for bv_to_int (#4967)yoni206
2020-08-28(proof-new) Make CombinationEngine proof producing (#4955)Andrew Reynolds
2020-08-28(new theory) Update TheoryQuantifiers to the new interface (#4950)Andrew Reynolds
2020-08-28(proof-new) Add the SMT proof post processor (#4913)Andrew Reynolds
2020-08-28(new theory) Update TheoryFP to the new interface (#4953)Andrew Reynolds
2020-08-28(cad-solver) Fixed excluding lemma generation. (#4958)Gereon Kremer
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback