projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
bv2int: implementing the iand-sum mode (#5265)
[cvc5.git] / test / regress / CMakeLists.txt
2020-10-14 yoni206bv2int: implementing the iand-sum mode (#5265) blob | commitdiff | raw
2020-10-14 yoni206bv2int: rewritings and unsat cores (#5263) blob | commitdiff | raw | diff to current
2020-10-12 Andrew ReynoldsRemove uf-ss-totality option (#5251) blob | commitdiff | raw | diff to current
2020-10-12 Andrew ReynoldsEnsure uninterpreted sort owner is UF if uf-ho or finit... blob | commitdiff | raw | diff to current
2020-10-09 Andres Noetzlireset-assertions: Remove all non-global symbols in... blob | commitdiff | raw | diff to current
2020-10-07 Gereon KremerMake sure conflicts are not rewritten (in arithmetic... blob | commitdiff | raw | diff to current
2020-10-06 yoni206bv-to-int: change order of passes (#5208) blob | commitdiff | raw | diff to current
2020-09-29 Andrew ReynoldsReset assertions on resetAssertions (#5153) blob | commitdiff | raw | diff to current
2020-09-29 Andrew ReynoldsDisable regression that is timing out (#5142) blob | commitdiff | raw | diff to current
2020-09-27 Andrew ReynoldsFix sygus quantifier elimination preprocess for multipl... blob | commitdiff | raw | diff to current
2020-09-26 Andrew ReynoldsUse original quantified formula for single invocation... blob | commitdiff | raw | diff to current
2020-09-24 Andrew ReynoldsModify lemma vs fact policy for datatype equalities... blob | commitdiff | raw | diff to current
2020-09-23 Andrew ReynoldsDisable cegqi-bv when using sygus (#5124) blob | commitdiff | raw | diff to current
2020-09-23 yoni206bv2int: new options for bvand translation (#5096) blob | commitdiff | raw | diff to current
2020-09-23 Andrew ReynoldsAllow E-matching by default when strings are enabled... blob | commitdiff | raw | diff to current
2020-09-23 Abdalrhman MohamedRefactor Commands to use the Public API. (#5105) blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... blob | commitdiff | raw | diff to current
2020-09-18 yoni206bv2int: quantifiers support (#5080) blob | commitdiff | raw | diff to current
2020-09-18 Andres Noetzli[Strings] Fix extended equality rewriter (#5092) blob | commitdiff | raw | diff to current
2020-09-17 yoni206Dumping internal define-funs with no arguments (#5077) blob | commitdiff | raw | diff to current
2020-09-15 Andrew ReynoldsFix needsModel method for CEGQI (#5048) blob | commitdiff | raw | diff to current
2020-09-15 Ying ShengInterpolation: Add implementation for SyGuS interpolati... blob | commitdiff | raw | diff to current
2020-09-14 Andrew ReynoldsRefactoring the rewriter of sets (#4856) blob | commitdiff | raw | diff to current
2020-09-10 yoni206bv2int: improvement in lazy failures (#5020) blob | commitdiff | raw | diff to current
2020-09-09 Andrew ReynoldsFixes for regular expressions + sygus (#5044) blob | commitdiff | raw | diff to current
2020-09-09 mudathirmahgoubAdd is_singleton operator to the theory of sets (#5033) blob | commitdiff | raw | diff to current
2020-09-08 Andres NoetzliMake CVC/API BV div/mod semantics match SMT-LIB (#4997) blob | commitdiff | raw | diff to current
2020-09-03 Gereon KremerAdded a new rule to simplify (bvugt (bvurem T x) x... blob | commitdiff | raw | diff to current
2020-09-01 Haniel BarbosaRemoves old proof code (#4964) blob | commitdiff | raw | diff to current
2020-08-31 Gereon KremerFix --ackermann in the presence on syntactically differ... blob | commitdiff | raw | diff to current
2020-08-28 yoni206Incremental support for bv_to_int (#4967) blob | commitdiff | raw | diff to current
2020-08-24 Mathias PreinerIncrease regress level to 2 for production build. ... blob | commitdiff | raw | diff to current
2020-08-21 Andrew ReynoldsSimplify and fix care graph for ufHo (#4924) blob | commitdiff | raw | diff to current
2020-08-19 Andres NoetzliRequire `--strings-exp` when using `str.substr` (#4916) blob | commitdiff | raw | diff to current
2020-08-19 Andres Noetzli[Regressions] Do not test `--check-proofs` anymore... blob | commitdiff | raw | diff to current
2020-08-19 Gereon KremerFix SmtEngine::reset() (#4917) blob | commitdiff | raw | diff to current
2020-08-12 Andrew ReynoldsFixes for degenerate case of sygus decision tree learni... blob | commitdiff | raw | diff to current
2020-08-05 Gereon KremerImprove error message for unsupported exponents (#4852) blob | commitdiff | raw | diff to current
2020-08-02 Andres NoetzliEnsure strict length constraint for decompose rule... blob | commitdiff | raw | diff to current
2020-08-01 Andrew ReynoldsFix component contains for splicing due to substring... blob | commitdiff | raw | diff to current
2020-07-28 Andrew ReynoldsFix regular expression delta for complement (#4765) blob | commitdiff | raw | diff to current
2020-07-28 yoni206Supporting seq.nth (#4723) blob | commitdiff | raw | diff to current
2020-07-27 Alex OzdemirConsider negation's proof before triggering arith pfs... blob | commitdiff | raw | diff to current
2020-07-21 Andrew ReynoldsSupport uninterpreted constants in the evaluator (... blob | commitdiff | raw | diff to current
2020-07-14 Andrew ReynoldsDebug instantiations output (#4739) blob | commitdiff | raw | diff to current
2020-07-14 Andres NoetzliFix caching in TheoryEngine::getExplanation() (#4736) blob | commitdiff | raw | diff to current
2020-07-13 Andrew Reynolds User-facing print debug option for sygus candidates... blob | commitdiff | raw | diff to current
2020-07-13 Andrew ReynoldsStatistics on instantiations per quantified formula... blob | commitdiff | raw | diff to current
2020-07-13 Andrew ReynoldsAdd support for string/sequence update (#4725) blob | commitdiff | raw | diff to current
2020-07-10 Andrew ReynoldsFront end support for integer AND (#4717) blob | commitdiff | raw | diff to current
2020-07-10 Andrew ReynoldsEnsure legal elimination for witness rewrite (#4688) blob | commitdiff | raw | diff to current
2020-07-06 Andrew ReynoldsFront end support for sequences (#4690) blob | commitdiff | raw | diff to current
2020-06-30 Andrew ReynoldsFix normal form for re.comp (#4676) blob | commitdiff | raw | diff to current
2020-06-30 Andrew ReynoldsSimplify quantifiers strategy for when to apply last... blob | commitdiff | raw | diff to current
2020-06-28 Andrew ReynoldsFix non-termination issues in simpleRegExpConsume ... blob | commitdiff | raw | diff to current
2020-06-24 Andres Noetzli[unconstrained] Fix gathering of visited-once vars... blob | commitdiff | raw | diff to current
2020-06-23 Mathias PreinerAdd support for eqrange predicate (#4562) blob | commitdiff | raw | diff to current
2020-06-19 yoni206Bv to int elimination bugfix (#4435) blob | commitdiff | raw | diff to current
2020-06-19 Andres NoetzliAdd logic check for define-fun(s)-rec (#4577) blob | commitdiff | raw | diff to current
2020-06-17 Andrew ReynoldsDo not traverse WITNESS for partial substitutions in... blob | commitdiff | raw | diff to current
2020-06-16 Aina NiemetzBV: Fix querying equality status in lazy bit-blaster... blob | commitdiff | raw | diff to current
2020-06-15 Aina NiemetzBV: Add missing type check for BITVECTOR_REPEAT_OP... blob | commitdiff | raw | diff to current
2020-06-15 Aina NiemetzBV: Add missing type check for INT_TO_BITVECTOR. (... blob | commitdiff | raw | diff to current
2020-06-15 Andrew Reynolds Do RE derivation inference only for concrete constant... blob | commitdiff | raw | diff to current
2020-06-11 Andrew Reynolds(proof-new) Remove arith-snorm option. (#4591) blob | commitdiff | raw | diff to current
2020-06-10 Andres NoetzliAdd support for str.replace_re/str.replace_re_all ... blob | commitdiff | raw | diff to current
2020-06-06 Andres NoetzliFix destruction order in NodeManager (#4578) blob | commitdiff | raw | diff to current
2020-06-06 Andres NoetzliKeep definitions when global-declarations enabled ... blob | commitdiff | raw | diff to current
2020-06-06 Andrew ReynoldsSmt2 parsing support for nested recursive datatypes... blob | commitdiff | raw | diff to current
2020-06-05 Andres NoetzliFix handling of Boolean term variables (#4550) blob | commitdiff | raw | diff to current
2020-06-04 Andrew ReynoldsFix abduction with datatypes (#4566) blob | commitdiff | raw | diff to current
2020-06-03 Andrew ReynoldsDo not apply unconstrained simplification when quantifi... blob | commitdiff | raw | diff to current
2020-06-02 Andrew ReynoldsFix scope issue with pulling ITEs in extended rewriter... blob | commitdiff | raw | diff to current
2020-06-02 Andrew ReynoldsDo not handle universal quantification on functions... blob | commitdiff | raw | diff to current
2020-06-01 Andres NoetzliSet theoryof-mode after theory widening (#4545) blob | commitdiff | raw | diff to current
2020-06-01 Andres NoetzliDo not parse ->/lambda unless --uf-ho enabled (#4544) blob | commitdiff | raw | diff to current
2020-05-31 Andres NoetzliDo not cache operator eliminations in arith (#4542) blob | commitdiff | raw | diff to current
2020-05-26 MartinFix an incorrect limit in conversion from real to float... blob | commitdiff | raw | diff to current
2020-05-23 Andrew ReynoldsRefactor operator elimination in arithmetic (#4519) blob | commitdiff | raw | diff to current
2020-05-22 Andrew Reynolds(proof-new) Add rewrite corresponding to regular expres... blob | commitdiff | raw | diff to current
2020-05-21 Andrew ReynoldsFix missing check for cardinality one in unconstrained... blob | commitdiff | raw | diff to current
2020-05-20 Andrew ReynoldsNormal form equality conflicts and uniqueness check... blob | commitdiff | raw | diff to current
2020-05-20 Andrew ReynoldsFix parametric datatype instantiation (#4493) blob | commitdiff | raw | diff to current
2020-05-20 Andrew ReynoldsDo not eliminate variables that are equal to unevaluata... blob | commitdiff | raw | diff to current
2020-05-20 Andrew ReynoldsFix cached free variable identifiers in sygus term... blob | commitdiff | raw | diff to current
2020-05-19 mudathirmahgoubRenamed operator CHOICE to WITNESS (#4207) blob | commitdiff | raw | diff to current
2020-05-19 Andres NoetzliMake SolveEq and PlusCombineLikeTerms idempotent (... blob | commitdiff | raw | diff to current
2020-05-05 Andrew ReynoldsAlways introduce fresh variable for unconstrained APPLY... blob | commitdiff | raw | diff to current
2020-05-02 Andrew ReynoldsMove slow regression to regress3 (#4430) blob | commitdiff | raw | diff to current
2020-04-30 Andrew ReynoldsRemove skolem share involving pre_first_ctn. (#4423) blob | commitdiff | raw | diff to current
2020-04-29 Andrew ReynoldsAvoid circular dependencies for justifying reductions... blob | commitdiff | raw | diff to current
2020-04-28 Andrew ReynoldsUpdate cardinality in strings to unicode standard ... blob | commitdiff | raw | diff to current
2020-04-26 Andrew Reynolds Fix sets cardinality cycle rule (#4392) blob | commitdiff | raw | diff to current
2020-04-22 Andrew ReynoldsEnsure disequality splits are processed as lemmas ... blob | commitdiff | raw | diff to current
2020-04-22 Andres NoetzliReinstantiate support for conjunctions in facts (#4377) blob | commitdiff | raw | diff to current
2020-04-17 Mathias PreinerSyGuS instantiation quantifiers module (#3910) blob | commitdiff | raw | diff to current
2020-04-15 Andrew ReynoldsDo not normalize to representatives for variable equali... blob | commitdiff | raw | diff to current
2020-04-15 Andrew ReynoldsAlways assign function values in higher order (#4279) blob | commitdiff | raw | diff to current
2020-04-15 Andrew ReynoldsDisable preregistration of instantiations for cegqi... blob | commitdiff | raw | diff to current
2020-04-14 Andrew ReynoldsRemove a few spurious assertions (#4294) blob | commitdiff | raw | diff to current
next