projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
pow2 -- final changes (#6800)
[cvc5.git] / src / theory /
2021-06-26 yoni206pow2 -- final changes (#6800) tree | commitdiff
2021-06-25 yoni206pow2: Adding monotonicity lemma (#6793) tree | commitdiff
2021-06-24 Andrew ReynoldsFix linear arithmetic for duplicate lemmas in increment... tree | commitdiff
2021-06-24 Gereon KremerAdd CoCoA implementation (#6733) tree | commitdiff
2021-06-23 yoni206pow2: more implementations (#6756) tree | commitdiff
2021-06-23 Aina NiemetzFP: Remove sections guarded with undefined macro SYMFPU... tree | commitdiff
2021-06-22 Andrew ReynoldsAvoid full normalization of lambdas in getValue (#6787) tree | commitdiff
2021-06-22 yoni206modular bv2int: Stubs and some implementations (#6760) tree | commitdiff
2021-06-22 Andrew ReynoldsMinor simplification to equality engine notifications... tree | commitdiff
2021-06-22 Andrew ReynoldsAlways check legal eliminations in quantified logics... tree | commitdiff
2021-06-22 Andrew ReynoldsFix type enumeration for non first-class sorts in FMF... tree | commitdiff
2021-06-22 Andrew ReynoldsFix cases of ITE within regular expressions (#6783) tree | commitdiff
2021-06-22 Andrew ReynoldsSet up fine grained equality notifications (#6734) tree | commitdiff
2021-06-21 Mathias PreinerFix model issues with --bitblast=eager. (#6753) tree | commitdiff
2021-06-21 Mathias PreinerMove cnfConversionTime statistic to CnfStream. (#6769) tree | commitdiff
2021-06-18 Andres NoetzliFix build without libpoly (#6759) tree | commitdiff
2021-06-16 Aina NiemetzMake symfpu a required dependency. (#6749) tree | commitdiff
2021-06-15 yoni206pow2: adding a kind, inference rules, and some implemen... tree | commitdiff
2021-06-15 Gereon KremerRemove public option wrappers (#6716) tree | commitdiff
2021-06-13 Andrew ReynoldsMinor simplifications to LogicInfo (#6737) tree | commitdiff
2021-06-11 Haniel BarbosaBetter support for HOL parsing and set up (#6697) tree | commitdiff
2021-06-11 Gereon KremerAdd skeleton for new Lazard evaluation (#6732) tree | commitdiff
2021-06-11 Andrew ReynoldsRemove support for lazy BV extended function reductions... tree | commitdiff
2021-06-10 Andrew ReynoldsEnsure bv2nat and int2bv are not rewritten when using... tree | commitdiff
2021-06-09 Andres NoetzliReorder ITE rewrites (#6723) tree | commitdiff
2021-06-08 Andrew ReynoldsFix for 2 dimensional dependent bounded quantifiers... tree | commitdiff
2021-06-08 Andrew ReynoldsMake TheoryUF compatible with central equality engine... tree | commitdiff
2021-06-08 Andrew ReynoldsFix str.update reduction (#6696) tree | commitdiff
2021-06-07 Andrew Reynolds(proof-new) Fix missing connection in trust substitutio... tree | commitdiff
2021-06-07 Gereon KremerRemove `Options::wasSetByUser()` (#6682) tree | commitdiff
2021-06-07 Andrew Reynolds(proof-new) Lazy proof chain debug names (#6680) tree | commitdiff
2021-06-05 Andres NoetzliRemove unwanted side effects in `SPLIT_EQ_STRIP_L`... tree | commitdiff
2021-06-04 Andrew ReynoldsMiscellaneous changes from central ee branch (#6687) tree | commitdiff
2021-06-04 yoni206pow2: header file for pow2 solver (#6676) tree | commitdiff
2021-06-04 Mathias Preinerbv: Enable bitblast solver by default. (#6660) tree | commitdiff
2021-06-04 Andres NoetzliFix handling of start index in `str.indexof_re` (#6674) tree | commitdiff
2021-06-02 Andres NoetzliRemove option to ignore negative memberships (#6665) tree | commitdiff
2021-06-02 Aina NiemetzRemove redundant logic ALL_SUPPORTED. (#6664) tree | commitdiff
2021-06-02 Andres NoetzliMake `STRINGS_CTN_DECOMPOSE` an explicit conflict ... tree | commitdiff
2021-06-02 Gereon KremerMove public wrapper functions out of options class... tree | commitdiff
2021-06-02 Gereon KremerFix issues with double negation in circuit propagator... tree | commitdiff
2021-06-02 Gereon KremerFix issues when poly is disabled (#6668) tree | commitdiff
2021-06-01 Andrew ReynoldsUse top-level substitutions in ITE simp (#6651) tree | commitdiff
2021-05-31 Andres NoetzliCompute model values for nested sequences in order... tree | commitdiff
2021-05-29 Gereon KremerRemove `Options::set()` method (#6556) tree | commitdiff
2021-05-28 Andres Noetzli`STRINGS_CTN_DECOMPOSE`: Avoid multiple conflicts ... tree | commitdiff
2021-05-27 Andrew ReynoldsFix regular expression aggressive elim (#6627) tree | commitdiff
2021-05-27 Andres NoetzliFix `str.replace_re` and `str.replace_re_all` (#6615) tree | commitdiff
2021-05-27 Andrew ReynoldsUpdate proof namespaces (#6614) tree | commitdiff
2021-05-27 Andrew ReynoldsFix CEGQI for datatypes with Boolean subfields (#6630) tree | commitdiff
2021-05-27 Aina NiemetzFP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD... tree | commitdiff
2021-05-27 Andres NoetzliReturn `REWRITE_AGAIN` after rewriting bvcomp (#6624) tree | commitdiff
2021-05-26 Andres Noetzli More precise includes of `Node` constants (#6617) tree | commitdiff
2021-05-24 Andrew ReynoldsFix non-fixed length case in re-elim (#6612) tree | commitdiff
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611) tree | commitdiff
2021-05-24 Andrew ReynoldsFix re-elim length requirement for symbolic RE membersh... tree | commitdiff
2021-05-24 Andrew ReynoldsFix instance of no rewrite in extended rewriter (#6610) tree | commitdiff
2021-05-24 Andrew ReynoldsBetter formalization of regular expression unfolding... tree | commitdiff
2021-05-21 Andrew ReynoldsFix and refactor relevant domain (#6528) tree | commitdiff
2021-05-21 Andrew ReynoldsMinor simplification to boolean proof checker (#6590) tree | commitdiff
2021-05-21 Andrew Reynolds(proof-new) Minor documentation sync (#6592) tree | commitdiff
2021-05-21 Andrew ReynoldsUpdate to sygus standard output for check-synth respons... tree | commitdiff
2021-05-21 Andres NoetzliSupport braced-init-lists with `mkNode()` (#6580) tree | commitdiff
2021-05-21 Aina NiemetzBV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589) tree | commitdiff
2021-05-20 Haniel BarbosaRemove old unsat cores (#6581) tree | commitdiff
2021-05-20 Alex OzdemirExpand arith's farkas lemma rule as a macro (#6577) tree | commitdiff
2021-05-19 Andrew ReynoldsPass empty vector when constructing re empty, fixes... tree | commitdiff
2021-05-19 Andrew ReynoldsMake strings emp inference an unhandled inference for... tree | commitdiff
2021-05-19 Andrew ReynoldsFix strings rewriter for non-standard re range (#6570) tree | commitdiff
2021-05-19 Andrew ReynoldsAdd more missing inference ids (#6313) tree | commitdiff
2021-05-19 Mathias Preinerbv: Add support for --bitblast=eager. (#6516) tree | commitdiff
2021-05-19 Andrew ReynoldsFix positive contains indexof rewrites for empty string... tree | commitdiff
2021-05-19 Andrew ReynoldsFix handling of non-standard re.range terms (#6563) tree | commitdiff
2021-05-18 Abdalrhman MohamedLoop over terms to reconstruct instead of obligations... tree | commitdiff
2021-05-18 Andres NoetzliFix `collectEmptyEqs()` in string utils (#6562) tree | commitdiff
2021-05-18 Andrew Reynolds(proof-new) Miscellaneous updates to strings from proof... tree | commitdiff
2021-05-17 Andres NoetzliFix `SPLIT_EQ_STRIP_R`/`SPLIT_EQ_STRIP_L` rewrites... tree | commitdiff
2021-05-17 Gereon KremerImprove integration of CAD with nl-Ext (#6542) tree | commitdiff
2021-05-14 Mathias Preinerbv: Assert input facts on user-level 0. (#6515) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-05-12 Andrew ReynoldsEnsure sequences of Booleans generate Boolean term... tree | commitdiff
2021-05-10 Andrew ReynoldsUnify top-level substitutions and model substitutions... tree | commitdiff
2021-05-08 Andrew ReynoldsAdd support for datatype update (#6449) tree | commitdiff
2021-05-07 Andrew ReynoldsSimplifications to expand definitions (#6487) tree | commitdiff
2021-05-06 Haniel Barbosa[proof-new] Updating documentation for Subs/Rw ids... tree | commitdiff
2021-05-06 Andrew ReynoldsDiscard duplicate terms in patterns (#6501) tree | commitdiff
2021-05-06 Andrew ReynoldsUse constant folding for evaluating BV eager atom ... tree | commitdiff
2021-05-05 Andrew ReynoldsDo not have quantifiers model inherit from theory model... tree | commitdiff
2021-05-04 Andrew ReynoldsMove env into smt solver, theory engine, prop engine... tree | commitdiff
2021-05-04 Aina NiemetzFP: Move removal of generic to_fp operations to rewrite... tree | commitdiff
2021-05-04 Aina NiemetzFP: Move type check from expandDefinitions. (#6479) tree | commitdiff
2021-05-03 Aina NiemetzFP: Rewrite to_fp conversion from signed bit-vector... tree | commitdiff
2021-04-30 Mathias Preinerbv: Refactor ppAssert and move to TheoryBV. (#6470) tree | commitdiff
2021-04-30 Aina NiemetzAdd parameter name for argument `isPreRewrite` for... tree | commitdiff
2021-04-30 Andrew ReynoldsUse substitutions for implementing defined functions... tree | commitdiff
2021-04-29 Gereon KremerAvoid exponential explosion of small constant in CEGQI... tree | commitdiff
2021-04-28 Gereon KremerRemove exception headers from options.h (#6456) tree | commitdiff
2021-04-27 Andrew ReynoldsAdd internal support for datatype update (#6450) tree | commitdiff
2021-04-27 Andrew ReynoldsFix refutational soundness bug in quantifier prenexing... tree | commitdiff
2021-04-27 Aina NiemetzBool: Move implementation of type rules to cpp. (#6420) tree | commitdiff
next