summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
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-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
2020-08-04Modify the smt2 parser to use the Sygus grammar. (#4829)Abdalrhman Mohamed
2020-08-04Add API interface for specialized constructor term (#4817)Andrew Reynolds
2020-08-04Properly initialize d_fullyInited. (#4840)Gereon Kremer
2020-08-04Add CAD-based solver (#4834)Gereon Kremer
2020-08-03Update documentation for Solver::mkVar() (#4833)Andres Noetzli
2020-08-03Add implementation for SyGuS interpolation module (step4) (#4811)Ying Sheng
2020-08-03New BV rewrite rules aimed at bv_to_int preprocessing pass (#4769)yoni206
2020-08-03Generalize interface for candidate rewrite database (#4797)Andrew Reynolds
2020-08-03Update datatypes in cvc parser to the new API (#4826)Andrew Reynolds
2020-08-03Delete solver pointer in Cython __dealloc__ (#4799)makaimann
2020-08-03Split expression names from SmtEngine (#4832)Andrew Reynolds
2020-08-03Split dump manager from SmtEngine (#4824)Andrew Reynolds
2020-08-02Updates to dtype constructor in preparation for eliminating Expr-level dataty...Andrew Reynolds
2020-08-02Fix ASan failure in interactive_shell_black (#4827)Andres Noetzli
2020-08-01Ensure strict length constraint for decompose rule (#4821)Andres Noetzli
2020-08-01Add methods for constructing datatype types from NodeManager (#4823)Andrew Reynolds
2020-08-01Fix component contains for splicing due to substring. (#4705)Andrew Reynolds
2020-07-31Add SyGuS Python API (#4812)yoni206
2020-07-31Split listener classes from SmtEngine (#4816)Andrew Reynolds
2020-07-30Standardize explanations in arrays (#4804)Andrew Reynolds
2020-07-30Python API: Add support for sequences (#4757)Andres Noetzli
2020-07-30Cad implementation (#4774)Gereon Kremer
2020-07-30Adds the interface for the CAD-based arithmetic solver. (#4773)Gereon Kremer
2020-07-30When linking Editline, use 'pkg-config' to correctly find the link-time depen...Andrew V. Jones
2020-07-30Fix null case for sygus printing (#4793)Andrew Reynolds
2020-07-30(proof-new) Stream output for ProofNode (#4789)Andrew Reynolds
2020-07-29(proof-new) Fixes for getFreeAssumptions (#4802)Andrew Reynolds
2020-07-28fixing issue #4808. (#4810)Ying Sheng
2020-07-28Remove arrays lazy rintro option (#4806)Andrew Reynolds
2020-07-28Replace Expr with Node in Term/Op (#4781)Andres Noetzli
2020-07-28Fix regular expression delta for complement (#4765)Andrew Reynolds
2020-07-28Supporting seq.nth (#4723)yoni206
2020-07-28Interpolation: Add interface for SyGuS interpolation module (step3) (#4726)Ying Sheng
2020-07-28Use lemma property enum for OutputChannel::lemma (#4755)Andrew Reynolds
2020-07-27(proof-new) Proof production for term formula removal (#4687)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback