summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-09-03Remove unused postsolve infrastructurermPostsolveAndres Noetzli
2020-09-03Split lazy bit-vector solver from TheoryBV (#5009)Mathias Preiner
2020-09-03Add interfaces for making trust nodes in TheoryInferenceManager. (#5016)Andrew Reynolds
2020-09-03Update sets inference manager to inherit from InferenceManagerBuffered (#5007)Andrew Reynolds
2020-09-03Added a new rule to simplify (bvugt (bvurem T x) x) (#4993)Gereon Kremer
2020-09-03Minor cleanup of quantifiers engine (#4994)Andrew Reynolds
2020-09-03Changing the handled operators in bv2int preprocessing pass (#4970)yoni206
2020-09-03Basic integration of arith::InferenceManager (#4999)Gereon Kremer
2020-09-03Make nonlinear extension (more) deterministic (#4996)Gereon Kremer
2020-09-02Drop {INCLUDE,LIBRARY,RUNTIME}_INSTALL_DIR variables in CMakeLists.txt (#4979)FabianWolff
2020-09-02Make ExtTheory independent of Theory (#5010)Andrew Reynolds
2020-09-02(proof-new) Support proofs of quantifier instantiation (#5001)Andrew Reynolds
2020-09-02(proof-new) Improve debugging infrastructure for open proofs (#4984)Andrew Reynolds
2020-09-02Fix CryptoMiniSat build, regression (#5006)Andres Noetzli
2020-09-02[Python API] Add missing methods to Datatype/Term (#4998)Andres Noetzli
2020-09-02Remove #line directives from generated files. (#5005)Gereon Kremer
2020-09-02(proof-new) Updates to builtin proof checker (#4962)Andrew Reynolds
2020-09-02(proof-new) Add proof support in TheoryUF (#5002)Andrew Reynolds
2020-09-02Use SMT-COMP configuration for competition build (#4995)Andres Noetzli
2020-09-02(proof-new) Make term conversion proof generator optionally term-context sens...Andrew Reynolds
2020-09-02Migrating from using the 'glpk-cut-log' repo to using an official GPLK releas...Andrew V. Jones
2020-09-02Introduce an internal version of Commands. (#4988)Abdalrhman Mohamed
2020-09-02Minor updates to theory inference manager (#5004)Andrew Reynolds
2020-09-02(new theory) Update TheoryArrays to the new standard (#5000)Andrew Reynolds
2020-09-02Use std::unique_ptr instead of std::shared_ptr for inference manager (#5003)Gereon Kremer
2020-09-02Add ArithLemma and arith::InferenceManager (#4960)Gereon Kremer
2020-09-02(new theory) Update TheorySets to the new interface (#4951)Andrew Reynolds
2020-09-01[API] Fix Python Examples (#4943)Andres Noetzli
2020-09-01Removes old proof code (#4964)Haniel Barbosa
2020-09-01 (new theory) Update TheoryDatatypes to the new standard (#4986)Andrew Reynolds
2020-09-01Add TheoryInference base class (#4990)Andrew Reynolds
2020-09-01CMS: Update to version 5.8.0. (#4991)Aina Niemetz
2020-09-01Add arithmetic-specific, runtime, proof-macros. (#4992)Alex Ozdemir
2020-08-31'fix-install-headers.sh' should respect DESTDIR environment variable (#4978)FabianWolff
2020-08-31Add the inference manager for datatypes (#4968)Andrew Reynolds
2020-08-31Fix spelling errors (#4977)FabianWolff
2020-08-31(new theory) Update TheoryStrings to new standard (#4963)Andrew Reynolds
2020-08-31Fix --ackermann in the presence on syntactically different but possibly equal...Gereon Kremer
2020-08-31Simplify interface for computing relevant terms. (#4966)Andrew Reynolds
2020-08-31[CI] Fix Cython installation (#4983)Andres Noetzli
2020-08-31Basic proof support in inference manager (#4975)Andrew Reynolds
2020-08-28(proof-new) More term context utilities. (#4912)Andrew Reynolds
2020-08-28New C++ API: Add REGEXP_{REPEAT,LOOP}_OP handling in getIndices. (#4969)Mathias Preiner
2020-08-28Replace Theory::Set with TheoryIdSet (#4959)Andrew Reynolds
2020-08-28Incremental support for bv_to_int (#4967)yoni206
2020-08-28(proof-new) Make CombinationEngine proof producing (#4955)Andrew Reynolds
2020-08-28(new theory) Update TheoryQuantifiers to the new interface (#4950)Andrew Reynolds
2020-08-28(proof-new) Add the SMT proof post processor (#4913)Andrew Reynolds
2020-08-28(new theory) Update TheoryFP to the new interface (#4953)Andrew Reynolds
2020-08-28(cad-solver) Fixed excluding lemma generation. (#4958)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback