summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-08-18minorfix7017Andres Noetzli
2021-08-18Minor fixes of policy for eliminating quantifiersAndres Noetzli
2021-08-18Make TheoryProxy use Env, simplify initialization of PropEngine (#7031)Andrew Reynolds
2021-08-17Replace `Maybe` with `std::optional` (#7005)Andres Noetzli
2021-08-17Make SmtEngineState use Env (#7028)Andrew Reynolds
2021-08-17Refactoring theory-specific variable elimination in quantifiers rewriter (#7026)Andrew Reynolds
2021-08-17Fix policy for eliminating quantified formulas (#7017)Andrew Reynolds
2021-08-17Make theory BV use central eq engine when option is enabled (#7025)Andrew Reynolds
2021-08-17Cosmetic improvements to theory datatypes (#7020)Andrew Reynolds
2021-08-17Improve conversion to skolems in expression miner (#7019)Andrew Reynolds
2021-08-17Initial refactoring of set defaults (#7021)Andrew Reynolds
2021-08-16Push Env class into TheoryState (#7012)Gereon Kremer
2021-08-16Use InferenceManager in ExtTheory (#7006)Gereon Kremer
2021-08-16Make Theory class use Env (#7011)Gereon Kremer
2021-08-16[Strings] Make fact detection more robust (#7007)Andres Noetzli
2021-08-16Add check for static libraries when compiling CryptoMiniSat #7010 (#7014)Andrew V. Jones
2021-08-15Correct copyright print for GLPK (#7015)Andrew V. Jones
2021-08-13Refactor setDefaults to use an options object (#6994)Gereon Kremer
2021-08-10Disable external initialization of `thread_local` variables (#7004)Andres Noetzli
2021-08-10Simplify generation of option module code. (#6995)Gereon Kremer
2021-08-09Create grouping of tests that exercise '--use-approx' (#6958)Andrew V. Jones
2021-08-09Support older CMake versions (#7003)Andres Noetzli
2021-08-06Merge options cmake into general cmake file (#6989)Gereon Kremer
2021-08-06Clear options manager (#6991)Gereon Kremer
2021-08-05Normalize val in BitVector(val_str, base) (#6955)Alex Ozdemir
2021-08-05Generalize term canonizer for type classes (#6895)Andrew Reynolds
2021-08-05[Unit Tests] Add missing include (#6990)Andres Noetzli
2021-08-05Fix policy for rewriting string equalities (#6916)Andrew Reynolds
2021-08-05No longer call solver constructor with an options object. (#6985)Gereon Kremer
2021-08-04Consolidate solver resets (#6986)Gereon Kremer
2021-08-04Proper printing of proofs in the internal calculus (#6975)Andrew Reynolds
2021-08-04Fix policy for merging subproofs (#6981)Andrew Reynolds
2021-08-04[proof] [dot] Fix comments on dot printer (#6983)Diego Della Rocca de Camargos
2021-08-04Add inference ids for remainder of sygus solver (#6977)Andrew Reynolds
2021-08-04Improve error messages for UF catching higher-order (#6982)Haniel Barbosa
2021-08-04syqi: Add debug information for dumping instantiations. (#6978)Mathias Preiner
2021-08-04Add optional debug information for dumping instantiations (#6950)Andrew Reynolds
2021-08-04Update bug_report.mdAina Niemetz
2021-08-04Add containsAssumption proof utility (#6953)Andrew Reynolds
2021-08-04Refactor managed streams (#6934)Gereon Kremer
2021-08-04Add API function to get list of option names (#6971)Gereon Kremer
2021-08-04Replace numeric predicates by explicit minimum and maximum (#6976)Gereon Kremer
2021-08-04Add missing inference identifiers (#6962)Andrew Reynolds
2021-08-04[proof] Add getProof to API and use it in GetProofCommand (#6974)Haniel Barbosa
2021-08-04Add IEEE-BV-to-FP to external-to-internal mapping in C++ API (#6951)Alex Ozdemir
2021-08-03Remove dependencies on smt engine in smt solver (#6965)Andrew Reynolds
2021-08-03Use int64_t, uint64_t or double for all numeric options. (#6970)Gereon Kremer
2021-08-03Refactor shared solver to use theory builtin inference manager (#6960)Andrew Reynolds
2021-08-03Remove "inUnsatCore" flag throughout (#6964)Andrew Reynolds
2021-08-03Properly honor --stats-all and --stats-expert when printing statistics (#6967)Gereon Kremer
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback