summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-11-24api: Fix creation of nary term kinds via Op. (#7688)Aina Niemetz
2021-11-23Make difficulty manager only consider lemmas at full effort (#7685)Andrew Reynolds
2021-11-23Enable model-based reduction technique for strings (#7680)Andrew Reynolds
2021-11-23Add kinds to python docs (#7672)Gereon Kremer
2021-11-23Push output language inside the printing code (#7683)Gereon Kremer
2021-11-23Add rewrite rule for bag.card operator using bag.map and lambda (#7643)mudathirmahgoub
2021-11-23Python API documentation: terms (#7659)yoni206
2021-11-23Make `node_value.h` not depend on `node_manager.h` (#7676)Andres Noetzli
2021-11-22Refactor IO stream manipulators (#7555)Gereon Kremer
2021-11-22Add rewrite for repeated re.allchar (#7681)Andrew Reynolds
2021-11-22Set proper system processor for arm64 toolchain (#7665)Gereon Kremer
2021-11-22[prop] Remove unused #define in theory proxy (#7670)Haniel Barbosa
2021-11-22Improve error for check theory assertions with model (#7679)Andrew Reynolds
2021-11-21Fix const RE test for internal regexp rv kind (#7678)Andrew Reynolds
2021-11-20bv2int module: translation of more cases (#7653)yoni206
2021-11-19[API] Avoid copying values (#7666)Andres Noetzli
2021-11-19Clean up relationship of metakind and node_manager (#7649)Andres Noetzli
2021-11-19Remove n-ary builder (#7671)Andrew Reynolds
2021-11-19Allow negative denominator for CLN Rationals constructed from string. (#7667)Mathias Preiner
2021-11-18api: Fix categorization of DT kinds in kind maps. (#7668)Aina Niemetz
2021-11-18Refactor CAD option for linear model seed (#7657)Gereon Kremer
2021-11-18[proofs] Fix trace in SatProofManager (#7664)Haniel Barbosa
2021-11-18[proofs] Alethe: Rename DUPLICATED_LITERALS (#7661)Lachnitt
2021-11-18api: Fix kind documentation for BAG_MAKE. (#7663)Aina Niemetz
2021-11-17Improve naming in term canonization when handling HO variables (#7660)Haniel Barbosa
2021-11-17[sat] Fix indentation in "reason" (#7662)Haniel Barbosa
2021-11-17Add documentation for z3py compatibility API (#7652)Gereon Kremer
2021-11-17Preparations for eliminating arithmetic subtyping (#7637)Andrew Reynolds
2021-11-17Revert change and clean datatypes cons candidate generator (#7645)Andrew Reynolds
2021-11-17Implement aggressive pruning in CAD solver (#7650)Gereon Kremer
2021-11-17Update Python packaging infrastructure (#7654)Alex Ozdemir
2021-11-17make default and modes strings instead of enum values (#7656)Gereon Kremer
2021-11-17Fix binding of quoted symbols in `define-fun` (#7655)Andres Noetzli
2021-11-17Remove documentation for --lib-only (#7648)Alex Ozdemir
2021-11-17Update SimpleVC.java (#7647)mudathirmahgoub
2021-11-16Translating API tests to Python — part 1 (#7597)yoni206
2021-11-16Fix compile errors with java examples (#7646)mudathirmahgoub
2021-11-16[proofs] Make sure --proof-check=... is no-op when not checking proofs (#7638)Haniel Barbosa
2021-11-16Refactor `metakind` (#7639)Andres Noetzli
2021-11-15api: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632)Aina Niemetz
2021-11-15[Strings] Minor refactor of eager solver (#7628)Andres Noetzli
2021-11-15Add documentation for theory_bags_type_rules.h (#7642)mudathirmahgoub
2021-11-13Skip `str.code` inferences for sequence eqcs (#7644)Andres Noetzli
2021-11-13Fix type error for rewriting bag.map bag.union_disjoint (#7640)mudathirmahgoub
2021-11-13Add operator set.map to theory of sets (#7641)mudathirmahgoub
2021-11-12bags: Rename kinds with a more consistent naming scheme (#7611)mudathirmahgoub
2021-11-12[proofs] Cancel SYMM in CDProof, throw an error for cyclic proofs during doub...Andrew Reynolds
2021-11-12Fix redundant definitions of `NodeValue::getConst` (#7636)Andres Noetzli
2021-11-12Add some basic rewrites for regular expression intersection (#7629)Andrew Reynolds
2021-11-12Remove `ConstantMap<Rational>` (#7635)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback