summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2020-08-16Add non-emptiness to conclusion of positive RE star unfolding. (#4899)Andrew Reynolds
2020-08-15(cad solver) Use the current model as initial assignment (#4893)Gereon Kremer
2020-08-15Minor cleanup related to notifications (#4898)Andrew Reynolds
2020-08-15Add finishInit method to PropEngine (#4895)Andrew Reynolds
2020-08-15(proof-new) Add the strings proof checker (#4858)Andrew Reynolds
2020-08-14Simplify equality engine notifications (#4896)Andrew Reynolds
2020-08-14correctly parse sygus lang option (#4884)E Polgreen
2020-08-14Inspect roots to avoid certain resultants (Algorithm 4, lines 8,9). (#4892)Gereon Kremer
2020-08-13Split SmtSolver from SmtEngine (#4880)Andrew Reynolds
2020-08-13Fixes for corner case of decision tree learning with different types (#4887)Andrew Reynolds
2020-08-13More basic fix for dumping synth-fun (#4886)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback