projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Implement lazy proof checking modes (#7106)
[cvc5.git] / test /
2021-09-02 Andrew ReynoldsImplement lazy proof checking modes (#7106) tree | commitdiff
2021-09-02 Andres Noetzli[Unit Tests] Fix bags rewrite test (#7114) tree | commitdiff
2021-09-02 Aina Niemetzpp: Derive PreprocessingPass from EnvObj. (#7112) tree | commitdiff
2021-09-02 Aina NiemetzEnable sygus-inst for FP, NIA and NRA. (#7098) tree | commitdiff
2021-09-01 Haniel Barbosa[proof] [sat] Fix lost reference to reason when process... tree | commitdiff
2021-09-01 Andrew ReynoldsPrint response to get-model using the API (#7084) tree | commitdiff
2021-09-01 mudathirmahgoubFixed TestTheoryWhiteBagsRewriter.map failure (#7103) tree | commitdiff
2021-09-01 Andrew ReynoldsFix issues with cyclic proofs due to double SYMM applic... tree | commitdiff
2021-08-31 Gereon KremerMake sure modes are sorted in ModeInfo (#7097) tree | commitdiff
2021-08-31 yoni206bv-to-int-module: implementations and stubs for transla... tree | commitdiff
2021-08-30 Gereon KremerAdd API function to obtain information about a single... tree | commitdiff
2021-08-30 mudathirmahgoubAdd kind BAG_MAP and its type rule to bags (#6503) tree | commitdiff
2021-08-30 Andrew ReynoldsFix proof equality engine for "no-explain" premises... tree | commitdiff
2021-08-30 Andrew ReynoldsFix quantifiers dynamic split module for parametric... tree | commitdiff
2021-08-27 Gereon KremerHandle languages as strings in driver (#7074) tree | commitdiff
2021-08-27 Andrew ReynoldsAdd missing methods to Solver API for models (#7052) tree | commitdiff
2021-08-27 yoni206Add `isNull` to cpp api tests, python api, and python... tree | commitdiff
2021-08-26 Gereon KremerImprove integration of nonlinear arithmetic into the... tree | commitdiff
2021-08-26 Mathias Preinerint2bv: Fix conversion of signed bit-vector values... tree | commitdiff
2021-08-26 Gereon KremerConsolidate language types (#7065) tree | commitdiff
2021-08-24 yoni206bv-to-int: more implementations (#7051) tree | commitdiff
2021-08-23 Andrew ReynoldsPurify substitutions in strings proof reconstruction... tree | commitdiff
2021-08-23 Andrew ReynoldsGeneralize inequality elimination in quantifiers rewrit... tree | commitdiff
2021-08-23 Andrew ReynoldsFix single invocation partition for higher-order (... tree | commitdiff
2021-08-23 Gereon KremerMove options parsing code to main (#7054) tree | commitdiff
2021-08-23 Aina Niemetzapi: Require size argument for mkBitVector. (#6998) tree | commitdiff
2021-08-22 Andrew ReynoldsPrenex quantified formulas with user annotations by... tree | commitdiff
2021-08-20 Andrew ReynoldsSimplify how user-provided quantifier attributes are... tree | commitdiff
2021-08-20 mudathirmahgoubAdd Term.java to the Java API (#6330) tree | commitdiff
2021-08-20 Andrew ReynoldsSupport sygus standard command syntax set-feature ... tree | commitdiff
2021-08-20 Gereon KremerUse Env class in nonlinear extension (#7039) tree | commitdiff
2021-08-18 Andres NoetzliMinor fixes of policy for eliminating quantifiers ... tree | commitdiff
2021-08-17 Andrew ReynoldsFix policy for eliminating quantified formulas (#7017) tree | commitdiff
2021-08-17 Gereon KremerPush Env class into TheoryState (#7012) tree | commitdiff
2021-08-16 Gereon KremerMake Theory class use Env (#7011) tree | commitdiff
2021-08-09 Andrew V. JonesCreate grouping of tests that exercise '--use-approx... tree | commitdiff
2021-08-05 Alex OzdemirNormalize val in BitVector(val_str, base) (#6955) tree | commitdiff
2021-08-05 Andres Noetzli[Unit Tests] Add missing include (#6990) tree | commitdiff
2021-08-05 Andrew ReynoldsFix policy for rewriting string equalities (#6916) tree | commitdiff
2021-08-05 Gereon KremerNo longer call solver constructor with an options objec... tree | commitdiff
2021-08-04 Andrew ReynoldsFix policy for merging subproofs (#6981) tree | commitdiff
2021-08-04 Gereon KremerRefactor managed streams (#6934) tree | commitdiff
2021-08-04 Gereon KremerAdd API function to get list of option names (#6971) tree | commitdiff
2021-08-04 Haniel Barbosa[proof] Add getProof to API and use it in GetProofComma... tree | commitdiff
2021-08-04 Andrew ReynoldsRemove dependencies on smt engine in smt solver (#6965) tree | commitdiff
2021-08-03 Andrew ReynoldsRefactor shared solver to use theory builtin inference... tree | commitdiff
2021-08-02 Aina NiemetzAdd 'REQUIRES: poly' to regression. (#6966) tree | commitdiff
2021-08-02 Mathias Preinerbv: Enable equality engine for bitblast-internal. ... tree | commitdiff
2021-07-30 Gereon KremerAllow changing certain options while solving (#6945) tree | commitdiff
2021-07-29 Haniel Barbosa[proofs] Set BV solver to better proof-producing one... tree | commitdiff
2021-07-29 Andrew ReynoldsIntegrate central equality engine approach into theory... tree | commitdiff
2021-07-28 Gereon KremerOnly use libedit on tty inputs (#6946) tree | commitdiff
2021-07-27 Andrew ReynoldsRevert change to regression (#6940) tree | commitdiff
2021-07-27 Andres NoetzliAdd regression for fixed `str.indexof_re` issue (#6938) tree | commitdiff
2021-07-27 Andrew ReynoldsMinor changes from proof-new (#6937) tree | commitdiff
2021-07-26 Gereon KremerMove public options functions to separate file (#6671) tree | commitdiff
2021-07-23 Aina NiemetzFP: Add option to word-blast more lazily. (#6904) tree | commitdiff
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
next