summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2020-08-12(proof-new) Improving proof-production in Equality Engine (#4871)Haniel Barbosa
2020-08-12Fix connection to master equality engine in sets (#4877)Andrew Reynolds
2020-08-12Fix infinite loop in arith_ite_simp (#4805)Gereon Kremer
2020-08-11Fix unsupported option in regress1. (#4874)Andrew Reynolds
2020-08-11Split SmtEngineState from SmtEngine (#4855)Andrew Reynolds
2020-08-11Prepare theory of sets for dynamic allocation of equality engine (#4868)Andrew Reynolds
2020-08-11Final preparations for changing API to use the Node-level datatype (#4863)Andrew Reynolds
2020-08-11(proof-new) Extensions to proof checker interface (#4857)Andrew Reynolds
2020-08-11Update Expr-level unit tests that depend on datatypes to Node (#4860)Andrew Reynolds
2020-08-11Remove instantiation model true option (#4861)Andrew Reynolds
2020-08-11New C++ API: Remove redundant API functions for mkReal. (#4870)Aina Niemetz
2020-08-09Make valuation class more robust to null underlying TheoryEngine. (#4864)Andrew Reynolds
2020-08-09Splitting a few utility classes from EqualityEngine to their own file (#4862)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback