projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Fix component contains for splicing due to substring. (#4705)
[cvc5.git] / test / regress / CMakeLists.txt
2020-08-01 Andrew ReynoldsFix component contains for splicing due to substring... blob | commitdiff | raw
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
2020-04-14 Andrew ReynoldsFix dump-unsat-cores-full (#4303) blob | commitdiff | raw | diff to current
2020-04-13 Andrew ReynoldsFix SyGuS define-fun printing from benchmarks coming... blob | commitdiff | raw | diff to current
2020-04-12 Andrew ReynoldsFixes for extended rewriter (#4278) blob | commitdiff | raw | diff to current
2020-04-12 Andrew ReynoldsMove slow nl regression to regress3 (#4276) blob | commitdiff | raw | diff to current
2020-04-11 Andrew ReynoldsEnsure exported sygus solutions match grammar (#4270) blob | commitdiff | raw | diff to current
2020-04-09 Andrew ReynoldsDisable slow sygus regression (#4232) blob | commitdiff | raw | diff to current
2020-04-08 mudathirmahgoubAdded CHOOSE operator for sets (#4211) blob | commitdiff | raw | diff to current
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) blob | commitdiff | raw | diff to current
2020-04-08 Andrew ReynoldsFix dump models and dump proofs (#4230) blob | commitdiff | raw | diff to current
2020-04-07 Andrew ReynoldsDisable slow regression (#4221) blob | commitdiff | raw | diff to current
2020-04-03 Andrew ReynoldsOnly rewrite lambdas via array representations when... blob | commitdiff | raw | diff to current
2020-04-01 Andrew ReynoldsSupport char smt-lib syntax (#4188) blob | commitdiff | raw | diff to current
2020-03-30 Andrew ReynoldsSupport indexed operators re.loop and re.^ (#4167) blob | commitdiff | raw | diff to current
2020-03-30 mudathirmahgoubFrontend support for the choice operator (#4175) blob | commitdiff | raw | diff to current
2020-03-27 Andres NoetzliFix issues with unsat cores and reset-assertions (... blob | commitdiff | raw | diff to current
2020-03-27 Andrew ReynoldsSupport unicode internal representation and escape... blob | commitdiff | raw | diff to current
2020-03-26 Andrew ReynoldsDisable slow regression (#4157) blob | commitdiff | raw | diff to current
2020-03-24 yoni206Int2BV fail on demand (#4079) blob | commitdiff | raw | diff to current
2020-03-23 Andrew ReynoldsSimplify auxiliary variable handling in CEGQI (#4141) blob | commitdiff | raw | diff to current
2020-03-22 Andrew ReynoldsSort inference does not handle APPLY_UF when higher... blob | commitdiff | raw | diff to current
2020-03-20 Andrew ReynoldsFix variable shadowing issue in sygus-inference (#4121) blob | commitdiff | raw | diff to current
2020-03-20 Andrew ReynoldsGuard cases of sort inference in quantifier free logics... blob | commitdiff | raw | diff to current
2020-03-20 Andrew ReynoldsDo not assign higher-order representative if function... blob | commitdiff | raw | diff to current
2020-03-19 yoni206Bv2int fail on demand blob | commitdiff | raw | diff to current
2020-03-19 Andres NoetzliOnly apply testConstStringInRegExp to const regexp... blob | commitdiff | raw | diff to current
2020-03-19 Andres NoetzliOnly allow bv2nat/int2bv with BV and integer logic... blob | commitdiff | raw | diff to current
2020-03-19 Andrew ReynoldsFix issue with multiple infinities in CEGQI for LIRA... blob | commitdiff | raw | diff to current
2020-03-16 Andres NoetzliCreate master equality engine at context level 0 (... blob | commitdiff | raw | diff to current
2020-03-13 Andrew ReynoldsRemove regress for real to int (#4071) blob | commitdiff | raw | diff to current
2020-03-12 Andrew ReynoldsDo not allow quantifiers over real variables in real... blob | commitdiff | raw | diff to current
2020-03-12 Andrew ReynoldsDo not make models for quantified function variables... blob | commitdiff | raw | diff to current
2020-03-12 Aina NiemetzNew C++ API: Remove support for (reset). (#4037) blob | commitdiff | raw | diff to current
2020-03-12 Andrew ReynoldsFix double notify in equality engine (#4036) blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsDo not enable some SMT-COMP specific options by default... blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsGuard against null relevancy condition in SyGuS (#4033) blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsSwitch to Nodes for conjecture generator (#4026) blob | commitdiff | raw | diff to current
2020-03-11 Andres Noetzlireset-assertions: Update TheoryEngine's PropEngine... blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsFix non-parametrized operators in subgoal generation... blob | commitdiff | raw | diff to current
2020-03-11 Andrew ReynoldsFix duplicate variable issue in sygus-qe-preproc (... blob | commitdiff | raw | diff to current
next