summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-17[CI] Update package listCIAddFlexAndres 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
2020-08-07Move datatype index constant to its own file (#4859)Andrew Reynolds
2020-08-07GH Actions: Remove cancel action. (#4843)Aina Niemetz
2020-08-06Updates not related to creation for eliminating Expr-level datatype (#4838)Andrew Reynolds
2020-08-06Split preprocessor from SmtEngine (#4854)Andrew Reynolds
2020-08-06(proof-new) Refactor regular expression operation (#4596)Andrew Reynolds
2020-08-05Split Assertions from SmtEngine (#4788)Andrew Reynolds
2020-08-05Improve error message for unsupported exponents (#4852)Gereon Kremer
2020-08-05When checking models, ensure that error message is correctly formatted (#4853)Andrew V. Jones
2020-08-05[Strings] Add eager context-dependent evaluation (#4847)Andres Noetzli
2020-08-04Add dummy returns if libpoly is unavailable. (#4845)Gereon Kremer
2020-08-04Fixes for getInterpolant and getAbduct API methods (#4846)Andrew Reynolds
2020-08-04Add documentation and build instructions for recompilation (LGPL). (#4844)Mathias Preiner
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback