Simplify the syntax and representation of the separation logic empty heap constraint...
[cvc5.git] / test /
2021-09-30 Andrew ReynoldsSimplify the syntax and representation of the separatio...
2021-09-29 Abdalrhman MohamedRemove support for extended `(check-sat <term>)` comman...
2021-09-29 Andrew ReynoldsProperly restrict PBE symmetry breaking for abduction...
2021-09-29 Andrew ReynoldsUpdate the syntax for tuples in smt2 (#7265)
2021-09-29 Gereon Kremerremove stuff (#7258)
2021-09-29 mudathirmahgoubAdd Sort.java to the java API (#6382)
2021-09-24 Andrew ReynoldsEliminate calls to Rewriter::rewrite from strings entai...
2021-09-23 Andrew ReynoldsImplement alpha equivalence proofs (#7066)
2021-09-22 Mathias PreinerRemove CVC language support (#7219)
2021-09-22 Andrew ReynoldsTowards standard usage of evaluator (#7189)
2021-09-22 OuyanchengFix solver_black unit test (#7233)
2021-09-22 Andrew ReynoldsMinimal fixing version for tuple update parsing (#7228)
2021-09-21 Andres NoetzliFix handling of conversions between FP and reals (...
2021-09-17 Andres NoetzliUse a single `NodeManager` per thread (#7204)
2021-09-14 Andrew ReynoldsAdd get-difficulty to the API (#7194)
2021-09-14 Andres NoetzliMake `-o raw-benchmark` work with `--parse-only` (...
2021-09-14 Andrew ReynoldsSupport sygus version 2.1 command assume (#7081)
2021-09-14 Mathias Preinerproofs: Properly track pre- and post-rewrites in bbAtom...
2021-09-14 Andrew ReynoldsReimplement `--dump=raw-benchmark` as `-o raw-benchmark...
2021-09-13 Gereon KremerAdd Solver::isOutputOn() (#7187)
2021-09-11 Gereon KremerUse StatisticsRegistry from Env (#7166)
2021-09-11 Mathias Preinerbv: Move IsPowerOfTwo rule to preprocessing pass and...
2021-09-10 Aina NiemetzFP: Do not send trivial lemmas. (#7167)
2021-09-10 mudathirmahgoubAdd Op.java to the java API (#6387)
2021-09-10 Andres NoetzliUse C++17 attributes (#7154)
2021-09-09 Aina Niemetzpp passes: Use EnvObj::rewrite() instead of Rewriter...
2021-09-09 Andrew ReynoldsDisable shared selectors for quantified logics without...
2021-09-08 Gereon KremerA couple of minor cleanups (#7141)
2021-09-08 Andrew ReynoldsTowards standard usage of ExtendedRewriter (#7145)
2021-09-08 mudathirmahgoubAdd Datatype.java to the Java API (#6389)
2021-09-07 Andrew ReynoldsRefactoring and fixes of set defaults for quantifiers...
2021-09-02 Andres Noetzli[Unit Tests] Fix shell test for Editline (#7117)
2021-09-02 Aina NiemetzDisable sygus-inst for regression close to time limit...
2021-09-02 Gereon KremerAdd API check whether option in getOptionInfo() exists...
2021-09-02 Gereon KremerDriver & Options cleanup (#7109)
2021-09-02 Andrew ReynoldsImplement lazy proof checking modes (#7106)
2021-09-02 Andres Noetzli[Unit Tests] Fix bags rewrite test (#7114)
2021-09-02 Aina Niemetzpp: Derive PreprocessingPass from EnvObj. (#7112)
2021-09-02 Aina NiemetzEnable sygus-inst for FP, NIA and NRA. (#7098)
2021-09-01 Haniel Barbosa[proof] [sat] Fix lost reference to reason when process...
2021-09-01 Andrew ReynoldsPrint response to get-model using the API (#7084)
2021-09-01 mudathirmahgoubFixed TestTheoryWhiteBagsRewriter.map failure (#7103)
2021-09-01 Andrew ReynoldsFix issues with cyclic proofs due to double SYMM applic...
2021-08-31 Gereon KremerMake sure modes are sorted in ModeInfo (#7097)
2021-08-31 yoni206bv-to-int-module: implementations and stubs for transla...
2021-08-30 Gereon KremerAdd API function to obtain information about a single...
2021-08-30 mudathirmahgoubAdd kind BAG_MAP and its type rule to bags (#6503)
2021-08-30 Andrew ReynoldsFix proof equality engine for "no-explain" premises...
2021-08-30 Andrew ReynoldsFix quantifiers dynamic split module for parametric...
2021-08-27 Gereon KremerHandle languages as strings in driver (#7074)
2021-08-27 Andrew ReynoldsAdd missing methods to Solver API for models (#7052)
2021-08-27 yoni206Add `isNull` to cpp api tests, python api, and python...
2021-08-26 Gereon KremerImprove integration of nonlinear arithmetic into the...
2021-08-26 Mathias Preinerint2bv: Fix conversion of signed bit-vector values...
2021-08-26 Gereon KremerConsolidate language types (#7065)
2021-08-24 yoni206bv-to-int: more implementations (#7051)
2021-08-23 Andrew ReynoldsPurify substitutions in strings proof reconstruction...
2021-08-23 Andrew ReynoldsGeneralize inequality elimination in quantifiers rewrit...
2021-08-23 Andrew ReynoldsFix single invocation partition for higher-order (...
2021-08-23 Gereon KremerMove options parsing code to main (#7054)
2021-08-23 Aina Niemetzapi: Require size argument for mkBitVector. (#6998)
2021-08-22 Andrew ReynoldsPrenex quantified formulas with user annotations by...
2021-08-20 Andrew ReynoldsSimplify how user-provided quantifier attributes are...
2021-08-20 mudathirmahgoubAdd Term.java to the Java API (#6330)
2021-08-20 Andrew ReynoldsSupport sygus standard command syntax set-feature ...
2021-08-20 Gereon KremerUse Env class in nonlinear extension (#7039)
2021-08-18 Andres NoetzliMinor fixes of policy for eliminating quantifiers ...
2021-08-17 Andrew ReynoldsFix policy for eliminating quantified formulas (#7017)
2021-08-17 Gereon KremerPush Env class into TheoryState (#7012)
2021-08-16 Gereon KremerMake Theory class use Env (#7011)
2021-08-09 Andrew V. JonesCreate grouping of tests that exercise '--use-approx...
2021-08-05 Alex OzdemirNormalize val in BitVector(val_str, base) (#6955)
2021-08-05 Andres Noetzli[Unit Tests] Add missing include (#6990)
2021-08-05 Andrew ReynoldsFix policy for rewriting string equalities (#6916)
2021-08-05 Gereon KremerNo longer call solver constructor with an options objec...
2021-08-04 Andrew ReynoldsFix policy for merging subproofs (#6981)
2021-08-04 Gereon KremerRefactor managed streams (#6934)
2021-08-04 Gereon KremerAdd API function to get list of option names (#6971)
2021-08-04 Haniel Barbosa[proof] Add getProof to API and use it in GetProofComma...
2021-08-04 Andrew ReynoldsRemove dependencies on smt engine in smt solver (#6965)
2021-08-03 Andrew ReynoldsRefactor shared solver to use theory builtin inference...
2021-08-02 Aina NiemetzAdd 'REQUIRES: poly' to regression. (#6966)
2021-08-02 Mathias Preinerbv: Enable equality engine for bitblast-internal. ...
2021-07-30 Gereon KremerAllow changing certain options while solving (#6945)
2021-07-29 Haniel Barbosa[proofs] Set BV solver to better proof-producing one...
2021-07-29 Andrew ReynoldsIntegrate central equality engine approach into theory...
2021-07-28 Gereon KremerOnly use libedit on tty inputs (#6946)
2021-07-27 Andrew ReynoldsRevert change to regression (#6940)
2021-07-27 Andres NoetzliAdd regression for fixed `str.indexof_re` issue (#6938)
2021-07-27 Andrew ReynoldsMinor changes from proof-new (#6937)
2021-07-26 Gereon KremerMove public options functions to separate file (#6671)
2021-07-23 Aina NiemetzFP: Add option to word-blast more lazily. (#6904)
2021-07-22 Andres NoetzliAdd support for minimal unsat cores (#4605)
2021-07-22 mudathirmahgoubAdd std::vector<Term> Op:: getIndices() and operator...
2021-07-16 Andres Noetzli[Unit Tests] Avoid linking against external libs (...
2021-07-16 Andres Noetzli[Unit Tests] Reenable `top_scope_context_obj` (#6892)
2021-07-15 Mathias Preinerbv: Rename lazy solver to layered solver. (#6889)
2021-07-15 Mathias Preinerbv: Rename simple solver to bitblast-internal. (#6888)
2021-07-14 Haniel Barbosa[proof] Fix open proof issues in SAT proof (#6887)
2021-07-14 Haniel BarbosaAdd option that exercises the previously buggy behavior...
next