projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Simplify computation of relevant terms in datatypes (#6885)
[cvc5.git] / test /
2021-07-22 Andres NoetzliAdd support for minimal unsat cores (#4605) tree | commitdiff
2021-07-22 mudathirmahgoubAdd std::vector<Term> Op:: getIndices() and operator... tree | commitdiff
2021-07-16 Andres Noetzli[Unit Tests] Avoid linking against external libs (... tree | commitdiff
2021-07-16 Andres Noetzli[Unit Tests] Reenable `top_scope_context_obj` (#6892) tree | commitdiff
2021-07-15 Mathias Preinerbv: Rename lazy solver to layered solver. (#6889) tree | commitdiff
2021-07-15 Mathias Preinerbv: Rename simple solver to bitblast-internal. (#6888) tree | commitdiff
2021-07-14 Haniel Barbosa[proof] Fix open proof issues in SAT proof (#6887) tree | commitdiff
2021-07-14 Haniel BarbosaAdd option that exercises the previously buggy behavior... tree | commitdiff
2021-07-14 Andrew ReynoldsFix for context on input proof generator (#6873) tree | commitdiff
2021-07-14 Gereon KremerClean up option usage in command executor (#6844) tree | commitdiff
2021-07-14 Mathias PreinerAdd missing space for check macro error messages. ... tree | commitdiff
2021-07-13 Haniel Barbosa[rewriter] Add rewrite to order IFF (equality for Boole... tree | commitdiff
2021-07-12 Andrew ReynoldsFix for learned rewrite pass, add regression (#6850) tree | commitdiff
2021-07-09 Haniel Barbosatest also with default cores (#6858) tree | commitdiff
2021-07-09 Andres NoetzliMake regression test `issue4971-0` more robust (#6857) tree | commitdiff
2021-07-09 Andrew ReynoldsFix sets cardinality inference involving equivalent... tree | commitdiff
2021-07-08 Andrew ReynoldsDisable ordering heuristic for justification by default... tree | commitdiff
2021-07-07 Haniel Barbosa[unsat cores] Adding regressions from #4971 (#6852) tree | commitdiff
2021-07-07 Aina NiemetzRename operator pow2 to int.pow2. (#6849) tree | commitdiff
2021-07-07 Andrew ReynoldsFix regressions for competition build (#6846) tree | commitdiff
2021-07-06 Gereon KremerIntegrate Lazard into CAD module (#6812) tree | commitdiff
2021-07-05 Andres Noetzli[Strings] Fix incorrect rewrite (#6837) tree | commitdiff
2021-07-03 Andres NoetzliFix performance of string regression (#6832) tree | commitdiff
2021-07-03 Mathias PreinerAdd output tags -o, --output. (#6826) tree | commitdiff
2021-07-02 Mathias PreinerFix bv assert input reset assertions (#6820) tree | commitdiff
2021-07-02 Andrew ReynoldsFix rewriter for negative constant seq.nth (#6827) tree | commitdiff
2021-07-02 Andres NoetzliAdd reverse iterators to `Node`/`TNode` (#6825) tree | commitdiff
2021-07-01 Andrew ReynoldsAdd recursive function definitions to subsolver in... tree | commitdiff
2021-06-30 Mathias PreinerUse SAT context level for --bv-assert-input instead... tree | commitdiff
2021-06-30 yoni206pow2: new test (#6819) tree | commitdiff
2021-06-30 Andrew ReynoldsDo not apply fmfBound to standard quantifiers when... tree | commitdiff
2021-06-30 Andrew ReynoldsFix pre vs. post-rewrite in proofs for theory preproces... tree | commitdiff
2021-06-30 yoni206int-to-bv: correct model values (#6811) tree | commitdiff
2021-06-28 yoni206Rewrite POW to POW2 when the base is 2 (#6806) tree | commitdiff
2021-06-28 Andrew ReynoldsRename internal string kinds to match API (#6797) tree | commitdiff
2021-06-26 yoni206pow2 -- final changes (#6800) tree | commitdiff
2021-06-24 Aina Niemetzapi: getRealValue: Fix printing of integer values.... tree | commitdiff
2021-06-24 Andrew ReynoldsFix linear arithmetic for duplicate lemmas in increment... tree | commitdiff
2021-06-23 Haniel Barbosa[hol] Disable bound fmf when HOL (#6792) tree | commitdiff
2021-06-23 Haniel Barbosa[regressions] Adding regression from #5371 (#6791) tree | commitdiff
2021-06-23 Haniel Barbosa[parser] [hol] Fix parser check for allowing functions... tree | commitdiff
2021-06-22 Andrew ReynoldsAvoid full normalization of lambdas in getValue (#6787) tree | commitdiff
2021-06-22 yoni206python api unit tests for Op (#6785) 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 yoni206Python api unit tests for Result (#6763) tree | commitdiff
2021-06-21 Andres Noetzli[Attributes] Remove parameter `context_dependent` ... tree | commitdiff
2021-06-21 Mathias PreinerFix model issues with --bitblast=eager. (#6753) tree | commitdiff
2021-06-21 mudathirmahgoubAdd Grammar.java to the java API (#6388) tree | commitdiff
2021-06-21 Mathias PreinerMake CaDiCaL a required dependency. (#6761) tree | commitdiff
2021-06-19 Ying ShengAdding python API test part 5 (#6743) tree | commitdiff
2021-06-18 Mathias PreinerMake CnfStream::toCNF iterative (#6757) 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 Ouyancheng[Optimization] Use Result in OptimizationResult (#6740) tree | commitdiff
2021-06-15 Gereon KremerRemove public option wrappers (#6716) tree | commitdiff
2021-06-11 Haniel BarbosaBetter support for HOL parsing and set up (#6697) 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 NoetzliMake `--solve-int-as-bv=X` robust to rewriting (#6722) tree | commitdiff
2021-06-09 Andres NoetzliReorder ITE rewrites (#6723) tree | commitdiff
2021-06-09 Ouyancheng[Optimization] support for push/pop (#6706) tree | commitdiff
2021-06-09 Gereon KremerRequire statistics for regression (#6714) tree | commitdiff
2021-06-08 Andrew ReynoldsFix for 2 dimensional dependent bounded quantifiers... tree | commitdiff
2021-06-08 Gereon KremerFix statistics option handler (#6703) tree | commitdiff
2021-06-08 Gereon KremerRemove `binary_name` option (#6693) tree | commitdiff
2021-06-08 Alex OzdemirChange output of getRealValue to a fraction. (#6692) 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-05 Andres NoetzliRemove unwanted side effects in `SPLIT_EQ_STRIP_L`... 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-03 yoni206Adding unit tests for the datatypes python API (#6658) tree | commitdiff
2021-06-03 yoni206Renaming pow2 to p2 in regression tests (#6675) tree | commitdiff
2021-06-02 Andres NoetzliRemove option to ignore negative memberships (#6665) tree | commitdiff
2021-06-02 yoni206Adding getters to the python API and testing them ... tree | commitdiff
2021-06-02 Aina NiemetzRemove redundant logic ALL_SUPPORTED. (#6664) tree | commitdiff
2021-06-02 yoni206Move `toPythonObj` tests to the new API unit test direc... tree | commitdiff
2021-06-02 Andrew ReynoldsFix unsat core proofs (#6655) 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-01 yoni206Some additions to the datatypes python API (#6640) tree | commitdiff
2021-06-01 Andrew ReynoldsDisable timeout regressions (#6650) tree | commitdiff
2021-06-01 yoni206FP value support in python API (#6644) tree | commitdiff
2021-05-31 yoni206Update `toPythonObj` to use new getters -- part 1 ... 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 Ouyancheng(Optimization) remove popObjective, add resetObjectives... tree | commitdiff
2021-05-28 yoni206Python API: bugfix + translating tests from cpp unit... tree | commitdiff
2021-05-28 Andres NoetzliDisable `--jh-rlv-order` for slow regressions (#6633) 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 OuyanchengAdd Lexicographic + Pareto Optimizations (#6626) 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 Andrew ReynoldsFix spurious assertion for trivial abduction (#6629) tree | commitdiff
2021-05-27 Andres NoetzliReturn `REWRITE_AGAIN` after rewriting bvcomp (#6624) tree | commitdiff
next