summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2020-08-13Add the distributed equality engine manager (#4867)Andrew Reynolds
2020-08-12[proof-new] Adding support for corner case of transitivity simulating MERGED_...Haniel Barbosa
2020-08-12generalize handling MERGED_THROUGH_CONSTANST in EqProof conversion (#4878)Haniel Barbosa
2020-08-12Refactor functions that print commands (Part 1) (#4869)Abdalrhman Mohamed
2020-08-12Fixes for degenerate case of sygus decision tree learning (#4800)Andrew Reynolds
2020-08-12(proof-new) Improve robustness of CONG rule (#4882)Andrew Reynolds
2020-08-12(proof-new) Proof support in the strings term registry. (#4876)Andrew Reynolds
2020-08-12(proof-new) Improve interfaces to proof generators (#4803)Andrew Reynolds
2020-08-12Add option to only build library (#4801)makaimann
2020-08-12(proof-new) Witness form proof generator (#4782)Andrew Reynolds
2020-08-12Add naive support for integer variables. (#4835)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback