summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Expand)Author
2021-03-08New C++ API: Migrate to Node layer. (#6070)Aina Niemetz
2021-03-08Fix handling of negation of Boolean bound variables in FMF (#6066)Andrew Reynolds
2021-03-08(proof-new) Separating optimizations for strings skolem caching (#6064)Andrew Reynolds
2021-03-08(proof-new) Prepare arithmetic for changes to ppRewrite (#6063)Andrew Reynolds
2021-03-08Simplify theory preprocessing (#6058)Andrew Reynolds
2021-03-08Fix justification heuristic again (#6074)Gereon Kremer
2021-03-08Do not process conjunctions as facts in strings (#6065)Andrew Reynolds
2021-03-05Remove partial UDIV/UREM operators. (#6069)Mathias Preiner
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
2021-03-05Initial implementation of an optimization solver with unit tests. (#5849)mcjuneho
2021-03-05Reimplement time limit mechanism for windows (#6049)Gereon Kremer
2021-03-04New C++ API: Clean up usage of interal datatype classes. (#6055)Aina Niemetz
2021-03-04Add initial bit-blaster for proof logging. (#6053)Aina Niemetz
2021-03-04New C++ Api: Clean up usage of internal types in Term. (#6054)Aina Niemetz
2021-03-04Add proper define for libpoly usage (#6050)Gereon Kremer
2021-03-04Ignore isInConflict when adding conflicts (#5995)Gereon Kremer
2021-03-04New C++ API: Clean up usage of internal Type/TypeNodes. (#6044)Aina Niemetz
2021-03-04New C++ API: Clean up usage of internal Result. (#6043)Aina Niemetz
2021-03-03New C++ API: Clean up usage of internal types in Op. (#6045)Aina Niemetz
2021-03-03(proof-new) Simplifications to arithmetic operator elimination and preprocess...Andrew Reynolds
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
2021-03-03Remove uses of SExpr class. (#6035)Abdalrhman Mohamed
2021-03-03Add tuple projection operator (#5904)mudathirmahgoub
2021-03-02Remove non-ASCII characters from source files. (#6039)Mathias Preiner
2021-03-02Improve handling of utf8 encoded inputs (#5694)Gereon Kremer
2021-03-02Add aarch64 (ARM64) cross-compile support. (#6033)Mathias Preiner
2021-03-02Fix nightly errors. (#6034)Mathias Preiner
2021-03-02Introduce quantifiers term registry (#5983)Andrew Reynolds
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2021-03-01Refactor collection of debug and trace tags (#5996)Gereon Kremer
2021-02-27google test: theory: Migrate theory_white. (#6006)Aina Niemetz
2021-02-26Some formatting and better tracing in prop engine (#6022)Haniel Barbosa
2021-02-26Minor improvement and fix to smt2 printer (#6009)Andrew Reynolds
2021-02-26Optionally permit creation of non-flat function types (#6010)Andrew Reynolds
2021-02-25Store Node instead of TNode (#5993)Gereon Kremer
2021-02-25(proof-new) Fix regular expression unfolding under substitution (#5958)Andrew Reynolds
2021-02-26Move (optional) rewrite from TrustSubstitutionMap to SubstitutionMap. (#5992)Gereon Kremer
2021-02-25Datatypes lemmas: share only external types (#5997)yoni206
2021-02-24Enable -Werror. (#5969)Mathias Preiner
2021-02-24Ensure static-learning adds rewritten assertions. (#5982)Gereon Kremer
2021-02-24(proof-new) Add proofs for CAD solver (#5981)Gereon Kremer
2021-02-23Add state and inference manager to inst match generator (#5968)Andrew Reynolds
2021-02-23Add interface to TheoryState for sort inference and facts (#5967)Andrew Reynolds
2021-02-23Switch to C++17. (#5959)Mathias Preiner
2021-02-23Add proof for mult sign lemma (#5966)Gereon Kremer
2021-02-23[proof-new] Fix dangling pointer in SAT proof generation (#5963)Haniel Barbosa
2021-02-23Add proof for monomial bounds check (#5965)Gereon Kremer
2021-02-23(proof-new) Add proof generator for CAD solver (#5964)Gereon Kremer
2021-02-23[proof-new] Fix handling of removable clauses in proof cnf stream (#5961)Haniel Barbosa
2021-02-22Add trans secant proofs. (#5957)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback